# HG changeset patch
# User berghofe
# Date 1184145876 -7200
# Node ID a7c7edf2c5ad5e9b52e2e6ef074b7419aaead15c
# Parent  a1db5f819d005f0048ca4a006e7a6a9fa697d06e
Restored set notation.

diff -r a1db5f819d00 -r a7c7edf2c5ad src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Jul 11 11:23:24 2007 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Jul 11 11:24:36 2007 +0200
@@ -386,28 +386,28 @@
 subsubsection {* Well-foundedness *}
 
 definition
-  mult1 :: "('a => 'a => bool) => 'a multiset => 'a multiset => bool" where
+  mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
   "mult1 r =
-    (%N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
-      (\<forall>b. b :# K --> r b a))"
+    {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
+      (\<forall>b. b :# K --> (b, a) \<in> r)}"
 
 definition
-  mult :: "('a => 'a => bool) => 'a multiset => 'a multiset => bool" where
-  "mult r = (mult1 r)\<^sup>+\<^sup>+"
+  mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
+  "mult r = (mult1 r)\<^sup>+"
 
-lemma not_less_empty [iff]: "\<not> mult1 r M {#}"
+lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
   by (simp add: mult1_def)
 
-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)"
+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)"
   (is "_ \<Longrightarrow> ?case1 (mult1 r) \<or> ?case2")
 proof (unfold mult1_def)
-  let ?r = "\<lambda>K a. \<forall>b. b :# K --> r b a"
+  let ?r = "\<lambda>K a. \<forall>b. b :# K --> (b, a) \<in> r"
   let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a"
-  let ?case1 = "?case1 ?R"
+  let ?case1 = "?case1 {(N, M). ?R N M}"
 
-  assume "?R N (M0 + {#a#})"
+  assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}"
   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"
@@ -435,80 +435,80 @@
   qed
 qed
 
-lemma all_accessible: "wfP r ==> \<forall>M. acc (mult1 r) M"
+lemma all_accessible: "wf r ==> \<forall>M. M \<in> acc (mult1 r)"
 proof
   let ?R = "mult1 r"
   let ?W = "acc ?R"
   {
     fix M 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#}"])
+    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#}"])
       fix N
-      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))"
+      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))"
         by (rule less_add)
-      then show "?W N"
+      then show "N \<in> ?W"
       proof (elim exE disjE conjE)
-        fix M assume "?R M M0" and N: "N = M + {#a#}"
-        from acc_hyp have "?R M M0 --> ?W (M + {#a#})" ..
-        from this and `?R M M0` have "?W (M + {#a#})" ..
-        then show "?W N" by (simp only: N)
+        fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}"
+        from acc_hyp have "(M, M0) \<in> ?R --> M + {#a#} \<in> ?W" ..
+        from this and `(M, M0) \<in> ?R` have "M + {#a#} \<in> ?W" ..
+        then show "N \<in> ?W" by (simp only: N)
       next
         fix K
         assume N: "N = M0 + K"
-        assume "\<forall>b. b :# K --> r b a"
-        then have "?W (M0 + K)"
+        assume "\<forall>b. b :# K --> (b, a) \<in> r"
+        then have "M0 + K \<in> ?W"
         proof (induct K)
           case empty
-          from M0 show "?W (M0 + {#})" by simp
+          from M0 show "M0 + {#} \<in> ?W" by simp
         next
           case (add K x)
-          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)
+          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)
         qed
-        then show "?W N" by (simp only: N)
+        then show "N \<in> ?W" by (simp only: N)
       qed
     qed
   } note tedious_reasoning = this
 
-  assume wf: "wfP r"
+  assume wf: "wf r"
   fix M
-  show "?W M"
+  show "M \<in> ?W"
   proof (induct M)
-    show "?W {#}"
+    show "{#} \<in> ?W"
     proof (rule accI)
-      fix b assume "?R b {#}"
-      with not_less_empty show "?W b" by contradiction
+      fix b assume "(b, {#}) \<in> ?R"
+      with not_less_empty show "b \<in> ?W" by contradiction
     qed
 
-    fix M a assume "?W M"
-    from wf have "\<forall>M \<triangleright> ?W. ?W (M + {#a#})"
+    fix M a assume "M \<in> ?W"
+    from wf have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
     proof induct
       fix a
-      assume r: "!!b. r b a ==> \<forall>M \<triangleright> ?W. ?W (M + {#b#})"
-      show "\<forall>M \<triangleright> ?W. ?W (M + {#a#})"
+      assume r: "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
+      show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
       proof
-        fix M assume "?W M"
-        then show "?W (M + {#a#})"
+        fix M assume "M \<in> ?W"
+        then show "M + {#a#} \<in> ?W"
           by (rule acc_induct) (rule tedious_reasoning [OF _ r])
       qed
     qed
-    from this and `?W M` show "?W (M + {#a#})" ..
+    from this and `M \<in> ?W` show "M + {#a#} \<in> ?W" ..
   qed
 qed
 
-theorem wf_mult1: "wfP r ==> wfP (mult1 r)"
+theorem wf_mult1: "wf r ==> wf (mult1 r)"
   by (rule acc_wfI) (rule all_accessible)
 
-theorem wf_mult: "wfP r ==> wfP (mult r)"
-  unfolding mult_def by (rule wfP_trancl) (rule wf_mult1)
+theorem wf_mult: "wf r ==> wf (mult r)"
+  unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
 
 
 subsubsection {* Closure-free presentation *}
@@ -521,16 +521,16 @@
 text {* One direction. *}
 
 lemma mult_implies_one_step:
-  "transP r ==> mult r M N ==>
+  "trans r ==> (M, N) \<in> mult r ==>
     \<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. r k j)"
+    (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
   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 :# Ka")
+  apply (case_tac "a :# K")
    apply (rule_tac x = I in exI)
    apply (simp (no_asm))
-   apply (rule_tac x = "(Ka - {#a#}) + K" in exI)
+   apply (rule_tac x = "(K - {#a#}) + Ka" 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)
@@ -561,29 +561,30 @@
   done
 
 lemma one_step_implies_mult_aux:
-  "\<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)"
+  "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"
   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 trancl.r_into_trancl)
+   apply (rule 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. r x a" in multiset_partition)
+  apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" 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
-    "mult r ((I + {# x : K. r x a #}) + {# x : K. \<not> r x a #})
-      ((I + {# x : K. r x a #}) + J')")
+    "((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #},
+      (I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r")
    prefer 2
    apply force
   apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
-  apply (erule trancl_trans')
-  apply (rule trancl.r_into_trancl)
+  apply (erule trancl_trans)
+  apply (rule 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)
@@ -591,8 +592,8 @@
   done
 
 lemma one_step_implies_mult:
-  "J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. r k j
-    ==> mult r (I + K) (I + J)"
+  "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"
   using one_step_implies_mult_aux by blast
 
 
@@ -601,10 +602,10 @@
 instance multiset :: (type) ord ..
 
 defs (overloaded)
-  less_multiset_def: "op < == mult op <"
+  less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"
   le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"
 
-lemma trans_base_order: "transP (op < :: 'a::order => 'a => bool)"
+lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
   unfolding trans_def by (blast intro: order_less_trans)
 
 text {*
@@ -629,7 +630,7 @@
 text {* Transitivity. *}
 
 theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)"
-  unfolding less_multiset_def mult_def by (blast intro: trancl_trans')
+  unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
 
 text {* Asymmetry. *}
 
@@ -665,17 +666,17 @@
 
 instance multiset :: (order) order
   apply intro_classes
-    apply (rule mult_less_le)
-    apply (rule mult_le_refl)
-    apply (erule mult_le_trans, assumption)
-    apply (erule mult_le_antisym, assumption)
+  apply (rule mult_less_le)
+  apply (rule mult_le_refl)
+  apply (erule mult_le_trans, assumption)
+  apply (erule mult_le_antisym, assumption)
   done
 
 
 subsubsection {* Monotonicity of multiset union *}
 
 lemma mult1_union:
-    "mult1 r B D ==> mult1 r (C + B) (C + D)"
+    "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
   apply (unfold mult1_def, auto)
   apply (rule_tac x = a in exI)
   apply (rule_tac x = "C + M0" in exI)
@@ -684,9 +685,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)
-  apply (blast intro: mult1_union trancl.r_into_trancl trancl_trans')
+  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)
   done
 
 lemma union_less_mono1: "B < D ==> B + C < D + (C::'a::order multiset)"
@@ -709,10 +710,10 @@
   apply (unfold le_multiset_def less_multiset_def)
   apply (case_tac "M = {#}")
    prefer 2
-   apply (subgoal_tac "mult op < ({#} + {#}) ({#} + M)")
+   apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
     prefer 2
     apply (rule one_step_implies_mult)
-      apply auto
+      apply (simp only: trans_def, auto)
   done
 
 lemma union_upper1: "A <= A + (B::'a::order multiset)"