author  bulwahn 
Wed, 14 Dec 2011 15:56:29 +0100  
changeset 45866  e62b319c7696 
parent 45694  4a8743618257 
child 45989  b39256df5f8a 
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 

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

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

14 

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

15 
typedef (open) 'a multiset = "multiset :: ('a => nat) set" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

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

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

22 
lemmas multiset_typedef = Abs_multiset_inverse count_inverse count 
19086  23 

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

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

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

10249  29 

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

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

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

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

33 

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

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

35 
"(\<And>x. count A x = count B x) \<Longrightarrow> A = B" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

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

37 

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

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

39 
\medskip Preservation of the representing set @{term multiset}. 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

41 

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

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

43 
"(\<lambda>a. 0) \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

45 

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

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

47 
"(\<lambda>b. if b = a then n else 0) \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

49 

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

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

51 
"M \<in> multiset \<Longrightarrow> N \<in> multiset \<Longrightarrow> (\<lambda>a. M a + N a) \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

53 

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

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

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

56 
shows "(\<lambda>a. M a  N a) \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

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

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

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

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

63 

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

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

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

66 
shows "(\<lambda>x. if P x then M x else 0) \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

68 
have "{x. (P x \<longrightarrow> 0 < M x) \<and> P x} \<subseteq> {x. 0 < M x}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

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

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

73 

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

74 
lemmas in_multiset = const0_in_multiset only1_in_multiset 
41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

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

76 

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

77 

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

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

79 

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

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

81 

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

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

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

84 

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

85 
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

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

87 

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

88 
abbreviation Mempty :: "'a multiset" ("{#}") where 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

90 

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

91 
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

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

93 

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

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

95 

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

96 
end 
10249  97 

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

98 
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

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

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

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

106 

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

108 
by (simp add: Mempty_def in_multiset multiset_typedef) 
10249  109 

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

110 
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

111 
by (simp add: single_def in_multiset multiset_typedef) 
29901  112 

10249  113 

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

114 
subsection {* Basic operations *} 
10249  115 

116 
subsubsection {* Union *} 

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

119 
by (simp add: union_def in_multiset multiset_typedef) 
10249  120 

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

121 
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

122 
qed (simp_all add: multiset_eq_iff) 
10277  123 

10249  124 

125 
subsubsection {* Difference *} 

126 

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

128 
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

129 

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

130 
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

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

132 

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

133 
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

134 

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

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

136 

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

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

139 

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

141 
by(simp add: multiset_eq_iff) 
36903  142 

143 
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

144 
by (rule multiset_eqI) simp 
10249  145 

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

147 
by(simp add: multiset_eq_iff) 
10249  148 

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

150 
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

151 

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

152 
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

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

154 
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

155 

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

156 
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

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

158 
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

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

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

162 
by (auto simp add: multiset_eq_iff) 
36903  163 

164 
lemma diff_add: 

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

166 
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

167 

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

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

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

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

171 

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

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

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

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

175 

10249  176 

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

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

178 

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

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

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

181 

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

182 
lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

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

184 

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

185 
lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

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

187 

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

188 
lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

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

190 

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

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

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

193 

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

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

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

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

197 

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

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

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

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

201 

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

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

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

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

205 

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

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

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

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

209 

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

210 
lemma union_is_single: 
36903  211 
"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

212 
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

213 
next 
36903  214 
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

215 
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

216 
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

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

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

220 
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

221 

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

222 
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

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

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

225 
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

226 
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

227 
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

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

229 
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

230 
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

231 
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

232 
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

233 
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

234 
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

235 
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

236 
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

237 
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

238 
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

239 
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

240 
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

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

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

243 

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

245 
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

246 
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

247 
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

248 
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

249 
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

250 
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

251 
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

252 
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

253 
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

254 

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

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

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

258 
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

259 

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

260 

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

262 

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

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

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

265 

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

266 
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

267 
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

268 

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

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

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

271 

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

272 
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

273 
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

274 

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

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

276 

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

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

278 
"(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le> B" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

280 

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

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

282 
"(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

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

286 

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

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

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

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

290 

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

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

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

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

294 

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

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

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

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

298 

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

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

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

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

