74 (* ------------------------------------------------------------------------- *) |
74 (* ------------------------------------------------------------------------- *) |
75 |
75 |
76 goalw Substitution.thy [subst_rec_def] |
76 goalw Substitution.thy [subst_rec_def] |
77 "!!n.[|i:nat; k:nat; u:redexes|]==> \ |
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)))"; |
78 \ subst_rec(u,Var(i),k) = if(k<i,Var(i#-1),if(k=i,u,Var(i)))"; |
79 by (asm_full_simp_tac (!simpset addsimps [gt_not_eq,leI]) 1); |
79 by (asm_full_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1); |
80 qed "subst_Var"; |
80 qed "subst_Var"; |
81 |
81 |
82 goalw Substitution.thy [subst_rec_def] |
82 goalw Substitution.thy [subst_rec_def] |
83 "!!n.[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u"; |
83 "!!n.[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u"; |
84 by (asm_full_simp_tac (!simpset) 1); |
84 by (asm_full_simp_tac (simpset()) 1); |
85 qed "subst_eq"; |
85 qed "subst_eq"; |
86 |
86 |
87 goalw Substitution.thy [subst_rec_def] |
87 goalw Substitution.thy [subst_rec_def] |
88 "!!n.[|n:nat; u:redexes; p:nat; p<n|]==> \ |
88 "!!n.[|n:nat; u:redexes; p:nat; p<n|]==> \ |
89 \ subst_rec(u,Var(n),p) = Var(n#-1)"; |
89 \ subst_rec(u,Var(n),p) = Var(n#-1)"; |
90 by (asm_full_simp_tac (!simpset) 1); |
90 by (asm_full_simp_tac (simpset()) 1); |
91 qed "subst_gt"; |
91 qed "subst_gt"; |
92 |
92 |
93 goalw Substitution.thy [subst_rec_def] |
93 goalw Substitution.thy [subst_rec_def] |
94 "!!n.[|n:nat; u:redexes; p:nat; n<p|]==> \ |
94 "!!n.[|n:nat; u:redexes; p:nat; n<p|]==> \ |
95 \ subst_rec(u,Var(n),p) = Var(n)"; |
95 \ subst_rec(u,Var(n),p) = Var(n)"; |
96 by (asm_full_simp_tac (!simpset addsimps [gt_not_eq,leI]) 1); |
96 by (asm_full_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1); |
97 qed "subst_lt"; |
97 qed "subst_lt"; |
98 |
98 |
99 goalw Substitution.thy [subst_rec_def] |
99 goalw Substitution.thy [subst_rec_def] |
100 "!!n.[|p:nat; u:redexes|]==> \ |
100 "!!n.[|p:nat; u:redexes|]==> \ |
101 \ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) "; |
101 \ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) "; |
102 by (asm_full_simp_tac (!simpset) 1); |
102 by (asm_full_simp_tac (simpset()) 1); |
103 qed "subst_Fun"; |
103 qed "subst_Fun"; |
104 |
104 |
105 goalw Substitution.thy [subst_rec_def] |
105 goalw Substitution.thy [subst_rec_def] |
106 "!!n.[|p:nat; u:redexes|]==> \ |
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))"; |
107 \ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))"; |
108 by (asm_full_simp_tac (!simpset) 1); |
108 by (asm_full_simp_tac (simpset()) 1); |
109 qed "subst_App"; |
109 qed "subst_App"; |
110 |
110 |
111 fun addsplit ss = (ss setloop (split_inside_tac [expand_if]) |
111 fun addsplit ss = (ss setloop (split_inside_tac [expand_if]) |
112 addsimps [lift_rec_Var,subst_Var]); |
112 addsimps [lift_rec_Var,subst_Var]); |
113 |
113 |
114 |
114 |
115 goal Substitution.thy |
115 goal Substitution.thy |
116 "!!n. u:redexes ==> ALL k:nat. lift_rec(u,k):redexes"; |
116 "!!n. u:redexes ==> ALL k:nat. lift_rec(u,k):redexes"; |
117 by (eresolve_tac [redexes.induct] 1); |
117 by (eresolve_tac [redexes.induct] 1); |
118 by (ALLGOALS(asm_full_simp_tac |
118 by (ALLGOALS(asm_full_simp_tac |
119 ((addsplit (!simpset)) addsimps [lift_rec_Fun,lift_rec_App]))); |
119 ((addsplit (simpset())) addsimps [lift_rec_Fun,lift_rec_App]))); |
120 qed "lift_rec_type_a"; |
120 qed "lift_rec_type_a"; |
121 val lift_rec_type = lift_rec_type_a RS bspec; |
121 val lift_rec_type = lift_rec_type_a RS bspec; |
122 |
122 |
123 goalw Substitution.thy [] |
123 goalw Substitution.thy [] |
124 "!!n. v:redexes ==> ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes"; |
124 "!!n. v:redexes ==> ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes"; |
125 by (eresolve_tac [redexes.induct] 1); |
125 by (eresolve_tac [redexes.induct] 1); |
126 by (ALLGOALS(asm_full_simp_tac |
126 by (ALLGOALS(asm_full_simp_tac |
127 ((addsplit (!simpset)) addsimps [subst_Fun,subst_App, |
127 ((addsplit (simpset())) addsimps [subst_Fun,subst_App, |
128 lift_rec_type]))); |
128 lift_rec_type]))); |
129 qed "subst_type_a"; |
129 qed "subst_type_a"; |
130 val subst_type = subst_type_a RS bspec RS bspec; |
130 val subst_type = subst_type_a RS bspec RS bspec; |
131 |
131 |
132 |
132 |
146 THEN (ALLGOALS Asm_simp_tac)); |
146 THEN (ALLGOALS Asm_simp_tac)); |
147 by Safe_tac; |
147 by Safe_tac; |
148 by (excluded_middle_tac "na < xa" 1); |
148 by (excluded_middle_tac "na < xa" 1); |
149 by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); |
149 by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); |
150 by (ALLGOALS(asm_full_simp_tac |
150 by (ALLGOALS(asm_full_simp_tac |
151 ((addsplit (!simpset)) addsimps [leI]))); |
151 ((addsplit (simpset())) addsimps [leI]))); |
152 qed "lift_lift_rec"; |
152 qed "lift_lift_rec"; |
153 |
153 |
154 |
154 |
155 goalw Substitution.thy [] |
155 goalw Substitution.thy [] |
156 "!!n.[|u:redexes; n:nat|]==> \ |
156 "!!n.[|u:redexes; n:nat|]==> \ |
157 \ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"; |
157 \ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"; |
158 by (asm_simp_tac (!simpset addsimps [lift_lift_rec]) 1); |
158 by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1); |
159 qed "lift_lift"; |
159 qed "lift_lift"; |
160 |
160 |
161 goal Substitution.thy |
161 goal Substitution.thy |
162 "!!n. v:redexes ==> \ |
162 "!!n. v:redexes ==> \ |
163 \ ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\ |
163 \ ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\ |
164 \ lift_rec(subst_rec(u,v,n),m) = \ |
164 \ lift_rec(subst_rec(u,v,n),m) = \ |
165 \ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"; |
165 \ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"; |
166 by ((eresolve_tac [redexes.induct] 1) |
166 by ((eresolve_tac [redexes.induct] 1) |
167 THEN (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])))); |
167 THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])))); |
168 by Safe_tac; |
168 by Safe_tac; |
169 by (excluded_middle_tac "na < x" 1); |
169 by (excluded_middle_tac "na < x" 1); |
170 by (asm_full_simp_tac (!simpset) 1); |
170 by (asm_full_simp_tac (simpset()) 1); |
171 by (eres_inst_tac [("j","na")] leE 1); |
171 by (eres_inst_tac [("j","na")] leE 1); |
172 by (asm_full_simp_tac ((addsplit (!simpset)) |
172 by (asm_full_simp_tac ((addsplit (simpset())) |
173 addsimps [leI,gt_pred,succ_pred]) 1); |
173 addsimps [leI,gt_pred,succ_pred]) 1); |
174 by (hyp_subst_tac 1); |
174 by (hyp_subst_tac 1); |
175 by (asm_full_simp_tac (!simpset) 1); |
175 by (asm_full_simp_tac (simpset()) 1); |
176 by (forw_inst_tac [("j","x")] lt_trans2 1); |
176 by (forw_inst_tac [("j","x")] lt_trans2 1); |
177 by (assume_tac 1); |
177 by (assume_tac 1); |
178 by (asm_full_simp_tac (!simpset addsimps [leI]) 1); |
178 by (asm_full_simp_tac (simpset() addsimps [leI]) 1); |
179 qed "lift_rec_subst_rec"; |
179 qed "lift_rec_subst_rec"; |
180 |
180 |
181 goalw Substitution.thy [] |
181 goalw Substitution.thy [] |
182 "!!n.[|v:redexes; u:redexes; n:nat|]==> \ |
182 "!!n.[|v:redexes; u:redexes; n:nat|]==> \ |
183 \ lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"; |
183 \ lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"; |
184 by (asm_full_simp_tac (!simpset addsimps [lift_rec_subst_rec]) 1); |
184 by (asm_full_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1); |
185 qed "lift_subst"; |
185 qed "lift_subst"; |
186 |
186 |
187 |
187 |
188 goalw Substitution.thy [] |
188 goalw Substitution.thy [] |
189 "!!n. v:redexes ==> \ |
189 "!!n. v:redexes ==> \ |
190 \ ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\ |
190 \ ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\ |
191 \ lift_rec(subst_rec(u,v,n),m) = \ |
191 \ lift_rec(subst_rec(u,v,n),m) = \ |
192 \ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"; |
192 \ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"; |
193 by ((eresolve_tac [redexes.induct] 1) |
193 by ((eresolve_tac [redexes.induct] 1) |
194 THEN (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])))); |
194 THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])))); |
195 by Safe_tac; |
195 by Safe_tac; |
196 by (excluded_middle_tac "na < x" 1); |
196 by (excluded_middle_tac "na < x" 1); |
197 by (asm_full_simp_tac (!simpset) 1); |
197 by (asm_full_simp_tac (simpset()) 1); |
198 by (eres_inst_tac [("i","x")] leE 1); |
198 by (eres_inst_tac [("i","x")] leE 1); |
199 by (forward_tac [lt_trans1] 1 THEN assume_tac 1); |
199 by (forward_tac [lt_trans1] 1 THEN assume_tac 1); |
200 by (ALLGOALS(asm_full_simp_tac |
200 by (ALLGOALS(asm_full_simp_tac |
201 (!simpset addsimps [succ_pred,leI,gt_pred]))); |
201 (simpset() addsimps [succ_pred,leI,gt_pred]))); |
202 by (hyp_subst_tac 1); |
202 by (hyp_subst_tac 1); |
203 by (asm_full_simp_tac (!simpset addsimps [leI]) 1); |
203 by (asm_full_simp_tac (simpset() addsimps [leI]) 1); |
204 by (excluded_middle_tac "na < xa" 1); |
204 by (excluded_middle_tac "na < xa" 1); |
205 by (asm_full_simp_tac (!simpset) 1); |
205 by (asm_full_simp_tac (simpset()) 1); |
206 by (asm_full_simp_tac (!simpset addsimps [leI]) 1); |
206 by (asm_full_simp_tac (simpset() addsimps [leI]) 1); |
207 qed "lift_rec_subst_rec_lt"; |
207 qed "lift_rec_subst_rec_lt"; |
208 |
208 |
209 |
209 |
210 goalw Substitution.thy [] |
210 goalw Substitution.thy [] |
211 "!!n. u:redexes ==> \ |
211 "!!n. u:redexes ==> \ |
213 by ((eresolve_tac [redexes.induct] 1) |
213 by ((eresolve_tac [redexes.induct] 1) |
214 THEN (ALLGOALS Asm_simp_tac)); |
214 THEN (ALLGOALS Asm_simp_tac)); |
215 by Safe_tac; |
215 by Safe_tac; |
216 by (excluded_middle_tac "na < x" 1); |
216 by (excluded_middle_tac "na < x" 1); |
217 (* x <= na *) |
217 (* x <= na *) |
218 by (asm_full_simp_tac (!simpset) 1); |
218 by (asm_full_simp_tac (simpset()) 1); |
219 by (asm_full_simp_tac (!simpset) 1); |
219 by (asm_full_simp_tac (simpset()) 1); |
220 qed "subst_rec_lift_rec"; |
220 qed "subst_rec_lift_rec"; |
221 |
221 |
222 goal Substitution.thy |
222 goal Substitution.thy |
223 "!!n. v:redexes ==> \ |
223 "!!n. v:redexes ==> \ |
224 \ ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le n --> \ |
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)=\ |
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)"; |
226 \ subst_rec(w,subst_rec(u,v,m),n)"; |
227 by ((eresolve_tac [redexes.induct] 1) THEN |
227 by ((eresolve_tac [redexes.induct] 1) THEN |
228 (ALLGOALS(asm_simp_tac (!simpset addsimps |
228 (ALLGOALS(asm_simp_tac (simpset() addsimps |
229 [lift_lift RS sym,lift_rec_subst_rec_lt])))); |
229 [lift_lift RS sym,lift_rec_subst_rec_lt])))); |
230 by Safe_tac; |
230 by Safe_tac; |
231 by (excluded_middle_tac "na le succ(xa)" 1); |
231 by (excluded_middle_tac "na le succ(xa)" 1); |
232 by (asm_full_simp_tac (!simpset) 1); |
232 by (asm_full_simp_tac (simpset()) 1); |
233 by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); |
233 by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); |
234 by (etac leE 1); |
234 by (etac leE 1); |
235 by (asm_simp_tac (!simpset addsimps [succ_pred,lt_pred]) 2); |
235 by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 2); |
236 by (forward_tac [succ_leI RS lt_trans] 1 THEN assume_tac 1); |
236 by (forward_tac [succ_leI RS lt_trans] 1 THEN assume_tac 1); |
237 by (forw_inst_tac [("i","x")] |
237 by (forw_inst_tac [("i","x")] |
238 (nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1); |
238 (nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1); |
239 by (asm_simp_tac (!simpset addsimps [succ_pred,lt_pred]) 1); |
239 by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 1); |
240 by (eres_inst_tac [("i","na")] leE 1); |
240 by (eres_inst_tac [("i","na")] leE 1); |
241 by (asm_full_simp_tac |
241 by (asm_full_simp_tac |
242 (!simpset addsimps [succ_pred,subst_rec_lift_rec,leI]) 2); |
242 (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2); |
243 by (excluded_middle_tac "na < x" 1); |
243 by (excluded_middle_tac "na < x" 1); |
244 by (asm_full_simp_tac (!simpset) 1); |
244 by (asm_full_simp_tac (simpset()) 1); |
245 by (eres_inst_tac [("j","na")] leE 1); |
245 by (eres_inst_tac [("j","na")] leE 1); |
246 by (asm_simp_tac (!simpset addsimps [gt_pred]) 1); |
246 by (asm_simp_tac (simpset() addsimps [gt_pred]) 1); |
247 by (asm_simp_tac (!simpset addsimps [subst_rec_lift_rec]) 1); |
247 by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1); |
248 by (forward_tac [lt_trans2] 1 THEN assume_tac 1); |
248 by (forward_tac [lt_trans2] 1 THEN assume_tac 1); |
249 by (asm_simp_tac (!simpset addsimps [gt_pred]) 1); |
249 by (asm_simp_tac (simpset() addsimps [gt_pred]) 1); |
250 qed "subst_rec_subst_rec"; |
250 qed "subst_rec_subst_rec"; |
251 |
251 |
252 |
252 |
253 goalw Substitution.thy [] |
253 goalw Substitution.thy [] |
254 "!!n.[|v:redexes; u:redexes; w:redexes; n:nat|]==> \ |
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)"; |
255 \ subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"; |
256 by (asm_simp_tac (!simpset addsimps [subst_rec_subst_rec]) 1); |
256 by (asm_simp_tac (simpset() addsimps [subst_rec_subst_rec]) 1); |
257 qed "substitution"; |
257 qed "substitution"; |
258 |
258 |
259 (* ------------------------------------------------------------------------- *) |
259 (* ------------------------------------------------------------------------- *) |
260 (* Preservation lemmas *) |
260 (* Preservation lemmas *) |
261 (* Substitution preserves comp and regular *) |
261 (* Substitution preserves comp and regular *) |
263 |
263 |
264 |
264 |
265 goal Substitution.thy |
265 goal Substitution.thy |
266 "!!n.[|n:nat; u ~ v|]==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)"; |
266 "!!n.[|n:nat; u ~ v|]==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)"; |
267 by (etac Scomp.induct 1); |
267 by (etac Scomp.induct 1); |
268 by (ALLGOALS(asm_simp_tac (!simpset addsimps [comp_refl]))); |
268 by (ALLGOALS(asm_simp_tac (simpset() addsimps [comp_refl]))); |
269 qed "lift_rec_preserve_comp"; |
269 qed "lift_rec_preserve_comp"; |
270 |
270 |
271 goal Substitution.thy |
271 goal Substitution.thy |
272 "!!n. u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\ |
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)"; |
273 \ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"; |
274 by (etac Scomp.induct 1); |
274 by (etac Scomp.induct 1); |
275 by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps |
275 by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps |
276 ([lift_rec_preserve_comp,comp_refl])))); |
276 ([lift_rec_preserve_comp,comp_refl])))); |
277 qed "subst_rec_preserve_comp"; |
277 qed "subst_rec_preserve_comp"; |
278 |
278 |
279 goal Substitution.thy |
279 goal Substitution.thy |
280 "!!n. regular(u) ==> ALL m:nat. regular(lift_rec(u,m))"; |
280 "!!n. regular(u) ==> ALL m:nat. regular(lift_rec(u,m))"; |
281 by (eresolve_tac [Sreg.induct] 1); |
281 by (eresolve_tac [Sreg.induct] 1); |
282 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset)))); |
282 by (ALLGOALS(asm_full_simp_tac (addsplit (simpset())))); |
283 qed "lift_rec_preserve_reg"; |
283 qed "lift_rec_preserve_reg"; |
284 |
284 |
285 goal Substitution.thy |
285 goal Substitution.thy |
286 "!!n. regular(v) ==> \ |
286 "!!n. regular(v) ==> \ |
287 \ ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))"; |
287 \ ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))"; |
288 by (eresolve_tac [Sreg.induct] 1); |
288 by (eresolve_tac [Sreg.induct] 1); |
289 by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps |
289 by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps |
290 [lift_rec_preserve_reg]))); |
290 [lift_rec_preserve_reg]))); |
291 qed "subst_rec_preserve_reg"; |
291 qed "subst_rec_preserve_reg"; |