author | paulson |
Fri, 03 Jan 1997 15:01:55 +0100 | |
changeset 2469 | b50b8c0eec01 |
parent 1732 | 38776e927da8 |
child 2496 | 40efb87985b5 |
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 |
||
26 |
(*For type checking: replaces a-1->b by a,b:comb *) |
|
27 |
val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2; |
|
28 |
val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1; |
|
29 |
val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2; |
|
30 |
||
31 |
goal Comb.thy "field(contract) = comb"; |
|
2469 | 32 |
by (fast_tac (!claset addIs [equalityI,contract.K] addSEs [contract_combE2]) 1); |
760 | 33 |
qed "field_contract_eq"; |
515 | 34 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
35 |
bind_thm ("reduction_refl", |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
36 |
(field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl)); |
515 | 37 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
38 |
bind_thm ("rtrancl_into_rtrancl2", |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
39 |
(r_into_rtrancl RS (trans_rtrancl RS transD))); |
515 | 40 |
|
41 |
val reduction_rls = [reduction_refl, contract.K, contract.S, |
|
1461 | 42 |
contract.K RS rtrancl_into_rtrancl2, |
43 |
contract.S RS rtrancl_into_rtrancl2, |
|
44 |
contract.Ap1 RS rtrancl_into_rtrancl2, |
|
45 |
contract.Ap2 RS rtrancl_into_rtrancl2]; |
|
515 | 46 |
|
47 |
(*Example only: not used*) |
|
48 |
goalw Comb.thy [I_def] "!!p. p:comb ==> I#p ---> p"; |
|
49 |
by (REPEAT (ares_tac (comb.intrs @ reduction_rls) 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
50 |
qed "reduce_I"; |
515 | 51 |
|
52 |
goalw Comb.thy [I_def] "I: comb"; |
|
53 |
by (REPEAT (ares_tac comb.intrs 1)); |
|
760 | 54 |
qed "comb_I"; |
515 | 55 |
|
56 |
(** Non-contraction results **) |
|
0 | 57 |
|
515 | 58 |
(*Derive a case for each combinator constructor*) |
59 |
val K_contractE = contract.mk_cases comb.con_defs "K -1-> r"; |
|
60 |
val S_contractE = contract.mk_cases comb.con_defs "S -1-> r"; |
|
61 |
val Ap_contractE = contract.mk_cases comb.con_defs "p#q -1-> r"; |
|
62 |
||
2469 | 63 |
AddSIs comb.intrs; |
64 |
AddIs contract.intrs; |
|
65 |
AddSEs [contract_combD1,contract_combD2]; (*type checking*) |
|
66 |
AddSEs [K_contractE, S_contractE, Ap_contractE]; |
|
67 |
AddSEs comb.free_SEs; |
|
515 | 68 |
|
69 |
goalw Comb.thy [I_def] "!!r. I -1-> r ==> P"; |
|
2469 | 70 |
by (Fast_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
71 |
qed "I_contract_E"; |
515 | 72 |
|
73 |
goal Comb.thy "!!p r. K#p -1-> r ==> (EX q. r = K#q & p -1-> q)"; |
|
2469 | 74 |
by (Fast_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
75 |
qed "K1_contractD"; |
515 | 76 |
|
77 |
goal Comb.thy "!!p r. [| p ---> q; r: comb |] ==> p#r ---> q#r"; |
|
78 |
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1); |
|
79 |
by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1); |
|
80 |
by (etac rtrancl_induct 1); |
|
2469 | 81 |
by (fast_tac (!claset addIs reduction_rls) 1); |
515 | 82 |
by (etac (trans_rtrancl RS transD) 1); |
2469 | 83 |
by (fast_tac (!claset addIs reduction_rls) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
84 |
qed "Ap_reduce1"; |
515 | 85 |
|
86 |
goal Comb.thy "!!p r. [| p ---> q; r: comb |] ==> r#p ---> r#q"; |
|
87 |
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1); |
|
88 |
by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1); |
|
89 |
by (etac rtrancl_induct 1); |
|
2469 | 90 |
by (fast_tac (!claset addIs reduction_rls) 1); |
515 | 91 |
by (etac (trans_rtrancl RS transD) 1); |
2469 | 92 |
by (fast_tac (!claset addIs reduction_rls) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
93 |
qed "Ap_reduce2"; |
515 | 94 |
|
95 |
(** Counterexample to the diamond property for -1-> **) |
|
96 |
||
97 |
goal Comb.thy "K#I#(I#I) -1-> I"; |
|
98 |
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
|
99 |
qed "KIII_contract1"; |
515 | 100 |
|
101 |
goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))"; |
|
102 |
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
|
103 |
qed "KIII_contract2"; |
515 | 104 |
|
105 |
goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I"; |
|
106 |
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
|
107 |
qed "KIII_contract3"; |
515 | 108 |
|
109 |
goalw Comb.thy [diamond_def] "~ diamond(contract)"; |
|
2469 | 110 |
by (fast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3] |
515 | 111 |
addSEs [I_contract_E]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
112 |
qed "not_diamond_contract"; |
515 | 113 |
|
0 | 114 |
|
115 |
||
515 | 116 |
(*** Results about Parallel Contraction ***) |
117 |
||
118 |
(*For type checking: replaces a=1=>b by a,b:comb *) |
|
119 |
val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2; |
|
120 |
val parcontract_combD1 = parcontract.dom_subset RS subsetD RS SigmaD1; |
|
121 |
val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2; |
|
122 |
||
123 |
goal Comb.thy "field(parcontract) = comb"; |
|
2469 | 124 |
by (fast_tac (!claset addIs [equalityI, parcontract.K] |
1461 | 125 |
addSEs [parcontract_combE2]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
126 |
qed "field_parcontract_eq"; |
515 | 127 |
|
128 |
(*Derive a case for each combinator constructor*) |
|
129 |
val K_parcontractE = parcontract.mk_cases comb.con_defs "K =1=> r"; |
|
130 |
val S_parcontractE = parcontract.mk_cases comb.con_defs "S =1=> r"; |
|
131 |
val Ap_parcontractE = parcontract.mk_cases comb.con_defs "p#q =1=> r"; |
|
132 |
||
2469 | 133 |
AddSIs comb.intrs; |
134 |
AddIs parcontract.intrs; |
|
135 |
AddSEs [Ap_E, K_parcontractE, S_parcontractE, Ap_parcontractE]; |
|
136 |
AddSEs [parcontract_combD1, parcontract_combD2]; (*type checking*) |
|
137 |
AddSEs comb.free_SEs; |
|
515 | 138 |
|
139 |
(*** Basic properties of parallel contraction ***) |
|
140 |
||
141 |
goal Comb.thy "!!p r. K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')"; |
|
2469 | 142 |
by (Fast_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
143 |
qed "K1_parcontractD"; |
515 | 144 |
|
145 |
goal Comb.thy "!!p r. S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')"; |
|
2469 | 146 |
by (Fast_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
147 |
qed "S1_parcontractD"; |
515 | 148 |
|
149 |
goal Comb.thy |
|
150 |
"!!p q r. S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')"; |
|
2469 | 151 |
by (fast_tac (!claset addSDs [S1_parcontractD]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
152 |
qed "S2_parcontractD"; |
515 | 153 |
|
154 |
(*Church-Rosser property for parallel contraction*) |
|
155 |
goalw Comb.thy [diamond_def] "diamond(parcontract)"; |
|
156 |
by (rtac (impI RS allI RS allI) 1); |
|
1732 | 157 |
by (etac parcontract.induct 1); |
515 | 158 |
by (ALLGOALS |
2469 | 159 |
(fast_tac (!claset addSDs [K1_parcontractD,S2_parcontractD]))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
160 |
qed "diamond_parcontract"; |
515 | 161 |
|
162 |
(*** Transitive closure preserves the Church-Rosser property ***) |
|
0 | 163 |
|
515 | 164 |
goalw Comb.thy [diamond_def] |
165 |
"!!x y r. [| diamond(r); <x,y>:r^+ |] ==> \ |
|
166 |
\ ALL y'. <x,y'>:r --> (EX z. <y',z>: r^+ & <y,z>: r)"; |
|
167 |
by (etac trancl_induct 1); |
|
2469 | 168 |
by (fast_tac (!claset addIs [r_into_trancl]) 1); |
169 |
by (slow_best_tac (!claset addSDs [spec RS mp] |
|
1461 | 170 |
addIs [r_into_trancl, trans_trancl RS transD]) 1); |
1692 | 171 |
val diamond_strip_lemmaE = result() RS spec RS mp RS exE; |
515 | 172 |
|
173 |
val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)"; |
|
1461 | 174 |
by (rewtac diamond_def); (*unfold only in goal, not in premise!*) |
515 | 175 |
by (rtac (impI RS allI RS allI) 1); |
176 |
by (etac trancl_induct 1); |
|
177 |
by (ALLGOALS |
|
2469 | 178 |
(slow_best_tac (!claset addIs [r_into_trancl, trans_trancl RS transD] |
1692 | 179 |
addEs [major RS diamond_strip_lemmaE]))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
180 |
qed "diamond_trancl"; |
515 | 181 |
|
182 |
||
183 |
(*** Equivalence of p--->q and p===>q ***) |
|
184 |
||
185 |
goal Comb.thy "!!p q. p-1->q ==> p=1=>q"; |
|
1732 | 186 |
by (etac contract.induct 1); |
2469 | 187 |
by (ALLGOALS (fast_tac (!claset))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
188 |
qed "contract_imp_parcontract"; |
0 | 189 |
|
515 | 190 |
goal Comb.thy "!!p q. p--->q ==> p===>q"; |
191 |
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1); |
|
192 |
by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1); |
|
193 |
by (etac rtrancl_induct 1); |
|
2469 | 194 |
by (fast_tac (!claset addIs [r_into_trancl]) 1); |
195 |
by (fast_tac (!claset addIs [contract_imp_parcontract, |
|
1461 | 196 |
r_into_trancl, trans_trancl RS transD]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
197 |
qed "reduce_imp_parreduce"; |
515 | 198 |
|
0 | 199 |
|
515 | 200 |
goal Comb.thy "!!p q. p=1=>q ==> p--->q"; |
1732 | 201 |
by (etac parcontract.induct 1); |
2469 | 202 |
by (fast_tac (!claset addIs reduction_rls) 1); |
203 |
by (fast_tac (!claset addIs reduction_rls) 1); |
|
204 |
by (fast_tac (!claset addIs reduction_rls) 1); |
|
515 | 205 |
by (rtac (trans_rtrancl RS transD) 1); |
206 |
by (ALLGOALS |
|
207 |
(fast_tac |
|
2469 | 208 |
(!claset addIs [Ap_reduce1, Ap_reduce2] |
515 | 209 |
addSEs [parcontract_combD1,parcontract_combD2]))); |
760 | 210 |
qed "parcontract_imp_reduce"; |
515 | 211 |
|
212 |
goal Comb.thy "!!p q. p===>q ==> p--->q"; |
|
213 |
by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1); |
|
214 |
by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1); |
|
215 |
by (etac trancl_induct 1); |
|
216 |
by (etac parcontract_imp_reduce 1); |
|
217 |
by (etac (trans_rtrancl RS transD) 1); |
|
218 |
by (etac parcontract_imp_reduce 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
219 |
qed "parreduce_imp_reduce"; |
515 | 220 |
|
221 |
goal Comb.thy "p===>q <-> p--->q"; |
|
222 |
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
|
223 |
qed "parreduce_iff_reduce"; |
515 | 224 |
|
225 |
writeln"Reached end of file."; |