433 (* 4. then rel-equality (which need to be instantiated to avoid loops *) |
433 (* 4. then rel-equality (which need to be instantiated to avoid loops *) |
434 thm eq_imp_rel |
434 thm eq_imp_rel |
435 (* 5. then simplification like 0 *) |
435 (* 5. then simplification like 0 *) |
436 (* finally jump back to 1 *) |
436 (* finally jump back to 1 *) |
437 |
437 |
|
438 ML {* |
|
439 fun quotient_tac ctxt = |
|
440 REPEAT_ALL_NEW (FIRST' |
|
441 [rtac @{thm identity_quotient}, |
|
442 resolve_tac (quotient_rules_get ctxt)]) |
|
443 |
|
444 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
|
445 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
|
446 *} |
438 |
447 |
439 ML {* |
448 ML {* |
440 fun regularize_tac ctxt = |
449 fun regularize_tac ctxt = |
441 let |
450 let |
442 val thy = ProofContext.theory_of ctxt |
451 val thy = ProofContext.theory_of ctxt |
443 val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} |
452 val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} |
444 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
453 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
445 val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
454 val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
446 val simpset = (mk_minimal_ss ctxt) |
455 val simpset = (mk_minimal_ss ctxt) |
447 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv} |
456 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
448 addsimprocs [simproc] addSolver equiv_solver |
457 addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver |
449 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
458 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
450 (* can this cause loops in equiv_tac ? *) |
459 (* can this cause loops in equiv_tac ? *) |
451 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
460 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
452 in |
461 in |
453 simp_tac simpset THEN' |
462 simp_tac simpset THEN' |
547 *} |
556 *} |
548 |
557 |
549 section {* Injection Tactic *} |
558 section {* Injection Tactic *} |
550 |
559 |
551 ML {* |
560 ML {* |
552 fun quotient_tac ctxt = |
|
553 REPEAT_ALL_NEW (FIRST' |
|
554 [rtac @{thm identity_quotient}, |
|
555 resolve_tac (quotient_rules_get ctxt)]) |
|
556 |
|
557 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
|
558 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
|
559 *} |
|
560 |
|
561 ML {* |
|
562 fun solve_quotient_assums ctxt thm = |
561 fun solve_quotient_assums ctxt thm = |
563 let |
562 let |
564 val goal = hd (Drule.strip_imp_prems (cprop_of thm)) |
563 val goal = hd (Drule.strip_imp_prems (cprop_of thm)) |
565 in |
564 in |
566 thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)] |
565 thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)] |
616 and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
615 and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
617 by (simp_all add: QUOT_TRUE_def ext) |
616 by (simp_all add: QUOT_TRUE_def ext) |
618 |
617 |
619 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
618 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
620 by (simp add: QUOT_TRUE_def) |
619 by (simp add: QUOT_TRUE_def) |
|
620 |
|
621 lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
|
622 by(auto simp add: QUOT_TRUE_def) |
621 |
623 |
622 ML {* |
624 ML {* |
623 fun quot_true_conv1 ctxt fnctn ctrm = |
625 fun quot_true_conv1 ctxt fnctn ctrm = |
624 case (term_of ctrm) of |
626 case (term_of ctrm) of |
625 (Const (@{const_name QUOT_TRUE}, _) $ x) => |
627 (Const (@{const_name QUOT_TRUE}, _) $ x) => |