429 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" |
429 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" |
430 *} |
430 *} |
431 |
431 |
432 |
432 |
433 (* 0. preliminary simplification step according to *) |
433 (* 0. preliminary simplification step according to *) |
434 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *) |
434 thm ball_reg_eqv bex_reg_eqv (* babs_reg_eqv is of no use *) |
435 ball_reg_eqv_range bex_reg_eqv_range |
435 ball_reg_eqv_range bex_reg_eqv_range |
436 (* 1. eliminating simple Ball/Bex instances*) |
436 (* 1. eliminating simple Ball/Bex instances*) |
437 thm ball_reg_right bex_reg_left |
437 thm ball_reg_right bex_reg_left |
438 (* 2. monos *) |
438 (* 2. monos *) |
439 (* 3. commutation rules for ball and bex *) |
439 (* 3. commutation rules for ball and bex *) |
704 *} |
704 *} |
705 |
705 |
706 thm rep_abs_rsp |
706 thm rep_abs_rsp |
707 |
707 |
708 ML {* |
708 ML {* |
|
709 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
|
710 |
709 fun rep_abs_rsp_tac ctxt = |
711 fun rep_abs_rsp_tac ctxt = |
710 SUBGOAL (fn (goal, i) => |
712 SUBGOAL (fn (goal, i) => |
711 case (bare_concl goal) of |
713 case (bare_concl goal) of |
712 (rel $ _ $ (rep $ (abs $ _))) => |
714 (rel $ _ $ (rep $ (abs $ _))) => |
713 let |
715 (let |
714 val thy = ProofContext.theory_of ctxt; |
716 val thy = ProofContext.theory_of ctxt; |
715 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
717 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]; |
718 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]; |
719 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} |
720 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
719 in |
721 in |
720 (rtac inst_thm THEN' SOLVE o (quotient_tac ctxt)) i |
722 (rtac inst_thm THEN' SOLVES' (quotient_tac ctxt)) i |
721 end |
723 end |
|
724 handle THM _ => no_tac | TYPE _ => no_tac) |
722 | _ => no_tac) |
725 | _ => no_tac) |
723 *} |
726 *} |
724 |
727 |
725 ML {* |
728 ML {* |
726 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
729 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
1058 *} |
1061 *} |
1059 |
1062 |
1060 section {* Automatic Proofs *} |
1063 section {* Automatic Proofs *} |
1061 |
1064 |
1062 ML {* |
1065 ML {* |
1063 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
|
1064 |
|
1065 (* prints warning, if goal is unsolved *) |
1066 (* prints warning, if goal is unsolved *) |
1066 fun WARN (tac, msg) i st = |
1067 fun WARN (tac, msg) i st = |
1067 case Seq.pull ((SOLVES' tac) i st) of |
1068 case Seq.pull ((SOLVES' tac) i st) of |
1068 NONE => (warning msg; Seq.single st) |
1069 NONE => (warning msg; Seq.single st) |
1069 | seqcell => Seq.make (fn () => seqcell) |
1070 | seqcell => Seq.make (fn () => seqcell) |