327 |
327 |
328 | (Bound i, Bound i') => |
328 | (Bound i, Bound i') => |
329 if i = i' then rtrm |
329 if i = i' then rtrm |
330 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
330 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
331 |
331 |
332 | (rt, qt) => |
332 | _ => |
333 let |
333 let |
334 val rts = Syntax.string_of_term lthy rt |
334 val rtrm_str = Syntax.string_of_term lthy rtrm |
335 val qts = Syntax.string_of_term lthy qt |
335 val qtrm_str = Syntax.string_of_term lthy qtrm |
336 in |
336 in |
337 raise (LIFT_MATCH ("regularize failed (default: " ^ rts ^ "," ^ qts ^ ")")) |
337 raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) |
338 end |
338 end |
339 *} |
339 *} |
340 |
340 |
341 section {* Regularize Tactic *} |
341 section {* Regularize Tactic *} |
342 |
342 |
373 let |
373 let |
374 val thy = ProofContext.theory_of ctxt |
374 val thy = ProofContext.theory_of ctxt |
375 val goal = Const (@{const_name "equivp"}, dummyT) $ R2 |
375 val goal = Const (@{const_name "equivp"}, dummyT) $ R2 |
376 |> Syntax.check_term ctxt |
376 |> Syntax.check_term ctxt |
377 |> HOLogic.mk_Trueprop |
377 |> HOLogic.mk_Trueprop |
378 val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1) |
378 val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1) |
379 val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) |
379 val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) |
380 val R1c = cterm_of thy R1 |
380 val R1c = cterm_of thy R1 |
381 val thmi = Drule.instantiate' [] [SOME R1c] thm |
381 val thmi = Drule.instantiate' [] [SOME R1c] thm |
382 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex |
382 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex |
383 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) |
383 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) |
607 |
607 |
608 lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
608 lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
609 by(auto simp add: QUOT_TRUE_def) |
609 by(auto simp add: QUOT_TRUE_def) |
610 |
610 |
611 ML {* |
611 ML {* |
612 fun quot_true_conv1 ctxt fnctn ctrm = |
612 fun quot_true_simple_conv ctxt fnctn ctrm = |
613 case (term_of ctrm) of |
613 case (term_of ctrm) of |
614 (Const (@{const_name QUOT_TRUE}, _) $ x) => |
614 (Const (@{const_name QUOT_TRUE}, _) $ x) => |
615 let |
615 let |
616 val fx = fnctn x; |
616 val fx = fnctn x; |
617 val thy = ProofContext.theory_of ctxt; |
617 val thy = ProofContext.theory_of ctxt; |
627 |
627 |
628 ML {* |
628 ML {* |
629 fun quot_true_conv ctxt fnctn ctrm = |
629 fun quot_true_conv ctxt fnctn ctrm = |
630 case (term_of ctrm) of |
630 case (term_of ctrm) of |
631 (Const (@{const_name QUOT_TRUE}, _) $ _) => |
631 (Const (@{const_name QUOT_TRUE}, _) $ _) => |
632 quot_true_conv1 ctxt fnctn ctrm |
632 quot_true_simple_conv ctxt fnctn ctrm |
633 | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm |
633 | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm |
634 | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm |
634 | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm |
635 | _ => Conv.all_conv ctrm |
635 | _ => Conv.all_conv ctrm |
636 *} |
636 *} |
637 |
637 |
638 ML {* |
638 ML {* |
639 fun quot_true_tac ctxt fnctn = CONVERSION |
639 fun quot_true_tac ctxt fnctn = |
|
640 CONVERSION |
640 ((Conv.params_conv ~1 (fn ctxt => |
641 ((Conv.params_conv ~1 (fn ctxt => |
641 (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) |
642 (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) |
642 *} |
643 *} |
643 |
644 |
644 ML {* fun dest_comb (f $ a) = (f, a) *} |
645 ML {* fun dest_comb (f $ a) = (f, a) *} |
721 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
722 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
722 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
723 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
723 in |
724 in |
724 (rtac thm THEN' quotient_tac ctxt) i |
725 (rtac thm THEN' quotient_tac ctxt) i |
725 end |
726 end |
726 handle _ => no_tac) (* what is the catch for ? *) |
727 handle _ => no_tac) (* what is the catch for ? Should go away, no? *) |
727 | _ => no_tac) |
728 | _ => no_tac) |
728 *} |
729 *} |
729 |
730 |
730 ML {* |
731 ML {* |
731 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
732 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
732 (case (bare_concl goal) of |
733 (case (bare_concl goal) of |
733 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
734 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
734 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
735 (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) |
735 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
736 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
736 |
737 |
737 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
738 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
738 | (Const (@{const_name "op ="},_) $ |
739 | (Const (@{const_name "op ="},_) $ |
739 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
740 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
761 | (_ $ |
762 | (_ $ |
762 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
763 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
763 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
764 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
764 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
765 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
765 |
766 |
766 | Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => (rtac @{thm refl} ORELSE' |
767 | Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => |
|
768 (rtac @{thm refl} ORELSE' |
767 (equals_rsp_tac R ctxt THEN' RANGE [ |
769 (equals_rsp_tac R ctxt THEN' RANGE [ |
768 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) |
770 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) |
769 |
771 |
770 (* reflexivity of operators arising from Cong_tac *) |
772 (* reflexivity of operators arising from Cong_tac *) |
771 | Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl} |
773 | Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl} |
775 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
777 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
776 |
778 |
777 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
779 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
778 (* observe ---> *) |
780 (* observe ---> *) |
779 | _ $ _ $ _ |
781 | _ $ _ $ _ |
780 => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) ORELSE' rep_abs_rsp_tac ctxt |
782 => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) |
781 |
783 ORELSE' rep_abs_rsp_tac ctxt |
782 | _ => error "inj_repabs_tac not a relation" |
784 |
|
785 | _ => K no_tac |
783 ) i) |
786 ) i) |
784 *} |
787 *} |
785 |
788 |
786 ML {* |
789 ML {* |
787 fun inj_repabs_step_tac ctxt rel_refl = |
790 fun inj_repabs_step_tac ctxt rel_refl = |
821 *} |
824 *} |
822 |
825 |
823 section {* Cleaning of the Theorem *} |
826 section {* Cleaning of the Theorem *} |
824 |
827 |
825 ML {* |
828 ML {* |
826 (* expands all ---> except in front of bound variables *) |
829 (* expands all fun_maps, except in front of bound variables *) |
|
830 |
827 fun fun_map_simple_conv xs ctxt ctrm = |
831 fun fun_map_simple_conv xs ctxt ctrm = |
828 case (term_of ctrm) of |
832 case (term_of ctrm) of |
829 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
833 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
830 if (member (op=) xs h) |
834 if (member (op=) xs h) |
831 then Conv.all_conv ctrm |
835 then Conv.all_conv ctrm |