author | clasohm |
Tue, 30 Jan 1996 13:42:57 +0100 | |
changeset 1461 | 6bcb44e4d6e5 |
parent 782 | 200a16083201 |
child 1692 | 5324be24a5fa |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/comb.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson |
0 | 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 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
26 |
bind_thm ("contract_induct", |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
27 |
(contract.mutual_induct RS spec RS spec RSN (2,rev_mp))); |
515 | 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 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
38 |
bind_thm ("reduction_refl", |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
39 |
(field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl)); |
515 | 40 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
41 |
bind_thm ("rtrancl_into_rtrancl2", |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
42 |
(r_into_rtrancl RS (trans_rtrancl RS transD))); |
515 | 43 |
|
44 |
val reduction_rls = [reduction_refl, contract.K, contract.S, |
|
1461 | 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]; |
|
515 | 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)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
53 |
qed "reduce_I"; |
515 | 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 |
|
1461 | 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; |
|
515 | 72 |
|
73 |
goalw Comb.thy [I_def] "!!r. I -1-> r ==> P"; |
|
74 |
by (fast_tac contract_cs 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
75 |
qed "I_contract_E"; |
515 | 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); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
79 |
qed "K1_contractD"; |
515 | 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); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
88 |
qed "Ap_reduce1"; |
515 | 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); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
97 |
qed "Ap_reduce2"; |
515 | 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)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
103 |
qed "KIII_contract1"; |
515 | 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)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
107 |
qed "KIII_contract2"; |
515 | 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)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
111 |
qed "KIII_contract3"; |
515 | 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); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
116 |
qed "not_diamond_contract"; |
515 | 117 |
|
0 | 118 |
|
119 |
||
515 | 120 |
(*** Results about Parallel Contraction ***) |
121 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
122 |
bind_thm ("parcontract_induct", |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
123 |
(parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp))); |
515 | 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] |
|
1461 | 132 |
addSEs [parcontract_combE2]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
133 |
qed "field_parcontract_eq"; |
515 | 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 |
|
1461 | 142 |
addIs parcontract.intrs |
143 |
addSEs [Ap_E, K_parcontractE, S_parcontractE, |
|
144 |
Ap_parcontractE] |
|
145 |
addSEs [parcontract_combD1, parcontract_combD2] (*type checking*) |
|
515 | 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); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
152 |
qed "K1_parcontractD"; |
515 | 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); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
156 |
qed "S1_parcontractD"; |
515 | 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); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
161 |
qed "S2_parcontractD"; |
515 | 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]))); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
169 |
qed "diamond_parcontract"; |
515 | 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] |
|
1461 | 179 |
addIs [r_into_trancl, trans_trancl RS transD]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
180 |
qed "diamond_trancl_lemma"; |
515 | 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^+)"; |
|
1461 | 185 |
by (rewtac diamond_def); (*unfold only in goal, not in premise!*) |
515 | 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] |
|
1461 | 190 |
addEs [major RS diamond_lemmaE]))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
191 |
qed "diamond_trancl"; |
515 | 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))); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
199 |
qed "contract_imp_parcontract"; |
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, |
|
1461 | 207 |
r_into_trancl, trans_trancl RS transD]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
208 |
qed "reduce_imp_parreduce"; |
515 | 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); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
230 |
qed "parreduce_imp_reduce"; |
515 | 231 |
|
232 |
goal Comb.thy "p===>q <-> p--->q"; |
|
233 |
by (REPEAT (ares_tac [iffI, parreduce_imp_reduce, reduce_imp_parreduce] 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
234 |
qed "parreduce_iff_reduce"; |
515 | 235 |
|
236 |
writeln"Reached end of file."; |