342 done |
342 done |
343 |
343 |
344 lemma cheat: "P" sorry |
344 lemma cheat: "P" sorry |
345 |
345 |
346 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} |
346 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} |
347 ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] *} |
|
348 |
347 |
349 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
348 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
350 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
349 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
351 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
350 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
352 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
351 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
353 prefer 2 |
352 prefer 2 |
354 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
353 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
355 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *) |
354 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
356 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
355 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
357 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
356 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
358 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *) |
357 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
359 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
358 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
360 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
359 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
361 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
360 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
362 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
361 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
363 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
362 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
364 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
363 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
365 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
364 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
366 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *) |
365 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
367 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
366 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
368 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* D *) (* reflexivity of basic relations *) |
367 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *) |
369 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
368 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
370 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
369 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
371 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
370 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
372 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
371 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
373 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
372 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
374 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* C *) (* = and extensionality *) |
373 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *) |
375 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *) |
374 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
376 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
375 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
377 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
376 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
378 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
377 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
379 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
378 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
380 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
379 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
381 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
380 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
382 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
381 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
383 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *) |
382 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
384 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
383 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
385 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *) |
384 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
386 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
385 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
387 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
386 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
388 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *) |
387 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
389 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
388 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
390 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
389 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
391 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
390 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
392 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 7 *) (* respectfulness *) |
391 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *) |
393 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
392 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
394 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
393 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
395 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *) |
394 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
396 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
395 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
397 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
396 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
398 done |
397 done |
399 |
398 |
400 quotient_def |
399 quotient_def |
401 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
400 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
402 where |
401 where |
457 apply (rule FUN_QUOTIENT) |
456 apply (rule FUN_QUOTIENT) |
458 apply (rule QUOTIENT_fset) |
457 apply (rule QUOTIENT_fset) |
459 apply (rule IDENTITY_QUOTIENT) |
458 apply (rule IDENTITY_QUOTIENT) |
460 apply (rule IDENTITY_QUOTIENT) |
459 apply (rule IDENTITY_QUOTIENT) |
461 apply (rule IDENTITY_QUOTIENT) |
460 apply (rule IDENTITY_QUOTIENT) |
|
461 prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) |
|
462 prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) |
|
463 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
464 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
465 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
466 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
467 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
468 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
469 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
470 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
471 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
472 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
462 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
473 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
463 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
474 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
464 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
475 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
465 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
476 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
466 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
477 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
467 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
478 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
468 apply (rule IDENTITY_QUOTIENT) |
479 apply (rule IDENTITY_QUOTIENT) |
469 apply (rule IDENTITY_QUOTIENT) |
|
470 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
471 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
472 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
473 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
474 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
475 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
476 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
477 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
478 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
479 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
480 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
|
481 apply (rule IDENTITY_QUOTIENT) |
|
482 apply (rule FUN_QUOTIENT) |
480 apply (rule FUN_QUOTIENT) |
483 apply (rule QUOTIENT_fset) |
481 apply (rule QUOTIENT_fset) |
484 apply (rule IDENTITY_QUOTIENT) |
482 apply (rule IDENTITY_QUOTIENT) |
485 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
483 prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) |
486 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
484 prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) |
487 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
485 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
488 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
486 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
489 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
487 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
490 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
488 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
491 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
489 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
492 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
490 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
493 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
491 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
494 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
492 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
495 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
493 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
496 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
494 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
497 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
495 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
498 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
496 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
499 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
497 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
500 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
498 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
501 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
499 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
502 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
500 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
503 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
501 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
504 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) |
502 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
503 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
|
504 apply (rule IDENTITY_QUOTIENT) |
|
505 apply (rule FUN_QUOTIENT) |
|
506 apply (rule QUOTIENT_fset) |
|
507 apply (rule IDENTITY_QUOTIENT) |
|
508 prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) |
|
509 prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) |
|
510 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
505 apply assumption |
511 apply assumption |
506 apply (rule refl) |
512 apply (rule refl) |
507 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
513 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
508 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
514 apply assumption |
509 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
515 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
510 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
516 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
511 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) |
517 apply (rule IDENTITY_QUOTIENT) |
512 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
518 apply (rule FUN_QUOTIENT) |
513 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
519 apply (rule QUOTIENT_fset) |
|
520 apply (rule IDENTITY_QUOTIENT) |
|
521 prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) |
|
522 prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) |
|
523 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
524 apply assumption |
|
525 apply (rule refl) |
514 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *}) |
526 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *}) |
515 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
527 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
516 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
528 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
517 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) |
529 apply (rule IDENTITY_QUOTIENT) |
|
530 apply (rule FUN_QUOTIENT) |
|
531 apply (rule QUOTIENT_fset) |
|
532 apply (rule IDENTITY_QUOTIENT) |
|
533 prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) |
|
534 prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) |
|
535 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
518 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
536 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
519 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
537 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
520 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
538 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
521 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
539 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
522 done |
540 done |