author | wenzelm |
Wed, 15 Oct 1997 15:12:59 +0200 | |
changeset 3872 | a5839ecee7b8 |
parent 3840 | e0baea4d485a |
child 4091 | 771b1f6422a8 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: Substitution.ML |
1048 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Ole Rasmussen |
1048 | 4 |
Copyright 1995 University of Cambridge |
5 |
Logic Image: ZF |
|
6 |
*) |
|
7 |
||
8 |
open Substitution; |
|
9 |
||
10 |
(* ------------------------------------------------------------------------- *) |
|
11 |
(* Arithmetic extensions *) |
|
12 |
(* ------------------------------------------------------------------------- *) |
|
13 |
||
14 |
goal Arith.thy |
|
15 |
"!!m.[| p < n; n:nat|]==> n~=p"; |
|
2469 | 16 |
by (Fast_tac 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
17 |
qed "gt_not_eq"; |
1048 | 18 |
|
19 |
val succ_pred = prove_goal Arith.thy |
|
20 |
"!!i.[|j:nat; i:nat|]==> i < j --> succ(j #- 1) = j" |
|
21 |
(fn prems =>[(etac nat_induct 1), |
|
2469 | 22 |
(Fast_tac 1), |
23 |
(Asm_simp_tac 1)]); |
|
1048 | 24 |
|
25 |
goal Arith.thy |
|
26 |
"!!i.[|succ(x)<n; n:nat; x:nat|]==> x < n#-1 "; |
|
1461 | 27 |
by (rtac succ_leE 1); |
1048 | 28 |
by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); |
2469 | 29 |
by (asm_simp_tac (!simpset addsimps [succ_pred]) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
30 |
qed "lt_pred"; |
1048 | 31 |
|
32 |
goal Arith.thy |
|
33 |
"!!i.[|n < succ(x); p<n; p:nat; n:nat; x:nat|]==> n#-1 < x "; |
|
1461 | 34 |
by (rtac succ_leE 1); |
2469 | 35 |
by (asm_simp_tac (!simpset addsimps [succ_pred]) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
36 |
qed "gt_pred"; |
1048 | 37 |
|
38 |
||
2469 | 39 |
Addsimps [nat_into_Ord, not_lt_iff_le, if_P, if_not_P]; |
1048 | 40 |
|
41 |
||
42 |
(* ------------------------------------------------------------------------- *) |
|
43 |
(* lift_rec equality rules *) |
|
44 |
(* ------------------------------------------------------------------------- *) |
|
45 |
goalw Substitution.thy [lift_rec_def] |
|
46 |
"!!n.[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i<n,Var(i),Var(succ(i)))"; |
|
2469 | 47 |
by (Asm_full_simp_tac 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
48 |
qed "lift_rec_Var"; |
1048 | 49 |
|
50 |
goalw Substitution.thy [lift_rec_def] |
|
51 |
"!!n.[|n:nat; i:nat; k:nat; k le i|]==> lift_rec(Var(i),k) = Var(succ(i))"; |
|
2469 | 52 |
by (Asm_full_simp_tac 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
53 |
qed "lift_rec_le"; |
1048 | 54 |
|
55 |
goalw Substitution.thy [lift_rec_def] |
|
56 |
"!!n.[|i:nat; k:nat; i<k |]==> lift_rec(Var(i),k) = Var(i)"; |
|
2469 | 57 |
by (Asm_full_simp_tac 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
58 |
qed "lift_rec_gt"; |
1048 | 59 |
|
60 |
goalw Substitution.thy [lift_rec_def] |
|
61 |
"!!n.[|n:nat; k:nat|]==> \ |
|
62 |
\ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))"; |
|
2469 | 63 |
by (Asm_full_simp_tac 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
64 |
qed "lift_rec_Fun"; |
1048 | 65 |
|
66 |
goalw Substitution.thy [lift_rec_def] |
|
67 |
"!!n.[|n:nat; k:nat|]==> \ |
|
68 |
\ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))"; |
|
2469 | 69 |
by (Asm_full_simp_tac 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
70 |
qed "lift_rec_App"; |
1048 | 71 |
|
72 |
(* ------------------------------------------------------------------------- *) |
|
73 |
(* substitution quality rules *) |
|
74 |
(* ------------------------------------------------------------------------- *) |
|
75 |
||
76 |
goalw Substitution.thy [subst_rec_def] |
|
77 |
"!!n.[|i:nat; k:nat; u:redexes|]==> \ |
|
78 |
\ subst_rec(u,Var(i),k) = if(k<i,Var(i#-1),if(k=i,u,Var(i)))"; |
|
2469 | 79 |
by (asm_full_simp_tac (!simpset addsimps [gt_not_eq,leI]) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
80 |
qed "subst_Var"; |
1048 | 81 |
|
82 |
goalw Substitution.thy [subst_rec_def] |
|
83 |
"!!n.[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u"; |
|
2469 | 84 |
by (asm_full_simp_tac (!simpset) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
85 |
qed "subst_eq"; |
1048 | 86 |
|
87 |
goalw Substitution.thy [subst_rec_def] |
|
88 |
"!!n.[|n:nat; u:redexes; p:nat; p<n|]==> \ |
|
89 |
\ subst_rec(u,Var(n),p) = Var(n#-1)"; |
|
2469 | 90 |
by (asm_full_simp_tac (!simpset) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
91 |
qed "subst_gt"; |
1048 | 92 |
|
93 |
goalw Substitution.thy [subst_rec_def] |
|
94 |
"!!n.[|n:nat; u:redexes; p:nat; n<p|]==> \ |
|
95 |
\ subst_rec(u,Var(n),p) = Var(n)"; |
|
2469 | 96 |
by (asm_full_simp_tac (!simpset addsimps [gt_not_eq,leI]) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
97 |
qed "subst_lt"; |
1048 | 98 |
|
99 |
goalw Substitution.thy [subst_rec_def] |
|
100 |
"!!n.[|p:nat; u:redexes|]==> \ |
|
101 |
\ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) "; |
|
2469 | 102 |
by (asm_full_simp_tac (!simpset) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
103 |
qed "subst_Fun"; |
1048 | 104 |
|
105 |
goalw Substitution.thy [subst_rec_def] |
|
106 |
"!!n.[|p:nat; u:redexes|]==> \ |
|
107 |
\ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))"; |
|
2469 | 108 |
by (asm_full_simp_tac (!simpset) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
109 |
qed "subst_App"; |
1048 | 110 |
|
1723 | 111 |
fun addsplit ss = (ss setloop (split_inside_tac [expand_if]) |
1461 | 112 |
addsimps [lift_rec_Var,subst_Var]); |
1048 | 113 |
|
114 |
||
115 |
goal Substitution.thy |
|
3840 | 116 |
"!!n. u:redexes ==> ALL k:nat. lift_rec(u,k):redexes"; |
1048 | 117 |
by (eresolve_tac [redexes.induct] 1); |
118 |
by (ALLGOALS(asm_full_simp_tac |
|
2469 | 119 |
((addsplit (!simpset)) addsimps [lift_rec_Fun,lift_rec_App]))); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
120 |
qed "lift_rec_type_a"; |
1048 | 121 |
val lift_rec_type = lift_rec_type_a RS bspec; |
122 |
||
123 |
goalw Substitution.thy [] |
|
3840 | 124 |
"!!n. v:redexes ==> ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes"; |
1048 | 125 |
by (eresolve_tac [redexes.induct] 1); |
126 |
by (ALLGOALS(asm_full_simp_tac |
|
2469 | 127 |
((addsplit (!simpset)) addsimps [subst_Fun,subst_App, |
1461 | 128 |
lift_rec_type]))); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
129 |
qed "subst_type_a"; |
1048 | 130 |
val subst_type = subst_type_a RS bspec RS bspec; |
131 |
||
132 |
||
2469 | 133 |
Addsimps [subst_eq, subst_gt, subst_lt, subst_Fun, subst_App, subst_type, |
134 |
lift_rec_le, lift_rec_gt, lift_rec_Fun, lift_rec_App, |
|
135 |
lift_rec_type]; |
|
1048 | 136 |
|
137 |
||
138 |
(* ------------------------------------------------------------------------- *) |
|
139 |
(* lift and substitution proofs *) |
|
140 |
(* ------------------------------------------------------------------------- *) |
|
141 |
||
142 |
goalw Substitution.thy [] |
|
3840 | 143 |
"!!n. u:redexes ==> ALL n:nat. ALL i:nat. i le n --> \ |
1048 | 144 |
\ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"; |
145 |
by ((eresolve_tac [redexes.induct] 1) |
|
2469 | 146 |
THEN (ALLGOALS Asm_simp_tac)); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
147 |
by Safe_tac; |
1048 | 148 |
by (excluded_middle_tac "na < xa" 1); |
149 |
by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); |
|
150 |
by (ALLGOALS(asm_full_simp_tac |
|
2469 | 151 |
((addsplit (!simpset)) addsimps [leI]))); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
152 |
qed "lift_lift_rec"; |
1048 | 153 |
|
154 |
||
155 |
goalw Substitution.thy [] |
|
156 |
"!!n.[|u:redexes; n:nat|]==> \ |
|
157 |
\ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"; |
|
2469 | 158 |
by (asm_simp_tac (!simpset addsimps [lift_lift_rec]) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
159 |
qed "lift_lift"; |
1048 | 160 |
|
161 |
goal Substitution.thy |
|
3840 | 162 |
"!!n. v:redexes ==> \ |
163 |
\ ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\ |
|
1048 | 164 |
\ lift_rec(subst_rec(u,v,n),m) = \ |
165 |
\ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"; |
|
166 |
by ((eresolve_tac [redexes.induct] 1) |
|
2469 | 167 |
THEN (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])))); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
168 |
by Safe_tac; |
1048 | 169 |
by (excluded_middle_tac "na < x" 1); |
2469 | 170 |
by (asm_full_simp_tac (!simpset) 1); |
1048 | 171 |
by (eres_inst_tac [("j","na")] leE 1); |
2469 | 172 |
by (asm_full_simp_tac ((addsplit (!simpset)) |
1048 | 173 |
addsimps [leI,gt_pred,succ_pred]) 1); |
174 |
by (hyp_subst_tac 1); |
|
2469 | 175 |
by (asm_full_simp_tac (!simpset) 1); |
1048 | 176 |
by (forw_inst_tac [("j","x")] lt_trans2 1); |
177 |
by (assume_tac 1); |
|
2469 | 178 |
by (asm_full_simp_tac (!simpset addsimps [leI]) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
179 |
qed "lift_rec_subst_rec"; |
1048 | 180 |
|
181 |
goalw Substitution.thy [] |
|
182 |
"!!n.[|v:redexes; u:redexes; n:nat|]==> \ |
|
183 |
\ lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"; |
|
2469 | 184 |
by (asm_full_simp_tac (!simpset addsimps [lift_rec_subst_rec]) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
185 |
qed "lift_subst"; |
1048 | 186 |
|
187 |
||
188 |
goalw Substitution.thy [] |
|
3840 | 189 |
"!!n. v:redexes ==> \ |
190 |
\ ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\ |
|
1048 | 191 |
\ lift_rec(subst_rec(u,v,n),m) = \ |
192 |
\ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"; |
|
193 |
by ((eresolve_tac [redexes.induct] 1) |
|
2469 | 194 |
THEN (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])))); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
195 |
by Safe_tac; |
1048 | 196 |
by (excluded_middle_tac "na < x" 1); |
2469 | 197 |
by (asm_full_simp_tac (!simpset) 1); |
1048 | 198 |
by (eres_inst_tac [("i","x")] leE 1); |
199 |
by (forward_tac [lt_trans1] 1 THEN assume_tac 1); |
|
200 |
by (ALLGOALS(asm_full_simp_tac |
|
2469 | 201 |
(!simpset addsimps [succ_pred,leI,gt_pred]))); |
1048 | 202 |
by (hyp_subst_tac 1); |
2469 | 203 |
by (asm_full_simp_tac (!simpset addsimps [leI]) 1); |
1048 | 204 |
by (excluded_middle_tac "na < xa" 1); |
2469 | 205 |
by (asm_full_simp_tac (!simpset) 1); |
206 |
by (asm_full_simp_tac (!simpset addsimps [leI]) 1); |
|
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
207 |
qed "lift_rec_subst_rec_lt"; |
1048 | 208 |
|
209 |
||
210 |
goalw Substitution.thy [] |
|
3840 | 211 |
"!!n. u:redexes ==> \ |
212 |
\ ALL n:nat. ALL v:redexes. subst_rec(v,lift_rec(u,n),n) = u"; |
|
1048 | 213 |
by ((eresolve_tac [redexes.induct] 1) |
2469 | 214 |
THEN (ALLGOALS Asm_simp_tac)); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
215 |
by Safe_tac; |
1048 | 216 |
by (excluded_middle_tac "na < x" 1); |
217 |
(* x <= na *) |
|
2469 | 218 |
by (asm_full_simp_tac (!simpset) 1); |
219 |
by (asm_full_simp_tac (!simpset) 1); |
|
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
220 |
qed "subst_rec_lift_rec"; |
1048 | 221 |
|
222 |
goal Substitution.thy |
|
3840 | 223 |
"!!n. v:redexes ==> \ |
224 |
\ ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le n --> \ |
|
1048 | 225 |
\ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\ |
226 |
\ subst_rec(w,subst_rec(u,v,m),n)"; |
|
227 |
by ((eresolve_tac [redexes.induct] 1) THEN |
|
2469 | 228 |
(ALLGOALS(asm_simp_tac (!simpset addsimps |
1048 | 229 |
[lift_lift RS sym,lift_rec_subst_rec_lt])))); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
230 |
by Safe_tac; |
1048 | 231 |
by (excluded_middle_tac "na le succ(xa)" 1); |
2469 | 232 |
by (asm_full_simp_tac (!simpset) 1); |
1048 | 233 |
by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); |
1461 | 234 |
by (etac leE 1); |
2469 | 235 |
by (asm_simp_tac (!simpset addsimps [succ_pred,lt_pred]) 2); |
1048 | 236 |
by (forward_tac [succ_leI RS lt_trans] 1 THEN assume_tac 1); |
237 |
by (forw_inst_tac [("i","x")] |
|
238 |
(nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1); |
|
2469 | 239 |
by (asm_simp_tac (!simpset addsimps [succ_pred,lt_pred]) 1); |
1048 | 240 |
by (eres_inst_tac [("i","na")] leE 1); |
241 |
by (asm_full_simp_tac |
|
2469 | 242 |
(!simpset addsimps [succ_pred,subst_rec_lift_rec,leI]) 2); |
1048 | 243 |
by (excluded_middle_tac "na < x" 1); |
2469 | 244 |
by (asm_full_simp_tac (!simpset) 1); |
1048 | 245 |
by (eres_inst_tac [("j","na")] leE 1); |
2469 | 246 |
by (asm_simp_tac (!simpset addsimps [gt_pred]) 1); |
247 |
by (asm_simp_tac (!simpset addsimps [subst_rec_lift_rec]) 1); |
|
1048 | 248 |
by (forward_tac [lt_trans2] 1 THEN assume_tac 1); |
2469 | 249 |
by (asm_simp_tac (!simpset addsimps [gt_pred]) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
250 |
qed "subst_rec_subst_rec"; |
1048 | 251 |
|
252 |
||
253 |
goalw Substitution.thy [] |
|
254 |
"!!n.[|v:redexes; u:redexes; w:redexes; n:nat|]==> \ |
|
255 |
\ subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"; |
|
2469 | 256 |
by (asm_simp_tac (!simpset addsimps [subst_rec_subst_rec]) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
257 |
qed "substitution"; |
1048 | 258 |
|
259 |
(* ------------------------------------------------------------------------- *) |
|
260 |
(* Preservation lemmas *) |
|
261 |
(* Substitution preserves comp and regular *) |
|
262 |
(* ------------------------------------------------------------------------- *) |
|
263 |
||
264 |
||
265 |
goal Substitution.thy |
|
3840 | 266 |
"!!n.[|n:nat; u ~ v|]==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)"; |
1732 | 267 |
by (etac Scomp.induct 1); |
2469 | 268 |
by (ALLGOALS(asm_simp_tac (!simpset addsimps [comp_refl]))); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
269 |
qed "lift_rec_preserve_comp"; |
1048 | 270 |
|
271 |
goal Substitution.thy |
|
3840 | 272 |
"!!n. u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\ |
1048 | 273 |
\ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"; |
1732 | 274 |
by (etac Scomp.induct 1); |
2469 | 275 |
by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps |
1461 | 276 |
([lift_rec_preserve_comp,comp_refl])))); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
277 |
qed "subst_rec_preserve_comp"; |
1048 | 278 |
|
279 |
goal Substitution.thy |
|
3840 | 280 |
"!!n. regular(u) ==> ALL m:nat. regular(lift_rec(u,m))"; |
1048 | 281 |
by (eresolve_tac [Sreg.induct] 1); |
2469 | 282 |
by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset)))); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
283 |
qed "lift_rec_preserve_reg"; |
1048 | 284 |
|
285 |
goal Substitution.thy |
|
3840 | 286 |
"!!n. regular(v) ==> \ |
287 |
\ ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))"; |
|
1048 | 288 |
by (eresolve_tac [Sreg.induct] 1); |
2469 | 289 |
by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps |
1461 | 290 |
[lift_rec_preserve_reg]))); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
291 |
qed "subst_rec_preserve_reg"; |