291 (* cu: Changed the lookup\<dots>not sure whether this works *) |
291 (* cu: Changed the lookup\<dots>not sure whether this works *) |
292 (* TODO: Should no longer be needed *) |
292 (* TODO: Should no longer be needed *) |
293 val rty = Logic.unvarifyT (#rtyp quotdata) |
293 val rty = Logic.unvarifyT (#rtyp quotdata) |
294 val rel = #rel quotdata |
294 val rel = #rel quotdata |
295 val rel_eqv = #equiv_thm quotdata |
295 val rel_eqv = #equiv_thm quotdata |
296 val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv] |
296 val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] |
297 val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre] |
|
298 in |
297 in |
299 (rty, rel, rel_refl, rel_eqv) |
298 (rty, rel, rel_refl, rel_eqv) |
300 end |
299 end |
301 *} |
300 *} |
302 |
301 |
492 ML {* |
491 ML {* |
493 fun regularize_tac ctxt rel_eqv rel_refl = |
492 fun regularize_tac ctxt rel_eqv rel_refl = |
494 (ObjectLogic.full_atomize_tac) THEN' |
493 (ObjectLogic.full_atomize_tac) THEN' |
495 REPEAT_ALL_NEW (FIRST' |
494 REPEAT_ALL_NEW (FIRST' |
496 [(K (print_tac "start")) THEN' (K no_tac), |
495 [(K (print_tac "start")) THEN' (K no_tac), |
497 DT ctxt "1" (rtac rel_refl), |
496 DT ctxt "1" (FIRST' (map rtac rel_refl)), |
498 DT ctxt "2" atac, |
497 DT ctxt "2" atac, |
499 DT ctxt "3" (rtac @{thm universal_twice}), |
498 DT ctxt "3" (rtac @{thm universal_twice}), |
500 DT ctxt "4" (rtac @{thm impI} THEN' atac), |
499 DT ctxt "4" (rtac @{thm impI} THEN' atac), |
501 DT ctxt "5" (rtac @{thm implication_twice}), |
500 DT ctxt "5" (rtac @{thm implication_twice}), |
502 DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0] |
501 DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0] |
503 [(@{thm equiv_res_forall} OF [rel_eqv]), |
502 [(@{thm equiv_res_forall} OF [rel_eqv]), |
504 (@{thm equiv_res_exists} OF [rel_eqv])]), |
503 (@{thm equiv_res_exists} OF [rel_eqv])]), |
505 (* For a = b \<longrightarrow> a \<approx> b *) |
504 (* For a = b \<longrightarrow> a \<approx> b *) |
506 DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
505 DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (FIRST' (map rtac rel_refl))), |
507 DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
506 DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
508 ]); |
507 ]); |
509 *} |
508 *} |
510 |
509 |
511 lemma move_forall: |
510 lemma move_forall: |
588 (resolve_tac (Inductive.get_monos ctxt)), |
587 (resolve_tac (Inductive.get_monos ctxt)), |
589 (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
588 (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
590 (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
589 (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
591 rtac @{thm move_forall}, |
590 rtac @{thm move_forall}, |
592 rtac @{thm move_exists}, |
591 rtac @{thm move_exists}, |
593 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl) |
592 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' FIRST' (map rtac rel_refl)) |
594 ]) |
593 ]) |
595 end |
594 end |
596 *} |
595 *} |
597 |
596 |
598 section {* Injections of REP and ABSes *} |
597 section {* Injections of REP and ABSes *} |
718 handle _ => no_tac) |
717 handle _ => no_tac) |
719 *} |
718 *} |
720 |
719 |
721 |
720 |
722 ML {* |
721 ML {* |
723 fun quotient_tac quot_thm = |
722 fun quotient_tac quot_thms = |
724 REPEAT_ALL_NEW (FIRST' [ |
723 REPEAT_ALL_NEW (FIRST' [ |
725 rtac @{thm FUN_QUOTIENT}, |
724 rtac @{thm FUN_QUOTIENT}, |
726 rtac quot_thm, |
725 FIRST' (map rtac quot_thms), |
727 rtac @{thm IDENTITY_QUOTIENT}, |
726 rtac @{thm IDENTITY_QUOTIENT}, |
728 (* For functional identity quotients, (op = ---> op =) *) |
727 (* For functional identity quotients, (op = ---> op =) *) |
|
728 (* TODO: think about the other way around, if we need to shorten the relation *) |
729 CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps})) |
729 CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps})) |
730 ]) |
730 ]) |
731 *} |
731 *} |
732 |
732 |
733 ML {* |
733 ML {* |
801 end |
801 end |
802 handle _ => no_tac) |
802 handle _ => no_tac) |
803 *} |
803 *} |
804 |
804 |
805 ML {* |
805 ML {* |
806 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
806 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans_thm rsp_thms = |
807 (FIRST' [ |
807 (FIRST' [ |
808 rtac trans_thm, |
808 rtac trans_thm, |
809 LAMBDA_RES_TAC ctxt, |
809 LAMBDA_RES_TAC ctxt, |
810 rtac @{thm RES_FORALL_RSP}, |
810 rtac @{thm RES_FORALL_RSP}, |
811 ball_rsp_tac ctxt, |
811 ball_rsp_tac ctxt, |
812 rtac @{thm RES_EXISTS_RSP}, |
812 rtac @{thm RES_EXISTS_RSP}, |
813 bex_rsp_tac ctxt, |
813 bex_rsp_tac ctxt, |
814 FIRST' (map rtac rsp_thms), |
814 FIRST' (map rtac rsp_thms), |
815 rtac refl, |
815 rtac refl, |
816 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' |
816 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' |
817 (RANGE [SOLVES' (quotient_tac quot_thm)])), |
817 (RANGE [SOLVES' (quotient_tac quot_thms)])), |
818 (APPLY_RSP_TAC rty ctxt THEN' |
818 (APPLY_RSP_TAC rty ctxt THEN' |
819 (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])), |
819 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
820 Cong_Tac.cong_tac @{thm cong}, |
820 Cong_Tac.cong_tac @{thm cong}, |
821 rtac @{thm ext}, |
821 rtac @{thm ext}, |
822 rtac reflex_thm, |
822 FIRST' (map rtac rel_refl), |
823 atac, |
823 atac, |
824 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
824 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
825 WEAK_LAMBDA_RES_TAC ctxt, |
825 WEAK_LAMBDA_RES_TAC ctxt, |
826 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})) |
826 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})) |
827 ]) |
827 ]) |
849 14) simplifying (= ===> =) for simpler respectfulness |
849 14) simplifying (= ===> =) for simpler respectfulness |
850 |
850 |
851 *) |
851 *) |
852 |
852 |
853 ML {* |
853 ML {* |
854 fun r_mk_comb_tac' ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
854 fun r_mk_comb_tac' ctxt rty quot_thms reflex_thm trans_thm rsp_thms = |
855 REPEAT_ALL_NEW (FIRST' [ |
855 REPEAT_ALL_NEW (FIRST' [ |
856 (K (print_tac "start")) THEN' (K no_tac), |
856 (K (print_tac "start")) THEN' (K no_tac), |
857 DT ctxt "1" (rtac trans_thm), |
857 DT ctxt "1" (rtac trans_thm), |
858 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
858 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
859 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
859 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
861 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
861 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
862 DT ctxt "6" (bex_rsp_tac ctxt), |
862 DT ctxt "6" (bex_rsp_tac ctxt), |
863 DT ctxt "7" (FIRST' (map rtac rsp_thms)), |
863 DT ctxt "7" (FIRST' (map rtac rsp_thms)), |
864 DT ctxt "8" (rtac refl), |
864 DT ctxt "8" (rtac refl), |
865 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
865 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
866 THEN' (RANGE [SOLVES' (quotient_tac quot_thm)]))), |
866 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
867 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
867 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
868 (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)]))), |
868 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
869 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
869 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
870 DT ctxt "C" (rtac @{thm ext}), |
870 DT ctxt "C" (rtac @{thm ext}), |
871 DT ctxt "D" (rtac reflex_thm), |
871 DT ctxt "D" (rtac reflex_thm), |
872 DT ctxt "E" (atac), |
872 DT ctxt "E" (atac), |
873 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
873 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
896 val largs = map2 mk_rep (raty ~~ qaty) args; |
896 val largs = map2 mk_rep (raty ~~ qaty) args; |
897 val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs)); |
897 val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs)); |
898 val llhs = Syntax.check_term lthy lhs; |
898 val llhs = Syntax.check_term lthy lhs; |
899 val eq = Logic.mk_equals (llhs, rhs); |
899 val eq = Logic.mk_equals (llhs, rhs); |
900 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
900 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
901 val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps id_simps}); |
901 val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep); |
902 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
902 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
903 val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t; |
903 val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t; |
904 in |
904 in |
905 singleton (ProofContext.export lthy' lthy) t_id |
905 singleton (ProofContext.export lthy' lthy) t_id |
906 end |
906 end |
948 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
948 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
949 end |
949 end |
950 *} |
950 *} |
951 |
951 |
952 ML {* |
952 ML {* |
953 fun lambda_prs_conv1 ctxt quot ctrm = |
953 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
954 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
954 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
955 let |
955 let |
956 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
956 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
957 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); |
957 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); |
958 val thy = ProofContext.theory_of ctxt; |
958 val thy = ProofContext.theory_of ctxt; |
960 val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; |
960 val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; |
961 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
961 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
962 val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; |
962 val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; |
963 val tac = |
963 val tac = |
964 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
964 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
965 (quotient_tac quot); |
965 (quotient_tac quot_thms); |
966 val gc = Drule.strip_imp_concl (cprop_of lpi); |
966 val gc = Drule.strip_imp_concl (cprop_of lpi); |
967 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
967 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
968 val te = @{thm eq_reflection} OF [t] |
968 val te = @{thm eq_reflection} OF [t] |
969 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
969 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
970 val tl = Thm.lhs_of ts |
970 val tl = Thm.lhs_of ts |
1001 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1001 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1002 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1002 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1003 *} |
1003 *} |
1004 |
1004 |
1005 ML {* |
1005 ML {* |
1006 fun clean_tac lthy quot defs reps_same absrep aps = |
1006 fun clean_tac lthy quot defs aps = |
1007 let |
1007 let |
1008 val lower = flat (map (add_lower_defs lthy) defs) |
1008 val lower = flat (map (add_lower_defs lthy) defs) |
|
1009 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
|
1010 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1009 val aps_thms = map (applic_prs lthy absrep) aps |
1011 val aps_thms = map (applic_prs lthy absrep) aps |
1010 in |
1012 in |
1011 EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1013 EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1012 lambda_prs_tac lthy quot, |
1014 lambda_prs_tac lthy quot, |
1013 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), |
1015 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), |
1014 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower), |
1016 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower), |
1015 simp_tac (HOL_ss addsimps [reps_same])] |
1017 simp_tac (HOL_ss addsimps reps_same)] |
1016 end |
1018 end |
1017 *} |
1019 *} |
1018 |
1020 |
1019 section {* Genralisation of free variables in a goal *} |
1021 section {* Genralisation of free variables in a goal *} |
1020 |
1022 |
1112 end) lthy |
1114 end) lthy |
1113 *} |
1115 *} |
1114 |
1116 |
1115 ML {* |
1117 ML {* |
1116 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1118 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1117 fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs = |
1119 fun lift_tac lthy rthm rel_eqv rty quot trans2 rsp_thms defs = |
1118 ObjectLogic.full_atomize_tac |
1120 ObjectLogic.full_atomize_tac |
1119 THEN' gen_frees_tac lthy |
1121 THEN' gen_frees_tac lthy |
1120 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1122 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1121 let |
1123 let |
1122 val rthm' = atomize_thm rthm |
1124 val rthm' = atomize_thm rthm |
1123 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1125 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1124 val aps = find_aps (prop_of rthm') (term_of concl) |
1126 val aps = find_aps (prop_of rthm') (term_of concl) |
|
1127 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv |
1125 in |
1128 in |
1126 EVERY1 |
1129 EVERY1 |
1127 [rtac rule, |
1130 [rtac rule, |
1128 RANGE [rtac rthm', |
1131 RANGE [rtac rthm', |
1129 regularize_tac lthy [rel_eqv] rel_refl, |
1132 regularize_tac lthy rel_eqv rel_refl, |
1130 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1133 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1131 clean_tac lthy quot defs reps_same absrep aps]] |
1134 clean_tac lthy quot defs aps]] |
1132 end) lthy |
1135 end) lthy |
1133 *} |
1136 *} |
1134 |
1137 |
1135 end |
1138 end |
1136 |
1139 |