author | berghofe |
Fri, 24 Jul 1998 13:19:38 +0200 | |
changeset 5184 | 9b8547a9496a |
parent 5146 | 1ea751ae62b2 |
child 5261 | ce3c25c8a694 |
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 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
16 |
val eta_cases = map (eta.mk_cases dB.simps) |
5146 | 17 |
["Abs s -e> z","s $ t -e> u","Var i -e> t"]; |
1269 | 18 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
19 |
val beta_cases = map (beta.mk_cases dB.simps) |
5146 | 20 |
["s $ t -> u","Var i -> t"]; |
1269 | 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 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
25 |
section "eta, subst and free"; |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
26 |
|
5069 | 27 |
Goal "!i t u. ~free s i --> s[t/i] = s[u/i]"; |
5184 | 28 |
by (induct_tac "s" 1); |
4089 | 29 |
by (ALLGOALS(simp_tac (addsplit (simpset())))); |
2891 | 30 |
by (Blast_tac 1); |
31 |
by (Blast_tac 1); |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
32 |
qed_spec_mp "subst_not_free"; |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
33 |
Addsimps [subst_not_free RS eqTrueI]; |
1269 | 34 |
|
5117 | 35 |
Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))"; |
5184 | 36 |
by (induct_tac "t" 1); |
4089 | 37 |
by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong]))); |
2891 | 38 |
by (Blast_tac 2); |
5184 | 39 |
by (simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
40 |
by (safe_tac HOL_cs); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
41 |
by (ALLGOALS trans_tac); |
1269 | 42 |
qed "free_lift"; |
43 |
Addsimps [free_lift]; |
|
44 |
||
5069 | 45 |
Goal "!i k t. free (s[t/k]) i = \ |
1269 | 46 |
\ (free s k & free t i | free s (if i<k then i else Suc i))"; |
5184 | 47 |
by (induct_tac "s" 1); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
48 |
by (Asm_simp_tac 2); |
2891 | 49 |
by (Blast_tac 2); |
4089 | 50 |
by (asm_full_simp_tac (addsplit (simpset())) 2); |
4360 | 51 |
by (simp_tac (simpset() addsimps [diff_Suc,subst_Var] |
5184 | 52 |
addsplits [nat.split]) 1); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
53 |
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
|
54 |
by (ALLGOALS trans_tac); |
1269 | 55 |
qed "free_subst"; |
56 |
Addsimps [free_subst]; |
|
57 |
||
5117 | 58 |
Goal "s -e> t ==> !i. free t i = free s i"; |
1730 | 59 |
by (etac eta.induct 1); |
4089 | 60 |
by (ALLGOALS(asm_simp_tac (simpset() addcongs [conj_cong]))); |
1486 | 61 |
qed_spec_mp "free_eta"; |
1269 | 62 |
|
5117 | 63 |
Goal "[| s -e> t; ~free s i |] ==> ~free t i"; |
4089 | 64 |
by (asm_simp_tac (simpset() addsimps [free_eta]) 1); |
1269 | 65 |
qed "not_free_eta"; |
66 |
||
5117 | 67 |
Goal "s -e> t ==> !u i. s[u/i] -e> t[u/i]"; |
1730 | 68 |
by (etac eta.induct 1); |
4089 | 69 |
by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_subst RS sym]))); |
1486 | 70 |
qed_spec_mp "eta_subst"; |
1269 | 71 |
Addsimps [eta_subst]; |
72 |
||
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
73 |
section "Confluence of -e>"; |
1269 | 74 |
|
5069 | 75 |
Goalw [square_def,id_def] "square eta eta (eta^=) (eta^=)"; |
1730 | 76 |
by (rtac (impI RS allI RS allI) 1); |
2057 | 77 |
by (Simp_tac 1); |
1730 | 78 |
by (etac eta.induct 1); |
4089 | 79 |
by (slow_tac (claset() addIs [subst_not_free,eta_subst] |
80 |
addIs [free_eta RS iffD1] addss simpset()) 1); |
|
4162 | 81 |
by Safe_tac; |
4089 | 82 |
by (blast_tac (claset() addSIs [eta_subst] addIs [free_eta RS iffD1]) 5); |
2922 | 83 |
by (ALLGOALS Blast_tac); |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
84 |
qed "square_eta"; |
1269 | 85 |
|
5069 | 86 |
Goal "confluent(eta)"; |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
87 |
by (rtac (square_eta RS square_reflcl_confluent) 1); |
1269 | 88 |
qed "eta_confluent"; |
89 |
||
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
90 |
section "Congruence rules for -e>>"; |
1269 | 91 |
|
5117 | 92 |
Goal "s -e>> s' ==> Abs s -e>> Abs s'"; |
1465 | 93 |
by (etac rtrancl_induct 1); |
4089 | 94 |
by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
95 |
qed "rtrancl_eta_Abs"; |
1269 | 96 |
|
5146 | 97 |
Goal "s -e>> s' ==> s $ t -e>> s' $ t"; |
1465 | 98 |
by (etac rtrancl_induct 1); |
4089 | 99 |
by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
1269 | 100 |
qed "rtrancl_eta_AppL"; |
101 |
||
5146 | 102 |
Goal "t -e>> t' ==> s $ t -e>> s $ t'"; |
1465 | 103 |
by (etac rtrancl_induct 1); |
4089 | 104 |
by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
1269 | 105 |
qed "rtrancl_eta_AppR"; |
106 |
||
5146 | 107 |
Goal "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'"; |
4089 | 108 |
by (blast_tac (claset() addSIs [rtrancl_eta_AppL, rtrancl_eta_AppR] |
2922 | 109 |
addIs [rtrancl_trans]) 1); |
1269 | 110 |
qed "rtrancl_eta_App"; |
111 |
||
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
112 |
section "Commutation of -> and -e>"; |
1269 | 113 |
|
5117 | 114 |
Goal "s -> t ==> (!i. free t i --> free s i)"; |
1730 | 115 |
by (etac beta.induct 1); |
2031 | 116 |
by (ALLGOALS(Asm_full_simp_tac)); |
1486 | 117 |
qed_spec_mp "free_beta"; |
1269 | 118 |
|
5117 | 119 |
Goal "s -> t ==> !u i. s[u/i] -> t[u/i]"; |
1730 | 120 |
by (etac beta.induct 1); |
4089 | 121 |
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_subst RS sym]))); |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
122 |
qed_spec_mp "beta_subst"; |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
123 |
AddIs [beta_subst]; |
1269 | 124 |
|
5069 | 125 |
Goal "!i. t[Var i/i] = t[Var(i)/Suc i]"; |
5184 | 126 |
by (induct_tac "t" 1); |
4089 | 127 |
by (ALLGOALS (asm_simp_tac (addsplit (simpset())))); |
4162 | 128 |
by (safe_tac (HOL_cs addSEs [nat_neqE])); |
129 |
by (ALLGOALS trans_tac); |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
130 |
qed_spec_mp "subst_Var_Suc"; |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
131 |
Addsimps [subst_Var_Suc]; |
1269 | 132 |
|
5117 | 133 |
Goal "s -e> t ==> (!i. lift s i -e> lift t i)"; |
1730 | 134 |
by (etac eta.induct 1); |
4089 | 135 |
by (ALLGOALS(asm_simp_tac (addsplit (simpset())))); |
1486 | 136 |
qed_spec_mp "eta_lift"; |
1269 | 137 |
Addsimps [eta_lift]; |
138 |
||
5069 | 139 |
Goal "!s t i. s -e> t --> u[s/i] -e>> u[t/i]"; |
5184 | 140 |
by (induct_tac "u" 1); |
4089 | 141 |
by (ALLGOALS(asm_simp_tac (addsplit (simpset())))); |
142 |
by (blast_tac (claset() addIs [r_into_rtrancl]) 1); |
|
143 |
by (blast_tac (claset() addSIs [rtrancl_eta_App]) 1); |
|
144 |
by (blast_tac (claset() addSIs [rtrancl_eta_Abs,eta_lift]) 1); |
|
1486 | 145 |
qed_spec_mp "rtrancl_eta_subst"; |
1269 | 146 |
|
5069 | 147 |
Goalw [square_def] "square beta eta (eta^*) (beta^=)"; |
1730 | 148 |
by (rtac (impI RS allI RS allI) 1); |
149 |
by (etac beta.induct 1); |
|
4089 | 150 |
by (slow_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_subst,eta_subst] |
151 |
addss simpset()) 1); |
|
152 |
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1); |
|
153 |
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1); |
|
2922 | 154 |
(*23 seconds?*) |
2931
8658bf6c1a5b
Mod because of "Turned Addsimps into AddIffs for datatype laws."
nipkow
parents:
2922
diff
changeset
|
155 |
DelIffs dB.distinct; |
8658bf6c1a5b
Mod because of "Turned Addsimps into AddIffs for datatype laws."
nipkow
parents:
2922
diff
changeset
|
156 |
Addsimps dB.distinct; |
4089 | 157 |
by (slow_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_Abs,free_beta] |
158 |
addss simpset()) 1); |
|
1269 | 159 |
qed "square_beta_eta"; |
160 |
||
5069 | 161 |
Goal "confluent(beta Un eta)"; |
2031 | 162 |
by (REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un, |
1269 | 163 |
beta_confluent,eta_confluent,square_beta_eta] 1)); |
164 |
qed "confluent_beta_eta"; |
|
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
165 |
|
5146 | 166 |
section "Implicit definition of -e>: Abs(lift s 0 $ Var 0) -e> s"; |
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
167 |
|
5069 | 168 |
Goal "!i. (~free s i) = (? t. s = lift t i)"; |
5184 | 169 |
by (induct_tac "s" 1); |
4686 | 170 |
by (Simp_tac 1); |
2057 | 171 |
by (SELECT_GOAL(safe_tac HOL_cs)1); |
4162 | 172 |
by (etac nat_neqE 1); |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
173 |
by (res_inst_tac [("x","Var nat")] exI 1); |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
174 |
by (Asm_simp_tac 1); |
4360 | 175 |
by (res_inst_tac [("x","Var(nat-1)")] exI 1); |
2057 | 176 |
by (Asm_simp_tac 1); |
177 |
by (rtac notE 1); |
|
178 |
by (assume_tac 2); |
|
179 |
by (etac thin_rl 1); |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
180 |
by (res_inst_tac [("dB","t")] dB_case_distinction 1); |
4686 | 181 |
by (Simp_tac 1); |
2891 | 182 |
by (blast_tac (HOL_cs addDs [less_not_refl2]) 1); |
2057 | 183 |
by (Simp_tac 1); |
184 |
by (Simp_tac 1); |
|
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2083
diff
changeset
|
185 |
by (Asm_simp_tac 1); |
2057 | 186 |
by (etac thin_rl 1); |
187 |
by (etac thin_rl 1); |
|
188 |
by (rtac allI 1); |
|
189 |
by (rtac iffI 1); |
|
190 |
by (REPEAT(eresolve_tac [conjE,exE] 1)); |
|
191 |
by (rename_tac "u1 u2" 1); |
|
5146 | 192 |
by (res_inst_tac [("x","u1$u2")] exI 1); |
2057 | 193 |
by (Asm_simp_tac 1); |
194 |
by (etac exE 1); |
|
195 |
by (etac rev_mp 1); |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
196 |
by (res_inst_tac [("dB","t")] dB_case_distinction 1); |
4686 | 197 |
by (Simp_tac 1); |
2057 | 198 |
by (Simp_tac 1); |
2891 | 199 |
by (Blast_tac 1); |
2057 | 200 |
by (Simp_tac 1); |
2031 | 201 |
by (Asm_simp_tac 1); |
202 |
by (etac thin_rl 1); |
|
203 |
by (rtac allI 1); |
|
204 |
by (rtac iffI 1); |
|
2057 | 205 |
by (etac exE 1); |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
206 |
by (res_inst_tac [("x","Abs t")] exI 1); |
2057 | 207 |
by (Asm_simp_tac 1); |
2031 | 208 |
by (etac exE 1); |
209 |
by (etac rev_mp 1); |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
210 |
by (res_inst_tac [("dB","t")] dB_case_distinction 1); |
4686 | 211 |
by (Simp_tac 1); |
2057 | 212 |
by (Simp_tac 1); |
2031 | 213 |
by (Simp_tac 1); |
2891 | 214 |
by (Blast_tac 1); |
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1730
diff
changeset
|
215 |
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
|
216 |
|
5146 | 217 |
Goal "(!s u. (~free s 0) --> R(Abs(s $ Var 0))(s[u/0])) = \ |
218 |
\ (!s. R(Abs(lift s 0 $ Var 0))(s))"; |
|
4089 | 219 |
by (fast_tac (HOL_cs addss (simpset() addsimps [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
|
220 |
qed "explicit_is_implicit"; |