author | paulson |
Thu, 26 Sep 1996 12:47:47 +0200 | |
changeset 2031 | 03a843f0f447 |
parent 1974 | b50f96543dec |
child 2116 | 73bbf2cc7651 |
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 |
||
6 |
Substitution-lemmas. Most of the proofs, esp. those about natural numbers, |
|
7 |
are ported from Ole Rasmussen's ZF development. In ZF, m<=n is syntactic |
|
8 |
sugar for m<Suc(n). In HOL <= is a separate operator. Hence we have to prove |
|
9 |
some compatibility lemmas. |
|
10 |
*) |
|
11 |
||
12 |
(*** Nat ***) |
|
13 |
||
14 |
goal Nat.thy "!!i. [| i < Suc j; j < k |] ==> i < k"; |
|
1465 | 15 |
by (rtac le_less_trans 1); |
16 |
by (assume_tac 2); |
|
2031 | 17 |
by (asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1); |
18 |
by (fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1); |
|
1120 | 19 |
qed "lt_trans1"; |
20 |
||
21 |
goal Nat.thy "!!i. [| i < j; j < Suc(k) |] ==> i < k"; |
|
1465 | 22 |
by (etac less_le_trans 1); |
2031 | 23 |
by (asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1); |
24 |
by (fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1); |
|
1120 | 25 |
qed "lt_trans2"; |
26 |
||
27 |
val major::prems = goal Nat.thy |
|
28 |
"[| i < Suc j; i < j ==> P; i = j ==> P |] ==> P"; |
|
1465 | 29 |
by (rtac (major RS lessE) 1); |
2031 | 30 |
by (ALLGOALS Asm_full_simp_tac); |
31 |
by (resolve_tac prems 1 THEN etac sym 1); |
|
32 |
by (fast_tac (HOL_cs addIs prems) 1); |
|
1120 | 33 |
qed "leqE"; |
34 |
||
35 |
goal Arith.thy "!!i. Suc i < j ==> i < pred j "; |
|
1465 | 36 |
by (rtac Suc_less_SucD 1); |
1302 | 37 |
by (Asm_simp_tac 1); |
1120 | 38 |
qed "lt_pred"; |
39 |
||
40 |
goal Arith.thy "!!i. [| i < Suc j; k < i |] ==> pred i < j "; |
|
1465 | 41 |
by (rtac Suc_less_SucD 1); |
1302 | 42 |
by (Asm_simp_tac 1); |
1120 | 43 |
qed "gt_pred"; |
44 |
||
1153 | 45 |
|
1120 | 46 |
(*** Lambda ***) |
47 |
||
48 |
open Lambda; |
|
49 |
||
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
50 |
Delsimps [subst_Var]; |
1269 | 51 |
Addsimps ([if_not_P, not_less_eq] @ beta.intrs); |
1120 | 52 |
|
1302 | 53 |
(* don't add r_into_rtrancl! *) |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
54 |
AddSIs beta.intrs; |
1120 | 55 |
|
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1723
diff
changeset
|
56 |
val db_case_distinction = |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1723
diff
changeset
|
57 |
rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])db.induct; |
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1723
diff
changeset
|
58 |
|
1120 | 59 |
(*** Congruence rules for ->> ***) |
60 |
||
61 |
goal Lambda.thy "!!s. s ->> s' ==> Fun s ->> Fun s'"; |
|
1465 | 62 |
by (etac rtrancl_induct 1); |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
63 |
by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl]))); |
1120 | 64 |
qed "rtrancl_beta_Fun"; |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
65 |
AddSIs [rtrancl_beta_Fun]; |
1120 | 66 |
|
67 |
goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t"; |
|
1465 | 68 |
by (etac rtrancl_induct 1); |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
69 |
by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl]))); |
1120 | 70 |
qed "rtrancl_beta_AppL"; |
71 |
||
72 |
goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'"; |
|
1465 | 73 |
by (etac rtrancl_induct 1); |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
74 |
by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl]))); |
1120 | 75 |
qed "rtrancl_beta_AppR"; |
76 |
||
77 |
goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'"; |
|
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
78 |
by (deepen_tac (!claset addSIs [rtrancl_beta_AppL,rtrancl_beta_AppR] |
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
79 |
addIs [rtrancl_trans]) 3 1); |
1120 | 80 |
qed "rtrancl_beta_App"; |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
81 |
AddIs [rtrancl_beta_App]; |
1120 | 82 |
|
83 |
(*** subst and lift ***) |
|
84 |
||
1723 | 85 |
fun addsplit ss = ss addsimps [subst_Var] setloop (split_inside_tac [expand_if]); |
1120 | 86 |
|
1153 | 87 |
goal Lambda.thy "(Var k)[u/k] = u"; |
1269 | 88 |
by (asm_full_simp_tac(addsplit(!simpset)) 1); |
1120 | 89 |
qed "subst_eq"; |
90 |
||
1153 | 91 |
goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(pred j)"; |
1269 | 92 |
by (asm_full_simp_tac(addsplit(!simpset)) 1); |
1120 | 93 |
qed "subst_gt"; |
94 |
||
1153 | 95 |
goal Lambda.thy "!!s. j<i ==> (Var j)[u/i] = Var(j)"; |
1269 | 96 |
by (asm_full_simp_tac (addsplit(!simpset) addsimps |
1120 | 97 |
[less_not_refl2 RS not_sym,less_SucI]) 1); |
98 |
qed "subst_lt"; |
|
99 |
||
1266 | 100 |
Addsimps [subst_eq,subst_gt,subst_lt]; |
1120 | 101 |
|
102 |
goal Lambda.thy |
|
1172 | 103 |
"!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i"; |
2031 | 104 |
by (db.induct_tac "t" 1); |
105 |
by (ALLGOALS Asm_simp_tac); |
|
106 |
by (strip_tac 1); |
|
1120 | 107 |
by (excluded_middle_tac "nat < i" 1); |
108 |
by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); |
|
1269 | 109 |
by (ALLGOALS(asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI]))); |
1486 | 110 |
qed_spec_mp "lift_lift"; |
1120 | 111 |
|
1153 | 112 |
goal Lambda.thy "!i j s. j < Suc i --> \ |
113 |
\ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]"; |
|
2031 | 114 |
by (db.induct_tac "t" 1); |
115 |
by (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift]))); |
|
116 |
by (strip_tac 1); |
|
1153 | 117 |
by (excluded_middle_tac "nat < j" 1); |
1269 | 118 |
by (Asm_full_simp_tac 1); |
1120 | 119 |
by (eres_inst_tac [("j","nat")] leqE 1); |
1269 | 120 |
by (asm_full_simp_tac (addsplit(!simpset) |
1302 | 121 |
addsimps [less_SucI,gt_pred]) 1); |
1120 | 122 |
by (hyp_subst_tac 1); |
1266 | 123 |
by (Asm_simp_tac 1); |
1153 | 124 |
by (forw_inst_tac [("j","j")] lt_trans2 1); |
1120 | 125 |
by (assume_tac 1); |
1269 | 126 |
by (asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI]) 1); |
1120 | 127 |
qed "lift_subst"; |
1266 | 128 |
Addsimps [lift_subst]; |
1120 | 129 |
|
130 |
goal Lambda.thy |
|
1172 | 131 |
"!i j s. i < Suc j -->\ |
132 |
\ lift (t[s/j]) i = (lift t i) [lift s i / Suc j]"; |
|
2031 | 133 |
by (db.induct_tac "t" 1); |
134 |
by (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift]))); |
|
135 |
by (strip_tac 1); |
|
1153 | 136 |
by (excluded_middle_tac "nat < j" 1); |
1269 | 137 |
by (Asm_full_simp_tac 1); |
1153 | 138 |
by (eres_inst_tac [("i","j")] leqE 1); |
1120 | 139 |
by (forward_tac [lt_trans1] 1 THEN assume_tac 1); |
1269 | 140 |
by (ALLGOALS(asm_full_simp_tac |
1302 | 141 |
(!simpset addsimps [less_SucI,gt_pred]))); |
1120 | 142 |
by (hyp_subst_tac 1); |
1269 | 143 |
by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1); |
2031 | 144 |
by (split_tac [expand_if] 1); |
1266 | 145 |
by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1); |
1120 | 146 |
qed "lift_subst_lt"; |
147 |
||
1172 | 148 |
goal Lambda.thy "!k s. (lift t k)[s/k] = t"; |
2031 | 149 |
by (db.induct_tac "t" 1); |
150 |
by (ALLGOALS Asm_simp_tac); |
|
151 |
by (split_tac [expand_if] 1); |
|
152 |
by (ALLGOALS Asm_full_simp_tac); |
|
1120 | 153 |
qed "subst_lift"; |
1266 | 154 |
Addsimps [subst_lift]; |
1120 | 155 |
|
156 |
||
1172 | 157 |
goal Lambda.thy "!i j u v. i < Suc j --> \ |
158 |
\ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"; |
|
2031 | 159 |
by (db.induct_tac "t" 1); |
160 |
by (ALLGOALS(asm_simp_tac(!simpset addsimps [lift_lift RS sym,lift_subst_lt]))); |
|
161 |
by (strip_tac 1); |
|
1153 | 162 |
by (excluded_middle_tac "nat < Suc(Suc j)" 1); |
2031 | 163 |
by (Asm_full_simp_tac 1); |
1120 | 164 |
by (forward_tac [lessI RS less_trans] 1); |
1465 | 165 |
by (etac leqE 1); |
1302 | 166 |
by (asm_simp_tac (!simpset addsimps [lt_pred]) 2); |
1120 | 167 |
by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1); |
1153 | 168 |
by (forw_inst_tac [("i","i")] (lessI RS less_trans) 1); |
1302 | 169 |
by (asm_simp_tac (!simpset addsimps [lt_pred]) 1); |
1120 | 170 |
by (eres_inst_tac [("i","nat")] leqE 1); |
1302 | 171 |
by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 2); |
1153 | 172 |
by (excluded_middle_tac "nat < i" 1); |
1269 | 173 |
by (Asm_full_simp_tac 1); |
1120 | 174 |
by (eres_inst_tac [("j","nat")] leqE 1); |
1266 | 175 |
by (asm_simp_tac (!simpset addsimps [gt_pred]) 1); |
176 |
by (Asm_simp_tac 1); |
|
1120 | 177 |
by (forward_tac [lt_trans2] 1 THEN assume_tac 1); |
1266 | 178 |
by (asm_simp_tac (!simpset addsimps [gt_pred]) 1); |
1486 | 179 |
qed_spec_mp "subst_subst"; |
1153 | 180 |
|
181 |
||
182 |
(*** Equivalence proof for optimized substitution ***) |
|
183 |
||
184 |
goal Lambda.thy "!k. liftn 0 t k = t"; |
|
2031 | 185 |
by (db.induct_tac "t" 1); |
186 |
by (ALLGOALS(asm_simp_tac(addsplit(!simpset)))); |
|
1153 | 187 |
qed "liftn_0"; |
1266 | 188 |
Addsimps [liftn_0]; |
1153 | 189 |
|
190 |
goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k"; |
|
2031 | 191 |
by (db.induct_tac "t" 1); |
192 |
by (ALLGOALS(asm_simp_tac(addsplit(!simpset)))); |
|
193 |
by (fast_tac (HOL_cs addDs [add_lessD1]) 1); |
|
1153 | 194 |
qed "liftn_lift"; |
1266 | 195 |
Addsimps [liftn_lift]; |
1153 | 196 |
|
197 |
goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]"; |
|
2031 | 198 |
by (db.induct_tac "t" 1); |
199 |
by (ALLGOALS(asm_simp_tac(addsplit(!simpset)))); |
|
1153 | 200 |
qed "substn_subst_n"; |
1266 | 201 |
Addsimps [substn_subst_n]; |
1153 | 202 |
|
203 |
goal Lambda.thy "substn t s 0 = t[s/0]"; |
|
2031 | 204 |
by (Simp_tac 1); |
1153 | 205 |
qed "substn_subst_0"; |