author  haftmann 
Wed, 03 Nov 2010 12:15:47 +0100  
changeset 40347  429bf4388b2f 
parent 40346  58af2b8327b7 
child 40606  af1a0b0c6202 
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 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

8 
imports Main 
15131  9 
begin 
10249  10 

11 
subsection {* The type of multisets *} 

12 

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

13 
typedef 'a multiset = "{f :: 'a => nat. finite {x. f x > 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

14 
morphisms count Abs_multiset 
10249  15 
proof 
11464  16 
show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp 
10249  17 
qed 
18 

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

19 
lemmas multiset_typedef = Abs_multiset_inverse count_inverse count 
19086  20 

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

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

26145  24 
notation (xsymbols) 
25 
Melem (infix "\<in>#" 50) 

10249  26 

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

27 
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

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

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

30 

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

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

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

33 
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

34 

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

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

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 

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

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

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

41 
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

42 

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

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

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

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

46 

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

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

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

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

50 

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

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

52 
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

53 
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

54 
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

55 
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

56 
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

57 
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

58 
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

59 
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

60 

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

62 
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

63 
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

64 
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

65 
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

66 
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

67 
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

68 
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

69 
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

70 

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

72 
union_preserves_multiset diff_preserves_multiset MCollect_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

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 

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

75 
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

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 
text {* Multiset comprehension *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

78 

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

79 
definition MCollect :: "'a multiset => ('a => bool) => 'a multiset" where 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

80 
"MCollect M P = Abs_multiset (\<lambda>x. if P x then count M x 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

81 

10249  82 
syntax 
26033  83 
"_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ :# _./ _#})") 
10249  84 
translations 
26033  85 
"{#x :# M. P#}" == "CONST MCollect M (\<lambda>x. P)" 
10249  86 

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

89 

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

90 
instantiation multiset :: (type) "{zero, plus}" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

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

92 

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

93 
definition Mempty_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

94 
"0 = Abs_multiset (\<lambda>a. 0)" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

95 

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

96 
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

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

98 

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

99 
definition union_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

100 
"M + N = Abs_multiset (\<lambda>a. count M a + count N a)" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

101 

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

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

103 

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

104 
end 
10249  105 

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

106 
definition single :: "'a => '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

107 
"single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)" 
15869  108 

26145  109 
syntax 
26176  110 
"_multiset" :: "args => 'a multiset" ("{#(_)#}") 
25507  111 
translations 
112 
"{#x, xs#}" == "{#x#} + {#xs#}" 

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

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 
lemma count_empty [simp]: "count {#} 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

116 
by (simp add: Mempty_def in_multiset multiset_typedef) 
10249  117 

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

118 
lemma count_single [simp]: "count {#b#} a = (if b = a 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

119 
by (simp add: single_def in_multiset multiset_typedef) 
29901  120 

10249  121 

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

122 
subsection {* Basic operations *} 
10249  123 

124 
subsubsection {* Union *} 

125 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
lemma count_union [simp]: "count (M + N) a = count M a + count 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

127 
by (simp add: union_def in_multiset multiset_typedef) 
10249  128 

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

129 
instance multiset :: (type) cancel_comm_monoid_add proof 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

130 
qed (simp_all add: multiset_eq_iff) 
10277  131 

10249  132 

133 
subsubsection {* Difference *} 

134 

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

136 
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

137 

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

138 
definition diff_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

139 
"M  N = Abs_multiset (\<lambda>a. count M a  count 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

140 

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

141 
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

142 

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

143 
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

144 

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

145 
lemma count_diff [simp]: "count (M  N) a = count M a  count 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

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

147 

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

149 
by(simp add: multiset_eq_iff) 
36903  150 

151 
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

152 
by (rule multiset_eqI) simp 
10249  153 

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

155 
by(simp add: multiset_eq_iff) 
10249  156 

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

158 
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

159 

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

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

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

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

163 

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

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

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

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

167 

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

168 
lemma diff_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

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

170 
by (auto simp add: multiset_eq_iff) 
36903  171 

172 
lemma diff_add: 

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

174 
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

175 

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

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

178 
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

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

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

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

183 

10249  184 

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

186 

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

187 
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

188 
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

189 

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

190 
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

191 
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

192 

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

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

197 
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

198 

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

200 
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

201 

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

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

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

204 
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

205 

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

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

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

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

209 

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

210 
lemma union_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

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

212 
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

213 

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

214 
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

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

216 
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

217 

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

220 
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

221 
next 
36903  222 
assume ?lhs thus ?rhs 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

223 
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

224 
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

225 

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

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

228 
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

229 

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

231 
"M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N  {#a#} + {#b#} \<and> N = M  {#b#} + {#a#}" (is "?lhs = ?rhs") 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

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

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

235 
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

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

237 
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

238 
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

239 
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

240 
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

241 
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

242 
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

243 
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

244 
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

245 
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

246 
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

247 
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

248 
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

249 
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

250 
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

251 

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

253 
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

254 
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

255 
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

256 
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

257 
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

258 
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

259 
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

260 
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

261 
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

262 

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

263 
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

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

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

266 
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

267 

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

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

269 
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

270 

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

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

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

273 

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

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

275 
mset_le_def: "A \<le> B \<longleftrightarrow> (\<forall>a. count A a \<le> count B 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

276 

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

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

278 
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

279 

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

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

281 
qed (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

282 

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

283 
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

284 

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

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

287 
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

288 

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

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

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

291 
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

292 
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

293 
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

294 

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

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

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

297 
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

298 

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

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

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

301 
by (fact add_le_cancel_left) 
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_mono_add: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

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

305 
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

306 

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

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

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

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

310 

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

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

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

313 
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

314 

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

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

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

317 
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

318 

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

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

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

321 
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

322 

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

325 
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

326 

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

329 

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

330 
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

331 
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

332 
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

333 
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

334 
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

335 

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

336 
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

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

339 
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

340 
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

341 

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

342 
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

343 
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

344 
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

345 
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

346 
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

347 
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

348 
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

349 
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

350 

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

351 
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

352 
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

353 
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

354 
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

355 
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

356 

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

357 
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

358 
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

359 

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

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

361 
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

362 

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

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

364 
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

365 

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

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

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

368 
by (fact add_less_imp_less_right) 
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 
lemma mset_less_empty_nonempty: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

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

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

373 

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

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

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

376 
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

377 

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

378 

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

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

380 

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

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

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

383 

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

384 
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

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

386 

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

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

388 
have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n  (n  q)" by arith 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

389 
show "OFCLASS('a multiset, semilattice_inf_class)" proof 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

390 
qed (auto simp add: multiset_inter_def mset_le_def aux) 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

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

392 

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

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

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

397 

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

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

399 
"count (A #\<inter> B) x = min (count A x) (count B x)" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

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

401 

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

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

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

404 

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

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

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

407 
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

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

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

410 
from assms have "min (count B x) (count C x) = 0" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

411 
by (auto simp add: multiset_inter_count multiset_eq_iff) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

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

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

414 
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

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

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

417 

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

418 

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

419 
subsubsection {* Comprehension (filter) *} 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

420 

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

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

422 
"count {# x:#M. P x #} a = (if P a then count M a else 0)" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

423 
by (simp add: MCollect_def in_multiset multiset_typedef) 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

424 

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

425 
lemma MCollect_empty [simp]: "MCollect {#} 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

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

427 

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

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

429 
"MCollect {#x#} P = (if P x then {#x#} else {#})" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

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

431 

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

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

433 
"MCollect (M + N) f = MCollect M f + MCollect N f" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

434 
by (rule multiset_eqI) simp 
10249  435 

436 

437 
subsubsection {* Set of elements *} 

438 

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

439 
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

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

441 

17161  442 
lemma set_of_empty [simp]: "set_of {#} = {}" 
26178  443 
by (simp add: set_of_def) 
10249  444 

17161  445 
lemma set_of_single [simp]: "set_of {#b#} = {b}" 
26178  446 
by (simp add: set_of_def) 
10249  447 

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

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

452 
by (auto simp add: set_of_def multiset_eq_iff) 
10249  453 

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

26033  457 
lemma set_of_MCollect [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}" 
26178  458 
by (auto simp add: set_of_def) 
10249  459 

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

460 
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

461 
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

462 

10249  463 

464 
subsubsection {* Size *} 

465 

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

466 
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

467 
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

468 

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

469 
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

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

471 

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

472 
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

473 

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

474 
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

475 

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

476 
lemma size_empty [simp]: "size {#} = 0" 
26178  477 
by (simp add: size_def) 
10249  478 

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

479 
lemma size_single [simp]: "size {#b#} = 1" 
26178  480 
by (simp add: size_def) 
10249  481 

17161  482 
lemma setsum_count_Int: 
26178  483 
"finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A" 
484 
apply (induct rule: finite_induct) 

485 
apply simp 

486 
apply (simp add: Int_insert_left set_of_def) 

487 
done 

10249  488 

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

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

492 
prefer 2 

493 
apply (rule ext, simp) 

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

495 
apply (subst Int_commute) 

496 
apply (simp (no_asm_simp) add: setsum_count_Int) 

497 
done 

10249  498 

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

500 
by (auto simp add: size_def multiset_eq_iff) 
26016  501 

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

26178  503 
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty) 
10249  504 

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

508 
apply auto 

509 
done 

10249  510 

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

511 
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

512 
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

513 
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

514 
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

515 
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

516 
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

517 
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

518 
then show ?thesis by blast 
23611  519 
qed 
15869  520 

26016  521 

522 
subsection {* Induction and case splits *} 

10249  523 

524 
lemma setsum_decr: 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11655
diff
changeset

525 
"finite F ==> (0::nat) < f a ==> 
15072  526 
setsum (f (a := f a  1)) F = (if a\<in>F then setsum f F  1 else setsum f F)" 
26178  527 
apply (induct rule: finite_induct) 
528 
apply auto 

529 
apply (drule_tac a = a in mk_disjoint_insert, auto) 

530 
done 

10249  531 

10313  532 
lemma rep_multiset_induct_aux: 
26178  533 
assumes 1: "P (\<lambda>a. (0::nat))" 
534 
and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))" 

535 
shows "\<forall>f. f \<in> multiset > setsum f {x. f x \<noteq> 0} = n > P f" 

536 
apply (unfold multiset_def) 

537 
apply (induct_tac n, simp, clarify) 

538 
apply (subgoal_tac "f = (\<lambda>a.0)") 

539 
apply simp 

540 
apply (rule 1) 

541 
apply (rule ext, force, clarify) 

542 
apply (frule setsum_SucD, clarify) 

543 
apply (rename_tac a) 

544 
apply (subgoal_tac "finite {x. (f (a := f a  1)) x > 0}") 

545 
prefer 2 

546 
apply (rule finite_subset) 

547 
prefer 2 

548 
apply assumption 

549 
apply simp 

550 
apply blast 

551 
apply (subgoal_tac "f = (f (a := f a  1))(a := (f (a := f a  1)) a + 1)") 

552 
prefer 2 

553 
apply (rule ext) 

554 
apply (simp (no_asm_simp)) 

555 
apply (erule ssubst, rule 2 [unfolded multiset_def], blast) 

556 
apply (erule allE, erule impE, erule_tac [2] mp, blast) 

557 
apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def) 

558 
apply (subgoal_tac "{x. x \<noteq> a > f x \<noteq> 0} = {x. f x \<noteq> 0}") 

559 
prefer 2 

560 
apply blast 

561 
apply (subgoal_tac "{x. x \<noteq> a \<and> f x \<noteq> 0} = {x. f x \<noteq> 0}  {a}") 

562 
prefer 2 

563 
apply blast 

564 
apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong) 

565 
done 

10249  566 

10313  567 
theorem rep_multiset_induct: 
11464  568 
"f \<in> multiset ==> P (\<lambda>a. 0) ==> 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11655
diff
changeset

569 
(!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" 
26178  570 
using rep_multiset_induct_aux by blast 
10249  571 

18258  572 
theorem multiset_induct [case_names empty add, induct type: multiset]: 
26178  573 
assumes empty: "P {#}" 
574 
and add: "!!M x. P M ==> P (M + {#x#})" 

575 
shows "P M" 

10249  576 
proof  
577 
note defns = union_def single_def Mempty_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

578 
note add' = add [unfolded defns, simplified] 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
have aux: "\<And>a::'a. count (Abs_multiset (\<lambda>b. if b = a 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

580 
(\<lambda>b. if b = a then 1 else 0)" by (simp add: Abs_multiset_inverse in_multiset) 
10249  581 
show ?thesis 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
apply (rule count_inverse [THEN subst]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
apply (rule count [THEN rep_multiset_induct]) 
18258  584 
apply (rule empty [unfolded defns]) 
15072  585 
apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))") 
10249  586 
prefer 2 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

587 
apply (simp add: fun_eq_iff) 
10249  588 
apply (erule ssubst) 
17200  589 
apply (erule Abs_multiset_inverse [THEN subst]) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

590 
apply (drule add') 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
apply (simp add: aux) 
10249  592 
done 
593 
qed 

594 

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

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

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

601 
shows "P" 

25610  602 
proof (cases "M = {#}") 
26145  603 
assume "M = {#}" then show ?thesis using em by simp 
25610  604 
next 
605 
assume "M \<noteq> {#}" 

606 
then obtain M' m where "M = M' + {#m#}" 

607 
by (blast dest: multi_nonempty_split) 

26145  608 
then show ?thesis using add by simp 
25610  609 
qed 
610 

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

26178  612 
apply (cases M) 
613 
apply simp 

614 
apply (rule_tac x="M  {#x#}" in exI, simp) 

615 
done 

25610  616 

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

618 
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

619 

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

621 
apply (subst multiset_eq_iff) 
26178  622 
apply auto 
623 
done 

10249  624 

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

625 
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

626 
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

627 
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

628 
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

629 
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

630 
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

631 
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

632 
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

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

634 
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

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

636 
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

637 
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

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

639 
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

640 
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

641 
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

642 
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

643 
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

644 

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

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

646 
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

647 

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

649 

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

650 
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

651 

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

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

654 
"mset_less_rel = {(A,B). A < B}" 
10249  655 

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

656 
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

657 
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

658 
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

659 
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

660 
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

661 
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

662 
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

663 
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

664 
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

665 
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

666 
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

667 

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

668 
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

669 
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

670 
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

671 
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

672 
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

673 

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

674 
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

675 

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

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

677 
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

678 
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

679 
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

680 
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

681 
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

682 

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

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

684 
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

685 
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

686 
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

687 
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

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

689 
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

690 
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

691 
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

692 
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

693 
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

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

695 
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

696 
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

697 
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

698 
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

699 
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

700 
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

701 
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

702 
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

703 
qed 
26145  704 

17161  705 

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

706 
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

707 

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

708 
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

709 

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

710 
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

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

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

713 

37107  714 
lemma in_multiset_in_set: 
715 
"x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs" 

716 
by (induct xs) simp_all 

717 

718 
lemma count_multiset_of: 

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

720 
by (induct xs) simp_all 

721 

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

722 
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

723 
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

724 

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

725 
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

726 
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

727 

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

728 
lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set 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

729 
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

730 

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

731 
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

732 
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

733 

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

734 
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

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

736 
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

737 

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

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

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

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

741 

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

742 
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

743 
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

744 
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

745 
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

746 
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

747 
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

748 
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

749 
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

750 

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

751 
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

752 
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

753 

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

754 
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

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

756 
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

757 
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

758 
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

759 
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

760 
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

761 
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

762 

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

763 
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

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

765 
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

766 

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

767 
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

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

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

770 
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

771 

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

772 
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

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

774 
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

775 
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

776 
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

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

778 
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

779 
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

780 

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

781 
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

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

783 
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

784 

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

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

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

787 
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

788 

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

789 
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

790 
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

791 
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

792 
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

793 
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

794 
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

795 

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

798 
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

799 

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

800 
lemma multiset_of_eq_length: 
37107  801 
assumes "multiset_of xs = multiset_of ys" 
802 
shows "length xs = length ys" 

803 
using assms proof (induct xs arbitrary: ys) 

804 
case Nil then show ?case by simp 

805 
next 

806 
case (Cons x xs) 

807 
then have "x \<in># multiset_of ys" by (simp add: union_single_eq_member) 

808 
then have "x \<in> set ys" by (simp add: in_multiset_in_set) 

809 
from Cons.prems [symmetric] have "multiset_of xs = multiset_of (remove1 x ys)" 

810 
by simp 

811 
with Cons.hyps have "length xs = length (remove1 x ys)" . 

812 
with `x \<in> set ys` show ?case 

813 
by (auto simp add: length_remove1 dest: length_pos_if_in_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

814 
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

815 

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

816 
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

817 
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

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

819 
proof (cases "z \<in># multiset_of xs") 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

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

821 
moreover have "\<not> z \<in># multiset_of ys" using assms False by simp 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

822 
ultimately show ?thesis by (simp add: count_filter) 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

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

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

825 
moreover have "z \<in># multiset_of ys" using assms True by simp 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

826 
show ?thesis using assms proof (induct xs arbitrary: ys) 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

827 
case Nil then show ?case by simp 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

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

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

830 
from `multiset_of (x # xs) = multiset_of ys` [symmetric] 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

831 
have *: "multiset_of xs = multiset_of (remove1 x ys)" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

832 
and "x \<in> set ys" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

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

834 
from * have "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) (remove1 x ys))" by (rule Cons.hyps) 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

835 
moreover from `x \<in> set ys` have "length (filter (\<lambda>y. x = y) ys) > 0" by (simp add: filter_empty_conv) 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

836 
ultimately show ?case using `x \<in> set ys` 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

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

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

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

840 

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

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

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

843 

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

844 
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

845 
"multiset_of (insort_key k x xs) = {#x#} + multiset_of xs" 
37107  846 
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

847 

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

848 
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

849 
"multiset_of (sort_key k xs) = multiset_of xs" 
37107  850 
by (induct xs) (simp_all add: ac_simps) 
851 

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

852 
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

853 
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

854 
@{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

855 
*} 
37074  856 

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

857 
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

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

859 
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

860 
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

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

862 
using assms 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

863 
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

864 
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

865 
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

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

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

868 
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

869 
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

870 
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

871 
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

872 
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

873 
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

874 
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

875 

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

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

877 
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

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

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

880 
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

881 
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

882 
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

883 
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

884 
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

885 
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

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

887 
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

888 
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

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

890 

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

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

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

893 
@ [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

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

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

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

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

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

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

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

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

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

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

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

907 
unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) 
40346  908 
with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp 
909 
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 

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

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

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

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

914 
proof (cases "f l" ?pivot rule: linorder_cases) 
40307  915 
case less then moreover have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto 
916 
ultimately show ?thesis 

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

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

921 
next 
40307  922 
case greater then moreover have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto 
923 
ultimately show ?thesis 

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

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

927 

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

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

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

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

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

932 
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

933 

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

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

935 

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

936 
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

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

938 

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

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

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

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

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

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

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

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

946 

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

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

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

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

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

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

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

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

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

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

956 
case (Cons _ ys) note hyps = Cons show ?thesis proof (cases ys) 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

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

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

959 
case (Cons _ zs) note hyps = hyps Cons show ?thesis proof (cases zs) 
429bf4388b2f
added code lemmas for stable parametrized quicksort
haftmann
parents:
40346
diff
changeset

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

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

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

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

964 
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

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

966 
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

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

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

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

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

971 

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

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

973 

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

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

975 

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

976 
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

977 
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

978 

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

979 
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

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

981 
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

982 
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

983 
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

984 
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

985 
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

986 
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

987 
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

988 
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

989 
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

990 
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

991 
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

992 
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

993 
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

994 
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

995 
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

996 
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

997 
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

998 
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

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

1000 
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

1001 

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

1002 
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

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

1004 
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

1005 
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

1006 

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

1007 

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

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

1009 

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

1010 
definition count_of :: "('a \<times> nat) list \<Rightarrow> 'a \<Rightarrow> nat" 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

1011 
"count_of xs x = (case map_of xs x of None \<Rightarrow> 0  Some n \<Rightarrow> 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

1012 

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

1014 
"count_of xs \<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

1015 
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

1016 
let ?A = "{x::'a. 0 < (case map_of xs x of None \<Rightarrow> 0\<Colon>nat  Some (n\<Colon>nat) \<Rightarrow> 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

1017 
have "?A \<subseteq> dom (map_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

1018 
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

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

1020 
assume "x \<in> ?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

1021 
then have "0 < (case map_of xs x of None \<Rightarrow> 0\<Colon>nat  Some (n\<Colon>nat) \<Rightarrow> n)" 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

1022 
then have "map_of xs x \<noteq> None" by (cases "map_of xs 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

1023 
then show "x \<in> dom (map_of xs)" 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

1024 
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

1025 
with finite_dom_map_of [of xs] have "finite ?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

1026 
by (auto 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

1027 
then show ?thesis 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

1028 
by (simp add: count_of_def fun_eq_iff 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

1029 
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

1030 

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

1031 
lemma count_simps [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

1032 
"count_of [] = (\<lambda>_. 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

1033 
"count_of ((x, n) # xs) = (\<lambda>y. if x = y then n else count_of xs 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

1034 
by (simp_all add: count_of_def 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

1035 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
lemma count_of_empty: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1037 
"x \<notin> fst ` set xs \<Longrightarrow> count_of xs x = 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

1038 
by (induct xs) (simp_all add: count_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

1039 

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

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

1041 
"count_of (filter (P \<circ> fst) xs) x = (if P x then count_of xs x 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

1042 
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

1043 

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

1044 
definition Bag :: "('a \<times> nat) 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

1045 
"Bag xs = Abs_multiset (count_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

1046 

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

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

1048 

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

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

1050 
"count (Bag xs) = count_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

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

1052 

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

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

1054 
"{#} = Bag []" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

1055 
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

1056 

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

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

1058 
"{#x#} = Bag [(x, 1)]" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

1059 
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

1060 

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

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

1062 
"MCollect (Bag xs) P = Bag (filter (P \<circ> fst) xs)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

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

1064 

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

1065 
lemma mset_less_eq_Bag [code]: 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

1066 
"Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A 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

1067 
(is "?lhs \<longleftrightarrow> ?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

1068 
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

1069 
assume ?lhs then 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

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

1071 
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

1072 
assume ?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

1073 
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

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

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

1076 
from `?rhs` have "count_of xs x \<le> count A 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

1077 
by (cases "x \<in> fst ` set xs") (auto simp add: count_of_empty) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1078 
then show "count (Bag xs) x \<le> count A 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

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

1080 
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

1081 
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

1082 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

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

1084 
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

1085 

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

1086 
definition 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

1087 
"HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<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

1088 

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

1089 
instance proof 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

1090 
qed (simp add: equal_multiset_def 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

1091 

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

1092 
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

1093 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

1094 
lemma [code nbe]: 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

1095 
"HOL.equal (A :: 'a::equal multiset) A \<longleftrightarrow> True" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

1096 
by (fact equal_refl) 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

1097 

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

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

1099 
bagify :: "('a\<Colon>typerep \<times> nat) list \<times> (unit \<Rightarrow> Code_Evaluation.term) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1100 
\<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" 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

1101 
[code_unfold]: "bagify xs = Code_Evaluation.valtermify Bag {\<cdot>} 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

1102 

37751  1103 
notation fcomp (infixl "\<circ>>" 60) 
1104 
notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

1105 

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

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

1107 
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

1108 

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

1109 
definition 
37751  1110 
"Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (bagify xs))" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1111 

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

1112 
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

1113 

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

1114 
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

1115 

37751  1116 
no_notation fcomp (infixl "\<circ>>" 60) 
1117 
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

1118 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35712
diff
changeset

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

1120 

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

1121 

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

1122 
subsection {* The multiset order *} 
10249  1123 

1124 
subsubsection {* Wellfoundedness *} 

1125 

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

1126 
definition mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where 
37765  1127 
"mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> 
23751  1128 
(\<forall>b. b :# K > (b, a) \<in> r)}" 
10249  1129 

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

1130 
definition mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where 
37765  1131 
"mult r = (mult1 r)\<^sup>+" 
10249  1132 

23751  1133 
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r" 
26178  1134 
by (simp add: mult1_def) 
10249  1135 

23751  1136 
lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==> 
1137 
(\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or> 

1138 
(\<exists>K. (\<forall>b. b :# K > (b, a) \<in> r) \<and> N = M0 + K)" 

19582  1139 
(is "_ \<Longrightarrow> ?case1 (mult1 r) \<or> ?case2") 
10249  1140 
proof (unfold mult1_def) 
23751  1141 
let ?r = "\<lambda>K a. \<forall>b. b :# K > (b, a) \<in> r" 
11464  1142 
let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a" 
23751  1143 
let ?case1 = "?case1 {(N, M). ?R N M}" 
10249  1144 

23751  1145 
assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}" 
18258  1146 
then have "\<exists>a' M0' K. 
11464  1147 
M0 + {#a#} = M0' + {#a'#} \<and> N = M0' + K \<and> ?r K a'" by simp 
18258  1148 
then show "?case1 \<or> ?case2" 
10249  1149 
proof (elim exE conjE) 
1150 
fix a' M0' K 

1151 
assume N: "N = M0' + K" and r: "?r K a'" 

1152 
assume "M0 + {#a#} = M0' + {#a'#}" 

18258  1153 
then have "M0 = M0' \<and> a = a' \<or> 
11464  1154 
(\<exists>K'. M0 = K' + {#a'#} \<and> M0' = K' + {#a#})" 
10249  1155 
by (simp only: add_eq_conv_ex) 
18258  1156 
then show ?thesis 
10249  1157 
proof (elim disjE conjE exE) 
1158 
assume "M0 = M0'" "a = a'" 

11464  1159 
with N r have "?r K a \<and> N = M0 + K" by simp 
18258  1160 
then have ?case2 .. then show ?thesis .. 
10249  1161 
next 
1162 
fix K' 

1163 
assume "M0' = K' + {#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

1164 
with N have n: "N = K' + K + {#a#}" by (simp add: add_ac) 
10249  1165 

1166 
assume "M0 = 