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);
|
1048
|
17 |
val gt_not_eq = result();
|
|
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);
|
1048
|
30 |
val lt_pred = result();
|
|
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);
|
1048
|
36 |
val gt_pred = result();
|
|
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);
|
1048
|
48 |
val lift_rec_Var = result();
|
|
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);
|
1048
|
53 |
val lift_rec_le = result();
|
|
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);
|
1048
|
58 |
val lift_rec_gt = result();
|
|
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);
|
1048
|
64 |
val lift_rec_Fun = result();
|
|
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);
|
1048
|
70 |
val lift_rec_App = result();
|
|
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);
|
1048
|
80 |
val subst_Var = result();
|
|
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);
|
1048
|
85 |
val subst_eq = result();
|
|
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);
|
1048
|
91 |
val subst_gt = result();
|
|
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);
|
1048
|
97 |
val subst_lt = result();
|
|
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);
|
1048
|
103 |
val subst_Fun = result();
|
|
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);
|
1048
|
109 |
val subst_App = result();
|
|
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
|
|
116 |
"!!n.u:redexes ==> ALL k:nat.lift_rec(u,k):redexes";
|
|
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])));
|
1048
|
120 |
val lift_rec_type_a = result();
|
|
121 |
val lift_rec_type = lift_rec_type_a RS bspec;
|
|
122 |
|
|
123 |
goalw Substitution.thy []
|
|
124 |
"!!n.v:redexes ==> ALL n:nat.ALL u:redexes.subst_rec(u,v,n):redexes";
|
|
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])));
|
1048
|
129 |
val subst_type_a = result();
|
|
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 []
|
|
143 |
"!!n.u:redexes ==> ALL n:nat.ALL i:nat.i le n --> \
|
|
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));
|
|
147 |
by (step_tac (!claset) 1);
|
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])));
|
1048
|
152 |
val lift_lift_rec = result();
|
|
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);
|
1048
|
159 |
val lift_lift = result();
|
|
160 |
|
|
161 |
goal Substitution.thy
|
|
162 |
"!!n.v:redexes ==> \
|
|
163 |
\ ALL n:nat.ALL m:nat.ALL u:redexes.n le m-->\
|
|
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]))));
|
|
168 |
by (step_tac (!claset) 1);
|
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);
|
1048
|
179 |
val lift_rec_subst_rec = result();
|
|
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);
|
1048
|
185 |
val lift_subst = result();
|
|
186 |
|
|
187 |
|
|
188 |
goalw Substitution.thy []
|
|
189 |
"!!n.v:redexes ==> \
|
|
190 |
\ ALL n:nat.ALL m:nat.ALL u:redexes.m le n-->\
|
|
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]))));
|
|
195 |
by (step_tac (!claset) 1);
|
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);
|
1048
|
207 |
val lift_rec_subst_rec_lt = result();
|
|
208 |
|
|
209 |
|
|
210 |
goalw Substitution.thy []
|
|
211 |
"!!n.u:redexes ==> \
|
|
212 |
\ ALL n:nat.ALL v:redexes.subst_rec(v,lift_rec(u,n),n) = u";
|
|
213 |
by ((eresolve_tac [redexes.induct] 1)
|
2469
|
214 |
THEN (ALLGOALS Asm_simp_tac));
|
|
215 |
by (step_tac (!claset) 1);
|
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);
|
1048
|
220 |
val subst_rec_lift_rec = result();
|
|
221 |
|
|
222 |
goal Substitution.thy
|
|
223 |
"!!n.v:redexes ==> \
|
|
224 |
\ ALL m:nat.ALL n:nat.ALL u:redexes.ALL w:redexes.m le n --> \
|
|
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]))));
|
2469
|
230 |
by (step_tac (!claset) 1);
|
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);
|
1048
|
250 |
val subst_rec_subst_rec = result();
|
|
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);
|
1048
|
257 |
val substitution = result();
|
|
258 |
|
|
259 |
(* ------------------------------------------------------------------------- *)
|
|
260 |
(* Preservation lemmas *)
|
|
261 |
(* Substitution preserves comp and regular *)
|
|
262 |
(* ------------------------------------------------------------------------- *)
|
|
263 |
|
|
264 |
|
|
265 |
goal Substitution.thy
|
|
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])));
|
1048
|
269 |
val lift_rec_preserve_comp = result();
|
|
270 |
|
|
271 |
goal Substitution.thy
|
|
272 |
"!!n.u2 ~ v2 ==> ALL m:nat.ALL u1:redexes.ALL v1:redexes.\
|
|
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]))));
|
1048
|
277 |
val subst_rec_preserve_comp = result();
|
|
278 |
|
|
279 |
goal Substitution.thy
|
|
280 |
"!!n.regular(u) ==> ALL m:nat.regular(lift_rec(u,m))";
|
|
281 |
by (eresolve_tac [Sreg.induct] 1);
|
2469
|
282 |
by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset))));
|
1048
|
283 |
val lift_rec_preserve_reg = result();
|
|
284 |
|
|
285 |
goal Substitution.thy
|
|
286 |
"!!n.regular(v) ==> \
|
|
287 |
\ ALL m:nat.ALL u:redexes.regular(u)-->regular(subst_rec(u,v,m))";
|
|
288 |
by (eresolve_tac [Sreg.induct] 1);
|
2469
|
289 |
by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps
|
1461
|
290 |
[lift_rec_preserve_reg])));
|
1048
|
291 |
val subst_rec_preserve_reg = result();
|