src/HOL/Library/Multiset.thy
changeset 60607 d440af2e584f
parent 60606 e5cb9271e339
child 60608 c5cbd90bd94e
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Jun 29 15:36:29 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Jun 29 15:41:16 2015 +0200
     1.3 @@ -305,7 +305,7 @@
     1.4  lemma mset_le_add_right [simp]: "B \<le># (A::'a multiset) + B"
     1.5    unfolding subseteq_mset_def by auto
     1.6  
     1.7 -lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B"
     1.8 +lemma mset_le_single: "a \<in># B \<Longrightarrow> {#a#} \<le># B"
     1.9    by (simp add: subseteq_mset_def)
    1.10  
    1.11  lemma multiset_diff_union_assoc:
    1.12 @@ -510,7 +510,7 @@
    1.13  subsubsection \<open>Set of elements\<close>
    1.14  
    1.15  definition set_mset :: "'a multiset \<Rightarrow> 'a set"
    1.16 -  where "set_mset M = {x. x :# M}"
    1.17 +  where "set_mset M = {x. x \<in># M}"
    1.18  
    1.19  lemma set_mset_empty [simp]: "set_mset {#} = {}"
    1.20  by (simp add: set_mset_def)
    1.21 @@ -524,16 +524,16 @@
    1.22  lemma set_mset_eq_empty_iff [simp]: "(set_mset M = {}) = (M = {#})"
    1.23  by (auto simp add: set_mset_def multiset_eq_iff)
    1.24  
    1.25 -lemma mem_set_mset_iff [simp]: "(x \<in> set_mset M) = (x :# M)"
    1.26 +lemma mem_set_mset_iff [simp]: "(x \<in> set_mset M) = (x \<in># M)"
    1.27  by (auto simp add: set_mset_def)
    1.28  
    1.29 -lemma set_mset_filter [simp]: "set_mset {# x:#M. P x #} = set_mset M \<inter> {x. P x}"
    1.30 +lemma set_mset_filter [simp]: "set_mset {# x\<in>#M. P x #} = set_mset M \<inter> {x. P x}"
    1.31  by (auto simp add: set_mset_def)
    1.32  
    1.33  lemma finite_set_mset [iff]: "finite (set_mset M)"
    1.34    using count [of M] by (simp add: multiset_def set_mset_def)
    1.35  
    1.36 -lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
    1.37 +lemma finite_Collect_mem [iff]: "finite {x. x \<in># M}"
    1.38    unfolding set_mset_def[symmetric] by simp
    1.39  
    1.40  lemma set_mset_mono: "A \<le># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
    1.41 @@ -605,7 +605,7 @@
    1.42  lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
    1.43  by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
    1.44  
    1.45 -lemma size_eq_Suc_imp_elem: "size M = Suc n \<Longrightarrow> \<exists>a. a :# M"
    1.46 +lemma size_eq_Suc_imp_elem: "size M = Suc n \<Longrightarrow> \<exists>a. a \<in># M"
    1.47  apply (unfold size_multiset_overloaded_eq)
    1.48  apply (drule setsum_SucD)
    1.49  apply auto
    1.50 @@ -665,7 +665,7 @@
    1.51  lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
    1.52  by (cases "B = {#}") (auto dest: multi_member_split)
    1.53  
    1.54 -lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
    1.55 +lemma multiset_partition: "M = {# x\<in>#M. P x #} + {# x\<in>#M. \<not> P x #}"
    1.56  apply (subst multiset_eq_iff)
    1.57  apply auto
    1.58  done
    1.59 @@ -816,9 +816,9 @@
    1.60  subsection \<open>Image\<close>
    1.61  
    1.62  definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
    1.63 -  "image_mset f = fold_mset (plus o single o f) {#}"
    1.64 -
    1.65 -lemma comp_fun_commute_mset_image: "comp_fun_commute (plus o single o f)"
    1.66 +  "image_mset f = fold_mset (plus \<circ> single \<circ> f) {#}"
    1.67 +
    1.68 +lemma comp_fun_commute_mset_image: "comp_fun_commute (plus \<circ> single \<circ> f)"
    1.69  proof
    1.70  qed (simp add: ac_simps fun_eq_iff)
    1.71  
    1.72 @@ -827,14 +827,14 @@
    1.73  
    1.74  lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
    1.75  proof -
    1.76 -  interpret comp_fun_commute "plus o single o f"
    1.77 +  interpret comp_fun_commute "plus \<circ> single \<circ> f"
    1.78      by (fact comp_fun_commute_mset_image)
    1.79    show ?thesis by (simp add: image_mset_def)
    1.80  qed
    1.81  
    1.82  lemma image_mset_union [simp]: "image_mset f (M + N) = image_mset f M + image_mset f N"
    1.83  proof -
    1.84 -  interpret comp_fun_commute "plus o single o f"
    1.85 +  interpret comp_fun_commute "plus \<circ> single \<circ> f"
    1.86      by (fact comp_fun_commute_mset_image)
    1.87    show ?thesis by (induct N) (simp_all add: image_mset_def ac_simps)
    1.88  qed
    1.89 @@ -876,10 +876,10 @@
    1.90    "{#e | x\<in>#M. P#}" \<rightharpoonup> "{#e. x \<in># {# x\<in>#M. P#}#}"
    1.91  
    1.92  text \<open>
    1.93 -  This allows to write not just filters like @{term "{#x:#M. x<c#}"}
    1.94 -  but also images like @{term "{#x+x. x:#M #}"} and @{term [source]
    1.95 -  "{#x+x|x:#M. x<c#}"}, where the latter is currently displayed as
    1.96 -  @{term "{#x+x|x:#M. x<c#}"}.
    1.97 +  This allows to write not just filters like @{term "{#x\<in>#M. x<c#}"}
    1.98 +  but also images like @{term "{#x+x. x\<in>#M #}"} and @{term [source]
    1.99 +  "{#x+x|x\<in>#M. x<c#}"}, where the latter is currently displayed as
   1.100 +  @{term "{#x+x|x\<in>#M. x<c#}"}.
   1.101  \<close>
   1.102  
   1.103  lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
   1.104 @@ -939,7 +939,7 @@
   1.105  lemma set_mset_mset[simp]: "set_mset (mset x) = set x"
   1.106  by (induct x) auto
   1.107  
   1.108 -lemma mem_set_multiset_eq: "x \<in> set xs = (x :# mset xs)"
   1.109 +lemma mem_set_multiset_eq: "x \<in> set xs = (x \<in># mset xs)"
   1.110  by (induct xs) auto
   1.111  
   1.112  lemma size_mset [simp]: "size (mset xs) = length xs"
   1.113 @@ -948,7 +948,7 @@
   1.114  lemma mset_append [simp]: "mset (xs @ ys) = mset xs + mset ys"
   1.115    by (induct xs arbitrary: ys) (auto simp: ac_simps)
   1.116  
   1.117 -lemma mset_filter: "mset (filter P xs) = {#x :# mset xs. P x #}"
   1.118 +lemma mset_filter: "mset (filter P xs) = {#x \<in># mset xs. P x #}"
   1.119    by (induct xs) simp_all
   1.120  
   1.121  lemma mset_rev [simp]:
   1.122 @@ -997,7 +997,7 @@
   1.123  lemma mset_compl_union [simp]: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
   1.124    by (induct xs) (auto simp: ac_simps)
   1.125  
   1.126 -lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) :# mset ls"
   1.127 +lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
   1.128  apply (induct ls arbitrary: i)
   1.129   apply simp
   1.130  apply (case_tac i)
   1.131 @@ -1501,7 +1501,7 @@
   1.132  
   1.133  definition mult1 :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
   1.134    "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
   1.135 -      (\<forall>b. b :# K \<longrightarrow> (b, a) \<in> r)}"
   1.136 +      (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r)}"
   1.137  
   1.138  definition mult :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
   1.139    "mult r = (mult1 r)\<^sup>+"
   1.140 @@ -1511,10 +1511,10 @@
   1.141  
   1.142  lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r \<Longrightarrow>
   1.143      (\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
   1.144 -    (\<exists>K. (\<forall>b. b :# K \<longrightarrow> (b, a) \<in> r) \<and> N = M0 + K)"
   1.145 +    (\<exists>K. (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r) \<and> N = M0 + K)"
   1.146    (is "_ \<Longrightarrow> ?case1 (mult1 r) \<or> ?case2")
   1.147  proof (unfold mult1_def)
   1.148 -  let ?r = "\<lambda>K a. \<forall>b. b :# K \<longrightarrow> (b, a) \<in> r"
   1.149 +  let ?r = "\<lambda>K a. \<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r"
   1.150    let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a"
   1.151    let ?case1 = "?case1 {(N, M). ?R N M}"
   1.152  
   1.153 @@ -1556,7 +1556,7 @@
   1.154        fix N
   1.155        assume "(N, M0 + {#a#}) \<in> ?R"
   1.156        then have "((\<exists>M. (M, M0) \<in> ?R \<and> N = M + {#a#}) \<or>
   1.157 -          (\<exists>K. (\<forall>b. b :# K \<longrightarrow> (b, a) \<in> r) \<and> N = M0 + K))"
   1.158 +          (\<exists>K. (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r) \<and> N = M0 + K))"
   1.159          by (rule less_add)
   1.160        then show "N \<in> ?W"
   1.161        proof (elim exE disjE conjE)
   1.162 @@ -1567,7 +1567,7 @@
   1.163        next
   1.164          fix K
   1.165          assume N: "N = M0 + K"
   1.166 -        assume "\<forall>b. b :# K \<longrightarrow> (b, a) \<in> r"
   1.167 +        assume "\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r"
   1.168          then have "M0 + K \<in> ?W"
   1.169          proof (induct K)
   1.170            case empty
   1.171 @@ -1629,7 +1629,7 @@
   1.172  apply (unfold mult_def mult1_def set_mset_def)
   1.173  apply (erule converse_trancl_induct, clarify)
   1.174   apply (rule_tac x = M0 in exI, simp, clarify)
   1.175 -apply (case_tac "a :# K")
   1.176 +apply (case_tac "a \<in># K")
   1.177   apply (rule_tac x = I in exI)
   1.178   apply (simp (no_asm))
   1.179   apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
   1.180 @@ -1638,7 +1638,7 @@
   1.181   apply (simp add: diff_union_single_conv)
   1.182   apply (simp (no_asm_use) add: trans_def)
   1.183   apply blast
   1.184 -apply (subgoal_tac "a :# I")
   1.185 +apply (subgoal_tac "a \<in># I")
   1.186   apply (rule_tac x = "I - {#a#}" in exI)
   1.187   apply (rule_tac x = "J + {#a#}" in exI)
   1.188   apply (rule_tac x = "K + Ka" in exI)
   1.189 @@ -1649,7 +1649,7 @@
   1.190    apply (simp add: multiset_eq_iff split: nat_diff_split)
   1.191   apply (simp (no_asm_use) add: trans_def)
   1.192   apply blast
   1.193 -apply (subgoal_tac "a :# (M0 + {#a#})")
   1.194 +apply (subgoal_tac "a \<in># (M0 + {#a#})")
   1.195   apply simp
   1.196  apply (simp (no_asm))
   1.197  done
   1.198 @@ -1672,8 +1672,8 @@
   1.199  apply (erule ssubst)
   1.200  apply (simp add: Ball_def, auto)
   1.201  apply (subgoal_tac
   1.202 -  "((I + {# x :# K. (x, a) \<in> r #}) + {# x :# K. (x, a) \<notin> r #},
   1.203 -    (I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r")
   1.204 +  "((I + {# x \<in># K. (x, a) \<in> r #}) + {# x \<in># K. (x, a) \<notin> r #},
   1.205 +    (I + {# x \<in># K. (x, a) \<in> r #}) + J') \<in> mult r")
   1.206   prefer 2
   1.207   apply force
   1.208  apply (simp (no_asm_use) add: add.assoc [symmetric] mult_def)