author | nipkow |
Wed, 22 May 1996 18:32:37 +0200 | |
changeset 1759 | a42d6c537f4a |
parent 1730 | 1c7f793fc374 |
child 1910 | 6d572f96fb76 |
permissions | -rw-r--r-- |
1269 | 1 |
(* Title: HOL/Lambda/Eta.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
||
6 |
Eta reduction, |
|
1302 | 7 |
confluence of eta, |
1269 | 8 |
commutation of beta/eta, |
9 |
confluence of beta+eta |
|
10 |
*) |
|
11 |
||
12 |
open Eta; |
|
13 |
||
1302 | 14 |
Addsimps eta.intrs; |
1269 | 15 |
|
16 |
val eta_cases = map (eta.mk_cases db.simps) |
|
17 |
["Fun s -e> z","s @ t -e> u","Var i -e> t"]; |
|
18 |
||
19 |
val beta_cases = map (beta.mk_cases db.simps) |
|
20 |
["s @ t -> u","Var i -> t"]; |
|
21 |
||
1302 | 22 |
val eta_cs = lambda_cs addIs eta.intrs |
1269 | 23 |
addSEs (beta_cases@eta_cases); |
24 |
||
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
25 |
section "Arithmetic lemmas"; |
1269 | 26 |
|
27 |
goal HOL.thy "!!P. P ==> P=True"; |
|
28 |
by(fast_tac HOL_cs 1); |
|
29 |
qed "True_eq"; |
|
30 |
||
31 |
Addsimps [less_not_sym RS True_eq]; |
|
32 |
||
33 |
goal Arith.thy "i < j --> pred i < j"; |
|
34 |
by(nat_ind_tac "j" 1); |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1486
diff
changeset
|
35 |
by(ALLGOALS(asm_simp_tac(simpset_of "Arith" addsimps [less_Suc_eq]))); |
1269 | 36 |
by(nat_ind_tac "j1" 1); |
37 |
by(ALLGOALS(asm_simp_tac(simpset_of "Arith"))); |
|
1486 | 38 |
qed_spec_mp "less_imp_pred_less"; |
1269 | 39 |
|
40 |
goal Arith.thy "i<j --> ~ pred j < i"; |
|
41 |
by(nat_ind_tac "j" 1); |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1486
diff
changeset
|
42 |
by(ALLGOALS(asm_simp_tac(simpset_of "Arith" addsimps [less_Suc_eq]))); |
1269 | 43 |
by(fast_tac (HOL_cs addDs [less_imp_pred_less]) 1); |
1486 | 44 |
qed_spec_mp "less_imp_not_pred_less"; |
1269 | 45 |
Addsimps [less_imp_not_pred_less]; |
46 |
||
47 |
goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i"; |
|
48 |
by(nat_ind_tac "j" 1); |
|
49 |
by(ALLGOALS(simp_tac(simpset_of "Nat"))); |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1486
diff
changeset
|
50 |
by(simp_tac(simpset_of "Nat" addsimps [less_Suc_eq])1); |
1269 | 51 |
by(fast_tac (HOL_cs addDs [less_not_sym]) 1); |
1486 | 52 |
qed_spec_mp "less_interval1"; |
1269 | 53 |
|
54 |
||
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
55 |
section "decr and free"; |
1269 | 56 |
|
57 |
goal Eta.thy "!i k. free (lift t k) i = \ |
|
58 |
\ (i < k & free t i | k < i & free t (pred i))"; |
|
59 |
by(db.induct_tac "t" 1); |
|
60 |
by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong]))); |
|
61 |
by(fast_tac HOL_cs 2); |
|
62 |
by(safe_tac (HOL_cs addSIs [iffI])); |
|
1465 | 63 |
by (dtac Suc_mono 1); |
1269 | 64 |
by(ALLGOALS(Asm_full_simp_tac)); |
65 |
by(dtac less_trans_Suc 1 THEN atac 1); |
|
66 |
by(dtac less_trans_Suc 2 THEN atac 2); |
|
67 |
by(ALLGOALS(Asm_full_simp_tac)); |
|
68 |
qed "free_lift"; |
|
69 |
Addsimps [free_lift]; |
|
70 |
||
71 |
goal Eta.thy "!i k t. free (s[t/k]) i = \ |
|
72 |
\ (free s k & free t i | free s (if i<k then i else Suc i))"; |
|
73 |
by(db.induct_tac "s" 1); |
|
74 |
by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addsimps |
|
75 |
[less_not_refl2,less_not_refl2 RS not_sym]))); |
|
76 |
by(fast_tac HOL_cs 2); |
|
77 |
by(safe_tac (HOL_cs addSIs [iffI])); |
|
78 |
by(ALLGOALS(Asm_simp_tac)); |
|
79 |
by(fast_tac (HOL_cs addEs [less_imp_not_pred_less RS notE]) 1); |
|
80 |
by(fast_tac (HOL_cs addDs [less_not_sym]) 1); |
|
1465 | 81 |
by (dtac Suc_mono 1); |
1269 | 82 |
by(dtac less_interval1 1 THEN atac 1); |
83 |
by(asm_full_simp_tac (simpset_of "Nat" addsimps [eq_sym_conv]) 1); |
|
84 |
by(dtac less_trans_Suc 1 THEN atac 1); |
|
85 |
by(Asm_full_simp_tac 1); |
|
86 |
qed "free_subst"; |
|
87 |
Addsimps [free_subst]; |
|
88 |
||
89 |
goal Eta.thy "!!s. s -e> t ==> !i. free t i = free s i"; |
|
1730 | 90 |
by (etac eta.induct 1); |
1269 | 91 |
by(ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong]))); |
1486 | 92 |
qed_spec_mp "free_eta"; |
1269 | 93 |
|
94 |
goal Eta.thy "!!s. [| s -e> t; ~free s i |] ==> ~free t i"; |
|
95 |
by(asm_simp_tac (!simpset addsimps [free_eta]) 1); |
|
96 |
qed "not_free_eta"; |
|
97 |
||
98 |
goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]"; |
|
99 |
by(db.induct_tac "s" 1); |
|
100 |
by(ALLGOALS(simp_tac (addsplit (!simpset)))); |
|
101 |
by(fast_tac HOL_cs 1); |
|
102 |
by(fast_tac HOL_cs 1); |
|
1486 | 103 |
qed_spec_mp "subst_not_free"; |
1269 | 104 |
|
105 |
goalw Eta.thy [decr_def] "!!s. ~free s i ==> s[t/i] = decr s i"; |
|
1465 | 106 |
by (etac subst_not_free 1); |
1269 | 107 |
qed "subst_decr"; |
108 |
||
109 |
goal Eta.thy "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]"; |
|
1730 | 110 |
by (etac eta.induct 1); |
1269 | 111 |
by(ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def]))); |
112 |
by(asm_simp_tac (!simpset addsimps [subst_decr]) 1); |
|
1486 | 113 |
qed_spec_mp "eta_subst"; |
1269 | 114 |
Addsimps [eta_subst]; |
115 |
||
116 |
goalw Eta.thy [decr_def] "!!s. s -e> t ==> decr s i -e> decr t i"; |
|
1465 | 117 |
by (etac eta_subst 1); |
1269 | 118 |
qed "eta_decr"; |
119 |
||
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
120 |
section "Confluence of -e>"; |
1269 | 121 |
|
1431 | 122 |
goalw Eta.thy [square_def,id_def] "square eta eta (eta^=) (eta^=)"; |
1730 | 123 |
by (rtac (impI RS allI RS allI) 1); |
124 |
by (etac eta.induct 1); |
|
1269 | 125 |
by(ALLGOALS(fast_tac (eta_cs addSEs [eta_decr,not_free_eta] addss !simpset))); |
1431 | 126 |
val lemma = result(); |
1269 | 127 |
|
128 |
goal Eta.thy "confluent(eta)"; |
|
1431 | 129 |
by(rtac (lemma RS square_reflcl_confluent) 1); |
1269 | 130 |
qed "eta_confluent"; |
131 |
||
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
132 |
section "Congruence rules for -e>>"; |
1269 | 133 |
|
134 |
goal Eta.thy "!!s. s -e>> s' ==> Fun s -e>> Fun s'"; |
|
1465 | 135 |
by (etac rtrancl_induct 1); |
1269 | 136 |
by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
137 |
qed "rtrancl_eta_Fun"; |
|
138 |
||
139 |
goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t"; |
|
1465 | 140 |
by (etac rtrancl_induct 1); |
1269 | 141 |
by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
142 |
qed "rtrancl_eta_AppL"; |
|
143 |
||
144 |
goal Eta.thy "!!s. t -e>> t' ==> s @ t -e>> s @ t'"; |
|
1465 | 145 |
by (etac rtrancl_induct 1); |
1269 | 146 |
by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
147 |
qed "rtrancl_eta_AppR"; |
|
148 |
||
149 |
goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'"; |
|
150 |
by (fast_tac (eta_cs addSIs [rtrancl_eta_AppL,rtrancl_eta_AppR] |
|
151 |
addIs [rtrancl_trans]) 1); |
|
152 |
qed "rtrancl_eta_App"; |
|
153 |
||
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
154 |
section "Commutation of -> and -e>"; |
1269 | 155 |
|
1730 | 156 |
goal Eta.thy "!!s t. s -> t ==> (!i. free t i --> free s i)"; |
157 |
by (etac beta.induct 1); |
|
1269 | 158 |
by(ALLGOALS(Asm_full_simp_tac)); |
1486 | 159 |
qed_spec_mp "free_beta"; |
1269 | 160 |
|
1730 | 161 |
goalw Eta.thy [decr_def] "!!s t. s -> t ==> (!i. decr s i -> decr t i)"; |
162 |
by (etac beta.induct 1); |
|
1269 | 163 |
by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym]))); |
1486 | 164 |
qed_spec_mp "beta_decr"; |
1269 | 165 |
|
166 |
goalw Eta.thy [decr_def] |
|
167 |
"decr (Var i) k = (if i<=k then Var i else Var(pred i))"; |
|
168 |
by(simp_tac (addsplit (!simpset) addsimps [le_def]) 1); |
|
169 |
qed "decr_Var"; |
|
170 |
Addsimps [decr_Var]; |
|
171 |
||
172 |
goalw Eta.thy [decr_def] "decr (s@t) i = (decr s i)@(decr t i)"; |
|
173 |
by(Simp_tac 1); |
|
174 |
qed "decr_App"; |
|
175 |
Addsimps [decr_App]; |
|
176 |
||
177 |
goalw Eta.thy [decr_def] "decr (Fun s) i = Fun (decr s (Suc i))"; |
|
178 |
by(Simp_tac 1); |
|
179 |
qed "decr_Fun"; |
|
180 |
Addsimps [decr_Fun]; |
|
181 |
||
182 |
goal Eta.thy "!i. ~free t (Suc i) --> decr t i = decr t (Suc i)"; |
|
183 |
by(db.induct_tac "t" 1); |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1486
diff
changeset
|
184 |
by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq]))); |
1269 | 185 |
by(fast_tac HOL_cs 1); |
186 |
qed "decr_not_free"; |
|
187 |
Addsimps [decr_not_free]; |
|
188 |
||
1730 | 189 |
goal Eta.thy "!!s t. s -e> t ==> (!i. lift s i -e> lift t i)"; |
190 |
by (etac eta.induct 1); |
|
1269 | 191 |
by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def]))); |
192 |
by(asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1); |
|
1486 | 193 |
qed_spec_mp "eta_lift"; |
1269 | 194 |
Addsimps [eta_lift]; |
195 |
||
196 |
goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]"; |
|
197 |
by(db.induct_tac "u" 1); |
|
198 |
by(ALLGOALS(asm_simp_tac (addsplit (!simpset)))); |
|
199 |
by(fast_tac (eta_cs addIs [r_into_rtrancl]) 1); |
|
1302 | 200 |
by(fast_tac (eta_cs addSIs [rtrancl_eta_App]) 1); |
1269 | 201 |
by(fast_tac (eta_cs addSIs [rtrancl_eta_Fun,eta_lift]) 1); |
1486 | 202 |
qed_spec_mp "rtrancl_eta_subst"; |
1269 | 203 |
|
204 |
goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)"; |
|
1730 | 205 |
by (rtac (impI RS allI RS allI) 1); |
206 |
by (etac beta.induct 1); |
|
1269 | 207 |
by(strip_tac 1); |
1465 | 208 |
by (eresolve_tac eta_cases 1); |
209 |
by (eresolve_tac eta_cases 1); |
|
1269 | 210 |
by(fast_tac (eta_cs addss (!simpset addsimps [subst_decr])) 1); |
211 |
by(fast_tac (eta_cs addIs [r_into_rtrancl,eta_subst]) 1); |
|
212 |
by(fast_tac (eta_cs addIs [rtrancl_eta_subst]) 1); |
|
213 |
by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1); |
|
214 |
by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1); |
|
215 |
by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr] |
|
216 |
addss (!simpset addsimps[subst_decr,symmetric decr_def])) 1); |
|
217 |
qed "square_beta_eta"; |
|
218 |
||
219 |
goal Eta.thy "confluent(beta Un eta)"; |
|
220 |
by(REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un, |
|
221 |
beta_confluent,eta_confluent,square_beta_eta] 1)); |
|
222 |
qed "confluent_beta_eta"; |
|
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
223 |
|
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
224 |
|
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
225 |
section "Implicit definition of -e>: Fun(lift s 0 @ Var 0) -e> s"; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
226 |
|
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
227 |
goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)"; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
228 |
by(db.induct_tac "s" 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
229 |
by(simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
230 |
by(SELECT_GOAL(safe_tac HOL_cs)1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
231 |
by(res_inst_tac [("m","nat"),("n","i")] nat_less_cases 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
232 |
by(res_inst_tac [("x","Var nat")] exI 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
233 |
by(Asm_simp_tac 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
234 |
by(fast_tac HOL_cs 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
235 |
by(res_inst_tac [("x","Var(pred nat)")] exI 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
236 |
by(Asm_simp_tac 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
237 |
br notE 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
238 |
ba 2; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
239 |
be thin_rl 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
240 |
by(res_inst_tac [("db","t")] db_case_distinction 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
241 |
by(simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
242 |
by(fast_tac (HOL_cs addDs [less_not_refl2]) 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
243 |
by(Simp_tac 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
244 |
by(Simp_tac 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
245 |
by(asm_simp_tac (!simpset addsimps [de_Morgan_disj]) 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
246 |
be thin_rl 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
247 |
be thin_rl 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
248 |
br allI 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
249 |
br iffI 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
250 |
by(REPEAT(eresolve_tac [conjE,exE] 1)); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
251 |
by(rename_tac "u1 u2" 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
252 |
by(res_inst_tac [("x","u1@u2")] exI 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
253 |
by(Asm_simp_tac 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
254 |
be exE 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
255 |
be rev_mp 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
256 |
by(res_inst_tac [("db","t")] db_case_distinction 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
257 |
by(simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
258 |
by(Simp_tac 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
259 |
by(fast_tac HOL_cs 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
260 |
by(Simp_tac 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
261 |
by(Asm_simp_tac 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
262 |
be thin_rl 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
263 |
br allI 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
264 |
br iffI 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
265 |
be exE 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
266 |
by(res_inst_tac [("x","Fun t")] exI 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
267 |
by(Asm_simp_tac 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
268 |
be exE 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
269 |
be rev_mp 1; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
270 |
by(res_inst_tac [("db","t")] db_case_distinction 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
271 |
by(simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
272 |
by(Simp_tac 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
273 |
by(Simp_tac 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
274 |
by(fast_tac HOL_cs 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
275 |
qed_spec_mp "not_free_iff_lifted"; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
276 |
|
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
277 |
goalw Eta.thy [decr_def] |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
278 |
"(!s. (~free s 0) --> R(Fun(s @ Var 0))(decr s 0)) = \ |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
279 |
\ (!s. R(Fun(lift s 0 @ Var 0))(s))"; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
280 |
by(fast_tac (HOL_cs addss (!simpset addsimps [lemma,not_free_iff_lifted])) 1); |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
281 |
qed "explicit_is_implicit"; |