derive pred_mono property for BNFs

--- 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 \<Longrightarrow> X \<subseteq> Collect (case_prod A) \<Longrightarrow> x \<in> X \<Longrightarrow> B ((f o fst) x) ((g o snd) x)"
   unfolding rel_fun_def by auto
 
+lemma eq_onp_mono_iff: "eq_onp P \<le> eq_onp Q \<longleftrightarrow> P \<le> 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"

--- 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;
 

--- 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,