302 

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

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

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

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

306 

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

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

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

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

310 

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

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

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

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

314 

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

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

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

318 

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

321 

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

322 
lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

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

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

327 

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

328 
lemma mset_leD: "A \<le> B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

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

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

333 

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

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

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

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

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

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

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

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

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

342 

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

343 
lemma mset_le_insertD: "(A + {#x#} \<le> B) \<Longrightarrow> (x \<in># B \<and> A \<le> B)" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

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

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

348 

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

349 
lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

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

351 

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

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

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

354 

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

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

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

357 

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

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

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

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

361 

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

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

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

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

365 

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

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

367 
"c \<in># B \<Longrightarrow> B  {#c#} < B" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

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

369 

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

370 

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

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

372 

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

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

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

375 

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

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

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

378 

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

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

380 
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

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

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

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

384 

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

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

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

389 

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

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

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

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

393 

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

394 
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

395 
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

396 

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

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

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

399 
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

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

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

402 
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

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

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

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

406 
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

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

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

409 

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

410 

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

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

412 

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

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

414 

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

415 
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

416 
"filter P M = Abs_multiset (\<lambda>x. if P x then count M x else 0)" 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

417 

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

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

419 

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

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

421 
"count (Multiset.filter P M) a = (if P a then count M a else 0)" 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

422 
by (simp add: filter_def in_multiset multiset_typedef) 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

423 

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

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

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

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

427 

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

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

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

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

431 

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

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

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

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

435 

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

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

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

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

439 

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

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

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

442 
by (rule multiset_eqI) simp 
10249  443 

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

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

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

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

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

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

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

450 

10249  451 

452 
subsubsection {* Set of elements *} 

453 

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

454 
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

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

456 

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

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

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

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

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

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

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

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

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

476 
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

477 

10249  478 

479 
subsubsection {* Size *} 

480 

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

481 
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

482 
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

483 

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

484 
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

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

486 

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

487 
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

488 

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

489 
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

490 

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

491 
lemma size_empty [simp]: "size {#} = 0" 
26178  492 
by (simp add: size_def) 
10249  493 

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

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

17161  497 
lemma setsum_count_Int: 
26178  498 
"finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A" 
499 
apply (induct rule: finite_induct) 

500 
apply simp 

501 
apply (simp add: Int_insert_left set_of_def) 

502 
done 

10249  503 

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

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

507 
prefer 2 

508 
apply (rule ext, simp) 

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

510 
apply (subst Int_commute) 

511 
apply (simp (no_asm_simp) add: setsum_count_Int) 

512 
done 

10249  513 

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

515 
by (auto simp add: size_def multiset_eq_iff) 
26016  516 

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

26178  518 
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty) 
10249  519 

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

523 
apply auto 

524 
done 

10249  525 

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

526 
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

527 
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

528 
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

529 
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

530 
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

531 
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

532 
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

533 
then show ?thesis by blast 
23611  534 
qed 
15869  535 

26016  536 

537 
subsection {* Induction and case splits *} 

10249  538 

539 
lemma setsum_decr: 

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

540 
"finite F ==> (0::nat) < f a ==> 
15072  541 
setsum (f (a := f a  1)) F = (if a\<in>F then setsum f F  1 else setsum f F)" 
26178  542 
apply (induct rule: finite_induct) 
543 
apply auto 

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

545 
done 

10249  546 

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

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

551 
apply (unfold multiset_def) 

552 
apply (induct_tac n, simp, clarify) 

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

554 
apply simp 

555 
apply (rule 1) 

556 
apply (rule ext, force, clarify) 

557 
apply (frule setsum_SucD, clarify) 

558 
apply (rename_tac a) 

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

560 
prefer 2 

561 
apply (rule finite_subset) 

562 
prefer 2 

563 
apply assumption 

564 
apply simp 

565 
apply blast 

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

567 
prefer 2 

568 
apply (rule ext) 

569 
apply (simp (no_asm_simp)) 

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

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

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

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

574 
prefer 2 

575 
apply blast 

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

577 
prefer 2 

578 
apply blast 

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

580 
done 

10249  581 

10313  582 
theorem rep_multiset_induct: 
11464  583 
"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

584 
(!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" 
26178  585 
using rep_multiset_induct_aux by blast 
10249  586 

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

590 
shows "P M" 

10249  591 
proof  
592 
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

593 
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

594 
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

595 
(\<lambda>b. if b = a then 1 else 0)" by (simp add: Abs_multiset_inverse in_multiset) 
10249  596 
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

597 
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

598 
apply (rule count [THEN rep_multiset_induct]) 
18258  599 
apply (rule empty [unfolded defns]) 
15072  600 
apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))") 
10249  601 
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

602 
apply (simp add: fun_eq_iff) 
10249  603 
apply (erule ssubst) 
17200  604 
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

605 
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

606 
apply (simp add: aux) 
10249  607 
done 
608 
qed 

609 

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

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

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

616 
shows "P" 

25610  617 
proof (cases "M = {#}") 
26145  618 
assume "M = {#}" then show ?thesis using em by simp 
25610  619 
next 
620 
assume "M \<noteq> {#}" 

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

622 
by (blast dest: multi_nonempty_split) 

26145  623 
then show ?thesis using add by simp 
25610  624 
qed 
625 

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

26178  627 
apply (cases M) 
628 
apply simp 

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

630 
done 

25610  631 

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

633 
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

634 

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

636 
apply (subst multiset_eq_iff) 
26178  637 
apply auto 
638 
done 

10249  639 

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

640 
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

641 
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

642 
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

643 
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

644 
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

645 
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

646 
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

647 
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

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

649 
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

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

651 
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

652 
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

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

654 
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

655 
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

656 
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

657 
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

658 
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

659 

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

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

662 

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

664 

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

666 

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

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

669 
"mset_less_rel = {(A,B). A < B}" 
10249  670 

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

672 
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

673 
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

674 
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

675 
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

676 
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

677 
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

678 
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

679 
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

680 
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

681 
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

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

684 
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

685 
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

686 
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

687 
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

688 

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

689 
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

690 

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

692 
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

693 
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

694 
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

695 
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

696 
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

697 

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

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

699 
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

700 
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

701 
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

702 
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

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

704 
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

705 
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

706 
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

707 
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

708 
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

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

710 
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

711 
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

712 
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

713 
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

714 
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

715 
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

716 
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

717 
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

718 
qed 
26145  719 

17161  720 

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

721 
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

722 

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

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

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

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

728 

37107  729 
lemma in_multiset_in_set: 
730 
"x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs" 

731 
by (induct xs) simp_all 

732 

733 
lemma count_multiset_of: 

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

735 
by (induct xs) simp_all 

736 

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

738 
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

739 

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

740 
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

741 
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

742 

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

744 
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

745 

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

747 
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

748 

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

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

751 
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

752 

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

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

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

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

756 

40950  757 
lemma multiset_of_rev [simp]: 
758 
"multiset_of (rev xs) = multiset_of xs" 

759 
by (induct xs) simp_all 

760 

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

762 
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

763 
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

764 
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

765 
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

766 
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

767 
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

768 
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

769 

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

770 
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

771 
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

772 

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

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

775 
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

776 
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

777 
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

778 
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

779 
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

780 
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

781 

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

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

784 
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

785 

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

786 
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

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

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

789 
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

790 

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

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

793 
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

794 
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

795 
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

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

797 
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

798 
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

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

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

802 
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

803 

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

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

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

806 
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

807 

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

808 
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

809 
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

810 
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

811 
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

812 
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

813 
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

814 

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

817 
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

818 

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

819 
lemma multiset_of_eq_length: 
37107  820 
assumes "multiset_of xs = multiset_of ys" 
821 
shows "length xs = length ys" 

822 
using assms proof (induct xs arbitrary: ys) 

823 
case Nil then show ?case by simp 

824 
next 

825 
case (Cons x xs) 

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

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

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

829 
by simp 

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

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

832 
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

833 
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

834 

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

835 
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

836 
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

837 
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

838 
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

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

840 
moreover have "\<not> z \<in># multiset_of ys" using assms False by simp 
41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

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

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

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

844 
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

845 
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

846 
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

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

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

849 
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

850 
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

851 
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

852 
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

853 
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

