837 end |
837 end |
838 end |
838 end |
839 | _ => no_tac) |
839 | _ => no_tac) |
840 *} |
840 *} |
841 |
841 |
|
842 (* It proves the QUOTIENT assumptions by calling quotient_tac *) |
|
843 ML {* |
|
844 fun solve_quotient_assum i ctxt thm = |
|
845 let |
|
846 val tac = |
|
847 (compose_tac (false, thm, i)) THEN_ALL_NEW |
|
848 (quotient_tac ctxt); |
|
849 val gc = Drule.strip_imp_concl (cprop_of thm); |
|
850 in |
|
851 Goal.prove_internal [] gc (fn _ => tac 1) |
|
852 end |
|
853 handle _ => error "solve_quotient_assum" |
|
854 *} |
|
855 |
|
856 ML {* |
|
857 fun solve_quotient_assums ctxt thm = |
|
858 let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in |
|
859 thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)] |
|
860 end |
|
861 handle _ => error "solve_quotient_assums" |
|
862 *} |
|
863 |
|
864 ML {* |
|
865 val APPLY_RSP1_TAC' = |
|
866 Subgoal.FOCUS (fn {concl, asms, context,...} => |
|
867 case ((HOLogic.dest_Trueprop (term_of concl))) of |
|
868 ((R2 $ (f $ x) $ (g $ y))) => |
|
869 let |
|
870 val (asmf, asma) = find_qt_asm (map term_of asms); |
|
871 in |
|
872 if (fastype_of asmf) = (fastype_of f) then no_tac else let |
|
873 val ty_a = fastype_of x; |
|
874 val ty_b = fastype_of asma; |
|
875 val ty_c = range_type (type_of f); |
|
876 val thy = ProofContext.theory_of context; |
|
877 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; |
|
878 val thm = Drule.instantiate' ty_inst [] @{thm APPLY_RSP1} |
|
879 val te = solve_quotient_assums context thm |
|
880 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
|
881 val thm = Drule.instantiate' [] t_inst te |
|
882 in |
|
883 (* TODO try sth like: compose_tac (false, thm, 1) 1 *) |
|
884 rtac thm 1 |
|
885 end |
|
886 end |
|
887 | _ => no_tac) |
|
888 *} |
842 |
889 |
843 ML {* |
890 ML {* |
844 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
891 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
845 *} |
892 *} |
846 |
893 |
1024 |
1071 |
1025 ML {* |
1072 ML {* |
1026 fun inj_repabs_tac' ctxt rel_refl trans2 = |
1073 fun inj_repabs_tac' ctxt rel_refl trans2 = |
1027 (FIRST' [ |
1074 (FIRST' [ |
1028 inj_repabs_tac_fast ctxt trans2, |
1075 inj_repabs_tac_fast ctxt trans2, |
1029 NDT ctxt "A" (APPLY_RSP1_TAC ctxt THEN' |
1076 NDT ctxt "A" (APPLY_RSP1_TAC' ctxt THEN' |
1030 (RANGE [SOLVES' (quotient_tac ctxt), |
1077 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1031 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
|
1032 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
1078 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
1033 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1079 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1034 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
1080 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
1035 NDT ctxt "E" (atac), |
1081 NDT ctxt "E" (atac), |
1036 NDT ctxt "D" (resolve_tac rel_refl), |
1082 NDT ctxt "D" (resolve_tac rel_refl), |
1068 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
1114 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
1069 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
1115 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
1070 | Bound j => if i = j then error "make_inst" else t |
1116 | Bound j => if i = j then error "make_inst" else t |
1071 | _ => t); |
1117 | _ => t); |
1072 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1118 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1073 *} |
|
1074 |
|
1075 (* It proves the QUOTIENT assumptions by calling quotient_tac *) |
|
1076 ML {* |
|
1077 fun solve_quotient_assum i ctxt thm = |
|
1078 let |
|
1079 val tac = |
|
1080 (compose_tac (false, thm, i)) THEN_ALL_NEW |
|
1081 (quotient_tac ctxt); |
|
1082 val gc = Drule.strip_imp_concl (cprop_of thm); |
|
1083 in |
|
1084 Goal.prove_internal [] gc (fn _ => tac 1) |
|
1085 end |
|
1086 handle _ => error "solve_quotient_assum" |
|
1087 *} |
1119 *} |
1088 |
1120 |
1089 ML {* |
1121 ML {* |
1090 fun lambda_allex_prs_simple_conv ctxt ctrm = |
1122 fun lambda_allex_prs_simple_conv ctxt ctrm = |
1091 case (term_of ctrm) of |
1123 case (term_of ctrm) of |