152 use "quotient_info.ML" |
152 use "quotient_info.ML" |
153 |
153 |
154 declare [[map list = (map, LIST_REL)]] |
154 declare [[map list = (map, LIST_REL)]] |
155 declare [[map * = (prod_fun, prod_rel)]] |
155 declare [[map * = (prod_fun, prod_rel)]] |
156 declare [[map "fun" = (fun_map, FUN_REL)]] |
156 declare [[map "fun" = (fun_map, FUN_REL)]] |
|
157 |
|
158 lemmas [quotient_thm] = |
|
159 FUN_QUOTIENT IDENTITY_QUOTIENT LIST_QUOTIENT |
157 |
160 |
158 ML {* maps_lookup @{theory} "List.list" *} |
161 ML {* maps_lookup @{theory} "List.list" *} |
159 ML {* maps_lookup @{theory} "*" *} |
162 ML {* maps_lookup @{theory} "*" *} |
160 ML {* maps_lookup @{theory} "fun" *} |
163 ML {* maps_lookup @{theory} "fun" *} |
161 |
164 |
728 end |
731 end |
729 handle _ => no_tac) |
732 handle _ => no_tac) |
730 *} |
733 *} |
731 |
734 |
732 ML {* |
735 ML {* |
733 fun quotient_tac ctxt quot_thms = |
736 fun quotient_tac ctxt = |
734 REPEAT_ALL_NEW (FIRST' |
737 REPEAT_ALL_NEW (FIRST' |
735 [rtac @{thm FUN_QUOTIENT}, |
738 [rtac @{thm IDENTITY_QUOTIENT}, |
736 resolve_tac quot_thms, |
739 resolve_tac (quotient_rules_get ctxt)]) |
737 rtac @{thm IDENTITY_QUOTIENT}, |
|
738 rtac @{thm LIST_QUOTIENT}, |
|
739 (* For functional identity quotients, (op = ---> op =) *) |
|
740 (* TODO: think about the other way around, if we need to shorten the relation *) |
|
741 CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))]) |
|
742 *} |
740 *} |
743 |
741 |
744 lemma FUN_REL_I: |
742 lemma FUN_REL_I: |
745 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
743 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
746 shows "(R1 ===> R2) f g" |
744 shows "(R1 ===> R2) f g" |
899 (Abs a) => snd (Term.dest_abs a) |
897 (Abs a) => snd (Term.dest_abs a) |
900 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) *} |
898 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) *} |
901 |
899 |
902 |
900 |
903 ML {* |
901 ML {* |
904 fun inj_repabs_tac ctxt quot_thms rel_refl trans2 = |
902 fun inj_repabs_tac ctxt rel_refl trans2 = |
905 (FIRST' [ |
903 (FIRST' [ |
906 (* "cong" rule of the of the relation / transitivity*) |
904 (* "cong" rule of the of the relation / transitivity*) |
907 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
905 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
908 NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [ |
906 NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [ |
909 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), |
907 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), |
931 NDT ctxt "8" (rtac @{thm refl}), |
929 NDT ctxt "8" (rtac @{thm refl}), |
932 |
930 |
933 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
931 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
934 (* observe ---> *) |
932 (* observe ---> *) |
935 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
933 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
936 THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), |
934 THEN' (RANGE [SOLVES' (quotient_tac ctxt)]))), |
937 |
935 |
938 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
936 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
939 NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN' |
937 NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN' |
940 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), |
938 (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt), |
941 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
939 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
942 |
940 |
943 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
941 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
944 (* merge with previous tactic *) |
942 (* merge with previous tactic *) |
945 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
943 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
951 (* reflexivity of the basic relations *) |
949 (* reflexivity of the basic relations *) |
952 (* R \<dots> \<dots> *) |
950 (* R \<dots> \<dots> *) |
953 NDT ctxt "D" (resolve_tac rel_refl), |
951 NDT ctxt "D" (resolve_tac rel_refl), |
954 |
952 |
955 (* resolving with R x y assumptions *) |
953 (* resolving with R x y assumptions *) |
956 NDT ctxt "E" (atac), |
954 NDT ctxt "E" (atac) |
957 |
955 |
958 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
956 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
959 (* global simplification *) |
957 (* global simplification *) |
960 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
958 (*NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*) |
961 *} |
959 ]) |
962 |
960 *} |
963 ML {* |
961 |
964 fun all_inj_repabs_tac ctxt quot_thms rel_refl trans2 = |
962 ML {* |
965 REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2) |
963 fun all_inj_repabs_tac ctxt rel_refl trans2 = |
|
964 REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) |
966 *} |
965 *} |
967 |
966 |
968 (* A faster version *) |
967 (* A faster version *) |
969 |
968 |
970 ML {* |
969 ML {* |
1022 |
1021 |
1023 section {* Cleaning of the theorem *} |
1022 section {* Cleaning of the theorem *} |
1024 |
1023 |
1025 |
1024 |
1026 (* TODO: This is slow *) |
1025 (* TODO: This is slow *) |
1027 ML {* |
1026 (* |
1028 fun allex_prs_tac ctxt quot = |
1027 ML {* |
1029 (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot) |
1028 fun allex_prs_tac ctxt = |
1030 *} |
1029 (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt) |
|
1030 *} |
|
1031 *) |
1031 |
1032 |
1032 ML {* |
1033 ML {* |
1033 fun make_inst lhs t = |
1034 fun make_inst lhs t = |
1034 let |
1035 let |
1035 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
1036 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
1044 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1045 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1045 *} |
1046 *} |
1046 |
1047 |
1047 (* It proves the QUOTIENT assumptions by calling quotient_tac *) |
1048 (* It proves the QUOTIENT assumptions by calling quotient_tac *) |
1048 ML {* |
1049 ML {* |
1049 fun solve_quotient_assum i quot_thms ctxt thm = |
1050 fun solve_quotient_assum i ctxt thm = |
1050 let |
1051 let |
1051 val tac = |
1052 val tac = |
1052 (compose_tac (false, thm, i)) THEN_ALL_NEW |
1053 (compose_tac (false, thm, i)) THEN_ALL_NEW |
1053 (quotient_tac ctxt quot_thms); |
1054 (quotient_tac ctxt); |
1054 val gc = Drule.strip_imp_concl (cprop_of thm); |
1055 val gc = Drule.strip_imp_concl (cprop_of thm); |
1055 in |
1056 in |
1056 Goal.prove_internal [] gc (fn _ => tac 1) |
1057 Goal.prove_internal [] gc (fn _ => tac 1) |
1057 end |
1058 end |
1058 handle _ => error "solve_quotient_assum" |
1059 handle _ => error "solve_quotient_assum" |
1059 *} |
1060 *} |
1060 |
1061 |
1061 ML {* |
1062 ML {* |
1062 fun lambda_allex_prs_simple_conv quot_thms ctxt ctrm = |
1063 fun lambda_allex_prs_simple_conv ctxt ctrm = |
1063 case (term_of ctrm) of |
1064 case (term_of ctrm) of |
1064 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1065 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1065 let |
1066 let |
1066 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
1067 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
1067 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); |
1068 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); |
1068 val thy = ProofContext.theory_of ctxt; |
1069 val thy = ProofContext.theory_of ctxt; |
1069 val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d] |
1070 val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d] |
1070 val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; |
1071 val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; |
1071 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1072 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1072 val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; |
1073 val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; |
1073 val te = @{thm eq_reflection} OF [solve_quotient_assum 2 quot_thms ctxt lpi] |
1074 val te = @{thm eq_reflection} OF [solve_quotient_assum 2 ctxt lpi] |
1074 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1075 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1075 val tl = Thm.lhs_of ts; |
1076 val tl = Thm.lhs_of ts; |
1076 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
1077 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
1077 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1078 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1078 in |
1079 in |
1085 val thy = ProofContext.theory_of ctxt; |
1086 val thy = ProofContext.theory_of ctxt; |
1086 val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
1087 val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
1087 val tyinst = [SOME cty_a, SOME cty_b]; |
1088 val tyinst = [SOME cty_a, SOME cty_b]; |
1088 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1089 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1089 val thm = Drule.instantiate' tyinst tinst @{thm all_prs}; |
1090 val thm = Drule.instantiate' tyinst tinst @{thm all_prs}; |
1090 val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm]; |
1091 val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm]; |
1091 in |
1092 in |
1092 Conv.rewr_conv ti ctrm |
1093 Conv.rewr_conv ti ctrm |
1093 end |
1094 end |
1094 | (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
1095 | (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
1095 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
1096 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
1098 val thy = ProofContext.theory_of ctxt; |
1099 val thy = ProofContext.theory_of ctxt; |
1099 val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
1100 val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
1100 val tyinst = [SOME cty_a, SOME cty_b]; |
1101 val tyinst = [SOME cty_a, SOME cty_b]; |
1101 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1102 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1102 val thm = Drule.instantiate' tyinst tinst @{thm ex_prs}; |
1103 val thm = Drule.instantiate' tyinst tinst @{thm ex_prs}; |
1103 val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm]; |
1104 val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm]; |
1104 in |
1105 in |
1105 Conv.rewr_conv ti ctrm |
1106 Conv.rewr_conv ti ctrm |
1106 end |
1107 end |
1107 | _ => Conv.all_conv ctrm |
1108 | _ => Conv.all_conv ctrm |
1108 *} |
1109 *} |
1109 |
1110 |
1110 (* quot stands for the QUOTIENT theorems: *) |
1111 (* quot stands for the QUOTIENT theorems: *) |
1111 (* could be potentially all of them *) |
1112 (* could be potentially all of them *) |
1112 ML {* |
1113 ML {* |
1113 fun lambda_allex_prs_conv quot = |
1114 val lambda_allex_prs_conv = |
1114 More_Conv.top_conv (lambda_allex_prs_simple_conv quot) |
1115 More_Conv.top_conv lambda_allex_prs_simple_conv |
1115 *} |
1116 *} |
1116 |
1117 |
1117 ML {* |
1118 ML {* |
1118 fun lambda_allex_prs_tac quot ctxt = CONVERSION (lambda_allex_prs_conv quot ctxt) |
1119 fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt) |
1119 *} |
1120 *} |
1120 |
1121 |
1121 (* |
1122 (* |
1122 Cleaning the theorem consists of 6 kinds of rewrites. |
1123 Cleaning the theorem consists of 6 kinds of rewrites. |
1123 The first two need to be done before fun_map is unfolded |
1124 The first two need to be done before fun_map is unfolded |
1143 The second one is an EqSubst (slow). |
1144 The second one is an EqSubst (slow). |
1144 The rest are a simp_tac and are fast. |
1145 The rest are a simp_tac and are fast. |
1145 *) |
1146 *) |
1146 |
1147 |
1147 ML {* |
1148 ML {* |
1148 fun clean_tac lthy quot = |
1149 fun clean_tac lthy = |
1149 let |
1150 let |
1150 val thy = ProofContext.theory_of lthy; |
1151 val thy = ProofContext.theory_of lthy; |
|
1152 val quotients = quotient_rules_get lthy |
1151 val defs = map (Thm.varifyT o #def) (qconsts_dest thy); |
1153 val defs = map (Thm.varifyT o #def) (qconsts_dest thy); |
1152 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1154 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quotients |
1153 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1155 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1154 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1156 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quotients |
1155 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1157 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1156 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1158 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1157 (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) |
1159 (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) |
1158 in |
1160 in |
1159 EVERY' [ |
1161 EVERY' [ |
1160 (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f *) |
1162 (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f *) |
1161 (* \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f *) |
1163 (* \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f *) |
1162 NDT lthy "a" (TRY o lambda_allex_prs_tac quot lthy), |
1164 NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), |
1163 |
1165 |
1164 (* NewConst ----> (rep ---> abs) oldConst *) |
1166 (* NewConst ----> (rep ---> abs) oldConst *) |
1165 (* Abs (Rep x) ----> x *) |
1167 (* Abs (Rep x) ----> x *) |
1166 (* id_simps; fun_map.simps *) |
1168 (* id_simps; fun_map.simps *) |
1167 NDT lthy "c" (TRY o simp_tac simp_ctxt), |
1169 NDT lthy "c" (TRY o simp_tac simp_ctxt), |