src/HOL/Library/Multiset.thy

   "mult r = (mult1 r)\<^sup>+"
 
 definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
   "multp r M N \<longleftrightarrow> (M, N) \<in> mult {(x, y). r x y}"
 
+declare multp_def[pred_set_conv]
+
 lemma mult1I:
   assumes "M = add_mset a M0" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
   shows "(N, M) \<in> mult1 r"
   using assms unfolding mult1_def by blast
 

           rule_tac x = "K + K'" in exI)
         (use z y N False K in \<open>auto simp: add.assoc\<close>)
   qed
 qed
 
-lemmas multp_implies_one_step =
-  mult_implies_one_step[of "{(x, y). r x y}" for r, folded multp_def transp_trans, simplified]
+lemma multp_implies_one_step:
+  "transp R \<Longrightarrow> multp R M N \<Longrightarrow> \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>#K. \<exists>x\<in>#J. R k x)"
+  by (rule mult_implies_one_step[to_pred])
 
 lemma one_step_implies_mult:
   assumes
     "J \<noteq> {#}" and
     "\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r"

     ultimately show ?thesis
       unfolding mult_def by simp
   qed
 qed
 
-lemmas one_step_implies_multp =
-  one_step_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def, simplified]
+lemma one_step_implies_multp:
+  "J \<noteq> {#} \<Longrightarrow> \<forall>k\<in>#K. \<exists>j\<in>#J. R k j \<Longrightarrow> multp R (I + K) (I + J)"
+  by (rule one_step_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def, simplified])
 
 lemma subset_implies_mult:
   assumes sub: "A \<subset># B"
   shows "(A, B) \<in> mult r"
 proof -

     using sub by (simp add: Diff_eq_empty_iff_mset subset_mset.less_le_not_le)
   thus ?thesis
     by (rule one_step_implies_mult[of "B - A" "{#}" _ A, unfolded ApBmA, simplified])
 qed
 
-lemmas subset_implies_multp = subset_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def]
+lemma subset_implies_multp: "A \<subset># B \<Longrightarrow> multp r A B"
+  by (rule subset_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def])
 
 
 subsubsection \<open>Monotonicity\<close>
 
 lemma multp_mono_strong:

     where "Y = I + J" "X = I + K" "J \<noteq> {#}" "\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> s"
     using mult_implies_one_step[OF \<open>trans s\<close>] by blast
   thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
 qed
 
-lemmas multp_cancel =
-  mult_cancel[of "{(x, y). r x y}" for r,
-    folded multp_def transp_trans irreflp_irrefl_eq, simplified]
-
-lemmas mult_cancel_add_mset =
-  mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral]
-
-lemmas multp_cancel_add_mset =
-  mult_cancel_add_mset[of "{(x, y). r x y}" for r,
-    folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+lemma multp_cancel:
+  "transp R \<Longrightarrow> irreflp R \<Longrightarrow> multp R (X + Z) (Y + Z) \<longleftrightarrow> multp R X Y"
+  by (rule mult_cancel[to_pred])
+
+lemma mult_cancel_add_mset:
+  "trans r \<Longrightarrow> irrefl r \<Longrightarrow> ((add_mset z X, add_mset z Y) \<in> mult r) = ((X, Y) \<in> mult r)"
+  by (rule mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral])
+
+lemma multp_cancel_add_mset:
+  "transp R \<Longrightarrow> irreflp R \<Longrightarrow> multp R (add_mset z X) (add_mset z Y) = multp R X Y"
+  by (rule mult_cancel_add_mset[to_pred])
 
 lemma mult_cancel_max0:
   assumes "trans s" and "irrefl s"
   shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
 proof -

   thus ?thesis using mult_cancel[OF assms, of "X - X \<inter># Y"  "X \<inter># Y" "Y - X \<inter># Y"] by auto
 qed
 
 lemmas mult_cancel_max = mult_cancel_max0[simplified]
 
-lemmas multp_cancel_max =
-  mult_cancel_max[of "{(x, y). r x y}" for r,
-    folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+lemma multp_cancel_max: "transp R \<Longrightarrow> irreflp R \<Longrightarrow> multp R X Y = multp R (X - Y) (Y - X)"
+  by (rule mult_cancel_max[to_pred])
 
 
 subsubsection \<open>Partial-order properties\<close>
 
 lemma mult1_lessE:

     thus ?case ..
   qed
   with * show False by simp
 qed
 
-lemmas irreflp_multp =
-  irrefl_mult[of "{(x, y). r x y}" for r,
-    folded transp_trans_eq irreflp_irrefl_eq, simplified, folded multp_def]
+lemma irreflp_multp: "transp R \<Longrightarrow> irreflp R \<Longrightarrow> irreflp (multp R)"
+  by (rule irrefl_mult[of "{(x, y). r x y}" for r,
+    folded transp_trans_eq irreflp_irrefl_eq, simplified, folded multp_def])
 
 instantiation multiset :: (preorder) order begin
 
 definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
   where "M < N \<longleftrightarrow> multp (<) M N"