854 
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

855 
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

856 
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

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

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

859 

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

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

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

862 

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

863 
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

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

866 

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

867 
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

868 
"multiset_of (sort_key k xs) = multiset_of xs" 
37107  869 
by (induct xs) (simp_all add: ac_simps) 
870 

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

871 
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

872 
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

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

874 
*} 
37074  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_key: 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

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

878 
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

879 
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

880 
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

881 
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

882 
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

883 
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

884 
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

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

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

887 
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

888 
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

889 
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

890 
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

891 
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

892 
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

893 
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

894 

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

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

896 
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

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

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

899 
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

900 
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

901 
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

902 
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

903 
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

904 
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

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

906 
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

907 
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

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

909 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

940 
next 
40307  941 
case greater then moreover have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto 
942 
ultimately show ?thesis 

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

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

946 

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

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

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

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

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

951 
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

952 

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

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

954 

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

955 
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

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

957 

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

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

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

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

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

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

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

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

965 

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

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

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

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

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

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

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

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

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

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

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

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

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

978 
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

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

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

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

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

983 
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

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

985 
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

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

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

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

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

990 

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

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

992 

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

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

994 

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

995 
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

996 
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

997 

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

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

1000 
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

1001 
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

1002 
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

1003 
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

1004 
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

1005 
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

1006 
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

1007 
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

1008 
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

1009 
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

1010 
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

1011 
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

1012 
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

1013 
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

1014 
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

1015 
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

1016 
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

1017 
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

1018 
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

1019 
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

1020 

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

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

1023 
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

1024 
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

1025 

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

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

1028 

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

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

1031 

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

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

1034 
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

1035 
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

1036 
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

1037 
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

1038 
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

1039 
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

1040 
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

1041 
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

1042 
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

1043 
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

1044 
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

1045 
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

1046 
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

1047 
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

1048 
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

1049 

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

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

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

1053 
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

1054 

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

1055 
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

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

1057 
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

1058 

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

1059 
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

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

1061 
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

1062 

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

1063 
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

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

1065 

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

1066 
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

1067 

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

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

1070 
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

1071 

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

1073 
"{#} = 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

1074 
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

1075 

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

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

1078 
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

1079 

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

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

1081 
"Multiset.filter P (Bag xs) = Bag (filter (P \<circ> fst) xs)" 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

1082 
by (rule multiset_eqI) (simp add: 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

1083 

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

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

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

1087 
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

1088 
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

1089 
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

1090 
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

1091 
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

1092 
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

1093 
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

1094 
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

1095 
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

1096 
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

1097 
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

1098 
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

1099 
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

1100 
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

1101 

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

1102 
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

1103 
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

1104 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
definition 
45866
e62b319c7696
adding code attribute to enable evaluation of equality on multisets
bulwahn
parents:
45694
diff
changeset

1106 
[code]: "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

1107 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
instance proof 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

1109 
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

1110 

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

1112 

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

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

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

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

1116 

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

1117 
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

1118 
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

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

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

1121 

37751  1122 
notation fcomp (infixl "\<circ>>" 60) 
1123 
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

1124 

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

1125 
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

1126 
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

1127 

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

1128 
definition 
37751  1129 
"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

1130 

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

1131 
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

1132 

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

1133 
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

1134 

37751  1135 
no_notation fcomp (infixl "\<circ>>" 60) 
1136 
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

1137 

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

1138 
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

1139 

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

1140 

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

1141 
subsection {* The multiset order *} 
10249  1142 

1143 
subsubsection {* Wellfoundedness *} 

1144 

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

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

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

1149 
definition mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where 
37765  1150 
"mult r = (mult1 r)\<^sup>+" 
10249  1151 

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

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

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

19582  1158 
(is "_ \<Longrightarrow> ?case1 (mult1 r) \<or> ?case2") 
10249  1159 
proof (unfold mult1_def) 
23751  1160 
let ?r = "\<lambda>K a. \<forall>b. b :# K > (b, a) \<in> r" 
11464  1161 
let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a" 
23751  1162 
let ?case1 = "?case1 {(N, M). ?R N M}" 
10249  1163 

23751  1164 
assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}" 
18258 