119 *} |
119 *} |
120 |
120 |
121 ML {* |
121 ML {* |
122 fun OF1 thm1 thm2 = thm2 RS thm1 |
122 fun OF1 thm1 thm2 = thm2 RS thm1 |
123 *} |
123 *} |
|
124 |
|
125 (* various tactic combinators *) |
|
126 ML {* |
|
127 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
|
128 *} |
|
129 |
|
130 ML {* |
|
131 (* prints warning, if goal is unsolved *) |
|
132 fun WARN (tac, msg) i st = |
|
133 case Seq.pull ((SOLVES' tac) i st) of |
|
134 NONE => (warning msg; Seq.single st) |
|
135 | seqcell => Seq.make (fn () => seqcell) |
|
136 |
|
137 fun RANGE_WARN xs = RANGE (map WARN xs) |
|
138 *} |
|
139 |
124 |
140 |
125 section {* Atomize Infrastructure *} |
141 section {* Atomize Infrastructure *} |
126 |
142 |
127 lemma atomize_eqv[atomize]: |
143 lemma atomize_eqv[atomize]: |
128 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
144 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
408 lemma eq_imp_rel: |
424 lemma eq_imp_rel: |
409 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
425 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
410 by (simp add: equivp_reflp) |
426 by (simp add: equivp_reflp) |
411 |
427 |
412 ML {* |
428 ML {* |
413 fun quotient_tac ctxt = |
429 (* test whether DETERM makes any difference *) |
414 REPEAT_ALL_NEW (DETERM o FIRST' |
430 fun quotient_tac ctxt = SOLVES' |
|
431 (REPEAT_ALL_NEW (FIRST' |
415 [rtac @{thm identity_quotient}, |
432 [rtac @{thm identity_quotient}, |
416 resolve_tac (quotient_rules_get ctxt)]) |
433 resolve_tac (quotient_rules_get ctxt)])) |
417 |
434 |
418 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
435 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
419 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
436 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
420 *} |
437 *} |
421 |
438 |
429 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" |
446 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" |
430 *} |
447 *} |
431 |
448 |
432 |
449 |
433 (* 0. preliminary simplification step according to *) |
450 (* 0. preliminary simplification step according to *) |
434 thm ball_reg_eqv bex_reg_eqv (* babs_reg_eqv is of no use *) |
451 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv |
435 ball_reg_eqv_range bex_reg_eqv_range |
452 ball_reg_eqv_range bex_reg_eqv_range |
436 (* 1. eliminating simple Ball/Bex instances*) |
453 (* 1. eliminating simple Ball/Bex instances*) |
437 thm ball_reg_right bex_reg_left |
454 thm ball_reg_right bex_reg_left |
438 (* 2. monos *) |
455 (* 2. monos *) |
439 (* 3. commutation rules for ball and bex *) |
456 (* 3. commutation rules for ball and bex *) |
451 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
468 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
452 val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
469 val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
453 val simpset = (mk_minimal_ss ctxt) |
470 val simpset = (mk_minimal_ss ctxt) |
454 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
471 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
455 addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver |
472 addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver |
456 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
|
457 (* can this cause loops in equiv_tac ? *) |
|
458 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
473 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
459 in |
474 in |
460 simp_tac simpset THEN' |
475 simp_tac simpset THEN' |
461 REPEAT_ALL_NEW (CHANGED o FIRST' [ |
476 REPEAT_ALL_NEW (CHANGED o FIRST' [ |
462 resolve_tac @{thms ball_reg_right bex_reg_left}, |
477 resolve_tac @{thms ball_reg_right bex_reg_left}, |
555 |
570 |
556 definition |
571 definition |
557 "QUOT_TRUE x \<equiv> True" |
572 "QUOT_TRUE x \<equiv> True" |
558 |
573 |
559 ML {* |
574 ML {* |
|
575 (* looks for QUOT_TRUE assumtions, and in case its argument *) |
|
576 (* is an application, it returns the function and the argument *) |
560 fun find_qt_asm asms = |
577 fun find_qt_asm asms = |
561 let |
578 let |
562 fun find_fun trm = |
579 fun find_fun trm = |
563 case trm of |
580 case trm of |
564 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
581 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
657 ML {* |
674 ML {* |
658 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
675 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
659 *} |
676 *} |
660 |
677 |
661 ML {* |
678 ML {* |
662 (* FIXME / TODO: what is asmf and asma in the code below *) |
679 (* we apply apply_rsp only in case if the type needs lifting, *) |
663 (* asmf is the QUOT_TRUE assumption function |
680 (* which is the case if the type of the data in the QUOT_TRUE *) |
664 asma are QUOT_TRUE assumption arguments *) |
681 (* assumption is different from the corresponding type in the goal *) |
665 val apply_rsp_tac = |
682 val apply_rsp_tac = |
666 Subgoal.FOCUS (fn {concl, asms, context,...} => |
683 Subgoal.FOCUS (fn {concl, asms, context,...} => |
667 let |
684 let |
668 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
685 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
669 val qt_asm = find_qt_asm (map term_of asms) |
686 val qt_asm = find_qt_asm (map term_of asms) |
670 in |
687 in |
671 case (bare_concl, qt_asm) of |
688 case (bare_concl, qt_asm) of |
672 (R2 $ (f $ x) $ (g $ y), SOME (asmf, asma)) => |
689 (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => |
673 if (fastype_of asmf) = (fastype_of f) |
690 if (fastype_of qt_fun) = (fastype_of f) |
674 then no_tac |
691 then no_tac |
675 else |
692 else |
676 let |
693 let |
677 val ty_x = fastype_of x |
694 val ty_x = fastype_of x |
678 val ty_b = fastype_of asma |
695 val ty_b = fastype_of qt_arg |
679 val ty_f = range_type (fastype_of f) |
696 val ty_f = range_type (fastype_of f) |
680 val thy = ProofContext.theory_of context |
697 val thy = ProofContext.theory_of context |
681 val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] |
698 val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] |
682 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
699 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
683 val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} |
700 val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} |
686 end |
703 end |
687 | _ => no_tac |
704 | _ => no_tac |
688 end) |
705 end) |
689 *} |
706 *} |
690 |
707 |
|
708 thm equals_rsp |
|
709 |
691 ML {* |
710 ML {* |
692 fun equals_rsp_tac R ctxt = |
711 fun equals_rsp_tac R ctxt = |
693 let |
712 let |
694 val ty = domain_type (fastype_of R); |
713 val ty = domain_type (fastype_of R); |
695 val thy = ProofContext.theory_of ctxt |
714 val thy = ProofContext.theory_of ctxt |
696 val thm = Drule.instantiate' |
715 val thm = Drule.instantiate' |
697 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
716 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
698 in |
717 in |
699 rtac thm THEN' quotient_tac ctxt |
718 rtac thm THEN' quotient_tac ctxt |
700 end |
719 end |
|
720 (* raised by instantiate' *) |
701 handle THM _ => K no_tac |
721 handle THM _ => K no_tac |
702 | TYPE _ => K no_tac |
722 | TYPE _ => K no_tac |
703 | TERM _ => K no_tac |
723 | TERM _ => K no_tac |
704 *} |
724 *} |
705 |
725 |
706 thm rep_abs_rsp |
726 ML {* |
707 |
|
708 ML {* |
|
709 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
|
710 |
|
711 fun rep_abs_rsp_tac ctxt = |
727 fun rep_abs_rsp_tac ctxt = |
712 SUBGOAL (fn (goal, i) => |
728 SUBGOAL (fn (goal, i) => |
713 case (bare_concl goal) of |
729 case (bare_concl goal) of |
714 (rel $ _ $ (rep $ (abs $ _))) => |
730 (rel $ _ $ (rep $ (abs $ _))) => |
715 (let |
731 (let |
717 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
733 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
718 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
734 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
719 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
735 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
720 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
736 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
721 in |
737 in |
722 (rtac inst_thm THEN' SOLVES' (quotient_tac ctxt)) i |
738 (rtac inst_thm THEN' quotient_tac ctxt) i |
723 end |
739 end |
724 handle THM _ => no_tac | TYPE _ => no_tac) |
740 handle THM _ => no_tac | TYPE _ => no_tac) |
725 | _ => no_tac) |
741 | _ => no_tac) |
726 *} |
742 *} |
727 |
743 |
904 let |
920 let |
905 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
921 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
906 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
922 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
907 in |
923 in |
908 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
924 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
909 end); |
925 end) |
910 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
926 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
911 (tracing "lambda_prs"; |
927 (tracing "lambda_prs"; |
912 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
928 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
913 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
929 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
914 tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
930 tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |