0
|
1 |
(* Title: ZF/ex/comb.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
515
|
6 |
Combinatory Logic example: the Church-Rosser Theorem
|
|
7 |
Curiously, combinators do not include free variables.
|
|
8 |
|
|
9 |
Example taken from
|
|
10 |
J. Camilleri and T. F. Melham.
|
|
11 |
Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
|
|
12 |
Report 265, University of Cambridge Computer Laboratory, 1992.
|
|
13 |
|
|
14 |
HOL system proofs may be found in
|
|
15 |
/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
|
|
16 |
*)
|
|
17 |
|
|
18 |
open Comb;
|
|
19 |
|
|
20 |
val [_,_,comb_Ap] = comb.intrs;
|
|
21 |
val Ap_E = comb.mk_cases comb.con_defs "p#q : comb";
|
|
22 |
|
|
23 |
|
|
24 |
(*** Results about Contraction ***)
|
|
25 |
|
|
26 |
val contract_induct = standard
|
|
27 |
(contract.mutual_induct RS spec RS spec RSN (2,rev_mp));
|
|
28 |
|
|
29 |
(*For type checking: replaces a-1->b by a,b:comb *)
|
|
30 |
val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2;
|
|
31 |
val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1;
|
|
32 |
val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2;
|
|
33 |
|
|
34 |
goal Comb.thy "field(contract) = comb";
|
|
35 |
by (fast_tac (ZF_cs addIs [equalityI,contract.K] addSEs [contract_combE2]) 1);
|
760
|
36 |
qed "field_contract_eq";
|
515
|
37 |
|
|
38 |
val reduction_refl = standard
|
|
39 |
(field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl);
|
|
40 |
|
|
41 |
val rtrancl_into_rtrancl2 = standard
|
|
42 |
(r_into_rtrancl RS (trans_rtrancl RS transD));
|
|
43 |
|
|
44 |
val reduction_rls = [reduction_refl, contract.K, contract.S,
|
|
45 |
contract.K RS rtrancl_into_rtrancl2,
|
|
46 |
contract.S RS rtrancl_into_rtrancl2,
|
|
47 |
contract.Ap1 RS rtrancl_into_rtrancl2,
|
|
48 |
contract.Ap2 RS rtrancl_into_rtrancl2];
|
|
49 |
|
|
50 |
(*Example only: not used*)
|
|
51 |
goalw Comb.thy [I_def] "!!p. p:comb ==> I#p ---> p";
|
|
52 |
by (REPEAT (ares_tac (comb.intrs @ reduction_rls) 1));
|
|
53 |
val reduce_I = result();
|
|
54 |
|
|
55 |
goalw Comb.thy [I_def] "I: comb";
|
|
56 |
by (REPEAT (ares_tac comb.intrs 1));
|
760
|
57 |
qed "comb_I";
|
515
|
58 |
|
|
59 |
(** Non-contraction results **)
|
0
|
60 |
|
515
|
61 |
(*Derive a case for each combinator constructor*)
|
|
62 |
val K_contractE = contract.mk_cases comb.con_defs "K -1-> r";
|
|
63 |
val S_contractE = contract.mk_cases comb.con_defs "S -1-> r";
|
|
64 |
val Ap_contractE = contract.mk_cases comb.con_defs "p#q -1-> r";
|
|
65 |
|
|
66 |
val contract_cs =
|
|
67 |
ZF_cs addSIs comb.intrs
|
|
68 |
addIs contract.intrs
|
|
69 |
addSEs [contract_combD1,contract_combD2] (*type checking*)
|
|
70 |
addSEs [K_contractE, S_contractE, Ap_contractE]
|
|
71 |
addSEs comb.free_SEs;
|
|
72 |
|
|
73 |
goalw Comb.thy [I_def] "!!r. I -1-> r ==> P";
|
|
74 |
by (fast_tac contract_cs 1);
|
|
75 |
val I_contract_E = result();
|
|
76 |
|
|
77 |
goal Comb.thy "!!p r. K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
|
|
78 |
by (fast_tac contract_cs 1);
|
|
79 |
val K1_contractD = result();
|
|
80 |
|
|
81 |
goal Comb.thy "!!p r. [| p ---> q; r: comb |] ==> p#r ---> q#r";
|
|
82 |
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
|
|
83 |
by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
|
|
84 |
by (etac rtrancl_induct 1);
|
|
85 |
by (fast_tac (contract_cs addIs reduction_rls) 1);
|
|
86 |
by (etac (trans_rtrancl RS transD) 1);
|
|
87 |
by (fast_tac (contract_cs addIs reduction_rls) 1);
|
|
88 |
val Ap_reduce1 = result();
|
|
89 |
|
|
90 |
goal Comb.thy "!!p r. [| p ---> q; r: comb |] ==> r#p ---> r#q";
|
|
91 |
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
|
|
92 |
by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
|
|
93 |
by (etac rtrancl_induct 1);
|
|
94 |
by (fast_tac (contract_cs addIs reduction_rls) 1);
|
|
95 |
by (etac (trans_rtrancl RS transD) 1);
|
|
96 |
by (fast_tac (contract_cs addIs reduction_rls) 1);
|
|
97 |
val Ap_reduce2 = result();
|
|
98 |
|
|
99 |
(** Counterexample to the diamond property for -1-> **)
|
|
100 |
|
|
101 |
goal Comb.thy "K#I#(I#I) -1-> I";
|
|
102 |
by (REPEAT (ares_tac [contract.K, comb_I, comb_Ap] 1));
|
|
103 |
val KIII_contract1 = result();
|
|
104 |
|
|
105 |
goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
|
|
106 |
by (DEPTH_SOLVE (resolve_tac (comb.intrs @ contract.intrs) 1));
|
|
107 |
val KIII_contract2 = result();
|
|
108 |
|
|
109 |
goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
|
|
110 |
by (REPEAT (ares_tac (comb.intrs @ [contract.K, comb_I]) 1));
|
|
111 |
val KIII_contract3 = result();
|
|
112 |
|
|
113 |
goalw Comb.thy [diamond_def] "~ diamond(contract)";
|
|
114 |
by (fast_tac (ZF_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3]
|
|
115 |
addSEs [I_contract_E]) 1);
|
|
116 |
val not_diamond_contract = result();
|
|
117 |
|
0
|
118 |
|
|
119 |
|
515
|
120 |
(*** Results about Parallel Contraction ***)
|
|
121 |
|
|
122 |
val parcontract_induct = standard
|
|
123 |
(parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp));
|
|
124 |
|
|
125 |
(*For type checking: replaces a=1=>b by a,b:comb *)
|
|
126 |
val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2;
|
|
127 |
val parcontract_combD1 = parcontract.dom_subset RS subsetD RS SigmaD1;
|
|
128 |
val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2;
|
|
129 |
|
|
130 |
goal Comb.thy "field(parcontract) = comb";
|
|
131 |
by (fast_tac (ZF_cs addIs [equalityI, parcontract.K]
|
|
132 |
addSEs [parcontract_combE2]) 1);
|
|
133 |
val field_parcontract_eq = result();
|
|
134 |
|
|
135 |
(*Derive a case for each combinator constructor*)
|
|
136 |
val K_parcontractE = parcontract.mk_cases comb.con_defs "K =1=> r";
|
|
137 |
val S_parcontractE = parcontract.mk_cases comb.con_defs "S =1=> r";
|
|
138 |
val Ap_parcontractE = parcontract.mk_cases comb.con_defs "p#q =1=> r";
|
|
139 |
|
|
140 |
val parcontract_cs =
|
|
141 |
ZF_cs addSIs comb.intrs
|
|
142 |
addIs parcontract.intrs
|
|
143 |
addSEs [Ap_E, K_parcontractE, S_parcontractE,
|
|
144 |
Ap_parcontractE]
|
|
145 |
addSEs [parcontract_combD1, parcontract_combD2] (*type checking*)
|
|
146 |
addSEs comb.free_SEs;
|
|
147 |
|
|
148 |
(*** Basic properties of parallel contraction ***)
|
|
149 |
|
|
150 |
goal Comb.thy "!!p r. K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')";
|
|
151 |
by (fast_tac parcontract_cs 1);
|
|
152 |
val K1_parcontractD = result();
|
|
153 |
|
|
154 |
goal Comb.thy "!!p r. S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')";
|
|
155 |
by (fast_tac parcontract_cs 1);
|
|
156 |
val S1_parcontractD = result();
|
|
157 |
|
|
158 |
goal Comb.thy
|
|
159 |
"!!p q r. S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
|
|
160 |
by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1);
|
|
161 |
val S2_parcontractD = result();
|
|
162 |
|
|
163 |
(*Church-Rosser property for parallel contraction*)
|
|
164 |
goalw Comb.thy [diamond_def] "diamond(parcontract)";
|
|
165 |
by (rtac (impI RS allI RS allI) 1);
|
|
166 |
by (etac parcontract_induct 1);
|
|
167 |
by (ALLGOALS
|
|
168 |
(fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
|
|
169 |
val diamond_parcontract = result();
|
|
170 |
|
|
171 |
(*** Transitive closure preserves the Church-Rosser property ***)
|
0
|
172 |
|
515
|
173 |
goalw Comb.thy [diamond_def]
|
|
174 |
"!!x y r. [| diamond(r); <x,y>:r^+ |] ==> \
|
|
175 |
\ ALL y'. <x,y'>:r --> (EX z. <y',z>: r^+ & <y,z>: r)";
|
|
176 |
by (etac trancl_induct 1);
|
|
177 |
by (fast_tac (ZF_cs addIs [r_into_trancl]) 1);
|
|
178 |
by (slow_best_tac (ZF_cs addSDs [spec RS mp]
|
|
179 |
addIs [r_into_trancl, trans_trancl RS transD]) 1);
|
|
180 |
val diamond_trancl_lemma = result();
|
|
181 |
|
|
182 |
val diamond_lemmaE = diamond_trancl_lemma RS spec RS mp RS exE;
|
|
183 |
|
|
184 |
val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)";
|
|
185 |
bw diamond_def; (*unfold only in goal, not in premise!*)
|
|
186 |
by (rtac (impI RS allI RS allI) 1);
|
|
187 |
by (etac trancl_induct 1);
|
|
188 |
by (ALLGOALS
|
|
189 |
(slow_best_tac (ZF_cs addIs [r_into_trancl, trans_trancl RS transD]
|
|
190 |
addEs [major RS diamond_lemmaE])));
|
|
191 |
val diamond_trancl = result();
|
|
192 |
|
|
193 |
|
|
194 |
(*** Equivalence of p--->q and p===>q ***)
|
|
195 |
|
|
196 |
goal Comb.thy "!!p q. p-1->q ==> p=1=>q";
|
|
197 |
by (etac contract_induct 1);
|
|
198 |
by (ALLGOALS (fast_tac (parcontract_cs)));
|
|
199 |
val contract_imp_parcontract = result();
|
0
|
200 |
|
515
|
201 |
goal Comb.thy "!!p q. p--->q ==> p===>q";
|
|
202 |
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
|
|
203 |
by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
|
|
204 |
by (etac rtrancl_induct 1);
|
|
205 |
by (fast_tac (parcontract_cs addIs [r_into_trancl]) 1);
|
|
206 |
by (fast_tac (ZF_cs addIs [contract_imp_parcontract,
|
|
207 |
r_into_trancl, trans_trancl RS transD]) 1);
|
|
208 |
val reduce_imp_parreduce = result();
|
|
209 |
|
0
|
210 |
|
515
|
211 |
goal Comb.thy "!!p q. p=1=>q ==> p--->q";
|
|
212 |
by (etac parcontract_induct 1);
|
|
213 |
by (fast_tac (contract_cs addIs reduction_rls) 1);
|
|
214 |
by (fast_tac (contract_cs addIs reduction_rls) 1);
|
|
215 |
by (fast_tac (contract_cs addIs reduction_rls) 1);
|
|
216 |
by (rtac (trans_rtrancl RS transD) 1);
|
|
217 |
by (ALLGOALS
|
|
218 |
(fast_tac
|
|
219 |
(contract_cs addIs [Ap_reduce1, Ap_reduce2]
|
|
220 |
addSEs [parcontract_combD1,parcontract_combD2])));
|
760
|
221 |
qed "parcontract_imp_reduce";
|
515
|
222 |
|
|
223 |
goal Comb.thy "!!p q. p===>q ==> p--->q";
|
|
224 |
by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1);
|
|
225 |
by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1);
|
|
226 |
by (etac trancl_induct 1);
|
|
227 |
by (etac parcontract_imp_reduce 1);
|
|
228 |
by (etac (trans_rtrancl RS transD) 1);
|
|
229 |
by (etac parcontract_imp_reduce 1);
|
|
230 |
val parreduce_imp_reduce = result();
|
|
231 |
|
|
232 |
goal Comb.thy "p===>q <-> p--->q";
|
|
233 |
by (REPEAT (ares_tac [iffI, parreduce_imp_reduce, reduce_imp_parreduce] 1));
|
|
234 |
val parreduce_iff_reduce = result();
|
|
235 |
|
|
236 |
writeln"Reached end of file.";
|