author | nipkow |
Fri, 27 Nov 1998 17:00:30 +0100 | |
changeset 5983 | 79e301a6a51b |
parent 5351 | 6d6467c2b8b9 |
child 6055 | fdf4638bf726 |
permissions | -rw-r--r-- |
1269 | 1 |
(* Title: HOL/Lambda/Lambda.ML |
1120 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
||
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
6 |
Substitution-lemmas. |
1120 | 7 |
*) |
8 |
||
9 |
(*** Lambda ***) |
|
10 |
||
5261
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
11 |
val beta_cases = map (beta.mk_cases dB.simps) |
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
12 |
["Var i -> t", "Abs r -> s", "s $ t -> u"]; |
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
13 |
AddSEs beta_cases; |
1120 | 14 |
|
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
15 |
Delsimps [subst_Var]; |
1269 | 16 |
Addsimps ([if_not_P, not_less_eq] @ beta.intrs); |
1120 | 17 |
|
1302 | 18 |
(* don't add r_into_rtrancl! *) |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
19 |
AddSIs beta.intrs; |
1120 | 20 |
|
21 |
(*** Congruence rules for ->> ***) |
|
22 |
||
5117 | 23 |
Goal "s ->> s' ==> Abs s ->> Abs s'"; |
1465 | 24 |
by (etac rtrancl_induct 1); |
4089 | 25 |
by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
26 |
qed "rtrancl_beta_Abs"; |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
27 |
AddSIs [rtrancl_beta_Abs]; |
1120 | 28 |
|
5146 | 29 |
Goal "s ->> s' ==> s $ t ->> s' $ t"; |
1465 | 30 |
by (etac rtrancl_induct 1); |
4089 | 31 |
by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
1120 | 32 |
qed "rtrancl_beta_AppL"; |
33 |
||
5146 | 34 |
Goal "t ->> t' ==> s $ t ->> s $ t'"; |
1465 | 35 |
by (etac rtrancl_induct 1); |
4089 | 36 |
by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
1120 | 37 |
qed "rtrancl_beta_AppR"; |
38 |
||
5146 | 39 |
Goal "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'"; |
4089 | 40 |
by (blast_tac (claset() addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR] |
2922 | 41 |
addIs [rtrancl_trans]) 1); |
1120 | 42 |
qed "rtrancl_beta_App"; |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
43 |
AddIs [rtrancl_beta_App]; |
1120 | 44 |
|
45 |
(*** subst and lift ***) |
|
46 |
||
3919 | 47 |
fun addsplit ss = ss addsimps [subst_Var] |
4831 | 48 |
delsplits [split_if] |
49 |
setloop (split_inside_tac [split_if]); |
|
1120 | 50 |
|
5069 | 51 |
Goal "(Var k)[u/k] = u"; |
4089 | 52 |
by (asm_full_simp_tac(addsplit(simpset())) 1); |
1120 | 53 |
qed "subst_eq"; |
54 |
||
5117 | 55 |
Goal "i<j ==> (Var j)[u/i] = Var(j-1)"; |
4089 | 56 |
by (asm_full_simp_tac(addsplit(simpset())) 1); |
1120 | 57 |
qed "subst_gt"; |
58 |
||
5117 | 59 |
Goal "j<i ==> (Var j)[u/i] = Var(j)"; |
5351 | 60 |
by (asm_full_simp_tac (addsplit(simpset()) addsimps [less_not_refl3]) 1); |
1120 | 61 |
qed "subst_lt"; |
62 |
||
1266 | 63 |
Addsimps [subst_eq,subst_gt,subst_lt]; |
1120 | 64 |
|
5069 | 65 |
Goal |
1172 | 66 |
"!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i"; |
5184 | 67 |
by (induct_tac "t" 1); |
5983 | 68 |
by (Auto_tac); |
1486 | 69 |
qed_spec_mp "lift_lift"; |
1120 | 70 |
|
5117 | 71 |
Goal "!i j s. j < Suc i --> lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]"; |
5184 | 72 |
by (induct_tac "t" 1); |
4360 | 73 |
by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift] |
5983 | 74 |
addsplits [nat.split]))); |
75 |
by (Auto_tac); |
|
1120 | 76 |
qed "lift_subst"; |
1266 | 77 |
Addsimps [lift_subst]; |
1120 | 78 |
|
5069 | 79 |
Goal |
5117 | 80 |
"!i j s. i < Suc j --> lift (t[s/j]) i = (lift t i) [lift s i / Suc j]"; |
5184 | 81 |
by (induct_tac "t" 1); |
5983 | 82 |
by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift]))); |
1120 | 83 |
qed "lift_subst_lt"; |
84 |
||
5069 | 85 |
Goal "!k s. (lift t k)[s/k] = t"; |
5184 | 86 |
by (induct_tac "t" 1); |
4686 | 87 |
by (ALLGOALS Asm_full_simp_tac); |
1120 | 88 |
qed "subst_lift"; |
1266 | 89 |
Addsimps [subst_lift]; |
1120 | 90 |
|
91 |
||
5117 | 92 |
Goal "!i j u v. i < Suc j --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"; |
5184 | 93 |
by (induct_tac "t" 1); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
94 |
by (ALLGOALS(asm_simp_tac |
4360 | 95 |
(simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt] |
5983 | 96 |
addsplits [nat.split]))); |
2922 | 97 |
by (safe_tac (HOL_cs addSEs [nat_neqE])); |
5983 | 98 |
by (ALLGOALS Simp_tac); |
1486 | 99 |
qed_spec_mp "subst_subst"; |
1153 | 100 |
|
101 |
||
102 |
(*** Equivalence proof for optimized substitution ***) |
|
103 |
||
5069 | 104 |
Goal "!k. liftn 0 t k = t"; |
5184 | 105 |
by (induct_tac "t" 1); |
4089 | 106 |
by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
1153 | 107 |
qed "liftn_0"; |
1266 | 108 |
Addsimps [liftn_0]; |
1153 | 109 |
|
5069 | 110 |
Goal "!k. liftn (Suc n) t k = lift (liftn n t k) k"; |
5184 | 111 |
by (induct_tac "t" 1); |
4089 | 112 |
by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
113 |
by (blast_tac (claset() addDs [add_lessD1]) 1); |
|
1153 | 114 |
qed "liftn_lift"; |
1266 | 115 |
Addsimps [liftn_lift]; |
1153 | 116 |
|
5069 | 117 |
Goal "!n. substn t s n = t[liftn n s 0 / n]"; |
5184 | 118 |
by (induct_tac "t" 1); |
4089 | 119 |
by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
1153 | 120 |
qed "substn_subst_n"; |
1266 | 121 |
Addsimps [substn_subst_n]; |
1153 | 122 |
|
5069 | 123 |
Goal "substn t s 0 = t[s/0]"; |
2031 | 124 |
by (Simp_tac 1); |
1153 | 125 |
qed "substn_subst_0"; |
5261
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
126 |
|
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
127 |
(*** Preservation thms ***) |
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
128 |
(* Not used in CR-proof but in SN-proof *) |
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
129 |
|
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
130 |
Goal "r -> s ==> !t i. r[t/i] -> s[t/i]"; |
5326 | 131 |
by (etac beta.induct 1); |
5318 | 132 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [subst_subst RS sym]))); |
5261
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
133 |
qed_spec_mp "subst_preserves_beta"; |
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
134 |
Addsimps [subst_preserves_beta]; |
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
135 |
|
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
136 |
Goal "r -> s ==> !i. lift r i -> lift s i"; |
5326 | 137 |
by (etac beta.induct 1); |
5318 | 138 |
by (Auto_tac); |
5261
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
139 |
qed_spec_mp "lift_preserves_beta"; |
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
140 |
Addsimps [lift_preserves_beta]; |
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
141 |
|
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
142 |
Goal "!r s i. r -> s --> t[r/i] ->> t[s/i]"; |
5318 | 143 |
by (induct_tac "t" 1); |
144 |
by (asm_simp_tac (addsplit(simpset() addsimps [r_into_rtrancl])) 1); |
|
145 |
by (asm_simp_tac (simpset() addsimps [rtrancl_beta_App]) 1); |
|
146 |
by (asm_simp_tac (simpset() addsimps [rtrancl_beta_Abs]) 1); |
|
5261
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
147 |
qed_spec_mp "subst_preserves_beta2"; |
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
5184
diff
changeset
|
148 |
Addsimps [subst_preserves_beta2]; |