equal
deleted
inserted
replaced
387 |
387 |
388 fun inj_repabs_tac ctxt = |
388 fun inj_repabs_tac ctxt = |
389 let |
389 let |
390 val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) |
390 val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) |
391 in |
391 in |
392 inj_repabs_step_tac ctxt rel_refl |
392 simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) |
|
393 THEN' inj_repabs_step_tac ctxt rel_refl |
393 end |
394 end |
394 |
395 |
395 fun all_inj_repabs_tac ctxt = |
396 fun all_inj_repabs_tac ctxt = |
396 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
397 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
397 |
398 |
489 (* 4. simplification with *) |
490 (* 4. simplification with *) |
490 (* thm Quotient_abs_rep Quotient_rel_rep id_simps *) |
491 (* thm Quotient_abs_rep Quotient_rel_rep id_simps *) |
491 (* *) |
492 (* *) |
492 (* 5. Test for refl *) |
493 (* 5. Test for refl *) |
493 |
494 |
494 fun clean_tac lthy = |
495 fun clean_tac_aux lthy = |
495 let |
496 let |
496 val thy = ProofContext.theory_of lthy; |
497 val thy = ProofContext.theory_of lthy; |
497 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
498 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
498 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
499 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
499 |
500 |
506 lambda_prs_tac lthy, |
507 lambda_prs_tac lthy, |
507 simp_tac (simps thms2), |
508 simp_tac (simps thms2), |
508 TRY o rtac refl] |
509 TRY o rtac refl] |
509 end |
510 end |
510 |
511 |
511 |
512 fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *) |
512 |
513 |
513 (* Tactic for Genralisation of Free Variables in a Goal *) |
514 (* Tactic for Genralisation of Free Variables in a Goal *) |
514 |
515 |
515 fun inst_spec ctrm = |
516 fun inst_spec ctrm = |
516 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
517 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |