src/HOL/Library/Multiset.thy
author nipkow
Fri, 18 Mar 2016 12:48:00 +0100
changeset 62651 66568c9b8216
parent 62537 7a9aa69f9b38
child 62837 237ef2bab6c7
permissions -rw-r--r--
superfluous premise (noticed by Julian Nagele)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Library/Multiset.thy
15072
4861bf6af0b4 new material courtesy of Norbert Voelker
paulson
parents: 14981
diff changeset
     2
    Author:     Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
55129
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 54868
diff changeset
     3
    Author:     Andrei Popescu, TU Muenchen
59813
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
     4
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
     5
    Author:     Dmitriy Traytel, TU Muenchen
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
     6
    Author:     Mathias Fleury, MPII
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
     7
*)
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
     8
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
     9
section \<open>(Finite) multisets\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    10
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15072
diff changeset
    11
theory Multiset
51599
1559e9266280 optionalized very specific code setup for multisets
haftmann
parents: 51548
diff changeset
    12
imports Main
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15072
diff changeset
    13
begin
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    14
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    15
subsection \<open>The type of multisets\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    16
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    17
definition "multiset = {f :: 'a \<Rightarrow> nat. finite {x. f x > 0}}"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    18
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    19
typedef 'a multiset = "multiset :: ('a \<Rightarrow> nat) set"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    20
  morphisms count Abs_multiset
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45608
diff changeset
    21
  unfolding multiset_def
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    22
proof
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45608
diff changeset
    23
  show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    24
qed
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    25
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
    26
