|
1 (* Title: HOL/ex/comb.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
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 (*** Reflexive/Transitive closure preserves the Church-Rosser property |
|
21 So does the Transitive closure; use r_into_trancl instead of rtrancl_refl |
|
22 ***) |
|
23 |
|
24 val [_, spec_mp] = [spec] RL [mp]; |
|
25 |
|
26 (*Strip lemma. The induction hyp is all but the last diamond of the strip.*) |
|
27 goalw Comb.thy [diamond_def] |
|
28 "!!r. [| diamond(r); (x,y):r^* |] ==> \ |
|
29 \ ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)"; |
|
30 by (etac rtrancl_induct 1); |
|
31 by (Blast_tac 1); |
|
32 by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)] |
|
33 addSDs [spec_mp]) 1); |
|
34 val diamond_strip_lemmaE = result() RS spec RS mp RS exE; |
|
35 |
|
36 val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)"; |
|
37 by (rewtac diamond_def); (*unfold only in goal, not in premise!*) |
|
38 by (rtac (impI RS allI RS allI) 1); |
|
39 by (etac rtrancl_induct 1); |
|
40 by (Blast_tac 1); |
|
41 by (slow_best_tac (*Seems to be a brittle, undirected search*) |
|
42 (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)] |
|
43 addEs [major RS diamond_strip_lemmaE]) 1); |
|
44 qed "diamond_rtrancl"; |
|
45 |
|
46 |
|
47 (*** Results about Contraction ***) |
|
48 |
|
49 (*Derive a case for each combinator constructor*) |
|
50 val K_contractE = contract.mk_cases comb.simps "K -1-> z"; |
|
51 val S_contractE = contract.mk_cases comb.simps "S -1-> z"; |
|
52 val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z"; |
|
53 |
|
54 AddSIs [contract.K, contract.S]; |
|
55 AddIs [contract.Ap1, contract.Ap2]; |
|
56 AddSEs [K_contractE, S_contractE, Ap_contractE]; |
|
57 Unsafe_Addss (!simpset); |
|
58 |
|
59 goalw Comb.thy [I_def] "!!z. I -1-> z ==> P"; |
|
60 by (Blast_tac 1); |
|
61 qed "I_contract_E"; |
|
62 AddSEs [I_contract_E]; |
|
63 |
|
64 goal Comb.thy "!!x z. K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')"; |
|
65 by (Blast_tac 1); |
|
66 qed "K1_contractD"; |
|
67 AddSEs [K1_contractD]; |
|
68 |
|
69 goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z"; |
|
70 by (etac rtrancl_induct 1); |
|
71 by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]))); |
|
72 qed "Ap_reduce1"; |
|
73 |
|
74 goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y"; |
|
75 by (etac rtrancl_induct 1); |
|
76 by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]))); |
|
77 qed "Ap_reduce2"; |
|
78 |
|
79 (** Counterexample to the diamond property for -1-> **) |
|
80 |
|
81 goal Comb.thy "K#I#(I#I) -1-> I"; |
|
82 by (rtac contract.K 1); |
|
83 qed "KIII_contract1"; |
|
84 |
|
85 goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))"; |
|
86 by (Blast_tac 1); |
|
87 qed "KIII_contract2"; |
|
88 |
|
89 goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I"; |
|
90 by (Blast_tac 1); |
|
91 qed "KIII_contract3"; |
|
92 |
|
93 goalw Comb.thy [diamond_def] "~ diamond(contract)"; |
|
94 by (blast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]) 1); |
|
95 qed "not_diamond_contract"; |
|
96 |
|
97 |
|
98 |
|
99 (*** Results about Parallel Contraction ***) |
|
100 |
|
101 (*Derive a case for each combinator constructor*) |
|
102 val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z"; |
|
103 val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z"; |
|
104 val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z"; |
|
105 |
|
106 AddIs parcontract.intrs; |
|
107 AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE]; |
|
108 Unsafe_Addss (!simpset); |
|
109 |
|
110 (*** Basic properties of parallel contraction ***) |
|
111 |
|
112 goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')"; |
|
113 by (Blast_tac 1); |
|
114 qed "K1_parcontractD"; |
|
115 AddSDs [K1_parcontractD]; |
|
116 |
|
117 goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')"; |
|
118 by (Blast_tac 1); |
|
119 qed "S1_parcontractD"; |
|
120 AddSDs [S1_parcontractD]; |
|
121 |
|
122 goal Comb.thy |
|
123 "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')"; |
|
124 by (Blast_tac 1); |
|
125 qed "S2_parcontractD"; |
|
126 AddSDs [S2_parcontractD]; |
|
127 |
|
128 (*The rules above are not essential but make proofs much faster*) |
|
129 |
|
130 |
|
131 (*Church-Rosser property for parallel contraction*) |
|
132 goalw Comb.thy [diamond_def] "diamond parcontract"; |
|
133 by (rtac (impI RS allI RS allI) 1); |
|
134 by (etac parcontract.induct 1 THEN prune_params_tac); |
|
135 by (Step_tac 1); |
|
136 by (ALLGOALS Blast_tac); |
|
137 qed "diamond_parcontract"; |
|
138 |
|
139 |
|
140 (*** Equivalence of x--->y and x===>y ***) |
|
141 |
|
142 goal Comb.thy "contract <= parcontract"; |
|
143 by (rtac subsetI 1); |
|
144 by (split_all_tac 1); |
|
145 by (etac contract.induct 1); |
|
146 by (ALLGOALS Blast_tac); |
|
147 qed "contract_subset_parcontract"; |
|
148 |
|
149 (*Reductions: simply throw together reflexivity, transitivity and |
|
150 the one-step reductions*) |
|
151 |
|
152 AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans]; |
|
153 |
|
154 (*Example only: not used*) |
|
155 goalw Comb.thy [I_def] "I#x ---> x"; |
|
156 by (Blast_tac 1); |
|
157 qed "reduce_I"; |
|
158 |
|
159 goal Comb.thy "parcontract <= contract^*"; |
|
160 by (rtac subsetI 1); |
|
161 by (split_all_tac 1); |
|
162 by (etac parcontract.induct 1 THEN prune_params_tac); |
|
163 by (ALLGOALS Blast_tac); |
|
164 qed "parcontract_subset_reduce"; |
|
165 |
|
166 goal Comb.thy "contract^* = parcontract^*"; |
|
167 by (REPEAT |
|
168 (resolve_tac [equalityI, |
|
169 contract_subset_parcontract RS rtrancl_mono, |
|
170 parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1)); |
|
171 qed "reduce_eq_parreduce"; |
|
172 |
|
173 goal Comb.thy "diamond(contract^*)"; |
|
174 by (simp_tac (!simpset addsimps [reduce_eq_parreduce, diamond_rtrancl, |
|
175 diamond_parcontract]) 1); |
|
176 qed "diamond_reduce"; |
|
177 |
|
178 |
|
179 writeln"Reached end of file."; |