1 (* ========================================================================= *)
2 (* Church-Rosser property for combinatory logic (S and K combinators). *)
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: *)
8 (* http://www.comlab.ox.ac.uk/tom.melham/pub/Camilleri-1992-RID.pdf *)
9 (* ========================================================================= *)
11 needs "Examples/reduct.ml";;
13 (* ------------------------------------------------------------------------- *)
14 (* Definition of confluence. *)
15 (* ------------------------------------------------------------------------- *)
17 let confluent = define
19 !x y z. RTC R x y /\ RTC R x z ==> ?u. RTC R y u /\ RTC R z u`;;
21 let confluent_diamond_RTC = prove
22 (`!R. confluent R <=> CR(RTC R)`,
23 REWRITE_TAC[confluent; CR]);;
25 (* ------------------------------------------------------------------------- *)
26 (* Basic term structure: S and K combinators and function application ("%"). *)
27 (* ------------------------------------------------------------------------- *)
29 parse_as_infix("%",(20,"left"));;
31 let cl_INDUCT,cl_RECURSION = define_type "cl = S | K | % cl cl";;
33 (* ------------------------------------------------------------------------- *)
34 (* Reduction relation. *)
35 (* ------------------------------------------------------------------------- *)
37 parse_as_infix("-->",(12,"right"));;
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))`;;
45 (* ------------------------------------------------------------------------- *)
46 (* A different, "parallel", reduction relation. *)
47 (* ------------------------------------------------------------------------- *)
49 parse_as_infix("-||->",(12,"right"));;
51 let predn_rules, predn_ind, predn_cases = new_inductive_definition
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))`;;
57 (* ------------------------------------------------------------------------- *)
58 (* Abbreviations for their reflexive-transitive closures. *)
59 (* ------------------------------------------------------------------------- *)
61 parse_as_infix("-->*",(12,"right"));;
62 parse_as_infix("-||->*",(12,"right"));;
64 let RTCredn = define `(-->*) = RTC(-->)`;;
65 let RTCpredn = define `(-||->*) = RTC(-||->)`;;
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);;
72 (* ------------------------------------------------------------------------- *)
73 (* Prove that the two RTCs are actually the same. *)
74 (* ------------------------------------------------------------------------- *)
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]);;
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]);;
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]);;
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]);;
94 let RTCpredn_EQ_RTCredn = prove
96 REWRITE_TAC[FUN_EQ_THM] THEN MESON_TAC[RTCpredn_RTCredn; RTCredn_RTCpredn]);;
98 (* ------------------------------------------------------------------------- *)
99 (* Now prove diamond property for "-||->" reduction. *)
100 (* ------------------------------------------------------------------------- *)
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);;
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`]);;
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`]);;
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]);;
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]);;
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]);;
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]]);;
152 let predn_diamond = prove
154 MESON_TAC[CR; predn_diamond_lemma]);;
156 (* ------------------------------------------------------------------------- *)
157 (* Hence we have confluence of the main reduction. *)
158 (* ------------------------------------------------------------------------- *)
160 let confluent_redn = prove
162 MESON_TAC[confluent_diamond_RTC; RTCpredn_EQ_RTCredn; RTCredn; RTCpredn;
163 RTC_CR; predn_diamond]);;