setup_lifting type_definition_multiset
19086
1b3780be6cc2 new-style definitions/abbreviations;
wenzelm
parents: 18730
diff changeset
    27
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    28
lemma multiset_eq_iff: "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
    29
  by (simp only: count_inject [symmetric] fun_eq_iff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    30
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    31
lemma multiset_eqI: "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
    32
  using multiset_eq_iff by auto
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    33
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    34
text \<open>Preservation of the representing set @{term multiset}.\<close>
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    35
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    36
lemma const0_in_multiset: "(\<lambda>a. 0) \<in> multiset"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    37
  by (simp add: multiset_def)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    38
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    39
lemma only1_in_multiset: "(\<lambda>b. if b = a then n else 0) \<in> multiset"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    40
  by (simp add: multiset_def)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    41
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    42
lemma union_preserves_multiset: "M \<in> multiset \<Longrightarrow> N \<in> multiset \<Longrightarrow> (\<lambda>a. M a + N a) \<in> multiset"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    43
  by (simp add: multiset_def)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    44
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    45
lemma diff_preserves_multiset:
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    46
  assumes "M \<in> multiset"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    47
  shows "(\<lambda>a. M a - N a) \<in> multiset"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    48
proof -
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    49
  have "{x. N x < M x} \<subseteq> {x. 0 < M x}"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    50
    by auto
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    51
  with assms show ?thesis
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    52
    by (auto simp add: multiset_def intro: finite_subset)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    53
qed
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    54
41069
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
    55
lemma filter_preserves_multiset:
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    56
  assumes "M \<in> multiset"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    57
  shows "(\<lambda>x. if P x then M x else 0) \<in> multiset"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    58
proof -
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    59
  have "{x. (P x \<longrightarrow> 0 < M x) \<and> P x} \<subseteq> {x. 0 < M x}"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    60
    by auto
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    61
  with assms show ?thesis
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    62
    by (auto simp add: multiset_def intro: finite_subset)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    63
qed
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    64
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    65
lemmas in_multiset = const0_in_multiset only1_in_multiset
41069
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
    66
  union_preserves_multiset diff_preserves_multiset filter_preserves_multiset
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    67
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    68
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    69
subsection \<open>Representing multisets\<close>
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    70
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    71
text \<open>Multiset enumeration\<close>
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    72
48008
846ff14337a4 use transfer method for instance proof
huffman
parents: 47429
diff changeset
    73
instantiation multiset :: (type) cancel_comm_monoid_add
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    74
begin
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    75
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
    76
lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0"
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
    77
by (rule const0_in_multiset)
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    78
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    79
abbreviation Mempty :: "'a multiset" ("{#}") where
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    80
  "Mempty \<equiv> 0"
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    81
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    82
lift_definition plus_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
    83
by (rule union_preserves_multiset)
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    84
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    85
lift_definition minus_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59813
diff changeset
    86
by (rule diff_preserves_multiset)
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59813
diff changeset
    87
48008
846ff14337a4 use transfer method for instance proof
huffman
parents: 47429
diff changeset
    88
instance
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
    89
  by (standard; transfer; simp add: fun_eq_iff)
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    90
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    91
end
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    92
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    93
lift_definition single :: "'a \<Rightarrow> 'a multiset" is "\<lambda>a b. if b = a then 1 else 0"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
    94
by (rule only1_in_multiset)
15869
3aca7f05cd12 intersection
kleing
parents: 15867
diff changeset
    95
26145
95670b6e1fa3 tuned document;
wenzelm
parents: 26143
diff changeset
    96
syntax
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    97
  "_multiset" :: "args \<Rightarrow> 'a multiset"    ("{#(_)#}")
25507
d13468d40131 added {#.,.,...#}
nipkow
parents: 25208
diff changeset
    98
translations
d13468d40131 added {#.,.,...#}
nipkow
parents: 25208
diff changeset
    99
  "{#x, xs#}" == "{#x#} + {#xs#}"
d13468d40131 added {#.,.,...#}
nipkow
parents: 25208
diff changeset
   100
  "{#x#}" == "CONST single x"
d13468d40131 added {#.,.,...#}
nipkow
parents: 25208
diff changeset
   101
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   102
lemma count_empty [simp]: "count {#} a = 0"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   103
  by (simp add: zero_multiset.rep_eq)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   104
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   105
lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   106
  by (simp add: single.rep_eq)
29901
f4b3f8fbf599 finiteness lemmas
nipkow
parents: 29509
diff changeset
   107
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   108
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   109
subsection \<open>Basic operations\<close>
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   110
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   111
subsubsection \<open>Conversion to set and membership\<close>
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   112
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   113
definition set_mset :: "'a multiset \<Rightarrow> 'a set"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   114
  where "set_mset M = {x. count M x > 0}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   115
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   116
abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   117
  where "Melem a M \<equiv> a \<in> set_mset M"
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   118
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   119
notation
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   120
  Melem  ("op \<in>#") and
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   121
  Melem  ("(_/ \<in># _)" [51, 51] 50)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   122
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   123
notation  (ASCII)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   124
  Melem  ("op :#") and
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   125
  Melem  ("(_/ :# _)" [51, 51] 50)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   126
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   127
abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   128
  where "not_Melem a M \<equiv> a \<notin> set_mset M"
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   129
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   130
notation
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   131
  not_Melem  ("op \<notin>#") and
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   132
  not_Melem  ("(_/ \<notin># _)" [51, 51] 50)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   133
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   134
notation  (ASCII)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   135
  not_Melem  ("op ~:#") and
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   136
  not_Melem  ("(_/ ~:# _)" [51, 51] 50)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   137
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   138
context
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   139
begin
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   140
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   141
qualified abbreviation Ball :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   142
  where "Ball M \<equiv> Set.Ball (set_mset M)"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   143
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   144
qualified abbreviation Bex :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   145
  where "Bex M \<equiv> Set.Bex (set_mset M)"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   146
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   147
end
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   148
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   149
syntax
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   150
  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_\<in>#_./ _)" [0, 0, 10] 10)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   151
  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_\<in>#_./ _)" [0, 0, 10] 10)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   152
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   153
syntax  (ASCII)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   154
  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_:#_./ _)" [0, 0, 10] 10)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   155
  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_:#_./ _)" [0, 0, 10] 10)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   156
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   157
translations
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   158
  "\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   159
  "\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   160
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   161
lemma count_eq_zero_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   162
  "count M x = 0 \<longleftrightarrow> x \<notin># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   163
  by (auto simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   164
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   165
lemma not_in_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   166
  "x \<notin># M \<longleftrightarrow> count M x = 0"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   167
  by (auto simp add: count_eq_zero_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   168
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   169
lemma count_greater_zero_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   170
  "count M x > 0 \<longleftrightarrow> x \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   171
  by (auto simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   172
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   173
lemma count_inI:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   174
  assumes "count M x = 0 \<Longrightarrow> False"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   175
  shows "x \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   176
proof (rule ccontr)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   177
  assume "x \<notin># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   178
  with assms show False by (simp add: not_in_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   179
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   180
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   181
lemma in_countE:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   182
  assumes "x \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   183
  obtains n where "count M x = Suc n"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   184
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   185
  from assms have "count M x > 0" by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   186
  then obtain n where "count M x = Suc n"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   187
    using gr0_conv_Suc by blast
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   188
  with that show thesis .
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   189
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   190
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   191
lemma count_greater_eq_Suc_zero_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   192
  "count M x \<ge> Suc 0 \<longleftrightarrow> x \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   193
  by (simp add: Suc_le_eq)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   194
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   195
lemma count_greater_eq_one_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   196
  "count M x \<ge> 1 \<longleftrightarrow> x \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   197
  by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   198
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   199
lemma set_mset_empty [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   200
  "set_mset {#} = {}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   201
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   202
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   203
lemma set_mset_single [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   204
  "set_mset {#b#} = {b}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   205
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   206
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   207
lemma set_mset_eq_empty_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   208
  "set_mset M = {} \<longleftrightarrow> M = {#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   209
  by (auto simp add: multiset_eq_iff count_eq_zero_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   210
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   211
lemma finite_set_mset [iff]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   212
  "finite (set_mset M)"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   213
  using count [of M] by (simp add: multiset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   214
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   215
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   216
subsubsection \<open>Union\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   217
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   218
lemma count_union [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   219
  "count (M + N) a = count M a + count N a"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   220
  by (simp add: plus_multiset.rep_eq)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   221
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   222
lemma set_mset_union [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   223
  "set_mset (M + N) = set_mset M \<union> set_mset N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   224
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_union) simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   225
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   226
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   227
subsubsection \<open>Difference\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   228
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   229
instance multiset :: (type) comm_monoid_diff
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   230
  by standard (transfer; simp add: fun_eq_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   231
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   232
lemma count_diff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   233
  "count (M - N) a = count M a - count N a"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   234
  by (simp add: minus_multiset.rep_eq)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   235
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   236
lemma in_diff_count:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   237
  "a \<in># M - N \<longleftrightarrow> count N a < count M a"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   238
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   239
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   240
lemma count_in_diffI:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   241
  assumes "\<And>n. count N x = n + count M x \<Longrightarrow> False"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   242
  shows "x \<in># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   243
proof (rule ccontr)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   244
  assume "x \<notin># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   245
  then have "count N x = (count N x - count M x) + count M x"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   246
    by (simp add: in_diff_count not_less)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   247
  with assms show False by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   248
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   249
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   250
lemma in_diff_countE:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   251
  assumes "x \<in># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   252
  obtains n where "count M x = Suc n + count N x"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   253
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   254
  from assms have "count M x - count N x > 0" by (simp add: in_diff_count)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   255
  then have "count M x > count N x" by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   256
  then obtain n where "count M x = Suc n + count N x"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   257
    using less_iff_Suc_add by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   258
  with that show thesis .
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   259
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   260
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   261
lemma in_diffD:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   262
  assumes "a \<in># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   263
  shows "a \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   264
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   265
  have "0 \<le> count N a" by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   266
  also from assms have "count N a < count M a"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   267
    by (simp add: in_diff_count)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   268
  finally show ?thesis by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   269
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   270
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   271
lemma set_mset_diff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   272
  "set_mset (M - N) = {a. count N a < count M a}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   273
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   274
17161
57c69627d71a tuned some proofs;
wenzelm
parents: 15869
diff changeset
   275
lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   276
  by rule (fact Groups.diff_zero, fact Groups.zero_diff)
36903
489c1fbbb028 Multiset: renamed, added and tuned lemmas;
nipkow
parents: 36867
diff changeset
   277
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   278
lemma diff_cancel [simp]: "A - A = {#}"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   279
  by (fact Groups.diff_cancel)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   280
36903
489c1fbbb028 Multiset: renamed, added and tuned lemmas;
nipkow
parents: 36867
diff changeset
   281
lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   282
  by (fact add_diff_cancel_right')
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   283
36903
489c1fbbb028 Multiset: renamed, added and tuned lemmas;
nipkow
parents: 36867
diff changeset
   284
lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   285
  by (fact add_diff_cancel_left')
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   286
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   287
lemma diff_right_commute:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   288
  fixes M N Q :: "'a multiset"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   289
  shows "M - N - Q = M - Q - N"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   290
  by (fact diff_right_commute)
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   291
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   292
lemma diff_add:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   293
  fixes M N Q :: "'a multiset"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   294
  shows "M - (N + Q) = M - N - Q"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   295
  by (rule sym) (fact diff_diff_add)
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   296
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   297
lemma insert_DiffM: "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   298
  by (clarsimp simp: multiset_eq_iff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   299
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   300
lemma insert_DiffM2 [simp]: "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   301
  by (clarsimp simp: multiset_eq_iff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   302
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   303
lemma diff_union_swap: "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   304
  by (auto simp add: multiset_eq_iff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   305
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   306
lemma diff_union_single_conv:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   307
  "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   308
  by (simp add: multiset_eq_iff Suc_le_eq)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   309
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   310
lemma mset_add [elim?]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   311
  assumes "a \<in># A"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   312
  obtains B where "A = B + {#a#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   313
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   314
  from assms have "A = (A - {#a#}) + {#a#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   315
    by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   316
  with that show thesis .
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   317
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   318
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   319
lemma union_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   320
  "a \<in># A + B \<longleftrightarrow> a \<in># A \<or> a \<in># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   321
  by auto
26143
314c0bcb7df7 Added useful general lemmas from the work with the HeapMonad
bulwahn
parents: 26033
diff changeset
   322
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   323
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   324
subsubsection \<open>Equality of multisets\<close>
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   325
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   326
lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   327
  by (simp add: multiset_eq_iff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   328
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   329
lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   330
  by (auto simp add: multiset_eq_iff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   331
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   332
lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   333
  by (auto simp add: multiset_eq_iff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   334
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   335
lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   336
  by (auto simp add: multiset_eq_iff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   337
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   338
lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   339
  by (auto simp add: multiset_eq_iff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   340
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   341
lemma diff_single_trivial: "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   342
  by (auto simp add: multiset_eq_iff not_in_iff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   343
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   344
lemma diff_single_eq_union: "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = N + {#x#}"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   345
  by auto
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   346
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   347
lemma union_single_eq_diff: "M + {#x#} = N \<Longrightarrow> M = N - {#x#}"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   348
  by (auto dest: sym)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   349
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   350
lemma union_single_eq_member: "M + {#x#} = N \<Longrightarrow> x \<in># N"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   351
  by auto
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   352
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   353
lemma union_is_single:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   354
  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N = {#} \<or> M = {#} \<and> N = {#a#}"
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   355
  (is "?lhs = ?rhs")
46730
e3b99d0231bc tuned proofs;
wenzelm
parents: 46394
diff changeset
   356
proof
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   357
  show ?lhs if ?rhs using that by auto
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   358
  show ?rhs if ?lhs
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   359
    by (metis Multiset.diff_cancel add.commute add_diff_cancel_left' diff_add_zero diff_single_trivial insert_DiffM that)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   360
qed
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   361
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   362
lemma single_is_union: "{#a#} = M + N \<longleftrightarrow> {#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   363
  by (auto simp add: eq_commute [of "{#a#}" "M + N"] union_is_single)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   364
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   365
lemma add_eq_conv_diff:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   366
  "M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   367
  (is "?lhs \<longleftrightarrow> ?rhs")
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44339
diff changeset
   368
(* shorter: by (simp add: multiset_eq_iff) fastforce *)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   369
proof
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   370
  show ?lhs if ?rhs
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   371
    using that
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   372
    by (auto simp add: add.assoc add.commute [of "{#b#}"])
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   373
      (drule sym, simp add: add.assoc [symmetric])
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   374
  show ?rhs if ?lhs
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   375
  proof (cases "a = b")
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   376
    case True with \<open>?lhs\<close> show ?thesis by simp
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   377
  next
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   378
    case False
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   379
    from \<open>?lhs\<close> have "a \<in># N + {#b#}" by (rule union_single_eq_member)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   380
    with False have "a \<in># N" by auto
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   381
    moreover from \<open>?lhs\<close> have "M = N + {#b#} - {#a#}" by (rule union_single_eq_diff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   382
    moreover note False
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   383
    ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"] diff_union_swap)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   384
  qed
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   385
qed
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   386
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   387
lemma insert_noteq_member:
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   388
  assumes BC: "B + {#b#} = C + {#c#}"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   389
   and bnotc: "b \<noteq> c"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   390
  shows "c \<in># B"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   391
proof -
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   392
  have "c \<in># C + {#c#}" by simp
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   393
  have nc: "\<not> c \<in># {#b#}" using bnotc by simp
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   394
  then have "c \<in># B + {#b#}" using BC by simp
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   395
  then show "c \<in># B" using nc by simp
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   396
qed
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   397
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   398
lemma add_eq_conv_ex:
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   399
  "(M + {#a#} = N + {#b#}) =
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   400
    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   401
  by (auto simp add: add_eq_conv_diff)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   402
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   403
lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   404
  by (rule exI [where x = "M - {#x#}"]) simp
51600
197e25f13f0c default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents: 51599
diff changeset
   405
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   406
lemma multiset_add_sub_el_shuffle:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   407
  assumes "c \<in># B"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   408
    and "b \<noteq> c"
58098
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   409
  shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   410
proof -
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   411
  from \<open>c \<in># B\<close> obtain A where B: "B = A + {#c#}"
58098
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   412
    by (blast dest: multi_member_split)
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   413
  have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   414
  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
58098
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   415
    by (simp add: ac_simps)
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   416
  then show ?thesis using B by simp
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   417
qed
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   418
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   419
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   420
subsubsection \<open>Pointwise ordering induced by count\<close>
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   421
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   422
definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   423
  where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)"
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   424
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   425
definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   426
  where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)"
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   427
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   428
abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<supseteq>#" 50)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   429
  where "supseteq_mset A B \<equiv> B \<subseteq># A"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   431
abbreviation (input) supset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<supset>#" 50)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   432
  where "supset_mset A B \<equiv> B \<subset># A"
62208
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   433
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   434
notation (input)
62208
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   435
  subseteq_mset  (infix "\<le>#" 50) and
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   436
  supseteq_mset  (infix "\<ge>#" 50)
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   437
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   438
notation (ASCII)
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   439
  subseteq_mset  (infix "<=#" 50) and
62208
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   440
  subset_mset  (infix "<#" 50) and
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   441
  supseteq_mset  (infix ">=#" 50) and
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   442
  supset_mset  (infix ">#" 50)
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   443
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   444
interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   445
  by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   446
  -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   447
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   448
lemma mset_less_eqI:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   449
  "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B"
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   450
  by (simp add: subseteq_mset_def)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   451
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   452
lemma mset_less_eq_count:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   453
  "A \<subseteq># B \<Longrightarrow> count A a \<le> count B a"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   454
  by (simp add: subseteq_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   455
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   456
lemma mset_le_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)"
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   457
  unfolding subseteq_mset_def
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   458
  apply (rule iffI)
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   459
   apply (rule exI [where x = "B - A"])
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   460
   apply (auto intro: multiset_eq_iff [THEN iffD2])
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   461
  done
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   462
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
   463
interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" 0 "op \<le>#" "op <#" "op -"
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   464
  by standard (simp, fact mset_le_exists_conv)
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   465
62378
85ed00c1fe7c generalize more theorems to support enat and ennreal
hoelzl
parents: 62376
diff changeset
   466
declare subset_mset.zero_order[simp del]
85ed00c1fe7c generalize more theorems to support enat and ennreal
hoelzl
parents: 62376
diff changeset
   467
  -- \<open>this removes some simp rules not in the usual order for multisets\<close>
85ed00c1fe7c generalize more theorems to support enat and ennreal
hoelzl
parents: 62376
diff changeset
   468
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   469
lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   470
   by (fact subset_mset.add_le_cancel_right)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   471
 
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   472
lemma mset_le_mono_add_left_cancel [simp]: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   473
   by (fact subset_mset.add_le_cancel_left)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   474
 
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   475
lemma mset_le_mono_add: "(A::'a multiset) \<subseteq># B \<Longrightarrow> C \<subseteq># D \<Longrightarrow> A + C \<subseteq># B + D"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   476
   by (fact subset_mset.add_mono)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   477
 
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   478
lemma mset_le_add_left [simp]: "(A::'a multiset) \<subseteq># A + B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   479
   unfolding subseteq_mset_def by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   480
 
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   481
lemma mset_le_add_right [simp]: "B \<subseteq># (A::'a multiset) + B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   482
   unfolding subseteq_mset_def by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   483
 
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   484
lemma single_subset_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   485
  "{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   486
  by (auto simp add: subseteq_mset_def Suc_le_eq)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   487
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   488
lemma mset_le_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   489
  by (simp add: subseteq_mset_def Suc_le_eq)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   490
 
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   491
lemma multiset_diff_union_assoc:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   492
  fixes A B C D :: "'a multiset"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   493
  shows "C \<subseteq># B \<Longrightarrow> A + B - C = A + (B - C)"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   494
  by (fact subset_mset.diff_add_assoc)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   495
 
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   496
lemma mset_le_multiset_union_diff_commute:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   497
  fixes A B C D :: "'a multiset"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   498
  shows "B \<subseteq># A \<Longrightarrow> A - B + C = A + C - B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   499
  by (fact subset_mset.add_diff_assoc2)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   500
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   501
lemma diff_le_self[simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   502
  "(M::'a multiset) - N \<subseteq># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   503
  by (simp add: subseteq_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   504
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   505
lemma mset_leD:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   506
  assumes "A \<subseteq># B" and "x \<in># A"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   507
  shows "x \<in># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   508
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   509
  from \<open>x \<in># A\<close> have "count A x > 0" by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   510
  also from \<open>A \<subseteq># B\<close> have "count A x \<le> count B x"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   511
    by (simp add: subseteq_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   512
  finally show ?thesis by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   513
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   514
  
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   515
lemma mset_lessD:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   516
  "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   517
  by (auto intro: mset_leD [of A])
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   518
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   519
lemma set_mset_mono:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   520
  "A \<subseteq># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   521
  by (metis mset_leD subsetI)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   522
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   523
lemma mset_le_insertD:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   524
  "A + {#x#} \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   525
apply (rule conjI)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   526
 apply (simp add: mset_leD)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   527
 apply (clarsimp simp: subset_mset_def subseteq_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   528
 apply safe
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   529
  apply (erule_tac x = a in allE)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   530
  apply (auto split: if_split_asm)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   531
done
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   532
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   533
lemma mset_less_insertD:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   534
  "A + {#x#} \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   535
  by (rule mset_le_insertD) simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   536
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   537
lemma mset_less_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   538
  by (auto simp add: subseteq_mset_def subset_mset_def multiset_eq_iff)
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   539
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   540
lemma empty_le [simp]: "{#} \<subseteq># A"
55808
488c3e8282c8 added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents: 55565
diff changeset
   541
  unfolding mset_le_exists_conv by auto
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   542
 
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   543
lemma insert_subset_eq_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   544
  "{#a#} + A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   545
  using le_diff_conv2 [of "Suc 0" "count B a" "count A a"]
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   546
  apply (auto simp add: subseteq_mset_def not_in_iff Suc_le_eq)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   547
  apply (rule ccontr)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   548
  apply (auto simp add: not_in_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   549
  done
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   550
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   551
lemma insert_union_subset_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   552
  "{#a#} + A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   553
  by (auto simp add: insert_subset_eq_iff subset_mset_def insert_DiffM)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   554
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   555
lemma subset_eq_diff_conv:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   556
  "A - C \<subseteq># B \<longleftrightarrow> A \<subseteq># B + C"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   557
  by (simp add: subseteq_mset_def le_diff_conv)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   558
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   559
lemma le_empty [simp]: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   560
  unfolding mset_le_exists_conv by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   561
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   562
lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   563
  by (auto simp: subset_mset_def subseteq_mset_def)
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   564
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   565
lemma multi_psub_self[simp]: "(A::'a multiset) \<subset># A = False"
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   566
  by simp
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   567
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   568
lemma mset_less_add_bothsides: "N + {#x#} \<subset># M + {#x#} \<Longrightarrow> N \<subset># M"
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   569
  by (fact subset_mset.add_less_imp_less_right)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   570
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   571
lemma mset_less_empty_nonempty: "{#} \<subset># S \<longleftrightarrow> S \<noteq> {#}"
62378
85ed00c1fe7c generalize more theorems to support enat and ennreal
hoelzl
parents: 62376
diff changeset
   572
  by (fact subset_mset.zero_less_iff_neq_zero)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   573
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   574
lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   575
  by (auto simp: subset_mset_def elim: mset_add)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   576
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   577
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   578
subsubsection \<open>Intersection\<close>
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   579
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   580
definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   581
  multiset_inter_def: "inf_subset_mset A B = A - (A - B)"
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   582
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   583
interpretation subset_mset: semilattice_inf inf_subset_mset "op \<subseteq>#" "op \<subset>#"
46921
aa862ff8a8a9 some proof indentation;
wenzelm
parents: 46756
diff changeset
   584
proof -
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   585
  have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   586
    by arith
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   587
  show "class.semilattice_inf op #\<inter> op \<subseteq># op \<subset>#"
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   588
    by standard (auto simp add: multiset_inter_def subseteq_mset_def)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   589
qed
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   590
  -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   591
41069
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
   592
lemma multiset_inter_count [simp]:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   593
  fixes A B :: "'a multiset"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   594
  shows "count (A #\<inter> B) x = min (count A x) (count B x)"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   595
  by (simp add: multiset_inter_def)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   596
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   597
lemma set_mset_inter [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   598
  "set_mset (A #\<inter> B) = set_mset A \<inter> set_mset B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   599
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] multiset_inter_count) simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   600
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   601
lemma diff_intersect_left_idem [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   602
  "M - M #\<inter> N = M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   603
  by (simp add: multiset_eq_iff min_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   604
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   605
lemma diff_intersect_right_idem [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   606
  "M - N #\<inter> M = M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   607
  by (simp add: multiset_eq_iff min_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   608
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   609
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
46730
e3b99d0231bc tuned proofs;
wenzelm
parents: 46394
diff changeset
   610
  by (rule multiset_eqI) auto
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   611
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   612
lemma multiset_union_diff_commute:
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   613
  assumes "B #\<inter> C = {#}"
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   614
  shows "A + B - C = A - C + B"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   615
proof (rule multiset_eqI)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   616
  fix x
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   617
  from assms have "min (count B x) (count C x) = 0"
46730
e3b99d0231bc tuned proofs;
wenzelm
parents: 46394
diff changeset
   618
    by (auto simp add: multiset_eq_iff)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   619
  then have "count B x = 0 \<or> count C x = 0"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   620
    unfolding min_def by (auto split: if_splits)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   621
  then show "count (A + B - C) x = count (A - C + B) x"
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   622
    by auto
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   623
qed
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   624
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   625
lemma disjunct_not_in:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   626
  "A #\<inter> B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)" (is "?P \<longleftrightarrow> ?Q")
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   627
proof
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   628
  assume ?P
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   629
  show ?Q
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   630
  proof
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   631
    fix a
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   632
    from \<open>?P\<close> have "min (count A a) (count B a) = 0"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   633
      by (simp add: multiset_eq_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   634
    then have "count A a = 0 \<or> count B a = 0"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   635
      by (cases "count A a \<le> count B a") (simp_all add: min_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   636
    then show "a \<notin># A \<or> a \<notin># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   637
      by (simp add: not_in_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   638
  qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   639
next
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   640
  assume ?Q
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   641
  show ?P
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   642
  proof (rule multiset_eqI)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   643
    fix a
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   644
    from \<open>?Q\<close> have "count A a = 0 \<or> count B a = 0"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   645
      by (auto simp add: not_in_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   646
    then show "count (A #\<inter> B) a = count {#} a"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   647
      by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   648
  qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   649
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   650
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   651
lemma empty_inter [simp]: "{#} #\<inter> M = {#}"
51600
197e25f13f0c default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents: 51599
diff changeset
   652
  by (simp add: multiset_eq_iff)
197e25f13f0c default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents: 51599
diff changeset
   653
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   654
lemma inter_empty [simp]: "M #\<inter> {#} = {#}"
51600
197e25f13f0c default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents: 51599
diff changeset
   655
  by (simp add: multiset_eq_iff)
197e25f13f0c default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents: 51599
diff changeset
   656
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   657
lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = M #\<inter> N"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   658
  by (simp add: multiset_eq_iff not_in_iff)
51600
197e25f13f0c default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents: 51599
diff changeset
   659
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   660
lemma inter_add_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = (M #\<inter> (N - {#x#})) + {#x#}"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   661
  by (auto simp add: multiset_eq_iff elim: mset_add)
51600
197e25f13f0c default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents: 51599
diff changeset
   662
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   663
lemma inter_add_right1: "\<not> x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = N #\<inter> M"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   664
  by (simp add: multiset_eq_iff not_in_iff)
51600
197e25f13f0c default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents: 51599
diff changeset
   665
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   666
lemma inter_add_right2: "x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = ((N - {#x#}) #\<inter> M) + {#x#}"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   667
  by (auto simp add: multiset_eq_iff elim: mset_add)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   668
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   669
lemma disjunct_set_mset_diff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   670
  assumes "M #\<inter> N = {#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   671
  shows "set_mset (M - N) = set_mset M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   672
proof (rule set_eqI)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   673
  fix a
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   674
  from assms have "a \<notin># M \<or> a \<notin># N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   675
    by (simp add: disjunct_not_in)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   676
  then show "a \<in># M - N \<longleftrightarrow> a \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   677
    by (auto dest: in_diffD) (simp add: in_diff_count not_in_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   678
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   679
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   680
lemma at_most_one_mset_mset_diff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   681
  assumes "a \<notin># M - {#a#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   682
  shows "set_mset (M - {#a#}) = set_mset M - {a}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   683
  using assms by (auto simp add: not_in_iff in_diff_count set_eq_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   684
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   685
lemma more_than_one_mset_mset_diff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   686
  assumes "a \<in># M - {#a#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   687
  shows "set_mset (M - {#a#}) = set_mset M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   688
proof (rule set_eqI)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   689
  fix b
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   690
  have "Suc 0 < count M b \<Longrightarrow> count M b > 0" by arith
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   691
  then show "b \<in># M - {#a#} \<longleftrightarrow> b \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   692
    using assms by (auto simp add: in_diff_count)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   693
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   694
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   695
lemma inter_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   696
  "a \<in># A #\<inter> B \<longleftrightarrow> a \<in># A \<and> a \<in># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   697
  by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   698
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   699
lemma inter_union_distrib_left:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   700
  "A #\<inter> B + C = (A + C) #\<inter> (B + C)"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   701
  by (simp add: multiset_eq_iff min_add_distrib_left)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   702
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   703
lemma inter_union_distrib_right:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   704
  "C + A #\<inter> B = (C + A) #\<inter> (C + B)"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   705
  using inter_union_distrib_left [of A B C] by (simp add: ac_simps)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   706
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   707
lemma inter_subset_eq_union:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   708
  "A #\<inter> B \<subseteq># A + B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   709
  by (auto simp add: subseteq_mset_def)
51600
197e25f13f0c default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents: 51599
diff changeset
   710
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   711
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   712
subsubsection \<open>Bounded union\<close>
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   713
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   714
definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   715
  where "sup_subset_mset A B = A + (B - A)" -- \<open>FIXME irregular fact name\<close>
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   716
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   717
interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#"
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   718
proof -
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   719
  have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   720
    by arith
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   721
  show "class.semilattice_sup op #\<union> op \<subseteq># op \<subset>#"
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   722
    by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   723
qed
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   724
  -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   725
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   726
lemma sup_subset_mset_count [simp]: -- \<open>FIXME irregular fact name\<close>
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   727
  "count (A #\<union> B) x = max (count A x) (count B x)"
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   728
  by (simp add: sup_subset_mset_def)
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   729
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   730
lemma set_mset_sup [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   731
  "set_mset (A #\<union> B) = set_mset A \<union> set_mset B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   732
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   733
    (auto simp add: not_in_iff elim: mset_add)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   734
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   735
lemma empty_sup [simp]: "{#} #\<union> M = M"
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   736
  by (simp add: multiset_eq_iff)
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   737
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   738
lemma sup_empty [simp]: "M #\<union> {#} = M"
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   739
  by (simp add: multiset_eq_iff)
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   740
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   741
lemma sup_union_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   742
  by (simp add: multiset_eq_iff not_in_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   743
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   744
lemma sup_union_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N - {#x#})) + {#x#}"
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   745
  by (simp add: multiset_eq_iff)
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   746
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   747
lemma sup_union_right1: "\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   748
  by (simp add: multiset_eq_iff not_in_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   749
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   750
lemma sup_union_right2: "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}"
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   751
  by (simp add: multiset_eq_iff)
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   752
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   753
lemma sup_union_distrib_left:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   754
  "A #\<union> B + C = (A + C) #\<union> (B + C)"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   755
  by (simp add: multiset_eq_iff max_add_distrib_left)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   756
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   757
lemma union_sup_distrib_right:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   758
  "C + A #\<union> B = (C + A) #\<union> (C + B)"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   759
  using sup_union_distrib_left [of A B C] by (simp add: ac_simps)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   760
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   761
lemma union_diff_inter_eq_sup:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   762
  "A + B - A #\<inter> B = A #\<union> B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   763
  by (auto simp add: multiset_eq_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   764
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   765
lemma union_diff_sup_eq_inter:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   766
  "A + B - A #\<union> B = A #\<inter> B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   767
  by (auto simp add: multiset_eq_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   768
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   769
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   770
subsubsection \<open>Subset is an order\<close>
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   771
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   772
interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   773
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   774
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   775
subsubsection \<open>Filter (with comprehension syntax)\<close>
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   776
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   777
text \<open>Multiset comprehension\<close>
41069
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
   778
59998
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
   779
lift_definition filter_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
   780
is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   781
by (rule filter_preserves_multiset)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   782
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   783
syntax (ASCII)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   784
  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ :# _./ _#})")
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   785
syntax
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   786
  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ \<in># _./ _#})")
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   787
translations
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   788
  "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   789
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   790
lemma count_filter_mset [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   791
  "count (filter_mset P M) a = (if P a then count M a else 0)"
59998
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
   792
  by (simp add: filter_mset.rep_eq)
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
   793
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   794
lemma set_mset_filter [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   795
  "set_mset (filter_mset P M) = {a \<in> set_mset M. P a}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   796
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_filter_mset) simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   797
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   798
lemma filter_empty_mset [simp]: "filter_mset P {#} = {#}"
59998
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
   799
  by (rule multiset_eqI) simp
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
   800
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   801
lemma filter_single_mset [simp]: "filter_mset P {#x#} = (if P x then {#x#} else {#})"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   802
  by (rule multiset_eqI) simp
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   803
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   804
lemma filter_union_mset [simp]: "filter_mset P (M + N) = filter_mset P M + filter_mset P N"
41069
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
   805
  by (rule multiset_eqI) simp
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
   806
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   807
lemma filter_diff_mset [simp]: "filter_mset P (M - N) = filter_mset P M - filter_mset P N"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   808
  by (rule multiset_eqI) simp
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   809
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   810
lemma filter_inter_mset [simp]: "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N"
41069
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
   811
  by (rule multiset_eqI) simp
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
   812
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   813
lemma multiset_filter_subset[simp]: "filter_mset f M \<subseteq># M"
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   814
  by (simp add: mset_less_eqI)
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   815
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   816
lemma multiset_filter_mono:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   817
  assumes "A \<subseteq># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   818
  shows "filter_mset f A \<subseteq># filter_mset f B"
58035
177eeda93a8c added lemmas contributed by Rene Thiemann
blanchet
parents: 57966
diff changeset
   819
proof -
177eeda93a8c added lemmas contributed by Rene Thiemann
blanchet
parents: 57966
diff changeset
   820
  from assms[unfolded mset_le_exists_conv]
177eeda93a8c added lemmas contributed by Rene Thiemann
blanchet
parents: 57966
diff changeset
   821
  obtain C where B: "B = A + C" by auto
177eeda93a8c added lemmas contributed by Rene Thiemann
blanchet
parents: 57966
diff changeset
   822
  show ?thesis unfolding B by auto
177eeda93a8c added lemmas contributed by Rene Thiemann
blanchet
parents: 57966
diff changeset
   823
qed
177eeda93a8c added lemmas contributed by Rene Thiemann
blanchet
parents: 57966
diff changeset
   824
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   825
lemma filter_mset_eq_conv:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   826
  "filter_mset P M = N \<longleftrightarrow> N \<subseteq># M \<and> (\<forall>b\<in>#N. P b) \<and> (\<forall>a\<in>#M - N. \<not> P a)" (is "?P \<longleftrightarrow> ?Q")
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   827
proof
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   828
  assume ?P then show ?Q by auto (simp add: multiset_eq_iff in_diff_count)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   829
next
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   830
  assume ?Q
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   831
  then obtain Q where M: "M = N + Q"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   832
    by (auto simp add: mset_le_exists_conv)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   833
  then have MN: "M - N = Q" by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   834
  show ?P
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   835
  proof (rule multiset_eqI)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   836
    fix a
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   837
    from \<open>?Q\<close> MN have *: "\<not> P a \<Longrightarrow> a \<notin># N" "P a \<Longrightarrow> a \<notin># Q"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   838
      by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   839
    show "count (filter_mset P M) a = count N a"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   840
    proof (cases "a \<in># M")
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   841
      case True
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   842
      with * show ?thesis
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   843
        by (simp add: not_in_iff M)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   844
    next
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   845
      case False then have "count M a = 0"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   846
        by (simp add: not_in_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   847
      with M show ?thesis by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   848
    qed 
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   849
  qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   850
qed
59813
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
   851
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
   852
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   853
subsubsection \<open>Size\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   854
56656
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   855
definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))"
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   856
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   857
lemma wcount_union: "wcount f (M + N) a = wcount f M a + wcount f N a"
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   858
  by (auto simp: wcount_def add_mult_distrib)
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   859
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   860
definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where
60495
d7ff0a1df90a renamed Multiset.set_of to the canonical set_mset
nipkow
parents: 60400
diff changeset
   861
  "size_multiset f M = setsum (wcount f M) (set_mset M)"
56656
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   862
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   863
lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def]
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   864
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   865
instantiation multiset :: (type) size
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   866
begin
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   867
56656
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   868
definition size_multiset where
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   869
  size_multiset_overloaded_def: "size_multiset = Multiset.size_multiset (\<lambda>_. 0)"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   870
instance ..
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   871
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   872
end
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   873
56656
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   874
lemmas size_multiset_overloaded_eq =
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   875
  size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified]
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   876
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   877
lemma size_multiset_empty [simp]: "size_multiset f {#} = 0"
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   878
by (simp add: size_multiset_def)
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   879
28708
a1a436f09ec6 explicit check for pattern discipline before code translation
haftmann
parents: 28562
diff changeset
   880
lemma size_empty [simp]: "size {#} = 0"
56656
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   881
by (simp add: size_multiset_overloaded_def)
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   882
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   883
lemma size_multiset_single [simp]: "size_multiset f {#b#} = Suc (f b)"
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   884
by (simp add: size_multiset_eq)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   885
28708
a1a436f09ec6 explicit check for pattern discipline before code translation
haftmann
parents: 28562
diff changeset
   886
lemma size_single [simp]: "size {#b#} = 1"
56656
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   887
by (simp add: size_multiset_overloaded_def)
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   888
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   889
lemma setsum_wcount_Int:
60495
d7ff0a1df90a renamed Multiset.set_of to the canonical set_mset
nipkow
parents: 60400
diff changeset
   890
  "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_mset N) = setsum (wcount f N) A"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   891
  by (induct rule: finite_induct)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   892
    (simp_all add: Int_insert_left wcount_def count_eq_zero_iff)
56656
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   893
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   894
lemma size_multiset_union [simp]:
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   895
  "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56656
diff changeset
   896
apply (simp add: size_multiset_def setsum_Un_nat setsum.distrib setsum_wcount_Int wcount_union)
56656
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   897
apply (subst Int_commute)
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   898
apply (simp add: setsum_wcount_Int)
26178
nipkow
parents: 26176
diff changeset
   899
done
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   900
28708
a1a436f09ec6 explicit check for pattern discipline before code translation
haftmann
parents: 28562
diff changeset
   901
lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
56656
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   902
by (auto simp add: size_multiset_overloaded_def)
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   903
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   904
lemma size_multiset_eq_0_iff_empty [iff]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   905
  "size_multiset f M = 0 \<longleftrightarrow> M = {#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   906
  by (auto simp add: size_multiset_eq count_eq_zero_iff)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   907
17161
57c69627d71a tuned some proofs;
wenzelm
parents: 15869
diff changeset
   908
lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
56656
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   909
by (auto simp add: size_multiset_overloaded_def)
26016
f9d1bf2fc59c added multiset comprehension
nipkow
parents: 25759
diff changeset
   910
f9d1bf2fc59c added multiset comprehension
nipkow
parents: 25759
diff changeset
   911
lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
26178
nipkow
parents: 26176
diff changeset
   912
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   913
60607
d440af2e584f more symbols;
wenzelm
parents: 60606
diff changeset
   914
lemma size_eq_Suc_imp_elem: "size M = Suc n \<Longrightarrow> \<exists>a. a \<in># M"
56656
7f9b686bf30a size function for multisets
blanchet
parents: 55945
diff changeset
   915
apply (unfold size_multiset_overloaded_eq)
26178
nipkow
parents: 26176
diff changeset
   916
apply (drule setsum_SucD)
nipkow
parents: 26176
diff changeset
   917
apply auto
nipkow
parents: 26176
diff changeset
   918
done
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   919
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   920
lemma size_eq_Suc_imp_eq_union:
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   921
  assumes "size M = Suc n"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   922
  shows "\<exists>a N. M = N + {#a#}"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   923
proof -
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   924
  from assms obtain a where "a \<in># M"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   925
    by (erule size_eq_Suc_imp_elem [THEN exE])
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   926
  then have "M = M - {#a#} + {#a#}" by simp
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   927
  then show ?thesis by blast
23611
65b168646309 more interpretations
nipkow
parents: 23373
diff changeset
   928
qed
15869
3aca7f05cd12 intersection
kleing
parents: 15867
diff changeset
   929
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   930
lemma size_mset_mono:
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   931
  fixes A B :: "'a multiset"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   932
  assumes "A \<subseteq># B"
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   933
  shows "size A \<le> size B"
59949
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
   934
proof -
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
   935
  from assms[unfolded mset_le_exists_conv]
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
   936
  obtain C where B: "B = A + C" by auto
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   937
  show ?thesis unfolding B by (induct C) auto
59949
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
   938
qed
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
   939
59998
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
   940
lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \<le> size M"
59949
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
   941
by (rule size_mset_mono[OF multiset_filter_subset])
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
   942
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
   943
lemma size_Diff_submset:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   944
  "M \<subseteq># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
59949
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
   945
by (metis add_diff_cancel_left' size_union mset_le_exists_conv)
26016
f9d1bf2fc59c added multiset comprehension
nipkow
parents: 25759
diff changeset
   946
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   947
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   948
subsection \<open>Induction and case splits\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   949
18258
836491e9b7d5 tuned induct proofs;
wenzelm
parents: 17778
diff changeset
   950
theorem multiset_induct [case_names empty add, induct type: multiset]:
48009
9b9150033b5a shortened some proofs
huffman
parents: 48008
diff changeset
   951
  assumes empty: "P {#}"
9b9150033b5a shortened some proofs
huffman
parents: 48008
diff changeset
   952
  assumes add: "\<And>M x. P M \<Longrightarrow> P (M + {#x#})"
9b9150033b5a shortened some proofs
huffman
parents: 48008
diff changeset
   953
  shows "P M"
9b9150033b5a shortened some proofs
huffman
parents: 48008
diff changeset
   954
proof (induct n \<equiv> "size M" arbitrary: M)
9b9150033b5a shortened some proofs
huffman
parents: 48008
diff changeset
   955
  case 0 thus "P M" by (simp add: empty)
9b9150033b5a shortened some proofs
huffman
parents: 48008
diff changeset
   956
next
9b9150033b5a shortened some proofs
huffman
parents: 48008
diff changeset
   957
  case (Suc k)
9b9150033b5a shortened some proofs
huffman
parents: 48008
diff changeset
   958
  obtain N x where "M = N + {#x#}"
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   959
    using \<open>Suc k = size M\<close> [symmetric]
48009
9b9150033b5a shortened some proofs
huffman
parents: 48008
diff changeset
   960
    using size_eq_Suc_imp_eq_union by fast
9b9150033b5a shortened some proofs
huffman
parents: 48008
diff changeset
   961
  with Suc add show "P M" by simp
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   962
qed
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   963
25610
72e1563aee09 a fold operation for multisets + more lemmas
kleing
parents: 25595
diff changeset
   964
lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}"
26178
nipkow
parents: 26176
diff changeset
   965
by (induct M) auto
25610
72e1563aee09 a fold operation for multisets + more lemmas
kleing
parents: 25595
diff changeset
   966
55913
c1409c103b77 proper UTF-8;
wenzelm
parents: 55811
diff changeset
   967
lemma multiset_cases [cases type]:
c1409c103b77 proper UTF-8;
wenzelm
parents: 55811
diff changeset
   968
  obtains (empty) "M = {#}"
c1409c103b77 proper UTF-8;
wenzelm
parents: 55811
diff changeset
   969
    | (add) N x where "M = N + {#x#}"
c1409c103b77 proper UTF-8;
wenzelm
parents: 55811
diff changeset
   970
  using assms by (induct M) simp_all
25610
72e1563aee09 a fold operation for multisets + more lemmas
kleing
parents: 25595
diff changeset
   971
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   972
lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   973
by (cases "B = {#}") (auto dest: multi_member_split)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   974
60607
d440af2e584f more symbols;
wenzelm
parents: 60606
diff changeset
   975
lemma multiset_partition: "M = {# x\<in>#M. P x #} + {# x\<in>#M. \<not> P x #}"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
   976
apply (subst multiset_eq_iff)
26178
nipkow
parents: 26176
diff changeset
   977
apply auto
nipkow
parents: 26176
diff changeset
   978
done
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   979
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   980
lemma mset_less_size: "(A::'a multiset) \<subset># B \<Longrightarrow> size A < size B"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   981
proof (induct A arbitrary: B)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   982
  case (empty M)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   983
  then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   984
  then obtain M' x where "M = M' + {#x#}"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   985
    by (blast dest: multi_nonempty_split)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   986
  then show ?case by simp
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   987
next
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   988
  case (add S x T)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   989
  have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   990
  have SxsubT: "S + {#x#} \<subset># T" by fact
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   991
  then have "x \<in># T" and "S \<subset># T"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   992
    by (auto dest: mset_less_insertD)
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   993
  then obtain T' where T: "T = T' + {#x#}"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   994
    by (blast dest: multi_member_split)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   995
  then have "S \<subset># T'" using SxsubT
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   996
    by (blast intro: mset_less_add_bothsides)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   997
  then have "size S < size T'" using IH by simp
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   998
  then show ?case using T by simp
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   999
qed
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1000
59949
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
  1001
lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
  1002
by (cases M) auto
fc4c896c8e74 Removed mcard because it is equal to size
nipkow
parents: 59815
diff changeset
  1003
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
  1004
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
  1005
subsubsection \<open>Strong induction and subset induction for multisets\<close>
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
  1006
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
  1007
text \<open>Well-foundedness of strict subset relation\<close>
58098
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
  1008
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
  1009
lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1010
apply (rule wf_measure [THEN wf_subset, where f1=size])
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1011
apply (clarsimp simp: measure_def inv_image_def mset_less_size)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1012
done
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1013
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1014
lemma full_multiset_induct [case_names less]:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
  1015
assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1016
shows "P B"
58098
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
  1017
apply (rule wf_less_mset_rel [THEN wf_induct])
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
  1018
apply (rule ih, auto)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1019
done
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1020
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1021
lemma multi_subset_induct [consumes 2, case_names empty add]:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
  1022
  assumes "F \<subseteq># A"
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1023
    and empty: "P {#}"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1024
    and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1025
  shows "P F"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1026
proof -
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
  1027
  from \<open>F \<subseteq># A\<close>
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1028
  show ?thesis
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1029
  proof (induct F)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1030
    show "P {#}" by fact
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1031
  next
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1032
    fix x F
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
  1033
    assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># A"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1034
    show "P (F + {#x#})"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1035
    proof (rule insert)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1036
      from i show "x \<in># A" by (auto dest: mset_le_insertD)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
  1037
      from i have "F \<subseteq># A" by (auto dest: mset_le_insertD)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1038
      with P show "P F" .
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1039
    qed
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1040
  qed
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
  1041
qed
26145
95670b6e1fa3 tuned document;
wenzelm
parents: 26143
diff changeset
  1042
17161
57c69627d71a tuned some proofs;
wenzelm
parents: 15869
diff changeset
  1043
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
  1044
subsection \<open>The fold combinator\<close>
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1045
59998
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
  1046
definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1047
where
60495
d7ff0a1df90a renamed Multiset.set_of to the canonical set_mset
nipkow
parents: 60400
diff changeset
  1048
  "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_mset M)"
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1049
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1050
lemma fold_mset_empty [simp]: "fold_mset f s {#} = s"
59998
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
  1051
  by (simp add: fold_mset_def)
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1052
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1053
context comp_fun_commute
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1054
begin
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1055
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1056
lemma fold_mset_insert: "fold_mset f s (M + {#x#}) = f x (fold_mset f s M)"
49822
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1057
proof -
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1058
  interpret mset: comp_fun_commute "\<lambda>y. f y ^^ count M y"
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1059
    by (fact comp_fun_commute_funpow)
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1060
  interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (M + {#x#}) y"
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1061
    by (fact comp_fun_commute_funpow)
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1062
  show ?thesis
60495
d7ff0a1df90a renamed Multiset.set_of to the canonical set_mset
nipkow
parents: 60400
diff changeset
  1063
  proof (cases "x \<in> set_mset M")
49822
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1064
    case False
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
  1065
    then have *: "count (M + {#x#}) x = 1"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
  1066
      by (simp add: not_in_iff)
60495
d7ff0a1df90a renamed Multiset.set_of to the canonical set_mset
nipkow
parents: 60400
diff changeset
  1067
    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_mset M) =
d7ff0a1df90a renamed Multiset.set_of to the canonical set_mset
nipkow
parents: 60400
diff changeset
  1068
      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)"
49822
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1069
      by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1070
    with False * show ?thesis
59998
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
  1071
      by (simp add: fold_mset_def del: count_union)
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1072
  next
49822
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1073
    case True
60495
d7ff0a1df90a renamed Multiset.set_of to the canonical set_mset
nipkow
parents: 60400
diff changeset
  1074
    def N \<equiv> "set_mset M - {x}"
d7ff0a1df90a renamed Multiset.set_of to the canonical set_mset
nipkow
parents: 60400
diff changeset
  1075
    from N_def True have *: "set_mset M = insert x N" "x \<notin> N" "finite N" by auto
49822
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1076
    then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1077
      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1078
      by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
59998
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
  1079
    with * show ?thesis by (simp add: fold_mset_def del: count_union) simp
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1080
  qed
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1081
qed
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1082
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1083
corollary fold_mset_single [simp]: "fold_mset f s {#x#} = f x s"
49822
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1084
proof -
59998
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
  1085
  have "fold_mset f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp
49822
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1086
  then show ?thesis by simp
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1087
qed
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1088
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1089
lemma fold_mset_fun_left_comm: "f x (fold_mset f s M) = fold_mset f (f x s) M"
49822
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1090
  by (induct M) (simp_all add: fold_mset_insert fun_left_comm)
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1091
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1092
lemma fold_mset_union [simp]: "fold_mset f s (M + N) = fold_mset f (fold_mset f s M) N"
49822
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1093
proof (induct M)
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1094
  case empty then show ?case by simp
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1095
next
49822
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1096
  case (add M x)
0cfc1651be25 simplified construction of fold combinator on multisets;
haftmann
parents: 49717
diff changeset
  1097
  have "M + {#x#} + N = (M + N) + {#x#}"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
  1098
    by (simp add: ac_simps)
51548
757fa47af981 centralized various multiset operations in theory multiset;
haftmann
parents: 51161
diff changeset
  1099
  with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm)
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1100
qed
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1101
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1102
lemma fold_mset_fusion:
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1103
  assumes "comp_fun_commute g"
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1104
    and *: "\<And>x y. h (g x y) = f x (h y)"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1105
  shows "h (fold_mset g w A) = fold_mset f (h w) A"
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1106
proof -
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1107
  interpret comp_fun_commute g by (fact assms)
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1108
  from * show ?thesis by (induct A) auto
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1109
qed
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1110
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1111
end
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1112
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
  1113
text \<open>
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1114
  A note on code generation: When defining some function containing a
59998
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
  1115
  subterm @{term "fold_mset F"}, code generation is not automatic. When
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 61566
diff changeset
  1116
  interpreting locale \<open>left_commutative\<close> with \<open>F\<close>, the
59998
c54d36be22ef renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents: 59986
diff changeset
  1117
  would be code thms for @{const fold_mset} become thms like
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 61566
diff changeset
  1118
  @{term "fold_mset F z {#} = z"} where \<open>F\<close> is not a pattern but
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1119
  contains defined symbols, i.e.\ is not a code thm. Hence a separate
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 61566
diff changeset
  1120
  constant with its own code thms needs to be introduced for \<open>F\<close>. See the image operator below.
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
  1121
\<close>
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
  1122
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
  1123
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
  1124
subsection \<open>Image\<close>
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1125
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1126
definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
60607
d440af2e584f more symbols;
wenzelm
parents: 60606
diff changeset
  1127
  "image_mset f = fold_mset (plus \<circ> single \<circ> f) {#}"
d440af2e584f more symbols;
wenzelm
parents: 60606
diff changeset
  1128
d440af2e584f more symbols;
wenzelm
parents: 60606
diff changeset
  1129
lemma comp_fun_commute_mset_image: "comp_fun_commute (plus \<circ> single \<circ> f)"
49823
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1130
proof
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
  1131
qed (simp add: ac_simps fun_eq_iff)
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1132
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1133
lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
49823
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1134
  by (simp add: image_mset_def)
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1135
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1136
lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
49823
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1137
proof -
60607
d440af2e584f more symbols;
wenzelm
parents: 60606
diff changeset
  1138
  interpret comp_fun_commute "plus \<circ> single \<circ> f"
49823
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1139
    by (fact comp_fun_commute_mset_image)
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1140
  show ?thesis by (simp add: image_mset_def)
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1141
qed
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1142
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1143
lemma image_mset_union [simp]: "image_mset f (M + N) = image_mset f M + image_mset f N"
49823
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1144
proof -
60607
d440af2e584f more symbols;
wenzelm
parents: 60606
diff changeset
  1145
  interpret comp_fun_commute "plus \<circ> single \<circ> f"
49823
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1146
    by (fact comp_fun_commute_mset_image)
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
  1147
  show ?thesis by (induct N) (simp_all add: image_mset_def ac_simps)
49823
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1148
qed
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1149
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1150
corollary image_mset_insert: "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
49823
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1151
  by simp
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1152
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1153
lemma set_image_mset [simp]: "set_mset (image_mset f M) = image f (set_mset M)"
49823
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1154
  by (induct M) simp_all
48040
4caf6cd063be add lemma set_of_image_mset
huffman
parents: 48023
diff changeset
  1155
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1156
lemma size_image_mset [simp]: "size (image_mset f M) = size M"
49823
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1157
  by (induct M) simp_all
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1158
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1159
lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
49823
1c146fa7701e avoid global interpretation
haftmann
parents: 49822
diff changeset
  1160
  by (cases M) auto
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1161
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
  1162
syntax (ASCII)
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
  1163
  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ :# _#})")
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1164
syntax
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
  1165
  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ \<in># _#})")
59813
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
  1166
translations
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
  1167
  "{#e. x \<in># M#}" \<rightleftharpoons> "CONST image_mset (\<lambda>x. e) M"
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
  1168
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
  1169
syntax (ASCII)
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
  1170
  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  ("({#_/ | _ :# _./ _#})")
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1171
syntax
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
  1172
  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  ("({#_/ | _ \<in># _./ _#})")
59813
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
  1173
translations
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
  1174
  "{#e | x\<in>#M. P#}" \<rightharpoonup> "{#e. x \<in># {# x\<in>#M. P#}#}"
59813
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
  1175
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
  1176
text \<open>
60607
d440af2e584f more symbols;
wenzelm
parents: 60606
diff changeset
  1177
  This allows to write not just filters like @{term "{#x\<in>#M. x<c#}"}
d440af2e584f more symbols;
wenzelm
parents: 60606
diff changeset
  1178
  but also images like @{term "{#x+x. x\<in>#M #}"} and @{term [source]
d440af2e584f more symbols;
wenzelm
parents: 60606
diff changeset
  1179
  "{#x+x|x\<in>#M. x<c#}"}, where the latter is currently displayed as
d440af2e584f more symbols;
wenzelm
parents: 60606
diff changeset
  1180
  @{term "{#x+x|x\<in>#M. x<c#}"}.
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
  1181
\<close>
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1182
60495
d7ff0a1df90a renamed Multiset.set_of to the canonical set_mset
nipkow
parents: 60400
diff changeset
  1183
lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
  1184
by (metis set_image_mset)
59813
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
  1185
55467
a5c9002bc54d renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
blanchet
parents: 55417
diff changeset
  1186
functor image_mset: image_mset
48023
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1187
proof -
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1188
  fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1189
  proof
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1190
    fix A
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1191
    show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1192
      by (induct A) simp_all
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1193
  qed
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1194
  show "image_mset id = id"
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1195
  proof
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1196
    fix A
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1197
    show "image_mset id A = id A"
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1198
      by (induct A) simp_all
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1199
  qed
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1200
qed
6dfe5e774012 reordered sections
huffman
parents: 48012
diff changeset
  1201
59813
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
  1202
declare
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
  1203
  image_mset.id [simp]
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
  1204
  image_mset.identity [simp]
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
  1205
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
  1206
lemma image_mset_id[simp]: "image_mset id x = x"
6320064f22bb more multiset theorems
<