src/HOL/Library/Multiset.thy
author desharna
Mon, 23 May 2022 10:13:08 +0200
changeset 75459 ec4b514bcfad
parent 75457 cbf011677235
child 75467 9e34819a7ca1
permissions -rw-r--r--
added lemma image_mset_filter_mset_swap
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
74803
825cd198d85c renamed Multiset.multp and Multiset.multeqp
desharna
parents: 74634
diff changeset
     7
    Author:     Martin Desharnais, MPI-INF Saarbruecken
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
     8
*)
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
     9
65048
805d0a9a4e37 added multiset lemma
blanchet
parents: 65047
diff changeset
    10
section \<open>(Finite) Multisets\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    11
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15072
diff changeset
    12
theory Multiset
74865
b5031a8f7718 added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset
desharna
parents: 74864
diff changeset
    13
  imports Cancellation
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15072
diff changeset
    14
begin
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    15
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    16
subsection \<open>The type of multisets\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    17
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    18
typedef 'a multiset = \<open>{f :: 'a \<Rightarrow> nat. finite {x. f x > 0}}\<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
    19
  morphisms count Abs_multiset
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    20
proof
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    21
  show \<open>(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}\<close>
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    22
    by simp
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    23
qed
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    24
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
    25
setup_lifting type_definition_multiset
19086
1b3780be6cc2 new-style definitions/abbreviations;
wenzelm
parents: 18730
diff changeset
    26
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    27
lemma count_Abs_multiset:
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    28
  \<open>count (Abs_multiset f) = f\<close> if \<open>finite {x. f x > 0}\<close>
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    29
  by (rule Abs_multiset_inverse) (simp add: that)
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    30
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    31
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
    32
  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
    33
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    34
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
    35
  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
    36
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69442
diff changeset
    37
text \<open>Preservation of the representing set \<^term>\<open>multiset\<close>.\<close>
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    38
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
    39
lemma diff_preserves_multiset:
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    40
  \<open>finite {x. 0 < M x - N x}\<close> if \<open>finite {x. 0 < M x}\<close> for M N :: \<open>'a \<Rightarrow> nat\<close>
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    41
  using that by (rule rev_finite_subset) 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
    42
41069
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
    43
lemma filter_preserves_multiset:
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    44
  \<open>finite {x. 0 < (if P x then M x else 0)}\<close> if \<open>finite {x. 0 < M x}\<close> for M N :: \<open>'a \<Rightarrow> nat\<close>
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    45
  using that by (rule rev_finite_subset) auto
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    46
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    47
lemmas in_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
    48
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
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    50
subsection \<open>Representing multisets\<close>
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    51
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    52
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
    53
48008
846ff14337a4 use transfer method for instance proof
huffman
parents: 47429
diff changeset
    54
instantiation multiset :: (type) cancel_comm_monoid_add
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    55
begin
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    56
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
    57
lift_definition zero_multiset :: \<open>'a multiset\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
    58
  is \<open>\<lambda>a. 0\<close>
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    59
  by simp
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    60
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
    61
abbreviation empty_mset :: \<open>'a multiset\<close> (\<open>{#}\<close>)
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
    62
  where \<open>empty_mset \<equiv> 0\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
    63
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
    64
lift_definition plus_multiset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
    65
  is \<open>\<lambda>M N a. M a + N a\<close>
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    66
  by simp
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    67
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
    68
lift_definition minus_multiset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
    69
  is \<open>\<lambda>M N a. M a - N a\<close>
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    70
  by (rule diff_preserves_multiset)
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59813
diff changeset
    71
48008
846ff14337a4 use transfer method for instance proof
huffman
parents: 47429
diff changeset
    72
instance
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    73
  by (standard; transfer) (simp_all add: fun_eq_iff)
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    74
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    75
end
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    76
63195
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    77
context
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    78
begin
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    79
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    80
qualified definition is_empty :: "'a multiset \<Rightarrow> bool" where
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    81
  [code_abbrev]: "is_empty A \<longleftrightarrow> A = {#}"
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    82
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    83
end
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    84
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
    85
lemma add_mset_in_multiset:
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    86
  \<open>finite {x. 0 < (if x = a then Suc (M x) else M x)}\<close>
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    87
  if \<open>finite {x. 0 < M x}\<close>
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
    88
  using that by (simp add: flip: insert_Collect)
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
    89
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
    90
lift_definition add_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
    91
  "\<lambda>a M b. if b = a then Suc (M b) else M b"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
    92
by (rule add_mset_in_multiset)
15869
3aca7f05cd12 intersection
kleing
parents: 15867
diff changeset
    93
26145
95670b6e1fa3 tuned document;
wenzelm
parents: 26143
diff changeset
    94
syntax
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    95
  "_multiset" :: "args \<Rightarrow> 'a multiset"    ("{#(_)#}")
