# HG changeset patch # User traytel # Date 1471511407 -7200 # Node ID b62f4f765353b2ca0e766ba7ea9b91331349d4a3 # Parent 009e176e10103c49a9bff010080bb8dfd974b2c5 derive pred_mono property for BNFs diff -r 009e176e1010 -r b62f4f765353 src/HOL/BNF_Def.thy --- a/src/HOL/BNF_Def.thy Wed Aug 17 16:16:38 2016 +0200 +++ b/src/HOL/BNF_Def.thy Thu Aug 18 11:10:07 2016 +0200 @@ -269,6 +269,9 @@ "rel_fun A B f g \ X \ Collect (case_prod A) \ x \ X \ B ((f o fst) x) ((g o snd) x)" unfolding rel_fun_def by auto +lemma eq_onp_mono_iff: "eq_onp P \ eq_onp Q \ P \ Q" + unfolding eq_onp_def by auto + ML_file "Tools/BNF/bnf_util.ML" ML_file "Tools/BNF/bnf_tactics.ML" ML_file "Tools/BNF/bnf_def_tactics.ML" diff -r 009e176e1010 -r b62f4f765353 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Wed Aug 17 16:16:38 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Thu Aug 18 11:10:07 2016 +0200 @@ -83,6 +83,7 @@ val pred_map_of_bnf: bnf -> thm val pred_mono_strong0_of_bnf: bnf -> thm val pred_mono_strong_of_bnf: bnf -> thm + val pred_mono_of_bnf: bnf -> thm val pred_set_of_bnf: bnf -> thm val pred_rel_of_bnf: bnf -> thm val pred_transfer_of_bnf: bnf -> thm @@ -298,6 +299,7 @@ pred_rel: thm lazy, pred_mono_strong0: thm lazy, pred_mono_strong: thm lazy, + pred_mono: thm lazy, pred_cong0: thm lazy, pred_cong: thm lazy, pred_cong_simp: thm lazy @@ -308,7 +310,8 @@ map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp 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 rel_eq_onp pred_transfer pred_True - pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_cong0 pred_cong pred_cong_simp = { + pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_mono pred_cong0 pred_cong + pred_cong_simp = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, bd_Cnotzero = bd_Cnotzero, @@ -354,6 +357,7 @@ pred_rel = pred_rel, pred_mono_strong0 = pred_mono_strong0, pred_mono_strong = pred_mono_strong, + pred_mono = pred_mono, pred_cong0 = pred_cong0, pred_cong = pred_cong, pred_cong_simp = pred_cong_simp}; @@ -404,6 +408,7 @@ pred_rel, pred_mono_strong0, pred_mono_strong, + pred_mono, pred_cong0, pred_cong, pred_cong_simp} = @@ -452,6 +457,7 @@ pred_rel = Lazy.map f pred_rel, pred_mono_strong0 = Lazy.map f pred_mono_strong0, pred_mono_strong = Lazy.map f pred_mono_strong, + pred_mono = Lazy.map f pred_mono, pred_cong0 = Lazy.map f pred_cong0, pred_cong = Lazy.map f pred_cong, pred_cong_simp = Lazy.map f pred_cong_simp}; @@ -587,6 +593,7 @@ val pred_map_of_bnf = Lazy.force o #pred_map o #facts o rep_bnf; val pred_mono_strong0_of_bnf = Lazy.force o #pred_mono_strong0 o #facts o rep_bnf; val pred_mono_strong_of_bnf = Lazy.force o #pred_mono_strong o #facts o rep_bnf; +val pred_mono_of_bnf = Lazy.force o #pred_mono o #facts o rep_bnf; val pred_cong0_of_bnf = Lazy.force o #pred_cong0 o #facts o rep_bnf; val pred_cong_of_bnf = Lazy.force o #pred_cong o #facts o rep_bnf; val pred_cong_simp_of_bnf = Lazy.force o #pred_cong_simp o #facts o rep_bnf; @@ -809,6 +816,7 @@ val map_transferN = "map_transfer"; val pred_mono_strong0N = "pred_mono_strong0"; val pred_mono_strongN = "pred_mono_strong"; +val pred_monoN = "pred_mono"; val pred_transferN = "pred_transfer"; val pred_TrueN = "pred_True"; val pred_mapN = "pred_map"; @@ -901,6 +909,7 @@ (map_transferN, [Lazy.force (#map_transfer facts)], []), (map_identN, [Lazy.force (#map_ident facts)], []), (pred_mono_strongN, [Lazy.force (#pred_mono_strong facts)], []), + (pred_monoN, [Lazy.force (#pred_mono facts)], []), (pred_congN, [Lazy.force (#pred_cong facts)], fundefcong_attrs), (pred_cong_simpN, [Lazy.force (#pred_cong_simp facts)], []), (pred_mapN, [Lazy.force (#pred_map facts)], []), @@ -1699,6 +1708,20 @@ val pred_mono_strong = Lazy.map (Object_Logic.rulify lthy) pred_mono_strong0; + fun mk_pred_mono () = + let + val mono_prems = mk_pred_prems mk_leq; + val mono_concl = mk_pred_concl (uncurry mk_leq); + in + Goal.prove_sorry lthy [] [] + (fold_rev Logic.all (Ps @ Ps_copy) (Logic.list_implies (mono_prems, mono_concl))) + (fn {context = ctxt, prems = _} => + mk_pred_mono_tac ctxt (Lazy.force rel_eq_onp) (Lazy.force rel_mono)) + |> Thm.close_derivation + end; + + val pred_mono = Lazy.lazy mk_pred_mono; + fun mk_pred_cong_prem mk_implies x z set P P_copy = Logic.all z (mk_implies (mk_Trueprop_mem (z, set $ x), mk_Trueprop_eq (P $ z, P_copy $ z))); @@ -1946,8 +1969,8 @@ map_ident0 map_ident map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp 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 rel_eq_onp - pred_transfer pred_True pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_cong0 - pred_cong pred_cong_simp; + pred_transfer pred_True pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_mono + pred_cong0 pred_cong pred_cong_simp; val wits = map2 mk_witness bnf_wits wit_thms; diff -r 009e176e1010 -r b62f4f765353 src/HOL/Tools/BNF/bnf_def_tactics.ML --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Aug 17 16:16:38 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Aug 18 11:10:07 2016 +0200 @@ -31,6 +31,7 @@ val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic val mk_rel_eq_onp_tac: Proof.context -> thm -> thm -> thm -> tactic val mk_pred_mono_strong0_tac: Proof.context -> thm -> thm -> tactic + val mk_pred_mono_tac: Proof.context -> thm -> thm -> tactic val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic val mk_pred_transfer_tac: Proof.context -> int -> thm -> thm -> thm -> tactic @@ -396,6 +397,10 @@ unfold_thms_tac ctxt [pred_rel] THEN HEADGOAL (etac ctxt rel_mono_strong0 THEN_ALL_NEW etac ctxt @{thm eq_onp_mono0}); +fun mk_pred_mono_tac ctxt rel_eq_onp rel_mono = + unfold_thms_tac ctxt (map mk_sym [@{thm eq_onp_mono_iff}, rel_eq_onp]) THEN + HEADGOAL (rtac ctxt rel_mono THEN_ALL_NEW assume_tac ctxt); + fun mk_pred_transfer_tac ctxt n in_rel pred_map pred_cong = HEADGOAL (EVERY' [REPEAT_DETERM_N (n + 1) o rtac ctxt rel_funI, dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE}, hyp_subst_tac ctxt,