752 (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i |
752 (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i |
753 | _ => no_tac) |
753 | _ => no_tac) |
754 *} |
754 *} |
755 |
755 |
756 ML {* |
756 ML {* |
757 val weak_lambda_rsp_tac = |
|
758 SUBGOAL (fn (goal, i) => |
|
759 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
|
760 (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i |
|
761 | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} i |
|
762 | _ => no_tac) |
|
763 *} |
|
764 |
|
765 ML {* |
|
766 val ball_rsp_tac = |
757 val ball_rsp_tac = |
767 SUBGOAL (fn (goal, i) => |
758 SUBGOAL (fn (goal, i) => |
768 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
759 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
769 (_ $ (Const (@{const_name Ball}, _) $ _) |
760 (_ $ (Const (@{const_name Ball}, _) $ _) |
770 $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i |
761 $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i |
916 | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm |
907 | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm |
917 | _ => Conv.all_conv ctrm |
908 | _ => Conv.all_conv ctrm |
918 *} |
909 *} |
919 |
910 |
920 ML {* |
911 ML {* |
921 fun quot_true_tac ctxt fnctn = CSUBGOAL (fn (goal, i) => |
912 fun quot_true_tac ctxt fnctn = CONVERSION |
922 CONVERSION |
913 ((Conv.params_conv ~1 (fn ctxt => |
923 (Conv.params_conv ~1 (fn ctxt => |
914 (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) |
924 (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn))) ctxt) i) |
|
925 *} |
915 *} |
926 |
916 |
927 ML {* fun dest_comb (f $ a) = (f, a) *} |
917 ML {* fun dest_comb (f $ a) = (f, a) *} |
928 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} |
918 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} |
929 (* TODO: Can this be done easier? *) |
919 (* TODO: Can this be done easier? *) |
931 fun unlam t = |
921 fun unlam t = |
932 case t of |
922 case t of |
933 (Abs a) => snd (Term.dest_abs a) |
923 (Abs a) => snd (Term.dest_abs a) |
934 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) *} |
924 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) *} |
935 |
925 |
936 ML {* |
|
937 fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 = |
|
938 (FIRST' [ |
|
939 (* "cong" rule of the of the relation / transitivity*) |
|
940 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
|
941 NDT ctxt "1" (resolve_tac trans2), |
|
942 |
|
943 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
|
944 NDT ctxt "2" (lambda_rsp_tac), |
|
945 |
|
946 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
947 NDT ctxt "3" (rtac @{thm ball_rsp}), |
|
948 |
|
949 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
|
950 NDT ctxt "4" (ball_rsp_tac), |
|
951 |
|
952 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
953 NDT ctxt "5" (rtac @{thm bex_rsp}), |
|
954 |
|
955 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
|
956 NDT ctxt "6" (bex_rsp_tac), |
|
957 |
|
958 (* respectfulness of constants *) |
|
959 NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)), |
|
960 |
|
961 (* reflexivity of operators arising from Cong_tac *) |
|
962 NDT ctxt "8" (rtac @{thm refl}), |
|
963 |
|
964 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
|
965 (* observe ---> *) |
|
966 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
|
967 THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), |
|
968 |
|
969 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
|
970 NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
|
971 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms)]))), |
|
972 |
|
973 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
|
974 (* merge with previous tactic *) |
|
975 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
|
976 |
|
977 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
978 NDT ctxt "C" (rtac @{thm ext}), |
|
979 |
|
980 (* reflexivity of the basic relations *) |
|
981 (* R \<dots> \<dots> *) |
|
982 NDT ctxt "D" (resolve_tac rel_refl), |
|
983 |
|
984 (* resolving with R x y assumptions *) |
|
985 NDT ctxt "E" (atac), |
|
986 |
|
987 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
|
988 (* global simplification *) |
|
989 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
|
990 *} |
|
991 |
926 |
992 ML {* |
927 ML {* |
993 fun inj_repabs_tac ctxt quot_thms rel_refl trans2 = |
928 fun inj_repabs_tac ctxt quot_thms rel_refl trans2 = |
994 (FIRST' [ |
929 (FIRST' [ |
995 (* "cong" rule of the of the relation / transitivity*) |
930 (* "cong" rule of the of the relation / transitivity*) |