538 val ctxt = Simplifier.the_context ss |
538 val ctxt = Simplifier.the_context ss |
539 val thy = ProofContext.theory_of ctxt |
539 val thy = ProofContext.theory_of ctxt |
540 in |
540 in |
541 case redex of |
541 case redex of |
542 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
542 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
543 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => |
543 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) => |
544 (let |
544 (let |
545 val gl = Const (@{const_name "equivp"}, dummyT) $ R2; |
545 val gl = Const (@{const_name "equivp"}, dummyT) $ R2; |
546 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
546 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
547 (* val _ = tracing (Syntax.string_of_term ctxt glc);*) |
547 (* val _ = tracing (Syntax.string_of_term ctxt glc);*) |
548 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
548 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
569 val ctxt = Simplifier.the_context ss |
569 val ctxt = Simplifier.the_context ss |
570 val thy = ProofContext.theory_of ctxt |
570 val thy = ProofContext.theory_of ctxt |
571 in |
571 in |
572 case redex of |
572 case redex of |
573 (ogl as ((Const (@{const_name "Bex"}, _)) $ |
573 (ogl as ((Const (@{const_name "Bex"}, _)) $ |
574 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => |
574 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) => |
575 (let |
575 (let |
576 val gl = Const (@{const_name "equivp"}, dummyT) $ R2; |
576 val gl = Const (@{const_name "equivp"}, dummyT) $ R2; |
577 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
577 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
578 (* val _ = tracing (Syntax.string_of_term ctxt glc); *) |
578 (* val _ = tracing (Syntax.string_of_term ctxt glc); *) |
579 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
579 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
726 REPEAT_ALL_NEW (FIRST' |
726 REPEAT_ALL_NEW (FIRST' |
727 [rtac @{thm IDENTITY_Quotient}, |
727 [rtac @{thm IDENTITY_Quotient}, |
728 resolve_tac (quotient_rules_get ctxt)]) |
728 resolve_tac (quotient_rules_get ctxt)]) |
729 *} |
729 *} |
730 |
730 |
731 lemma FUN_REL_I: |
731 lemma fun_rel_id: |
732 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
732 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
733 shows "(R1 ===> R2) f g" |
733 shows "(R1 ===> R2) f g" |
734 using a by simp |
734 using a by simp |
735 |
|
736 ML {* |
|
737 val lambda_rsp_tac = |
|
738 SUBGOAL (fn (goal, i) => |
|
739 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
|
740 (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i |
|
741 | _ => no_tac) |
|
742 *} |
|
743 |
|
744 ML {* |
|
745 val ball_rsp_tac = |
|
746 SUBGOAL (fn (goal, i) => |
|
747 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
|
748 (_ $ (Const (@{const_name Ball}, _) $ _) |
|
749 $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i |
|
750 |_ => no_tac) |
|
751 *} |
|
752 |
|
753 ML {* |
|
754 val bex_rsp_tac = |
|
755 SUBGOAL (fn (goal, i) => |
|
756 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
|
757 (_ $ (Const (@{const_name Bex}, _) $ _) |
|
758 $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i |
|
759 | _ => no_tac) |
|
760 *} |
|
761 |
735 |
762 definition |
736 definition |
763 "QUOT_TRUE x \<equiv> True" |
737 "QUOT_TRUE x \<equiv> True" |
764 |
738 |
765 ML {* |
739 ML {* |
934 |
908 |
935 ML {* |
909 ML {* |
936 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
910 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
937 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
911 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
938 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
912 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
939 ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
913 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
940 => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam |
914 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
941 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
915 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
942 | (Const (@{const_name "op ="},_) $ |
916 | (Const (@{const_name "op ="},_) $ |
943 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
917 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
944 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
918 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
945 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
919 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
946 (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *) |
920 (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *) |
947 | (Const (@{const_name FUN_REL}, _) $ _ $ _) $ |
921 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
948 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
922 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
949 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
923 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
950 => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam |
924 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
951 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
925 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
952 | Const (@{const_name "op ="},_) $ |
926 | Const (@{const_name "op ="},_) $ |
953 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
927 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
954 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
928 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
955 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
929 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
956 (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *) |
930 (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *) |
957 | (Const (@{const_name FUN_REL}, _) $ _ $ _) $ |
931 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
958 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
932 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
959 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
933 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
960 => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam |
934 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
961 | Const (@{const_name "op ="},_) $ _ $ _ => |
935 | Const (@{const_name "op ="},_) $ _ $ _ => |
962 (* reflexivity of operators arising from Cong_tac *) |
936 (* reflexivity of operators arising from Cong_tac *) |
963 rtac @{thm refl} ORELSE' |
937 rtac @{thm refl} ORELSE' |
964 (resolve_tac trans2 THEN' RANGE [ |
938 (resolve_tac trans2 THEN' RANGE [ |
965 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
939 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |