author  huffman 
Tue, 29 May 2012 17:06:04 +0200  
changeset 48023  6dfe5e774012 
parent 48012  b6e5e86a7303 
child 48040  4caf6cd063be 
permissions  rwrr 
10249  1 
(* Title: HOL/Library/Multiset.thy 
15072  2 
Author: Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker 
10249  3 
*) 
4 

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

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

15131  7 
theory Multiset 
46237  8 
imports Main DAList 
15131  9 
begin 
10249  10 

11 
subsection {* The type of multisets *} 

12 

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

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

14 

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

15 
typedef (open) '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

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

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

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

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

22 
setup_lifting type_definition_multiset 
19086  23 

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

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

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

10249  29 

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

30 
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

31 
"M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

32 
by (simp only: count_inject [symmetric] fun_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

33 

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

34 
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

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

36 
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

37 

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

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

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

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

44 
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

45 

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

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

48 
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

49 

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

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

52 
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

53 

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

55 
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

56 
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

57 
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

58 
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

59 
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

60 
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

61 
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

62 
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

63 

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

64 
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

65 
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

66 
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

67 
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

68 
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

69 
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

70 
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

71 
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

72 
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

73 

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

75 
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

76 

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

79 

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

81 

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

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

84 

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

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

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

87 

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

88 
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

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

90 

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

91 
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

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

93 

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

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

96 

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

97 
end 
10249  98 

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

99 
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

100 
by (rule only1_in_multiset) 
15869  101 

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

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

107 

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

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

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

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

111 
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

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

10249  114 

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

115 
subsection {* Basic operations *} 
10249  116 

117 
subsubsection {* Union *} 

118 

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

119 
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

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

122 

123 
subsubsection {* Difference *} 

124 

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

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

126 
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

127 

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

128 
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

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

130 

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

131 
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

132 

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

133 
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

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

136 
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

137 

17161  138 
lemma diff_empty [simp]: "M  {#} = M \<and> {#}  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

139 
by(simp add: multiset_eq_iff) 
36903  140 

141 
lemma diff_cancel[simp]: "A  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

142 
by (rule multiset_eqI) simp 
10249  143 

36903  144 
lemma diff_union_cancelR [simp]: "M + N  N = (M::'a multiset)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

145 
by(simp add: multiset_eq_iff) 
10249  146 

36903  147 
lemma diff_union_cancelL [simp]: "N + M  N = (M::'a multiset)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

148 
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

149 

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

150 
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

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

152 
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

153 

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

154 
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

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

156 
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

157 

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

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

159 
"(M::'a multiset)  N  Q = M  Q  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

160 
by (auto simp add: multiset_eq_iff) 
36903  161 

162 
lemma diff_add: 

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

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

164 
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

165 

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

166 
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

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

168 
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

169 

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

170 
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

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

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

173 

10249  174 

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

175 
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

176 

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

178 
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

179 

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

180 
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

181 
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

182 

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

183 
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

184 
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

185 

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

186 
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

187 
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

188 

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

189 
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

190 
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

191 

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

192 
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

193 
"\<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

194 
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

195 

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

196 
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

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

198 
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

199 

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

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

202 
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

203 

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

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

206 
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

207 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
lemma union_is_single: 
46730  209 
"M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs") 
210 
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

211 
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

212 
next 
46730  213 
assume ?lhs then show ?rhs 
214 
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

215 
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

216 

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

218 
"{#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

219 
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

220 

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

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

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

224 
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

225 
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

226 
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

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

228 
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

229 
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

230 
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

231 
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

232 
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

233 
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

234 
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

235 
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

236 
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

237 
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

238 
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

239 
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

240 
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

241 
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

242 

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

244 
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

245 
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

246 
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

247 
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

248 
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

249 
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

250 
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

251 
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

252 
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

253 

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

255 
"(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

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

257 
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

258 

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

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

261 

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

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

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

264 

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

265 
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

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

267 
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

268 

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

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

270 
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

271 

46921  272 
instance 
273 
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

274 

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

275 
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

276 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
lemma mset_less_eqI: 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

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

279 
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

280 

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

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

282 
"(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

283 
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

284 
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

285 
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

286 

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

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

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

289 
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

290 

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

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

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

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

294 

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

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

296 
"(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

297 
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

298 

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

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

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

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

302 

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

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

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

305 
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

306 

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

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

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

309 
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

310 

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

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

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

313 
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

314 

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

317 
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

318 

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

321 

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

322 
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

323 
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

324 
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

325 
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

326 
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

327 

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

328 
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

329 
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

330 
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

331 
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

332 
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

333 

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

334 
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

335 
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

336 
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

337 
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

338 
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

339 
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

340 
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

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

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

346 
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

347 
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

348 

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

349 
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

350 
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

351 

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

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

353 
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

354 

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

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

356 
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

357 

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

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

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

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

361 

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

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

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

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

365 

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

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

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

368 
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

369 

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 
subsubsection {* Intersection *} 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

372 

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

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

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

375 

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

376 
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

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

378 

46921  379 
instance 
380 
proof  

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

381 
have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n  (n  q)" by arith 
46921  382 
show "OFCLASS('a multiset, semilattice_inf_class)" 
383 
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

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

385 

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

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

387 

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

388 
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

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

390 

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

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

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

393 
by (simp add: multiset_inter_def) 
35268
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 
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}" 
46730  396 
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

397 

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

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

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

400 
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

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

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

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

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

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

407 
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

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

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

410 

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

411 

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

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

413 

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

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

415 

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

416 
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

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

418 

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

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

420 

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

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

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

423 
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

424 

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

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

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

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

428 

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

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

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

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

432 

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

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

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

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

436 

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

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

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

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

440 

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

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

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

443 
by (rule multiset_eqI) simp 
10249  444 

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

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

446 
"_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

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

448 
"_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

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

450 
"{#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

451 

10249  452 

453 
subsubsection {* Set of elements *} 

454 

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

455 
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

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

457 

17161  458 
lemma set_of_empty [simp]: "set_of {#} = {}" 
26178  459 
by (simp add: set_of_def) 
10249  460 

17161  461 
lemma set_of_single [simp]: "set_of {#b#} = {b}" 
26178  462 
by (simp add: set_of_def) 
10249  463 

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

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

468 
by (auto simp add: set_of_def multiset_eq_iff) 
10249  469 

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

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

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

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

476 
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

477 
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

478 

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

479 
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

480 
unfolding set_of_def[symmetric] by simp 
10249  481 

482 
subsubsection {* Size *} 

483 

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

484 
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

485 
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

486 

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

487 
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

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

489 

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

490 
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

491 

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

492 
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

493 

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

494 
lemma size_empty [simp]: "size {#} = 0" 
26178  495 
by (simp add: size_def) 
10249  496 

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

497 
lemma size_single [simp]: "size {#b#} = 1" 
26178  498 
by (simp add: size_def) 
10249  499 

17161  500 
lemma setsum_count_Int: 
26178  501 
"finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A" 
502 
apply (induct rule: finite_induct) 

503 
apply simp 

504 
apply (simp add: Int_insert_left set_of_def) 

505 
done 

10249  506 

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

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

510 
prefer 2 

511 
apply (rule ext, simp) 

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

513 
apply (subst Int_commute) 

514 
apply (simp (no_asm_simp) add: setsum_count_Int) 

515 
done 

10249  516 

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

518 
by (auto simp add: size_def multiset_eq_iff) 
26016  519 

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

26178  521 
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty) 
10249  522 

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

526 
apply auto 

527 
done 

10249  528 

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

529 
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

530 
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

531 
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

532 
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

533 
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

534 
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

535 
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

536 
then show ?thesis by blast 
23611  537 
qed 
15869  538 

26016  539 

540 
subsection {* Induction and case splits *} 

10249  541 

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

545 
shows "P M" 

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

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

548 
next 

549 
case (Suc k) 

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

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

552 
using size_eq_Suc_imp_eq_union by fast 

553 
with Suc add show "P M" by simp 

10249  554 
qed 
555 

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

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

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

562 
shows "P" 

48009  563 
using assms by (induct M) simp_all 
25610  564 

565 
lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}" 

48009  566 
by (rule_tac x="M  {#x#}" in exI, simp) 
25610  567 

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

568 
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

569 
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

570 

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

572 
apply (subst multiset_eq_iff) 
26178  573 
apply auto 
574 
done 

10249  575 

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

576 
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

577 
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

578 
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

579 
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

580 
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

581 
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

582 
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

583 
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

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

585 
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

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

587 
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

588 
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

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

590 
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

591 
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

592 
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

593 
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

594 
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

595 

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

596 

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

597 
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

598 

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

599 
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

600 

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

601 
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

602 

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

603 
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

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

605 
"mset_less_rel = {(A,B). A < B}" 
10249  606 

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

607 
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

608 
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

609 
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

610 
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

611 
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

612 
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

613 
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

614 
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

615 
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

616 
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

617 
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

618 

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

619 
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

620 
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

621 
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

622 
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

623 
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

624 

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

625 
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

626 

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

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

628 
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

629 
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

630 
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

631 
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

632 
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

633 

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

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

635 
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

636 
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

637 
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

638 
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

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

640 
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

641 
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

642 
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

643 
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

644 
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

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

646 
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

647 
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

648 
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

649 
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

650 
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

651 
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

652 
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

653 
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

654 
qed 
26145  655 

17161  656 

48023  657 
subsection {* The fold combinator *} 
658 

659 
text {* 

660 
The intended behaviour is 

661 
@{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"} 

662 
if @{text f} is associativecommutative. 

663 
*} 

664 

665 
text {* 

666 
The graph of @{text "fold_mset"}, @{text "z"}: the start element, 

667 
@{text "f"}: folding function, @{text "A"}: the multiset, @{text 

668 
"y"}: the result. 

669 
*} 

670 
inductive 

671 
fold_msetG :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b \<Rightarrow> bool" 

672 
for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 

673 
and z :: 'b 

674 
where 

675 
emptyI [intro]: "fold_msetG f z {#} z" 

676 
 insertI [intro]: "fold_msetG f z A y \<Longrightarrow> fold_msetG f z (A + {#x#}) (f x y)" 

677 

678 
inductive_cases empty_fold_msetGE [elim!]: "fold_msetG f z {#} x" 

679 
inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y" 

680 

681 
definition 

682 
fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" where 

683 
"fold_mset f z A = (THE x. fold_msetG f z A x)" 

684 

685 
lemma Diff1_fold_msetG: 

686 
"fold_msetG f z (A  {#x#}) y \<Longrightarrow> x \<in># A \<Longrightarrow> fold_msetG f z A (f x y)" 

687 
apply (frule_tac x = x in fold_msetG.insertI) 

688 
apply auto 

689 
done 

690 

691 
lemma fold_msetG_nonempty: "\<exists>x. fold_msetG f z A x" 

692 
apply (induct A) 

693 
apply blast 

694 
apply clarsimp 

695 
apply (drule_tac x = x in fold_msetG.insertI) 

696 
apply auto 

697 
done 

698 

699 
lemma fold_mset_empty[simp]: "fold_mset f z {#} = z" 

700 
unfolding fold_mset_def by blast 

701 

702 
context comp_fun_commute 

703 
begin 

704 

705 
lemma fold_msetG_insertE_aux: 

706 
"fold_msetG f z A y \<Longrightarrow> a \<in># A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_msetG f z (A  {#a#}) y'" 

707 
proof (induct set: fold_msetG) 

708 
case (insertI A y x) show ?case 

709 
proof (cases "x = a") 

710 
assume "x = a" with insertI show ?case by auto 

711 
next 

712 
assume "x \<noteq> a" 

713 
then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A  {#a#}) y'" 

714 
using insertI by auto 

715 
have "f x y = f a (f x y')" 

716 
unfolding y by (rule fun_left_comm) 

717 
moreover have "fold_msetG f z (A + {#x#}  {#a#}) (f x y')" 

718 
using y' and `x \<noteq> a` 

719 
by (simp add: diff_union_swap [symmetric] fold_msetG.insertI) 

720 
ultimately show ?case by fast 

721 
qed 

722 
qed simp 

723 

724 
lemma fold_msetG_insertE: 

725 
assumes "fold_msetG f z (A + {#x#}) v" 

726 
obtains y where "v = f x y" and "fold_msetG f z A y" 

727 
using assms by (auto dest: fold_msetG_insertE_aux [where a=x]) 

728 

729 
lemma fold_msetG_determ: 

730 
"fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x" 

731 
proof (induct arbitrary: y set: fold_msetG) 

732 
case (insertI A y x v) 

733 
from `fold_msetG f z (A + {#x#}) v` 

734 
obtain y' where "v = f x y'" and "fold_msetG f z A y'" 

735 
by (rule fold_msetG_insertE) 

736 
from `fold_msetG f z A y'` have "y' = y" by (rule insertI) 

737 
with `v = f x y'` show "v = f x y" by simp 

738 
qed fast 

739 

740 
lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y" 

741 
unfolding fold_mset_def by (blast intro: fold_msetG_determ) 

742 

743 
lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)" 

744 
proof  

745 
from fold_msetG_nonempty fold_msetG_determ 

746 
have "\<exists>!x. fold_msetG f z A x" by (rule ex_ex1I) 

747 
then show ?thesis unfolding fold_mset_def by (rule theI') 

748 
qed 

749 

750 
lemma fold_mset_insert: 

751 
"fold_mset f z (A + {#x#}) = f x (fold_mset f z A)" 

752 
by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset) 

753 

754 
lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A" 

755 
by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x]) 

756 

757 
lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z" 

758 
using fold_mset_insert [of z "{#}"] by simp 

759 

760 
lemma fold_mset_union [simp]: 

761 
"fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B" 

762 
proof (induct A) 

763 
case empty then show ?case by simp 

764 
next 

765 
case (add A x) 

766 
have "A + {#x#} + B = (A+B) + {#x#}" by (simp add: add_ac) 

767 
then have "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))" 

768 
by (simp add: fold_mset_insert) 

769 
also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B" 

770 
by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert) 

771 
finally show ?case . 

772 
qed 

773 

774 
lemma fold_mset_fusion: 

775 
assumes "comp_fun_commute g" 

776 
shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P") 

777 
proof  

778 
interpret comp_fun_commute g by (fact assms) 

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

780 
qed 

781 

782 
lemma fold_mset_rec: 

783 
assumes "a \<in># A" 

784 
shows "fold_mset f z A = f a (fold_mset f z (A  {#a#}))" 

785 
proof  

786 
from assms obtain A' where "A = A' + {#a#}" 

787 
by (blast dest: multi_member_split) 

788 
then show ?thesis by simp 

789 
qed 

790 

791 
end 

792 

793 
text {* 

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

795 
subterm @{term"fold_mset F"}, code generation is not automatic. When 

796 
interpreting locale @{text left_commutative} with @{text F}, the 

797 
would be code thms for @{const fold_mset} become thms like 

798 
@{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but 

799 
contains defined symbols, i.e.\ is not a code thm. Hence a separate 

800 
constant with its own code thms needs to be introduced for @{text 

801 
F}. See the image operator below. 

802 
*} 

803 

804 

805 
subsection {* Image *} 

806 

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

808 
"image_mset f = fold_mset (op + o single o f) {#}" 

809 

810 
interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f 

811 
proof qed (simp add: add_ac fun_eq_iff) 

812 

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

814 
by (simp add: image_mset_def) 

815 

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

817 
by (simp add: image_mset_def) 

818 

819 
lemma image_mset_insert: 

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

821 
by (simp add: image_mset_def add_ac) 

822 

823 
lemma image_mset_union [simp]: 

824 
"image_mset f (M+N) = image_mset f M + image_mset f N" 

825 
apply (induct N) 

826 
apply simp 

827 
apply (simp add: add_assoc [symmetric] image_mset_insert) 

828 
done 

829 

830 
lemma size_image_mset [simp]: "size (image_mset f M) = size M" 

831 
by (induct M) simp_all 

832 

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

834 
by (cases M) auto 

835 

836 
syntax 

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

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

839 
translations 

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

841 

842 
syntax 

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

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

845 
translations 

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

847 

848 
text {* 

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

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

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

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

853 
*} 

854 

855 
enriched_type image_mset: image_mset 

856 
proof  

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

858 
proof 

859 
fix A 

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

861 
by (induct A) simp_all 

862 
qed 

863 
show "image_mset id = id" 

864 
proof 

865 
fix A 

866 
show "image_mset id A = id A" 

867 
by (induct A) simp_all 

868 
qed 

869 
qed 

870 

871 

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

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

873 

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

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

875 

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

876 
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

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

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

879 

37107  880 
lemma in_multiset_in_set: 
881 
"x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs" 

882 
by (induct xs) simp_all 

883 

884 
lemma count_multiset_of: 

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

886 
by (induct xs) simp_all 

887 

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

888 
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

889 
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

890 

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

891 
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

892 
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

893 

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

895 
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

896 

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

897 
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

898 
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

899 

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

902 

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

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

905 
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

906 

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

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

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

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

910 

40950  911 
lemma multiset_of_rev [simp]: 
912 
"multiset_of (rev xs) = multiset_of xs" 

913 
by (induct xs) simp_all 

914 

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

915 
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

916 
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

917 
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

918 
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

919 
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

920 
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

921 
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

922 
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

923 

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

925 
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

926 

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

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

929 
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

930 
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

931 
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

932 
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

933 
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

934 
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

935 

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

936 
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

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

938 
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

939 

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

940 
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

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

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

943 
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

944 

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

946 
"(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

947 
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

948 
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

949 
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

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

951 
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

952 
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

953 

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

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

956 
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

957 

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

958 
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

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

960 
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

961 

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

963 
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

964 
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

965 
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

966 
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

967 
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

968 

36903  969 
lemma multiset_of_remove1[simp]: 
970 
"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

971 
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

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 multiset_of_eq_length: 
37107  974 
assumes "multiset_of xs = multiset_of ys" 
975 
shows "length xs = length ys" 

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

977 

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

978 
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

979 
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

980 
shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)" 
48012  981 
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

982 

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

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

984 
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

985 
and equiv: "multiset_of xs = multiset_of ys" 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

986 
shows "fold f xs = fold f ys" 
46921  987 
using f equiv [symmetric] 
988 
proof (induct xs arbitrary: ys) 

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

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

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

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

992 
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

993 
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

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

995 
moreover from * have "x \<in> set ys" by simp 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

996 
ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split) 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

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

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

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

1000 

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

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

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

1003 

40210
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
39533
diff
changeset

1004 
lemma multiset_of_insort [simp]: 
39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1005 
"multiset_of (insort_key k x xs) = {#x#} + multiset_of xs" 
37107  1006 
by (induct xs) (simp_all add: ac_simps) 
39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1007 

40210
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
39533
diff
changeset

1008 
lemma multiset_of_sort [simp]: 
39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1009 
"multiset_of (sort_key k xs) = multiset_of xs" 
37107  1010 
by (induct xs) (simp_all add: ac_simps) 
1011 

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

1012 
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

1013 
This lemma shows which properties suffice to show that a function 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1014 
@{text "f"} with @{text "f xs = ys"} behaves like sort. 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1015 
*} 
37074  1016 

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

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

1018 
assumes "multiset_of ys = multiset_of xs" 
40305
41833242cc42
tuned lemma proposition of properties_for_sort_key
haftmann
parents:
40303
diff
changeset

1019 
and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs" 
39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1020 
and "sorted (map f ys)" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1021 
shows "sort_key f xs = ys" 
46921  1022 
using assms 
1023 
proof (induct xs arbitrary: ys) 

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

1024 
case Nil 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

1025 
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

1026 
case (Cons x xs) 
39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1027 
from Cons.prems(2) have 
40305
41833242cc42
tuned lemma proposition of properties_for_sort_key
haftmann
parents:
40303
diff
changeset

1028 
"\<forall>k \<in> set ys. filter (\<lambda>x. f k = f x) (remove1 x ys) = filter (\<lambda>x. f k = f x) xs" 
39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1029 
by (simp add: filter_remove1) 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1030 
with Cons.prems have "sort_key f xs = remove1 x ys" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1031 
by (auto intro!: Cons.hyps simp add: sorted_map_remove1) 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1032 
moreover from Cons.prems have "x \<in> set ys" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1033 
by (auto simp add: mem_set_multiset_eq intro!: ccontr) 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1034 
ultimately show ?case using Cons.prems by (simp add: insort_key_remove1) 
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

1035 
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

1036 

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

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

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

1039 
and "sorted ys" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1040 
shows "sort xs = ys" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1041 
proof (rule properties_for_sort_key) 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1042 
from multiset show "multiset_of ys = multiset_of xs" . 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1043 
from `sorted ys` show "sorted (map (\<lambda>x. x) ys)" by simp 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1044 
from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1045 
by (rule 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

1046 
then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1047 
by simp 
40305
41833242cc42
tuned lemma proposition of properties_for_sort_key
haftmann
parents:
40303
diff
changeset

1048 
then show "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs" 
39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1049 
by (simp add: replicate_length_filter) 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

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

1051 

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

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

1053 
"sort_key f xs = sort_key f [x\<leftarrow>xs. f x < f (xs ! (length xs div 2))] 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1054 
@ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))] 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1055 
@ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs") 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1056 
proof (rule properties_for_sort_key) 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1057 
show "multiset_of ?rhs = multiset_of ?lhs" 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1058 
by (rule multiset_eqI) (auto simp add: multiset_of_filter) 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

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

1060 
show "sorted (map f ?rhs)" 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1061 
by (auto simp add: sorted_append intro: sorted_map_same) 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1062 
next 
40305
41833242cc42
tuned lemma proposition of properties_for_sort_key
haftmann
parents:
40303
diff
changeset

1063 
fix l 
41833242cc42
tuned lemma proposition of properties_for_sort_key
haftmann
parents:
40303
diff
changeset

1064 
assume "l \<in> set ?rhs" 
40346  1065 
let ?pivot = "f (xs ! (length xs div 2))" 
1066 
have *: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto 

40306  1067 
have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]" 
40305
41833242cc42
tuned lemma proposition of properties_for_sort_key
haftmann
parents:
40303
diff
changeset

1068 
unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) 
40346  1069 
with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp 
1070 
have "\<And>x P. P (f x) ?pivot \<and> f l = f x \<longleftrightarrow> P (f l) ?pivot \<and> f l = f x" by auto 

1071 
then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] = 

1072 
[x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp 

1073 
note *** = this [of "op <"] this [of "op >"] this [of "op ="] 

40306  1074 
show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]" 
40305
41833242cc42
tuned lemma proposition of properties_for_sort_key
haftmann
parents:
40303
diff
changeset

1075 
proof (cases "f l" ?pivot rule: linorder_cases) 
46730  1076 
case less 
1077 
then have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto 

1078 
with less show ?thesis 

40346  1079 
by (simp add: filter_sort [symmetric] ** ***) 
40305
41833242cc42
tuned lemma proposition of properties_for_sort_key
haftmann
parents:
40303
diff
changeset

1080 
next 
40306  1081 
case equal then show ?thesis 
40346  1082 
by (simp add: * less_le) 
40305
41833242cc42
tuned lemma proposition of properties_for_sort_key
haftmann
parents:
40303
diff
changeset

1083 
next 
46730  1084 
case greater 
1085 
then have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto 

1086 
with greater show ?thesis 

40346  1087 
by (simp add: filter_sort [symmetric] ** ***) 
40306  1088 
qed 
40303
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

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

1090 

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

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

1092 
"sort xs = sort [x\<leftarrow>xs. x < xs ! (length xs div 2)] 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1093 
@ [x\<leftarrow>xs. x = xs ! (length xs div 2)] 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1094 
@ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs") 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1095 
using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1096 

40347
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1097 
text {* A stable parametrized quicksort *} 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1098 

429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1099 
definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1100 
"part f pivot xs = ([x \<leftarrow> xs. f x < pivot], [x \<leftarrow> xs. f x = pivot], [x \<leftarrow> xs. pivot < f x])" 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1101 

429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1102 
lemma part_code [code]: 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1103 
"part f pivot [] = ([], [], [])" 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1104 
"part f pivot (x # xs) = (let (lts, eqs, gts) = part f pivot xs; x' = f x in 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1105 
if x' < pivot then (x # lts, eqs, gts) 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1106 
else if x' > pivot then (lts, eqs, x # gts) 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1107 
else (lts, x # eqs, gts))" 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1108 
by (auto simp add: part_def Let_def split_def) 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1109 

429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1110 
lemma sort_key_by_quicksort_code [code]: 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1111 
"sort_key f xs = (case xs of [] \<Rightarrow> [] 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1112 
 [x] \<Rightarrow> xs 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1113 
 [x, y] \<Rightarrow> (if f x \<le> f y then xs else [y, x]) 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1114 
 _ \<Rightarrow> (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1115 
in sort_key f lts @ eqs @ sort_key f gts))" 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1116 
proof (cases xs) 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1117 
case Nil then show ?thesis by simp 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1118 
next 
46921  1119 
case (Cons _ ys) note hyps = Cons show ?thesis 
1120 
proof (cases ys) 

40347
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1121 
case Nil with hyps show ?thesis by simp 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1122 
next 
46921  1123 
case (Cons _ zs) note hyps = hyps Cons show ?thesis 
1124 
proof (cases zs) 

40347
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1125 
case Nil with hyps show ?thesis by auto 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1126 
next 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1127 
case Cons 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1128 
from sort_key_by_quicksort [of f xs] 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1129 
have "sort_key f xs = (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1130 
in sort_key f lts @ eqs @ sort_key f gts)" 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1131 
by (simp only: split_def Let_def part_def fst_conv snd_conv) 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1132 
with hyps Cons show ?thesis by (simp only: list.cases) 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1133 
qed 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1134 
qed 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1135 
qed 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1136 

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

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

1138 

40347
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1139 
hide_const (open) part 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

1140 

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

1141 
lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

1142 
by (induct xs) (auto intro: order_trans) 
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

1143 

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

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

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

1146 
proof (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

1147 
case Nil 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

1148 
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

1149 
case (Cons x 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

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

1151 
proof (cases 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

1152 
case 0 then 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

1153 
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

1154 
case (Suc 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

1155 
with Cons 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

1156 
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

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

1158 
apply (subst add_commute [of "{#v#}" "{#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

1159 
apply (subst 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

1160 
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

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

1162 
apply (simp add: mset_le_single nth_mem_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

1163 
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

1164 
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

1165 
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

1166 

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

1167 
lemma multiset_of_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

1168 
"i < length ls \<Longrightarrow> j < length ls \<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

1169 
multiset_of (ls[j := ls ! i, i := ls ! j]) = 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

1170 
by (cases "i = j") (simp_all add: multiset_of_update nth_mem_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

1171 

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

1172 

46168
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1173 
subsubsection {* Association lists  including code generation *} 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1174 

bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1175 
text {* Preliminaries *} 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1176 

bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1177 
text {* Raw operations on lists *} 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1178 

bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1179 
definition join_raw :: "('key \<Rightarrow> 'val \<times> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1180 
where 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1181 
"join_raw f xs ys = foldr (\<lambda>(k, v). map_default k v (%v'. f k (v', v))) ys xs" 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1182 

bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1183 
lemma join_raw_Nil [simp]: 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1184 
"join_raw f xs [] = xs" 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1185 
by (simp add: join_raw_def) 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1186 

bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1187 
lemma join_raw_Cons [simp]: 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1188 
"join_raw f xs ((k, v) # ys) = map_default k v (%v'. f k (v', v)) (join_raw f xs ys)" 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1189 
by (simp add: join_raw_def) 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1190 

bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1191 
lemma map_of_join_raw: 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1192 
assumes "distinct (map fst ys)" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

1193 
shows "map_of (join_raw f xs ys) x = (case map_of xs x of None => map_of ys x  Some v => 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

1194 
(case map_of ys x of None => Some v  Some v' => Some (f x (v, v'))))" 
46168
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1195 
using assms 
bef8c811df20
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
bulwahn
parents:
45989
diff
changeset

1196 
apply (induct ys) 