author  blanchet 
Fri, 24 Jan 2014 11:51:45 +0100  
changeset 55129  26bd1cba3ab5 
parent 54868  bab6cade3cc5 
child 55417  01fbfb60c33e 
permissions  rwrr 
10249  1 
(* Title: HOL/Library/Multiset.thy 
15072  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 
10249  4 
*) 
5 

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

6 
header {* (Finite) multisets *} 
10249  7 

15131  8 
theory Multiset 
51599
1559e9266280
optionalized very specific code setup for multisets
haftmann
parents:
51548
diff
changeset

9 
imports Main 
15131  10 
begin 
10249  11 

12 
subsection {* The type of multisets *} 

13 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45608
diff
changeset

14 
definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45608
diff
changeset

15 

49834  16 
typedef 'a multiset = "multiset :: ('a => 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

17 
morphisms count Abs_multiset 
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45608
diff
changeset

18 
unfolding multiset_def 
10249  19 
proof 
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45608
diff
changeset

20 
show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp 
10249  21 
qed 
22 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

23 
setup_lifting type_definition_multiset 
19086  24 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

25 
abbreviation Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where 
25610  26 
"a :# M == 0 < count M a" 
27 

26145  28 
notation (xsymbols) 
29 
Melem (infix "\<in>#" 50) 

10249  30 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

31 
lemma 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

32 
"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

33 
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

34 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

35 
lemma multiset_eqI: 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

36 
"(\<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

37 
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

38 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

39 
text {* 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
\medskip Preservation of the representing set @{term 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

41 
*} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

42 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
lemma const0_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

44 
"(\<lambda>a. 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

45 
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

46 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
lemma only1_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 
"(\<lambda>b. if b = a then n 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

49 
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

50 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
lemma union_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

52 
"M \<in> multiset \<Longrightarrow> N \<in> multiset \<Longrightarrow> (\<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

53 
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

54 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

55 
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

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>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

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. 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

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 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

65 
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

66 
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

67 
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

68 
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

69 
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

70 
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

71 
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

72 
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

73 
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

74 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

75 
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

76 
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

77 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

78 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
subsection {* Representing multisets *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

81 
text {* Multiset enumeration *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

82 

48008  83 
instantiation multiset :: (type) cancel_comm_monoid_add 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

84 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

85 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

86 
lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0" 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

87 
by (rule const0_in_multiset) 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

88 

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

89 
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

90 
"Mempty \<equiv> 0" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

91 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

92 
lift_definition plus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)" 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

93 
by (rule union_preserves_multiset) 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

94 

48008  95 
instance 
96 
by default (transfer, simp add: fun_eq_iff)+ 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

97 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

98 
end 
10249  99 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

100 
lift_definition single :: "'a => 'a multiset" is "\<lambda>a b. if b = a then 1 else 0" 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

101 
by (rule only1_in_multiset) 
15869  102 

26145  103 
syntax 
26176  104 
"_multiset" :: "args => 'a multiset" ("{#(_)#}") 
25507  105 
translations 
106 
"{#x, xs#}" == "{#x#} + {#xs#}" 

107 
"{#x#}" == "CONST single x" 

108 

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

109 
lemma count_empty [simp]: "count {#} a = 0" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

110 
by (simp add: zero_multiset.rep_eq) 
10249  111 

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

112 
lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

113 
by (simp add: single.rep_eq) 
29901  114 

10249  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 
subsection {* Basic operations *} 
10249  117 

118 
subsubsection {* Union *} 

119 

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

120 
lemma count_union [simp]: "count (M + N) a = count M a + count N a" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

121 
by (simp add: plus_multiset.rep_eq) 
10249  122 

123 

124 
subsubsection {* Difference *} 

125 

49388  126 
instantiation multiset :: (type) comm_monoid_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

127 
begin 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

128 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

129 
lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a  N a" 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

130 
by (rule diff_preserves_multiset) 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

131 

49388  132 
instance 
133 
by default (transfer, simp add: 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

134 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

135 
end 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

136 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

137 
lemma count_diff [simp]: "count (M  N) a = count M a  count N a" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

138 
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

139 

17161  140 
lemma diff_empty [simp]: "M  {#} = M \<and> {#}  M = {#}" 
52289  141 
by rule (fact Groups.diff_zero, fact Groups.zero_diff) 
36903  142 

143 
lemma diff_cancel[simp]: "A  A = {#}" 

52289  144 
by (fact Groups.diff_cancel) 
10249  145 

36903  146 
lemma diff_union_cancelR [simp]: "M + N  N = (M::'a multiset)" 
52289  147 
by (fact add_diff_cancel_right') 
10249  148 

36903  149 
lemma diff_union_cancelL [simp]: "N + M  N = (M::'a multiset)" 
52289  150 
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

151 

52289  152 
lemma diff_right_commute: 
153 
"(M::'a multiset)  N  Q = M  Q  N" 

154 
by (fact diff_right_commute) 

155 

156 
lemma diff_add: 

157 
"(M::'a multiset)  (N + Q) = M  N  Q" 

158 
by (rule sym) (fact diff_diff_add) 

159 

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

160 
lemma insert_DiffM: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

161 
"x \<in># M \<Longrightarrow> {#x#} + (M  {#x#}) = M" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

162 
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

163 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

164 
lemma insert_DiffM2 [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

165 
"x \<in># M \<Longrightarrow> M  {#x#} + {#x#} = M" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

166 
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

167 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

168 
lemma diff_union_swap: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

169 
"a \<noteq> b \<Longrightarrow> M  {#a#} + {#b#} = M + {#b#}  {#a#}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

170 
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

171 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

172 
lemma diff_union_single_conv: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

173 
"a \<in># J \<Longrightarrow> I + J  {#a#} = I + (J  {#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

174 
by (simp add: multiset_eq_iff) 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

175 

10249  176 

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

177 
subsubsection {* Equality of multisets *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

178 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

179 
lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

180 
by (simp add: multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

181 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

182 
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

183 
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

184 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

185 
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

186 
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

187 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

188 
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

189 
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

190 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

191 
lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

192 
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

193 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

194 
lemma diff_single_trivial: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

195 
"\<not> x \<in># M \<Longrightarrow> 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

196 
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

197 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

198 
lemma diff_single_eq_union: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

199 
"x \<in># M \<Longrightarrow> M  {#x#} = N \<longleftrightarrow> M = N + {#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

200 
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

201 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

202 
lemma union_single_eq_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

203 
"M + {#x#} = N \<Longrightarrow> M = N  {#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

204 
by (auto dest: sym) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

205 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

206 
lemma union_single_eq_member: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

207 
"M + {#x#} = N \<Longrightarrow> x \<in># N" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

208 
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

209 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

210 
lemma union_is_single: 
46730  211 
"M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs") 
212 
proof 

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

213 
assume ?rhs then show ?lhs 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

214 
next 
46730  215 
assume ?lhs then show ?rhs 
216 
by (simp add: multiset_eq_iff split:if_splits) (metis add_is_1) 

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

217 
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

218 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

219 
lemma single_is_union: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

220 
"{#a#} = M + N \<longleftrightarrow> {#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

221 
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

222 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

223 
lemma 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

224 
"M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N  {#a#} + {#b#} \<and> N = M  {#b#} + {#a#}" (is "?lhs = ?rhs") 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44339
diff
changeset

225 
(* 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

226 
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

227 
assume ?rhs then show ?lhs 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

228 
by (auto simp add: add_assoc add_commute [of "{#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

229 
(drule sym, simp add: add_assoc [symmetric]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

230 
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

231 
assume ?lhs 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

232 
show ?rhs 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

233 
proof (cases "a = 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

234 
case True with `?lhs` show ?thesis 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

235 
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

236 
case False 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

237 
from `?lhs` have "a \<in># N + {#b#}" by (rule union_single_eq_member) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

238 
with False have "a \<in># N" 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

239 
moreover from `?lhs` have "M = N + {#b#}  {#a#}" by (rule union_single_eq_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

240 
moreover note False 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

241 
ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"] diff_union_swap) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

242 
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

243 
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

244 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

245 
lemma insert_noteq_member: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

246 
assumes BC: "B + {#b#} = C + {#c#}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

247 
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

248 
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

249 
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

250 
have "c \<in># C + {#c#}" by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

251 
have nc: "\<not> c \<in># {#b#}" using bnotc by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

252 
then have "c \<in># B + {#b#}" using BC by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

253 
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

254 
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

255 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

256 
lemma add_eq_conv_ex: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

257 
"(M + {#a#} = N + {#b#}) = 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

258 
(M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

259 
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

260 

51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

261 
lemma multi_member_split: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

262 
"x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

263 
by (rule_tac x = "M  {#x#}" in exI, simp) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

264 

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

265 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

266 
subsubsection {* Pointwise ordering induced by count *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

267 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

268 
instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

269 
begin 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

270 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

271 
lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)" 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

272 
by simp 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

273 
lemmas mset_le_def = less_eq_multiset_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

274 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

275 
definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

276 
mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> 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

277 

46921  278 
instance 
279 
by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym) 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

280 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

281 
end 
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

282 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

283 
lemma mset_less_eqI: 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

284 
"(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le> 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

285 
by (simp add: mset_le_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

286 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

287 
lemma mset_le_exists_conv: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

288 
"(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + 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

289 
apply (unfold mset_le_def, rule iffI, rule_tac x = "B  A" in exI) 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

290 
apply (auto intro: multiset_eq_iff [THEN iffD2]) 
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

291 
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

292 

52289  293 
instance multiset :: (type) ordered_cancel_comm_monoid_diff 
294 
by default (simp, fact mset_le_exists_conv) 

295 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

296 
lemma mset_le_mono_add_right_cancel [simp]: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

297 
"(A::'a multiset) + C \<le> B + C \<longleftrightarrow> A \<le> B" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

298 
by (fact add_le_cancel_right) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

299 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

300 
lemma mset_le_mono_add_left_cancel [simp]: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

301 
"C + (A::'a multiset) \<le> C + B \<longleftrightarrow> A \<le> B" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

302 
by (fact add_le_cancel_left) 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

303 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

304 
lemma mset_le_mono_add: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

305 
"(A::'a multiset) \<le> B \<Longrightarrow> C \<le> D \<Longrightarrow> A + C \<le> B + D" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

306 
by (fact add_mono) 
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

307 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

308 
lemma mset_le_add_left [simp]: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

309 
"(A::'a multiset) \<le> A + B" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

310 
unfolding mset_le_def by auto 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

311 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

312 
lemma mset_le_add_right [simp]: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

313 
"B \<le> (A::'a multiset) + B" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

314 
unfolding mset_le_def 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

315 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

316 
lemma mset_le_single: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

317 
"a :# B \<Longrightarrow> {#a#} \<le> B" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

318 
by (simp add: mset_le_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

319 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

320 
lemma multiset_diff_union_assoc: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

321 
"C \<le> B \<Longrightarrow> (A::'a multiset) + B  C = A + (B  C)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

322 
by (simp add: multiset_eq_iff mset_le_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

323 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

324 
lemma mset_le_multiset_union_diff_commute: 
36867  325 
"B \<le> A \<Longrightarrow> (A::'a multiset)  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

326 
by (simp add: multiset_eq_iff mset_le_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

327 

39301  328 
lemma diff_le_self[simp]: "(M::'a multiset)  N \<le> M" 
329 
by(simp add: mset_le_def) 

330 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

331 
lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># 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

332 
apply (clarsimp simp: mset_le_def mset_less_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

333 
apply (erule_tac x=x in allE) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

334 
apply 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

335 
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

336 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

337 
lemma mset_leD: "A \<le> B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># 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

338 
apply (clarsimp simp: mset_le_def mset_less_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

339 
apply (erule_tac x = x in allE) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

340 
apply 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

341 
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

342 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

343 
lemma mset_less_insertD: "(A + {#x#} < B) \<Longrightarrow> (x \<in># B \<and> A < 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

344 
apply (rule conjI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

345 
apply (simp add: mset_lessD) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

346 
apply (clarsimp simp: mset_le_def mset_less_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

347 
apply safe 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

348 
apply (erule_tac x = a in allE) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

349 
apply (auto split: split_if_asm) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

350 
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

351 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

352 
lemma mset_le_insertD: "(A + {#x#} \<le> B) \<Longrightarrow> (x \<in># B \<and> A \<le> 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

353 
apply (rule conjI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

354 
apply (simp add: mset_leD) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

355 
apply (force simp: mset_le_def mset_less_def split: split_if_asm) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

356 
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

357 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

358 
lemma mset_less_of_empty[simp]: "A < {#} \<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

359 
by (auto simp add: mset_less_def mset_le_def 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

360 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

361 
lemma multi_psub_of_add_self[simp]: "A < A + {#x#}" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

362 
by (auto simp: mset_le_def mset_less_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

363 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

364 
lemma multi_psub_self[simp]: "(A::'a multiset) < A = False" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

365 
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

366 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

367 
lemma mset_less_add_bothsides: 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

368 
"T + {#x#} < S + {#x#} \<Longrightarrow> T < S" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

369 
by (fact add_less_imp_less_right) 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

370 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

371 
lemma mset_less_empty_nonempty: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

372 
"{#} < S \<longleftrightarrow> S \<noteq> {#}" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

373 
by (auto simp: mset_le_def mset_less_def) 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

374 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

375 
lemma mset_less_diff_self: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

376 
"c \<in># B \<Longrightarrow> B  {#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

377 
by (auto simp: mset_le_def mset_less_def multiset_eq_iff) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

378 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

379 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

380 
subsubsection {* Intersection *} 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

381 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

382 
instantiation multiset :: (type) semilattice_inf 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

383 
begin 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

384 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

385 
definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

386 
multiset_inter_def: "inf_multiset A B = A  (A  B)" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

387 

46921  388 
instance 
389 
proof  

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

390 
have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n  (n  q)" by arith 
46921  391 
show "OFCLASS('a multiset, semilattice_inf_class)" 
392 
by default (auto simp add: multiset_inter_def mset_le_def aux) 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

393 
qed 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

394 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

395 
end 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

396 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

397 
abbreviation multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

398 
"multiset_inter \<equiv> inf" 
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

399 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

400 
lemma multiset_inter_count [simp]: 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

401 
"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

402 
by (simp add: multiset_inter_def) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

403 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

404 
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}" 
46730  405 
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

406 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

407 
lemma multiset_union_diff_commute: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

408 
assumes "B #\<inter> C = {#}" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

409 
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

410 
proof (rule multiset_eqI) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

411 
fix x 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

412 
from assms have "min (count B x) (count C x) = 0" 
46730  413 
by (auto simp add: multiset_eq_iff) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

414 
then have "count B x = 0 \<or> count C x = 0" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

415 
by auto 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

416 
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

417 
by auto 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

418 
qed 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

419 

51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

420 
lemma empty_inter [simp]: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

421 
"{#} #\<inter> M = {#}" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

422 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

423 

197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

424 
lemma inter_empty [simp]: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

425 
"M #\<inter> {#} = {#}" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

426 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

427 

197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

428 
lemma inter_add_left1: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

429 
"\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = M #\<inter> N" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

430 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

431 

197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

432 
lemma inter_add_left2: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

433 
"x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = (M #\<inter> (N  {#x#})) + {#x#}" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

434 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

435 

197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

436 
lemma inter_add_right1: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

437 
"\<not> x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = N #\<inter> M" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

438 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

439 

197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

440 
lemma inter_add_right2: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

441 
"x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = ((N  {#x#}) #\<inter> M) + {#x#}" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

442 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

443 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

444 

51623  445 
subsubsection {* Bounded union *} 
446 

447 
instantiation multiset :: (type) semilattice_sup 

448 
begin 

449 

450 
definition sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where 

451 
"sup_multiset A B = A + (B  A)" 

452 

453 
instance 

454 
proof  

455 
have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q  m) \<le> n" by arith 

456 
show "OFCLASS('a multiset, semilattice_sup_class)" 

457 
by default (auto simp add: sup_multiset_def mset_le_def aux) 

458 
qed 

459 

460 
end 

461 

462 
abbreviation sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<union>" 70) where 

463 
"sup_multiset \<equiv> sup" 

464 

465 
lemma sup_multiset_count [simp]: 

466 
"count (A #\<union> B) x = max (count A x) (count B x)" 

467 
by (simp add: sup_multiset_def) 

468 

469 
lemma empty_sup [simp]: 

470 
"{#} #\<union> M = M" 

471 
by (simp add: multiset_eq_iff) 

472 

473 
lemma sup_empty [simp]: 

474 
"M #\<union> {#} = M" 

475 
by (simp add: multiset_eq_iff) 

476 

477 
lemma sup_add_left1: 

478 
"\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}" 

479 
by (simp add: multiset_eq_iff) 

480 

481 
lemma sup_add_left2: 

482 
"x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N  {#x#})) + {#x#}" 

483 
by (simp add: multiset_eq_iff) 

484 

485 
lemma sup_add_right1: 

486 
"\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}" 

487 
by (simp add: multiset_eq_iff) 

488 

489 
lemma sup_add_right2: 

490 
"x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N  {#x#}) #\<union> M) + {#x#}" 

491 
by (simp add: multiset_eq_iff) 

492 

493 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

494 
subsubsection {* Filter (with comprehension syntax) *} 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

495 

6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

496 
text {* Multiset comprehension *} 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

497 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

498 
lift_definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>P M. \<lambda>x. if P x then M x else 0" 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

499 
by (rule filter_preserves_multiset) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

500 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

501 
hide_const (open) filter 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

502 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

503 
lemma count_filter [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

504 
"count (Multiset.filter P M) a = (if P a then count M a else 0)" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

505 
by (simp add: filter.rep_eq) 
41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

506 

6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

507 
lemma filter_empty [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

508 
"Multiset.filter P {#} = {#}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

509 
by (rule multiset_eqI) simp 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

510 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

511 
lemma filter_single [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

512 
"Multiset.filter P {#x#} = (if P x then {#x#} else {#})" 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

513 
by (rule multiset_eqI) simp 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

514 

6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

515 
lemma filter_union [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

516 
"Multiset.filter P (M + N) = Multiset.filter P M + Multiset.filter P N" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

517 
by (rule multiset_eqI) simp 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

518 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

519 
lemma filter_diff [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

520 
"Multiset.filter P (M  N) = Multiset.filter P M  Multiset.filter P N" 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

521 
by (rule multiset_eqI) simp 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

522 

6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

523 
lemma filter_inter [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

524 
"Multiset.filter P (M #\<inter> N) = Multiset.filter P M #\<inter> Multiset.filter P N" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

525 
by (rule multiset_eqI) simp 
10249  526 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

527 
syntax 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

528 
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ :# _./ _#})") 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

529 
syntax (xsymbol) 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

530 
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ \<in># _./ _#})") 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

531 
translations 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

532 
"{#x \<in># M. P#}" == "CONST Multiset.filter (\<lambda>x. P) M" 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

533 

10249  534 

535 
subsubsection {* Set of elements *} 

536 

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

537 
definition set_of :: "'a multiset => 'a set" 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

538 
"set_of M = {x. x :# M}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

539 

17161  540 
lemma set_of_empty [simp]: "set_of {#} = {}" 
26178  541 
by (simp add: set_of_def) 
10249  542 

17161  543 
lemma set_of_single [simp]: "set_of {#b#} = {b}" 
26178  544 
by (simp add: set_of_def) 
10249  545 

17161  546 
lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N" 
26178  547 
by (auto simp add: set_of_def) 
10249  548 

17161  549 
lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (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

550 
by (auto simp add: set_of_def multiset_eq_iff) 
10249  551 

17161  552 
lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)" 
26178  553 
by (auto simp add: set_of_def) 
26016  554 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

555 
lemma set_of_filter [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}" 
26178  556 
by (auto simp add: set_of_def) 
10249  557 

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 
lemma finite_set_of [iff]: "finite (set_of M)" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

559 
using count [of M] by (simp add: multiset_def set_of_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

560 

46756
faf62905cd53
adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
bulwahn
parents:
46730
diff
changeset

561 
lemma finite_Collect_mem [iff]: "finite {x. x :# M}" 
faf62905cd53
adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
bulwahn
parents:
46730
diff
changeset

562 
unfolding set_of_def[symmetric] by simp 
10249  563 

564 
subsubsection {* Size *} 

565 

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

566 
instantiation multiset :: (type) size 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

567 
begin 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

568 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

569 
definition size_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

570 
"size M = setsum (count M) (set_of M)" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

571 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

572 
instance .. 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

573 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

574 
end 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

575 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

576 
lemma size_empty [simp]: "size {#} = 0" 
26178  577 
by (simp add: size_def) 
10249  578 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

579 
lemma size_single [simp]: "size {#b#} = 1" 
26178  580 
by (simp add: size_def) 
10249  581 

17161  582 
lemma setsum_count_Int: 
26178  583 
"finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A" 
584 
apply (induct rule: finite_induct) 

585 
apply simp 

586 
apply (simp add: Int_insert_left set_of_def) 

587 
done 

10249  588 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

589 
lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N" 
26178  590 
apply (unfold size_def) 
591 
apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)") 

592 
prefer 2 

593 
apply (rule ext, simp) 

594 
apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int) 

595 
apply (subst Int_commute) 

596 
apply (simp (no_asm_simp) add: setsum_count_Int) 

597 
done 

10249  598 

17161  599 
lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (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

600 
by (auto simp add: size_def multiset_eq_iff) 
26016  601 

602 
lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)" 

26178  603 
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty) 
10249  604 

17161  605 
lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M" 
26178  606 
apply (unfold size_def) 
607 
apply (drule setsum_SucD) 

608 
apply auto 

609 
done 

10249  610 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

611 
lemma size_eq_Suc_imp_eq_union: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

612 
assumes "size M = Suc n" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

613 
shows "\<exists>a N. M = N + {#a#}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

614 
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

615 
from assms obtain a where "a \<in># M" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

616 
by (erule size_eq_Suc_imp_elem [THEN exE]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

617 
then have "M = M  {#a#} + {#a#}" by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

618 
then show ?thesis by blast 
23611  619 
qed 
15869  620 

26016  621 

622 
subsection {* Induction and case splits *} 

10249  623 

18258  624 
theorem multiset_induct [case_names empty add, induct type: multiset]: 
48009  625 
assumes empty: "P {#}" 
626 
assumes add: "\<And>M x. P M \<Longrightarrow> P (M + {#x#})" 

627 
shows "P M" 

628 
proof (induct n \<equiv> "size M" arbitrary: M) 

629 
case 0 thus "P M" by (simp add: empty) 

630 
next 

631 
case (Suc k) 

632 
obtain N x where "M = N + {#x#}" 

633 
using `Suc k = size M` [symmetric] 

634 
using size_eq_Suc_imp_eq_union by fast 

635 
with Suc add show "P M" by simp 

10249  636 
qed 
637 

25610  638 
lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}" 
26178  639 
by (induct M) auto 
25610  640 

641 
lemma multiset_cases [cases type, case_names empty add]: 

26178  642 
assumes em: "M = {#} \<Longrightarrow> P" 
643 
assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> P" 

644 
shows "P" 

48009  645 
using assms by (induct M) simp_all 
25610  646 

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

647 
lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B  {#c#} \<noteq> B" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

648 
by (cases "B = {#}") (auto dest: multi_member_split) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

649 

26033  650 
lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

651 
apply (subst multiset_eq_iff) 
26178  652 
apply auto 
653 
done 

10249  654 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

655 
lemma mset_less_size: "(A::'a multiset) < B \<Longrightarrow> size A < size B" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

656 
proof (induct A arbitrary: B) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

657 
case (empty M) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

658 
then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

659 
then obtain M' x where "M = 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

660 
by (blast dest: multi_nonempty_split) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

661 
then show ?case by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

662 
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

663 
case (add S x T) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

664 
have IH: "\<And>B. S < B \<Longrightarrow> size S < size B" by fact 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

665 
have SxsubT: "S + {#x#} < T" by fact 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

666 
then have "x \<in># T" and "S < T" by (auto dest: mset_less_insertD) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

667 
then obtain T' where T: "T = T' + {#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

668 
by (blast dest: multi_member_split) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

669 
then have "S < T'" using SxsubT 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

670 
by (blast intro: mset_less_add_bothsides) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

671 
then have "size S < size T'" using IH by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

672 
then show ?case using T by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

673 
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

674 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

675 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

676 
subsubsection {* Strong induction and subset induction for multisets *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

677 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

678 
text {* Wellfoundedness of proper subset operator: *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

679 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

680 
text {* proper multiset 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

681 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

682 
definition 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

683 
mset_less_rel :: "('a multiset * 'a multiset) set" where 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

684 
"mset_less_rel = {(A,B). A < B}" 
10249  685 

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

686 
lemma multiset_add_sub_el_shuffle: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

687 
assumes "c \<in># B" and "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

688 
shows "B  {#c#} + {#b#} = B + {#b#}  {#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

689 
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

690 
from `c \<in># B` obtain A where B: "B = A + {#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

691 
by (blast dest: multi_member_split) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

692 
have "A + {#b#} = A + {#b#} + {#c#}  {#c#}" by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

693 
then have "A + {#b#} = A + {#c#} + {#b#}  {#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

694 
by (simp add: add_ac) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

695 
then show ?thesis using B 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

696 
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

697 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

698 
lemma wf_mset_less_rel: "wf mset_less_rel" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

699 
apply (unfold mset_less_rel_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

700 
apply (rule wf_measure [THEN wf_subset, where f1=size]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

701 
apply (clarsimp simp: measure_def inv_image_def mset_less_size) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

702 
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

703 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

704 
text {* The induction rules: *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

705 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

706 
lemma full_multiset_induct [case_names less]: 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

707 
assumes ih: "\<And>B. \<forall>(A::'a multiset). A < B \<longrightarrow> P A \<Longrightarrow> P B" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

708 
shows "P 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

709 
apply (rule wf_mset_less_rel [THEN wf_induct]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

710 
apply (rule ih, auto simp: mset_less_rel_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

711 
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

712 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

713 
lemma multi_subset_induct [consumes 2, case_names empty add]: 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

714 
assumes "F \<le> 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

715 
and empty: "P {#}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

716 
and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

717 
shows "P F" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

718 
proof  
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

719 
from `F \<le> 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

720 
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

721 
proof (induct F) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

722 
show "P {#}" by fact 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

723 
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

724 
fix x F 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

725 
assume P: "F \<le> A \<Longrightarrow> P F" and i: "F + {#x#} \<le> 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

726 
show "P (F + {#x#})" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

727 
proof (rule insert) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

728 
from i show "x \<in># A" by (auto dest: mset_le_insertD) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

729 
from i have "F \<le> A" by (auto dest: mset_le_insertD) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

730 
with P show "P F" . 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

731 
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

732 
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

733 
qed 
26145  734 

17161  735 

48023  736 
subsection {* The fold combinator *} 
737 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

738 
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" 
48023  739 
where 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

740 
"fold f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)" 
48023  741 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

742 
lemma fold_mset_empty [simp]: 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

743 
"fold f s {#} = s" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

744 
by (simp add: fold_def) 
48023  745 

746 
context comp_fun_commute 

747 
begin 

748 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

749 
lemma fold_mset_insert: 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

750 
"fold f s (M + {#x#}) = f x (fold f s M)" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

751 
proof  
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

752 
interpret mset: comp_fun_commute "\<lambda>y. f y ^^ count M y" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

753 
by (fact comp_fun_commute_funpow) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

754 
interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (M + {#x#}) y" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

755 
by (fact comp_fun_commute_funpow) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

756 
show ?thesis 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

757 
proof (cases "x \<in> set_of M") 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

758 
case False 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

759 
then have *: "count (M + {#x#}) x = 1" by simp 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

760 
from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_of M) = 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

761 
Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_of M)" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

762 
by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

763 
with False * show ?thesis 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

764 
by (simp add: fold_def del: count_union) 
48023  765 
next 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

766 
case True 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

767 
def N \<equiv> "set_of M  {x}" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

768 
from N_def True have *: "set_of M = insert x N" "x \<notin> N" "finite N" by auto 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

769 
then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N = 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

770 
Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

771 
by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

772 
with * show ?thesis by (simp add: fold_def del: count_union) simp 
48023  773 
qed 
774 
qed 

775 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

776 
corollary fold_mset_single [simp]: 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

777 
"fold f s {#x#} = f x s" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

778 
proof  
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

779 
have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

780 
then show ?thesis by simp 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

781 
qed 
48023  782 

51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

783 
lemma fold_mset_fun_left_comm: 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

784 
"f x (fold f s M) = fold f (f x s) M" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

785 
by (induct M) (simp_all add: fold_mset_insert fun_left_comm) 
48023  786 

787 
lemma fold_mset_union [simp]: 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

788 
"fold f s (M + N) = fold f (fold f s M) N" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

789 
proof (induct M) 
48023  790 
case empty then show ?case by simp 
791 
next 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

792 
case (add M x) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

793 
have "M + {#x#} + N = (M + N) + {#x#}" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

794 
by (simp add: add_ac) 
51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

795 
with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm) 
48023  796 
qed 
797 

798 
lemma fold_mset_fusion: 

799 
assumes "comp_fun_commute g" 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

800 
shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold g w A) = fold f (h w) A" (is "PROP ?P") 
48023  801 
proof  
802 
interpret comp_fun_commute g by (fact assms) 

803 
show "PROP ?P" by (induct A) auto 

804 
qed 

805 

806 
end 

807 

808 
text {* 

809 
A note on code generation: When defining some function containing a 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

810 
subterm @{term "fold F"}, code generation is not automatic. When 
48023  811 
interpreting locale @{text left_commutative} with @{text F}, the 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

812 
would be code thms for @{const fold} become thms like 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

813 
@{term "fold F z {#} = z"} where @{text F} is not a pattern but 
48023  814 
contains defined symbols, i.e.\ is not a code thm. Hence a separate 
815 
constant with its own code thms needs to be introduced for @{text 

816 
F}. See the image operator below. 

817 
*} 

818 

819 

820 
subsection {* Image *} 

821 

822 
definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

823 
"image_mset f = fold (plus o single o f) {#}" 
48023  824 

49823  825 
lemma comp_fun_commute_mset_image: 
826 
"comp_fun_commute (plus o single o f)" 

827 
proof 

828 
qed (simp add: add_ac fun_eq_iff) 

48023  829 

830 
lemma image_mset_empty [simp]: "image_mset f {#} = {#}" 

49823  831 
by (simp add: image_mset_def) 
48023  832 

833 
lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}" 

49823  834 
proof  
835 
interpret comp_fun_commute "plus o single o f" 

836 
by (fact comp_fun_commute_mset_image) 

837 
show ?thesis by (simp add: image_mset_def) 

838 
qed 

48023  839 

840 
lemma image_mset_union [simp]: 

49823  841 
"image_mset f (M + N) = image_mset f M + image_mset f N" 
842 
proof  

843 
interpret comp_fun_commute "plus o single o f" 

844 
by (fact comp_fun_commute_mset_image) 

845 
show ?thesis by (induct N) (simp_all add: image_mset_def add_ac) 

846 
qed 

847 

848 
corollary image_mset_insert: 

849 
"image_mset f (M + {#a#}) = image_mset f M + {#f a#}" 

850 
by simp 

48023  851 

49823  852 
lemma set_of_image_mset [simp]: 
853 
"set_of (image_mset f M) = image f (set_of M)" 

854 
by (induct M) simp_all 

48040  855 

49823  856 
lemma size_image_mset [simp]: 
857 
"size (image_mset f M) = size M" 

858 
by (induct M) simp_all 

48023  859 

49823  860 
lemma image_mset_is_empty_iff [simp]: 
861 
"image_mset f M = {#} \<longleftrightarrow> M = {#}" 

862 
by (cases M) auto 

48023  863 

864 
syntax 

865 
"_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" 

866 
("({#_/. _ :# _#})") 

867 
translations 

868 
"{#e. x:#M#}" == "CONST image_mset (%x. e) M" 

869 

870 
syntax 

871 
"_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" 

872 
("({#_/  _ :# _./ _#})") 

873 
translations 

874 
"{#e  x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}" 

875 

876 
text {* 

877 
This allows to write not just filters like @{term "{#x:#M. x<c#}"} 

878 
but also images like @{term "{#x+x. x:#M #}"} and @{term [source] 

879 
"{#x+xx:#M. x<c#}"}, where the latter is currently displayed as 

880 
@{term "{#x+xx:#M. x<c#}"}. 

881 
*} 

882 

883 
enriched_type image_mset: image_mset 

884 
proof  

885 
fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)" 

886 
proof 

887 
fix A 

888 
show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A" 

889 
by (induct A) simp_all 

890 
qed 

891 
show "image_mset id = id" 

892 
proof 

893 
fix A 

894 
show "image_mset id A = id A" 

895 
by (induct A) simp_all 

896 
qed 

897 
qed 

898 

49717  899 
declare image_mset.identity [simp] 
900 

48023  901 

51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

902 
subsection {* Further conversions *} 
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

903 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

904 
primrec multiset_of :: "'a list \<Rightarrow> '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

905 
"multiset_of [] = {#}"  
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

906 
"multiset_of (a # x) = multiset_of x + {# a #}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

907 

37107  908 
lemma in_multiset_in_set: 
909 
"x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs" 

910 
by (induct xs) simp_all 

911 

912 
lemma count_multiset_of: 

913 
"count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)" 

914 
by (induct xs) simp_all 

915 

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

916 
lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (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

917 
by (induct x) 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

918 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

919 
lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (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

920 
by (induct x) 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

921 

40950  922 
lemma set_of_multiset_of[simp]: "set_of (multiset_of x) = set x" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

923 
by (induct x) 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

924 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

925 
lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

926 
by (induct xs) 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

927 

48012  928 
lemma size_multiset_of [simp]: "size (multiset_of xs) = length xs" 
929 
by (induct xs) simp_all 

930 

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

931 
lemma multiset_of_append [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

932 
"multiset_of (xs @ ys) = multiset_of xs + multiset_of ys" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

933 
by (induct xs arbitrary: ys) (auto simp: add_ac) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

934 

40303
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

935 
lemma multiset_of_filter: 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

936 
"multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}" 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

937 
by (induct xs) simp_all 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

938 

40950  939 
lemma multiset_of_rev [simp]: 
940 
"multiset_of (rev xs) = multiset_of xs" 

941 
by (induct xs) simp_all 

942 

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

943 
lemma surj_multiset_of: "surj multiset_of" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

944 
apply (unfold surj_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

945 
apply (rule allI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

946 
apply (rule_tac M = y in multiset_induct) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

947 
apply 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

948 
apply (rule_tac x = "x # xa" in exI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

949 
apply 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

950 
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

951 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

952 
lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

953 
by (induct x) 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

954 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

955 
lemma distinct_count_atmost_1: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

956 
"distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

957 
apply (induct x, simp, rule iffI, simp_all) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

958 
apply (rule conjI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

959 
apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

960 
apply (erule_tac x = a in allE, simp, clarify) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

961 
apply (erule_tac x = aa in allE, 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

962 
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

963 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

964 
lemma multiset_of_eq_setD: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

965 
"multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

966 
by (rule) (auto simp add:multiset_eq_iff set_count_greater_0) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

967 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

968 
lemma set_eq_iff_multiset_of_eq_distinct: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

969 
"distinct x \<Longrightarrow> distinct y \<Longrightarrow> 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

970 
(set x = set y) = (multiset_of x = multiset_of y)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

971 
by (auto simp: multiset_eq_iff distinct_count_atmost_1) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

972 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

973 
lemma set_eq_iff_multiset_of_remdups_eq: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

974 
"(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

975 
apply (rule iffI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

976 
apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

977 
apply (drule distinct_remdups [THEN distinct_remdups 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

978 
[THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

979 
apply 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

980 
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

981 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

982 
lemma multiset_of_compl_union [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

983 
"multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

984 
by (induct xs) (auto simp: add_ac) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

985 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

986 
lemma count_multiset_of_length_filter: 
39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

987 
"count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

988 
by (induct xs) 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

989 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

990 
lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

991 
apply (induct ls arbitrary: i) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

992 
apply 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

993 
apply (case_tac i) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

994 
apply 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

995 
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

996 

36903  997 
lemma multiset_of_remove1[simp]: 
998 
"multiset_of (remove1 a xs) = multiset_of xs  {#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

999 
by (induct xs) (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

1000 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1001 
lemma multiset_of_eq_length: 
37107  1002 
assumes "multiset_of xs = multiset_of ys" 
1003 
shows "length xs = length ys" 

48012  1004 
using assms by (metis size_multiset_of) 
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

1005 

39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1006 
lemma multiset_of_eq_length_filter: 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1007 
assumes "multiset_of xs = multiset_of ys" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1008 
shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)" 
48012  1009 
using assms by (metis count_multiset_of) 
39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1010 

45989
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1011 
lemma fold_multiset_equiv: 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1012 
assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1013 
and equiv: "multiset_of xs = multiset_of ys" 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

1014 
shows "List.fold f xs = List.fold f ys" 
46921  1015 
using f equiv [symmetric] 
1016 
proof (induct xs arbitrary: ys) 

45989
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1017 
case Nil then show ?case by simp 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1018 
next 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1019 
case (Cons x xs) 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1020 
then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD) 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1021 
have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1022 
by (rule Cons.prems(1)) (simp_all add: *) 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1023 
moreover from * have "x \<in> set ys" by simp 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

1024 
ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

1025 
moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)" by (auto intro: Cons.hyps) 
45989
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1026 
ultimately show ?case by simp 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1027 
qed 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1028 

51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1029 
lemma multiset_of_insort [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1030 
"multiset_of (insort x xs) = multiset_of xs + {#x#}" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1031 
by (induct xs) (simp_all add: ac_simps) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1032 

51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1033 
lemma in_multiset_of: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1034 
"x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1035 
by (induct xs) simp_all 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1036 

197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1037 
lemma multiset_of_map: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1038 
"multiset_of (map f xs) = image_mset f (multiset_of xs)" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1039 
by (induct xs) simp_all 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1040 

51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1041 
definition multiset_of_set :: "'a set \<Rightarrow> 'a multiset" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1042 
where 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1043 
"multiset_of_set = folding.F (\<lambda>x M. {#x#} + M) {#}" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1044 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1045 
interpretation multiset_of_set!: folding "\<lambda>x M. {#x#} + M" "{#}" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1046 
where 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1047 
"folding.F (\<lambda>x M. {#x#} + M) {#} = multiset_of_set" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1048 
proof  
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1049 
interpret comp_fun_commute "\<lambda>x M. {#x#} + M" by default (simp add: fun_eq_iff ac_simps) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1050 
show "folding (\<lambda>x M. {#x#} + M)" by default (fact comp_fun_commute) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1051 
from multiset_of_set_def show "folding.F (\<lambda>x M. {#x#} + M) {#} = multiset_of_set" .. 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1052 
qed 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1053 

51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1054 
lemma count_multiset_of_set [simp]: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1055 
"finite A \<Longrightarrow> x \<in> A \<Longrightarrow> count (multiset_of_set A) x = 1" (is "PROP ?P") 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1056 
"\<not> finite A \<Longrightarrow> count (multiset_of_set A) x = 0" (is "PROP ?Q") 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1057 
"x \<notin> A \<Longrightarrow> count (multiset_of_set A) x = 0" (is "PROP ?R") 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1058 
proof  
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1059 
{ fix A 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1060 
assume "x \<notin> A" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1061 
have "count (multiset_of_set A) x = 0" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1062 
proof (cases "finite A") 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1063 
case False then show ?thesis by simp 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1064 
next 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1065 
case True from True `x \<notin> A` show ?thesis by (induct A) auto 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1066 
qed 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1067 
} note * = this 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1068 
then show "PROP ?P" "PROP ?Q" "PROP ?R" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1069 
by (auto elim!: Set.set_insert) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1070 
qed  {* TODO: maybe define @{const multiset_of_set} also in terms of @{const Abs_multiset} *} 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1071 

51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1072 
context linorder 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1073 
begin 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1074 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1075 
definition sorted_list_of_multiset :: "'a multiset \<Rightarrow> 'a list" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1076 
where 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1077 
"sorted_list_of_multiset M = fold insort [] M" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1078 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1079 
lemma sorted_list_of_multiset_empty [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1080 
"sorted_list_of_multiset {#} = []" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1081 
by (simp add: sorted_list_of_multiset_def) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1082 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1083 
lemma sorted_list_of_multiset_singleton [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1084 
"sorted_list_of_multiset {#x#} = [x]" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1085 
proof  
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1086 
interpret comp_fun_commute insort by (fact comp_fun_commute_insort) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1087 
show ?thesis by (simp add: sorted_list_of_multiset_def) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1088 
qed 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1089 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1090 
lemma sorted_list_of_multiset_insert [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1091 
"sorted_list_of_multiset (M + {#x#}) = List.insort x (sorted_list_of_multiset M)" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1092 
proof  
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1093 
interpret comp_fun_commute insort by (fact comp_fun_commute_insort) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1094 
show ?thesis by (simp add: sorted_list_of_multiset_def) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1095 
qed 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1096 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1097 
end 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1098 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1099 
lemma multiset_of_sorted_list_of_multiset [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1100 
"multiset_of (sorted_list_of_multiset M) = M" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1101 
by (induct M) simp_all 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1102 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1103 
lemma sorted_list_of_multiset_multiset_of [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1104 
"sorted_list_of_multiset (multiset_of xs) = sort xs" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1105 
by (induct xs) simp_all 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1106 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1107 
lemma finite_set_of_multiset_of_set: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1108 
assumes "finite A" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1109 
shows "set_of (multiset_of_set A) = A" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1110 
using assms by (induct A) simp_all 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1111 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1112 
lemma infinite_set_of_multiset_of_set: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1113 
assumes "\<not> finite A" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1114 
shows "set_of (multiset_of_set A) = {}" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1115 
using assms by simp 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1116 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1117 
lemma set_sorted_list_of_multiset [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1118 
"set (sorted_list_of_multiset M) = set_of M" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1119 
by (induct M) (simp_all add: set_insort) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1120 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1121 
lemma sorted_list_of_multiset_of_set [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1122 
"sorted_list_of_multiset (multiset_of_set A) = sorted_list_of_set A" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1123 
by (cases "finite A") (induct A rule: finite_induct, simp_all add: ac_simps) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1124 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1125 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1126 
subsection {* Big operators *} 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1127 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1128 
no_notation times (infixl "*" 70) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1129 
no_notation Groups.one ("1") 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1130 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1131 
locale comm_monoid_mset = comm_monoid 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1132 
begin 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1133 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1134 
definition F :: "'a multiset \<Rightarrow> 'a" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1135 
where 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1136 
eq_fold: "F M = Multiset.fold f 1 M" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1137 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1138 
lemma empty [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1139 
"F {#} = 1" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1140 
by (simp add: eq_fold) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1141 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1142 
lemma singleton [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1143 
"F {#x#} = x" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1144 
proof  
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1145 
interpret comp_fun_commute 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1146 
by default (simp add: fun_eq_iff left_commute) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1147 
show ?thesis by (simp add: eq_fold) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1148 
qed 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1149 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1150 
lemma union [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1151 
"F (M + N) = F M * F N" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1152 
proof  
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1153 
interpret comp_fun_commute f 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1154 
by default (simp add: fun_eq_iff left_commute) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1155 
show ?thesis by (induct N) (simp_all add: left_commute eq_fold) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1156 
qed 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1157 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1158 
end 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1159 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1160 
notation times (infixl "*" 70) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1161 
notation Groups.one ("1") 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1162 

54868  1163 
context comm_monoid_add 
1164 
begin 

1165 

1166 
definition msetsum :: "'a multiset \<Rightarrow> 'a" 

51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1167 
where 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1168 
"msetsum = comm_monoid_mset.F plus 0" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1169 

54868  1170 
sublocale msetsum!: comm_monoid_mset plus 0 
51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1171 
where 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1172 
"comm_monoid_mset.F plus 0 = msetsum" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1173 
proof  
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1174 
show "comm_monoid_mset plus 0" .. 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1175 
from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" .. 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1176 
qed 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1177 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1178 
lemma setsum_unfold_msetsum: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1179 
"setsum f A = msetsum (image_mset f (multiset_of_set A))" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1180 
by (cases "finite A") (induct A rule: finite_induct, simp_all) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1181 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1182 
abbreviation msetsum_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1183 
where 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1184 
"msetsum_image f M \<equiv> msetsum (image_mset f M)" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1185 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1186 
end 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1187 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1188 
syntax 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1189 
"_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1190 
("(3SUM _:#_. _)" [0, 51, 10] 10) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1191 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1192 
syntax (xsymbols) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1193 
"_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1194 
("(3\<Sum>_:#_. _)" [0, 51, 10] 10) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1195 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1196 
syntax (HTML output) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1197 
"_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1198 
("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1199 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1200 
translations 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1201 
"SUM i :# A. b" == "CONST msetsum_image (\<lambda>i. b) A" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1202 

54868 