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