# HG changeset patch # User traytel # Date 1578405481 -3600 # Node ID c71a44893645489c56017613828474c0cd75fde4 # Parent 41f3ca717da5b79bf54edc0f6624062406a965f6 eliminated one redundant proof obligation in lift_bnf for quotients diff -r 41f3ca717da5 -r c71a44893645 src/Doc/Datatypes/Datatypes.thy --- 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 \ '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 \ 'b \ bool" and Q :: "'b \ 'c \ bool" assume "P OO Q \ bot" then show "rel_sum P P OO ignore_Inl OO rel_sum Q Q diff -r 41f3ca717da5 -r c71a44893645 src/HOL/Datatype_Examples/TLList.thy --- 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: "\b. (LNil :: 'a llist, b)" "\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 diff -r 41f3ca717da5 -r c71a44893645 src/HOL/Quotient.thy --- 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)\\ OO BNF_Def.Grp UNIV f) = eq_onp (\x. x \ range f)" + by (auto simp: fun_eq_iff Grp_def eq_onp_def image_iff) + +lemma Grp_conversep_nonempty: "(BNF_Def.Grp UNIV f)\\ OO BNF_Def.Grp UNIV f \ bot" + by (auto simp: fun_eq_iff Grp_def) + +lemma relcomppI2: "r a b \ s b c \ t c d \ (r OO s OO t) a d" + by (auto) + +lemma rel_conj_eq_onp: "equivp R \ rel_conj R (eq_onp P) \ 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 diff -r 41f3ca717da5 -r c71a44893645 src/HOL/Tools/BNF/bnf_lift.ML --- 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 "\A B. A \\ B \ bot \ REL \\ rel_F A \\ REL \\ rel_F B \\ REL \ REL \\ rel_F (A \\ B) \\ 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