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