# HG changeset patch
# User berghofe
# Date 1170866471 -3600
# Node ID 4ccb7e6be929b4c9d1396ef45245d7a941995612
# Parent  7c1e65897693470b40109d93217fb2b02329780d
Converted to predicate notation.

diff -r 7c1e65897693 -r 4ccb7e6be929 src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Wed Feb 07 17:39:49 2007 +0100
+++ b/src/HOL/Lambda/Commutation.thy	Wed Feb 07 17:41:11 2007 +0100
@@ -11,26 +11,26 @@
 subsection {* Basic definitions *}
 
 definition
-  square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool" where
+  square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
   "square R S T U =
-    (\<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U)))"
+    (\<forall>x y. R x y --> (\<forall>z. S x z --> (\<exists>u. T y u \<and> U z u)))"
 
 definition
-  commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool" where
+  commute :: "['a => 'a => bool, 'a => 'a => bool] => bool" where
   "commute R S = square R S S R"
 
 definition
-  diamond :: "('a \<times> 'a) set => bool" where
+  diamond :: "('a => 'a => bool) => bool" where
   "diamond R = commute R R"
 
 definition
-  Church_Rosser :: "('a \<times> 'a) set => bool" where
+  Church_Rosser :: "('a => 'a => bool) => bool" where
   "Church_Rosser R =
-    (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
+    (\<forall>x y. (join R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
 
 abbreviation
-  confluent :: "('a \<times> 'a) set => bool" where
-  "confluent R == diamond (R^*)"
+  confluent :: "('a => 'a => bool) => bool" where
+  "confluent R == diamond (R^**)"
 
 
 subsection {* Basic lemmas *}
@@ -43,31 +43,30 @@
   done
 
 lemma square_subset:
-    "[| square R S T U; T \<subseteq> T' |] ==> square R S T' U"
+    "[| square R S T U; T \<le> T' |] ==> square R S T' U"
   apply (unfold square_def)
-  apply blast
+  apply (blast dest: predicate2D)
   done
 
 lemma square_reflcl:
-    "[| square R S T (R^=); S \<subseteq> T |] ==> square (R^=) S T (R^=)"
+    "[| square R S T (R^==); S \<le> T |] ==> square (R^==) S T (R^==)"
   apply (unfold square_def)
-  apply blast
+  apply (blast dest: predicate2D)
   done
 
 lemma square_rtrancl:
-    "square R S S T ==> square (R^*) S S (T^*)"
+    "square R S S T ==> square (R^**) S S (T^**)"
   apply (unfold square_def)
   apply (intro strip)
-  apply (erule rtrancl_induct)
+  apply (erule rtrancl_induct')
    apply blast
-  apply (blast intro: rtrancl_into_rtrancl)
+  apply (blast intro: rtrancl.rtrancl_into_rtrancl)
   done
 
 lemma square_rtrancl_reflcl_commute:
-    "square R S (S^*) (R^=) ==> commute (R^*) (S^*)"
+    "square R S (S^**) (R^==) ==> commute (R^**) (S^**)"
   apply (unfold commute_def)
-  apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]
-    elim: r_into_rtrancl)
+  apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl])
   done
 
 
@@ -78,13 +77,13 @@
   apply (blast intro: square_sym)
   done
 
-lemma commute_rtrancl: "commute R S ==> commute (R^*) (S^*)"
+lemma commute_rtrancl: "commute R S ==> commute (R^**) (S^**)"
   apply (unfold commute_def)
   apply (blast intro: square_rtrancl square_sym)
   done
 
 lemma commute_Un:
-    "[| commute R T; commute S T |] ==> commute (R \<union> S) T"
+    "[| commute R T; commute S T |] ==> commute (join R S) T"
   apply (unfold commute_def square_def)
   apply blast
   done
@@ -93,7 +92,7 @@
 subsubsection {* diamond, confluence, and union *}
 
 lemma diamond_Un:
-    "[| diamond R; diamond S; commute R S |] ==> diamond (R \<union> S)"
+    "[| diamond R; diamond S; commute R S |] ==> diamond (join R S)"
   apply (unfold diamond_def)
   apply (assumption | rule commute_Un commute_sym)+
   done
@@ -104,22 +103,21 @@
   done
 
 lemma square_reflcl_confluent:
-    "square R R (R^=) (R^=) ==> confluent R"
+    "square R R (R^==) (R^==) ==> confluent R"
   apply (unfold diamond_def)
-  apply (fast intro: square_rtrancl_reflcl_commute r_into_rtrancl
-    elim: square_subset)
+  apply (fast intro: square_rtrancl_reflcl_commute elim: square_subset)
   done
 
 lemma confluent_Un:
-    "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (R \<union> S)"
-  apply (rule rtrancl_Un_rtrancl [THEN subst])
+    "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (join R S)"
+  apply (rule rtrancl_Un_rtrancl' [THEN subst])
   apply (blast dest: diamond_Un intro: diamond_confluent)
   done
 
 lemma diamond_to_confluence:
-    "[| diamond R; T \<subseteq> R; R \<subseteq> T^* |] ==> confluent T"
+    "[| diamond R; T \<le> R; R \<le> T^** |] ==> confluent T"
   apply (force intro: diamond_confluent
-    dest: rtrancl_subset [symmetric])
+    dest: rtrancl_subset' [symmetric])
   done
 
 
@@ -130,12 +128,12 @@
   apply (tactic {* safe_tac HOL_cs *})
    apply (tactic {*
      blast_tac (HOL_cs addIs
-       [thm "Un_upper2" RS thm "rtrancl_mono" RS thm "subsetD" RS thm "rtrancl_trans",
-        thm "rtrancl_converseI", thm "converseI",
-        thm "Un_upper1" RS thm "rtrancl_mono" RS thm "subsetD"]) 1 *})
-  apply (erule rtrancl_induct)
+       [thm "join_right_le" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
+        thm "rtrancl_converseI'", thm "conversepI",
+        thm "join_left_le" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
+  apply (erule rtrancl_induct')
    apply blast
-  apply (blast del: rtrancl_refl intro: rtrancl_trans)
+  apply (blast del: rtrancl.rtrancl_refl intro: rtrancl_trans')
   done
 
 
@@ -144,44 +142,44 @@
 text {* Proof by Stefan Berghofer *}
 
 theorem newman:
-  assumes wf: "wf (R\<inverse>)"
-  and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
-    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
-  shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
-    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
+  assumes wf: "wfP (R\<inverse>\<inverse>)"
+  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
+    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
+  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
+    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   using wf
 proof induct
   case (less x b c)
-  have xc: "(x, c) \<in> R\<^sup>*" .
-  have xb: "(x, b) \<in> R\<^sup>*" . thus ?case
-  proof (rule converse_rtranclE)
+  have xc: "R\<^sup>*\<^sup>* x c" .
+  have xb: "R\<^sup>*\<^sup>* x b" . thus ?case
+  proof (rule converse_rtranclE')
     assume "x = b"
-    with xc have "(b, c) \<in> R\<^sup>*" by simp
+    with xc have "R\<^sup>*\<^sup>* b c" by simp
     thus ?thesis by iprover
   next
     fix y
-    assume xy: "(x, y) \<in> R"
-    assume yb: "(y, b) \<in> R\<^sup>*"
+    assume xy: "R x y"
+    assume yb: "R\<^sup>*\<^sup>* y b"
     from xc show ?thesis
-    proof (rule converse_rtranclE)
+    proof (rule converse_rtranclE')
       assume "x = c"
-      with xb have "(c, b) \<in> R\<^sup>*" by simp
+      with xb have "R\<^sup>*\<^sup>* c b" by simp
       thus ?thesis by iprover
     next
       fix y'
-      assume y'c: "(y', c) \<in> R\<^sup>*"
-      assume xy': "(x, y') \<in> R"
-      with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
-      then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by iprover
-      from xy have "(y, x) \<in> R\<inverse>" ..
-      from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
-      then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by iprover
-      from xy' have "(y', x) \<in> R\<inverse>" ..
-      moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
+      assume y'c: "R\<^sup>*\<^sup>* y' c"
+      assume xy': "R x y'"
+      with xy have "\<exists>u. R\<^sup>*\<^sup>* y u \<and> R\<^sup>*\<^sup>* y' u" by (rule lc)
+      then obtain u where yu: "R\<^sup>*\<^sup>* y u" and y'u: "R\<^sup>*\<^sup>* y' u" by iprover
+      from xy have "R\<inverse>\<inverse> y x" ..
+      from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
+      then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
+      from xy' have "R\<inverse>\<inverse> y' x" ..
+      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtrancl_trans')
       moreover note y'c
-      ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
-      then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by iprover
-      from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
+      ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
+      then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
+      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtrancl_trans')
       with cw show ?thesis by iprover
     qed
   qed
@@ -195,42 +193,42 @@
 *}
 
 theorem newman':
-  assumes wf: "wf (R\<inverse>)"
-  and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
-    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
-  shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
-    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
+  assumes wf: "wfP (R\<inverse>\<inverse>)"
+  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
+    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
+  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
+    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   using wf
 proof induct
   case (less x b c)
-  note IH = `\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
-                     \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*`
-  have xc: "(x, c) \<in> R\<^sup>*" .
-  have xb: "(x, b) \<in> R\<^sup>*" .
+  note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
+                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
+  have xc: "R\<^sup>*\<^sup>* x c" .
+  have xb: "R\<^sup>*\<^sup>* x b" .
   thus ?case
-  proof (rule converse_rtranclE)
+  proof (rule converse_rtranclE')
     assume "x = b"
-    with xc have "(b, c) \<in> R\<^sup>*" by simp
+    with xc have "R\<^sup>*\<^sup>* b c" by simp
     thus ?thesis by iprover
   next
     fix y
-    assume xy: "(x, y) \<in> R"
-    assume yb: "(y, b) \<in> R\<^sup>*"
+    assume xy: "R x y"
+    assume yb: "R\<^sup>*\<^sup>* y b"
     from xc show ?thesis
-    proof (rule converse_rtranclE)
+    proof (rule converse_rtranclE')
       assume "x = c"
-      with xb have "(c, b) \<in> R\<^sup>*" by simp
+      with xb have "R\<^sup>*\<^sup>* c b" by simp
       thus ?thesis by iprover
     next
       fix y'
-      assume y'c: "(y', c) \<in> R\<^sup>*"
-      assume xy': "(x, y') \<in> R"
-      with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
+      assume y'c: "R\<^sup>*\<^sup>* y' c"
+      assume xy': "R x y'"
+      with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
         by (blast dest: lc)
       from yb u y'c show ?thesis
-        by (blast del: rtrancl_refl
-            intro: rtrancl_trans
-            dest: IH [OF xy [symmetric]] IH [OF xy' [symmetric]])
+        by (blast del: rtrancl.rtrancl_refl
+            intro: rtrancl_trans'
+            dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
     qed
   qed
 qed
diff -r 7c1e65897693 -r 4ccb7e6be929 src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Wed Feb 07 17:39:49 2007 +0100
+++ b/src/HOL/Lambda/ListOrder.thy	Wed Feb 07 17:41:11 2007 +0100
@@ -14,36 +14,35 @@
 *}
 
 definition
-  step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
+  step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where
   "step1 r =
-    {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys =
-      us @ z' # vs}"
+    (\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys =
+      us @ z' # vs)"
 
 
-lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1"
+lemma step1_converse [simp]: "step1 (r^--1) = (step1 r)^--1"
+  apply (unfold step1_def)
+  apply (blast intro!: order_antisym)
+  done
+
+lemma in_step1_converse [iff]: "(step1 (r^--1) x y) = ((step1 r)^--1 x y)"
+  apply auto
+  done
+
+lemma not_Nil_step1 [iff]: "\<not> step1 r [] xs"
   apply (unfold step1_def)
   apply blast
   done
 
-lemma in_step1_converse [iff]: "(p \<in> step1 (r^-1)) = (p \<in> (step1 r)^-1)"
-  apply auto
-  done
-
-lemma not_Nil_step1 [iff]: "([], xs) \<notin> step1 r"
-  apply (unfold step1_def)
-  apply blast
-  done
-
-lemma not_step1_Nil [iff]: "(xs, []) \<notin> step1 r"
+lemma not_step1_Nil [iff]: "\<not> step1 r xs []"
   apply (unfold step1_def)
   apply blast
   done
 
 lemma Cons_step1_Cons [iff]:
-    "((y # ys, x # xs) \<in> step1 r) =
-      ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
+    "(step1 r (y # ys) (x # xs)) =
+      (r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)"
   apply (unfold step1_def)
-  apply simp
   apply (rule iffI)
    apply (erule exE)
    apply (rename_tac ts)
@@ -56,8 +55,8 @@
   done
 
 lemma append_step1I:
-  "(ys, xs) \<in> step1 r \<and> vs = us \<or> ys = xs \<and> (vs, us) \<in> step1 r
-    ==> (ys @ vs, xs @ us) : step1 r"
+  "step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us
+    ==> step1 r (ys @ vs) (xs @ us)"
   apply (unfold step1_def)
   apply auto
    apply blast
@@ -65,9 +64,9 @@
   done
 
 lemma Cons_step1E [elim!]:
-  assumes "(ys, x # xs) \<in> step1 r"
-    and "!!y. ys = y # xs \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> R"
-    and "!!zs. ys = x # zs \<Longrightarrow> (zs, xs) \<in> step1 r \<Longrightarrow> R"
+  assumes "step1 r ys (x # xs)"
+    and "!!y. ys = y # xs \<Longrightarrow> r y x \<Longrightarrow> R"
+    and "!!zs. ys = x # zs \<Longrightarrow> step1 r zs xs \<Longrightarrow> R"
   shows R
   using prems
   apply (cases ys)
@@ -76,10 +75,9 @@
   done
 
 lemma Snoc_step1_SnocD:
-  "(ys @ [y], xs @ [x]) \<in> step1 r
-    ==> ((ys, xs) \<in> step1 r \<and> y = x \<or> ys = xs \<and> (y, x) \<in> r)"
+  "step1 r (ys @ [y]) (xs @ [x])
+    ==> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)"
   apply (unfold step1_def)
-  apply simp
   apply (clarify del: disjCI)
   apply (rename_tac vs)
   apply (rule_tac xs = vs in rev_exhaust)
@@ -89,7 +87,7 @@
   done
 
 lemma Cons_acc_step1I [intro!]:
-    "x \<in> acc r ==> xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r)"
+    "acc r x ==> acc (step1 r) xs \<Longrightarrow> acc (step1 r) (x # xs)"
   apply (induct arbitrary: xs set: acc)
   apply (erule thin_rl)
   apply (erule acc_induct)
@@ -97,8 +95,8 @@
   apply blast
   done
 
-lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)"
-  apply (induct set: lists)
+lemma lists_accD: "listsp (acc r) xs ==> acc (step1 r) xs"
+  apply (induct set: listsp)
    apply (rule accI)
    apply simp
   apply (rule accI)
@@ -106,18 +104,18 @@
   done
 
 lemma ex_step1I:
-  "[| x \<in> set xs; (y, x) \<in> r |]
-    ==> \<exists>ys. (ys, xs) \<in> step1 r \<and> y \<in> set ys"
+  "[| x \<in> set xs; r y x |]
+    ==> \<exists>ys. step1 r ys xs \<and> y \<in> set ys"
   apply (unfold step1_def)
   apply (drule in_set_conv_decomp [THEN iffD1])
   apply force
   done
 
-lemma lists_accI: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)"
+lemma lists_accI: "acc (step1 r) xs ==> listsp (acc r) xs"
   apply (induct set: acc)
   apply clarify
   apply (rule accI)
-  apply (drule ex_step1I, assumption)
+  apply (drule_tac r=r in ex_step1I, assumption)
   apply blast
   done
 
diff -r 7c1e65897693 -r 4ccb7e6be929 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Feb 07 17:39:49 2007 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Feb 07 17:41:11 2007 +0100
@@ -381,28 +381,28 @@
 subsubsection {* Well-foundedness *}
 
 definition
-  mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
+  mult1 :: "('a => 'a => bool) => 'a multiset => 'a multiset => bool" where
   "mult1 r =
-    {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
-      (\<forall>b. b :# K --> (b, a) \<in> r)}"
+    (%N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
+      (\<forall>b. b :# K --> r b a))"
 
 definition
-  mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
-  "mult r = (mult1 r)\<^sup>+"
+  mult :: "('a => 'a => bool) => 'a multiset => 'a multiset => bool" where
+  "mult r = (mult1 r)\<^sup>+\<^sup>+"
 
-lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
+lemma not_less_empty [iff]: "\<not> mult1 r M {#}"
   by (simp add: mult1_def)
 
-lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==>
-    (\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
-    (\<exists>K. (\<forall>b. b :# K --> (b, a) \<in> r) \<and> N = M0 + K)"
+lemma less_add: "mult1 r N (M0 + {#a#})==>
+    (\<exists>M. mult1 r M M0 \<and> N = M + {#a#}) \<or>
+    (\<exists>K. (\<forall>b. b :# K --> r b a) \<and> N = M0 + K)"
   (is "_ \<Longrightarrow> ?case1 (mult1 r) \<or> ?case2")
 proof (unfold mult1_def)
-  let ?r = "\<lambda>K a. \<forall>b. b :# K --> (b, a) \<in> r"
+  let ?r = "\<lambda>K a. \<forall>b. b :# K --> r b a"
   let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a"
-  let ?case1 = "?case1 {(N, M). ?R N M}"
+  let ?case1 = "?case1 ?R"
 
-  assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}"
+  assume "?R N (M0 + {#a#})"
   then have "\<exists>a' M0' K.
       M0 + {#a#} = M0' + {#a'#} \<and> N = M0' + K \<and> ?r K a'" by simp
   then show "?case1 \<or> ?case2"
@@ -430,80 +430,80 @@
   qed
 qed
 
-lemma all_accessible: "wf r ==> \<forall>M. M \<in> acc (mult1 r)"
+lemma all_accessible: "wfP r ==> \<forall>M. acc (mult1 r) M"
 proof
   let ?R = "mult1 r"
   let ?W = "acc ?R"
   {
     fix M M0 a
-    assume M0: "M0 \<in> ?W"
-      and wf_hyp: "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
-      and acc_hyp: "\<forall>M. (M, M0) \<in> ?R --> M + {#a#} \<in> ?W"
-    have "M0 + {#a#} \<in> ?W"
-    proof (rule accI [of "M0 + {#a#}"])
+    assume M0: "?W M0"
+      and wf_hyp: "!!b. r b a ==> \<forall>M \<triangleright> ?W. ?W (M + {#b#})"
+      and acc_hyp: "\<forall>M. ?R M M0 --> ?W (M + {#a#})"
+    have "?W (M0 + {#a#})"
+    proof (rule accI [of _ "M0 + {#a#}"])
       fix N
-      assume "(N, M0 + {#a#}) \<in> ?R"
-      then have "((\<exists>M. (M, M0) \<in> ?R \<and> N = M + {#a#}) \<or>
-          (\<exists>K. (\<forall>b. b :# K --> (b, a) \<in> r) \<and> N = M0 + K))"
+      assume "?R N (M0 + {#a#})"
+      then have "((\<exists>M. ?R M M0 \<and> N = M + {#a#}) \<or>
+          (\<exists>K. (\<forall>b. b :# K --> r b a) \<and> N = M0 + K))"
         by (rule less_add)
-      then show "N \<in> ?W"
+      then show "?W N"
       proof (elim exE disjE conjE)
-        fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}"
-        from acc_hyp have "(M, M0) \<in> ?R --> M + {#a#} \<in> ?W" ..
-        then have "M + {#a#} \<in> ?W" ..
-        then show "N \<in> ?W" by (simp only: N)
+        fix M assume "?R M M0" and N: "N = M + {#a#}"
+        from acc_hyp have "?R M M0 --> ?W (M + {#a#})" ..
+        then have "?W (M + {#a#})" ..
+        then show "?W N" by (simp only: N)
       next
         fix K
         assume N: "N = M0 + K"
-        assume "\<forall>b. b :# K --> (b, a) \<in> r"
-        then have "M0 + K \<in> ?W"
+        assume "\<forall>b. b :# K --> r b a"
+        then have "?W (M0 + K)"
         proof (induct K)
           case empty
-          from M0 show "M0 + {#} \<in> ?W" by simp
+          from M0 show "?W (M0 + {#})" by simp
         next
           case (add K x)
-          from add.prems have "(x, a) \<in> r" by simp
-          with wf_hyp have "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast
-          moreover from add have "M0 + K \<in> ?W" by simp
-          ultimately have "(M0 + K) + {#x#} \<in> ?W" ..
-          then show "M0 + (K + {#x#}) \<in> ?W" by (simp only: union_assoc)
+          from add.prems have "r x a" by simp
+          with wf_hyp have "\<forall>M \<triangleright> ?W. ?W (M + {#x#})" by blast
+          moreover from add have "?W (M0 + K)" by simp
+          ultimately have "?W ((M0 + K) + {#x#})" ..
+          then show "?W (M0 + (K + {#x#}))" by (simp only: union_assoc)
         qed
-        then show "N \<in> ?W" by (simp only: N)
+        then show "?W N" by (simp only: N)
       qed
     qed
   } note tedious_reasoning = this
 
-  assume wf: "wf r"
+  assume wf: "wfP r"
   fix M
-  show "M \<in> ?W"
+  show "?W M"
   proof (induct M)
-    show "{#} \<in> ?W"
+    show "?W {#}"
     proof (rule accI)
-      fix b assume "(b, {#}) \<in> ?R"
-      with not_less_empty show "b \<in> ?W" by contradiction
+      fix b assume "?R b {#}"
+      with not_less_empty show "?W b" by contradiction
     qed
 
-    fix M a assume "M \<in> ?W"
-    from wf have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
+    fix M a assume "?W M"
+    from wf have "\<forall>M \<triangleright> ?W. ?W (M + {#a#})"
     proof induct
       fix a
-      assume "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
-      show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
+      assume "!!b. r b a ==> \<forall>M \<triangleright> ?W. ?W (M + {#b#})"
+      show "\<forall>M \<triangleright> ?W. ?W (M + {#a#})"
       proof
-        fix M assume "M \<in> ?W"
-        then show "M + {#a#} \<in> ?W"
+        fix M assume "?W M"
+        then show "?W (M + {#a#})"
           by (rule acc_induct) (rule tedious_reasoning)
       qed
     qed
-    then show "M + {#a#} \<in> ?W" ..
+    then show "?W (M + {#a#})" ..
   qed
 qed
 
-theorem wf_mult1: "wf r ==> wf (mult1 r)"
+theorem wf_mult1: "wfP r ==> wfP (mult1 r)"
   by (rule acc_wfI, rule all_accessible)
 
-theorem wf_mult: "wf r ==> wf (mult r)"
-  by (unfold mult_def, rule wf_trancl, rule wf_mult1)
+theorem wf_mult: "wfP r ==> wfP (mult r)"
+  by (unfold mult_def, rule wfP_trancl, rule wf_mult1)
 
 
 subsubsection {* Closure-free presentation *}
@@ -516,16 +516,16 @@
 text {* One direction. *}
 
 lemma mult_implies_one_step:
-  "trans r ==> (M, N) \<in> mult r ==>
+  "transP r ==> mult r M N ==>
     \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
-    (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
+    (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. r k j)"
   apply (unfold mult_def mult1_def set_of_def)
-  apply (erule converse_trancl_induct, clarify)
+  apply (erule converse_trancl_induct', clarify)
    apply (rule_tac x = M0 in exI, simp, clarify)
-  apply (case_tac "a :# K")
+  apply (case_tac "a :# Ka")
    apply (rule_tac x = I in exI)
    apply (simp (no_asm))
-   apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
+   apply (rule_tac x = "(Ka - {#a#}) + K" in exI)
    apply (simp (no_asm_simp) add: union_assoc [symmetric])
    apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
    apply (simp add: diff_union_single_conv)
@@ -556,30 +556,29 @@
   done
 
 lemma one_step_implies_mult_aux:
-  "trans r ==>
-    \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r))
-      --> (I + K, I + J) \<in> mult r"
+  "\<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. r k j))
+    --> mult r (I + K) (I + J)"
   apply (induct_tac n, auto)
   apply (frule size_eq_Suc_imp_eq_union, clarify)
   apply (rename_tac "J'", simp)
   apply (erule notE, auto)
   apply (case_tac "J' = {#}")
    apply (simp add: mult_def)
-   apply (rule r_into_trancl)
+   apply (rule trancl.r_into_trancl)
    apply (simp add: mult1_def set_of_def, blast)
   txt {* Now we know @{term "J' \<noteq> {#}"}. *}
-  apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
+  apply (cut_tac M = K and P = "\<lambda>x. r x a" in multiset_partition)
   apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
   apply (erule ssubst)
   apply (simp add: Ball_def, auto)
   apply (subgoal_tac
-    "((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #},
-      (I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r")
+    "mult r ((I + {# x : K. r x a #}) + {# x : K. \<not> r x a #})
+      ((I + {# x : K. r x a #}) + J')")
    prefer 2
    apply force
   apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
-  apply (erule trancl_trans)
-  apply (rule r_into_trancl)
+  apply (erule trancl_trans')
+  apply (rule trancl.r_into_trancl)
   apply (simp add: mult1_def set_of_def)
   apply (rule_tac x = a in exI)
   apply (rule_tac x = "I + J'" in exI)
@@ -587,8 +586,8 @@
   done
 
 lemma one_step_implies_mult:
-  "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
-    ==> (I + K, I + J) \<in> mult r"
+  "J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. r k j
+    ==> mult r (I + K) (I + J)"
   apply (insert one_step_implies_mult_aux, blast)
   done
 
@@ -598,10 +597,10 @@
 instance multiset :: (type) ord ..
 
 defs (overloaded)
-  less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"
+  less_multiset_def: "op < == mult op <"
   le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"
 
-lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
+lemma trans_base_order: "transP (op < :: 'a::order => 'a => bool)"
   unfolding trans_def by (blast intro: order_less_trans)
 
 text {*
@@ -629,7 +628,7 @@
 
 theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)"
   apply (unfold less_multiset_def mult_def)
-  apply (blast intro: trancl_trans)
+  apply (blast intro: trancl_trans')
   done
 
 text {* Asymmetry. *}
@@ -676,7 +675,7 @@
 subsubsection {* Monotonicity of multiset union *}
 
 lemma mult1_union:
-    "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
+    "mult1 r B D ==> mult1 r (C + B) (C + D)"
   apply (unfold mult1_def, auto)
   apply (rule_tac x = a in exI)
   apply (rule_tac x = "C + M0" in exI)
@@ -685,9 +684,9 @@
 
 lemma union_less_mono2: "B < D ==> C + B < C + (D::'a::order multiset)"
   apply (unfold less_multiset_def mult_def)
-  apply (erule trancl_induct)
-   apply (blast intro: mult1_union transI order_less_trans r_into_trancl)
-  apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans)
+  apply (erule trancl_induct')
+   apply (blast intro: mult1_union)
+  apply (blast intro: mult1_union trancl.r_into_trancl trancl_trans')
   done
 
 lemma union_less_mono1: "B < D ==> B + C < D + (C::'a::order multiset)"
@@ -710,10 +709,10 @@
   apply (unfold le_multiset_def less_multiset_def)
   apply (case_tac "M = {#}")
    prefer 2
-   apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
+   apply (subgoal_tac "mult op < ({#} + {#}) ({#} + M)")
     prefer 2
     apply (rule one_step_implies_mult)
-      apply (simp only: trans_def, auto)
+      apply auto
   done
 
 lemma union_upper1: "A <= A + (B::'a::order multiset)"