219 ML {* val defs = |
219 ML {* val defs = |
220 @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def |
220 @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def |
221 FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} |
221 FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} |
222 *} |
222 *} |
223 |
223 |
224 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K'); |
224 lemma |
225 \<And>A A' K x x' K'. |
225 assumes a0: |
226 \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> |
226 "P1 TYP TYP" |
227 \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K'); |
227 and a1: |
228 \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j); |
228 "\<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> |
229 \<And>A A' M M'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P2 (TAPP A M) (TAPP A' M'); |
229 \<Longrightarrow> P1 (KPI A x K) (KPI A' x K')" |
230 \<And>A A' B B' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x B'); |
230 and a2: |
231 \<And>A A' B x x' B'. |
231 "\<And>A A' K K' x x'. \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); |
232 \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \<bullet> B'); P2 B ([(x, x')] \<bullet> B'); x \<notin> FV_ty B'; x \<notin> FV_ty B' - {x'}\<rbrakk> |
232 x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K')" |
233 \<Longrightarrow> P2 (TPI A x B) (TPI A' x' B'); |
233 and a3: |
234 \<And>i j m. i = j \<Longrightarrow> P3 (CONS i) (m (CONS j)); \<And>x y m. x = y \<Longrightarrow> P3 (VAR x) (m (VAR y)); |
234 "\<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j)" |
235 \<And>M m M' N N'. \<lbrakk>(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\<rbrakk> \<Longrightarrow> P3 (APP M N) (APP M' N'); |
235 and a4: |
236 \<And>A A' M M' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x M'); |
236 "\<And>A A' M M'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P2 (TAPP A M) (TAPP A' M')" |
237 \<And>A A' M x x' M' B'. |
237 and a5: |
238 \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> |
238 "\<And>A A' B B' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x B')" |
239 \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk> |
239 and a6: |
240 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
240 "\<And>A A' B x x' B'. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \<bullet> B'); P2 B ([(x, x')] \<bullet> B'); |
241 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
241 x \<notin> FV_ty B'; x \<notin> FV_ty B' - {x'}\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x' B')" |
|
242 and a7: |
|
243 "\<And>i j m. i = j \<Longrightarrow> P3 (CONS i) (m (CONS j))" |
|
244 and a8: |
|
245 "\<And>x y m. x = y \<Longrightarrow> P3 (VAR x) (m (VAR y))" |
|
246 and a9: |
|
247 "\<And>M m M' N N'. \<lbrakk>(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\<rbrakk> \<Longrightarrow> P3 (APP M N) (APP M' N')" |
|
248 and a10: |
|
249 "\<And>A A' M M' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x M')" |
|
250 and a11: |
|
251 "\<And>A A' M x x' M' B'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); |
|
252 x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')" |
|
253 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
|
254 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
|
255 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
|
256 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
|
257 apply - |
242 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
258 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
243 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
259 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
244 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *} |
260 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *} |
245 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
261 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
246 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
262 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
247 prefer 2 |
263 (* injecting *) |
|
264 ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *} |
|
265 ML_prf {* |
|
266 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
|
267 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs} |
|
268 *} |
|
269 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
270 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
271 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
272 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
273 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
274 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
275 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
276 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
277 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
278 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
279 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
280 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
281 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
282 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
283 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
284 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
285 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
286 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
287 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
288 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
289 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
290 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
291 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
292 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
293 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
294 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
295 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
296 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
297 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
298 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
299 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
300 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
301 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
302 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
303 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
304 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
305 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
306 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
307 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
308 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
309 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
310 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
311 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
312 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
313 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
314 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
315 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
316 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
317 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
318 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
319 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
320 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
321 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
322 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
323 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
324 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
325 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
326 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
327 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
328 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
329 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
330 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
331 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
332 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
333 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
334 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
335 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
336 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
337 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
338 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
339 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
340 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
341 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
342 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
343 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
344 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
345 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
346 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
347 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
348 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
349 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
350 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
351 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
352 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
353 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
354 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
355 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
356 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
357 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
358 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
359 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
360 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
361 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
362 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
363 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
364 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
365 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
366 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
367 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
368 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
369 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
370 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
371 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
372 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
373 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
374 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
375 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
376 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
377 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
378 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
379 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
380 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
381 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
382 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
383 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
384 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
385 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
386 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
387 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
388 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
389 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
390 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
391 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
392 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
393 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
394 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
395 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
396 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
397 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
398 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
399 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
400 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
401 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
402 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
403 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
404 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
405 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
406 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
407 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
408 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
409 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
410 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
411 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
412 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
413 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
414 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
415 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
416 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
417 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
418 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
419 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
420 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
421 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
422 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
423 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
424 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
425 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
426 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
427 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
428 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
429 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
430 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
431 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
432 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
433 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
434 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
435 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
436 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
437 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
438 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
439 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
440 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
441 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
442 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
443 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
444 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
445 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
446 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
447 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
448 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
449 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
450 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
451 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
452 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
453 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
454 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
455 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
456 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
457 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
458 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
459 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
460 (* cleaning *) |
248 ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *} |
461 ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *} |
249 (*apply(tactic {* clean_tac @{context} quot defs aps 1 *}) *) |
462 (*apply(tactic {* clean_tac @{context} quot defs aps 1 *}) *) |
250 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
463 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
251 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
464 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
252 ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *} |
465 ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *} |
277 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
490 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
278 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
491 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
279 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
492 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
280 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
493 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
281 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
494 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
282 ML_prf {* |
|
283 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
|
284 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs} |
|
285 *} |
|
286 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
287 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
288 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
289 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
290 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
291 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
292 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
293 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
294 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
295 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
296 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
297 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
298 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
299 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
300 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
301 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
302 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
303 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
304 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
305 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
306 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
307 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
308 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
309 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
310 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
311 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
312 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
313 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
314 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
315 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
316 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
317 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
318 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
319 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
320 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
321 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
322 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
323 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
324 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
325 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
326 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
327 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
328 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
329 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
330 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
331 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
332 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
333 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
334 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
335 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
336 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
337 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
338 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
339 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
340 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
341 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
342 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
343 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
344 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
345 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
346 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
347 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
348 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
349 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
350 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
351 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
352 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
353 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
354 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
355 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
356 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
357 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
358 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
359 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
360 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
361 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
362 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
363 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
364 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
365 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
366 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
367 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
368 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
369 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
370 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
371 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
372 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
373 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
374 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
375 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
376 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
377 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
378 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
379 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
380 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
381 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
382 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
383 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
384 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
385 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
386 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
387 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
388 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
389 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
390 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
391 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
392 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
393 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
394 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
395 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
396 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
397 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
398 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
399 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
400 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
401 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
402 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
403 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
404 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
405 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
406 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
407 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
408 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
409 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
410 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
411 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
412 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
413 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
414 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
415 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
416 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
417 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
418 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
419 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
420 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
421 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
422 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
423 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
424 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
425 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
426 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
427 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
428 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
429 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
430 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
431 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
432 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
433 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
434 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
435 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
436 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
437 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
438 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
439 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
440 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
441 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
442 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
443 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
444 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
445 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
446 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
447 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
448 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
449 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
450 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
451 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
452 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
453 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
454 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
455 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
456 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
457 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
458 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
459 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
460 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
461 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
462 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
463 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
464 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
465 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
466 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
467 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
468 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
469 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
470 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
471 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
472 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
473 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
474 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
475 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
476 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
477 done |
495 done |
478 |
496 |
479 print_quotients |
497 print_quotients |
480 |
498 |
481 end |
499 end |