author  haftmann 
Sat, 22 May 2010 10:12:49 +0200  
changeset 37074  322d065ebef7 
parent 36903  489c1fbbb028 
child 37107  1535aa1c943a 
permissions  rwrr 
10249  1 
(* Title: HOL/Library/Multiset.thy 
15072  2 
Author: Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker 
10249  3 
*) 
4 

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

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

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

8 
imports Main 
15131  9 
begin 
10249  10 

11 
subsection {* The type of multisets *} 

12 

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

13 
typedef 'a multiset = "{f :: 'a => nat. finite {x. f x > 0}}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

19 
lemmas multiset_typedef = Abs_multiset_inverse count_inverse count 
19086  20 

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

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

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

10249  26 

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

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

29 
by (simp only: count_inject [symmetric] expand_fun_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

30 

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

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

34 

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

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

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

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

38 

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

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

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

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

42 

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

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

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

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

46 

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

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

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

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

50 

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

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

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

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

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

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

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

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

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

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

60 

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

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

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

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

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

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

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

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

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

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

70 

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

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

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

73 

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

74 

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

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

76 

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

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

78 

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

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

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

81 

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

87 

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

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

89 

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

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

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

92 

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

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

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

95 

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

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

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

98 

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

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

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

101 

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

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

103 

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

104 
end 
10249  105 

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

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

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

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

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

114 

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

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

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

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

118 
lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

10249  121 

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

122 
subsection {* Basic operations *} 
10249  123 

124 
subsubsection {* Union *} 

125 

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

126 
lemma count_union [simp]: "count (M + N) a = count M a + count N a" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

129 
instance multiset :: (type) cancel_comm_monoid_add proof 
36903  130 
qed (simp_all add: multiset_ext_iff) 
10277  131 

10249  132 

133 
subsubsection {* Difference *} 

134 

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

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

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

137 

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

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

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

140 

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

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

142 

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

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

144 

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

145 
lemma count_diff [simp]: "count (M  N) a = count M a  count N a" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

147 

17161  148 
lemma diff_empty [simp]: "M  {#} = M \<and> {#}  M = {#}" 
36903  149 
by(simp add: multiset_ext_iff) 
150 

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

152 
by (rule multiset_ext) simp 

10249  153 

36903  154 
lemma diff_union_cancelR [simp]: "M + N  N = (M::'a multiset)" 
155 
by(simp add: multiset_ext_iff) 

10249  156 

36903  157 
lemma diff_union_cancelL [simp]: "N + M  N = (M::'a multiset)" 
158 
by(simp add: multiset_ext_iff) 

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

159 

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

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

161 
"x \<in># M \<Longrightarrow> {#x#} + (M  {#x#}) = M" 
36903  162 
by (clarsimp simp: multiset_ext_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

163 

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

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

165 
"x \<in># M \<Longrightarrow> M  {#x#} + {#x#} = M" 
36903  166 
by (clarsimp simp: multiset_ext_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

167 

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

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

169 
"(M::'a multiset)  N  Q = M  Q  N" 
36903  170 
by (auto simp add: multiset_ext_iff) 
171 

172 
lemma diff_add: 

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

174 
by (simp add: multiset_ext_iff) 

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

175 

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

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

177 
"a \<noteq> b \<Longrightarrow> M  {#a#} + {#b#} = M + {#b#}  {#a#}" 
36903  178 
by (auto simp add: multiset_ext_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

179 

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

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

181 
"a \<in># J \<Longrightarrow> I + J  {#a#} = I + (J  {#a#})" 
36903  182 
by (simp add: multiset_ext_iff) 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

183 

10249  184 

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

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

186 

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

187 
lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}" 
36903  188 
by (simp add: multiset_ext_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

189 

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

190 
lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b" 
36903  191 
by (auto simp add: multiset_ext_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

192 

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

193 
lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}" 
36903  194 
by (auto simp add: multiset_ext_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

195 

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

196 
lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}" 
36903  197 
by (auto simp add: multiset_ext_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

198 

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

199 
lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False" 
36903  200 
by (auto simp add: multiset_ext_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

201 

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

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

203 
"\<not> x \<in># M \<Longrightarrow> M  {#x#} = M" 
36903  204 
by (auto simp add: multiset_ext_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

205 

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

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

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

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

209 

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

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

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

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

213 

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

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

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

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

217 

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

218 
lemma union_is_single: 
36903  219 
"M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")proof 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

221 
next 
36903  222 
assume ?lhs thus ?rhs 
223 
by(simp add: multiset_ext_iff split:if_splits) (metis add_is_1) 

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

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

225 

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

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

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

228 
by (auto simp add: eq_commute [of "{#a#}" "M + N"] union_is_single) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

229 

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

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

231 
"M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N  {#a#} + {#b#} \<and> N = M  {#b#} + {#a#}" (is "?lhs = ?rhs") 
36903  232 
(* shorter: by (simp add: multiset_ext_iff) fastsimp *) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

235 
by (auto simp add: add_assoc add_commute [of "{#b#}"]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

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

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

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

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

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

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

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

245 
with False have "a \<in># N" by auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

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

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

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

251 

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

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

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

254 
and bnotc: "b \<noteq> c" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

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

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

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

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

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

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

262 

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

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

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

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

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

267 

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

268 

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

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

270 

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

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

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

273 

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

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

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

276 

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

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

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

279 

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

280 
instance proof 
36903  281 
qed (auto simp add: mset_le_def mset_less_def multiset_ext_iff intro: order_trans antisym) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

282 

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

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

284 

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

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

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

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

288 

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

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

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

291 
apply (unfold mset_le_def, rule iffI, rule_tac x = "B  A" in exI) 
36903  292 
apply (auto intro: multiset_ext_iff [THEN iffD2]) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

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

294 

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

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

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

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

298 

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

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

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

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

302 

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

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

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

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

306 

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

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

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

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

310 

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

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

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

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

314 

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

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

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

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

318 

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

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

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

322 

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

323 
lemma mset_le_multiset_union_diff_commute: 
36867  324 
"B \<le> A \<Longrightarrow> (A::'a multiset)  B + C = A + C  B" 
36903  325 
by (simp add: multiset_ext_iff mset_le_def) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

326 

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

327 
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

328 
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

329 
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

330 
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

331 
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

332 

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

333 
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

334 
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

335 
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

336 
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

337 
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

338 

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

339 
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

340 
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

341 
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

342 
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

343 
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

344 
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

345 
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

346 
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

347 

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

348 
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

349 
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

350 
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

351 
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

352 
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

353 

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

354 
lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False" 
36903  355 
by (auto simp add: mset_less_def mset_le_def multiset_ext_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

356 

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

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

358 
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

359 

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

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

361 
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

362 

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

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

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

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

366 

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

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

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

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

370 

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

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

372 
"c \<in># B \<Longrightarrow> B  {#c#} < B" 
36903  373 
by (auto simp: mset_le_def mset_less_def multiset_ext_iff) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

374 

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

375 

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

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

377 

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

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

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

380 

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

381 
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

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

383 

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

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

385 
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

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

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

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

389 

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

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

391 

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

392 
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

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

394 

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

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

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

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

398 

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

399 
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}" 
36903  400 
by (rule multiset_ext) (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

401 

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

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

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

404 
shows "A + B  C = A  C + B" 
36903  405 
proof (rule multiset_ext) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

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

407 
from assms have "min (count B x) (count C x) = 0" 
36903  408 
by (auto simp add: multiset_inter_count multiset_ext_iff) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

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

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

411 
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

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

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

414 

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

415 

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

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

417 

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

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

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

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

421 

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

422 
lemma MCollect_empty [simp]: "MCollect {#} P = {#}" 
36903  423 
by (rule multiset_ext) simp 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

424 

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

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

426 
"MCollect {#x#} P = (if P x then {#x#} else {#})" 
36903  427 
by (rule multiset_ext) simp 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

428 

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

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

430 
"MCollect (M + N) f = MCollect M f + MCollect N f" 
36903  431 
by (rule multiset_ext) simp 
10249  432 

433 

434 
subsubsection {* Set of elements *} 

435 

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

436 
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

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

438 

17161  439 
lemma set_of_empty [simp]: "set_of {#} = {}" 
26178  440 
by (simp add: set_of_def) 
10249  441 

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

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

17161  448 
lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" 
36903  449 
by (auto simp add: set_of_def multiset_ext_iff) 
10249  450 

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

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

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

457 
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

458 
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

459 

10249  460 

461 
subsubsection {* Size *} 

462 

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

463 
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

464 
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

465 

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

466 
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

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

468 

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

469 
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

470 

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

471 
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

472 

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

473 
lemma size_empty [simp]: "size {#} = 0" 
26178  474 
by (simp add: size_def) 
10249  475 

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

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

17161  479 
lemma setsum_count_Int: 
26178  480 
"finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A" 
481 
apply (induct rule: finite_induct) 

482 
apply simp 

483 
apply (simp add: Int_insert_left set_of_def) 

484 
done 

10249  485 

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

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

489 
prefer 2 

490 
apply (rule ext, simp) 

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

492 
apply (subst Int_commute) 

493 
apply (simp (no_asm_simp) add: setsum_count_Int) 

494 
done 

10249  495 

17161  496 
lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})" 
36903  497 
by (auto simp add: size_def multiset_ext_iff) 
26016  498 

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

26178  500 
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty) 
10249  501 

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

505 
apply auto 

506 
done 

10249  507 

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

508 
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

509 
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

510 
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

511 
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

512 
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

513 
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

514 
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

515 
then show ?thesis by blast 
23611  516 
qed 
15869  517 

26016  518 

519 
subsection {* Induction and case splits *} 

10249  520 

521 
lemma setsum_decr: 

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

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

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

527 
done 

10249  528 

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

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

533 
apply (unfold multiset_def) 

534 
apply (induct_tac n, simp, clarify) 

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

536 
apply simp 

537 
apply (rule 1) 

538 
apply (rule ext, force, clarify) 

539 
apply (frule setsum_SucD, clarify) 

540 
apply (rename_tac a) 

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

542 
prefer 2 

543 
apply (rule finite_subset) 

544 
prefer 2 

545 
apply assumption 

546 
apply simp 

547 
apply blast 

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

549 
prefer 2 

550 
apply (rule ext) 

551 
apply (simp (no_asm_simp)) 

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

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

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

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

556 
prefer 2 

557 
apply blast 

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

559 
prefer 2 

560 
apply blast 

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

562 
done 

10249  563 

10313  564 
theorem rep_multiset_induct: 
11464  565 
"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

566 
(!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" 
26178  567 
using rep_multiset_induct_aux by blast 
10249  568 

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

572 
shows "P M" 

10249  573 
proof  
574 
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

575 
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

576 
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

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

579 
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

580 
apply (rule count [THEN rep_multiset_induct]) 
18258  581 
apply (rule empty [unfolded defns]) 
15072  582 
apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))") 
10249  583 
prefer 2 
584 
apply (simp add: expand_fun_eq) 

585 
apply (erule ssubst) 

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

587 
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

588 
apply (simp add: aux) 
10249  589 
done 
590 
qed 

591 

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

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

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

598 
shows "P" 

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

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

604 
by (blast dest: multi_nonempty_split) 

26145  605 
then show ?thesis using add by simp 
25610  606 
qed 
607 

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

26178  609 
apply (cases M) 
610 
apply simp 

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

612 
done 

25610  613 

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

614 
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

615 
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

616 

26033  617 
lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}" 
36903  618 
apply (subst multiset_ext_iff) 
26178  619 
apply auto 
620 
done 

10249  621 

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

622 
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

623 
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

624 
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

625 
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

626 
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

627 
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

628 
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

629 
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

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

631 
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

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

633 
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

634 
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

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

636 
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

637 
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

638 
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

639 
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

640 
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

641 

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

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

644 

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

645 
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

646 

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

648 

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

649 
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

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

651 
"mset_less_rel = {(A,B). A < B}" 
10249  652 

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

654 
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

655 
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

656 
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

657 
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

658 
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

659 
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

660 
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

661 
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

662 
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

663 
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

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

666 
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

667 
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

668 
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

669 
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

670 

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

672 

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

674 
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

675 
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

676 
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

677 
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

678 
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

679 

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

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

681 
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

682 
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

683 
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

684 
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

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

686 
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

687 
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

688 
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

689 
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

690 
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

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

692 
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

693 
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

694 
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

695 
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

696 
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

697 
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

698 
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

699 
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

700 
qed 
26145  701 

17161  702 

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

704 

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

706 

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

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

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

710 

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

712 
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

713 

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

714 
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

715 
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

716 

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

718 
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

719 

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

720 
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

721 
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

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

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

725 
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

726 

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

728 
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

729 
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

730 
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

731 
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

732 
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

733 
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

734 
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

735 

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

736 
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

737 
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

738 

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

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

741 
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

742 
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

743 
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

744 
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

745 
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

746 
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

747 

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

749 
"multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys" 
36903  750 
by (rule) (auto simp add:multiset_ext_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

751 

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

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

754 
(set x = set y) = (multiset_of x = multiset_of y)" 
36903  755 
by (auto simp: multiset_ext_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

756 

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

757 
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

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

759 
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

760 
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

761 
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

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

763 
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

764 
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

765 

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

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

768 
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

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

771 
"count (multiset_of xs) x = length [y \<leftarrow> xs. y = 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

772 
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

773 

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

775 
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

776 
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

777 
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

778 
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

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

780 

36903  781 
lemma multiset_of_remove1[simp]: 
782 
"multiset_of (remove1 a xs) = multiset_of xs  {#a#}" 

783 
by (induct xs) (auto simp add: multiset_ext_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

784 

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

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

787 
shows "length xs = length 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

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

789 
proof (induct arbitrary: ys rule: length_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

790 
case (1 xs 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

791 
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

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

793 
case Nil with "1.prems" 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

794 
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

795 
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

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

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

799 
case Nil 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
with "1.prems" Cons 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

801 
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

802 
case (Cons y 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

803 
have x_in_ys: "x = y \<or> x \<in> set 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

804 
proof (cases "x = 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

805 
case True then 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

806 
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

807 
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

808 
from "1.prems" [symmetric] xCons Cons have "x :# multiset_of ys' + {#y#}" 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

809 
with False show ?thesis by (simp add: mem_set_multiset_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

810 
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

811 
from "1.hyps" have IH: "length xs' < length xs \<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

812 
(\<forall>x. multiset_of xs' = multiset_of x \<longrightarrow> length xs' = length x)" by blast 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
from "1.prems" x_in_ys Cons xCons have "multiset_of xs' = multiset_of (remove1 x (y#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

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

815 
apply (simp add: multiset_of_remove1, simp only: 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

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

817 
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

818 
with IH xCons have IH': "length xs' = length (remove1 x (y#ys'))" by fastsimp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
from x_in_ys have "x \<noteq> y \<Longrightarrow> length ys' > 0" 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

820 
with Cons xCons x_in_ys IH' show ?thesis by (auto simp add: length_remove1) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

821 
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

822 
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

823 
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

824 

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

825 
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

826 
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

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

828 
*} 
37074  829 

830 
lemma (in linorder) properties_for_sort: 

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

831 
"multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = 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

832 
proof (induct xs arbitrary: 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

833 
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

834 
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

835 
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

836 
then have "x \<in> set 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

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

838 
with Cons.prems Cons.hyps [of "remove1 x ys"] 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

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

840 
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

841 

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

842 
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

843 
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

844 

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

845 
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

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

847 
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

848 
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

849 
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

850 
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

851 
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

852 
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

853 
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

854 
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

855 
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

856 
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

857 
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

858 
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

859 
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

860 
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

861 
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

862 
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

863 
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

864 
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

865 
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

866 
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

867 

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

868 
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

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

870 
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

871 
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

872 

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

873 

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

874 
subsubsection {* 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

875 

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

876 
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

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

878 

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

879 
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

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

881 
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

882 
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

883 
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

884 
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

885 
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

886 
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

887 
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

888 
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

889 
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

890 
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

891 
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

892 
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

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

894 
by (simp add: count_of_def expand_fun_eq 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

895 
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

896 

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

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

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

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

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

901 

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

902 
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

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

904 
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

905 

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

906 
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

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

908 
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

909 

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

910 
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

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

912 

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

913 
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

914 

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

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

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

917 
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

918 

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

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

920 
"{#} = Bag []" 
36903  921 
by (simp add: multiset_ext_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

922 

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

923 
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

924 
"{#x#} = Bag [(x, 1)]" 
36903  925 
by (simp add: multiset_ext_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

926 

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

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

928 
"MCollect (Bag xs) P = Bag (filter (P \<circ> fst) xs)" 
36903  929 
by (simp add: multiset_ext_iff count_of_filter) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

930 

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

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

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

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

934 
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

935 
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

936 
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

937 
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

938 
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

939 
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

940 
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

941 
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

942 
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

943 
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

944 
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

945 
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

946 
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

947 
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

948 

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

949 
instantiation multiset :: (eq) 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

950 
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

951 

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

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

953 
"HOL.eq 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

954 

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

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

956 
qed (simp add: eq_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

957 

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

958 
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

959 

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

960 
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

961 
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

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

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

964 

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

965 
notation fcomp (infixl "o>" 60) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

966 
notation scomp (infixl "o\<rightarrow>" 60) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

967 

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

968 
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

969 
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

970 

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

971 
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

972 
"Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (bagify 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

973 

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

974 
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

975 

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

976 
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

977 

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

978 
no_notation fcomp (infixl "o>" 60) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

979 
no_notation scomp (infixl "o\<rightarrow>" 60) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

980 

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

981 
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

982 

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

983 

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

984 
subsection {* The multiset order *} 
10249  985 

986 
subsubsection {* Wellfoundedness *} 

987 

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

988 
definition mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

989 
[code del]: "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> 
23751  990 
(\<forall>b. b :# K > (b, a) \<in> r)}" 
10249  991 

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

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

993 
[code del]: "mult r = (mult1 r)\<^sup>+" 
10249  994 

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

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

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

19582  1001 
(is "_ \<Longrightarrow> ?case1 (mult1 r) \<or> ?case2") 
10249  1002 
proof (unfold mult1_def) 
23751  1003 
let ?r = "\<lambda>K a. \<forall>b. b :# K > (b, a) \<in> r" 
11464  1004 
let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a" 
23751  1005 
let ?case1 = "?case1 {(N, M). ?R N M}" 
10249  1006 

23751  1007 
assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}" 
18258  1008 
then have "\<exists>a' M0' K. 
11464  1009 
M0 + {#a#} = M0' + {#a'#} \<and> N = M0' + K \<and> ?r K a'" by simp 
18258  1010 
then show "?case1 \<or> ?case2" 
10249  1011 
proof (elim exE conjE) 
1012 
fix a' M0' K 

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

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

18258  1015 
then have "M0 = M0' \<and> a = a' \<or> 
11464  1016 
(\<exists>K'. M0 = K' + {#a'#} \<and> M0' = K' + {#a#})" 
10249  1017 
by (simp only: add_eq_conv_ex) 
18258  1018 
then show ?thesis 
10249  1019 
proof (elim disjE conjE exE) 
1020 
assume "M0 = M0'" "a = a'" 

11464  1021 
with N r have "?r K a \<and> N = M0 + K" by simp 
18258  1022 
then have ?case2 .. then show ?thesis .. 
10249  1023 
next 
1024 
fix K' 

1025 
assume "M0' = K' + {#a#}" 

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

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

1028 
assume "M0 = K' + {#a'#}" 

1029 
with r have "?R (K' + K) M0" by blast 

18258  1030 
with n have ?case1 by simp then show ?thesis .. 
10249  1031 
qed 
1032 
qed 

1033 
qed 

1034 

23751  1035 
lemma all_accessible: "wf r ==> \<forall>M. M \<in> acc (mult1 r)" 
10249  1036 
proof 
1037 
let ?R = "mult1 r" 

1038 
let ?W = "acc ?R" 

1039 
{ 

1040 
fix M M0 a 

23751  1041 
assume M0: "M0 \<in> ?W" 
1042 
and wf_hyp: "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)" 

1043 
and acc_hyp: "\<forall>M. (M, M0) \<in> ?R > M + {#a#} \<in> ?W" 

1044 
have "M0 + {#a#} \<in> ?W" 

1045 
proof (rule accI [of "M0 + {#a#}"]) 

10249  1046 
fix N 
23751  1047 
assume "(N, M0 + {#a#}) \<in> ?R" 
1048 
then have "((\<exists>M. (M, M0) \<in> ?R \<and> N = M + {#a#}) \<or> 

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

10249  1050 
by (rule less_add) 
23751  1051 
then show "N \<in> ?W" 
10249  1052 
proof (elim exE disjE conjE) 
23751  1053 
fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}" 
1054 
from acc_hyp have "(M, M0) \<in> ?R > M + {#a#} \<in> ?W" .. 

1055 
from this and `(M, M0) \<in> ?R` have "M + {#a#} \<in> ?W" .. 

1056 
then show "N \<in> ?W" by (simp only: N) 

10249  1057 
next 
1058 
fix K 

1059 
assume N: "N = M0 + K" 

23751  1060 
assume "\<forall>b. b :# K > (b, a) \<in> r" 
1061 
then have "M0 + K \<in> ?W" 

10249  1062 
proof (induct K) 
18730  1063 
case empty 
23751  1064 
from M0 show "M0 + {#} \<in> ?W" by simp 
18730  1065 
next 
1066 
case (add K x) 

23751  1067 
from add.prems have "(x, a) \<in> r" by simp 
1068 
with wf_hyp have "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast 

1069 
moreover from add have "M0 + K \<in> ?W" by simp 

1070 
ultimately have "(M0 + K) + {#x#} \<in> ?W" .. 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
then show "M0 + (K + {#x#}) \<in> ?W" by (simp only: add_assoc) 
10249  1072 
qed 
23751  1073 
then show "N \<in> ?W" by (simp only: N) 
10249  1074 
qed 
1075 
qed 

1076 
} note tedious_reasoning = this 

1077 

23751  1078 
assume wf: "wf r" 
10249  1079 
fix M 
23751  1080 
show "M \<in> ?W" 
10249  1081 
proof (induct M) 
23751  1082 
show "{#} \<in> ?W" 
10249  1083 
proof (rule accI) 
23751  1084 
fix b assume "(b, {#}) \<in> ?R" 
1085 
with not_less_empty show "b \<in> ?W" by contradiction 

10249  1086 
qed 
1087 

23751  1088 
fix M a assume "M \<in> ?W" 
1089 
from wf have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W" 

10249  1090 
proof induct 
1091 
fix a 

23751  1092 
assume r: "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)" 
1093 
show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W" 

10249  1094 
proof 
23751  1095 
fix M assume "M \<in> ?W" 
1096 
then show "M + {#a#} \<in> ?W" 

23373  1097 
by (rule acc_induct) (rule tedious_reasoning [OF _ r]) 
10249  1098 
qed 
1099 
qed 

23751  1100 
from this and `M \<in> ?W` show "M + {#a#} \<in> ?W" .. 
10249  1101 
qed 
1102 
qed 

1103 

23751  1104 
theorem wf_mult1: "wf r ==> wf (mult1 r)" 
26178  1105 
by (rule acc_wfI) (rule all_accessible) 
10249  1106 

23751  1107 
theorem wf_mult: "wf r ==> wf (mult r)" 
26178  1108 
unfolding mult_def by (rule wf_trancl) (rule wf_mult1) 
10249  1109 

1110 

1111 
subsubsection {* Closurefree presentation *} 

1112 

1113 
text {* One direction. *} 

1114 

1115 
lemma mult_implies_one_step: 

23751  1116 
"trans r ==> (M, N) \<in> mult r ==> 
11464  1117 
\<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> 
23751  1118 
(\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)" 
26178  1119 
apply (unfold mult_def mult1_def set_of_def) 
1120 
apply (erule converse_trancl_induct, clarify) 

1121 
apply (rule_tac x = M0 in exI, simp, clarify) 

1122 
apply (case_tac "a :# K") 

1123 
apply (rule_tac x = I in exI) 

1124 
apply (simp (no_asm)) 

1125 
apply (rule_tac x = "(K  {#a#}) + Ka" in exI) 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
apply (simp (no_asm_simp) add: add_assoc [symmetric]) 
26178  1127 
apply (drule_tac f = "\<lambda>M. M  {#a#}" in arg_cong) 
1128 
apply (simp add: diff_union_single_conv) 

1129 
apply (simp (no_asm_use) add: trans_def) 

1130 
apply blast 

1131 
apply (subgoal_tac "a :# I") 

1132 
apply (rule_tac x = "I  {#a#}" in exI) 

1133 
apply (rule_tac x = "J + {#a#}" in exI) 

1134 
apply (rule_tac x = "K + Ka" in exI) 

1135 
apply (rule conjI) 

36903  1136 
apply (simp add: multiset_ext_iff split: nat_diff_split) 
26178  1137 
apply (rule conjI) 
1138 
apply (drule_tac f = "\<lambda>M. M  {#a#}" in arg_cong, simp) 

36903  1139 
apply (simp add: multiset_ext_iff split: nat_diff_split) 
26178  1140 
apply (simp (no_asm_use) add: trans_def) 
1141 
apply blast 

1142 
apply (subgoal_tac "a :# (M0 + {#a#})") 

1143 
apply simp 

1144 
apply (simp (no_asm)) 

1145 
done 

10249  1146 

1147 
lemma one_step_implies_mult_aux: 

23751  1148 
"trans r ==> 
1149 
\<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)) 

1150 
> (I + K, I + J) \<in> mult r" 

26178  1151 
apply (induct_tac n, auto) 
1152 
apply (frule size_eq_Suc_imp_eq_union, clarify) 

1153 
apply (rename_tac "J'", simp) 

1154 
apply (erule notE, auto) 

1155 
apply (case_tac "J' = {#}") 

1156 
apply (simp add: mult_def) 

1157 
apply (rule r_into_trancl) 

1158 
apply (simp add: mult1_def set_of_def, blast) 

1159 
txt {* Now we know @{term "J' \<noteq> {#}"}. *} 

1160 
apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition) 

1161 
apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp) 

1162 
apply (erule ssubst) 

1163 
apply (simp add: Ball_def, auto) 

1164 
apply (subgoal_tac 

1165 
"((I + {# x :# K. (x, a) \<in> r #}) + {# x :# K. (x, a) \<notin> r #}, 

1166 
(I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r") 

1167 
prefer 2 

1168 
apply force 

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

1169 
apply (simp (no_asm_use) add: add_assoc [symmetric] mult_def) 
26178  1170 
apply (erule trancl_trans) 
1171 
apply (rule r_into_trancl) 

1172 
apply (simp add: mult1_def set_of_def) 

1173 
apply (rule_tac x = a in exI) 