25507
d13468d40131 added {#.,.,...#}
nipkow
parents: 25208
diff changeset
    96
translations
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
    97
  "{#x, xs#}" == "CONST add_mset x {#xs#}"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
    98
  "{#x#}" == "CONST add_mset x {#}"
25507
d13468d40131 added {#.,.,...#}
nipkow
parents: 25208
diff changeset
    99
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
   100
lemma count_empty [simp]: "count {#} a = 0"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   101
  by (simp add: zero_multiset.rep_eq)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   102
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   103
lemma count_add_mset [simp]:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   104
  "count (add_mset b A) a = (if b = a then Suc (count A a) else count A a)"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   105
  by (simp add: add_mset.rep_eq)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   106
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   107
lemma count_single: "count {#b#} a = (if b = a then 1 else 0)"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   108
  by simp
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   109
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   110
lemma
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   111
  add_mset_not_empty [simp]: \<open>add_mset a A \<noteq> {#}\<close> and
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   112
  empty_not_add_mset [simp]: "{#} \<noteq> add_mset a A"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   113
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   114
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   115
lemma add_mset_add_mset_same_iff [simp]:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   116
  "add_mset a A = add_mset a B \<longleftrightarrow> A = B"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   117
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   118
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   119
lemma add_mset_commute:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   120
  "add_mset x (add_mset y M) = add_mset y (add_mset x M)"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   121
  by (auto simp: multiset_eq_iff)
29901
f4b3f8fbf599 finiteness lemmas
nipkow
parents: 29509
diff changeset
   122
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   123
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   124
subsection \<open>Basic operations\<close>
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   125
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   126
subsubsection \<open>Conversion to set and membership\<close>
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   127
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   128
definition set_mset :: \<open>'a multiset \<Rightarrow> 'a set\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   129
  where \<open>set_mset M = {x. count M x > 0}\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   130
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   131
abbreviation member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   132
  where \<open>member_mset a M \<equiv> a \<in> set_mset M\<close>
62537
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
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   135
  member_mset  (\<open>'(\<in>#')\<close>) and
73394
2e6b2134956e follow corresponding precedence on sets
haftmann
parents: 73393
diff changeset
   136
  member_mset  (\<open>(_/ \<in># _)\<close> [50, 51] 50)
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   137
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   138
notation  (ASCII)
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   139
  member_mset  (\<open>'(:#')\<close>) and
73394
2e6b2134956e follow corresponding precedence on sets
haftmann
parents: 73393
diff changeset
   140
  member_mset  (\<open>(_/ :# _)\<close> [50, 51] 50)
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   141
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   142
abbreviation not_member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   143
  where \<open>not_member_mset a M \<equiv> a \<notin> set_mset M\<close>
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   144
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   145
notation
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   146
  not_member_mset  (\<open>'(\<notin>#')\<close>) and
73394
2e6b2134956e follow corresponding precedence on sets
haftmann
parents: 73393
diff changeset
   147
  not_member_mset  (\<open>(_/ \<notin># _)\<close> [50, 51] 50)
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   148
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   149
notation  (ASCII)
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   150
  not_member_mset  (\<open>'(~:#')\<close>) and
73394
2e6b2134956e follow corresponding precedence on sets
haftmann
parents: 73393
diff changeset
   151
  not_member_mset  (\<open>(_/ ~:# _)\<close> [50, 51] 50)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   152
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   153
context
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   154
begin
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   155
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   156
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
   157
  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
   158
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   159
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
   160
  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
   161
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   162
end
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   163
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   164
syntax
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   165
  "_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
   166
  "_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
   167
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   168
syntax  (ASCII)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   169
  "_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
   170
  "_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
   171
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   172
translations
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   173
  "\<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
   174
  "\<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
   175
71917
4c5778d8a53d should have been copied across from Set.thy as well for better printing
nipkow
parents: 71398
diff changeset
   176
print_translation \<open>
4c5778d8a53d should have been copied across from Set.thy as well for better printing
nipkow
parents: 71398
diff changeset
   177
 [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Ball\<close> \<^syntax_const>\<open>_MBall\<close>,
4c5778d8a53d should have been copied across from Set.thy as well for better printing
nipkow
parents: 71398
diff changeset
   178
  Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Bex\<close> \<^syntax_const>\<open>_MBex\<close>]
4c5778d8a53d should have been copied across from Set.thy as well for better printing
nipkow
parents: 71398
diff changeset
   179
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
4c5778d8a53d should have been copied across from Set.thy as well for better printing
nipkow
parents: 71398
diff changeset
   180
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   181
lemma count_eq_zero_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   182
  "count M x = 0 \<longleftrightarrow> x \<notin># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   183
  by (auto simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   184
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   185
lemma not_in_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   186
  "x \<notin># M \<longleftrightarrow> count M x = 0"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   187
  by (auto simp add: count_eq_zero_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   188
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   189
lemma count_greater_zero_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   190
  "count M x > 0 \<longleftrightarrow> x \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   191
  by (auto simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   192
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   193
lemma count_inI:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   194
  assumes "count M x = 0 \<Longrightarrow> False"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   195
  shows "x \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   196
proof (rule ccontr)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   197
  assume "x \<notin># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   198
  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
   199
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   200
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   201
lemma in_countE:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   202
  assumes "x \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   203
  obtains n where "count M x = Suc n"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   204
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   205
  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
   206
  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
   207
    using gr0_conv_Suc by blast
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   208
  with that show thesis .
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   209
qed
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 count_greater_eq_Suc_zero_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   212
  "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
   213
  by (simp add: Suc_le_eq)
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
lemma count_greater_eq_one_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   216
  "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
   217
  by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   218
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   219
lemma set_mset_empty [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   220
  "set_mset {#} = {}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   221
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   222
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   223
lemma set_mset_single:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   224
  "set_mset {#b#} = {b}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   225
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   226
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   227
lemma set_mset_eq_empty_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   228
  "set_mset M = {} \<longleftrightarrow> M = {#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   229
  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
   230
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   231
lemma finite_set_mset [iff]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   232
  "finite (set_mset M)"
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
   233
  using count [of M] by simp
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   234
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   235
lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close>
68406
6beb45f6cf67 utilize 'flip'
nipkow
parents: 68386
diff changeset
   236
  by (auto simp flip: count_greater_eq_Suc_zero_iff split: if_splits)
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   237
63924
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   238
lemma multiset_nonemptyE [elim]:
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   239
  assumes "A \<noteq> {#}"
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   240
  obtains x where "x \<in># A"
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   241
proof -
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   242
  have "\<exists>x. x \<in># A" by (rule ccontr) (insert assms, auto)
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   243
  with that show ?thesis by blast
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   244
qed
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   245
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   246
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   247
subsubsection \<open>Union\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   248
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   249
lemma count_union [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   250
  "count (M + N) a = count M a + count N a"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   251
  by (simp add: plus_multiset.rep_eq)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   252
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   253
lemma set_mset_union [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   254
  "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
   255
  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
   256
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   257
lemma union_mset_add_mset_left [simp]:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   258
  "add_mset a A + B = add_mset a (A + B)"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   259
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   260
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   261
lemma union_mset_add_mset_right [simp]:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   262
  "A + add_mset a B = add_mset a (A + B)"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   263
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   264
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   265
lemma add_mset_add_single: \<open>add_mset a A = A + {#a#}\<close>
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   266
  by (subst union_mset_add_mset_right, subst add.comm_neutral) standard
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   267
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   268
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   269
subsubsection \<open>Difference\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   270
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   271
instance multiset :: (type) comm_monoid_diff
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   272
  by standard (transfer; simp add: fun_eq_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   273
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   274
lemma count_diff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   275
  "count (M - N) a = count M a - count N a"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   276
  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
   277
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   278
lemma add_mset_diff_bothsides:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   279
  \<open>add_mset a M - add_mset a A = M - A\<close>
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   280
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   281
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   282
lemma in_diff_count:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   283
  "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
   284
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   285
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   286
lemma count_in_diffI:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   287
  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
   288
  shows "x \<in># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   289
proof (rule ccontr)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   290
  assume "x \<notin># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   291
  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
   292
    by (simp add: in_diff_count not_less)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   293
  with assms show False by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   294
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   295
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   296
lemma in_diff_countE:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   297
  assumes "x \<in># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   298
  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
   299
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   300
  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
   301
  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
   302
  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
   303
    using less_iff_Suc_add by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   304
  with that show thesis .
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   305
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   306
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   307
lemma in_diffD:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   308
  assumes "a \<in># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   309
  shows "a \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   310
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   311
  have "0 \<le> count N a" by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   312
  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
   313
    by (simp add: in_diff_count)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   314
  finally show ?thesis by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   315
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   316
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   317
lemma set_mset_diff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   318
  "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
   319
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   320
17161
57c69627d71a tuned some proofs;
wenzelm
parents: 15869
diff changeset
   321
lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   322
  by rule (fact Groups.diff_zero, fact Groups.zero_diff)
36903
489c1fbbb028 Multiset: renamed, added and tuned lemmas;
nipkow
parents: 36867
diff changeset
   323
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   324
lemma diff_cancel: "A - A = {#}"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   325
  by (fact Groups.diff_cancel)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   326
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   327
lemma diff_union_cancelR: "M + N - N = (M::'a multiset)"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   328
  by (fact add_diff_cancel_right')
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   329
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   330
lemma diff_union_cancelL: "N + M - N = (M::'a multiset)"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   331
  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
   332
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   333
lemma diff_right_commute:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   334
  fixes M N Q :: "'a multiset"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   335
  shows "M - N - Q = M - Q - N"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   336
  by (fact diff_right_commute)
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   337
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   338
lemma diff_add:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   339
  fixes M N Q :: "'a multiset"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   340
  shows "M - (N + Q) = M - N - Q"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   341
  by (rule sym) (fact diff_diff_add)
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   342
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   343
lemma insert_DiffM [simp]: "x \<in># M \<Longrightarrow> add_mset 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
   344
  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
   345
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   346
lemma insert_DiffM2: "x \<in># M \<Longrightarrow> (M - {#x#}) + {#x#} = M"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   347
  by simp
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   348
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   349
lemma diff_union_swap: "a \<noteq> b \<Longrightarrow> add_mset b (M - {#a#}) = add_mset b M - {#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
   350
  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
   351
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   352
lemma diff_add_mset_swap [simp]: "b \<notin># A \<Longrightarrow> add_mset b M - A = add_mset b (M - A)"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   353
  by (auto simp add: multiset_eq_iff simp: not_in_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   354
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   355
lemma diff_union_swap2 [simp]: "y \<in># M \<Longrightarrow> add_mset x M - {#y#} = add_mset x (M - {#y#})"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   356
  by (metis add_mset_diff_bothsides diff_union_swap diff_zero insert_DiffM)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   357
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   358
lemma diff_diff_add_mset [simp]: "(M::'a multiset) - N - P = M - (N + P)"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   359
  by (rule diff_diff_add)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   360
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   361
lemma diff_union_single_conv:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   362
  "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
   363
  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
   364
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   365
lemma mset_add [elim?]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   366
  assumes "a \<in># A"
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   367
  obtains B where "A = add_mset a B"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   368
proof -
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   369
  from assms have "A = add_mset a (A - {#a#})"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   370
    by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   371
  with that show thesis .
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   372
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   373
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   374
lemma union_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   375
  "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
   376
  by auto
26143
314c0bcb7df7 Added useful general lemmas from the work with the HeapMonad
bulwahn
parents: 26033
diff changeset
   377
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   378
66425
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   379
subsubsection \<open>Min and Max\<close>
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   380
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   381
abbreviation Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   382
"Min_mset m \<equiv> Min (set_mset m)"
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   383
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   384
abbreviation Max_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   385
"Max_mset m \<equiv> Max (set_mset m)"
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   386
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   387
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   388
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
   389
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
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
   391
  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
   392
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
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
   394
  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
   395
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
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
   397
  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
   398
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   399
lemma multi_self_add_other_not_self [simp]: "M = add_mset x M \<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
   400
  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
   401
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   402
lemma add_mset_remove_trivial [simp]: \<open>add_mset x M - {#x#} = M\<close>
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   403
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   404
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   405
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
   406
  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
   407
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   408
lemma diff_single_eq_union: "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = add_mset x N"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   409
  by auto
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   410
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   411
lemma union_single_eq_diff: "add_mset x M = N \<Longrightarrow> M = N - {#x#}"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   412
  unfolding add_mset_add_single[of _ M] by (fact add_implies_diff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   413
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   414
lemma union_single_eq_member: "add_mset x M = 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
   415
  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
   416
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   417
lemma add_mset_remove_trivial_If:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   418
  "add_mset a (N - {#a#}) = (if a \<in># N then N else add_mset a N)"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   419
  by (simp add: diff_single_trivial)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   420
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   421
lemma add_mset_remove_trivial_eq: \<open>N = add_mset a (N - {#a#}) \<longleftrightarrow> a \<in># N\<close>
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   422
  by (auto simp: add_mset_remove_trivial_If)
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
   423
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   424
lemma union_is_single:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   425
  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N = {#} \<or> M = {#} \<and> N = {#a#}"
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   426
  (is "?lhs = ?rhs")
46730
e3b99d0231bc tuned proofs;
wenzelm
parents: 46394
diff changeset
   427
proof
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   428
  show ?lhs if ?rhs using that by auto
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   429
  show ?rhs if ?lhs
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   430
    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
   431
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
   432
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   433
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
   434
  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
   435
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
   436
lemma add_eq_conv_diff:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   437
  "add_mset a M = add_mset b N \<longleftrightarrow> M = N \<and> a = b \<or> M = add_mset b (N - {#a#}) \<and> N = add_mset a (M - {#b#})"
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   438
  (is "?lhs \<longleftrightarrow> ?rhs")
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44339
diff changeset
   439
(* 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
   440
proof
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   441
  show ?lhs if ?rhs
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   442
    using that
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   443
    by (auto simp add: add_mset_commute[of a b])
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   444
  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
   445
  proof (cases "a = b")
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   446
    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
   447
  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
   448
    case False
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   449
    from \<open>?lhs\<close> have "a \<in># add_mset b N" 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
   450
    with False have "a \<in># N" by auto
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   451
    moreover from \<open>?lhs\<close> have "M = add_mset b N - {#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
   452
    moreover note False
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   453
    ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#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
   454
  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
   455
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
   456
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   457
lemma add_mset_eq_single [iff]: "add_mset b M = {#a#} \<longleftrightarrow> b = a \<and> M = {#}"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   458
  by (auto simp: add_eq_conv_diff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   459
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   460
lemma single_eq_add_mset [iff]: "{#a#} = add_mset b M \<longleftrightarrow> b = a \<and> M = {#}"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   461
  by (auto simp: add_eq_conv_diff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   462
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   463
lemma insert_noteq_member:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   464
  assumes BC: "add_mset b B = add_mset c C"
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
   465
   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
   466
  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
   467
proof -
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   468
  have "c \<in># add_mset c C" 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
   469
  have nc: "\<not> c \<in># {#b#}" using bnotc by simp
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   470
  then have "c \<in># add_mset b B" using BC 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
   471
  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
   472
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
   473
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
   474
lemma add_eq_conv_ex:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   475
  "(add_mset a M = add_mset b N) =
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   476
    (M = N \<and> a = b \<or> (\<exists>K. M = add_mset b K \<and> N = add_mset a K))"
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
   477
  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
   478
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   479
lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = add_mset x A"
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   480
  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
   481
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   482
lemma multiset_add_sub_el_shuffle:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   483
  assumes "c \<in># B"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   484
    and "b \<noteq> c"
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   485
  shows "add_mset b (B - {#c#}) = add_mset b B - {#c#}"
58098
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   486
proof -
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   487
  from \<open>c \<in># B\<close> obtain A where B: "B = add_mset c A"
58098
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   488
    by (blast dest: multi_member_split)
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   489
  have "add_mset b A = add_mset c (add_mset b A) - {#c#}" by simp
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   490
  then have "add_mset b A = add_mset b (add_mset c A) - {#c#}"
63794
bcec0534aeea clean argument of simp add
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63793
diff changeset
   491
    by (simp add: \<open>b \<noteq> c\<close>)
58098
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   492
  then show ?thesis using B by simp
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   493
qed
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   494
64418
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   495
lemma add_mset_eq_singleton_iff[iff]:
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   496
  "add_mset x M = {#y#} \<longleftrightarrow> M = {#} \<and> x = y"
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   497
  by auto
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   498
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
   499
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   500
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
   501
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   502
definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
65466
haftmann
parents: 65354
diff changeset
   503
  where "A \<subseteq># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   504
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   505
definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
65466
haftmann
parents: 65354
diff changeset
   506
  where "A \<subset># B \<longleftrightarrow> A \<subseteq># B \<and> A \<noteq> B"
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   507
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   508
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
   509
  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
   510
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   511
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
   512
  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
   513
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   514
notation (input)
62208
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   515
  subseteq_mset  (infix "\<le>#" 50) and
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   516
  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
   517
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   518
notation (ASCII)
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   519
  subseteq_mset  (infix "<=#" 50) and
62208
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   520
  subset_mset  (infix "<#" 50) and
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   521
  supseteq_mset  (infix ">=#" 50) and
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   522
  supset_mset  (infix ">#" 50)
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   523
73411
1f1366966296 avoid name clash
haftmann
parents: 73394
diff changeset
   524
global_interpretation subset_mset: ordering \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
1f1366966296 avoid name clash
haftmann
parents: 73394
diff changeset
   525
  by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order.trans order.antisym)
1f1366966296 avoid name clash
haftmann
parents: 73394
diff changeset
   526
73451
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   527
interpretation subset_mset: ordered_ab_semigroup_add_imp_le \<open>(+)\<close> \<open>(-)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   528
  by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
64585
2155c0c1ecb6 renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
haftmann
parents: 64531
diff changeset
   529
    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   530
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   531
interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "(+)" 0 "(-)" "(\<subseteq>#)" "(\<subset>#)"
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   532
  by standard
64585
2155c0c1ecb6 renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
haftmann
parents: 64531
diff changeset
   533
    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   534
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   535
lemma mset_subset_eqI:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   536
  "(\<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
   537
  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
   538
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   539
lemma mset_subset_eq_count:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   540
  "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
   541
  by (simp add: subseteq_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   542
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   543
lemma mset_subset_eq_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)"
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   544
  unfolding subseteq_mset_def
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   545
  apply (rule iffI)
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   546
   apply (rule exI [where x = "B - A"])
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   547
   apply (auto intro: multiset_eq_iff [THEN iffD2])
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   548
  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
   549
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   550
interpretation subset_mset: ordered_cancel_comm_monoid_diff "(+)" 0 "(\<subseteq>#)" "(\<subset>#)" "(-)"
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   551
  by standard (simp, fact mset_subset_eq_exists_conv)
64585
2155c0c1ecb6 renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
haftmann
parents: 64531
diff changeset
   552
    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   553
64017
6e7bf7678518 more multiset simp rules
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63924
diff changeset
   554
declare subset_mset.add_diff_assoc[simp] subset_mset.add_diff_assoc2[simp]
6e7bf7678518 more multiset simp rules
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63924
diff changeset
   555
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   556
lemma mset_subset_eq_mono_add_right_cancel: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   557
   by (fact subset_mset.add_le_cancel_right)
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   558
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   559
lemma mset_subset_eq_mono_add_left_cancel: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   560
   by (fact subset_mset.add_le_cancel_left)
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   561
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   562
lemma mset_subset_eq_mono_add: "(A::'a multiset) \<subseteq># B \<Longrightarrow> C \<subseteq># D \<Longrightarrow> A + C \<subseteq># B + D"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   563
   by (fact subset_mset.add_mono)
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   564
63560
3e3097ac37d1 more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63547
diff changeset
   565
lemma mset_subset_eq_add_left: "(A::'a multiset) \<subseteq># A + B"
3e3097ac37d1 more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63547
diff changeset
   566
   by simp
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   567
63560
3e3097ac37d1 more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63547
diff changeset
   568
lemma mset_subset_eq_add_right: "B \<subseteq># (A::'a multiset) + B"
3e3097ac37d1 more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63547
diff changeset
   569
   by simp
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   570
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   571
lemma single_subset_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   572
  "{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   573
  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
   574
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   575
lemma mset_subset_eq_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B"
63795
7f6128adfe67 tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63794
diff changeset
   576
  by simp
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   577
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   578
lemma mset_subset_eq_add_mset_cancel: \<open>add_mset a A \<subseteq># add_mset a B \<longleftrightarrow> A \<subseteq># B\<close>
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   579
  unfolding add_mset_add_single[of _ A] add_mset_add_single[of _ B]
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   580
  by (rule mset_subset_eq_mono_add_right_cancel)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   581
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   582
lemma multiset_diff_union_assoc:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   583
  fixes A B C D :: "'a multiset"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   584
  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
   585
  by (fact subset_mset.diff_add_assoc)
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   586
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   587
lemma mset_subset_eq_multiset_union_diff_commute:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   588
  fixes A B C D :: "'a multiset"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   589
  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
   590
  by (fact subset_mset.add_diff_assoc2)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   591
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   592
lemma diff_subset_eq_self[simp]:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   593
  "(M::'a multiset) - N \<subseteq># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   594
  by (simp add: subseteq_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   595
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   596
lemma mset_subset_eqD:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   597
  assumes "A \<subseteq># B" and "x \<in># A"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   598
  shows "x \<in># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   599
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   600
  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
   601
  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
   602
    by (simp add: subseteq_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   603
  finally show ?thesis by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   604
qed
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   605
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   606
lemma mset_subsetD:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   607
  "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   608
  by (auto intro: mset_subset_eqD [of A])
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   609
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   610
lemma set_mset_mono:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   611
  "A \<subseteq># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   612
  by (metis mset_subset_eqD subsetI)
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   613
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   614
lemma mset_subset_eq_insertD:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   615
  "add_mset x A \<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
   616
apply (rule conjI)
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   617
 apply (simp add: mset_subset_eqD)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   618
 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
   619
 apply safe
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   620
  apply (erule_tac x = a in allE)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   621
  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
   622
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
   623
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   624
lemma mset_subset_insertD:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   625
  "add_mset x A \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   626
  by (rule mset_subset_eq_insertD) simp
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   627
63831
ea7471c921f5 more simp
nipkow
parents: 63830
diff changeset
   628
lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
63795
7f6128adfe67 tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63794
diff changeset
   629
  by (simp only: subset_mset.not_less_zero)
7f6128adfe67 tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63794
diff changeset
   630
64587
8355a6e2df79 standardized notation
haftmann
parents: 64586
diff changeset
   631
lemma empty_subset_add_mset[simp]: "{#} \<subset># add_mset x M"
8355a6e2df79 standardized notation
haftmann
parents: 64586
diff changeset
   632
  by (auto intro: subset_mset.gr_zeroI)
63831
ea7471c921f5 more simp
nipkow
parents: 63830
diff changeset
   633
63795
7f6128adfe67 tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63794
diff changeset
   634
lemma empty_le: "{#} \<subseteq># A"
7f6128adfe67 tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63794
diff changeset
   635
  by (fact subset_mset.zero_le)
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   636
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   637
lemma insert_subset_eq_iff:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   638
  "add_mset a A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   639
  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
   640
  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
   641
  apply (rule ccontr)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   642
  apply (auto simp add: not_in_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   643
  done
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   644
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   645
lemma insert_union_subset_iff:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   646
  "add_mset a A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   647
  by (auto simp add: insert_subset_eq_iff subset_mset_def)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   648
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   649
lemma subset_eq_diff_conv:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   650
  "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
   651
  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
   652
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   653
lemma multi_psub_of_add_self [simp]: "A \<subset># add_mset x A"
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   654
  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
   655
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   656
lemma multi_psub_self: "A \<subset># A = False"
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   657
  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
   658
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   659
lemma mset_subset_add_mset [simp]: "add_mset x N \<subset># add_mset x M \<longleftrightarrow> N \<subset># M"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   660
  unfolding add_mset_add_single[of _ N] add_mset_add_single[of _ M]
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   661
  by (fact subset_mset.add_less_cancel_right)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   662
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   663
lemma mset_subset_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   664
  by (auto simp: subset_mset_def elim: mset_add)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   665
64077
6d770c2dc60d more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64076
diff changeset
   666
lemma Diff_eq_empty_iff_mset: "A - B = {#} \<longleftrightarrow> A \<subseteq># B"
6d770c2dc60d more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64076
diff changeset
   667
  by (auto simp: multiset_eq_iff subseteq_mset_def)
6d770c2dc60d more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64076
diff changeset
   668
64418
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   669
lemma add_mset_subseteq_single_iff[iff]: "add_mset a M \<subseteq># {#b#} \<longleftrightarrow> M = {#} \<and> a = b"
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   670
proof
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   671
  assume A: "add_mset a M \<subseteq># {#b#}"
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   672
  then have \<open>a = b\<close>
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   673
    by (auto dest: mset_subset_eq_insertD)
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   674
  then show "M={#} \<and> a=b"
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   675
    using A by (simp add: mset_subset_eq_add_mset_cancel)
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   676
qed simp
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   677
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   678
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   679
subsubsection \<open>Intersection and bounded union\<close>
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   680
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   681
definition inter_mset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>  (infixl \<open>\<inter>#\<close> 70)
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   682
  where \<open>A \<inter># B = A - (A - B)\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   683
73451
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   684
lemma count_inter_mset [simp]:
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   685
  \<open>count (A \<inter># B) x = min (count A x) (count B x)\<close>
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   686
  by (simp add: inter_mset_def)
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   687
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   688
(*global_interpretation subset_mset: semilattice_order \<open>(\<inter>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   689
  by standard (simp_all add: multiset_eq_iff subseteq_mset_def subset_mset_def min_def)*)
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   690
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   691
interpretation subset_mset: semilattice_inf \<open>(\<inter>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
73451
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   692
  by standard (simp_all add: multiset_eq_iff subseteq_mset_def)
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   693
  \<comment> \<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
   694
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   695
definition union_mset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>  (infixl \<open>\<union>#\<close> 70)
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   696
  where \<open>A \<union># B = A + (B - A)\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   697
73451
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   698
lemma count_union_mset [simp]:
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   699
  \<open>count (A \<union># B) x = max (count A x) (count B x)\<close>
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   700
  by (simp add: union_mset_def)
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   701
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   702
global_interpretation subset_mset: semilattice_neutr_order \<open>(\<union>#)\<close> \<open>{#}\<close> \<open>(\<supseteq>#)\<close> \<open>(\<supset>#)\<close>
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   703
  apply standard
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   704
      apply (simp_all add: multiset_eq_iff subseteq_mset_def subset_mset_def max_def)
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   705
   apply (auto simp add: le_antisym dest: sym)
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   706
   apply (metis nat_le_linear)+
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   707
  done
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
   708
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   709
interpretation subset_mset: semilattice_sup \<open>(\<union>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   710
proof -
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   711
  have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   712
    by arith
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   713
  show "class.semilattice_sup (\<union>#) (\<subseteq>#) (\<subset>#)"
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   714
    by standard (auto simp add: union_mset_def subseteq_mset_def)
64585
2155c0c1ecb6 renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
haftmann
parents: 64531
diff changeset
   715
qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   716
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   717
interpretation subset_mset: bounded_lattice_bot "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)"
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   718
  "(\<union>#)" "{#}"
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   719
  by standard auto
64585
2155c0c1ecb6 renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
haftmann
parents: 64531
diff changeset
   720
    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   721
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   722
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   723
subsubsection \<open>Additional intersection facts\<close>
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   724
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   725
lemma set_mset_inter [simp]:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   726
  "set_mset (A \<inter># B) = set_mset A \<inter> set_mset B"
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   727
  by (simp only: set_mset_def) auto
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   728
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   729
lemma diff_intersect_left_idem [simp]:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   730
  "M - M \<inter># N = M - N"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   731
  by (simp add: multiset_eq_iff min_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   732
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   733
lemma diff_intersect_right_idem [simp]:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   734
  "M - N \<inter># M = M - N"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   735
  by (simp add: multiset_eq_iff min_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   736
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   737
lemma multiset_inter_single[simp]: "a \<noteq> b \<Longrightarrow> {#a#} \<inter># {#b#} = {#}"
46730
e3b99d0231bc tuned proofs;
wenzelm
parents: 46394
diff changeset
   738
  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
   739
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   740
lemma multiset_union_diff_commute:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   741
  assumes "B \<inter># C = {#}"
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   742
  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
   743
proof (rule multiset_eqI)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   744
  fix x
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   745
  from assms have "min (count B x) (count C x) = 0"
46730
e3b99d0231bc tuned proofs;
wenzelm
parents: 46394
diff changeset
   746
    by (auto simp add: multiset_eq_iff)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   747
  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
   748
    unfolding min_def by (auto split: if_splits)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   749
  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
   750
    by auto
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   751
qed
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   752
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   753
lemma disjunct_not_in:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   754
  "A \<inter># B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)" (is "?P \<longleftrightarrow> ?Q")
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   755
proof
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   756
  assume ?P
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   757
  show ?Q
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   758
  proof
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   759
    fix a
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   760
    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
   761
      by (simp add: multiset_eq_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   762
    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
   763
      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
   764
    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
   765
      by (simp add: not_in_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   766
  qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   767
next
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   768
  assume ?Q
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   769
  show ?P
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   770
  proof (rule multiset_eqI)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   771
    fix a
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   772
    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
   773
      by (auto simp add: not_in_iff)
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   774
    then show "count (A \<inter># B) a = count {#} a"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   775
      by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   776
  qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   777
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   778
64077
6d770c2dc60d more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64076
diff changeset
   779
lemma inter_mset_empty_distrib_right: "A \<inter># (B + C) = {#} \<longleftrightarrow> A \<inter># B = {#} \<and> A \<inter># C = {#}"
6d770c2dc60d more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64076
diff changeset
   780
  by (meson disjunct_not_in union_iff)
6d770c2dc60d more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64076
diff changeset
   781
6d770c2dc60d more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64076
diff changeset
   782
lemma inter_mset_empty_distrib_left: "(A + B) \<inter># C = {#} \<longleftrightarrow> A \<inter># C = {#} \<and> B \<inter># C = {#}"
6d770c2dc60d more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64076
diff changeset
   783
  by (meson disjunct_not_in union_iff)
6d770c2dc60d more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64076
diff changeset
   784
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   785
lemma add_mset_inter_add_mset [simp]:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   786
  "add_mset a A \<inter># add_mset a B = add_mset a (A \<inter># B)"
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   787
  by (rule multiset_eqI) simp
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   788
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   789
lemma add_mset_disjoint [simp]:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   790
  "add_mset a A \<inter># B = {#} \<longleftrightarrow> a \<notin># B \<and> A \<inter># B = {#}"
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   791
  "{#} = add_mset a A \<inter># B \<longleftrightarrow> a \<notin># B \<and> {#} = A \<inter># B"
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   792
  by (auto simp: disjunct_not_in)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   794
lemma disjoint_add_mset [simp]:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   795
  "B \<inter># add_mset a A = {#} \<longleftrightarrow> a \<notin># B \<and> B \<inter># A = {#}"
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   796
  "{#} = A \<inter># add_mset b B \<longleftrightarrow> b \<notin># A \<and> {#} = A \<inter># B"
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   797
  by (auto simp: disjunct_not_in)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   798
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   799
lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) \<inter># N = M \<inter># N"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   800
  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
   801
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   802
lemma inter_add_left2: "x \<in># N \<Longrightarrow> (add_mset x M) \<inter># N = add_mset x (M \<inter># (N - {#x#}))"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   803
  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
   804
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   805
lemma inter_add_right1: "\<not> x \<in># N \<Longrightarrow> N \<inter># (add_mset x M) = N \<inter># M"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   806
  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
   807
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   808
lemma inter_add_right2: "x \<in># N \<Longrightarrow> N \<inter># (add_mset x M) = add_mset x ((N - {#x#}) \<inter># M)"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   809
  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
   810
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   811
lemma disjunct_set_mset_diff:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   812
  assumes "M \<inter># N = {#}"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   813
  shows "set_mset (M - N) = set_mset M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   814
proof (rule set_eqI)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   815
  fix a
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   816
  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
   817
    by (simp add: disjunct_not_in)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   818
  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
   819
    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
   820
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   821
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   822
lemma at_most_one_mset_mset_diff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   823
  assumes "a \<notin># M - {#a#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   824
  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
   825
  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
   826
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   827
lemma more_than_one_mset_mset_diff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   828
  assumes "a \<in># M - {#a#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   829
  shows "set_mset (M - {#a#}) = set_mset M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   830
proof (rule set_eqI)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   831
  fix b
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   832
  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
   833
  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
   834
    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
   835
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   836
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   837
lemma inter_iff:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   838
  "a \<in># A \<inter># B \<longleftrightarrow> a \<in># A \<and> a \<in># B"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   839
  by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   840
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   841
lemma inter_union_distrib_left:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   842
  "A \<inter># B + C = (A + C) \<inter># (B + C)"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   843
  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
   844
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   845
lemma inter_union_distrib_right:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   846
  "C + A \<inter># B = (C + A) \<inter># (C + B)"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   847
  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
   848
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   849
lemma inter_subset_eq_union:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   850
  "A \<inter># B \<subseteq># A + B"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   851
  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
   852
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   853
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   854
subsubsection \<open>Additional bounded union facts\<close>
63795
7f6128adfe67 tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63794
diff changeset
   855
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   856
lemma set_mset_sup [simp]:
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   857
  \<open>set_mset (A \<union># B) = set_mset A \<union> set_mset B\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   858
  by (simp only: set_mset_def) (auto simp add: less_max_iff_disj)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   859
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   860
lemma sup_union_left1 [simp]: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) \<union># N = add_mset x (M \<union># N)"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   861
  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
   862
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   863
lemma sup_union_left2: "x \<in># N \<Longrightarrow> (add_mset x M) \<union># N = add_mset x (M \<union># (N - {#x#}))"
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   864
  by (simp add: multiset_eq_iff)
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   865
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   866
lemma sup_union_right1 [simp]: "\<not> x \<in># N \<Longrightarrow> N \<union># (add_mset x M) = add_mset x (N \<union># M)"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   867
  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
   868
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   869
lemma sup_union_right2: "x \<in># N \<Longrightarrow> N \<union># (add_mset x M) = add_mset x ((N - {#x#}) \<union># M)"
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   870
  by (simp add: multiset_eq_iff)
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   871
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   872
lemma sup_union_distrib_left:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   873
  "A \<union># B + C = (A + C) \<union># (B + C)"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   874
  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
   875
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   876
lemma union_sup_distrib_right:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   877
  "C + A \<union># B = (C + A) \<union># (C + B)"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   878
  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
   879
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   880
lemma union_diff_inter_eq_sup:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   881
  "A + B - A \<inter># B = A \<union># B"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   882
  by (auto simp add: multiset_eq_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   883
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   884
lemma union_diff_sup_eq_inter:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   885
  "A + B - A \<union># B = A \<inter># B"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   886
  by (auto simp add: multiset_eq_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   887
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   888
lemma add_mset_union:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   889
  \<open>add_mset a A \<union># add_mset a B = add_mset a (A \<union># B)\<close>
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   890
  by (auto simp: multiset_eq_iff max_def)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   891
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   892
63908
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   893
subsection \<open>Replicate and repeat operations\<close>
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   894
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   895
definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   896
  "replicate_mset n x = (add_mset x ^^ n) {#}"
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   897
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   898
lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}"
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   899
  unfolding replicate_mset_def by simp
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   900
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   901
lemma replicate_mset_Suc [simp]: "replicate_mset (Suc n) x = add_mset x (replicate_mset n x)"
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   902
  unfolding replicate_mset_def by (induct n) (auto intro: add.commute)
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   903
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   904
lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   905
  unfolding replicate_mset_def by (induct n) auto
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   906
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   907
lift_definition repeat_mset :: \<open>nat \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   908
  is \<open>\<lambda>n M a. n * M a\<close> by simp
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   909
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   910
lemma count_repeat_mset [simp]: "count (repeat_mset i A) a = i * count A a"
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   911
  by transfer rule
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   912
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   913
lemma repeat_mset_0 [simp]:
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   914
  \<open>repeat_mset 0 M = {#}\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   915
  by transfer simp
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   916
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   917
lemma repeat_mset_Suc [simp]:
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   918
  \<open>repeat_mset (Suc n) M = M + repeat_mset n M\<close>
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   919
  by transfer simp
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   920
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   921
lemma repeat_mset_right [simp]: "repeat_mset a (repeat_mset b A) = repeat_mset (a * b) A"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   922
  by (auto simp: multiset_eq_iff left_diff_distrib')
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   923
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   924
lemma left_diff_repeat_mset_distrib': \<open>repeat_mset (i - j) u = repeat_mset i u - repeat_mset j u\<close>
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   925
  by (auto simp: multiset_eq_iff left_diff_distrib')
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   926
63908
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   927
lemma left_add_mult_distrib_mset:
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   928
  "repeat_mset i u + (repeat_mset j u + k) = repeat_mset (i+j) u + k"
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   929
  by (auto simp: multiset_eq_iff add_mult_distrib)
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   930
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   931
lemma repeat_mset_distrib:
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   932
  "repeat_mset (m + n) A = repeat_mset m A + repeat_mset n A"
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   933
  by (auto simp: multiset_eq_iff Nat.add_mult_distrib)
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   934
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   935
lemma repeat_mset_distrib2[simp]:
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   936
  "repeat_mset n (A + B) = repeat_mset n A + repeat_mset n B"
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   937
  by (auto simp: multiset_eq_iff add_mult_distrib2)
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   938
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   939
lemma repeat_mset_replicate_mset[simp]:
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   940
  "repeat_mset n {#a#} = replicate_mset n a"
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   941
  by (auto simp: multiset_eq_iff)
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   942
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   943
lemma repeat_mset_distrib_add_mset[simp]:
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   944
  "repeat_mset n (add_mset a A) = replicate_mset n a + repeat_mset n A"
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   945
  by (auto simp: multiset_eq_iff)
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   946
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   947
lemma repeat_mset_empty[simp]: "repeat_mset n {#} = {#}"
73393
716d256259d5 consolidated names
haftmann
parents: 73327
diff changeset
   948
  by transfer simp
63908
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   949
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   950
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   951
subsubsection \<open>Simprocs\<close>
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   952
65031
52e2c99f3711 use the cancellation simprocs directly
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65029
diff changeset
   953
lemma repeat_mset_iterate_add: \<open>repeat_mset n M = iterate_add n M\<close>
52e2c99f3711 use the cancellation simprocs directly
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65029
diff changeset
   954
  unfolding iterate_add_def by (induction n) auto
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   955
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   956
lemma mset_subseteq_add_iff1:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   957
  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subseteq># n)"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   958
  by (auto simp add: subseteq_mset_def nat_le_add_iff1)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   959
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   960
lemma mset_subseteq_add_iff2:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   961
  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (m \<subseteq># repeat_mset (j-i) u + n)"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   962
  by (auto simp add: subseteq_mset_def nat_le_add_iff2)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   963
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   964
lemma mset_subset_add_iff1:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   965
  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subset># n)"
65031
52e2c99f3711 use the cancellation simprocs directly
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65029
diff changeset
   966
  unfolding subset_mset_def repeat_mset_iterate_add
52e2c99f3711 use the cancellation simprocs directly
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65029
diff changeset
   967
  by (simp add: iterate_add_eq_add_iff1 mset_subseteq_add_iff1[unfolded repeat_mset_iterate_add])
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   968
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   969
lemma mset_subset_add_iff2:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   970
  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (m \<subset># repeat_mset (j-i) u + n)"
65031
52e2c99f3711 use the cancellation simprocs directly
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65029
diff changeset
   971
  unfolding subset_mset_def repeat_mset_iterate_add
52e2c99f3711 use the cancellation simprocs directly
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65029
diff changeset
   972
  by (simp add: iterate_add_eq_add_iff2 mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add])
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   973
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
   974
ML_file \<open>multiset_simprocs.ML\<close>
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   975
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   976
lemma add_mset_replicate_mset_safe[cancelation_simproc_pre]: \<open>NO_MATCH {#} M \<Longrightarrow> add_mset a M = {#a#} + M\<close>
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   977
  by simp
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   978
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   979
declare repeat_mset_iterate_add[cancelation_simproc_pre]
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   980
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   981
declare iterate_add_distrib[cancelation_simproc_pre]
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   982
declare repeat_mset_iterate_add[symmetric, cancelation_simproc_post]
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   983
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   984
declare add_mset_not_empty[cancelation_simproc_eq_elim]
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   985
    empty_not_add_mset[cancelation_simproc_eq_elim]
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   986
    subset_mset.le_zero_eq[cancelation_simproc_eq_elim]
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   987
    empty_not_add_mset[cancelation_simproc_eq_elim]
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   988
    add_mset_not_empty[cancelation_simproc_eq_elim]
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   989
    subset_mset.le_zero_eq[cancelation_simproc_eq_elim]
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   990
    le_zero_eq[cancelation_simproc_eq_elim]
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   991
65027
2b8583507891 renaming multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64911
diff changeset
   992
simproc_setup mseteq_cancel
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   993
  ("(l::'a multiset) + m = n" | "(l::'a multiset) = m + n" |
63908
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   994
   "add_mset a m = n" | "m = add_mset a n" |
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   995
   "replicate_mset p a = n" | "m = replicate_mset p a" |
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   996
   "repeat_mset p m = n" | "m = repeat_mset p m") =
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   997
  \<open>fn phi => Cancel_Simprocs.eq_cancel\<close>
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   998
65027
2b8583507891 renaming multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64911
diff changeset
   999
simproc_setup msetsubset_cancel
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1000
  ("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
63908
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
  1001
   "add_mset a m \<subset># n" | "m \<subset># add_mset a n" |
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
  1002
   "replicate_mset p r \<subset># n" | "m \<subset># replicate_mset p r" |
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
  1003
   "repeat_mset p m \<subset># n" | "m \<subset># repeat_mset p m") =
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1004
  \<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close>
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1005
65027
2b8583507891 renaming multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64911
diff changeset
  1006
simproc_setup msetsubset_eq_cancel
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1007
  ("(l::'a multiset) + m \<subseteq># n" | "(l::'a multiset) \<subseteq># m + n" |
63908
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
  1008
   "add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n" |
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
  1009
   "replicate_mset p r \<subseteq># n" | "m \<subseteq># replicate_mset p r" |
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
  1010
   "repeat_mset p m \<subseteq># n" | "m \<subseteq># repeat_mset p m") =
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1011
  \<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close>
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1012
65027
2b8583507891 renaming multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64911
diff changeset
  1013
simproc_setup msetdiff_cancel
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1014
  ("((l::'a multiset) + m) - n" | "(l::'a multiset) - (m + n)" |
63908
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
  1015
   "add_mset a m - n" | "m - add_mset a n" |
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
  1016
   "replicate_mset p r - n" | "m - replicate_mset p r" |
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
  1017
   "repeat_mset p m - n" | "m - repeat_mset p m") =
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
  1018
  \<open>fn phi => Cancel_Simprocs.diff_cancel\<close>
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1019
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1020
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1021
subsubsection \<open>Conditionally complete lattice\<close>
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1022
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1023
instantiation multiset :: (type) Inf
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1024
begin
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1025
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1026
lift_definition Inf_multiset :: "'a multiset set \<Rightarrow> 'a multiset" is
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1027
  "\<lambda>A i. if A = {} then 0 else Inf ((\<lambda>f. f i) ` A)"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1028
proof -
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1029
  fix A :: "('a \<Rightarrow> nat) set"
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1030
  assume *: "\<And>f. f \<in> A \<Longrightarrow> finite {x. 0 < f x}"
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1031
  show \<open>finite {i. 0 < (if A = {} then 0 else INF f\<in>A. f i)}\<close>
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1032
  proof (cases "A = {}")
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1033
    case False
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1034
    then obtain f where "f \<in> A" by blast
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1035
    hence "{i. Inf ((\<lambda>f. f i) ` A) > 0} \<subseteq> {i. f i > 0}"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1036
      by (auto intro: less_le_trans[OF _ cInf_lower])
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1037
    moreover from \<open>f \<in> A\<close> * have "finite \<dots>" by simp
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1038
    ultimately have "finite {i. Inf ((\<lambda>f. f i) ` A) > 0}" by (rule finite_subset)
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1039
    with False show ?thesis by simp
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1040
  qed simp_all
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1041
qed
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1042
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1043
instance ..
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1044
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1045
end
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1046
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1047
lemma Inf_multiset_empty: "Inf {} = {#}"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1048
  by transfer simp_all
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1049
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1050
lemma count_Inf_multiset_nonempty: "A \<noteq> {} \<Longrightarrow> count (Inf A) x = Inf ((\<lambda>X. count X x) ` A)"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1051
  by transfer simp_all
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1052
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1053
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1054
instantiation multiset :: (type) Sup
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1055
begin
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1056
63360
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1057
definition Sup_multiset :: "'a multiset set \<Rightarrow> 'a multiset" where
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1058
  "Sup_multiset A = (if A \<noteq> {} \<and> subset_mset.bdd_above A then
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1059
           Abs_multiset (\<lambda>i. Sup ((\<lambda>X. count X i) ` A)) else {#})"
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1060
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1061
lemma Sup_multiset_empty: "Sup {} = {#}"
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1062
  by (simp add: Sup_multiset_def)
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1063
73451
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
  1064
lemma Sup_multiset_unbounded: "\<not> subset_mset.bdd_above A \<Longrightarrow> Sup A = {#}"
63360
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1065
  by (simp add: Sup_multiset_def)
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1066
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1067
instance ..
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1068
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1069
end
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1070
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1071
lemma bdd_above_multiset_imp_bdd_above_count:
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1072
  assumes "subset_mset.bdd_above (A :: 'a multiset set)"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1073
  shows   "bdd_above ((\<lambda>X. count X x) ` A)"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1074
proof -
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1075
  from assms obtain Y where Y: "\<forall>X\<in>A. X \<subseteq># Y"
73451
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
  1076
    by (meson subset_mset.bdd_above.E)
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1077
  hence "count X x \<le> count Y x" if "X \<in> A" for X
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1078
    using that by (auto intro: mset_subset_eq_count)
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1079
  thus ?thesis by (intro bdd_aboveI[of _ "count Y x"]) auto
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1080
qed
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1081
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1082
lemma bdd_above_multiset_imp_finite_support:
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1083
  assumes "A \<noteq> {}" "subset_mset.bdd_above (A :: 'a multiset set)"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1084
  shows   "finite (\<Union>X\<in>A. {x. count X x > 0})"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1085
proof -
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1086
  from assms obtain Y where Y: "\<forall>X\<in>A. X \<subseteq># Y"
73451
99950990c7b3 prefer more direct interpretation
haftmann
parents: 73411
diff changeset
  1087
    by (meson subset_mset.bdd_above.E)
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1088
  hence "count X x \<le> count Y x" if "X \<in> A" for X x
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1089
    using that by (auto intro: mset_subset_eq_count)
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1090
  hence "(\<Union>X\<in>A. {x. count X x > 0}) \<subseteq> {x. count Y x > 0}"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1091
    by safe (erule less_le_trans)
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1092
  moreover have "finite \<dots>" by simp
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1093
  ultimately show ?thesis by (rule finite_subset)
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1094
qed
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1095
63360
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1096
lemma Sup_multiset_in_multiset:
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1097
  \<open>finite {i. 0 < (SUP M\<in>A. count M i)}\<close>
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1098
  if \<open>A \<noteq> {}\<close> \<open>subset_mset.bdd_above A\<close>
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1099
proof -
63360
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1100
  have "{i. Sup ((\<lambda>X. count X i) ` A) > 0} \<subseteq> (\<Union>X\<in>A. {i. 0 < count X i})"
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1101
  proof safe
69260
0a9688695a1b removed relics of ASCII syntax for indexed big operators
haftmann
parents: 69107
diff changeset
  1102
    fix i assume pos: "(SUP X\<in>A. count X i) > 0"
63360
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1103
    show "i \<in> (\<Union>X\<in>A. {i. 0 < count X i})"
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1104
    proof (rule ccontr)
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1105
      assume "i \<notin> (\<Union>X\<in>A. {i. 0 < count X i})"
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1106
      hence "\<forall>X\<in>A. count X i \<le> 0" by (auto simp: count_eq_zero_iff)
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1107
      with that have "(SUP X\<in>A. count X i) \<le> 0"
63360
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1108
        by (intro cSup_least bdd_above_multiset_imp_bdd_above_count) auto
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1109
      with pos show False by simp
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1110
    qed
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1111
  qed
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1112
  moreover from that have "finite \<dots>"
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1113
    by (rule bdd_above_multiset_imp_finite_support)
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1114
  ultimately show "finite {i. Sup ((\<lambda>X. count X i) ` A) > 0}"
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1115
    by (rule finite_subset)
63360
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1116
qed
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1117
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1118
lemma count_Sup_multiset_nonempty:
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1119
  \<open>count (Sup A) x = (SUP X\<in>A. count X x)\<close>
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1120
  if \<open>A \<noteq> {}\<close> \<open>subset_mset.bdd_above A\<close>
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73052
diff changeset
  1121
  using that by (simp add: Sup_multiset_def Sup_multiset_in_multiset count_Abs_multiset)
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1122
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
  1123
interpretation subset_mset: conditionally_complete_lattice Inf Sup "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)"
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1124
proof
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1125
  fix X :: "'a multiset" and A
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1126
  assume "X \<in> A"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1127
  show "Inf A \<subseteq># X"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1128
  proof (rule mset_subset_eqI)
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1129
    fix x
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1130
    from \<open>X \<in> A\<close> have "A \<noteq> {}" by auto
69260
0a9688695a1b removed relics of ASCII syntax for indexed big operators
haftmann
parents: 69107
diff changeset
  1131
    hence "count (Inf A) x = (INF X\<in>A. count X x)"
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1132
      by (simp add: count_Inf_multiset_nonempty)
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1133
    also from \<open>X \<in> A\<close> have "\<dots> \<le> count X x"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1134
      by (intro cInf_lower) simp_all
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1135
    finally show "count (Inf A) x \<le> count X x" .
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1136
  qed
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1137
next
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1138
  fix X :: "'a multiset" and A
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1139
  assume nonempty: "A \<noteq> {}" and le: "\<And>Y. Y \<in> A \<Longrightarrow> X \<subseteq># Y"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1140
  show "X \<subseteq># Inf A"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eber&#