# HG changeset patch # User traytel # Date 1443090079 -7200 # Node ID 464c5da3f508b7949a65ea7703a6a2ff303558c1 # Parent dd949db0ade8e043fee067f87b69a725c0f4e58f more useful properties of the relators diff -r dd949db0ade8 -r 464c5da3f508 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 24 12:21:19 2015 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 24 12:21:19 2015 +0200 @@ -1003,6 +1003,18 @@ \item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\ @{thm list.rel_refl[no_vars]} +\item[@{text "t."}\hthm{rel_refl_strong}\rm:] ~ \\ +@{thm list.rel_refl_strong[no_vars]} + +\item[@{text "t."}\hthm{rel_reflp}\rm:] ~ \\ +@{thm list.rel_reflp[no_vars]} + +\item[@{text "t."}\hthm{rel_symp}\rm:] ~ \\ +@{thm list.rel_symp[no_vars]} + +\item[@{text "t."}\hthm{rel_transp}\rm:] ~ \\ +@{thm list.rel_transp[no_vars]} + \item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm list.rel_transfer[no_vars]} \\ The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin diff -r dd949db0ade8 -r 464c5da3f508 src/HOL/BNF_Def.thy --- a/src/HOL/BNF_Def.thy Thu Sep 24 12:21:19 2015 +0200 +++ b/src/HOL/BNF_Def.thy Thu Sep 24 12:21:19 2015 +0200 @@ -234,6 +234,18 @@ lemma ge_eq_refl: "op = \ R \ R x x" by auto +lemma reflp_eq: "reflp R = (op = \ R)" + by (auto simp: reflp_def fun_eq_iff) + +lemma transp_relcompp: "transp r \ r OO r \ r" + by (auto simp: transp_def) + +lemma symp_conversep: "symp R = (R\\ \ R)" + by (auto simp: symp_def fun_eq_iff) + +lemma diag_imp_eq_le: "(\x. x \ A \ R x x) \ \x y. x \ A \ y \ A \ x = y \ R x y" + by blast + ML_file "Tools/BNF/bnf_util.ML" ML_file "Tools/BNF/bnf_tactics.ML" ML_file "Tools/BNF/bnf_def_tactics.ML" diff -r dd949db0ade8 -r 464c5da3f508 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Thu Sep 24 12:21:19 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Thu Sep 24 12:21:19 2015 +0200 @@ -82,6 +82,10 @@ val rel_mono_strong0_of_bnf: bnf -> thm val rel_mono_strong_of_bnf: bnf -> thm val rel_refl_of_bnf: bnf -> thm + val rel_refl_strong_of_bnf: bnf -> thm + val rel_reflp_of_bnf: bnf -> thm + val rel_symp_of_bnf: bnf -> thm + val rel_transp_of_bnf: bnf -> thm val rel_map_of_bnf: bnf -> thm list val rel_transfer_of_bnf: bnf -> thm val rel_eq_of_bnf: bnf -> thm @@ -254,13 +258,18 @@ rel_conversep: thm lazy, rel_OO: thm lazy, rel_refl: thm lazy, + rel_refl_strong: thm lazy, + rel_reflp: thm lazy, + rel_symp: thm lazy, + rel_transp: thm lazy, rel_transfer: thm lazy }; fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel - inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident - map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong - set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_transfer = { + inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident map_transfer + rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong set_transfer + rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp + rel_transfer = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, bd_Cnotzero = bd_Cnotzero, @@ -291,6 +300,10 @@ rel_conversep = rel_conversep, rel_OO = rel_OO, rel_refl = rel_refl, + rel_refl_strong = rel_refl_strong, + rel_reflp = rel_reflp, + rel_symp = rel_symp, + rel_transp = rel_transp, set_transfer = set_transfer}; fun map_facts f { @@ -324,6 +337,10 @@ rel_conversep, rel_OO, rel_refl, + rel_refl_strong, + rel_reflp, + rel_symp, + rel_transp, set_transfer} = {bd_Card_order = f bd_Card_order, bd_Cinfinite = f bd_Cinfinite, @@ -355,6 +372,10 @@ rel_conversep = Lazy.map f rel_conversep, rel_OO = Lazy.map f rel_OO, rel_refl = Lazy.map f rel_refl, + rel_refl_strong = Lazy.map f rel_refl_strong, + rel_reflp = Lazy.map f rel_reflp, + rel_symp = Lazy.map f rel_symp, + rel_transp = Lazy.map f rel_transp, set_transfer = Lazy.map (map f) set_transfer}; val morph_facts = map_facts o Morphism.thm; @@ -487,6 +508,10 @@ val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf; val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf; val rel_refl_of_bnf = Lazy.force o #rel_refl o #facts o rep_bnf; +val rel_refl_strong_of_bnf = Lazy.force o #rel_refl_strong o #facts o rep_bnf; +val rel_reflp_of_bnf = Lazy.force o #rel_reflp o #facts o rep_bnf; +val rel_symp_of_bnf = Lazy.force o #rel_symp o #facts o rep_bnf; +val rel_transp_of_bnf = Lazy.force o #rel_transp o #facts o rep_bnf; val rel_map_of_bnf = Lazy.force o #rel_map o #facts o rep_bnf; val rel_transfer_of_bnf = Lazy.force o #rel_transfer o #facts o rep_bnf; val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf; @@ -671,6 +696,10 @@ val rel_mono_strong0N = "rel_mono_strong0"; val rel_mono_strongN = "rel_mono_strong"; val rel_reflN = "rel_refl"; +val rel_refl_strongN = "rel_refl_strong"; +val rel_reflpN = "rel_reflp"; +val rel_sympN = "rel_symp"; +val rel_transpN = "rel_transp"; val rel_transferN = "rel_transfer"; val rel_comppN = "rel_compp"; val rel_compp_GrpN = "rel_compp_Grp"; @@ -743,6 +772,10 @@ (rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs), (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)], []), (rel_reflN, [Lazy.force (#rel_refl facts)], []), + (rel_refl_strongN, [Lazy.force (#rel_refl_strong facts)], []), + (rel_reflpN, [Lazy.force (#rel_reflp facts)], []), + (rel_sympN, [Lazy.force (#rel_symp facts)], []), + (rel_transpN, [Lazy.force (#rel_transp facts)], []), (rel_transferN, [Lazy.force (#rel_transfer facts)], []), (set_mapN, map Lazy.force (#set_map facts), []), (set_transferN, Lazy.force (#set_transfer facts), [])] @@ -1432,6 +1465,33 @@ val rel_refl = Lazy.lazy mk_rel_refl; + fun mk_rel_refl_strong () = + (rule_by_tactic lthy (ALLGOALS (Object_Logic.full_atomize_tac lthy)) + ((Lazy.force rel_eq RS @{thm predicate2_eqD}) RS @{thm iffD2[OF _ refl]} RS + Lazy.force rel_mono_strong)) OF + (replicate live @{thm diag_imp_eq_le}) + + val rel_refl_strong = Lazy.lazy mk_rel_refl_strong; + + fun mk_rel_preserves mk_prop prop_conv_thm thm () = + let + val Rs = map2 retype_const_or_free self_pred2RTs Rs; + val prems = map (HOLogic.mk_Trueprop o mk_prop) Rs; + val goal = HOLogic.mk_Trueprop (mk_prop (Term.list_comb (relAsAs, Rs))); + in + Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal)) + (fn {context = ctxt, prems = _} => + unfold_thms_tac ctxt [prop_conv_thm] THEN + HEADGOAL (rtac ctxt (Lazy.force thm RS sym RS @{thm ord_eq_le_trans}) + THEN' rtac ctxt (Lazy.force rel_mono) THEN_ALL_NEW assume_tac ctxt)) + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation + end; + + val rel_reflp = Lazy.lazy (mk_rel_preserves mk_reflp @{thm reflp_eq} rel_eq); + val rel_symp = Lazy.lazy (mk_rel_preserves mk_symp @{thm symp_conversep} rel_conversep); + val rel_transp = Lazy.lazy (mk_rel_preserves mk_transp @{thm transp_relcompp} rel_OO); + fun mk_map_transfer () = let val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs; @@ -1520,7 +1580,8 @@ val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 - rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_transfer; + rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong + rel_reflp rel_symp rel_transp rel_transfer; val wits = map2 mk_witness bnf_wits wit_thms; diff -r dd949db0ade8 -r 464c5da3f508 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 24 12:21:19 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 24 12:21:19 2015 +0200 @@ -61,6 +61,9 @@ val mk_rel_comp: term * term -> term val mk_rel_compp: term * term -> term val mk_vimage2p: term -> term -> term + val mk_reflp: term -> term + val mk_symp: term -> term + val mk_transp: term -> term (*parameterized terms*) val mk_nthN: int -> term -> int -> term @@ -348,6 +351,12 @@ (T1 --> T2) --> (U1 --> U2) --> mk_pred2T T2 U2 --> mk_pred2T T1 U1) $ f $ g end; +fun mk_pred name R = + Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R; +val mk_reflp = mk_pred @{const_name reflp}; +val mk_symp = mk_pred @{const_name symp}; +val mk_transp = mk_pred @{const_name transp}; + fun mk_trans thm1 thm2 = trans OF [thm1, thm2]; fun mk_sym thm = thm RS sym;