409 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
409 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
410 by (simp add: equivp_reflp) |
410 by (simp add: equivp_reflp) |
411 |
411 |
412 ML {* |
412 ML {* |
413 fun quotient_tac ctxt = |
413 fun quotient_tac ctxt = |
414 DETERM o REPEAT_ALL_NEW (FIRST' |
414 REPEAT_ALL_NEW (DETERM o FIRST' |
415 [rtac @{thm identity_quotient}, |
415 [rtac @{thm identity_quotient}, |
416 resolve_tac (quotient_rules_get ctxt)]) |
416 resolve_tac (quotient_rules_get ctxt)]) |
417 |
417 |
418 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
418 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
419 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
419 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
708 ML {* |
708 ML {* |
709 fun rep_abs_rsp_tac ctxt = |
709 fun rep_abs_rsp_tac ctxt = |
710 SUBGOAL (fn (goal, i) => |
710 SUBGOAL (fn (goal, i) => |
711 case (bare_concl goal) of |
711 case (bare_concl goal) of |
712 (rel $ _ $ (rep $ (abs $ _))) => |
712 (rel $ _ $ (rep $ (abs $ _))) => |
713 (let |
713 let |
714 val thy = ProofContext.theory_of ctxt; |
714 val thy = ProofContext.theory_of ctxt; |
715 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
715 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
716 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
716 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
717 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
717 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
718 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
718 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
719 in |
719 in |
720 (rtac inst_thm THEN' quotient_tac ctxt) i |
720 (rtac inst_thm THEN' SOLVE o (quotient_tac ctxt)) i |
721 end |
721 end |
722 handle _ => no_tac) (* FIXME / TODO what is the catch for ? Should go away, no? *) |
|
723 (* The catch was for an error of solve_quotient_assum. You replaced it by quotient_tac |
|
724 so I suppose it is equivalent to a "SOLVES" around quotient_tac. *) |
|
725 | _ => no_tac) |
722 | _ => no_tac) |
726 *} |
723 *} |
727 |
724 |
728 ML {* |
725 ML {* |
729 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
726 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |