|
1 (* Title: HOL/Lambda/Eta.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1995 TU Muenchen |
|
5 |
|
6 Eta reduction, |
|
7 confluence ot eta, |
|
8 commutation of beta/eta, |
|
9 confluence of beta+eta |
|
10 *) |
|
11 |
|
12 open Eta; |
|
13 |
|
14 (* FIXME: add Suc_pred glovbally *) |
|
15 Addsimps (Suc_pred :: eta.intrs); |
|
16 |
|
17 |
|
18 val eta_cases = map (eta.mk_cases db.simps) |
|
19 ["Fun s -e> z","s @ t -e> u","Var i -e> t"]; |
|
20 |
|
21 val beta_cases = map (beta.mk_cases db.simps) |
|
22 ["s @ t -> u","Var i -> t"]; |
|
23 |
|
24 (* FIXME: add r_into_rtrancl to trancl_cs ??? |
|
25 build on lambda_ss which should build on trancl_cs *) |
|
26 val eta_cs = trancl_cs addIs (beta.intrs@eta.intrs) |
|
27 addSEs (beta_cases@eta_cases); |
|
28 |
|
29 (*** Arithmetic lemmas ***) |
|
30 |
|
31 goal Nat.thy "~ Suc n <= n"; |
|
32 by(simp_tac (simpset_of "Nat" addsimps [le_def]) 1); |
|
33 qed "Suc_n_not_le_n"; |
|
34 |
|
35 (* FIXME: move into Nat.ML *) |
|
36 goalw Nat.thy [le_def] "(i <= 0) = (i = 0)"; |
|
37 by(nat_ind_tac "i" 1); |
|
38 by(ALLGOALS(Asm_simp_tac)); |
|
39 qed "le_0"; |
|
40 Addsimps [le_0]; |
|
41 |
|
42 goal HOL.thy "!!P. P ==> P=True"; |
|
43 by(fast_tac HOL_cs 1); |
|
44 qed "True_eq"; |
|
45 |
|
46 Addsimps [less_not_sym RS True_eq]; |
|
47 |
|
48 (* FIXME: move into Nat.ML *) |
|
49 goal Arith.thy "!!i. i<j ==> j<k --> Suc i < k"; |
|
50 by(nat_ind_tac "k" 1); |
|
51 by(ALLGOALS(asm_simp_tac(simpset_of "Arith"))); |
|
52 by(fast_tac (HOL_cs addDs [Suc_lessD]) 1); |
|
53 bind_thm("less_trans_Suc",result() RS mp); |
|
54 |
|
55 goal Arith.thy "i < j --> pred i < j"; |
|
56 by(nat_ind_tac "j" 1); |
|
57 by(ALLGOALS(asm_simp_tac(simpset_of "Arith"))); |
|
58 by(nat_ind_tac "j1" 1); |
|
59 by(ALLGOALS(asm_simp_tac(simpset_of "Arith"))); |
|
60 bind_thm("less_imp_pred_less",result() RS mp); |
|
61 |
|
62 goal Arith.thy "i<j --> ~ pred j < i"; |
|
63 by(nat_ind_tac "j" 1); |
|
64 by(ALLGOALS(asm_simp_tac(simpset_of "Arith"))); |
|
65 by(fast_tac (HOL_cs addDs [less_imp_pred_less]) 1); |
|
66 bind_thm("less_imp_not_pred_less", result() RS mp); |
|
67 Addsimps [less_imp_not_pred_less]; |
|
68 |
|
69 goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i"; |
|
70 by(nat_ind_tac "j" 1); |
|
71 by(ALLGOALS(simp_tac(simpset_of "Nat"))); |
|
72 by(fast_tac (HOL_cs addDs [less_not_sym]) 1); |
|
73 bind_thm("less_interval1", result() RS mp RS mp); |
|
74 |
|
75 |
|
76 (*** decr and free ***) |
|
77 |
|
78 goal Eta.thy "!i k. free (lift t k) i = \ |
|
79 \ (i < k & free t i | k < i & free t (pred i))"; |
|
80 by(db.induct_tac "t" 1); |
|
81 by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong]))); |
|
82 by(fast_tac HOL_cs 2); |
|
83 by(safe_tac (HOL_cs addSIs [iffI])); |
|
84 bd Suc_mono 1; |
|
85 by(ALLGOALS(Asm_full_simp_tac)); |
|
86 by(dtac less_trans_Suc 1 THEN atac 1); |
|
87 by(dtac less_trans_Suc 2 THEN atac 2); |
|
88 by(ALLGOALS(Asm_full_simp_tac)); |
|
89 qed "free_lift"; |
|
90 Addsimps [free_lift]; |
|
91 |
|
92 goal Eta.thy "!i k t. free (s[t/k]) i = \ |
|
93 \ (free s k & free t i | free s (if i<k then i else Suc i))"; |
|
94 by(db.induct_tac "s" 1); |
|
95 by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addsimps |
|
96 [less_not_refl2,less_not_refl2 RS not_sym]))); |
|
97 by(fast_tac HOL_cs 2); |
|
98 by(safe_tac (HOL_cs addSIs [iffI])); |
|
99 by(ALLGOALS(Asm_simp_tac)); |
|
100 by(fast_tac (HOL_cs addEs [less_imp_not_pred_less RS notE]) 1); |
|
101 by(fast_tac (HOL_cs addDs [less_not_sym]) 1); |
|
102 bd Suc_mono 1; |
|
103 by(dtac less_interval1 1 THEN atac 1); |
|
104 by(asm_full_simp_tac (simpset_of "Nat" addsimps [eq_sym_conv]) 1); |
|
105 by(dtac less_trans_Suc 1 THEN atac 1); |
|
106 by(Asm_full_simp_tac 1); |
|
107 qed "free_subst"; |
|
108 Addsimps [free_subst]; |
|
109 |
|
110 goal Eta.thy "!!s. s -e> t ==> !i. free t i = free s i"; |
|
111 be (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; |
|
112 by(ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong]))); |
|
113 bind_thm("free_eta",result() RS spec); |
|
114 |
|
115 goal Eta.thy "!!s. [| s -e> t; ~free s i |] ==> ~free t i"; |
|
116 by(asm_simp_tac (!simpset addsimps [free_eta]) 1); |
|
117 qed "not_free_eta"; |
|
118 |
|
119 goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]"; |
|
120 by(db.induct_tac "s" 1); |
|
121 by(ALLGOALS(simp_tac (addsplit (!simpset)))); |
|
122 by(fast_tac HOL_cs 1); |
|
123 by(fast_tac HOL_cs 1); |
|
124 bind_thm("subst_not_free", result() RS spec RS spec RS spec RS mp); |
|
125 |
|
126 goalw Eta.thy [decr_def] "!!s. ~free s i ==> s[t/i] = decr s i"; |
|
127 be subst_not_free 1; |
|
128 qed "subst_decr"; |
|
129 |
|
130 goal Eta.thy "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]"; |
|
131 be (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; |
|
132 by(ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def]))); |
|
133 by(asm_simp_tac (!simpset addsimps [subst_decr]) 1); |
|
134 bind_thm("eta_subst",result() RS spec RS spec); |
|
135 Addsimps [eta_subst]; |
|
136 |
|
137 goalw Eta.thy [decr_def] "!!s. s -e> t ==> decr s i -e> decr t i"; |
|
138 be eta_subst 1; |
|
139 qed "eta_decr"; |
|
140 |
|
141 (*** Confluence of eta ***) |
|
142 |
|
143 goalw Eta.thy [id_def] |
|
144 "!x y. x-e> y --> (!z. x-e>z --> (? u. y -e>= u & z -e>= u))"; |
|
145 br eta.mutual_induct 1; |
|
146 by(ALLGOALS(fast_tac (eta_cs addSEs [eta_decr,not_free_eta] addss !simpset))); |
|
147 val lemma = result() RS spec RS spec RS mp RS spec RS mp; |
|
148 |
|
149 goalw Eta.thy [diamond_def,commute_def,square_def] "diamond(eta^=)"; |
|
150 by(fast_tac (eta_cs addEs [lemma]) 1); |
|
151 qed "diamond_refl_eta"; |
|
152 |
|
153 goal Eta.thy "confluent(eta)"; |
|
154 by(stac (rtrancl_reflcl RS sym) 1); |
|
155 by(rtac (diamond_refl_eta RS diamond_confluent) 1); |
|
156 qed "eta_confluent"; |
|
157 |
|
158 (*** Congruence rules for ->> ***) |
|
159 |
|
160 goal Eta.thy "!!s. s -e>> s' ==> Fun s -e>> Fun s'"; |
|
161 be rtrancl_induct 1; |
|
162 by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
|
163 qed "rtrancl_eta_Fun"; |
|
164 |
|
165 goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t"; |
|
166 be rtrancl_induct 1; |
|
167 by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
|
168 qed "rtrancl_eta_AppL"; |
|
169 |
|
170 goal Eta.thy "!!s. t -e>> t' ==> s @ t -e>> s @ t'"; |
|
171 be rtrancl_induct 1; |
|
172 by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
|
173 qed "rtrancl_eta_AppR"; |
|
174 |
|
175 goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'"; |
|
176 by (fast_tac (eta_cs addSIs [rtrancl_eta_AppL,rtrancl_eta_AppR] |
|
177 addIs [rtrancl_trans]) 1); |
|
178 qed "rtrancl_eta_App"; |
|
179 |
|
180 (*** Commutation of beta and eta ***) |
|
181 |
|
182 goal Eta.thy "!!s. s -> t ==> !i. free t i --> free s i"; |
|
183 be (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; |
|
184 by(ALLGOALS(Asm_full_simp_tac)); |
|
185 bind_thm("free_beta", result() RS spec RS mp); |
|
186 |
|
187 goalw Eta.thy [decr_def] "!s t. s -> t --> (!i. decr s i -> decr t i)"; |
|
188 br beta.mutual_induct 1; |
|
189 by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym]))); |
|
190 bind_thm("beta_decr", result() RS spec RS spec RS mp RS spec); |
|
191 |
|
192 goalw Eta.thy [decr_def] |
|
193 "decr (Var i) k = (if i<=k then Var i else Var(pred i))"; |
|
194 by(simp_tac (addsplit (!simpset) addsimps [le_def]) 1); |
|
195 qed "decr_Var"; |
|
196 Addsimps [decr_Var]; |
|
197 |
|
198 goalw Eta.thy [decr_def] "decr (s@t) i = (decr s i)@(decr t i)"; |
|
199 by(Simp_tac 1); |
|
200 qed "decr_App"; |
|
201 Addsimps [decr_App]; |
|
202 |
|
203 goalw Eta.thy [decr_def] "decr (Fun s) i = Fun (decr s (Suc i))"; |
|
204 by(Simp_tac 1); |
|
205 qed "decr_Fun"; |
|
206 Addsimps [decr_Fun]; |
|
207 |
|
208 goal Eta.thy "!i. ~free t (Suc i) --> decr t i = decr t (Suc i)"; |
|
209 by(db.induct_tac "t" 1); |
|
210 by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def]))); |
|
211 by(fast_tac (HOL_cs addDs [less_interval1]) 1); |
|
212 by(fast_tac HOL_cs 1); |
|
213 qed "decr_not_free"; |
|
214 Addsimps [decr_not_free]; |
|
215 |
|
216 goal Eta.thy "!s t. s -e> t --> (!i. lift s i -e> lift t i)"; |
|
217 br eta.mutual_induct 1; |
|
218 by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def]))); |
|
219 by(asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1); |
|
220 bind_thm("eta_lift",result() RS spec RS spec RS mp RS spec); |
|
221 Addsimps [eta_lift]; |
|
222 |
|
223 goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]"; |
|
224 by(db.induct_tac "u" 1); |
|
225 by(ALLGOALS(asm_simp_tac (addsplit (!simpset)))); |
|
226 by(fast_tac (eta_cs addIs [r_into_rtrancl]) 1); |
|
227 by(fast_tac (eta_cs addIs [rtrancl_eta_App]) 1); |
|
228 by(fast_tac (eta_cs addSIs [rtrancl_eta_Fun,eta_lift]) 1); |
|
229 bind_thm("rtrancl_eta_subst", result() RS spec RS spec RS spec RS mp); |
|
230 |
|
231 goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)"; |
|
232 br beta.mutual_induct 1; |
|
233 by(strip_tac 1); |
|
234 bes eta_cases 1; |
|
235 bes eta_cases 1; |
|
236 by(fast_tac (eta_cs addss (!simpset addsimps [subst_decr])) 1); |
|
237 by(fast_tac (eta_cs addIs [r_into_rtrancl,eta_subst]) 1); |
|
238 by(fast_tac (eta_cs addIs [rtrancl_eta_subst]) 1); |
|
239 by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1); |
|
240 by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1); |
|
241 by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr] |
|
242 addss (!simpset addsimps[subst_decr,symmetric decr_def])) 1); |
|
243 qed "square_beta_eta"; |
|
244 |
|
245 goal Eta.thy "confluent(beta Un eta)"; |
|
246 by(REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un, |
|
247 beta_confluent,eta_confluent,square_beta_eta] 1)); |
|
248 qed "confluent_beta_eta"; |