774 SOME (_ $ (_ $ (f $ a))) => (f, a) |
774 SOME (_ $ (_ $ (f $ a))) => (f, a) |
775 | _ => error "find_qt_asm" |
775 | _ => error "find_qt_asm" |
776 end |
776 end |
777 *} |
777 *} |
778 |
778 |
779 ML {* |
|
780 val APPLY_RSP_TAC = |
|
781 Subgoal.FOCUS (fn {concl, asms, context,...} => |
|
782 case ((HOLogic.dest_Trueprop (term_of concl))) of |
|
783 ((R2 $ (f $ x) $ (g $ y))) => |
|
784 let |
|
785 val (asmf, asma) = find_qt_asm (map term_of asms); |
|
786 in |
|
787 if (fastype_of asmf) = (fastype_of f) then no_tac else let |
|
788 val ty_a = fastype_of x; |
|
789 val ty_b = fastype_of asma; |
|
790 val ty_c = range_type (type_of f); |
|
791 val ty_d = range_type (type_of asmf); |
|
792 val thy = ProofContext.theory_of context; |
|
793 val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c, ty_d]; |
|
794 val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y]; |
|
795 val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y]; |
|
796 val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP} |
|
797 val _ = tracing ("instantiated rule" ^ Syntax.string_of_term @{context} (prop_of thm)) |
|
798 in |
|
799 rtac thm 1 |
|
800 end |
|
801 end |
|
802 | _ => no_tac) |
|
803 *} |
|
804 |
|
805 ML {* |
|
806 val APPLY_RSP1_TAC = |
|
807 Subgoal.FOCUS (fn {concl, asms, context,...} => |
|
808 case ((HOLogic.dest_Trueprop (term_of concl))) of |
|
809 ((R2 $ (f $ x) $ (g $ y))) => |
|
810 let |
|
811 val (asmf, asma) = find_qt_asm (map term_of asms); |
|
812 in |
|
813 if (fastype_of asmf) = (fastype_of f) then no_tac else let |
|
814 val ty_a = fastype_of x; |
|
815 val ty_b = fastype_of asma; |
|
816 val ty_c = range_type (type_of f); |
|
817 (* val ty_d = range_type (type_of asmf);*) |
|
818 val thy = ProofContext.theory_of context; |
|
819 val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c]; |
|
820 val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y]; |
|
821 val t_inst = [NONE, NONE, NONE, SOME R2, SOME f, SOME g, SOME x, SOME y]; |
|
822 val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP1} |
|
823 (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*) |
|
824 in |
|
825 rtac thm 1 |
|
826 end |
|
827 end |
|
828 | _ => no_tac) |
|
829 *} |
|
830 |
|
831 (* It proves the QUOTIENT assumptions by calling quotient_tac *) |
779 (* It proves the QUOTIENT assumptions by calling quotient_tac *) |
832 ML {* |
780 ML {* |
833 fun solve_quotient_assum i ctxt thm = |
781 fun solve_quotient_assum i ctxt thm = |
834 let |
782 let |
835 val tac = |
783 val tac = |
849 end |
797 end |
850 handle _ => error "solve_quotient_assums" |
798 handle _ => error "solve_quotient_assums" |
851 *} |
799 *} |
852 |
800 |
853 ML {* |
801 ML {* |
854 val APPLY_RSP1_TAC' = |
802 val apply_rsp_tac = |
855 Subgoal.FOCUS (fn {concl, asms, context,...} => |
803 Subgoal.FOCUS (fn {concl, asms, context,...} => |
856 case ((HOLogic.dest_Trueprop (term_of concl))) of |
804 case ((HOLogic.dest_Trueprop (term_of concl))) of |
857 ((R2 $ (f $ x) $ (g $ y))) => |
805 ((R2 $ (f $ x) $ (g $ y))) => |
858 let |
806 let |
859 val (asmf, asma) = find_qt_asm (map term_of asms); |
807 val (asmf, asma) = find_qt_asm (map term_of asms); |
862 val ty_a = fastype_of x; |
810 val ty_a = fastype_of x; |
863 val ty_b = fastype_of asma; |
811 val ty_b = fastype_of asma; |
864 val ty_c = range_type (type_of f); |
812 val ty_c = range_type (type_of f); |
865 val thy = ProofContext.theory_of context; |
813 val thy = ProofContext.theory_of context; |
866 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; |
814 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; |
867 val thm = Drule.instantiate' ty_inst [] @{thm APPLY_RSP1} |
815 val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp} |
868 val te = solve_quotient_assums context thm |
816 val te = solve_quotient_assums context thm |
869 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
817 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
870 val thm = Drule.instantiate' [] t_inst te |
818 val thm = Drule.instantiate' [] t_inst te |
871 in |
819 in |
872 compose_tac (false, thm, 2) 1 |
820 compose_tac (false, thm, 2) 1 |
1025 |
973 |
1026 ML {* |
974 ML {* |
1027 fun inj_repabs_tac ctxt rel_refl trans2 = |
975 fun inj_repabs_tac ctxt rel_refl trans2 = |
1028 (FIRST' [ |
976 (FIRST' [ |
1029 inj_repabs_tac_match ctxt trans2, |
977 inj_repabs_tac_match ctxt trans2, |
1030 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
978 (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *) |
1031 NDT ctxt "A" (APPLY_RSP1_TAC' ctxt THEN' |
979 NDT ctxt "A" (apply_rsp_tac ctxt THEN' |
1032 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
980 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1033 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
981 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
1034 (* merge with previous tactic *) |
982 (* merge with previous tactic *) |
1035 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
983 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
1036 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
984 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1053 |
1001 |
1054 |
1002 |
1055 |
1003 |
1056 section {* Cleaning of the theorem *} |
1004 section {* Cleaning of the theorem *} |
1057 |
1005 |
1058 |
|
1059 (* TODO: This is slow *) |
|
1060 (* |
|
1061 ML {* |
|
1062 fun allex_prs_tac ctxt = |
|
1063 (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt) |
|
1064 *} |
|
1065 *) |
|
1066 |
|
1067 ML {* |
1006 ML {* |
1068 fun make_inst lhs t = |
1007 fun make_inst lhs t = |
1069 let |
1008 let |
1070 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
1009 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
1071 val _ $ (Abs (_, _, g)) = t; |
1010 val _ $ (Abs (_, _, g)) = t; |
1087 val (ty_b, ty_a) = dest_fun_type (fastype_of r1); |
1026 val (ty_b, ty_a) = dest_fun_type (fastype_of r1); |
1088 val (ty_c, ty_d) = dest_fun_type (fastype_of a2); |
1027 val (ty_c, ty_d) = dest_fun_type (fastype_of a2); |
1089 val thy = ProofContext.theory_of ctxt; |
1028 val thy = ProofContext.theory_of ctxt; |
1090 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1029 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1091 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1030 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1092 val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; |
1031 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}; |
1093 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1032 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1094 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1033 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1095 val tl = Thm.lhs_of ts; |
1034 val tl = Thm.lhs_of ts; |
1096 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
1035 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
1097 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1036 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1138 |
1077 |
1139 (* |
1078 (* |
1140 Cleaning the theorem consists of 6 kinds of rewrites. |
1079 Cleaning the theorem consists of 6 kinds of rewrites. |
1141 The first two need to be done before fun_map is unfolded |
1080 The first two need to be done before fun_map is unfolded |
1142 |
1081 |
1143 - LAMBDA_PRS: |
1082 - lambda_prs: |
1144 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f |
1083 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f |
1145 |
1084 |
1146 - FORALL_PRS (and the same for exists: EXISTS_PRS) |
1085 - all_prs (and the same for exists: ex_prs) |
1147 \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f |
1086 \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f |
1148 |
1087 |
1149 - Rewriting with definitions from the argument defs |
1088 - Rewriting with definitions from the argument defs |
1150 NewConst ----> (rep ---> abs) oldConst |
1089 NewConst ----> (rep ---> abs) oldConst |
1151 |
1090 |
1298 let |
1237 let |
1299 val rthm' = atomize_thm rthm |
1238 val rthm' = atomize_thm rthm |
1300 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1239 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1301 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv |
1240 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv |
1302 val quotients = quotient_rules_get lthy |
1241 val quotients = quotient_rules_get lthy |
1303 val trans2 = map (fn x => @{thm EQUALS_RSP} OF [x]) quotients |
1242 val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients |
1304 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} |
1243 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} |
1305 in |
1244 in |
1306 EVERY1 |
1245 EVERY1 |
1307 [rtac rule, |
1246 [rtac rule, |
1308 RANGE [rtac rthm', |
1247 RANGE [rtac rthm', |