873 end |
873 end |
874 | _ => no_tac) |
874 | _ => no_tac) |
875 *} |
875 *} |
876 |
876 |
877 ML {* |
877 ML {* |
|
878 val APPLY_RSP_TAC' = |
|
879 Subgoal.FOCUS (fn {concl, asms, context,...} => |
|
880 case ((HOLogic.dest_Trueprop (term_of concl))) of |
|
881 ((R2 $ (f $ x) $ (g $ y))) => |
|
882 let |
|
883 val (asmf, asma) = find_qt_asm (map term_of asms); |
|
884 in |
|
885 if (fastype_of asmf) = (fastype_of f) then no_tac else let |
|
886 val ty_a = fastype_of x; |
|
887 val ty_b = fastype_of asma; |
|
888 val ty_c = range_type (type_of f); |
|
889 val ty_d = range_type (type_of asmf); |
|
890 val thy = ProofContext.theory_of context; |
|
891 val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c, ty_d]; |
|
892 val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y]; |
|
893 val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y]; |
|
894 val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP} |
|
895 (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*) |
|
896 in |
|
897 rtac thm 1 |
|
898 end |
|
899 end |
|
900 | _ => no_tac) |
|
901 *} |
|
902 |
|
903 |
|
904 ML {* |
878 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
905 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
879 *} |
906 *} |
880 |
907 |
881 (* |
908 (* |
882 To prove that the regularised theorem implies the abs/rep injected, |
909 To prove that the regularised theorem implies the abs/rep injected, |
1017 ML {* |
1044 ML {* |
1018 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
1045 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
1019 (FIRST' [ |
1046 (FIRST' [ |
1020 (* "cong" rule of the of the relation / transitivity*) |
1047 (* "cong" rule of the of the relation / transitivity*) |
1021 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
1048 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
1022 NDT ctxt "1" (resolve_tac trans2), |
1049 NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [ |
|
1050 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), |
1023 |
1051 |
1024 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
1052 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
1025 NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam), |
1053 NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam), |
1026 |
1054 |
1027 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
1055 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
1047 (* observe ---> *) |
1075 (* observe ---> *) |
1048 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
1076 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
1049 THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), |
1077 THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), |
1050 |
1078 |
1051 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
1079 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
1052 NDT ctxt "A" (APPLY_RSP_TAC rty ctxt THEN' |
1080 NDT ctxt "A" (APPLY_RSP_TAC' ctxt THEN' |
1053 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), |
1081 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), |
1054 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1082 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1055 |
1083 |
1056 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
1084 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
1057 (* merge with previous tactic *) |
1085 (* merge with previous tactic *) |