1269
|
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";
|