41 |
41 |
42 (* ------------------------------------------------------------------------- *) |
42 (* ------------------------------------------------------------------------- *) |
43 (* lift_rec equality rules *) |
43 (* lift_rec equality rules *) |
44 (* ------------------------------------------------------------------------- *) |
44 (* ------------------------------------------------------------------------- *) |
45 Goalw [lift_rec_def] |
45 Goalw [lift_rec_def] |
46 "!!n.[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i<n,Var(i),Var(succ(i)))"; |
46 "[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i<n,Var(i),Var(succ(i)))"; |
47 by (Asm_full_simp_tac 1); |
47 by (Asm_full_simp_tac 1); |
48 qed "lift_rec_Var"; |
48 qed "lift_rec_Var"; |
49 |
49 |
50 Goalw [lift_rec_def] |
50 Goalw [lift_rec_def] |
51 "!!n.[|n:nat; i:nat; k:nat; k le i|]==> lift_rec(Var(i),k) = Var(succ(i))"; |
51 "[|n:nat; i:nat; k:nat; k le i|]==> lift_rec(Var(i),k) = Var(succ(i))"; |
52 by (Asm_full_simp_tac 1); |
52 by (Asm_full_simp_tac 1); |
53 qed "lift_rec_le"; |
53 qed "lift_rec_le"; |
54 |
54 |
55 Goalw [lift_rec_def] |
55 Goalw [lift_rec_def] |
56 "!!n.[|i:nat; k:nat; i<k |]==> lift_rec(Var(i),k) = Var(i)"; |
56 "[|i:nat; k:nat; i<k |]==> lift_rec(Var(i),k) = Var(i)"; |
57 by (Asm_full_simp_tac 1); |
57 by (Asm_full_simp_tac 1); |
58 qed "lift_rec_gt"; |
58 qed "lift_rec_gt"; |
59 |
59 |
60 Goalw [lift_rec_def] |
60 Goalw [lift_rec_def] |
61 "!!n.[|n:nat; k:nat|]==> \ |
61 "[|n:nat; k:nat|]==> \ |
62 \ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))"; |
62 \ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))"; |
63 by (Asm_full_simp_tac 1); |
63 by (Asm_full_simp_tac 1); |
64 qed "lift_rec_Fun"; |
64 qed "lift_rec_Fun"; |
65 |
65 |
66 Goalw [lift_rec_def] |
66 Goalw [lift_rec_def] |
67 "!!n.[|n:nat; k:nat|]==> \ |
67 "[|n:nat; k:nat|]==> \ |
68 \ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))"; |
68 \ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))"; |
69 by (Asm_full_simp_tac 1); |
69 by (Asm_full_simp_tac 1); |
70 qed "lift_rec_App"; |
70 qed "lift_rec_App"; |
71 |
71 |
72 (* ------------------------------------------------------------------------- *) |
72 (* ------------------------------------------------------------------------- *) |
73 (* substitution quality rules *) |
73 (* substitution quality rules *) |
74 (* ------------------------------------------------------------------------- *) |
74 (* ------------------------------------------------------------------------- *) |
75 |
75 |
76 Goalw [subst_rec_def] |
76 Goalw [subst_rec_def] |
77 "!!n.[|i:nat; k:nat; u:redexes|]==> \ |
77 "[|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 [subst_rec_def] |
82 Goalw [subst_rec_def] |
83 "!!n.[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u"; |
83 "[|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 [subst_rec_def] |
87 Goalw [subst_rec_def] |
88 "!!n.[|n:nat; u:redexes; p:nat; p<n|]==> \ |
88 "[|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 [subst_rec_def] |
93 Goalw [subst_rec_def] |
94 "!!n.[|n:nat; u:redexes; p:nat; n<p|]==> \ |
94 "[|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 [subst_rec_def] |
99 Goalw [subst_rec_def] |
100 "!!n.[|p:nat; u:redexes|]==> \ |
100 "[|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 [subst_rec_def] |
105 Goalw [subst_rec_def] |
106 "!!n.[|p:nat; u:redexes|]==> \ |
106 "[|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 [split_if]) |
111 fun addsplit ss = (ss setloop (split_inside_tac [split_if]) |
112 addsimps [lift_rec_Var,subst_Var]); |
112 addsimps [lift_rec_Var,subst_Var]); |
113 |
113 |
114 |
114 |
115 Goal |
115 Goal |
116 "!!n. u:redexes ==> ALL k:nat. lift_rec(u,k):redexes"; |
116 "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 [] |
123 Goal "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); |
124 by (eresolve_tac [redexes.induct] 1); |
126 by (ALLGOALS(asm_full_simp_tac |
125 by (ALLGOALS(asm_full_simp_tac |
127 ((addsplit (simpset())) addsimps [subst_Fun,subst_App, |
126 ((addsplit (simpset())) addsimps [subst_Fun,subst_App, |
128 lift_rec_type]))); |
127 lift_rec_type]))); |
129 qed "subst_type_a"; |
128 qed "subst_type_a"; |
137 |
136 |
138 (* ------------------------------------------------------------------------- *) |
137 (* ------------------------------------------------------------------------- *) |
139 (* lift and substitution proofs *) |
138 (* lift and substitution proofs *) |
140 (* ------------------------------------------------------------------------- *) |
139 (* ------------------------------------------------------------------------- *) |
141 |
140 |
142 Goalw [] |
141 Goal "u:redexes ==> ALL n:nat. ALL i:nat. i le n --> \ |
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))"; |
142 \ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"; |
145 by ((eresolve_tac [redexes.induct] 1) |
143 by ((eresolve_tac [redexes.induct] 1) THEN (ALLGOALS Asm_simp_tac)); |
146 THEN (ALLGOALS Asm_simp_tac)); |
144 by Safe_tac; |
147 by Safe_tac; |
145 by (excluded_middle_tac "n < xa" 1); |
148 by (excluded_middle_tac "na < xa" 1); |
|
149 by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); |
146 by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); |
150 by (ALLGOALS(asm_full_simp_tac |
147 by (ALLGOALS (asm_full_simp_tac (addsplit (simpset()) addsimps [leI]))); |
151 ((addsplit (simpset())) addsimps [leI]))); |
|
152 qed "lift_lift_rec"; |
148 qed "lift_lift_rec"; |
153 |
149 |
154 |
150 |
155 Goalw [] |
151 Goal "[|u:redexes; n:nat|]==> \ |
156 "!!n.[|u:redexes; n:nat|]==> \ |
|
157 \ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"; |
152 \ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"; |
158 by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1); |
153 by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1); |
159 qed "lift_lift"; |
154 qed "lift_lift"; |
160 |
155 |
161 Goal |
156 Goal "v:redexes ==> \ |
162 "!!n. v:redexes ==> \ |
|
163 \ ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\ |
157 \ ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\ |
164 \ lift_rec(subst_rec(u,v,n),m) = \ |
158 \ lift_rec(subst_rec(u,v,n),m) = \ |
165 \ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"; |
159 \ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"; |
166 by ((eresolve_tac [redexes.induct] 1) |
160 by ((eresolve_tac [redexes.induct] 1) |
167 THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])))); |
161 THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])))); |
168 by Safe_tac; |
162 by Safe_tac; |
169 by (excluded_middle_tac "na < x" 1); |
163 by (excluded_middle_tac "n < x" 1); |
170 by (asm_full_simp_tac (simpset()) 1); |
164 by (asm_full_simp_tac (simpset()) 1); |
171 by (eres_inst_tac [("j","na")] leE 1); |
165 by (eres_inst_tac [("j","n")] leE 1); |
172 by (asm_full_simp_tac ((addsplit (simpset())) |
166 by (asm_full_simp_tac ((addsplit (simpset())) |
173 addsimps [leI,gt_pred,succ_pred]) 1); |
167 addsimps [leI,gt_pred,succ_pred]) 1); |
174 by (hyp_subst_tac 1); |
168 by (hyp_subst_tac 1); |
175 by (asm_full_simp_tac (simpset()) 1); |
169 by (asm_full_simp_tac (simpset()) 1); |
176 by (forw_inst_tac [("j","x")] lt_trans2 1); |
170 by (forw_inst_tac [("j","x")] lt_trans2 1); |
177 by (assume_tac 1); |
171 by (assume_tac 1); |
178 by (asm_full_simp_tac (simpset() addsimps [leI]) 1); |
172 by (asm_full_simp_tac (simpset() addsimps [leI]) 1); |
179 qed "lift_rec_subst_rec"; |
173 qed "lift_rec_subst_rec"; |
180 |
174 |
181 Goalw [] |
175 Goal "[|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))"; |
176 \ 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); |
177 by (asm_full_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1); |
185 qed "lift_subst"; |
178 qed "lift_subst"; |
186 |
179 |
187 |
180 |
188 Goalw [] |
181 Goal "v:redexes ==> \ |
189 "!!n. v:redexes ==> \ |
|
190 \ ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\ |
182 \ ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\ |
191 \ lift_rec(subst_rec(u,v,n),m) = \ |
183 \ lift_rec(subst_rec(u,v,n),m) = \ |
192 \ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"; |
184 \ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"; |
193 by ((eresolve_tac [redexes.induct] 1) |
185 by ((eresolve_tac [redexes.induct] 1) |
194 THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])))); |
186 THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])))); |
195 by Safe_tac; |
187 by Safe_tac; |
196 by (excluded_middle_tac "na < x" 1); |
188 by (excluded_middle_tac "n < x" 1); |
197 by (asm_full_simp_tac (simpset()) 1); |
189 by (asm_full_simp_tac (simpset()) 1); |
198 by (eres_inst_tac [("i","x")] leE 1); |
190 by (eres_inst_tac [("i","x")] leE 1); |
199 by (forward_tac [lt_trans1] 1 THEN assume_tac 1); |
191 by (forward_tac [lt_trans1] 1 THEN assume_tac 1); |
200 by (ALLGOALS(asm_full_simp_tac |
192 by (ALLGOALS(asm_full_simp_tac |
201 (simpset() addsimps [succ_pred,leI,gt_pred]))); |
193 (simpset() addsimps [succ_pred,leI,gt_pred]))); |
202 by (asm_full_simp_tac (simpset() addsimps [leI]) 1); |
194 by (asm_full_simp_tac (simpset() addsimps [leI]) 1); |
203 by (excluded_middle_tac "na < xa" 1); |
195 by (excluded_middle_tac "n < xa" 1); |
204 by (asm_full_simp_tac (simpset()) 1); |
196 by (asm_full_simp_tac (simpset()) 1); |
205 by (asm_full_simp_tac (simpset() addsimps [leI]) 1); |
197 by (asm_full_simp_tac (simpset() addsimps [leI]) 1); |
206 qed "lift_rec_subst_rec_lt"; |
198 qed "lift_rec_subst_rec_lt"; |
207 |
199 |
208 |
200 |
209 Goalw [] |
201 Goal "u:redexes ==> \ |
210 "!!n. u:redexes ==> \ |
|
211 \ ALL n:nat. ALL v:redexes. subst_rec(v,lift_rec(u,n),n) = u"; |
202 \ ALL n:nat. ALL v:redexes. subst_rec(v,lift_rec(u,n),n) = u"; |
212 by ((eresolve_tac [redexes.induct] 1) |
203 by ((eresolve_tac [redexes.induct] 1) |
213 THEN (ALLGOALS Asm_simp_tac)); |
204 THEN (ALLGOALS Asm_simp_tac)); |
214 by Safe_tac; |
205 by Safe_tac; |
215 by (excluded_middle_tac "na < x" 1); |
206 by (excluded_middle_tac "n < x" 1); |
216 (* x <= na *) |
207 (* x <= n *) |
217 by (asm_full_simp_tac (simpset()) 1); |
208 by (asm_full_simp_tac (simpset()) 1); |
218 by (asm_full_simp_tac (simpset()) 1); |
209 by (asm_full_simp_tac (simpset()) 1); |
219 qed "subst_rec_lift_rec"; |
210 qed "subst_rec_lift_rec"; |
220 |
211 |
221 Goal |
212 Goal |
222 "!!n. v:redexes ==> \ |
213 "v:redexes ==> \ |
223 \ ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le n --> \ |
214 \ ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le n --> \ |
224 \ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\ |
215 \ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\ |
225 \ subst_rec(w,subst_rec(u,v,m),n)"; |
216 \ subst_rec(w,subst_rec(u,v,m),n)"; |
226 by ((eresolve_tac [redexes.induct] 1) THEN |
217 by ((eresolve_tac [redexes.induct] 1) THEN |
227 (ALLGOALS(asm_simp_tac (simpset() addsimps |
218 (ALLGOALS(asm_simp_tac (simpset() addsimps |
228 [lift_lift RS sym,lift_rec_subst_rec_lt])))); |
219 [lift_lift RS sym,lift_rec_subst_rec_lt])))); |
229 by Safe_tac; |
220 by Safe_tac; |
230 by (excluded_middle_tac "na le succ(xa)" 1); |
221 by (excluded_middle_tac "n le succ(xa)" 1); |
231 by (asm_full_simp_tac (simpset()) 1); |
222 by (asm_full_simp_tac (simpset()) 1); |
232 by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); |
223 by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); |
233 by (etac leE 1); |
224 by (etac leE 1); |
234 by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 2); |
225 by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 2); |
235 by (forward_tac [succ_leI RS lt_trans] 1 THEN assume_tac 1); |
226 by (forward_tac [succ_leI RS lt_trans] 1 THEN assume_tac 1); |
236 by (forw_inst_tac [("i","x")] |
227 by (forw_inst_tac [("i","x")] |
237 (nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1); |
228 (nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1); |
238 by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 1); |
229 by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 1); |
239 by (eres_inst_tac [("i","na")] leE 1); |
230 by (eres_inst_tac [("i","n")] leE 1); |
240 by (asm_full_simp_tac |
231 by (asm_full_simp_tac |
241 (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2); |
232 (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2); |
242 by (excluded_middle_tac "na < x" 1); |
233 by (excluded_middle_tac "n < x" 1); |
243 by (asm_full_simp_tac (simpset()) 1); |
234 by (asm_full_simp_tac (simpset()) 1); |
244 by (eres_inst_tac [("j","na")] leE 1); |
235 by (eres_inst_tac [("j","n")] leE 1); |
245 by (asm_simp_tac (simpset() addsimps [gt_pred]) 1); |
236 by (asm_simp_tac (simpset() addsimps [gt_pred]) 1); |
246 by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1); |
237 by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1); |
247 by (forward_tac [lt_trans2] 1 THEN assume_tac 1); |
238 by (forward_tac [lt_trans2] 1 THEN assume_tac 1); |
248 by (asm_simp_tac (simpset() addsimps [gt_pred]) 1); |
239 by (asm_simp_tac (simpset() addsimps [gt_pred]) 1); |
249 qed "subst_rec_subst_rec"; |
240 qed "subst_rec_subst_rec"; |
250 |
241 |
251 |
242 |
252 Goalw [] |
243 Goal "[|v:redexes; u:redexes; w:redexes; n:nat|]==> \ |
253 "!!n.[|v:redexes; u:redexes; w:redexes; n:nat|]==> \ |
|
254 \ subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"; |
244 \ subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"; |
255 by (asm_simp_tac (simpset() addsimps [subst_rec_subst_rec]) 1); |
245 by (asm_simp_tac (simpset() addsimps [subst_rec_subst_rec]) 1); |
256 qed "substitution"; |
246 qed "substitution"; |
257 |
247 |
258 (* ------------------------------------------------------------------------- *) |
248 (* ------------------------------------------------------------------------- *) |
259 (* Preservation lemmas *) |
249 (* Preservation lemmas *) |
260 (* Substitution preserves comp and regular *) |
250 (* Substitution preserves comp and regular *) |
261 (* ------------------------------------------------------------------------- *) |
251 (* ------------------------------------------------------------------------- *) |
262 |
252 |
263 |
253 |
264 Goal |
254 Goal "[|n:nat; u ~ v|]==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)"; |
265 "!!n.[|n:nat; u ~ v|]==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)"; |
|
266 by (etac Scomp.induct 1); |
255 by (etac Scomp.induct 1); |
267 by (ALLGOALS(asm_simp_tac (simpset() addsimps [comp_refl]))); |
256 by (ALLGOALS(asm_simp_tac (simpset() addsimps [comp_refl]))); |
268 qed "lift_rec_preserve_comp"; |
257 qed "lift_rec_preserve_comp"; |
269 |
258 |
270 Goal |
259 Goal "u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\ |
271 "!!n. u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\ |
|
272 \ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"; |
260 \ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"; |
273 by (etac Scomp.induct 1); |
261 by (etac Scomp.induct 1); |
274 by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps |
262 by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps |
275 ([lift_rec_preserve_comp,comp_refl])))); |
263 ([lift_rec_preserve_comp,comp_refl])))); |
276 qed "subst_rec_preserve_comp"; |
264 qed "subst_rec_preserve_comp"; |
277 |
265 |
278 Goal |
266 Goal "regular(u) ==> ALL m:nat. regular(lift_rec(u,m))"; |
279 "!!n. regular(u) ==> ALL m:nat. regular(lift_rec(u,m))"; |
|
280 by (eresolve_tac [Sreg.induct] 1); |
267 by (eresolve_tac [Sreg.induct] 1); |
281 by (ALLGOALS(asm_full_simp_tac (addsplit (simpset())))); |
268 by (ALLGOALS(asm_full_simp_tac (addsplit (simpset())))); |
282 qed "lift_rec_preserve_reg"; |
269 qed "lift_rec_preserve_reg"; |
283 |
270 |
284 Goal |
271 Goal "regular(v) ==> \ |
285 "!!n. regular(v) ==> \ |
|
286 \ ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))"; |
272 \ ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))"; |
287 by (eresolve_tac [Sreg.induct] 1); |
273 by (eresolve_tac [Sreg.induct] 1); |
288 by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps |
274 by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps |
289 [lift_rec_preserve_reg]))); |
275 [lift_rec_preserve_reg]))); |
290 qed "subst_rec_preserve_reg"; |
276 qed "subst_rec_preserve_reg"; |