1open HolKernel Parse boolLib
2
3open bossLib simpLib
4
5val _ = new_theory "cl";
6
7val _ = (hide "S"; hide "K")
8val _ = Datatype `cl = S | K | # cl cl`;
9
10val _ = set_fixity "#"  (Infixl 1100);
11
12val _ = set_mapped_fixity {tok = "-->", fixity = Infix(NONASSOC, 450),
13                           term_name = "redn"}
14
15val (redn_rules, _, _) = Hol_reln `
16    (!x y f. x --> y   ==>    f # x --> f # y) /\
17    (!f g x. f --> g   ==>    f # x --> g # x) /\
18    (!x y.   K # x # y --> x) /\
19    (!f g x. S # f # g # x --> (f # x) # (g # x))`;
20
21val _ = hide "RTC";
22
23val (RTC_rules, _, RTC_cases) = Hol_reln `
24    (!x.     RTC R x x) /\
25    (!x y z. R x y /\ RTC R y z ==> RTC R x z)`;
26
27val confluent_def = Define`
28  confluent R =
29     !x y z. RTC R x y /\ RTC R x z ==>
30             ?u. RTC R y u /\ RTC R z u`;
31
32val normform_def = Define `normform R x = !y. ~R x y`;
33
34
35val confluent_normforms_unique = store_thm(
36  "confluent_normforms_unique",
37  ``!R. confluent R ==>
38        !x y z. RTC R x y /\ normform R y /\ RTC R x z /\ normform R z
39                  ==>
40                (y = z)``,
41  rw[confluent_def] >>
42  `?u. RTC R y u /\ RTC R z u` by metis_tac [] >>
43  metis_tac [normform_def, RTC_cases]);
44
45val diamond_def = Define
46    `diamond R = !x y z. R x y /\ R x z ==> ?u. R y u /\ R z u`;
47
48val confluent_diamond_RTC = store_thm(
49  "confluent_diamond_RTC",
50  ``!R. confluent R = diamond (RTC R)``,
51  rw[confluent_def, diamond_def]);
52
53val R_RTC_diamond = store_thm(
54  "R_RTC_diamond",
55  ``!R. diamond R ==>
56         !x p. RTC R x p ==>
57               !z. R x z ==>
58                   ?u. RTC R p u /\ RTC R z u``,
59  GEN_TAC >> STRIP_TAC >> Induct_on `RTC` >>
60  metis_tac [diamond_def,RTC_rules]);
61
62val RTC_RTC = store_thm(
63  "RTC_RTC",
64  ``!R x y z. RTC R x y /\ RTC R y z ==> RTC R x z``,
65  SIMP_TAC std_ss [GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] >>
66  GEN_TAC >> Induct_on `RTC` >> metis_tac [RTC_rules]);
67
68val diamond_RTC_lemma = prove(
69  ``!R.
70       diamond R ==>
71       !x y. RTC R x y ==> !z. RTC R x z ==>
72                               ?u. RTC R y u /\ RTC R z u``,
73  GEN_TAC >> STRIP_TAC >> Induct_on `RTC` >> rw[] >| [
74    metis_tac[RTC_rules],
75    `?v. RTC R x' v /\ RTC R z v` by metis_tac[R_RTC_diamond] >>
76    metis_tac [RTC_RTC, RTC_rules]
77  ]);
78
79val diamond_RTC = store_thm(
80  "diamond_RTC",
81  ``!R. diamond R ==> diamond (RTC R)``,
82  metis_tac [diamond_def,diamond_RTC_lemma]);
83
84val _ = set_mapped_fixity {tok = "-||->", fixity = Infix(NONASSOC, 450),
85                           term_name = "predn"}
86val (predn_rules, predn_ind, predn_cases) = Hol_reln `
87  (!x. x -||-> x) /\
88  (!x y u v. x -||-> y /\ u -||-> v ==> x # u -||-> y # v) /\
89  (!x y. K # x # y -||-> x) /\
90  (!f g x. S # f # g # x -||-> (f # x) # (g # x))
91`;
92
93val RTC_monotone = store_thm(
94  "RTC_monotone",
95  ``!R1 R2. (!x y. R1 x y ==> R2 x y) ==>
96            (!x y. RTC R1 x y ==> RTC R2 x y)``,
97  rpt GEN_TAC >> STRIP_TAC >> Induct_on `RTC` >>
98  rpt STRIP_TAC >> metis_tac [RTC_rules]);
99
100val _ = set_fixity "-->*" (Infix(NONASSOC, 450));
101val _ = overload_on ("-->*", ``RTC redn``)
102
103val _ = set_fixity "-||->*" (Infix(NONASSOC, 450));
104val _ = overload_on ("-||->*", ``RTC predn``)
105
106val RTCredn_RTCpredn = store_thm(
107  "RTCredn_RTCpredn",
108  ``!x y. x -->* y   ==>   x -||->* y``,
109  HO_MATCH_MP_TAC RTC_monotone >> Induct_on `x --> y` >>
110  metis_tac [predn_rules]);
111
112val RTCredn_ap_congruence = store_thm(
113  "RTCredn_ap_congruence",
114  ``!x y. x -->* y ==> !z. x # z -->* y # z /\ z # x -->* z # y``,
115  Induct_on `RTC` >> metis_tac [RTC_rules, redn_rules]);
116
117val predn_RTCredn = store_thm(
118  "predn_RTCredn",
119  ``!x y. x -||-> y  ==>  x -->* y``,
120  Induct_on `x -||-> y` >>
121  metis_tac [RTC_rules,redn_rules,RTC_RTC,RTCredn_ap_congruence]);
122
123val RTCpredn_RTCredn = store_thm(
124  "RTCpredn_RTCredn",
125  ``!x y. x -||->* y   ==>  x -->* y``,
126  Induct_on `RTC` >> metis_tac [predn_RTCredn, RTC_RTC, RTC_rules]);
127
128val RTCpredn_EQ_RTCredn = store_thm(
129  "RTCpredn_EQ_RTCredn",
130  ``$-||->* = $-->*``,
131  SIMP_TAC std_ss [FUN_EQ_THM] >>
132  metis_tac [RTCpredn_RTCredn, RTCredn_RTCpredn]);
133
134fun characterise t = SIMP_RULE (srw_ss()) [] (SPEC t predn_cases);
135
136val K_predn = characterise ``K``;
137val S_predn = characterise ``S``;
138val Sx_predn0 = characterise ``S # x``;
139
140val Sx_predn = prove(
141  ``!x y. S # x -||-> y = ?z. (y = S # z) /\ (x -||-> z)``,
142  rw[Sx_predn0, predn_rules, S_predn, EQ_IMP_THM]);
143
144val Kx_predn = prove(
145  ``!x y. K # x -||-> y = ?z. (y = K # z) /\ (x -||-> z)``,
146  rw[characterise ``K # x``, predn_rules, K_predn, EQ_IMP_THM]);
147
148val Kxy_predn = prove(
149  ``!x y z. K # x # y -||-> z =
150            (?u v. (z = K # u # v) /\ (x -||-> u) /\ (y -||-> v)) \/
151            (z = x)``,
152  rw[characterise ``K # x # y``, predn_rules, Kx_predn, EQ_IMP_THM]);
153
154
155val Sxy_predn = prove(
156  ``!x y z. S # x # y -||-> z =
157            ?u v. (z = S # u # v) /\ (x -||-> u) /\ (y -||-> v)``,
158  rw[characterise ``S # x # y``, predn_rules, EQ_IMP_THM,
159     S_predn, Sx_predn]);
160
161val Sxyz_predn = prove(
162  ``!w x y z. S # w # x # y -||-> z =
163              (?p q r. (z = S # p # q # r) /\
164                       w -||-> p /\ x -||-> q /\ y -||-> r) \/
165              (z = (w # y) # (x # y))``,
166  rw[characterise ``S # w # x # y``, predn_rules, Sxy_predn, EQ_IMP_THM]);
167
168val x_ap_y_predn = characterise ``x # y``;
169
170val predn_diamond_lemma = prove(
171  ``!x y. x -||-> y ==>
172          !z. x -||-> z ==> ?u. y -||-> u /\ z -||-> u``,
173  Induct_on `x -||-> y` >> rpt conj_tac >| [
174    metis_tac [predn_rules],
175    rw[] >>
176    qpat_x_assum `_ # _ -||-> _`
177      (strip_assume_tac o SIMP_RULE std_ss [x_ap_y_predn]) >>
178    rw[] >| [
179      metis_tac[predn_rules],
180      metis_tac[predn_rules],
181      `?w. (y = K # w) /\ (z -||-> w)` by metis_tac [Kx_predn] >>
182      rw[] >> metis_tac [predn_rules],
183      `?p q. (y = S # p # q) /\ (f -||-> p) /\ (g -||-> q)` by
184         metis_tac [Sxy_predn] >>
185      rw[] >> metis_tac [predn_rules]
186    ],
187    rw[Kxy_predn] >> metis_tac [predn_rules],
188    rw[Sxyz_predn] >> metis_tac [predn_rules]
189  ]);
190
191val predn_diamond = store_thm(
192  "predn_diamond",
193  ``diamond predn``,
194  metis_tac [diamond_def, predn_diamond_lemma]);
195
196val confluent_redn = store_thm(
197  "confluent_redn",
198  ``confluent redn``,
199  metis_tac [predn_diamond, confluent_diamond_RTC,
200             RTCpredn_EQ_RTCredn, diamond_RTC]);
201
202
203val _ = export_theory();
204