author | nipkow |
Mon, 21 Oct 1996 09:51:18 +0200 | |
changeset 2116 | 73bbf2cc7651 |
parent 2083 | b56425a385b9 |
child 2159 | e650a3f6f600 |
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 |
||
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1910
diff
changeset
|
22 |
AddIs eta.intrs; |
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1910
diff
changeset
|
23 |
AddSEs (beta_cases@eta_cases); |
1269 | 24 |
|
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
25 |
section "decr and free"; |
1269 | 26 |
|
27 |
goal Eta.thy "!i k. free (lift t k) i = \ |
|
28 |
\ (i < k & free t i | k < i & free t (pred i))"; |
|
2031 | 29 |
by (db.induct_tac "t" 1); |
30 |
by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong]))); |
|
31 |
by (fast_tac HOL_cs 2); |
|
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
32 |
by(simp_tac (!simpset addsimps [pred_def] |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
33 |
setloop (split_tac [expand_nat_case])) 1); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
34 |
by (safe_tac HOL_cs); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
35 |
by (ALLGOALS trans_tac); |
1269 | 36 |
qed "free_lift"; |
37 |
Addsimps [free_lift]; |
|
38 |
||
39 |
goal Eta.thy "!i k t. free (s[t/k]) i = \ |
|
40 |
\ (free s k & free t i | free s (if i<k then i else Suc i))"; |
|
2031 | 41 |
by (db.induct_tac "s" 1); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
42 |
by (Asm_simp_tac 2); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
43 |
by (Fast_tac 2); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
44 |
by (asm_full_simp_tac (addsplit (!simpset)) 2); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
45 |
by(simp_tac (!simpset addsimps [pred_def,subst_Var] |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
46 |
setloop (split_tac [expand_if,expand_nat_case])) 1); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
47 |
by (safe_tac (HOL_cs addSEs [nat_neqE])); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
48 |
by (ALLGOALS trans_tac); |
1269 | 49 |
qed "free_subst"; |
50 |
Addsimps [free_subst]; |
|
51 |
||
52 |
goal Eta.thy "!!s. s -e> t ==> !i. free t i = free s i"; |
|
1730 | 53 |
by (etac eta.induct 1); |
2031 | 54 |
by (ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong]))); |
1486 | 55 |
qed_spec_mp "free_eta"; |
1269 | 56 |
|
57 |
goal Eta.thy "!!s. [| s -e> t; ~free s i |] ==> ~free t i"; |
|
2031 | 58 |
by (asm_simp_tac (!simpset addsimps [free_eta]) 1); |
1269 | 59 |
qed "not_free_eta"; |
60 |
||
61 |
goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]"; |
|
2031 | 62 |
by (db.induct_tac "s" 1); |
63 |
by (ALLGOALS(simp_tac (addsplit (!simpset)))); |
|
64 |
by (fast_tac HOL_cs 1); |
|
65 |
by (fast_tac HOL_cs 1); |
|
1486 | 66 |
qed_spec_mp "subst_not_free"; |
1269 | 67 |
|
68 |
goalw Eta.thy [decr_def] "!!s. ~free s i ==> s[t/i] = decr s i"; |
|
1465 | 69 |
by (etac subst_not_free 1); |
1269 | 70 |
qed "subst_decr"; |
71 |
||
72 |
goal Eta.thy "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]"; |
|
1730 | 73 |
by (etac eta.induct 1); |
2031 | 74 |
by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def]))); |
75 |
by (asm_simp_tac (!simpset addsimps [subst_decr]) 1); |
|
1486 | 76 |
qed_spec_mp "eta_subst"; |
1269 | 77 |
Addsimps [eta_subst]; |
78 |
||
79 |
goalw Eta.thy [decr_def] "!!s. s -e> t ==> decr s i -e> decr t i"; |
|
1465 | 80 |
by (etac eta_subst 1); |
1269 | 81 |
qed "eta_decr"; |
82 |
||
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
83 |
section "Confluence of -e>"; |
1269 | 84 |
|
1431 | 85 |
goalw Eta.thy [square_def,id_def] "square eta eta (eta^=) (eta^=)"; |
1730 | 86 |
by (rtac (impI RS allI RS allI) 1); |
2057 | 87 |
by (Simp_tac 1); |
1730 | 88 |
by (etac eta.induct 1); |
2057 | 89 |
by (best_tac (!claset addSIs [eta_decr] |
90 |
addIs [free_eta RS iffD1] addss !simpset) 1); |
|
91 |
by (slow_tac (!claset) 1); |
|
92 |
by (slow_tac (!claset) 1); |
|
93 |
by (slow_tac (!claset addSIs [eta_decr] |
|
94 |
addIs [free_eta RS iffD1]) 1); |
|
1431 | 95 |
val lemma = result(); |
1269 | 96 |
|
97 |
goal Eta.thy "confluent(eta)"; |
|
2031 | 98 |
by (rtac (lemma RS square_reflcl_confluent) 1); |
1269 | 99 |
qed "eta_confluent"; |
100 |
||
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
101 |
section "Congruence rules for -e>>"; |
1269 | 102 |
|
103 |
goal Eta.thy "!!s. s -e>> s' ==> Fun s -e>> Fun s'"; |
|
1465 | 104 |
by (etac rtrancl_induct 1); |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1910
diff
changeset
|
105 |
by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
1269 | 106 |
qed "rtrancl_eta_Fun"; |
107 |
||
108 |
goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t"; |
|
1465 | 109 |
by (etac rtrancl_induct 1); |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1910
diff
changeset
|
110 |
by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
1269 | 111 |
qed "rtrancl_eta_AppL"; |
112 |
||
113 |
goal Eta.thy "!!s. t -e>> t' ==> s @ t -e>> s @ t'"; |
|
1465 | 114 |
by (etac rtrancl_induct 1); |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1910
diff
changeset
|
115 |
by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
1269 | 116 |
qed "rtrancl_eta_AppR"; |
117 |
||
118 |
goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'"; |
|
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1910
diff
changeset
|
119 |
by (deepen_tac (!claset addSIs [rtrancl_eta_AppL,rtrancl_eta_AppR] |
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1910
diff
changeset
|
120 |
addIs [rtrancl_trans]) 2 1); |
1269 | 121 |
qed "rtrancl_eta_App"; |
122 |
||
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
123 |
section "Commutation of -> and -e>"; |
1269 | 124 |
|
1730 | 125 |
goal Eta.thy "!!s t. s -> t ==> (!i. free t i --> free s i)"; |
126 |
by (etac beta.induct 1); |
|
2031 | 127 |
by (ALLGOALS(Asm_full_simp_tac)); |
1486 | 128 |
qed_spec_mp "free_beta"; |
1269 | 129 |
|
1730 | 130 |
goalw Eta.thy [decr_def] "!!s t. s -> t ==> (!i. decr s i -> decr t i)"; |
131 |
by (etac beta.induct 1); |
|
2031 | 132 |
by (ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym]))); |
1486 | 133 |
qed_spec_mp "beta_decr"; |
1269 | 134 |
|
135 |
goalw Eta.thy [decr_def] |
|
136 |
"decr (Var i) k = (if i<=k then Var i else Var(pred i))"; |
|
2031 | 137 |
by (simp_tac (addsplit (!simpset) addsimps [le_def]) 1); |
1269 | 138 |
qed "decr_Var"; |
139 |
Addsimps [decr_Var]; |
|
140 |
||
141 |
goalw Eta.thy [decr_def] "decr (s@t) i = (decr s i)@(decr t i)"; |
|
2031 | 142 |
by (Simp_tac 1); |
1269 | 143 |
qed "decr_App"; |
144 |
Addsimps [decr_App]; |
|
145 |
||
146 |
goalw Eta.thy [decr_def] "decr (Fun s) i = Fun (decr s (Suc i))"; |
|
2031 | 147 |
by (Simp_tac 1); |
1269 | 148 |
qed "decr_Fun"; |
149 |
Addsimps [decr_Fun]; |
|
150 |
||
2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2057
diff
changeset
|
151 |
goal Eta.thy "!i. ~free t (Suc i) --> decr t (Suc i) = decr t i"; |
2031 | 152 |
by (db.induct_tac "t" 1); |
2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2057
diff
changeset
|
153 |
by (ALLGOALS |
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2057
diff
changeset
|
154 |
(asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq]))); |
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2057
diff
changeset
|
155 |
qed_spec_mp "decr_not_free"; |
1269 | 156 |
Addsimps [decr_not_free]; |
157 |
||
1730 | 158 |
goal Eta.thy "!!s t. s -e> t ==> (!i. lift s i -e> lift t i)"; |
159 |
by (etac eta.induct 1); |
|
2031 | 160 |
by (ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def]))); |
2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2057
diff
changeset
|
161 |
by (asm_simp_tac (!simpset addsimps [subst_decr]) 1); |
1486 | 162 |
qed_spec_mp "eta_lift"; |
1269 | 163 |
Addsimps [eta_lift]; |
164 |
||
165 |
goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]"; |
|
2031 | 166 |
by (db.induct_tac "u" 1); |
167 |
by (ALLGOALS(asm_simp_tac (addsplit (!simpset)))); |
|
168 |
by (fast_tac (!claset addIs [r_into_rtrancl]) 1); |
|
169 |
by (fast_tac (!claset addSIs [rtrancl_eta_App]) 1); |
|
170 |
by (fast_tac (!claset addSIs [rtrancl_eta_Fun,eta_lift]) 1); |
|
1486 | 171 |
qed_spec_mp "rtrancl_eta_subst"; |
1269 | 172 |
|
173 |
goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)"; |
|
1730 | 174 |
by (rtac (impI RS allI RS allI) 1); |
175 |
by (etac beta.induct 1); |
|
2031 | 176 |
by (strip_tac 1); |
1465 | 177 |
by (eresolve_tac eta_cases 1); |
178 |
by (eresolve_tac eta_cases 1); |
|
2031 | 179 |
by (fast_tac (!claset addss (!simpset addsimps [subst_decr])) 1); |
180 |
by (slow_tac (!claset addIs [r_into_rtrancl,eta_subst]) 1); |
|
181 |
by (slow_tac (!claset addIs [rtrancl_eta_subst]) 1); |
|
182 |
by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1); |
|
183 |
by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1); |
|
184 |
by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr] |
|
1269 | 185 |
addss (!simpset addsimps[subst_decr,symmetric decr_def])) 1); |
186 |
qed "square_beta_eta"; |
|
187 |
||
188 |
goal Eta.thy "confluent(beta Un eta)"; |
|
2031 | 189 |
by (REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un, |
1269 | 190 |
beta_confluent,eta_confluent,square_beta_eta] 1)); |
191 |
qed "confluent_beta_eta"; |
|
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
192 |
|
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
193 |
|
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
194 |
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
|
195 |
|
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
196 |
goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)"; |
2031 | 197 |
by (db.induct_tac "s" 1); |
2057 | 198 |
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
199 |
by (SELECT_GOAL(safe_tac HOL_cs)1); |
|
200 |
by (res_inst_tac [("m","nat"),("n","i")] nat_less_cases 1); |
|
201 |
by (res_inst_tac [("x","Var nat")] exI 1); |
|
202 |
by (Asm_simp_tac 1); |
|
203 |
by (fast_tac HOL_cs 1); |
|
204 |
by (res_inst_tac [("x","Var(pred nat)")] exI 1); |
|
205 |
by (Asm_simp_tac 1); |
|
206 |
by (rtac notE 1); |
|
207 |
by (assume_tac 2); |
|
208 |
by (etac thin_rl 1); |
|
209 |
by (res_inst_tac [("db","t")] db_case_distinction 1); |
|
210 |
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
|
211 |
by (fast_tac (HOL_cs addDs [less_not_refl2]) 1); |
|
212 |
by (Simp_tac 1); |
|
213 |
by (Simp_tac 1); |
|
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
214 |
by (Asm_simp_tac 1); |
2057 | 215 |
by (etac thin_rl 1); |
216 |
by (etac thin_rl 1); |
|
217 |
by (rtac allI 1); |
|
218 |
by (rtac iffI 1); |
|
219 |
by (REPEAT(eresolve_tac [conjE,exE] 1)); |
|
220 |
by (rename_tac "u1 u2" 1); |
|
221 |
by (res_inst_tac [("x","u1@u2")] exI 1); |
|
222 |
by (Asm_simp_tac 1); |
|
223 |
by (etac exE 1); |
|
224 |
by (etac rev_mp 1); |
|
225 |
by (res_inst_tac [("db","t")] db_case_distinction 1); |
|
226 |
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
|
227 |
by (Simp_tac 1); |
|
228 |
by (fast_tac HOL_cs 1); |
|
229 |
by (Simp_tac 1); |
|
2031 | 230 |
by (Asm_simp_tac 1); |
231 |
by (etac thin_rl 1); |
|
232 |
by (rtac allI 1); |
|
233 |
by (rtac iffI 1); |
|
2057 | 234 |
by (etac exE 1); |
235 |
by (res_inst_tac [("x","Fun t")] exI 1); |
|
236 |
by (Asm_simp_tac 1); |
|
2031 | 237 |
by (etac exE 1); |
238 |
by (etac rev_mp 1); |
|
239 |
by (res_inst_tac [("db","t")] db_case_distinction 1); |
|
2057 | 240 |
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
241 |
by (Simp_tac 1); |
|
2031 | 242 |
by (Simp_tac 1); |
243 |
by (fast_tac HOL_cs 1); |
|
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
244 |
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
|
245 |
|
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
246 |
goalw Eta.thy [decr_def] |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
247 |
"(!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
|
248 |
\ (!s. R(Fun(lift s 0 @ Var 0))(s))"; |
2031 | 249 |
by (fast_tac (HOL_cs addss (!simpset addsimps [lemma,not_free_iff_lifted])) 1); |
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
250 |
qed "explicit_is_implicit"; |