--- a/src/Doc/Datatypes/Datatypes.thy Tue Jan 07 12:37:12 2020 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jan 07 14:58:01 2020 +0100
@@ -3022,12 +3022,7 @@
lift_bnf 'a myoption (*<*)[wits: "Inl undefined :: 'a + 'a"](*>*)
- proof (intro rel_funI)
- fix f g :: "'a \<Rightarrow> 'b" and x y :: "'a + 'a"
- assume "f = g" "ignore_Inl x y"
- then show "ignore_Inl (map_sum f f x) (map_sum g g y)"
- by (cases x; cases y) auto
- next
+ proof -
fix P :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and Q :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
assume "P OO Q \<noteq> bot"
then show "rel_sum P P OO ignore_Inl OO rel_sum Q Q
--- a/src/HOL/Datatype_Examples/TLList.thy Tue Jan 07 12:37:12 2020 +0100
+++ b/src/HOL/Datatype_Examples/TLList.thy Tue Jan 07 14:58:01 2020 +0100
@@ -85,8 +85,6 @@
lift_bnf (tlset1: 'a, tlset2: 'b) tllist
[wits: "\<lambda>b. (LNil :: 'a llist, b)" "\<lambda>a. (lconst a, undefined)" ]
for map: tlmap rel: tlrel
- subgoal
- by (auto simp: rel_fun_def eq_tllist_def)
subgoal for P Q P' Q'
by (force simp: eq_tllist_def relcompp_apply llist.rel_compp lfinite_lrel_eq split: if_splits)
subgoal for Ss
--- a/src/HOL/Quotient.thy Tue Jan 07 12:37:12 2020 +0100
+++ b/src/HOL/Quotient.thy Tue Jan 07 14:58:01 2020 +0100
@@ -827,6 +827,18 @@
finally show ?thesis .
qed
+lemma Grp_conversep_eq_onp: "((BNF_Def.Grp UNIV f)\<inverse>\<inverse> OO BNF_Def.Grp UNIV f) = eq_onp (\<lambda>x. x \<in> range f)"
+ by (auto simp: fun_eq_iff Grp_def eq_onp_def image_iff)
+
+lemma Grp_conversep_nonempty: "(BNF_Def.Grp UNIV f)\<inverse>\<inverse> OO BNF_Def.Grp UNIV f \<noteq> bot"
+ by (auto simp: fun_eq_iff Grp_def)
+
+lemma relcomppI2: "r a b \<Longrightarrow> s b c \<Longrightarrow> t c d \<Longrightarrow> (r OO s OO t) a d"
+ by (auto)
+
+lemma rel_conj_eq_onp: "equivp R \<Longrightarrow> rel_conj R (eq_onp P) \<le> R"
+ by (auto simp: eq_onp_def transp_def equivp_def)
+
ML_file "Tools/BNF/bnf_lift.ML"
hide_fact
@@ -834,7 +846,7 @@
image_map_sum_unit_subset subset_lift_sum_unitD UNIV_sum_unit_conv subset_vimage_image_subset
relcompp_mem_Grp_neq_bot comp_projr_Inr in_rel_sum_in_image_projr subset_rel_sumI
relcompp_eq_Grp_neq_bot rel_fun_rel_OO1 rel_fun_rel_OO2 rel_sum_eq2_nonempty rel_sum_eq3_nonempty
- hypsubst equivp_add_relconj
+ hypsubst equivp_add_relconj Grp_conversep_eq_onp Grp_conversep_nonempty relcomppI2 rel_conj_eq_onp
end
--- a/src/HOL/Tools/BNF/bnf_lift.ML Tue Jan 07 12:37:12 2020 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Tue Jan 07 14:58:01 2020 +0100
@@ -923,10 +923,6 @@
val equiv_rel_a = #tm REL;
val (equiv_rel_b, equiv_rel_c) = apply2 (subst_Ts equiv_rel_a) (betas, gammas);
- (* map_F_respect: @{term "((=) ===> REL ===> REL) map_F map_F"} *)
- val map_F_respect = HOLogic.mk_Trueprop (fold_rev mk_rel_fun (map2 (fn xT => fn yT =>
- HOLogic.eq_const (xT --> yT)) alphas betas @ [equiv_rel_a]) (equiv_rel_b) $ map_F $ map_F);
-
(* rel_pos_distr: @{term "\<And>A B.
A \<circ>\<circ> B \<noteq> bot \<Longrightarrow> REL \<circ>\<circ> rel_F A \<circ>\<circ> REL \<circ>\<circ> rel_F B \<circ>\<circ> REL \<le> REL \<circ>\<circ> rel_F (A \<circ>\<circ> B) \<circ>\<circ> REL"} *)
fun compp_not_bot comp aT cT = let
@@ -1012,7 +1008,7 @@
val (Iwits, wit_goals) =
prepare_wits true repT wits opts alphas wits_F var_as var_as' sets' lthy;
- val goals = map_F_respect :: rel_pos_distr :: rel_Inters @
+ val goals = rel_pos_distr :: rel_Inters @
(case wits of NONE => [] | _ => wit_goals);
val plugins =
@@ -1020,7 +1016,7 @@
the_default Plugin_Name.default_filter;
fun after_qed thmss lthy =
- (case thmss of [map_F_respect_thm] :: [rel_pos_distr_thm0] :: thmss =>
+ (case thmss of [rel_pos_distr_thm0] :: thmss =>
let
val equiv_thm' = REL_rewr_all lthy equiv_thm;
val rel_pos_distr_thm =
@@ -1097,6 +1093,8 @@
val map_F_id0 = map_id0_of_bnf bnf_F;
val map_F_id = map_id_of_bnf bnf_F;
val rel_conversep = rel_conversep_of_bnf bnf_F;
+ val rel_flip = rel_flip_of_bnf bnf_F;
+ val rel_eq_onp = rel_eq_onp_of_bnf bnf_F;
val rel_Grp = rel_Grp_of_bnf bnf_F;
val rel_OO = rel_OO_of_bnf bnf_F;
val rel_map = rel_map_of_bnf bnf_F;
@@ -1104,6 +1102,29 @@
val set_bd_thms = set_bd_of_bnf bnf_F;
val set_map_thms = set_map_of_bnf bnf_F;
+
+
+ (* map_F_respect: @{term "((=) ===> REL ===> REL) map_F map_F"} *)
+ val map_F_respect = HOLogic.mk_Trueprop (fold_rev mk_rel_fun (map2 (fn xT => fn yT =>
+ HOLogic.eq_const (xT --> yT)) alphas betas @ [equiv_rel_a]) (equiv_rel_b) $ map_F $ map_F);
+
+ fun map_F_respect_tac ctxt =
+ HEADGOAL (EVERY'
+ [REPEAT_DETERM_N (live + 1) o rtac ctxt @{thm rel_funI}, hyp_subst_tac ctxt,
+ rtac ctxt (BNF_FP_Util.split_conj_prems live rel_pos_distr_thm0 OF
+ replicate live @{thm Grp_conversep_nonempty} RS rev_mp),
+ rtac ctxt impI, dtac ctxt @{thm predicate2D}, etac ctxt @{thm relcomppI2[rotated]},
+ rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]},
+ REPEAT_DETERM o resolve_tac ctxt [CollectI, conjI, subset_UNIV],
+ rtac ctxt (rel_flip RS iffD2),
+ rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]},
+ REPEAT_DETERM o resolve_tac ctxt [CollectI, conjI, subset_UNIV],
+ SELECT_GOAL (unfold_thms_tac ctxt (rel_eq_onp :: @{thms Grp_conversep_eq_onp})),
+ etac ctxt @{thm predicate2D[OF rel_conj_eq_onp, rotated]},
+ rtac ctxt equiv_thm']);
+
+ val map_F_respect_thm = prove lthy [] map_F_respect map_F_respect_tac;
+
val rel_funD = mk_rel_funDN (live+1);
val map_F_rsp = (rel_funD map_F_respect_thm) OF (replicate live refl);
fun map_F_rsp_of tms ctxt = (infer_instantiate' ctxt (NONE :: NONE