Examples/combin.ml

   1 (* ========================================================================= *)
   2 (* Church-Rosser property for combinatory logic (S and K combinators).       *)
   3 (*                                                                           *)
   4 (* This is adapted from a HOL4 develoment, itself derived from an old HOL88  *)
   5 (* example by Tom Melham and Juanito Camilleri. For a detailed discussion,   *)
   6 (* see pp. 29-39 of the following paper:                                     *)
   7 (*                                                                           *)
   8 (*    http://www.comlab.ox.ac.uk/tom.melham/pub/Camilleri-1992-RID.pdf       *)
   9 (* ========================================================================= *)
  10
  11 needs "Examples/reduct.ml";;
  12
  13 (* ------------------------------------------------------------------------- *)
  14 (* Definition of confluence.                                                 *)
  15 (* ------------------------------------------------------------------------- *)
  16
  17 let confluent = define
  18   `confluent R <=>
  19         !x y z. RTC R x y /\ RTC R x z ==> ?u. RTC R y u /\ RTC R z u`;;
  20
  21 let confluent_diamond_RTC = prove
  22  (`!R. confluent R <=> CR(RTC R)`,
  23   REWRITE_TAC[confluent; CR]);;
  24
  25 (* ------------------------------------------------------------------------- *)
  26 (* Basic term structure: S and K combinators and function application ("%"). *)
  27 (* ------------------------------------------------------------------------- *)
  28
  29 parse_as_infix("%",(20,"left"));;
  30
  31 let cl_INDUCT,cl_RECURSION = define_type "cl = S | K | % cl cl";;
  32
  33 (* ------------------------------------------------------------------------- *)
  34 (* Reduction relation.                                                       *)
  35 (* ------------------------------------------------------------------------- *)
  36
  37 parse_as_infix("-->",(12,"right"));;
  38
  39 let redn_rules, redn_ind, redn_cases = new_inductive_definition
  40  `(!x y f. x --> y   ==>    f % x --> f % y) /\
  41   (!f g x. f --> g   ==>    f % x --> g % x) /\
  42   (!x y.   K % x % y --> x) /\
  43   (!f g x. S % f % g % x --> (f % x) % (g % x))`;;
  44
  45 (* ------------------------------------------------------------------------- *)
  46 (* A different, "parallel", reduction relation.                              *)
  47 (* ------------------------------------------------------------------------- *)
  48
  49 parse_as_infix("-||->",(12,"right"));;
  50
  51 let predn_rules, predn_ind, predn_cases = new_inductive_definition
  52  `(!x. x -||-> x) /\
  53   (!x y u v. x -||-> y /\ u -||-> v ==> x % u -||-> y % v) /\
  54   (!x y. K % x % y -||-> x) /\
  55   (!f g x. S % f % g % x -||-> (f % x) % (g % x))`;;
  56
  57 (* ------------------------------------------------------------------------- *)
  58 (* Abbreviations for their reflexive-transitive closures.                    *)
  59 (* ------------------------------------------------------------------------- *)
  60
  61 parse_as_infix("-->*",(12,"right"));;
  62 parse_as_infix("-||->*",(12,"right"));;
  63
  64 let RTCredn = define `(-->*) = RTC(-->)`;;
  65 let RTCpredn = define `(-||->*) = RTC(-||->)`;;
  66
  67 let RTCredn_rules  = REWRITE_RULE[SYM RTCredn]  (ISPEC `(-->)` RTC_RULES);;
  68 let RTCredn_ind    = REWRITE_RULE[SYM RTCredn]  (ISPEC `(-->)` RTC_INDUCT);;
  69 let RTCpredn_rules = REWRITE_RULE[SYM RTCpredn] (ISPEC `(-||->)` RTC_RULES);;
  70 let RTCpredn_ind   = REWRITE_RULE[SYM RTCpredn] (ISPEC `(-||->)` RTC_INDUCT);;
  71
  72 (* ------------------------------------------------------------------------- *)
  73 (* Prove that the two RTCs are actually the same.                            *)
  74 (* ------------------------------------------------------------------------- *)
  75
  76 let RTCredn_RTCpredn = prove
  77  (`!x y. x -->* y ==> x -||->* y`,
  78   REWRITE_TAC[RTCredn; RTCpredn] THEN MATCH_MP_TAC RTC_MONO THEN
  79   MATCH_MP_TAC redn_ind THEN MESON_TAC[predn_rules]);;
  80
  81 let RTCredn_ap_monotonic = prove
  82  (`!x y. x -->* y ==> !z. x % z -->* y % z /\ z % x -->* z % y`,
  83   MATCH_MP_TAC RTCredn_ind THEN MESON_TAC[RTCredn_rules; redn_rules]);;
  84
  85 let predn_RTCredn = prove
  86  (`!x y. x -||-> y ==> x -->* y`,
  87   MATCH_MP_TAC predn_ind THEN
  88   MESON_TAC[RTCredn_rules; redn_rules; RTCredn_ap_monotonic]);;
  89
  90 let RTCpredn_RTCredn = prove
  91  (`!x y. x -||->* y ==> x -->* y`,
  92   MATCH_MP_TAC RTCpredn_ind THEN MESON_TAC[predn_RTCredn; RTCredn_rules]);;
  93
  94 let RTCpredn_EQ_RTCredn = prove
  95  (`(-||->*) = (-->*)`,
  96   REWRITE_TAC[FUN_EQ_THM] THEN MESON_TAC[RTCpredn_RTCredn; RTCredn_RTCpredn]);;
  97
  98 (* ------------------------------------------------------------------------- *)
  99 (* Now prove diamond property for "-||->" reduction.                         *)
 100 (* ------------------------------------------------------------------------- *)
 101
 102 let characterise t =
 103   SIMP_RULE[distinctness "cl"; injectivity "cl"; GSYM EXISTS_REFL;
 104             RIGHT_EXISTS_AND_THM; GSYM CONJ_ASSOC; UNWIND_THM1]
 105    (SPEC t predn_cases);;
 106
 107 let Sx_PREDN = prove
 108  (`!x y. S % x -||-> y <=> ?z. y = S % z /\ x -||-> z`,
 109   REWRITE_TAC[characterise `S % x`] THEN
 110   MESON_TAC[predn_rules; characterise `S`]);;
 111
 112 let Kx_PREDN = prove
 113  (`!x y. K % x -||-> y <=> ?z. y = K % z /\ x -||-> z`,
 114   REWRITE_TAC[characterise `K % x`] THEN
 115   MESON_TAC[predn_rules; characterise `K`]);;
 116
 117 let Kxy_PREDN = prove
 118  (`!x y z. K % x % y -||-> z <=>
 119             (?u v. z = K % u % v /\ x -||-> u /\ y -||-> v) \/ z = x`,
 120   REWRITE_TAC[characterise `K % x % y`] THEN
 121   MESON_TAC[predn_rules; Kx_PREDN]);;
 122
 123 let Sxy_PREDN = prove
 124  (`!x y z. S % x % y -||-> z <=>
 125             ?u v. z = S % u % v /\ x -||-> u /\ y -||-> v`,
 126   REWRITE_TAC[characterise `S % x % y`] THEN
 127   MESON_TAC[predn_rules; characterise `S`; Sx_PREDN]);;
 128
 129 let Sxyz_PREDN = prove
 130  (`!w x y z. S % w % x % y -||-> z <=>
 131               (?p q r. z = S % p % q % r /\
 132                        w -||-> p /\ x -||-> q /\ y -||-> r) \/
 133               z = (w % y) % (x % y)`,
 134   REWRITE_TAC[characterise `S % w % x % y`] THEN
 135   MESON_TAC[predn_rules; Sxy_PREDN]);;
 136
 137 let predn_diamond_lemma = prove
 138  (`!x y. x -||-> y ==> !z. x -||-> z ==> ?u. y -||-> u /\ z -||-> u`,
 139   ONCE_REWRITE_TAC[TAUT `a ==> b <=> a ==> a /\ b`] THEN
 140   MATCH_MP_TAC predn_ind THEN SIMP_TAC[predn_rules] THEN REPEAT CONJ_TAC THENL
 141    [MESON_TAC[predn_rules];
 142     REPEAT STRIP_TAC THEN UNDISCH_THEN `x % u -||-> z`
 143      (STRIP_ASSUME_TAC o SIMP_RULE[characterise `x % y`]) THENL
 144      [ASM_MESON_TAC[predn_rules];
 145       ASM_MESON_TAC[predn_rules];
 146       SUBGOAL_THEN `?w. y = K % w /\ z -||-> w` MP_TAC;
 147       SUBGOAL_THEN `?p q. y = S % p % q /\ f -||-> p /\ g -||-> q` MP_TAC] THEN
 148     ASM_MESON_TAC[Kx_PREDN; Sxy_PREDN; predn_rules];
 149     REWRITE_TAC[Kxy_PREDN] THEN MESON_TAC[predn_rules];
 150     REWRITE_TAC[Sxyz_PREDN] THEN MESON_TAC[predn_rules]]);;
 151
 152 let predn_diamond = prove
 153  (`CR (-||->)`,
 154   MESON_TAC[CR; predn_diamond_lemma]);;
 155
 156 (* ------------------------------------------------------------------------- *)
 157 (* Hence we have confluence of the main reduction.                           *)
 158 (* ------------------------------------------------------------------------- *)
 159
 160 let confluent_redn = prove
 161  (`confluent(-->)`,
 162   MESON_TAC[confluent_diamond_RTC; RTCpredn_EQ_RTCredn; RTCredn; RTCpredn;
 163             RTC_CR; predn_diamond]);;