838 Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys) |
838 Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys) |
839 | _ => false |
839 | _ => false |
840 |
840 |
841 *} |
841 *} |
842 |
842 |
843 |
843 definition |
844 |
844 "QUOT_TRUE x \<equiv> True" |
845 |
845 |
846 ML {* |
846 ML {* |
847 fun APPLY_RSP_TAC rty = |
847 fun find_qt_asm asms = |
848 Subgoal.FOCUS (fn {concl, ...} => |
848 let |
849 case HOLogic.dest_Trueprop (term_of concl) of |
849 fun find_fun trm = |
850 (_ $ (f $ _) $ (_ $ _)) => |
850 case trm of |
|
851 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
|
852 | _ => false |
|
853 in |
|
854 case find_first find_fun asms of |
|
855 SOME (_ $ (_ $ (f $ a))) => (f, a) |
|
856 | _ => error "find_qt_asm" |
|
857 end |
|
858 *} |
|
859 |
|
860 ML {* |
|
861 fun APPLY_RSP_TAC rty = |
|
862 Subgoal.FOCUS (fn {concl, asms, ...} => |
|
863 case ((HOLogic.dest_Trueprop (term_of concl))) of |
|
864 ((_ $ (f $ _) $ (_ $ _))) => |
851 let |
865 let |
|
866 val (asmf, asma) = find_qt_asm (map term_of asms); |
852 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
867 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
853 val insts = Thm.match (pat, concl) |
868 val insts = Thm.match (pat, concl) |
854 in |
869 in |
855 if needs_lift rty (fastype_of f) |
870 if (fastype_of asmf) = (fastype_of f) |
856 then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
871 then no_tac |
857 else no_tac |
872 else rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
858 end |
873 end |
859 | _ => no_tac) |
874 | _ => no_tac) |
860 *} |
875 *} |
861 |
876 |
862 ML {* |
877 ML {* |
884 D) unfolding lambda on one side |
899 D) unfolding lambda on one side |
885 E) simplifying (= ===> =) for simpler respectfulness |
900 E) simplifying (= ===> =) for simpler respectfulness |
886 |
901 |
887 *) |
902 *) |
888 |
903 |
889 definition |
|
890 "QUOT_TRUE x \<equiv> True" |
|
891 |
|
892 lemma quot_true_dests: |
904 lemma quot_true_dests: |
893 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
905 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
894 and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
906 and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
895 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
907 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
896 and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
908 and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
940 ML {* fun dest_comb (f $ a) = (f, a) *} |
952 ML {* fun dest_comb (f $ a) = (f, a) *} |
941 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} |
953 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} |
942 ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *} |
954 ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *} |
943 |
955 |
944 ML {* |
956 ML {* |
945 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
957 fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 = |
946 (FIRST' [ |
958 (FIRST' [ |
947 (* "cong" rule of the of the relation / transitivity*) |
959 (* "cong" rule of the of the relation / transitivity*) |
948 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
960 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
949 DT ctxt "1" (resolve_tac trans2), |
961 DT ctxt "1" (resolve_tac trans2), |
950 |
962 |
996 (* global simplification *) |
1008 (* global simplification *) |
997 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
1009 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
998 *} |
1010 *} |
999 |
1011 |
1000 ML {* |
1012 ML {* |
1001 fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 = |
1013 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
1002 (FIRST' [ |
1014 (FIRST' [ |
1003 (* "cong" rule of the of the relation / transitivity*) |
1015 (* "cong" rule of the of the relation / transitivity*) |
1004 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
1016 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
1005 DT ctxt "1" (resolve_tac trans2), |
1017 NDT ctxt "1" (resolve_tac trans2), |
1006 |
1018 |
1007 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
1019 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
1008 NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam), |
1020 NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam), |
1009 |
1021 |
1010 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
1022 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |