src/HOL/Library/Multiset.thy
author nipkow
Mon, 19 Feb 2018 13:56:16 +0100
changeset 67656 59feb83c6ab9
parent 67398 5eb932e604a2
child 68249 949d93804740
permissions -rw-r--r--
added lemma
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Library/Multiset.thy
15072
4861bf6af0b4 new material courtesy of Norbert Voelker
paulson
parents: 14981
diff changeset
     2
    Author:     Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
55129
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 54868
diff changeset
     3
    Author:     Andrei Popescu, TU Muenchen
59813
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
     4
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
     5
    Author:     Dmitriy Traytel, TU Muenchen
6320064f22bb more multiset theorems
blanchet
parents: 59807
diff changeset
     6
    Author:     Mathias Fleury, MPII
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
     7
*)
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
     8
65048
805d0a9a4e37 added multiset lemma
blanchet
parents: 65047
diff changeset
     9
section \<open>(Finite) Multisets\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    10
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15072
diff changeset
    11
theory Multiset
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
    12
imports Cancellation
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15072
diff changeset
    13
begin
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    14
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    15
subsection \<open>The type of multisets\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    16
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    17
definition "multiset = {f :: 'a \<Rightarrow> nat. finite {x. f x > 0}}"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    18
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    19
typedef 'a multiset = "multiset :: ('a \<Rightarrow> nat) set"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    20
  morphisms count Abs_multiset
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45608
diff changeset
    21
  unfolding multiset_def
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    22
proof
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45608
diff changeset
    23
  show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    24
qed
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    25
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
    26
setup_lifting type_definition_multiset
19086
1b3780be6cc2 new-style definitions/abbreviations;
wenzelm
parents: 18730
diff changeset
    27
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    28
lemma multiset_eq_iff: "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
    29
  by (simp only: count_inject [symmetric] fun_eq_iff)
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    30
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    31
lemma multiset_eqI: "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39301
diff changeset
    32
  using multiset_eq_iff by auto
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    33
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    34
text \<open>Preservation of the representing set @{term multiset}.\<close>
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    35
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    36
lemma const0_in_multiset: "(\<lambda>a. 0) \<in> multiset"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    37
  by (simp add: multiset_def)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    38
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    39
lemma only1_in_multiset: "(\<lambda>b. if b = a then n else 0) \<in> multiset"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    40
  by (simp add: multiset_def)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    41
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    42
lemma union_preserves_multiset: "M \<in> multiset \<Longrightarrow> N \<in> multiset \<Longrightarrow> (\<lambda>a. M a + N a) \<in> multiset"
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    43
  by (simp add: multiset_def)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    44
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    45
lemma diff_preserves_multiset:
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    46
  assumes "M \<in> multiset"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    47
  shows "(\<lambda>a. M a - N a) \<in> multiset"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    48
proof -
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    49
  have "{x. N x < M x} \<subseteq> {x. 0 < M x}"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    50
    by auto
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    51
  with assms show ?thesis
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    52
    by (auto simp add: multiset_def intro: finite_subset)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    53
qed
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    54
41069
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
    55
lemma filter_preserves_multiset:
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    56
  assumes "M \<in> multiset"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    57
  shows "(\<lambda>x. if P x then M x else 0) \<in> multiset"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    58
proof -
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    59
  have "{x. (P x \<longrightarrow> 0 < M x) \<and> P x} \<subseteq> {x. 0 < M x}"
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    60
    by auto
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    61
  with assms show ?thesis
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    62
    by (auto simp add: multiset_def intro: finite_subset)
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    63
qed
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    64
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    65
lemmas in_multiset = const0_in_multiset only1_in_multiset
41069
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
    66
  union_preserves_multiset diff_preserves_multiset filter_preserves_multiset
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    67
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    68
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    69
subsection \<open>Representing multisets\<close>
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    70
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
    71
text \<open>Multiset enumeration\<close>
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    72
48008
846ff14337a4 use transfer method for instance proof
huffman
parents: 47429
diff changeset
    73
instantiation multiset :: (type) cancel_comm_monoid_add
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    74
begin
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    75
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
    76
lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0"
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
    77
by (rule const0_in_multiset)
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    78
34943
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    79
abbreviation Mempty :: "'a multiset" ("{#}") where
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
    80
  "Mempty \<equiv> 0"
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    81
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    82
lift_definition plus_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
    83
by (rule union_preserves_multiset)
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    84
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
    85
lift_definition minus_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59813
diff changeset
    86
by (rule diff_preserves_multiset)
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59813
diff changeset
    87
48008
846ff14337a4 use transfer method for instance proof
huffman
parents: 47429
diff changeset
    88
instance
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
    89
  by (standard; transfer; simp add: fun_eq_iff)
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    90
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25507
diff changeset
    91
end
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
    92
63195
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    93
context
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    94
begin
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    95
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    96
qualified definition is_empty :: "'a multiset \<Rightarrow> bool" where
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    97
  [code_abbrev]: "is_empty A \<longleftrightarrow> A = {#}"
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    98
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
    99
end
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63099
diff changeset
   100
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   101
lemma add_mset_in_multiset:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   102
  assumes M: \<open>M \<in> multiset\<close>
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   103
  shows \<open>(\<lambda>b. if b = a then Suc (M b) else M b) \<in> multiset\<close>
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   104
  using assms by (simp add: multiset_def insert_Collect[symmetric])
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   105
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   106
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
   107
  "\<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
   108
by (rule add_mset_in_multiset)
15869
3aca7f05cd12 intersection
kleing
parents: 15867
diff changeset
   109
26145
95670b6e1fa3 tuned document;
wenzelm
parents: 26143
diff changeset
   110
syntax
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   111
  "_multiset" :: "args \<Rightarrow> 'a multiset"    ("{#(_)#}")
25507
d13468d40131 added {#.,.,...#}
nipkow
parents: 25208
diff changeset
   112
translations
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   113
  "{#x, xs#}" == "CONST add_mset x {#xs#}"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   114
  "{#x#}" == "CONST add_mset x {#}"
25507
d13468d40131 added {#.,.,...#}
nipkow
parents: 25208
diff changeset
   115
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
   116
lemma count_empty [simp]: "count {#} a = 0"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   117
  by (simp add: zero_multiset.rep_eq)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   118
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   119
lemma count_add_mset [simp]:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   120
  "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
   121
  by (simp add: add_mset.rep_eq)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   122
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   123
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
   124
  by simp
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   125
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   126
lemma
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   127
  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
   128
  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
   129
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   130
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   131
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
   132
  "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
   133
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   134
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   135
lemma add_mset_commute:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   136
  "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
   137
  by (auto simp: multiset_eq_iff)
29901
f4b3f8fbf599 finiteness lemmas
nipkow
parents: 29509
diff changeset
   138
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   139
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   140
subsection \<open>Basic operations\<close>
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   141
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   142
subsubsection \<open>Conversion to set and membership\<close>
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   143
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   144
definition set_mset :: "'a multiset \<Rightarrow> 'a set"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   145
  where "set_mset M = {x. count M x > 0}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   146
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   147
abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   148
  where "Melem a M \<equiv> a \<in> set_mset M"
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   149
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   150
notation
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   151
  Melem  ("'(\<in>#')") and
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   152
  Melem  ("(_/ \<in># _)" [51, 51] 50)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   153
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   154
notation  (ASCII)
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   155
  Melem  ("'(:#')") and
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   156
  Melem  ("(_/ :# _)" [51, 51] 50)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   157
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   158
abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   159
  where "not_Melem a M \<equiv> a \<notin> set_mset M"
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   160
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   161
notation
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   162
  not_Melem  ("'(\<notin>#')") and
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   163
  not_Melem  ("(_/ \<notin># _)" [51, 51] 50)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   164
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   165
notation  (ASCII)
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   166
  not_Melem  ("'(~:#')") and
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   167
  not_Melem  ("(_/ ~:# _)" [51, 51] 50)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   168
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   169
context
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   170
begin
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   171
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   172
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
   173
  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
   174
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   175
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
   176
  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
   177
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   178
end
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   179
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   180
syntax
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   181
  "_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
   182
  "_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
   183
62537
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   184
syntax  (ASCII)
7a9aa69f9b38 syntax for multiset membership modelled after syntax for set membership
haftmann
parents: 62430
diff changeset
   185
  "_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
   186
  "_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
   187
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   188
translations
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   189
  "\<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
   190
  "\<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
   191
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   192
lemma count_eq_zero_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   193
  "count M x = 0 \<longleftrightarrow> x \<notin># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   194
  by (auto simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   195
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   196
lemma not_in_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   197
  "x \<notin># M \<longleftrightarrow> count M x = 0"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   198
  by (auto simp add: count_eq_zero_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   199
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   200
lemma count_greater_zero_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   201
  "count M x > 0 \<longleftrightarrow> x \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   202
  by (auto simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   203
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   204
lemma count_inI:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   205
  assumes "count M x = 0 \<Longrightarrow> False"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   206
  shows "x \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   207
proof (rule ccontr)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   208
  assume "x \<notin># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   209
  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
   210
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   211
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   212
lemma in_countE:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   213
  assumes "x \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   214
  obtains n where "count M x = Suc n"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   215
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   216
  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
   217
  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
   218
    using gr0_conv_Suc by blast
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   219
  with that show thesis .
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   220
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   221
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   222
lemma count_greater_eq_Suc_zero_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   223
  "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
   224
  by (simp add: Suc_le_eq)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   225
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   226
lemma count_greater_eq_one_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   227
  "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
   228
  by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   229
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   230
lemma set_mset_empty [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   231
  "set_mset {#} = {}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   232
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   233
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   234
lemma set_mset_single:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   235
  "set_mset {#b#} = {b}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   236
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   237
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   238
lemma set_mset_eq_empty_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   239
  "set_mset M = {} \<longleftrightarrow> M = {#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   240
  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
   241
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   242
lemma finite_set_mset [iff]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   243
  "finite (set_mset M)"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   244
  using count [of M] by (simp add: multiset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   245
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   246
lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close>
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   247
  by (auto simp del: count_greater_eq_Suc_zero_iff
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   248
      simp: count_greater_eq_Suc_zero_iff[symmetric] split: if_splits)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   249
63924
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   250
lemma multiset_nonemptyE [elim]:
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   251
  assumes "A \<noteq> {#}"
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   252
  obtains x where "x \<in># A"
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   253
proof -
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   254
  have "\<exists>x. x \<in># A" by (rule ccontr) (insert assms, auto)
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   255
  with that show ?thesis by blast
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   256
qed
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63922
diff changeset
   257
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   258
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   259
subsubsection \<open>Union\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   260
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   261
lemma count_union [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   262
  "count (M + N) a = count M a + count N a"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   263
  by (simp add: plus_multiset.rep_eq)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   264
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   265
lemma set_mset_union [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   266
  "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
   267
  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
   268
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   269
lemma union_mset_add_mset_left [simp]:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   270
  "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
   271
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   272
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   273
lemma union_mset_add_mset_right [simp]:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   274
  "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
   275
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   276
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   277
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
   278
  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
   279
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   280
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   281
subsubsection \<open>Difference\<close>
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   282
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   283
instance multiset :: (type) comm_monoid_diff
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   284
  by standard (transfer; simp add: fun_eq_iff)
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_diff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   287
  "count (M - N) a = count M a - count N a"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   288
  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
   289
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   290
lemma add_mset_diff_bothsides:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   291
  \<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
   292
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   293
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   294
lemma in_diff_count:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   295
  "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
   296
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   297
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   298
lemma count_in_diffI:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   299
  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
   300
  shows "x \<in># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   301
proof (rule ccontr)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   302
  assume "x \<notin># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   303
  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
   304
    by (simp add: in_diff_count not_less)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   305
  with assms show False by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   306
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   307
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   308
lemma in_diff_countE:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   309
  assumes "x \<in># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   310
  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
   311
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   312
  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
   313
  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
   314
  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
   315
    using less_iff_Suc_add by auto
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   316
  with that show thesis .
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   317
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   318
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   319
lemma in_diffD:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   320
  assumes "a \<in># M - N"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   321
  shows "a \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   322
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   323
  have "0 \<le> count N a" by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   324
  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
   325
    by (simp add: in_diff_count)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   326
  finally show ?thesis by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   327
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   328
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   329
lemma set_mset_diff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   330
  "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
   331
  by (simp add: set_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   332
17161
57c69627d71a tuned some proofs;
wenzelm
parents: 15869
diff changeset
   333
lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   334
  by rule (fact Groups.diff_zero, fact Groups.zero_diff)
36903
489c1fbbb028 Multiset: renamed, added and tuned lemmas;
nipkow
parents: 36867
diff changeset
   335
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   336
lemma diff_cancel: "A - A = {#}"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   337
  by (fact Groups.diff_cancel)
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   338
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   339
lemma diff_union_cancelR: "M + N - N = (M::'a multiset)"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   340
  by (fact add_diff_cancel_right')
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   341
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   342
lemma diff_union_cancelL: "N + M - N = (M::'a multiset)"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   343
  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
   344
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   345
lemma diff_right_commute:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   346
  fixes M N Q :: "'a multiset"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   347
  shows "M - N - Q = M - Q - N"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   348
  by (fact diff_right_commute)
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   349
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   350
lemma diff_add:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   351
  fixes M N Q :: "'a multiset"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   352
  shows "M - (N + Q) = M - N - Q"
52289
83ce5d2841e7 type class for confined subtraction
haftmann
parents: 51623
diff changeset
   353
  by (rule sym) (fact diff_diff_add)
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   354
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   355
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
   356
  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
   357
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   358
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
   359
  by simp
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   360
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   361
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
   362
  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
   363
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   364
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
   365
  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
   366
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   367
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
   368
  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
   369
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   370
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
   371
  by (rule diff_diff_add)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   372
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   373
lemma diff_union_single_conv:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   374
  "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
   375
  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
   376
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   377
lemma mset_add [elim?]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   378
  assumes "a \<in># A"
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   379
  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
   380
proof -
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   381
  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
   382
    by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   383
  with that show thesis .
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   384
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   385
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   386
lemma union_iff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   387
  "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
   388
  by auto
26143
314c0bcb7df7 Added useful general lemmas from the work with the HeapMonad
bulwahn
parents: 26033
diff changeset
   389
10249
e4d13d8a9011 Multisets (from HOL/Induct/Multiset and friends);
wenzelm
parents:
diff changeset
   390
66425
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   391
subsubsection \<open>Min and Max\<close>
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   392
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   393
abbreviation Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   394
"Min_mset m \<equiv> Min (set_mset m)"
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   395
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   396
abbreviation Max_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   397
"Max_mset m \<equiv> Max (set_mset m)"
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   398
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66313
diff changeset
   399
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   400
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
   401
e97b22500a5c cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents: 33102
diff changeset
   402
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
   403
  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
   404
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
   405
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
   406
  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
   407
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
   408
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
   409
  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
   410
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   411
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
   412
  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
   413
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   414
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
   415
  by (auto simp: multiset_eq_iff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   416
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   417
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
   418
  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
   419
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   420
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
   421
  by auto
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   422
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   423
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
   424
  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
   425
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   426
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
   427
  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
   428
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   429
lemma add_mset_remove_trivial_If:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   430
  "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
   431
  by (simp add: diff_single_trivial)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   432
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   433
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
   434
  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
   435
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   436
lemma union_is_single:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   437
  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N = {#} \<or> M = {#} \<and> N = {#a#}"
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   438
  (is "?lhs = ?rhs")
46730
e3b99d0231bc tuned proofs;
wenzelm
parents: 46394
diff changeset
   439
proof
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   440
  show ?lhs if ?rhs using that by auto
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   441
  show ?rhs if ?lhs
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   442
    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
   443
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
   444
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   445
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
   446
  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
   447
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
lemma add_eq_conv_diff:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   449
  "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
   450
  (is "?lhs \<longleftrightarrow> ?rhs")
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44339
diff changeset
   451
(* 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
   452
proof
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   453
  show ?lhs if ?rhs
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   454
    using that
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   455
    by (auto simp add: add_mset_commute[of a b])
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   456
  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
   457
  proof (cases "a = b")
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   458
    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
   459
  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
   460
    case False
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   461
    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
   462
    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
   463
    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
   464
    moreover note False
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   465
    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
   466
  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
   467
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
   468
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   469
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
   470
  by (auto simp: add_eq_conv_diff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   471
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   472
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
   473
  by (auto simp: add_eq_conv_diff)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   474
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   475
lemma insert_noteq_member:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   476
  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
   477
   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
   478
  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
   479
proof -
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   480
  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
   481
  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
   482
  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
   483
  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
   484
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
   485
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
   486
lemma add_eq_conv_ex:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   487
  "(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
   488
    (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
   489
  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
   490
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   491
lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = add_mset x A"
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   492
  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
   493
58425
246985c6b20b simpler proof
blanchet
parents: 58247
diff changeset
   494
lemma multiset_add_sub_el_shuffle:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   495
  assumes "c \<in># B"
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   496
    and "b \<noteq> c"
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   497
  shows "add_mset b (B - {#c#}) = add_mset b B - {#c#}"
58098
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   498
proof -
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   499
  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
   500
    by (blast dest: multi_member_split)
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   501
  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
   502
  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
   503
    by (simp add: \<open>b \<noteq> c\<close>)
58098
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   504
  then show ?thesis using B by simp
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   505
qed
ff478d85129b inlined unused definition
haftmann
parents: 58035
diff changeset
   506
64418
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   507
lemma add_mset_eq_singleton_iff[iff]:
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   508
  "add_mset x M = {#y#} \<longleftrightarrow> M = {#} \<and> x = y"
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   509
  by auto
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   510
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
   511
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60400
diff changeset
   512
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
   513
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   514
definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
65466
haftmann
parents: 65354
diff changeset
   515
  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
   516
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   517
definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
65466
haftmann
parents: 65354
diff changeset
   518
  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
   519
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   520
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
   521
  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
   522
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   523
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
   524
  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
   525
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   526
notation (input)
62208
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   527
  subseteq_mset  (infix "\<le>#" 50) and
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   528
  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
   529
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   530
notation (ASCII)
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61890
diff changeset
   531
  subseteq_mset  (infix "<=#" 50) and
62208
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   532
  subset_mset  (infix "<#" 50) and
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   533
  supseteq_mset  (infix ">=#" 50) and
ad43b3ab06e4 added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents: 62082
diff changeset
   534
  supset_mset  (infix ">#" 50)
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   535
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   536
interpretation subset_mset: ordered_ab_semigroup_add_imp_le "(+)" "(-)" "(\<subseteq>#)" "(\<subset>#)"
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   537
  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
   538
    \<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
   539
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   540
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
   541
  by standard
64585
2155c0c1ecb6 renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
haftmann
parents: 64531
diff changeset
   542
    \<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
   543
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   544
lemma mset_subset_eqI:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   545
  "(\<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
   546
  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
   547
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   548
lemma mset_subset_eq_count:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   549
  "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
   550
  by (simp add: subseteq_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   551
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   552
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
   553
  unfolding subseteq_mset_def
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   554
  apply (rule iffI)
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   555
   apply (rule exI [where x = "B - A"])
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   556
   apply (auto intro: multiset_eq_iff [THEN iffD2])
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   557
  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
   558
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   559
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
   560
  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
   561
    \<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
   562
64017
6e7bf7678518 more multiset simp rules
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63924
diff changeset
   563
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
   564
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   565
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
   566
   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
   567
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   568
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
   569
   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
   570
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   571
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
   572
   by (fact subset_mset.add_mono)
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   573
63560
3e3097ac37d1 more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63547
diff changeset
   574
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
   575
   by simp
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   576
63560
3e3097ac37d1 more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63547
diff changeset
   577
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
   578
   by simp
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   579
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   580
lemma single_subset_iff [simp]:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   581
  "{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   582
  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
   583
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   584
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
   585
  by simp
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   586
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   587
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
   588
  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
   589
  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
   590
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   591
lemma multiset_diff_union_assoc:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   592
  fixes A B C D :: "'a multiset"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   593
  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
   594
  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
   595
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   596
lemma mset_subset_eq_multiset_union_diff_commute:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   597
  fixes A B C D :: "'a multiset"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   598
  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
   599
  by (fact subset_mset.add_diff_assoc2)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   600
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   601
lemma diff_subset_eq_self[simp]:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   602
  "(M::'a multiset) - N \<subseteq># M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   603
  by (simp add: subseteq_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   604
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   605
lemma mset_subset_eqD:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   606
  assumes "A \<subseteq># B" and "x \<in># A"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   607
  shows "x \<in># B"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   608
proof -
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   609
  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
   610
  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
   611
    by (simp add: subseteq_mset_def)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   612
  finally show ?thesis by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   613
qed
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   614
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   615
lemma mset_subsetD:
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   616
  "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
   617
  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
   618
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   619
lemma set_mset_mono:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   620
  "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
   621
  by (metis mset_subset_eqD subsetI)
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   622
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   623
lemma mset_subset_eq_insertD:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   624
  "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
   625
apply (rule conjI)
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   626
 apply (simp add: mset_subset_eqD)
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   627
 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
   628
 apply safe
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   629
  apply (erule_tac x = a in allE)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   630
  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
   631
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
   632
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   633
lemma mset_subset_insertD:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   634
  "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
   635
  by (rule mset_subset_eq_insertD) simp
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   636
63831
ea7471c921f5 more simp
nipkow
parents: 63830
diff changeset
   637
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
   638
  by (simp only: subset_mset.not_less_zero)
7f6128adfe67 tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63794
diff changeset
   639
64587
8355a6e2df79 standardized notation
haftmann
parents: 64586
diff changeset
   640
lemma empty_subset_add_mset[simp]: "{#} \<subset># add_mset x M"
8355a6e2df79 standardized notation
haftmann
parents: 64586
diff changeset
   641
  by (auto intro: subset_mset.gr_zeroI)
63831
ea7471c921f5 more simp
nipkow
parents: 63830
diff changeset
   642
63795
7f6128adfe67 tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63794
diff changeset
   643
lemma empty_le: "{#} \<subseteq># A"
7f6128adfe67 tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63794
diff changeset
   644
  by (fact subset_mset.zero_le)
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   645
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   646
lemma insert_subset_eq_iff:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   647
  "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
   648
  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
   649
  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
   650
  apply (rule ccontr)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   651
  apply (auto simp add: not_in_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   652
  done
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   653
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   654
lemma insert_union_subset_iff:
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   655
  "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
   656
  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
   657
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   658
lemma subset_eq_diff_conv:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   659
  "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
   660
  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
   661
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   662
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
   663
  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
   664
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   665
lemma multi_psub_self: "A \<subset># A = False"
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   666
  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
   667
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   668
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
   669
  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
   670
  by (fact subset_mset.add_less_cancel_right)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   671
63310
caaacf37943f normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63290
diff changeset
   672
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
   673
  by (auto simp: subset_mset_def elim: mset_add)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   674
64077
6d770c2dc60d more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64076
diff changeset
   675
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
   676
  by (auto simp: multiset_eq_iff subseteq_mset_def)
6d770c2dc60d more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64076
diff changeset
   677
64418
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   678
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
   679
proof
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   680
  assume A: "add_mset a M \<subseteq># {#b#}"
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   681
  then have \<open>a = b\<close>
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   682
    by (auto dest: mset_subset_eq_insertD)
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   683
  then show "M={#} \<and> a=b"
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   684
    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
   685
qed simp
91eae3a1be51 more lemmas
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64272
diff changeset
   686
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   687
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   688
subsubsection \<open>Intersection and bounded union\<close>
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   689
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   690
definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "\<inter>#" 70) where
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   691
  multiset_inter_def: "inf_subset_mset A B = A - (A - B)"
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   692
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   693
interpretation subset_mset: semilattice_inf inf_subset_mset "(\<subseteq>#)" "(\<subset>#)"
46921
aa862ff8a8a9 some proof indentation;
wenzelm
parents: 46756
diff changeset
   694
proof -
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   695
  have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   696
    by arith
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   697
  show "class.semilattice_inf (\<inter>#) (\<subseteq>#) (\<subset>#)"
60678
17ba2df56dee tuned proofs;
wenzelm
parents: 60613
diff changeset
   698
    by standard (auto simp add: multiset_inter_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
   699
qed \<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
   700
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   701
definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "\<union>#" 70)
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   702
  where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close>
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   703
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   704
interpretation subset_mset: semilattice_sup sup_subset_mset "(\<subseteq>#)" "(\<subset>#)"
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   705
proof -
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   706
  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
   707
    by arith
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   708
  show "class.semilattice_sup (\<union>#) (\<subseteq>#) (\<subset>#)"
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   709
    by standard (auto simp add: sup_subset_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
   710
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
   711
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   712
interpretation subset_mset: bounded_lattice_bot "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)"
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67332
diff changeset
   713
  "(\<union>#)" "{#}"
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   714
  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
   715
    \<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
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   717
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   718
subsubsection \<open>Additional intersection facts\<close>
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   719
41069
6fabc0414055 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents: 40968
diff changeset
   720
lemma multiset_inter_count [simp]:
60606
e5cb9271e339 more symbols;
wenzelm
parents: 60515
diff changeset
   721
  fixes A B :: "'a multiset"
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   722
  shows "count (A \<inter># B) x = min (count A x) (count B x)"
47429
ec64d94cbf9c multiset operations are defined with lift_definitions;
bulwahn
parents: 47308
diff changeset
   723
  by (simp add: multiset_inter_def)
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
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"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   727
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] multiset_inter_count) simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   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
63831
ea7471c921f5 more simp
nipkow
parents: 63830
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)"
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   787
  by (metis add_mset_add_single add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   788
      subset_mset.diff_add_assoc2)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   789
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   790
lemma add_mset_disjoint [simp]:
63919
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 = {#}"
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   792
  "{#} = 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
   793
  by (auto simp: disjunct_not_in)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   794
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   795
lemma disjoint_add_mset [simp]:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   796
  "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
   797
  "{#} = 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
   798
  by (auto simp: disjunct_not_in)
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   799
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   800
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
   801
  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
   802
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   803
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
   804
  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
   805
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   806
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
   807
  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
   808
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   809
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
   810
  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
   811
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   812
lemma disjunct_set_mset_diff:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   813
  assumes "M \<inter># N = {#}"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   814
  shows "set_mset (M - N) = set_mset M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   815
proof (rule set_eqI)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   816
  fix a
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   817
  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
   818
    by (simp add: disjunct_not_in)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   819
  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
   820
    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
   821
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   822
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   823
lemma at_most_one_mset_mset_diff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   824
  assumes "a \<notin># M - {#a#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   825
  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
   826
  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
   827
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   828
lemma more_than_one_mset_mset_diff:
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   829
  assumes "a \<in># M - {#a#}"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   830
  shows "set_mset (M - {#a#}) = set_mset M"
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   831
proof (rule set_eqI)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   832
  fix b
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   833
  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
   834
  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
   835
    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
   836
qed
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   837
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   838
lemma inter_iff:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   839
  "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
   840
  by simp
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   841
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   842
lemma inter_union_distrib_left:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   843
  "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
   844
  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
   845
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   846
lemma inter_union_distrib_right:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   847
  "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
   848
  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
   849
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   850
lemma inter_subset_eq_union:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   851
  "A \<inter># B \<subseteq># A + B"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   852
  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
   853
35268
04673275441a switched notations for pointwise and multiset order
haftmann
parents: 35028
diff changeset
   854
64076
9f089287687b tuning multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64075
diff changeset
   855
subsubsection \<open>Additional bounded union facts\<close>
63795
7f6128adfe67 tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63794
diff changeset
   856
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62651
diff changeset
   857
lemma sup_subset_mset_count [simp]: \<comment> \<open>FIXME irregular fact name\<close>
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   858
  "count (A \<union># B) x = max (count A x) (count B x)"
60397
f8a513fedb31 Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 59999
diff changeset
   859
  by (simp add: sup_subset_mset_def)
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   860
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   861
lemma set_mset_sup [simp]:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   862
  "set_mset (A \<union># B) = set_mset A \<union> set_mset B"
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   863
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   864
    (auto simp add: not_in_iff elim: mset_add)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   865
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   866
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
   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_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
   870
  by (simp add: multiset_eq_iff)
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   871
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   872
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
   873
  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
   874
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   875
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
   876
  by (simp add: multiset_eq_iff)
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   877
62430
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   878
lemma sup_union_distrib_left:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   879
  "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
   880
  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
   881
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   882
lemma union_sup_distrib_right:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   883
  "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
   884
  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
   885
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   886
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
   887
  "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
   888
  by (auto simp add: multiset_eq_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   889
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   890
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
   891
  "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
   892
  by (auto simp add: multiset_eq_iff)
9527ff088c15 more succint formulation of membership for multisets, similar to lists;
haftmann
parents: 62390
diff changeset
   893
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   894
lemma add_mset_union:
63919
9aed2da07200 # after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63908
diff changeset
   895
  \<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
   896
  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
   897
51623
1194b438426a sup on multisets
haftmann
parents: 51600
diff changeset
   898
63908
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   899
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
   900
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   901
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
   902
  "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
   903
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   904
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
   905
  unfolding replicate_mset_def by simp
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   906
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   907
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
   908
  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
   909
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   910
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
   911
  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
   912
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   913
fun repeat_mset :: "nat \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   914
  "repeat_mset 0 _ = {#}" |
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   915
  "repeat_mset (Suc n) A = A + repeat_mset n A"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   916
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   917
lemma count_repeat_mset [simp]: "count (repeat_mset i A) a = i * count A a"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   918
  by (induction i) auto
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   919
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   920
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
   921
  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
   922
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   923
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
   924
  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
   925
63908
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   926
lemma left_add_mult_distrib_mset:
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   927
  "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
   928
  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
   929
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   930
lemma repeat_mset_distrib:
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   931
  "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
   932
  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
   933
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   934
lemma repeat_mset_distrib2[simp]:
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   935
  "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
   936
  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
   937
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   938
lemma repeat_mset_replicate_mset[simp]:
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   939
  "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
   940
  by (auto simp: multiset_eq_iff)
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   941
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   942
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
   943
  "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
   944
  by (auto simp: multiset_eq_iff)
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   945
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   946
lemma repeat_mset_empty[simp]: "repeat_mset n {#} = {#}"
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   947
  by (induction n) simp_all
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   948
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
subsubsection \<open>Simprocs\<close>
ca41b6670904 support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63882
diff changeset
   951
65031
52e2c99f3711 use the cancellation simprocs directly
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65029
diff changeset
   952
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
   953
  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
   954
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   955
lemma mset_subseteq_add_iff1:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   956
  "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
   957
  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
   958
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   959
lemma mset_subseteq_add_iff2:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   960
  "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
   961
  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
   962
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   963
lemma mset_subset_add_iff1:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   964
  "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
   965
  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
   966
  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
   967
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   968
lemma mset_subset_add_iff2:
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   969
  "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
   970
  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
   971
  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
   972
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   973
ML_file "multiset_simprocs.ML"
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   974
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   975
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
   976
  by simp
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   977
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   978
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
   979
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   980
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
   981
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
   982
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 65027
diff changeset
   983
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
   984
    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
   985
    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
   986
    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
   987
    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
   988
    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
   989
    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
65027
2b8583507891 renaming multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64911
diff changeset
   991
simproc_setup mseteq_cancel
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   992
  ("(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
   993
   "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
   994
   "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
   995
   "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
   996
  \<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
   997
65027
2b8583507891 renaming multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64911
diff changeset
   998
simproc_setup msetsubset_cancel
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
   999
  ("(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
  1000
   "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
  1001
   "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
  1002
   "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
  1003
  \<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
  1004
65027
2b8583507891 renaming multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64911
diff changeset
  1005
simproc_setup msetsubset_eq_cancel
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1006
  ("(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
  1007
   "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
  1008
   "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
  1009
   "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
  1010
  \<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
  1011
65027
2b8583507891 renaming multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64911
diff changeset
  1012
simproc_setup msetdiff_cancel
63793
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1013
  ("((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
  1014
   "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
  1015
   "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
  1016
   "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
  1017
  \<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
  1018
e68a0b651eb5 add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63689
diff changeset
  1019
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1020
subsubsection \<open>Conditionally complete lattice\<close>
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1021
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1022
instantiation multiset :: (type) Inf
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1023
begin
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1024
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1025
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
  1026
  "\<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
  1027
proof -
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1028
  fix A :: "('a \<Rightarrow> nat) set" assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<in> multiset"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1029
  have "finite {i. (if A = {} then 0 else Inf ((\<lambda>f. f i) ` A)) > 0}" unfolding multiset_def
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1030
  proof (cases "A = {}")
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1031
    case False
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1032
    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
  1033
    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
  1034
      by (auto intro: less_le_trans[OF _ cInf_lower])
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1035
    moreover from \<open>f \<in> A\<close> * have "finite \<dots>" by (simp add: multiset_def)
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1036
    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
  1037
    with False show ?thesis by simp
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1038
  qed simp_all
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1039
  thus "(\<lambda>i. if A = {} then 0 else INF f:A. f i) \<in> multiset" by (simp add: multiset_def)
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1040
qed
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1041
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1042
instance ..
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1043
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1044
end
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1045
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1046
lemma Inf_multiset_empty: "Inf {} = {#}"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1047
  by transfer simp_all
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1048
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1049
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
  1050
  by transfer simp_all
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1051
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
instantiation multiset :: (type) Sup
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1054
begin
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1055
63360
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1056
definition Sup_multiset :: "'a multiset set \<Rightarrow> 'a multiset" where
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1057
  "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
  1058
           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
  1059
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1060
lemma Sup_multiset_empty: "Sup {} = {#}"
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1061
  by (simp add: Sup_multiset_def)
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1062
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1063
lemma Sup_multiset_unbounded: "\<not>subset_mset.bdd_above A \<Longrightarrow> Sup A = {#}"
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1064
  by (simp add: Sup_multiset_def)
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1065
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1066
instance ..
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1067
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1068
end
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1069
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"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1076
    by (auto simp: subset_mset.bdd_above_def)
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"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1087
    by (auto simp: subset_mset.bdd_above_def)
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:
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1097
  assumes "A \<noteq> {}" "subset_mset.bdd_above A"
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1098
  shows   "(\<lambda>i. SUP X:A. count X i) \<in> multiset"
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1099
  unfolding multiset_def
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1100
proof
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1101
  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
  1102
  proof safe
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1103
    fix i assume pos: "(SUP X:A. count X i) > 0"
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1104
    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
  1105
    proof (rule ccontr)
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1106
      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
  1107
      hence "\<forall>X\<in>A. count X i \<le> 0" by (auto simp: count_eq_zero_iff)
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1108
      with assms have "(SUP X:A. count X i) \<le> 0"
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1109
        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
  1110
      with pos show False by simp
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1111
    qed
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1112
  qed
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1113
  moreover from assms have "finite \<dots>" by (rule bdd_above_multiset_imp_finite_support)
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1114
  ultimately show "finite {i. Sup ((\<lambda>X. count X i) ` A) > 0}" by (rule finite_subset)
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1115
qed
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1116
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1117
lemma count_Sup_multiset_nonempty:
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1118
  assumes "A \<noteq> {}" "subset_mset.bdd_above A"
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1119
  shows   "count (Sup A) x = (SUP X:A. count X x)"
63360
65a9eb946ff2 Tuned multiset lattice
Manuel Eberl <eberlm@in.tum.de>
parents: 63358
diff changeset
  1120
  using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset)
63358
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset
  1121
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
a500677d4cec Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents: 63310
diff changeset