wenzelm@10249: (* Title: HOL/Library/Multiset.thy paulson@15072: Author: Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker blanchet@55129: Author: Andrei Popescu, TU Muenchen wenzelm@10249: *) wenzelm@10249: haftmann@34943: header {* (Finite) multisets *} wenzelm@10249: nipkow@15131: theory Multiset haftmann@51599: imports Main nipkow@15131: begin wenzelm@10249: wenzelm@10249: subsection {* The type of multisets *} wenzelm@10249: wenzelm@45694: definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}" wenzelm@45694: wenzelm@49834: typedef 'a multiset = "multiset :: ('a => nat) set" haftmann@34943: morphisms count Abs_multiset wenzelm@45694: unfolding multiset_def wenzelm@10249: proof wenzelm@45694: show "(\x. 0::nat) \ {f. finite {x. f x > 0}}" by simp wenzelm@10249: qed wenzelm@10249: bulwahn@47429: setup_lifting type_definition_multiset wenzelm@19086: haftmann@28708: abbreviation Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where kleing@25610: "a :# M == 0 < count M a" kleing@25610: wenzelm@26145: notation (xsymbols) wenzelm@26145: Melem (infix "\#" 50) wenzelm@10249: nipkow@39302: lemma multiset_eq_iff: haftmann@34943: "M = N \ (\a. count M a = count N a)" nipkow@39302: by (simp only: count_inject [symmetric] fun_eq_iff) haftmann@34943: nipkow@39302: lemma multiset_eqI: haftmann@34943: "(\x. count A x = count B x) \ A = B" nipkow@39302: using multiset_eq_iff by auto haftmann@34943: haftmann@34943: text {* haftmann@34943: \medskip Preservation of the representing set @{term multiset}. haftmann@34943: *} haftmann@34943: haftmann@34943: lemma const0_in_multiset: haftmann@34943: "(\a. 0) \ multiset" haftmann@34943: by (simp add: multiset_def) haftmann@34943: haftmann@34943: lemma only1_in_multiset: haftmann@34943: "(\b. if b = a then n else 0) \ multiset" haftmann@34943: by (simp add: multiset_def) haftmann@34943: haftmann@34943: lemma union_preserves_multiset: haftmann@34943: "M \ multiset \ N \ multiset \ (\a. M a + N a) \ multiset" haftmann@34943: by (simp add: multiset_def) haftmann@34943: haftmann@34943: lemma diff_preserves_multiset: haftmann@34943: assumes "M \ multiset" haftmann@34943: shows "(\a. M a - N a) \ multiset" haftmann@34943: proof - haftmann@34943: have "{x. N x < M x} \ {x. 0 < M x}" haftmann@34943: by auto haftmann@34943: with assms show ?thesis haftmann@34943: by (auto simp add: multiset_def intro: finite_subset) haftmann@34943: qed haftmann@34943: haftmann@41069: lemma filter_preserves_multiset: haftmann@34943: assumes "M \ multiset" haftmann@34943: shows "(\x. if P x then M x else 0) \ multiset" haftmann@34943: proof - haftmann@34943: have "{x. (P x \ 0 < M x) \ P x} \ {x. 0 < M x}" haftmann@34943: by auto haftmann@34943: with assms show ?thesis haftmann@34943: by (auto simp add: multiset_def intro: finite_subset) haftmann@34943: qed haftmann@34943: haftmann@34943: lemmas in_multiset = const0_in_multiset only1_in_multiset haftmann@41069: union_preserves_multiset diff_preserves_multiset filter_preserves_multiset haftmann@34943: haftmann@34943: haftmann@34943: subsection {* Representing multisets *} haftmann@34943: haftmann@34943: text {* Multiset enumeration *} haftmann@34943: huffman@48008: instantiation multiset :: (type) cancel_comm_monoid_add haftmann@25571: begin haftmann@25571: bulwahn@47429: lift_definition zero_multiset :: "'a multiset" is "\a. 0" bulwahn@47429: by (rule const0_in_multiset) haftmann@25571: haftmann@34943: abbreviation Mempty :: "'a multiset" ("{#}") where haftmann@34943: "Mempty \ 0" haftmann@25571: bulwahn@47429: lift_definition plus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\M N. (\a. M a + N a)" bulwahn@47429: by (rule union_preserves_multiset) haftmann@25571: huffman@48008: instance huffman@48008: by default (transfer, simp add: fun_eq_iff)+ haftmann@25571: haftmann@25571: end wenzelm@10249: bulwahn@47429: lift_definition single :: "'a => 'a multiset" is "\a b. if b = a then 1 else 0" bulwahn@47429: by (rule only1_in_multiset) kleing@15869: wenzelm@26145: syntax wenzelm@26176: "_multiset" :: "args => 'a multiset" ("{#(_)#}") nipkow@25507: translations nipkow@25507: "{#x, xs#}" == "{#x#} + {#xs#}" nipkow@25507: "{#x#}" == "CONST single x" nipkow@25507: haftmann@34943: lemma count_empty [simp]: "count {#} a = 0" bulwahn@47429: by (simp add: zero_multiset.rep_eq) wenzelm@10249: haftmann@34943: lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" bulwahn@47429: by (simp add: single.rep_eq) nipkow@29901: wenzelm@10249: haftmann@34943: subsection {* Basic operations *} wenzelm@10249: wenzelm@10249: subsubsection {* Union *} wenzelm@10249: haftmann@34943: lemma count_union [simp]: "count (M + N) a = count M a + count N a" bulwahn@47429: by (simp add: plus_multiset.rep_eq) wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Difference *} wenzelm@10249: haftmann@49388: instantiation multiset :: (type) comm_monoid_diff haftmann@34943: begin haftmann@34943: bulwahn@47429: lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\ M N. \a. M a - N a" bulwahn@47429: by (rule diff_preserves_multiset) bulwahn@47429: haftmann@49388: instance haftmann@49388: by default (transfer, simp add: fun_eq_iff)+ haftmann@34943: haftmann@34943: end haftmann@34943: haftmann@34943: lemma count_diff [simp]: "count (M - N) a = count M a - count N a" bulwahn@47429: by (simp add: minus_multiset.rep_eq) haftmann@34943: wenzelm@17161: lemma diff_empty [simp]: "M - {#} = M \ {#} - M = {#}" haftmann@52289: by rule (fact Groups.diff_zero, fact Groups.zero_diff) nipkow@36903: nipkow@36903: lemma diff_cancel[simp]: "A - A = {#}" haftmann@52289: by (fact Groups.diff_cancel) wenzelm@10249: nipkow@36903: lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)" haftmann@52289: by (fact add_diff_cancel_right') wenzelm@10249: nipkow@36903: lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)" haftmann@52289: by (fact add_diff_cancel_left') haftmann@34943: haftmann@52289: lemma diff_right_commute: haftmann@52289: "(M::'a multiset) - N - Q = M - Q - N" haftmann@52289: by (fact diff_right_commute) haftmann@52289: haftmann@52289: lemma diff_add: haftmann@52289: "(M::'a multiset) - (N + Q) = M - N - Q" haftmann@52289: by (rule sym) (fact diff_diff_add) haftmann@52289: haftmann@34943: lemma insert_DiffM: haftmann@34943: "x \# M \ {#x#} + (M - {#x#}) = M" nipkow@39302: by (clarsimp simp: multiset_eq_iff) haftmann@34943: haftmann@34943: lemma insert_DiffM2 [simp]: haftmann@34943: "x \# M \ M - {#x#} + {#x#} = M" nipkow@39302: by (clarsimp simp: multiset_eq_iff) haftmann@34943: haftmann@34943: lemma diff_union_swap: haftmann@34943: "a \ b \ M - {#a#} + {#b#} = M + {#b#} - {#a#}" nipkow@39302: by (auto simp add: multiset_eq_iff) haftmann@34943: haftmann@34943: lemma diff_union_single_conv: haftmann@34943: "a \# J \ I + J - {#a#} = I + (J - {#a#})" nipkow@39302: by (simp add: multiset_eq_iff) bulwahn@26143: wenzelm@10249: haftmann@34943: subsubsection {* Equality of multisets *} haftmann@34943: haftmann@34943: lemma single_not_empty [simp]: "{#a#} \ {#} \ {#} \ {#a#}" nipkow@39302: by (simp add: multiset_eq_iff) haftmann@34943: haftmann@34943: lemma single_eq_single [simp]: "{#a#} = {#b#} \ a = b" nipkow@39302: by (auto simp add: multiset_eq_iff) haftmann@34943: haftmann@34943: lemma union_eq_empty [iff]: "M + N = {#} \ M = {#} \ N = {#}" nipkow@39302: by (auto simp add: multiset_eq_iff) haftmann@34943: haftmann@34943: lemma empty_eq_union [iff]: "{#} = M + N \ M = {#} \ N = {#}" nipkow@39302: by (auto simp add: multiset_eq_iff) haftmann@34943: haftmann@34943: lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \ False" nipkow@39302: by (auto simp add: multiset_eq_iff) haftmann@34943: haftmann@34943: lemma diff_single_trivial: haftmann@34943: "\ x \# M \ M - {#x#} = M" nipkow@39302: by (auto simp add: multiset_eq_iff) haftmann@34943: haftmann@34943: lemma diff_single_eq_union: haftmann@34943: "x \# M \ M - {#x#} = N \ M = N + {#x#}" haftmann@34943: by auto haftmann@34943: haftmann@34943: lemma union_single_eq_diff: haftmann@34943: "M + {#x#} = N \ M = N - {#x#}" haftmann@34943: by (auto dest: sym) haftmann@34943: haftmann@34943: lemma union_single_eq_member: haftmann@34943: "M + {#x#} = N \ x \# N" haftmann@34943: by auto haftmann@34943: haftmann@34943: lemma union_is_single: wenzelm@46730: "M + N = {#a#} \ M = {#a#} \ N={#} \ M = {#} \ N = {#a#}" (is "?lhs = ?rhs") wenzelm@46730: proof haftmann@34943: assume ?rhs then show ?lhs by auto haftmann@34943: next wenzelm@46730: assume ?lhs then show ?rhs wenzelm@46730: by (simp add: multiset_eq_iff split:if_splits) (metis add_is_1) haftmann@34943: qed haftmann@34943: haftmann@34943: lemma single_is_union: haftmann@34943: "{#a#} = M + N \ {#a#} = M \ N = {#} \ M = {#} \ {#a#} = N" haftmann@34943: by (auto simp add: eq_commute [of "{#a#}" "M + N"] union_is_single) haftmann@34943: haftmann@34943: lemma add_eq_conv_diff: haftmann@34943: "M + {#a#} = N + {#b#} \ M = N \ a = b \ M = N - {#a#} + {#b#} \ N = M - {#b#} + {#a#}" (is "?lhs = ?rhs") nipkow@44890: (* shorter: by (simp add: multiset_eq_iff) fastforce *) haftmann@34943: proof haftmann@34943: assume ?rhs then show ?lhs haftmann@57512: by (auto simp add: add.assoc add.commute [of "{#b#}"]) haftmann@57512: (drule sym, simp add: add.assoc [symmetric]) haftmann@34943: next haftmann@34943: assume ?lhs haftmann@34943: show ?rhs haftmann@34943: proof (cases "a = b") haftmann@34943: case True with `?lhs` show ?thesis by simp haftmann@34943: next haftmann@34943: case False haftmann@34943: from `?lhs` have "a \# N + {#b#}" by (rule union_single_eq_member) haftmann@34943: with False have "a \# N" by auto haftmann@34943: moreover from `?lhs` have "M = N + {#b#} - {#a#}" by (rule union_single_eq_diff) haftmann@34943: moreover note False haftmann@34943: ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"] diff_union_swap) haftmann@34943: qed haftmann@34943: qed haftmann@34943: haftmann@34943: lemma insert_noteq_member: haftmann@34943: assumes BC: "B + {#b#} = C + {#c#}" haftmann@34943: and bnotc: "b \ c" haftmann@34943: shows "c \# B" haftmann@34943: proof - haftmann@34943: have "c \# C + {#c#}" by simp haftmann@34943: have nc: "\ c \# {#b#}" using bnotc by simp haftmann@34943: then have "c \# B + {#b#}" using BC by simp haftmann@34943: then show "c \# B" using nc by simp haftmann@34943: qed haftmann@34943: haftmann@34943: lemma add_eq_conv_ex: haftmann@34943: "(M + {#a#} = N + {#b#}) = haftmann@34943: (M = N \ a = b \ (\K. M = K + {#b#} \ N = K + {#a#}))" haftmann@34943: by (auto simp add: add_eq_conv_diff) haftmann@34943: haftmann@51600: lemma multi_member_split: haftmann@51600: "x \# M \ \A. M = A + {#x#}" haftmann@51600: by (rule_tac x = "M - {#x#}" in exI, simp) haftmann@51600: haftmann@34943: haftmann@34943: subsubsection {* Pointwise ordering induced by count *} haftmann@34943: haftmann@35268: instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le haftmann@35268: begin haftmann@35268: kuncar@55565: lift_definition less_eq_multiset :: "'a multiset \ 'a multiset \ bool" is "\ A B. (\a. A a \ B a)" . kuncar@55565: bulwahn@47429: lemmas mset_le_def = less_eq_multiset_def haftmann@34943: haftmann@35268: definition less_multiset :: "'a multiset \ 'a multiset \ bool" where haftmann@35268: mset_less_def: "(A::'a multiset) < B \ A \ B \ A \ B" haftmann@34943: wenzelm@46921: instance wenzelm@46921: by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym) haftmann@35268: haftmann@35268: end haftmann@34943: haftmann@34943: lemma mset_less_eqI: haftmann@35268: "(\x. count A x \ count B x) \ A \ B" haftmann@34943: by (simp add: mset_le_def) haftmann@34943: haftmann@35268: lemma mset_le_exists_conv: haftmann@35268: "(A::'a multiset) \ B \ (\C. B = A + C)" haftmann@34943: apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI) nipkow@39302: apply (auto intro: multiset_eq_iff [THEN iffD2]) haftmann@34943: done haftmann@34943: haftmann@52289: instance multiset :: (type) ordered_cancel_comm_monoid_diff haftmann@52289: by default (simp, fact mset_le_exists_conv) haftmann@52289: haftmann@35268: lemma mset_le_mono_add_right_cancel [simp]: haftmann@35268: "(A::'a multiset) + C \ B + C \ A \ B" haftmann@35268: by (fact add_le_cancel_right) haftmann@34943: haftmann@35268: lemma mset_le_mono_add_left_cancel [simp]: haftmann@35268: "C + (A::'a multiset) \ C + B \ A \ B" haftmann@35268: by (fact add_le_cancel_left) haftmann@35268: haftmann@35268: lemma mset_le_mono_add: haftmann@35268: "(A::'a multiset) \ B \ C \ D \ A + C \ B + D" haftmann@35268: by (fact add_mono) haftmann@34943: haftmann@35268: lemma mset_le_add_left [simp]: haftmann@35268: "(A::'a multiset) \ A + B" haftmann@35268: unfolding mset_le_def by auto haftmann@35268: haftmann@35268: lemma mset_le_add_right [simp]: haftmann@35268: "B \ (A::'a multiset) + B" haftmann@35268: unfolding mset_le_def by auto haftmann@34943: haftmann@35268: lemma mset_le_single: haftmann@35268: "a :# B \ {#a#} \ B" haftmann@35268: by (simp add: mset_le_def) haftmann@34943: haftmann@35268: lemma multiset_diff_union_assoc: haftmann@35268: "C \ B \ (A::'a multiset) + B - C = A + (B - C)" nipkow@39302: by (simp add: multiset_eq_iff mset_le_def) haftmann@34943: haftmann@34943: lemma mset_le_multiset_union_diff_commute: nipkow@36867: "B \ A \ (A::'a multiset) - B + C = A + C - B" nipkow@39302: by (simp add: multiset_eq_iff mset_le_def) haftmann@34943: nipkow@39301: lemma diff_le_self[simp]: "(M::'a multiset) - N \ M" nipkow@39301: by(simp add: mset_le_def) nipkow@39301: haftmann@35268: lemma mset_lessD: "A < B \ x \# A \ x \# B" haftmann@34943: apply (clarsimp simp: mset_le_def mset_less_def) haftmann@34943: apply (erule_tac x=x in allE) haftmann@34943: apply auto haftmann@34943: done haftmann@34943: haftmann@35268: lemma mset_leD: "A \ B \ x \# A \ x \# B" haftmann@34943: apply (clarsimp simp: mset_le_def mset_less_def) haftmann@34943: apply (erule_tac x = x in allE) haftmann@34943: apply auto haftmann@34943: done haftmann@34943: haftmann@35268: lemma mset_less_insertD: "(A + {#x#} < B) \ (x \# B \ A < B)" haftmann@34943: apply (rule conjI) haftmann@34943: apply (simp add: mset_lessD) haftmann@34943: apply (clarsimp simp: mset_le_def mset_less_def) haftmann@34943: apply safe haftmann@34943: apply (erule_tac x = a in allE) haftmann@34943: apply (auto split: split_if_asm) haftmann@34943: done haftmann@34943: haftmann@35268: lemma mset_le_insertD: "(A + {#x#} \ B) \ (x \# B \ A \ B)" haftmann@34943: apply (rule conjI) haftmann@34943: apply (simp add: mset_leD) haftmann@34943: apply (force simp: mset_le_def mset_less_def split: split_if_asm) haftmann@34943: done haftmann@34943: haftmann@35268: lemma mset_less_of_empty[simp]: "A < {#} \ False" nipkow@39302: by (auto simp add: mset_less_def mset_le_def multiset_eq_iff) haftmann@34943: nipkow@55808: lemma empty_le[simp]: "{#} \ A" nipkow@55808: unfolding mset_le_exists_conv by auto nipkow@55808: nipkow@55808: lemma le_empty[simp]: "(M \ {#}) = (M = {#})" nipkow@55808: unfolding mset_le_exists_conv by auto nipkow@55808: haftmann@35268: lemma multi_psub_of_add_self[simp]: "A < A + {#x#}" haftmann@35268: by (auto simp: mset_le_def mset_less_def) haftmann@34943: haftmann@35268: lemma multi_psub_self[simp]: "(A::'a multiset) < A = False" haftmann@35268: by simp haftmann@34943: haftmann@34943: lemma mset_less_add_bothsides: haftmann@35268: "T + {#x#} < S + {#x#} \ T < S" haftmann@35268: by (fact add_less_imp_less_right) haftmann@35268: haftmann@35268: lemma mset_less_empty_nonempty: haftmann@35268: "{#} < S \ S \ {#}" haftmann@35268: by (auto simp: mset_le_def mset_less_def) haftmann@35268: haftmann@35268: lemma mset_less_diff_self: haftmann@35268: "c \# B \ B - {#c#} < B" nipkow@39302: by (auto simp: mset_le_def mset_less_def multiset_eq_iff) haftmann@35268: haftmann@35268: haftmann@35268: subsubsection {* Intersection *} haftmann@35268: haftmann@35268: instantiation multiset :: (type) semilattice_inf haftmann@35268: begin haftmann@35268: haftmann@35268: definition inf_multiset :: "'a multiset \ 'a multiset \ 'a multiset" where haftmann@35268: multiset_inter_def: "inf_multiset A B = A - (A - B)" haftmann@35268: wenzelm@46921: instance wenzelm@46921: proof - haftmann@35268: have aux: "\m n q :: nat. m \ n \ m \ q \ m \ n - (n - q)" by arith wenzelm@46921: show "OFCLASS('a multiset, semilattice_inf_class)" wenzelm@46921: by default (auto simp add: multiset_inter_def mset_le_def aux) haftmann@35268: qed haftmann@35268: haftmann@35268: end haftmann@35268: haftmann@35268: abbreviation multiset_inter :: "'a multiset \ 'a multiset \ 'a multiset" (infixl "#\" 70) where haftmann@35268: "multiset_inter \ inf" haftmann@34943: haftmann@41069: lemma multiset_inter_count [simp]: haftmann@35268: "count (A #\ B) x = min (count A x) (count B x)" bulwahn@47429: by (simp add: multiset_inter_def) haftmann@35268: haftmann@35268: lemma multiset_inter_single: "a \ b \ {#a#} #\ {#b#} = {#}" wenzelm@46730: by (rule multiset_eqI) auto haftmann@34943: haftmann@35268: lemma multiset_union_diff_commute: haftmann@35268: assumes "B #\ C = {#}" haftmann@35268: shows "A + B - C = A - C + B" nipkow@39302: proof (rule multiset_eqI) haftmann@35268: fix x haftmann@35268: from assms have "min (count B x) (count C x) = 0" wenzelm@46730: by (auto simp add: multiset_eq_iff) haftmann@35268: then have "count B x = 0 \ count C x = 0" haftmann@35268: by auto haftmann@35268: then show "count (A + B - C) x = count (A - C + B) x" haftmann@35268: by auto haftmann@35268: qed haftmann@35268: haftmann@51600: lemma empty_inter [simp]: haftmann@51600: "{#} #\ M = {#}" haftmann@51600: by (simp add: multiset_eq_iff) haftmann@51600: haftmann@51600: lemma inter_empty [simp]: haftmann@51600: "M #\ {#} = {#}" haftmann@51600: by (simp add: multiset_eq_iff) haftmann@51600: haftmann@51600: lemma inter_add_left1: haftmann@51600: "\ x \# N \ (M + {#x#}) #\ N = M #\ N" haftmann@51600: by (simp add: multiset_eq_iff) haftmann@51600: haftmann@51600: lemma inter_add_left2: haftmann@51600: "x \# N \ (M + {#x#}) #\ N = (M #\ (N - {#x#})) + {#x#}" haftmann@51600: by (simp add: multiset_eq_iff) haftmann@51600: haftmann@51600: lemma inter_add_right1: haftmann@51600: "\ x \# N \ N #\ (M + {#x#}) = N #\ M" haftmann@51600: by (simp add: multiset_eq_iff) haftmann@51600: haftmann@51600: lemma inter_add_right2: haftmann@51600: "x \# N \ N #\ (M + {#x#}) = ((N - {#x#}) #\ M) + {#x#}" haftmann@51600: by (simp add: multiset_eq_iff) haftmann@51600: haftmann@35268: haftmann@51623: subsubsection {* Bounded union *} haftmann@51623: haftmann@51623: instantiation multiset :: (type) semilattice_sup haftmann@51623: begin haftmann@51623: haftmann@51623: definition sup_multiset :: "'a multiset \ 'a multiset \ 'a multiset" where haftmann@51623: "sup_multiset A B = A + (B - A)" haftmann@51623: haftmann@51623: instance haftmann@51623: proof - haftmann@51623: have aux: "\m n q :: nat. m \ n \ q \ n \ m + (q - m) \ n" by arith haftmann@51623: show "OFCLASS('a multiset, semilattice_sup_class)" haftmann@51623: by default (auto simp add: sup_multiset_def mset_le_def aux) haftmann@51623: qed haftmann@51623: haftmann@51623: end haftmann@51623: haftmann@51623: abbreviation sup_multiset :: "'a multiset \ 'a multiset \ 'a multiset" (infixl "#\" 70) where haftmann@51623: "sup_multiset \ sup" haftmann@51623: haftmann@51623: lemma sup_multiset_count [simp]: haftmann@51623: "count (A #\ B) x = max (count A x) (count B x)" haftmann@51623: by (simp add: sup_multiset_def) haftmann@51623: haftmann@51623: lemma empty_sup [simp]: haftmann@51623: "{#} #\ M = M" haftmann@51623: by (simp add: multiset_eq_iff) haftmann@51623: haftmann@51623: lemma sup_empty [simp]: haftmann@51623: "M #\ {#} = M" haftmann@51623: by (simp add: multiset_eq_iff) haftmann@51623: haftmann@51623: lemma sup_add_left1: haftmann@51623: "\ x \# N \ (M + {#x#}) #\ N = (M #\ N) + {#x#}" haftmann@51623: by (simp add: multiset_eq_iff) haftmann@51623: haftmann@51623: lemma sup_add_left2: haftmann@51623: "x \# N \ (M + {#x#}) #\ N = (M #\ (N - {#x#})) + {#x#}" haftmann@51623: by (simp add: multiset_eq_iff) haftmann@51623: haftmann@51623: lemma sup_add_right1: haftmann@51623: "\ x \# N \ N #\ (M + {#x#}) = (N #\ M) + {#x#}" haftmann@51623: by (simp add: multiset_eq_iff) haftmann@51623: haftmann@51623: lemma sup_add_right2: haftmann@51623: "x \# N \ N #\ (M + {#x#}) = ((N - {#x#}) #\ M) + {#x#}" haftmann@51623: by (simp add: multiset_eq_iff) haftmann@51623: haftmann@51623: haftmann@41069: subsubsection {* Filter (with comprehension syntax) *} haftmann@41069: haftmann@41069: text {* Multiset comprehension *} haftmann@41069: bulwahn@47429: lift_definition filter :: "('a \ bool) \ 'a multiset \ 'a multiset" is "\P M. \x. if P x then M x else 0" bulwahn@47429: by (rule filter_preserves_multiset) haftmann@35268: haftmann@41069: hide_const (open) filter haftmann@35268: haftmann@41069: lemma count_filter [simp]: haftmann@41069: "count (Multiset.filter P M) a = (if P a then count M a else 0)" bulwahn@47429: by (simp add: filter.rep_eq) haftmann@41069: haftmann@41069: lemma filter_empty [simp]: haftmann@41069: "Multiset.filter P {#} = {#}" nipkow@39302: by (rule multiset_eqI) simp haftmann@35268: haftmann@41069: lemma filter_single [simp]: haftmann@41069: "Multiset.filter P {#x#} = (if P x then {#x#} else {#})" haftmann@41069: by (rule multiset_eqI) simp haftmann@41069: haftmann@41069: lemma filter_union [simp]: haftmann@41069: "Multiset.filter P (M + N) = Multiset.filter P M + Multiset.filter P N" nipkow@39302: by (rule multiset_eqI) simp haftmann@35268: haftmann@41069: lemma filter_diff [simp]: haftmann@41069: "Multiset.filter P (M - N) = Multiset.filter P M - Multiset.filter P N" haftmann@41069: by (rule multiset_eqI) simp haftmann@41069: haftmann@41069: lemma filter_inter [simp]: haftmann@41069: "Multiset.filter P (M #\ N) = Multiset.filter P M #\ Multiset.filter P N" nipkow@39302: by (rule multiset_eqI) simp wenzelm@10249: haftmann@41069: syntax haftmann@41069: "_MCollect" :: "pttrn \ 'a multiset \ bool \ 'a multiset" ("(1{# _ :# _./ _#})") haftmann@41069: syntax (xsymbol) haftmann@41069: "_MCollect" :: "pttrn \ 'a multiset \ bool \ 'a multiset" ("(1{# _ \# _./ _#})") haftmann@41069: translations haftmann@41069: "{#x \# M. P#}" == "CONST Multiset.filter (\x. P) M" haftmann@41069: wenzelm@10249: wenzelm@10249: subsubsection {* Set of elements *} wenzelm@10249: haftmann@34943: definition set_of :: "'a multiset => 'a set" where haftmann@34943: "set_of M = {x. x :# M}" haftmann@34943: wenzelm@17161: lemma set_of_empty [simp]: "set_of {#} = {}" nipkow@26178: by (simp add: set_of_def) wenzelm@10249: wenzelm@17161: lemma set_of_single [simp]: "set_of {#b#} = {b}" nipkow@26178: by (simp add: set_of_def) wenzelm@10249: wenzelm@17161: lemma set_of_union [simp]: "set_of (M + N) = set_of M \ set_of N" nipkow@26178: by (auto simp add: set_of_def) wenzelm@10249: wenzelm@17161: lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" nipkow@39302: by (auto simp add: set_of_def multiset_eq_iff) wenzelm@10249: wenzelm@17161: lemma mem_set_of_iff [simp]: "(x \ set_of M) = (x :# M)" nipkow@26178: by (auto simp add: set_of_def) nipkow@26016: haftmann@41069: lemma set_of_filter [simp]: "set_of {# x:#M. P x #} = set_of M \ {x. P x}" nipkow@26178: by (auto simp add: set_of_def) wenzelm@10249: haftmann@34943: lemma finite_set_of [iff]: "finite (set_of M)" haftmann@34943: using count [of M] by (simp add: multiset_def set_of_def) haftmann@34943: bulwahn@46756: lemma finite_Collect_mem [iff]: "finite {x. x :# M}" bulwahn@46756: unfolding set_of_def[symmetric] by simp wenzelm@10249: nipkow@55808: lemma set_of_mono: "A \ B \ set_of A \ set_of B" nipkow@55808: by (metis mset_leD subsetI mem_set_of_iff) nipkow@55808: wenzelm@10249: subsubsection {* Size *} wenzelm@10249: blanchet@56656: definition wcount where "wcount f M = (\x. count M x * Suc (f x))" blanchet@56656: blanchet@56656: lemma wcount_union: "wcount f (M + N) a = wcount f M a + wcount f N a" blanchet@56656: by (auto simp: wcount_def add_mult_distrib) blanchet@56656: blanchet@56656: definition size_multiset :: "('a \ nat) \ 'a multiset \ nat" where blanchet@56656: "size_multiset f M = setsum (wcount f M) (set_of M)" blanchet@56656: blanchet@56656: lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def] blanchet@56656: blanchet@56656: instantiation multiset :: (type) size begin blanchet@56656: definition size_multiset where blanchet@56656: size_multiset_overloaded_def: "size_multiset = Multiset.size_multiset (\_. 0)" haftmann@34943: instance .. haftmann@34943: end haftmann@34943: blanchet@56656: lemmas size_multiset_overloaded_eq = blanchet@56656: size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified] blanchet@56656: blanchet@56656: lemma size_multiset_empty [simp]: "size_multiset f {#} = 0" blanchet@56656: by (simp add: size_multiset_def) blanchet@56656: haftmann@28708: lemma size_empty [simp]: "size {#} = 0" blanchet@56656: by (simp add: size_multiset_overloaded_def) blanchet@56656: blanchet@56656: lemma size_multiset_single [simp]: "size_multiset f {#b#} = Suc (f b)" blanchet@56656: by (simp add: size_multiset_eq) wenzelm@10249: haftmann@28708: lemma size_single [simp]: "size {#b#} = 1" blanchet@56656: by (simp add: size_multiset_overloaded_def) blanchet@56656: blanchet@56656: lemma setsum_wcount_Int: blanchet@56656: "finite A \ setsum (wcount f N) (A \ set_of N) = setsum (wcount f N) A" nipkow@26178: apply (induct rule: finite_induct) nipkow@26178: apply simp blanchet@56656: apply (simp add: Int_insert_left set_of_def wcount_def) blanchet@56656: done blanchet@56656: blanchet@56656: lemma size_multiset_union [simp]: blanchet@56656: "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N" haftmann@57418: apply (simp add: size_multiset_def setsum_Un_nat setsum.distrib setsum_wcount_Int wcount_union) blanchet@56656: apply (subst Int_commute) blanchet@56656: apply (simp add: setsum_wcount_Int) nipkow@26178: done wenzelm@10249: haftmann@28708: lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N" blanchet@56656: by (auto simp add: size_multiset_overloaded_def) blanchet@56656: blanchet@56656: lemma size_multiset_eq_0_iff_empty [iff]: "(size_multiset f M = 0) = (M = {#})" blanchet@56656: by (auto simp add: size_multiset_eq multiset_eq_iff) wenzelm@10249: wenzelm@17161: lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})" blanchet@56656: by (auto simp add: size_multiset_overloaded_def) nipkow@26016: nipkow@26016: lemma nonempty_has_size: "(S \ {#}) = (0 < size S)" nipkow@26178: by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty) wenzelm@10249: wenzelm@17161: lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \a. a :# M" blanchet@56656: apply (unfold size_multiset_overloaded_eq) nipkow@26178: apply (drule setsum_SucD) nipkow@26178: apply auto nipkow@26178: done wenzelm@10249: haftmann@34943: lemma size_eq_Suc_imp_eq_union: haftmann@34943: assumes "size M = Suc n" haftmann@34943: shows "\a N. M = N + {#a#}" haftmann@34943: proof - haftmann@34943: from assms obtain a where "a \# M" haftmann@34943: by (erule size_eq_Suc_imp_elem [THEN exE]) haftmann@34943: then have "M = M - {#a#} + {#a#}" by simp haftmann@34943: then show ?thesis by blast nipkow@23611: qed kleing@15869: nipkow@26016: nipkow@26016: subsection {* Induction and case splits *} wenzelm@10249: wenzelm@18258: theorem multiset_induct [case_names empty add, induct type: multiset]: huffman@48009: assumes empty: "P {#}" huffman@48009: assumes add: "\M x. P M \ P (M + {#x#})" huffman@48009: shows "P M" huffman@48009: proof (induct n \ "size M" arbitrary: M) huffman@48009: case 0 thus "P M" by (simp add: empty) huffman@48009: next huffman@48009: case (Suc k) huffman@48009: obtain N x where "M = N + {#x#}" huffman@48009: using `Suc k = size M` [symmetric] huffman@48009: using size_eq_Suc_imp_eq_union by fast huffman@48009: with Suc add show "P M" by simp wenzelm@10249: qed wenzelm@10249: kleing@25610: lemma multi_nonempty_split: "M \ {#} \ \A a. M = A + {#a#}" nipkow@26178: by (induct M) auto kleing@25610: wenzelm@55913: lemma multiset_cases [cases type]: wenzelm@55913: obtains (empty) "M = {#}" wenzelm@55913: | (add) N x where "M = N + {#x#}" wenzelm@55913: using assms by (induct M) simp_all kleing@25610: haftmann@34943: lemma multi_drop_mem_not_eq: "c \# B \ B - {#c#} \ B" haftmann@34943: by (cases "B = {#}") (auto dest: multi_member_split) haftmann@34943: nipkow@26033: lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \ P x #}" nipkow@39302: apply (subst multiset_eq_iff) nipkow@26178: apply auto nipkow@26178: done wenzelm@10249: haftmann@35268: lemma mset_less_size: "(A::'a multiset) < B \ size A < size B" haftmann@34943: proof (induct A arbitrary: B) haftmann@34943: case (empty M) haftmann@34943: then have "M \ {#}" by (simp add: mset_less_empty_nonempty) haftmann@34943: then obtain M' x where "M = M' + {#x#}" haftmann@34943: by (blast dest: multi_nonempty_split) haftmann@34943: then show ?case by simp haftmann@34943: next haftmann@34943: case (add S x T) haftmann@35268: have IH: "\B. S < B \ size S < size B" by fact haftmann@35268: have SxsubT: "S + {#x#} < T" by fact haftmann@35268: then have "x \# T" and "S < T" by (auto dest: mset_less_insertD) haftmann@34943: then obtain T' where T: "T = T' + {#x#}" haftmann@34943: by (blast dest: multi_member_split) haftmann@35268: then have "S < T'" using SxsubT haftmann@34943: by (blast intro: mset_less_add_bothsides) haftmann@34943: then have "size S < size T'" using IH by simp haftmann@34943: then show ?case using T by simp haftmann@34943: qed haftmann@34943: haftmann@34943: haftmann@34943: subsubsection {* Strong induction and subset induction for multisets *} haftmann@34943: haftmann@34943: text {* Well-foundedness of proper subset operator: *} haftmann@34943: haftmann@34943: text {* proper multiset subset *} haftmann@34943: haftmann@34943: definition haftmann@34943: mset_less_rel :: "('a multiset * 'a multiset) set" where haftmann@35268: "mset_less_rel = {(A,B). A < B}" wenzelm@10249: haftmann@34943: lemma multiset_add_sub_el_shuffle: haftmann@34943: assumes "c \# B" and "b \ c" haftmann@34943: shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}" haftmann@34943: proof - haftmann@34943: from `c \# B` obtain A where B: "B = A + {#c#}" haftmann@34943: by (blast dest: multi_member_split) haftmann@34943: have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp haftmann@34943: then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}" haftmann@34943: by (simp add: add_ac) haftmann@34943: then show ?thesis using B by simp haftmann@34943: qed haftmann@34943: haftmann@34943: lemma wf_mset_less_rel: "wf mset_less_rel" haftmann@34943: apply (unfold mset_less_rel_def) haftmann@34943: apply (rule wf_measure [THEN wf_subset, where f1=size]) haftmann@34943: apply (clarsimp simp: measure_def inv_image_def mset_less_size) haftmann@34943: done haftmann@34943: haftmann@34943: text {* The induction rules: *} haftmann@34943: haftmann@34943: lemma full_multiset_induct [case_names less]: haftmann@35268: assumes ih: "\B. \(A::'a multiset). A < B \ P A \ P B" haftmann@34943: shows "P B" haftmann@34943: apply (rule wf_mset_less_rel [THEN wf_induct]) haftmann@34943: apply (rule ih, auto simp: mset_less_rel_def) haftmann@34943: done haftmann@34943: haftmann@34943: lemma multi_subset_induct [consumes 2, case_names empty add]: haftmann@35268: assumes "F \ A" haftmann@34943: and empty: "P {#}" haftmann@34943: and insert: "\a F. a \# A \ P F \ P (F + {#a#})" haftmann@34943: shows "P F" haftmann@34943: proof - haftmann@35268: from `F \ A` haftmann@34943: show ?thesis haftmann@34943: proof (induct F) haftmann@34943: show "P {#}" by fact haftmann@34943: next haftmann@34943: fix x F haftmann@35268: assume P: "F \ A \ P F" and i: "F + {#x#} \ A" haftmann@34943: show "P (F + {#x#})" haftmann@34943: proof (rule insert) haftmann@34943: from i show "x \# A" by (auto dest: mset_le_insertD) haftmann@35268: from i have "F \ A" by (auto dest: mset_le_insertD) haftmann@34943: with P show "P F" . haftmann@34943: qed haftmann@34943: qed haftmann@34943: qed wenzelm@26145: wenzelm@17161: huffman@48023: subsection {* The fold combinator *} huffman@48023: haftmann@49822: definition fold :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b" huffman@48023: where haftmann@49822: "fold f s M = Finite_Set.fold (\x. f x ^^ count M x) s (set_of M)" huffman@48023: haftmann@49822: lemma fold_mset_empty [simp]: haftmann@49822: "fold f s {#} = s" haftmann@49822: by (simp add: fold_def) huffman@48023: huffman@48023: context comp_fun_commute huffman@48023: begin huffman@48023: haftmann@49822: lemma fold_mset_insert: haftmann@49822: "fold f s (M + {#x#}) = f x (fold f s M)" haftmann@49822: proof - haftmann@49822: interpret mset: comp_fun_commute "\y. f y ^^ count M y" haftmann@49822: by (fact comp_fun_commute_funpow) haftmann@49822: interpret mset_union: comp_fun_commute "\y. f y ^^ count (M + {#x#}) y" haftmann@49822: by (fact comp_fun_commute_funpow) haftmann@49822: show ?thesis haftmann@49822: proof (cases "x \ set_of M") haftmann@49822: case False haftmann@49822: then have *: "count (M + {#x#}) x = 1" by simp haftmann@49822: from False have "Finite_Set.fold (\y. f y ^^ count (M + {#x#}) y) s (set_of M) = haftmann@49822: Finite_Set.fold (\y. f y ^^ count M y) s (set_of M)" haftmann@49822: by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) haftmann@49822: with False * show ?thesis haftmann@49822: by (simp add: fold_def del: count_union) huffman@48023: next haftmann@49822: case True haftmann@49822: def N \ "set_of M - {x}" haftmann@49822: from N_def True have *: "set_of M = insert x N" "x \ N" "finite N" by auto haftmann@49822: then have "Finite_Set.fold (\y. f y ^^ count (M + {#x#}) y) s N = haftmann@49822: Finite_Set.fold (\y. f y ^^ count M y) s N" haftmann@49822: by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) haftmann@49822: with * show ?thesis by (simp add: fold_def del: count_union) simp huffman@48023: qed huffman@48023: qed huffman@48023: haftmann@49822: corollary fold_mset_single [simp]: haftmann@49822: "fold f s {#x#} = f x s" haftmann@49822: proof - haftmann@49822: have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp haftmann@49822: then show ?thesis by simp haftmann@49822: qed huffman@48023: haftmann@51548: lemma fold_mset_fun_left_comm: haftmann@49822: "f x (fold f s M) = fold f (f x s) M" haftmann@49822: by (induct M) (simp_all add: fold_mset_insert fun_left_comm) huffman@48023: huffman@48023: lemma fold_mset_union [simp]: haftmann@49822: "fold f s (M + N) = fold f (fold f s M) N" haftmann@49822: proof (induct M) huffman@48023: case empty then show ?case by simp huffman@48023: next haftmann@49822: case (add M x) haftmann@49822: have "M + {#x#} + N = (M + N) + {#x#}" haftmann@49822: by (simp add: add_ac) haftmann@51548: with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm) huffman@48023: qed huffman@48023: huffman@48023: lemma fold_mset_fusion: huffman@48023: assumes "comp_fun_commute g" haftmann@49822: shows "(\x y. h (g x y) = f x (h y)) \ h (fold g w A) = fold f (h w) A" (is "PROP ?P") huffman@48023: proof - huffman@48023: interpret comp_fun_commute g by (fact assms) huffman@48023: show "PROP ?P" by (induct A) auto huffman@48023: qed huffman@48023: huffman@48023: end huffman@48023: huffman@48023: text {* huffman@48023: A note on code generation: When defining some function containing a haftmann@49822: subterm @{term "fold F"}, code generation is not automatic. When huffman@48023: interpreting locale @{text left_commutative} with @{text F}, the haftmann@49822: would be code thms for @{const fold} become thms like haftmann@49822: @{term "fold F z {#} = z"} where @{text F} is not a pattern but huffman@48023: contains defined symbols, i.e.\ is not a code thm. Hence a separate huffman@48023: constant with its own code thms needs to be introduced for @{text huffman@48023: F}. See the image operator below. huffman@48023: *} huffman@48023: huffman@48023: huffman@48023: subsection {* Image *} huffman@48023: huffman@48023: definition image_mset :: "('a \ 'b) \ 'a multiset \ 'b multiset" where haftmann@49822: "image_mset f = fold (plus o single o f) {#}" huffman@48023: haftmann@49823: lemma comp_fun_commute_mset_image: haftmann@49823: "comp_fun_commute (plus o single o f)" haftmann@49823: proof haftmann@49823: qed (simp add: add_ac fun_eq_iff) huffman@48023: huffman@48023: lemma image_mset_empty [simp]: "image_mset f {#} = {#}" haftmann@49823: by (simp add: image_mset_def) huffman@48023: huffman@48023: lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}" haftmann@49823: proof - haftmann@49823: interpret comp_fun_commute "plus o single o f" haftmann@49823: by (fact comp_fun_commute_mset_image) haftmann@49823: show ?thesis by (simp add: image_mset_def) haftmann@49823: qed huffman@48023: huffman@48023: lemma image_mset_union [simp]: haftmann@49823: "image_mset f (M + N) = image_mset f M + image_mset f N" haftmann@49823: proof - haftmann@49823: interpret comp_fun_commute "plus o single o f" haftmann@49823: by (fact comp_fun_commute_mset_image) haftmann@49823: show ?thesis by (induct N) (simp_all add: image_mset_def add_ac) haftmann@49823: qed haftmann@49823: haftmann@49823: corollary image_mset_insert: haftmann@49823: "image_mset f (M + {#a#}) = image_mset f M + {#f a#}" haftmann@49823: by simp huffman@48023: haftmann@49823: lemma set_of_image_mset [simp]: haftmann@49823: "set_of (image_mset f M) = image f (set_of M)" haftmann@49823: by (induct M) simp_all huffman@48040: haftmann@49823: lemma size_image_mset [simp]: haftmann@49823: "size (image_mset f M) = size M" haftmann@49823: by (induct M) simp_all huffman@48023: haftmann@49823: lemma image_mset_is_empty_iff [simp]: haftmann@49823: "image_mset f M = {#} \ M = {#}" haftmann@49823: by (cases M) auto huffman@48023: huffman@48023: syntax huffman@48023: "_comprehension1_mset" :: "'a \ 'b \ 'b multiset \ 'a multiset" huffman@48023: ("({#_/. _ :# _#})") huffman@48023: translations huffman@48023: "{#e. x:#M#}" == "CONST image_mset (%x. e) M" huffman@48023: huffman@48023: syntax huffman@48023: "_comprehension2_mset" :: "'a \ 'b \ 'b multiset \ bool \ 'a multiset" huffman@48023: ("({#_/ | _ :# _./ _#})") huffman@48023: translations huffman@48023: "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}" huffman@48023: huffman@48023: text {* huffman@48023: This allows to write not just filters like @{term "{#x:#M. x image_mset g = image_mset (f \ g)" huffman@48023: proof huffman@48023: fix A huffman@48023: show "(image_mset f \ image_mset g) A = image_mset (f \ g) A" huffman@48023: by (induct A) simp_all huffman@48023: qed huffman@48023: show "image_mset id = id" huffman@48023: proof huffman@48023: fix A huffman@48023: show "image_mset id A = id A" huffman@48023: by (induct A) simp_all huffman@48023: qed huffman@48023: qed huffman@48023: haftmann@49717: declare image_mset.identity [simp] haftmann@49717: huffman@48023: haftmann@51548: subsection {* Further conversions *} haftmann@34943: haftmann@34943: primrec multiset_of :: "'a list \ 'a multiset" where haftmann@34943: "multiset_of [] = {#}" | haftmann@34943: "multiset_of (a # x) = multiset_of x + {# a #}" haftmann@34943: haftmann@37107: lemma in_multiset_in_set: haftmann@37107: "x \# multiset_of xs \ x \ set xs" haftmann@37107: by (induct xs) simp_all haftmann@37107: haftmann@37107: lemma count_multiset_of: haftmann@37107: "count (multiset_of xs) x = length (filter (\y. x = y) xs)" haftmann@37107: by (induct xs) simp_all haftmann@37107: haftmann@34943: lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])" haftmann@34943: by (induct x) auto haftmann@34943: haftmann@34943: lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])" haftmann@34943: by (induct x) auto haftmann@34943: haftmann@40950: lemma set_of_multiset_of[simp]: "set_of (multiset_of x) = set x" haftmann@34943: by (induct x) auto haftmann@34943: haftmann@34943: lemma mem_set_multiset_eq: "x \ set xs = (x :# multiset_of xs)" haftmann@34943: by (induct xs) auto haftmann@34943: huffman@48012: lemma size_multiset_of [simp]: "size (multiset_of xs) = length xs" huffman@48012: by (induct xs) simp_all huffman@48012: haftmann@34943: lemma multiset_of_append [simp]: haftmann@34943: "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys" haftmann@34943: by (induct xs arbitrary: ys) (auto simp: add_ac) haftmann@34943: haftmann@40303: lemma multiset_of_filter: haftmann@40303: "multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}" haftmann@40303: by (induct xs) simp_all haftmann@40303: haftmann@40950: lemma multiset_of_rev [simp]: haftmann@40950: "multiset_of (rev xs) = multiset_of xs" haftmann@40950: by (induct xs) simp_all haftmann@40950: haftmann@34943: lemma surj_multiset_of: "surj multiset_of" haftmann@34943: apply (unfold surj_def) haftmann@34943: apply (rule allI) haftmann@34943: apply (rule_tac M = y in multiset_induct) haftmann@34943: apply auto haftmann@34943: apply (rule_tac x = "x # xa" in exI) haftmann@34943: apply auto haftmann@34943: done haftmann@34943: haftmann@34943: lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}" haftmann@34943: by (induct x) auto haftmann@34943: haftmann@34943: lemma distinct_count_atmost_1: haftmann@34943: "distinct x = (! a. count (multiset_of x) a = (if a \ set x then 1 else 0))" haftmann@34943: apply (induct x, simp, rule iffI, simp_all) blanchet@55417: apply (rename_tac a b) haftmann@34943: apply (rule conjI) haftmann@34943: apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) haftmann@34943: apply (erule_tac x = a in allE, simp, clarify) haftmann@34943: apply (erule_tac x = aa in allE, simp) haftmann@34943: done haftmann@34943: haftmann@34943: lemma multiset_of_eq_setD: haftmann@34943: "multiset_of xs = multiset_of ys \ set xs = set ys" nipkow@39302: by (rule) (auto simp add:multiset_eq_iff set_count_greater_0) haftmann@34943: haftmann@34943: lemma set_eq_iff_multiset_of_eq_distinct: haftmann@34943: "distinct x \ distinct y \ haftmann@34943: (set x = set y) = (multiset_of x = multiset_of y)" nipkow@39302: by (auto simp: multiset_eq_iff distinct_count_atmost_1) haftmann@34943: haftmann@34943: lemma set_eq_iff_multiset_of_remdups_eq: haftmann@34943: "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))" haftmann@34943: apply (rule iffI) haftmann@34943: apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) haftmann@34943: apply (drule distinct_remdups [THEN distinct_remdups haftmann@34943: [THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]]) haftmann@34943: apply simp haftmann@34943: done haftmann@34943: haftmann@34943: lemma multiset_of_compl_union [simp]: haftmann@34943: "multiset_of [x\xs. P x] + multiset_of [x\xs. \P x] = multiset_of xs" haftmann@34943: by (induct xs) (auto simp: add_ac) haftmann@34943: haftmann@41069: lemma count_multiset_of_length_filter: haftmann@39533: "count (multiset_of xs) x = length (filter (\y. x = y) xs)" haftmann@39533: by (induct xs) auto haftmann@34943: haftmann@34943: lemma nth_mem_multiset_of: "i < length ls \ (ls ! i) :# multiset_of ls" haftmann@34943: apply (induct ls arbitrary: i) haftmann@34943: apply simp haftmann@34943: apply (case_tac i) haftmann@34943: apply auto haftmann@34943: done haftmann@34943: nipkow@36903: lemma multiset_of_remove1[simp]: nipkow@36903: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}" nipkow@39302: by (induct xs) (auto simp add: multiset_eq_iff) haftmann@34943: haftmann@34943: lemma multiset_of_eq_length: haftmann@37107: assumes "multiset_of xs = multiset_of ys" haftmann@37107: shows "length xs = length ys" huffman@48012: using assms by (metis size_multiset_of) haftmann@34943: haftmann@39533: lemma multiset_of_eq_length_filter: haftmann@39533: assumes "multiset_of xs = multiset_of ys" haftmann@39533: shows "length (filter (\x. z = x) xs) = length (filter (\y. z = y) ys)" huffman@48012: using assms by (metis count_multiset_of) haftmann@39533: haftmann@45989: lemma fold_multiset_equiv: haftmann@45989: assumes f: "\x y. x \ set xs \ y \ set xs \ f x \ f y = f y \ f x" haftmann@45989: and equiv: "multiset_of xs = multiset_of ys" haftmann@49822: shows "List.fold f xs = List.fold f ys" wenzelm@46921: using f equiv [symmetric] wenzelm@46921: proof (induct xs arbitrary: ys) haftmann@45989: case Nil then show ?case by simp haftmann@45989: next haftmann@45989: case (Cons x xs) haftmann@45989: then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD) haftmann@45989: have "\x y. x \ set ys \ y \ set ys \ f x \ f y = f y \ f x" haftmann@45989: by (rule Cons.prems(1)) (simp_all add: *) haftmann@45989: moreover from * have "x \ set ys" by simp haftmann@49822: ultimately have "List.fold f ys = List.fold f (remove1 x ys) \ f x" by (fact fold_remove1_split) haftmann@49822: moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)" by (auto intro: Cons.hyps) haftmann@45989: ultimately show ?case by simp haftmann@45989: qed haftmann@45989: haftmann@51548: lemma multiset_of_insort [simp]: haftmann@51548: "multiset_of (insort x xs) = multiset_of xs + {#x#}" haftmann@51548: by (induct xs) (simp_all add: ac_simps) haftmann@51548: haftmann@51600: lemma in_multiset_of: haftmann@51600: "x \# multiset_of xs \ x \ set xs" haftmann@51600: by (induct xs) simp_all haftmann@51600: haftmann@51600: lemma multiset_of_map: haftmann@51600: "multiset_of (map f xs) = image_mset f (multiset_of xs)" haftmann@51600: by (induct xs) simp_all haftmann@51600: haftmann@51548: definition multiset_of_set :: "'a set \ 'a multiset" haftmann@51548: where haftmann@51548: "multiset_of_set = folding.F (\x M. {#x#} + M) {#}" haftmann@51548: haftmann@51548: interpretation multiset_of_set!: folding "\x M. {#x#} + M" "{#}" haftmann@51548: where haftmann@51548: "folding.F (\x M. {#x#} + M) {#} = multiset_of_set" haftmann@51548: proof - haftmann@51548: interpret comp_fun_commute "\x M. {#x#} + M" by default (simp add: fun_eq_iff ac_simps) haftmann@51548: show "folding (\x M. {#x#} + M)" by default (fact comp_fun_commute) haftmann@51548: from multiset_of_set_def show "folding.F (\x M. {#x#} + M) {#} = multiset_of_set" .. haftmann@51548: qed haftmann@51548: haftmann@51600: lemma count_multiset_of_set [simp]: haftmann@51600: "finite A \ x \ A \ count (multiset_of_set A) x = 1" (is "PROP ?P") haftmann@51600: "\ finite A \ count (multiset_of_set A) x = 0" (is "PROP ?Q") haftmann@51600: "x \ A \ count (multiset_of_set A) x = 0" (is "PROP ?R") haftmann@51600: proof - haftmann@51600: { fix A haftmann@51600: assume "x \ A" haftmann@51600: have "count (multiset_of_set A) x = 0" haftmann@51600: proof (cases "finite A") haftmann@51600: case False then show ?thesis by simp haftmann@51600: next haftmann@51600: case True from True `x \ A` show ?thesis by (induct A) auto haftmann@51600: qed haftmann@51600: } note * = this haftmann@51600: then show "PROP ?P" "PROP ?Q" "PROP ?R" haftmann@51600: by (auto elim!: Set.set_insert) haftmann@51600: qed -- {* TODO: maybe define @{const multiset_of_set} also in terms of @{const Abs_multiset} *} haftmann@51600: haftmann@51548: context linorder haftmann@51548: begin haftmann@51548: haftmann@51548: definition sorted_list_of_multiset :: "'a multiset \ 'a list" haftmann@51548: where haftmann@51548: "sorted_list_of_multiset M = fold insort [] M" haftmann@51548: haftmann@51548: lemma sorted_list_of_multiset_empty [simp]: haftmann@51548: "sorted_list_of_multiset {#} = []" haftmann@51548: by (simp add: sorted_list_of_multiset_def) haftmann@51548: haftmann@51548: lemma sorted_list_of_multiset_singleton [simp]: haftmann@51548: "sorted_list_of_multiset {#x#} = [x]" haftmann@51548: proof - haftmann@51548: interpret comp_fun_commute insort by (fact comp_fun_commute_insort) haftmann@51548: show ?thesis by (simp add: sorted_list_of_multiset_def) haftmann@51548: qed haftmann@51548: haftmann@51548: lemma sorted_list_of_multiset_insert [simp]: haftmann@51548: "sorted_list_of_multiset (M + {#x#}) = List.insort x (sorted_list_of_multiset M)" haftmann@51548: proof - haftmann@51548: interpret comp_fun_commute insort by (fact comp_fun_commute_insort) haftmann@51548: show ?thesis by (simp add: sorted_list_of_multiset_def) haftmann@51548: qed haftmann@51548: haftmann@51548: end haftmann@51548: haftmann@51548: lemma multiset_of_sorted_list_of_multiset [simp]: haftmann@51548: "multiset_of (sorted_list_of_multiset M) = M" haftmann@51548: by (induct M) simp_all haftmann@51548: haftmann@51548: lemma sorted_list_of_multiset_multiset_of [simp]: haftmann@51548: "sorted_list_of_multiset (multiset_of xs) = sort xs" haftmann@51548: by (induct xs) simp_all haftmann@51548: haftmann@51548: lemma finite_set_of_multiset_of_set: haftmann@51548: assumes "finite A" haftmann@51548: shows "set_of (multiset_of_set A) = A" haftmann@51548: using assms by (induct A) simp_all haftmann@51548: haftmann@51548: lemma infinite_set_of_multiset_of_set: haftmann@51548: assumes "\ finite A" haftmann@51548: shows "set_of (multiset_of_set A) = {}" haftmann@51548: using assms by simp haftmann@51548: haftmann@51548: lemma set_sorted_list_of_multiset [simp]: haftmann@51548: "set (sorted_list_of_multiset M) = set_of M" haftmann@51548: by (induct M) (simp_all add: set_insort) haftmann@51548: haftmann@51548: lemma sorted_list_of_multiset_of_set [simp]: haftmann@51548: "sorted_list_of_multiset (multiset_of_set A) = sorted_list_of_set A" haftmann@51548: by (cases "finite A") (induct A rule: finite_induct, simp_all add: ac_simps) haftmann@51548: haftmann@51548: haftmann@51548: subsection {* Big operators *} haftmann@51548: haftmann@51548: no_notation times (infixl "*" 70) haftmann@51548: no_notation Groups.one ("1") haftmann@51548: haftmann@51548: locale comm_monoid_mset = comm_monoid haftmann@51548: begin haftmann@51548: haftmann@51548: definition F :: "'a multiset \ 'a" haftmann@51548: where haftmann@51548: eq_fold: "F M = Multiset.fold f 1 M" haftmann@51548: haftmann@51548: lemma empty [simp]: haftmann@51548: "F {#} = 1" haftmann@51548: by (simp add: eq_fold) haftmann@51548: haftmann@51548: lemma singleton [simp]: haftmann@51548: "F {#x#} = x" haftmann@51548: proof - haftmann@51548: interpret comp_fun_commute haftmann@51548: by default (simp add: fun_eq_iff left_commute) haftmann@51548: show ?thesis by (simp add: eq_fold) haftmann@51548: qed haftmann@51548: haftmann@51548: lemma union [simp]: haftmann@51548: "F (M + N) = F M * F N" haftmann@51548: proof - haftmann@51548: interpret comp_fun_commute f haftmann@51548: by default (simp add: fun_eq_iff left_commute) haftmann@51548: show ?thesis by (induct N) (simp_all add: left_commute eq_fold) haftmann@51548: qed haftmann@51548: haftmann@51548: end haftmann@51548: haftmann@51548: notation times (infixl "*" 70) haftmann@51548: notation Groups.one ("1") haftmann@51548: haftmann@54868: context comm_monoid_add haftmann@54868: begin haftmann@54868: haftmann@54868: definition msetsum :: "'a multiset \ 'a" haftmann@51548: where haftmann@51548: "msetsum = comm_monoid_mset.F plus 0" haftmann@51548: haftmann@54868: sublocale msetsum!: comm_monoid_mset plus 0 haftmann@51548: where haftmann@51548: "comm_monoid_mset.F plus 0 = msetsum" haftmann@51548: proof - haftmann@51548: show "comm_monoid_mset plus 0" .. haftmann@51548: from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" .. haftmann@51548: qed haftmann@51548: haftmann@51548: lemma setsum_unfold_msetsum: haftmann@51548: "setsum f A = msetsum (image_mset f (multiset_of_set A))" haftmann@51548: by (cases "finite A") (induct A rule: finite_induct, simp_all) haftmann@51548: haftmann@51548: abbreviation msetsum_image :: "('b \ 'a) \ 'b multiset \ 'a" haftmann@51548: where haftmann@51548: "msetsum_image f M \ msetsum (image_mset f M)" haftmann@51548: haftmann@51548: end haftmann@51548: haftmann@51548: syntax haftmann@51548: "_msetsum_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" haftmann@51548: ("(3SUM _:#_. _)" [0, 51, 10] 10) haftmann@51548: haftmann@51548: syntax (xsymbols) haftmann@51548: "_msetsum_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" haftmann@51548: ("(3\_:#_. _)" [0, 51, 10] 10) haftmann@51548: haftmann@51548: syntax (HTML output) haftmann@51548: "_msetsum_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" haftmann@51548: ("(3\_\#_. _)" [0, 51, 10] 10) haftmann@51548: haftmann@51548: translations haftmann@51548: "SUM i :# A. b" == "CONST msetsum_image (\i. b) A" haftmann@51548: haftmann@54868: context comm_monoid_mult haftmann@54868: begin haftmann@54868: haftmann@54868: definition msetprod :: "'a multiset \ 'a" haftmann@54868: where haftmann@54868: "msetprod = comm_monoid_mset.F times 1" haftmann@54868: haftmann@54868: sublocale msetprod!: comm_monoid_mset times 1 haftmann@51548: where haftmann@51548: "comm_monoid_mset.F times 1 = msetprod" haftmann@51548: proof - haftmann@51548: show "comm_monoid_mset times 1" .. haftmann@51548: from msetprod_def show "comm_monoid_mset.F times 1 = msetprod" .. haftmann@51548: qed haftmann@51548: haftmann@51548: lemma msetprod_empty: haftmann@51548: "msetprod {#} = 1" haftmann@51548: by (fact msetprod.empty) haftmann@51548: haftmann@51548: lemma msetprod_singleton: haftmann@51548: "msetprod {#x#} = x" haftmann@51548: by (fact msetprod.singleton) haftmann@51548: haftmann@51548: lemma msetprod_Un: haftmann@51548: "msetprod (A + B) = msetprod A * msetprod B" haftmann@51548: by (fact msetprod.union) haftmann@51548: haftmann@51548: lemma setprod_unfold_msetprod: haftmann@51548: "setprod f A = msetprod (image_mset f (multiset_of_set A))" haftmann@51548: by (cases "finite A") (induct A rule: finite_induct, simp_all) haftmann@51548: haftmann@51548: lemma msetprod_multiplicity: haftmann@51548: "msetprod M = setprod (\x. x ^ count M x) (set_of M)" haftmann@51548: by (simp add: Multiset.fold_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def) haftmann@51548: haftmann@51548: abbreviation msetprod_image :: "('b \ 'a) \ 'b multiset \ 'a" haftmann@51548: where haftmann@51548: "msetprod_image f M \ msetprod (image_mset f M)" haftmann@51548: haftmann@51548: end haftmann@51548: haftmann@51548: syntax haftmann@51548: "_msetprod_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_mult" haftmann@51548: ("(3PROD _:#_. _)" [0, 51, 10] 10) haftmann@51548: haftmann@51548: syntax (xsymbols) haftmann@51548: "_msetprod_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_mult" haftmann@51548: ("(3\_\#_. _)" [0, 51, 10] 10) haftmann@51548: haftmann@51548: syntax (HTML output) haftmann@51548: "_msetprod_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_mult" haftmann@51548: ("(3\_\#_. _)" [0, 51, 10] 10) haftmann@51548: haftmann@51548: translations haftmann@51548: "PROD i :# A. b" == "CONST msetprod_image (\i. b) A" haftmann@51548: haftmann@51548: lemma (in comm_semiring_1) dvd_msetprod: haftmann@51548: assumes "x \# A" haftmann@51548: shows "x dvd msetprod A" haftmann@51548: proof - haftmann@51548: from assms have "A = (A - {#x#}) + {#x#}" by simp haftmann@51548: then obtain B where "A = B + {#x#}" .. haftmann@51548: then show ?thesis by simp haftmann@51548: qed haftmann@51548: haftmann@51548: haftmann@51548: subsection {* Cardinality *} haftmann@51548: haftmann@51548: definition mcard :: "'a multiset \ nat" haftmann@51548: where haftmann@51548: "mcard = msetsum \ image_mset (\_. 1)" haftmann@51548: haftmann@51548: lemma mcard_empty [simp]: haftmann@51548: "mcard {#} = 0" haftmann@51548: by (simp add: mcard_def) haftmann@51548: haftmann@51548: lemma mcard_singleton [simp]: haftmann@51548: "mcard {#a#} = Suc 0" haftmann@51548: by (simp add: mcard_def) haftmann@51548: haftmann@51548: lemma mcard_plus [simp]: haftmann@51548: "mcard (M + N) = mcard M + mcard N" haftmann@51548: by (simp add: mcard_def) haftmann@51548: haftmann@51548: lemma mcard_empty_iff [simp]: haftmann@51548: "mcard M = 0 \ M = {#}" haftmann@51548: by (induct M) simp_all haftmann@51548: haftmann@51548: lemma mcard_unfold_setsum: haftmann@51548: "mcard M = setsum (count M) (set_of M)" haftmann@51548: proof (induct M) haftmann@51548: case empty then show ?case by simp haftmann@51548: next haftmann@51548: case (add M x) then show ?case haftmann@51548: by (cases "x \ set_of M") haftmann@51548: (simp_all del: mem_set_of_iff add: setsum.distrib setsum.delta' insert_absorb, simp) haftmann@51548: qed haftmann@51548: haftmann@51600: lemma size_eq_mcard: haftmann@51600: "size = mcard" blanchet@56656: by (simp add: fun_eq_iff size_multiset_overloaded_eq mcard_unfold_setsum) haftmann@51600: haftmann@51600: lemma mcard_multiset_of: haftmann@51600: "mcard (multiset_of xs) = length xs" haftmann@51600: by (induct xs) simp_all haftmann@51600: haftmann@51548: haftmann@51548: subsection {* Alternative representations *} haftmann@51548: haftmann@51548: subsubsection {* Lists *} haftmann@51548: haftmann@39533: context linorder haftmann@39533: begin haftmann@39533: haftmann@40210: lemma multiset_of_insort [simp]: haftmann@39533: "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs" haftmann@37107: by (induct xs) (simp_all add: ac_simps) haftmann@39533: haftmann@40210: lemma multiset_of_sort [simp]: haftmann@39533: "multiset_of (sort_key k xs) = multiset_of xs" haftmann@37107: by (induct xs) (simp_all add: ac_simps) haftmann@37107: haftmann@34943: text {* haftmann@34943: This lemma shows which properties suffice to show that a function haftmann@34943: @{text "f"} with @{text "f xs = ys"} behaves like sort. haftmann@34943: *} haftmann@37074: haftmann@39533: lemma properties_for_sort_key: haftmann@39533: assumes "multiset_of ys = multiset_of xs" haftmann@40305: and "\k. k \ set ys \ filter (\x. f k = f x) ys = filter (\x. f k = f x) xs" haftmann@39533: and "sorted (map f ys)" haftmann@39533: shows "sort_key f xs = ys" wenzelm@46921: using assms wenzelm@46921: proof (induct xs arbitrary: ys) haftmann@34943: case Nil then show ?case by simp haftmann@34943: next haftmann@34943: case (Cons x xs) haftmann@39533: from Cons.prems(2) have haftmann@40305: "\k \ set ys. filter (\x. f k = f x) (remove1 x ys) = filter (\x. f k = f x) xs" haftmann@39533: by (simp add: filter_remove1) haftmann@39533: with Cons.prems have "sort_key f xs = remove1 x ys" haftmann@39533: by (auto intro!: Cons.hyps simp add: sorted_map_remove1) haftmann@39533: moreover from Cons.prems have "x \ set ys" haftmann@39533: by (auto simp add: mem_set_multiset_eq intro!: ccontr) haftmann@39533: ultimately show ?case using Cons.prems by (simp add: insort_key_remove1) haftmann@34943: qed haftmann@34943: haftmann@39533: lemma properties_for_sort: haftmann@39533: assumes multiset: "multiset_of ys = multiset_of xs" haftmann@39533: and "sorted ys" haftmann@39533: shows "sort xs = ys" haftmann@39533: proof (rule properties_for_sort_key) haftmann@39533: from multiset show "multiset_of ys = multiset_of xs" . haftmann@39533: from `sorted ys` show "sorted (map (\x. x) ys)" by simp haftmann@39533: from multiset have "\k. length (filter (\y. k = y) ys) = length (filter (\x. k = x) xs)" haftmann@39533: by (rule multiset_of_eq_length_filter) haftmann@39533: then have "\k. replicate (length (filter (\y. k = y) ys)) k = replicate (length (filter (\x. k = x) xs)) k" haftmann@39533: by simp haftmann@40305: then show "\k. k \ set ys \ filter (\y. k = y) ys = filter (\x. k = x) xs" haftmann@39533: by (simp add: replicate_length_filter) haftmann@39533: qed haftmann@39533: haftmann@40303: lemma sort_key_by_quicksort: haftmann@40303: "sort_key f xs = sort_key f [x\xs. f x < f (xs ! (length xs div 2))] haftmann@40303: @ [x\xs. f x = f (xs ! (length xs div 2))] haftmann@40303: @ sort_key f [x\xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs") haftmann@40303: proof (rule properties_for_sort_key) haftmann@40303: show "multiset_of ?rhs = multiset_of ?lhs" haftmann@40303: by (rule multiset_eqI) (auto simp add: multiset_of_filter) haftmann@40303: next haftmann@40303: show "sorted (map f ?rhs)" haftmann@40303: by (auto simp add: sorted_append intro: sorted_map_same) haftmann@40303: next haftmann@40305: fix l haftmann@40305: assume "l \ set ?rhs" haftmann@40346: let ?pivot = "f (xs ! (length xs div 2))" haftmann@40346: have *: "\x. f l = f x \ f x = f l" by auto haftmann@40306: have "[x \ sort_key f xs . f x = f l] = [x \ xs. f x = f l]" haftmann@40305: unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) haftmann@40346: with * have **: "[x \ sort_key f xs . f l = f x] = [x \ xs. f l = f x]" by simp haftmann@40346: have "\x P. P (f x) ?pivot \ f l = f x \ P (f l) ?pivot \ f l = f x" by auto haftmann@40346: then have "\P. [x \ sort_key f xs . P (f x) ?pivot \ f l = f x] = haftmann@40346: [x \ sort_key f xs. P (f l) ?pivot \ f l = f x]" by simp haftmann@40346: note *** = this [of "op <"] this [of "op >"] this [of "op ="] haftmann@40306: show "[x \ ?rhs. f l = f x] = [x \ ?lhs. f l = f x]" haftmann@40305: proof (cases "f l" ?pivot rule: linorder_cases) wenzelm@46730: case less wenzelm@46730: then have "f l \ ?pivot" and "\ f l > ?pivot" by auto wenzelm@46730: with less show ?thesis haftmann@40346: by (simp add: filter_sort [symmetric] ** ***) haftmann@40305: next haftmann@40306: case equal then show ?thesis haftmann@40346: by (simp add: * less_le) haftmann@40305: next wenzelm@46730: case greater wenzelm@46730: then have "f l \ ?pivot" and "\ f l < ?pivot" by auto wenzelm@46730: with greater show ?thesis haftmann@40346: by (simp add: filter_sort [symmetric] ** ***) haftmann@40306: qed haftmann@40303: qed haftmann@40303: haftmann@40303: lemma sort_by_quicksort: haftmann@40303: "sort xs = sort [x\xs. x < xs ! (length xs div 2)] haftmann@40303: @ [x\xs. x = xs ! (length xs div 2)] haftmann@40303: @ sort [x\xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs") haftmann@40303: using sort_key_by_quicksort [of "\x. x", symmetric] by simp haftmann@40303: haftmann@40347: text {* A stable parametrized quicksort *} haftmann@40347: haftmann@40347: definition part :: "('b \ 'a) \ 'a \ 'b list \ 'b list \ 'b list \ 'b list" where haftmann@40347: "part f pivot xs = ([x \ xs. f x < pivot], [x \ xs. f x = pivot], [x \ xs. pivot < f x])" haftmann@40347: haftmann@40347: lemma part_code [code]: haftmann@40347: "part f pivot [] = ([], [], [])" haftmann@40347: "part f pivot (x # xs) = (let (lts, eqs, gts) = part f pivot xs; x' = f x in haftmann@40347: if x' < pivot then (x # lts, eqs, gts) haftmann@40347: else if x' > pivot then (lts, eqs, x # gts) haftmann@40347: else (lts, x # eqs, gts))" haftmann@40347: by (auto simp add: part_def Let_def split_def) haftmann@40347: haftmann@40347: lemma sort_key_by_quicksort_code [code]: haftmann@40347: "sort_key f xs = (case xs of [] \ [] haftmann@40347: | [x] \ xs haftmann@40347: | [x, y] \ (if f x \ f y then xs else [y, x]) haftmann@40347: | _ \ (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs haftmann@40347: in sort_key f lts @ eqs @ sort_key f gts))" haftmann@40347: proof (cases xs) haftmann@40347: case Nil then show ?thesis by simp haftmann@40347: next wenzelm@46921: case (Cons _ ys) note hyps = Cons show ?thesis wenzelm@46921: proof (cases ys) haftmann@40347: case Nil with hyps show ?thesis by simp haftmann@40347: next wenzelm@46921: case (Cons _ zs) note hyps = hyps Cons show ?thesis wenzelm@46921: proof (cases zs) haftmann@40347: case Nil with hyps show ?thesis by auto haftmann@40347: next haftmann@40347: case Cons haftmann@40347: from sort_key_by_quicksort [of f xs] haftmann@40347: have "sort_key f xs = (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs haftmann@40347: in sort_key f lts @ eqs @ sort_key f gts)" haftmann@40347: by (simp only: split_def Let_def part_def fst_conv snd_conv) haftmann@40347: with hyps Cons show ?thesis by (simp only: list.cases) haftmann@40347: qed haftmann@40347: qed haftmann@40347: qed haftmann@40347: haftmann@39533: end haftmann@39533: haftmann@40347: hide_const (open) part haftmann@40347: haftmann@35268: lemma multiset_of_remdups_le: "multiset_of (remdups xs) \ multiset_of xs" haftmann@35268: by (induct xs) (auto intro: order_trans) haftmann@34943: haftmann@34943: lemma multiset_of_update: haftmann@34943: "i < length ls \ multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}" haftmann@34943: proof (induct ls arbitrary: i) haftmann@34943: case Nil then show ?case by simp haftmann@34943: next haftmann@34943: case (Cons x xs) haftmann@34943: show ?case haftmann@34943: proof (cases i) haftmann@34943: case 0 then show ?thesis by simp haftmann@34943: next haftmann@34943: case (Suc i') haftmann@34943: with Cons show ?thesis haftmann@34943: apply simp haftmann@57512: apply (subst add.assoc) haftmann@57512: apply (subst add.commute [of "{#v#}" "{#x#}"]) haftmann@57512: apply (subst add.assoc [symmetric]) haftmann@34943: apply simp haftmann@34943: apply (rule mset_le_multiset_union_diff_commute) haftmann@34943: apply (simp add: mset_le_single nth_mem_multiset_of) haftmann@34943: done haftmann@34943: qed haftmann@34943: qed haftmann@34943: haftmann@34943: lemma multiset_of_swap: haftmann@34943: "i < length ls \ j < length ls \ haftmann@34943: multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls" haftmann@34943: by (cases "i = j") (simp_all add: multiset_of_update nth_mem_multiset_of) haftmann@34943: haftmann@34943: haftmann@34943: subsection {* The multiset order *} wenzelm@10249: wenzelm@10249: subsubsection {* Well-foundedness *} wenzelm@10249: haftmann@28708: definition mult1 :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" where haftmann@37765: "mult1 r = {(N, M). \a M0 K. M = M0 + {#a#} \ N = M0 + K \ berghofe@23751: (\b. b :# K --> (b, a) \ r)}" wenzelm@10249: haftmann@28708: definition mult :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" where haftmann@37765: "mult r = (mult1 r)\<^sup>+" wenzelm@10249: berghofe@23751: lemma not_less_empty [iff]: "(M, {#}) \ mult1 r" nipkow@26178: by (simp add: mult1_def) wenzelm@10249: berghofe@23751: lemma less_add: "(N, M0 + {#a#}) \ mult1 r ==> berghofe@23751: (\M. (M, M0) \ mult1 r \ N = M + {#a#}) \ berghofe@23751: (\K. (\b. b :# K --> (b, a) \ r) \ N = M0 + K)" wenzelm@19582: (is "_ \ ?case1 (mult1 r) \ ?case2") wenzelm@10249: proof (unfold mult1_def) berghofe@23751: let ?r = "\K a. \b. b :# K --> (b, a) \ r" nipkow@11464: let ?R = "\N M. \a M0 K. M = M0 + {#a#} \ N = M0 + K \ ?r K a" berghofe@23751: let ?case1 = "?case1 {(N, M). ?R N M}" wenzelm@10249: berghofe@23751: assume "(N, M0 + {#a#}) \ {(N, M). ?R N M}" wenzelm@18258: then have "\a' M0' K. nipkow@11464: M0 + {#a#} = M0' + {#a'#} \ N = M0' + K \ ?r K a'" by simp wenzelm@18258: then show "?case1 \ ?case2" wenzelm@10249: proof (elim exE conjE) wenzelm@10249: fix a' M0' K wenzelm@10249: assume N: "N = M0' + K" and r: "?r K a'" wenzelm@10249: assume "M0 + {#a#} = M0' + {#a'#}" wenzelm@18258: then have "M0 = M0' \ a = a' \ nipkow@11464: (\K'. M0 = K' + {#a'#} \ M0' = K' + {#a#})" wenzelm@10249: by (simp only: add_eq_conv_ex) wenzelm@18258: then show ?thesis wenzelm@10249: proof (elim disjE conjE exE) wenzelm@10249: assume "M0 = M0'" "a = a'" nipkow@11464: with N r have "?r K a \ N = M0 + K" by simp wenzelm@18258: then have ?case2 .. then show ?thesis .. wenzelm@10249: next wenzelm@10249: fix K' wenzelm@10249: assume "M0' = K' + {#a#}" haftmann@34943: with N have n: "N = K' + K + {#a#}" by (simp add: add_ac) wenzelm@10249: wenzelm@10249: assume "M0 = K' + {#a'#}" wenzelm@10249: with r have "?R (K' + K) M0" by blast wenzelm@18258: with n have ?case1 by simp then show ?thesis .. wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: haftmann@54295: lemma all_accessible: "wf r ==> \M. M \ Wellfounded.acc (mult1 r)" wenzelm@10249: proof wenzelm@10249: let ?R = "mult1 r" haftmann@54295: let ?W = "Wellfounded.acc ?R" wenzelm@10249: { wenzelm@10249: fix M M0 a berghofe@23751: assume M0: "M0 \ ?W" berghofe@23751: and wf_hyp: "!!b. (b, a) \ r ==> (\M \ ?W. M + {#b#} \ ?W)" berghofe@23751: and acc_hyp: "\M. (M, M0) \ ?R --> M + {#a#} \ ?W" berghofe@23751: have "M0 + {#a#} \ ?W" berghofe@23751: proof (rule accI [of "M0 + {#a#}"]) wenzelm@10249: fix N berghofe@23751: assume "(N, M0 + {#a#}) \ ?R" berghofe@23751: then have "((\M. (M, M0) \ ?R \ N = M + {#a#}) \ berghofe@23751: (\K. (\b. b :# K --> (b, a) \ r) \ N = M0 + K))" wenzelm@10249: by (rule less_add) berghofe@23751: then show "N \ ?W" wenzelm@10249: proof (elim exE disjE conjE) berghofe@23751: fix M assume "(M, M0) \ ?R" and N: "N = M + {#a#}" berghofe@23751: from acc_hyp have "(M, M0) \ ?R --> M + {#a#} \ ?W" .. berghofe@23751: from this and `(M, M0) \ ?R` have "M + {#a#} \ ?W" .. berghofe@23751: then show "N \ ?W" by (simp only: N) wenzelm@10249: next wenzelm@10249: fix K wenzelm@10249: assume N: "N = M0 + K" berghofe@23751: assume "\b. b :# K --> (b, a) \ r" berghofe@23751: then have "M0 + K \ ?W" wenzelm@10249: proof (induct K) wenzelm@18730: case empty berghofe@23751: from M0 show "M0 + {#} \ ?W" by simp wenzelm@18730: next wenzelm@18730: case (add K x) berghofe@23751: from add.prems have "(x, a) \ r" by simp berghofe@23751: with wf_hyp have "\M \ ?W. M + {#x#} \ ?W" by blast berghofe@23751: moreover from add have "M0 + K \ ?W" by simp berghofe@23751: ultimately have "(M0 + K) + {#x#} \ ?W" .. haftmann@57512: then show "M0 + (K + {#x#}) \ ?W" by (simp only: add.assoc) wenzelm@10249: qed berghofe@23751: then show "N \ ?W" by (simp only: N) wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: } note tedious_reasoning = this wenzelm@10249: berghofe@23751: assume wf: "wf r" wenzelm@10249: fix M berghofe@23751: show "M \ ?W" wenzelm@10249: proof (induct M) berghofe@23751: show "{#} \ ?W" wenzelm@10249: proof (rule accI) berghofe@23751: fix b assume "(b, {#}) \ ?R" berghofe@23751: with not_less_empty show "b \ ?W" by contradiction wenzelm@10249: qed wenzelm@10249: berghofe@23751: fix M a assume "M \ ?W" berghofe@23751: from wf have "\M \ ?W. M + {#a#} \ ?W" wenzelm@10249: proof induct wenzelm@10249: fix a berghofe@23751: assume r: "!!b. (b, a) \ r ==> (\M \ ?W. M + {#b#} \ ?W)" berghofe@23751: show "\M \ ?W. M + {#a#} \ ?W" wenzelm@10249: proof berghofe@23751: fix M assume "M \ ?W" berghofe@23751: then show "M + {#a#} \ ?W" wenzelm@23373: by (rule acc_induct) (rule tedious_reasoning [OF _ r]) wenzelm@10249: qed wenzelm@10249: qed berghofe@23751: from this and `M \ ?W` show "M + {#a#} \ ?W" .. wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: berghofe@23751: theorem wf_mult1: "wf r ==> wf (mult1 r)" nipkow@26178: by (rule acc_wfI) (rule all_accessible) wenzelm@10249: berghofe@23751: theorem wf_mult: "wf r ==> wf (mult r)" nipkow@26178: unfolding mult_def by (rule wf_trancl) (rule wf_mult1) wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Closure-free presentation *} wenzelm@10249: wenzelm@10249: text {* One direction. *} wenzelm@10249: wenzelm@10249: lemma mult_implies_one_step: berghofe@23751: "trans r ==> (M, N) \ mult r ==> nipkow@11464: \I J K. N = I + J \ M = I + K \ J \ {#} \ berghofe@23751: (\k \ set_of K. \j \ set_of J. (k, j) \ r)" nipkow@26178: apply (unfold mult_def mult1_def set_of_def) nipkow@26178: apply (erule converse_trancl_induct, clarify) nipkow@26178: apply (rule_tac x = M0 in exI, simp, clarify) nipkow@26178: apply (case_tac "a :# K") nipkow@26178: apply (rule_tac x = I in exI) nipkow@26178: apply (simp (no_asm)) nipkow@26178: apply (rule_tac x = "(K - {#a#}) + Ka" in exI) haftmann@57512: apply (simp (no_asm_simp) add: add.assoc [symmetric]) thomas@57492: apply (drule_tac f = "\M. M - {#a#}" and x="?S + ?T" in arg_cong) nipkow@26178: apply (simp add: diff_union_single_conv) nipkow@26178: apply (simp (no_asm_use) add: trans_def) nipkow@26178: apply blast nipkow@26178: apply (subgoal_tac "a :# I") nipkow@26178: apply (rule_tac x = "I - {#a#}" in exI) nipkow@26178: apply (rule_tac x = "J + {#a#}" in exI) nipkow@26178: apply (rule_tac x = "K + Ka" in exI) nipkow@26178: apply (rule conjI) nipkow@39302: apply (simp add: multiset_eq_iff split: nat_diff_split) nipkow@26178: apply (rule conjI) thomas@57492: apply (drule_tac f = "\M. M - {#a#}" and x="?S + ?T" in arg_cong, simp) nipkow@39302: apply (simp add: multiset_eq_iff split: nat_diff_split) nipkow@26178: apply (simp (no_asm_use) add: trans_def) nipkow@26178: apply blast nipkow@26178: apply (subgoal_tac "a :# (M0 + {#a#})") nipkow@26178: apply simp nipkow@26178: apply (simp (no_asm)) nipkow@26178: done wenzelm@10249: wenzelm@10249: lemma one_step_implies_mult_aux: berghofe@23751: "trans r ==> berghofe@23751: \I J K. (size J = n \ J \ {#} \ (\k \ set_of K. \j \ set_of J. (k, j) \ r)) berghofe@23751: --> (I + K, I + J) \ mult r" nipkow@26178: apply (induct_tac n, auto) nipkow@26178: apply (frule size_eq_Suc_imp_eq_union, clarify) nipkow@26178: apply (rename_tac "J'", simp) nipkow@26178: apply (erule notE, auto) nipkow@26178: apply (case_tac "J' = {#}") nipkow@26178: apply (simp add: mult_def) nipkow@26178: apply (rule r_into_trancl) nipkow@26178: apply (simp add: mult1_def set_of_def, blast) nipkow@26178: txt {* Now we know @{term "J' \ {#}"}. *} nipkow@26178: apply (cut_tac M = K and P = "\x. (x, a) \ r" in multiset_partition) nipkow@26178: apply (erule_tac P = "\k \ set_of K. ?P k" in rev_mp) nipkow@26178: apply (erule ssubst) nipkow@26178: apply (simp add: Ball_def, auto) nipkow@26178: apply (subgoal_tac nipkow@26178: "((I + {# x :# K. (x, a) \ r #}) + {# x :# K. (x, a) \ r #}, nipkow@26178: (I + {# x :# K. (x, a) \ r #}) + J') \ mult r") nipkow@26178: prefer 2 nipkow@26178: apply force haftmann@57512: apply (simp (no_asm_use) add: add.assoc [symmetric] mult_def) nipkow@26178: apply (erule trancl_trans) nipkow@26178: apply (rule r_into_trancl) nipkow@26178: apply (simp add: mult1_def set_of_def) nipkow@26178: apply (rule_tac x = a in exI) nipkow@26178: apply (rule_tac x = "I + J'" in exI) haftmann@34943: apply (simp add: add_ac) nipkow@26178: done wenzelm@10249: wenzelm@17161: lemma one_step_implies_mult: berghofe@23751: "trans r ==> J \ {#} ==> \k \ set_of K. \j \ set_of J. (k, j) \ r berghofe@23751: ==> (I + K, I + J) \ mult r" nipkow@26178: using one_step_implies_mult_aux by blast wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Partial-order properties *} wenzelm@10249: haftmann@35273: definition less_multiset :: "'a\order multiset \ 'a multiset \ bool" (infix "<#" 50) where haftmann@35273: "M' <# M \ (M', M) \ mult {(x', x). x' < x}" wenzelm@10249: haftmann@35273: definition le_multiset :: "'a\order multiset \ 'a multiset \ bool" (infix "<=#" 50) where haftmann@35273: "M' <=# M \ M' <# M \ M' = M" haftmann@35273: haftmann@35308: notation (xsymbols) less_multiset (infix "\#" 50) haftmann@35308: notation (xsymbols) le_multiset (infix "\#" 50) wenzelm@10249: haftmann@35268: interpretation multiset_order: order le_multiset less_multiset haftmann@35268: proof - haftmann@35268: have irrefl: "\M :: 'a multiset. \ M \# M" haftmann@35268: proof haftmann@35268: fix M :: "'a multiset" haftmann@35268: assume "M \# M" haftmann@35268: then have MM: "(M, M) \ mult {(x, y). x < y}" by (simp add: less_multiset_def) haftmann@35268: have "trans {(x'::'a, x). x' < x}" haftmann@35268: by (rule transI) simp haftmann@35268: moreover note MM haftmann@35268: ultimately have "\I J K. M = I + J \ M = I + K haftmann@35268: \ J \ {#} \ (\k\set_of K. \j\set_of J. (k, j) \ {(x, y). x < y})" haftmann@35268: by (rule mult_implies_one_step) haftmann@35268: then obtain I J K where "M = I + J" and "M = I + K" haftmann@35268: and "J \ {#}" and "(\k\set_of K. \j\set_of J. (k, j) \ {(x, y). x < y})" by blast haftmann@35268: then have aux1: "K \ {#}" and aux2: "\k\set_of K. \j\set_of K. k < j" by auto haftmann@35268: have "finite (set_of K)" by simp haftmann@35268: moreover note aux2 haftmann@35268: ultimately have "set_of K = {}" haftmann@35268: by (induct rule: finite_induct) (auto intro: order_less_trans) haftmann@35268: with aux1 show False by simp haftmann@35268: qed haftmann@35268: have trans: "\K M N :: 'a multiset. K \# M \ M \# N \ K \# N" haftmann@35268: unfolding less_multiset_def mult_def by (blast intro: trancl_trans) wenzelm@46921: show "class.order (le_multiset :: 'a multiset \ _) less_multiset" wenzelm@46921: by default (auto simp add: le_multiset_def irrefl dest: trans) haftmann@35268: qed wenzelm@10249: wenzelm@46730: lemma mult_less_irrefl [elim!]: "M \# (M::'a::order multiset) ==> R" wenzelm@46730: by simp haftmann@26567: wenzelm@10249: wenzelm@10249: subsubsection {* Monotonicity of multiset union *} wenzelm@10249: wenzelm@46730: lemma mult1_union: "(B, D) \ mult1 r ==> (C + B, C + D) \ mult1 r" nipkow@26178: apply (unfold mult1_def) nipkow@26178: apply auto nipkow@26178: apply (rule_tac x = a in exI) nipkow@26178: apply (rule_tac x = "C + M0" in exI) haftmann@57512: apply (simp add: add.assoc) nipkow@26178: done wenzelm@10249: haftmann@35268: lemma union_less_mono2: "B \# D ==> C + B \# C + (D::'a::order multiset)" nipkow@26178: apply (unfold less_multiset_def mult_def) nipkow@26178: apply (erule trancl_induct) noschinl@40249: apply (blast intro: mult1_union) noschinl@40249: apply (blast intro: mult1_union trancl_trans) nipkow@26178: done wenzelm@10249: haftmann@35268: lemma union_less_mono1: "B \# D ==> B + C \# D + (C::'a::order multiset)" haftmann@57512: apply (subst add.commute [of B C]) haftmann@57512: apply (subst add.commute [of D C]) nipkow@26178: apply (erule union_less_mono2) nipkow@26178: done wenzelm@10249: wenzelm@17161: lemma union_less_mono: haftmann@35268: "A \# C ==> B \# D ==> A + B \# C + (D::'a::order multiset)" haftmann@35268: by (blast intro!: union_less_mono1 union_less_mono2 multiset_order.less_trans) wenzelm@10249: haftmann@35268: interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset haftmann@35268: proof haftmann@35268: qed (auto simp add: le_multiset_def intro: union_less_mono2) wenzelm@26145: paulson@15072: krauss@29125: subsection {* Termination proofs with multiset orders *} krauss@29125: krauss@29125: lemma multi_member_skip: "x \# XS \ x \# {# y #} + XS" krauss@29125: and multi_member_this: "x \# {# x #} + XS" krauss@29125: and multi_member_last: "x \# {# x #}" krauss@29125: by auto krauss@29125: krauss@29125: definition "ms_strict = mult pair_less" haftmann@37765: definition "ms_weak = ms_strict \ Id" krauss@29125: krauss@29125: lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)" krauss@29125: unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def krauss@29125: by (auto intro: wf_mult1 wf_trancl simp: mult_def) krauss@29125: krauss@29125: lemma smsI: krauss@29125: "(set_of A, set_of B) \ max_strict \ (Z + A, Z + B) \ ms_strict" krauss@29125: unfolding ms_strict_def krauss@29125: by (rule one_step_implies_mult) (auto simp add: max_strict_def pair_less_def elim!:max_ext.cases) krauss@29125: krauss@29125: lemma wmsI: krauss@29125: "(set_of A, set_of B) \ max_strict \ A = {#} \ B = {#} krauss@29125: \ (Z + A, Z + B) \ ms_weak" krauss@29125: unfolding ms_weak_def ms_strict_def krauss@29125: by (auto simp add: pair_less_def max_strict_def elim!:max_ext.cases intro: one_step_implies_mult) krauss@29125: krauss@29125: inductive pw_leq krauss@29125: where krauss@29125: pw_leq_empty: "pw_leq {#} {#}" krauss@29125: | pw_leq_step: "\(x,y) \ pair_leq; pw_leq X Y \ \ pw_leq ({#x#} + X) ({#y#} + Y)" krauss@29125: krauss@29125: lemma pw_leq_lstep: krauss@29125: "(x, y) \ pair_leq \ pw_leq {#x#} {#y#}" krauss@29125: by (drule pw_leq_step) (rule pw_leq_empty, simp) krauss@29125: krauss@29125: lemma pw_leq_split: krauss@29125: assumes "pw_leq X Y" krauss@29125: shows "\A B Z. X = A + Z \ Y = B + Z \ ((set_of A, set_of B) \ max_strict \ (B = {#} \ A = {#}))" krauss@29125: using assms krauss@29125: proof (induct) krauss@29125: case pw_leq_empty thus ?case by auto krauss@29125: next krauss@29125: case (pw_leq_step x y X Y) krauss@29125: then obtain A B Z where krauss@29125: [simp]: "X = A + Z" "Y = B + Z" krauss@29125: and 1[simp]: "(set_of A, set_of B) \ max_strict \ (B = {#} \ A = {#})" krauss@29125: by auto krauss@29125: from pw_leq_step have "x = y \ (x, y) \ pair_less" krauss@29125: unfolding pair_leq_def by auto krauss@29125: thus ?case krauss@29125: proof krauss@29125: assume [simp]: "x = y" krauss@29125: have krauss@29125: "{#x#} + X = A + ({#y#}+Z) krauss@29125: \ {#y#} + Y = B + ({#y#}+Z) krauss@29125: \ ((set_of A, set_of B) \ max_strict \ (B = {#} \ A = {#}))" krauss@29125: by (auto simp: add_ac) krauss@29125: thus ?case by (intro exI) krauss@29125: next krauss@29125: assume A: "(x, y) \ pair_less" krauss@29125: let ?A' = "{#x#} + A" and ?B' = "{#y#} + B" krauss@29125: have "{#x#} + X = ?A' + Z" krauss@29125: "{#y#} + Y = ?B' + Z" krauss@29125: by (auto simp add: add_ac) krauss@29125: moreover have krauss@29125: "(set_of ?A', set_of ?B') \ max_strict" krauss@29125: using 1 A unfolding max_strict_def krauss@29125: by (auto elim!: max_ext.cases) krauss@29125: ultimately show ?thesis by blast krauss@29125: qed krauss@29125: qed krauss@29125: krauss@29125: lemma krauss@29125: assumes pwleq: "pw_leq Z Z'" krauss@29125: shows ms_strictI: "(set_of A, set_of B) \ max_strict \ (Z + A, Z' + B) \ ms_strict" krauss@29125: and ms_weakI1: "(set_of A, set_of B) \ max_strict \ (Z + A, Z' + B) \ ms_weak" krauss@29125: and ms_weakI2: "(Z + {#}, Z' + {#}) \ ms_weak" krauss@29125: proof - krauss@29125: from pw_leq_split[OF pwleq] krauss@29125: obtain A' B' Z'' krauss@29125: where [simp]: "Z = A' + Z''" "Z' = B' + Z''" krauss@29125: and mx_or_empty: "(set_of A', set_of B') \ max_strict \ (A' = {#} \ B' = {#})" krauss@29125: by blast krauss@29125: { krauss@29125: assume max: "(set_of A, set_of B) \ max_strict" krauss@29125: from mx_or_empty krauss@29125: have "(Z'' + (A + A'), Z'' + (B + B')) \ ms_strict" krauss@29125: proof krauss@29125: assume max': "(set_of A', set_of B') \ max_strict" krauss@29125: with max have "(set_of (A + A'), set_of (B + B')) \ max_strict" krauss@29125: by (auto simp: max_strict_def intro: max_ext_additive) krauss@29125: thus ?thesis by (rule smsI) krauss@29125: next krauss@29125: assume [simp]: "A' = {#} \ B' = {#}" krauss@29125: show ?thesis by (rule smsI) (auto intro: max) krauss@29125: qed krauss@29125: thus "(Z + A, Z' + B) \ ms_strict" by (simp add:add_ac) krauss@29125: thus "(Z + A, Z' + B) \ ms_weak" by (simp add: ms_weak_def) krauss@29125: } krauss@29125: from mx_or_empty krauss@29125: have "(Z'' + A', Z'' + B') \ ms_weak" by (rule wmsI) krauss@29125: thus "(Z + {#}, Z' + {#}) \ ms_weak" by (simp add:add_ac) krauss@29125: qed krauss@29125: nipkow@39301: lemma empty_neutral: "{#} + x = x" "x + {#} = x" krauss@29125: and nonempty_plus: "{# x #} + rs \ {#}" krauss@29125: and nonempty_single: "{# x #} \ {#}" krauss@29125: by auto krauss@29125: krauss@29125: setup {* krauss@29125: let wenzelm@35402: fun msetT T = Type (@{type_name multiset}, [T]); krauss@29125: wenzelm@35402: fun mk_mset T [] = Const (@{const_abbrev Mempty}, msetT T) krauss@29125: | mk_mset T [x] = Const (@{const_name single}, T --> msetT T) $ x krauss@29125: | mk_mset T (x :: xs) = krauss@29125: Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $ krauss@29125: mk_mset T [x] $ mk_mset T xs krauss@29125: krauss@29125: fun mset_member_tac m i = krauss@29125: (if m <= 0 then krauss@29125: rtac @{thm multi_member_this} i ORELSE rtac @{thm multi_member_last} i krauss@29125: else krauss@29125: rtac @{thm multi_member_skip} i THEN mset_member_tac (m - 1) i) krauss@29125: krauss@29125: val mset_nonempty_tac = krauss@29125: rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single} krauss@29125: krauss@29125: val regroup_munion_conv = wenzelm@35402: Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus} nipkow@39301: (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_neutral})) krauss@29125: krauss@29125: fun unfold_pwleq_tac i = krauss@29125: (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st)) krauss@29125: ORELSE (rtac @{thm pw_leq_lstep} i) krauss@29125: ORELSE (rtac @{thm pw_leq_empty} i) krauss@29125: krauss@29125: val set_of_simps = [@{thm set_of_empty}, @{thm set_of_single}, @{thm set_of_union}, krauss@29125: @{thm Un_insert_left}, @{thm Un_empty_left}] krauss@29125: in krauss@29125: ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset krauss@29125: { krauss@29125: msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv, krauss@29125: mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac, krauss@29125: mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps, wenzelm@30595: smsI'= @{thm ms_strictI}, wmsI2''= @{thm ms_weakI2}, wmsI1= @{thm ms_weakI1}, wenzelm@30595: reduction_pair= @{thm ms_reduction_pair} krauss@29125: }) wenzelm@10249: end krauss@29125: *} krauss@29125: haftmann@34943: haftmann@34943: subsection {* Legacy theorem bindings *} haftmann@34943: nipkow@39302: lemmas multi_count_eq = multiset_eq_iff [symmetric] haftmann@34943: haftmann@34943: lemma union_commute: "M + N = N + (M::'a multiset)" haftmann@57512: by (fact add.commute) haftmann@34943: haftmann@34943: lemma union_assoc: "(M + N) + K = M + (N + (K::'a multiset))" haftmann@57512: by (fact add.assoc) haftmann@34943: haftmann@34943: lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))" haftmann@57512: by (fact add.left_commute) haftmann@34943: haftmann@34943: lemmas union_ac = union_assoc union_commute union_lcomm haftmann@34943: haftmann@34943: lemma union_right_cancel: "M + K = N + K \ M = (N::'a multiset)" haftmann@34943: by (fact add_right_cancel) haftmann@34943: haftmann@34943: lemma union_left_cancel: "K + M = K + N \ M = (N::'a multiset)" haftmann@34943: by (fact add_left_cancel) haftmann@34943: haftmann@34943: lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \ X = Y" haftmann@34943: by (fact add_imp_eq) haftmann@34943: haftmann@35268: lemma mset_less_trans: "(M::'a multiset) < K \ K < N \ M < N" haftmann@35268: by (fact order_less_trans) haftmann@35268: haftmann@35268: lemma multiset_inter_commute: "A #\ B = B #\ A" haftmann@35268: by (fact inf.commute) haftmann@35268: haftmann@35268: lemma multiset_inter_assoc: "A #\ (B #\ C) = A #\ B #\ C" haftmann@35268: by (fact inf.assoc [symmetric]) haftmann@35268: haftmann@35268: lemma multiset_inter_left_commute: "A #\ (B #\ C) = B #\ (A #\ C)" haftmann@35268: by (fact inf.left_commute) haftmann@35268: haftmann@35268: lemmas multiset_inter_ac = haftmann@35268: multiset_inter_commute haftmann@35268: multiset_inter_assoc haftmann@35268: multiset_inter_left_commute haftmann@35268: haftmann@35268: lemma mult_less_not_refl: haftmann@35268: "\ M \# (M::'a::order multiset)" haftmann@35268: by (fact multiset_order.less_irrefl) haftmann@35268: haftmann@35268: lemma mult_less_trans: haftmann@35268: "K \# M ==> M \# N ==> K \# (N::'a::order multiset)" haftmann@35268: by (fact multiset_order.less_trans) haftmann@35268: haftmann@35268: lemma mult_less_not_sym: haftmann@35268: "M \# N ==> \ N \# (M::'a::order multiset)" haftmann@35268: by (fact multiset_order.less_not_sym) haftmann@35268: haftmann@35268: lemma mult_less_asym: haftmann@35268: "M \# N ==> (\ P ==> N \# (M::'a::order multiset)) ==> P" haftmann@35268: by (fact multiset_order.less_asym) haftmann@34943: blanchet@35712: ML {* blanchet@35712: fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T])) blanchet@35712: (Const _ $ t') = blanchet@35712: let blanchet@35712: val (maybe_opt, ps) = blanchet@35712: Nitpick_Model.dest_plain_fun t' ||> op ~~ blanchet@35712: ||> map (apsnd (snd o HOLogic.dest_number)) blanchet@35712: fun elems_for t = blanchet@35712: case AList.lookup (op =) ps t of blanchet@35712: SOME n => replicate n t blanchet@35712: | NONE => [Const (maybe_name, elem_T --> elem_T) $ t] blanchet@35712: in blanchet@35712: case maps elems_for (all_values elem_T) @ blanchet@37261: (if maybe_opt then [Const (Nitpick_Model.unrep (), elem_T)] blanchet@37261: else []) of blanchet@35712: [] => Const (@{const_name zero_class.zero}, T) blanchet@35712: | ts => foldl1 (fn (t1, t2) => blanchet@35712: Const (@{const_name plus_class.plus}, T --> T --> T) blanchet@35712: $ t1 $ t2) blanchet@35712: (map (curry (op $) (Const (@{const_name single}, blanchet@35712: elem_T --> T))) ts) blanchet@35712: end blanchet@35712: | multiset_postproc _ _ _ _ t = t blanchet@35712: *} blanchet@35712: blanchet@38287: declaration {* blanchet@38287: Nitpick_Model.register_term_postprocessor @{typ "'a multiset"} blanchet@38242: multiset_postproc blanchet@35712: *} blanchet@35712: haftmann@49822: hide_const (open) fold haftmann@49822: haftmann@51600: haftmann@51600: subsection {* Naive implementation using lists *} haftmann@51600: haftmann@51600: code_datatype multiset_of haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "{#} = multiset_of []" haftmann@51600: by simp haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "{#x#} = multiset_of [x]" haftmann@51600: by simp haftmann@51600: haftmann@51600: lemma union_code [code]: haftmann@51600: "multiset_of xs + multiset_of ys = multiset_of (xs @ ys)" haftmann@51600: by simp haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "image_mset f (multiset_of xs) = multiset_of (map f xs)" haftmann@51600: by (simp add: multiset_of_map) haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "Multiset.filter f (multiset_of xs) = multiset_of (filter f xs)" haftmann@51600: by (simp add: multiset_of_filter) haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "multiset_of xs - multiset_of ys = multiset_of (fold remove1 ys xs)" haftmann@51600: by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute) haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "multiset_of xs #\ multiset_of ys = haftmann@51600: multiset_of (snd (fold (\x (ys, zs). haftmann@51600: if x \ set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, [])))" haftmann@51600: proof - haftmann@51600: have "\zs. multiset_of (snd (fold (\x (ys, zs). haftmann@51600: if x \ set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, zs))) = haftmann@51600: (multiset_of xs #\ multiset_of ys) + multiset_of zs" haftmann@51623: by (induct xs arbitrary: ys) haftmann@51623: (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps) haftmann@51623: then show ?thesis by simp haftmann@51623: qed haftmann@51623: haftmann@51623: lemma [code]: haftmann@51623: "multiset_of xs #\ multiset_of ys = haftmann@51623: multiset_of (split append (fold (\x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))" haftmann@51623: proof - haftmann@51623: have "\zs. multiset_of (split append (fold (\x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) = haftmann@51623: (multiset_of xs #\ multiset_of ys) + multiset_of zs" haftmann@51623: by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff) haftmann@51600: then show ?thesis by simp haftmann@51600: qed haftmann@51600: haftmann@51600: lemma [code_unfold]: haftmann@51600: "x \# multiset_of xs \ x \ set xs" haftmann@51600: by (simp add: in_multiset_of) haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "count (multiset_of xs) x = fold (\y. if x = y then Suc else id) xs 0" haftmann@51600: proof - haftmann@51600: have "\n. fold (\y. if x = y then Suc else id) xs n = count (multiset_of xs) x + n" haftmann@51600: by (induct xs) simp_all haftmann@51600: then show ?thesis by simp haftmann@51600: qed haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "set_of (multiset_of xs) = set xs" haftmann@51600: by simp haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "sorted_list_of_multiset (multiset_of xs) = sort xs" haftmann@51600: by (induct xs) simp_all haftmann@51600: haftmann@51600: lemma [code]: -- {* not very efficient, but representation-ignorant! *} haftmann@51600: "multiset_of_set A = multiset_of (sorted_list_of_set A)" haftmann@51600: apply (cases "finite A") haftmann@51600: apply simp_all haftmann@51600: apply (induct A rule: finite_induct) haftmann@51600: apply (simp_all add: union_commute) haftmann@51600: done haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "mcard (multiset_of xs) = length xs" haftmann@51600: by (simp add: mcard_multiset_of) haftmann@51600: nipkow@55808: fun ms_lesseq_impl :: "'a list \ 'a list \ bool option" where nipkow@55808: "ms_lesseq_impl [] ys = Some (ys \ [])" nipkow@55808: | "ms_lesseq_impl (Cons x xs) ys = (case List.extract (op = x) ys of nipkow@55808: None \ None nipkow@55808: | Some (ys1,_,ys2) \ ms_lesseq_impl xs (ys1 @ ys2))" nipkow@55808: nipkow@55808: lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \ \ multiset_of xs \ multiset_of ys) \ nipkow@55808: (ms_lesseq_impl xs ys = Some True \ multiset_of xs < multiset_of ys) \ nipkow@55808: (ms_lesseq_impl xs ys = Some False \ multiset_of xs = multiset_of ys)" nipkow@55808: proof (induct xs arbitrary: ys) nipkow@55808: case (Nil ys) nipkow@55808: show ?case by (auto simp: mset_less_empty_nonempty) nipkow@55808: next nipkow@55808: case (Cons x xs ys) nipkow@55808: show ?case nipkow@55808: proof (cases "List.extract (op = x) ys") nipkow@55808: case None nipkow@55808: hence x: "x \ set ys" by (simp add: extract_None_iff) nipkow@55808: { nipkow@55808: assume "multiset_of (x # xs) \ multiset_of ys" nipkow@55808: from set_of_mono[OF this] x have False by simp nipkow@55808: } note nle = this nipkow@55808: moreover nipkow@55808: { nipkow@55808: assume "multiset_of (x # xs) < multiset_of ys" nipkow@55808: hence "multiset_of (x # xs) \ multiset_of ys" by auto nipkow@55808: from nle[OF this] have False . nipkow@55808: } nipkow@55808: ultimately show ?thesis using None by auto nipkow@55808: next nipkow@55808: case (Some res) nipkow@55808: obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto) nipkow@55808: note Some = Some[unfolded res] nipkow@55808: from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp nipkow@55808: hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}" nipkow@55808: by (auto simp: ac_simps) nipkow@55808: show ?thesis unfolding ms_lesseq_impl.simps nipkow@55808: unfolding Some option.simps split nipkow@55808: unfolding id nipkow@55808: using Cons[of "ys1 @ ys2"] nipkow@55808: unfolding mset_le_def mset_less_def by auto nipkow@55808: qed nipkow@55808: qed nipkow@55808: nipkow@55808: lemma [code]: "multiset_of xs \ multiset_of ys \ ms_lesseq_impl xs ys \ None" nipkow@55808: using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto) nipkow@55808: nipkow@55808: lemma [code]: "multiset_of xs < multiset_of ys \ ms_lesseq_impl xs ys = Some True" nipkow@55808: using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto) haftmann@51600: haftmann@51600: instantiation multiset :: (equal) equal haftmann@51600: begin haftmann@51600: haftmann@51600: definition nipkow@55808: [code del]: "HOL.equal A (B :: 'a multiset) \ A = B" nipkow@55808: lemma [code]: "HOL.equal (multiset_of xs) (multiset_of ys) \ ms_lesseq_impl xs ys = Some False" nipkow@55808: unfolding equal_multiset_def nipkow@55808: using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto) haftmann@51600: haftmann@51600: instance nipkow@55808: by default (simp add: equal_multiset_def) blanchet@37169: end haftmann@49388: haftmann@51600: lemma [code]: haftmann@51600: "msetsum (multiset_of xs) = listsum xs" haftmann@51600: by (induct xs) (simp_all add: add.commute) haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "msetprod (multiset_of xs) = fold times xs 1" haftmann@51600: proof - haftmann@51600: have "\x. fold times xs x = msetprod (multiset_of xs) * x" haftmann@51600: by (induct xs) (simp_all add: mult.assoc) haftmann@51600: then show ?thesis by simp haftmann@51600: qed haftmann@51600: haftmann@51600: lemma [code]: haftmann@51600: "size = mcard" haftmann@51600: by (fact size_eq_mcard) haftmann@51600: haftmann@51600: text {* haftmann@51600: Exercise for the casual reader: add implementations for @{const le_multiset} haftmann@51600: and @{const less_multiset} (multiset order). haftmann@51600: *} haftmann@51600: haftmann@51600: text {* Quickcheck generators *} haftmann@51600: haftmann@51600: definition (in term_syntax) haftmann@51600: msetify :: "'a\typerep list \ (unit \ Code_Evaluation.term) haftmann@51600: \ 'a multiset \ (unit \ Code_Evaluation.term)" where haftmann@51600: [code_unfold]: "msetify xs = Code_Evaluation.valtermify multiset_of {\} xs" haftmann@51600: haftmann@51600: notation fcomp (infixl "\>" 60) haftmann@51600: notation scomp (infixl "\\" 60) haftmann@51600: haftmann@51600: instantiation multiset :: (random) random haftmann@51600: begin haftmann@51600: haftmann@51600: definition haftmann@51600: "Quickcheck_Random.random i = Quickcheck_Random.random i \\ (\xs. Pair (msetify xs))" haftmann@51600: haftmann@51600: instance .. haftmann@51600: haftmann@51600: end haftmann@51600: haftmann@51600: no_notation fcomp (infixl "\>" 60) haftmann@51600: no_notation scomp (infixl "\\" 60) haftmann@51600: haftmann@51600: instantiation multiset :: (full_exhaustive) full_exhaustive haftmann@51600: begin haftmann@51600: haftmann@51600: definition full_exhaustive_multiset :: "('a multiset \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option" haftmann@51600: where haftmann@51600: "full_exhaustive_multiset f i = Quickcheck_Exhaustive.full_exhaustive (\xs. f (msetify xs)) i" haftmann@51600: haftmann@51600: instance .. haftmann@51600: haftmann@51600: end haftmann@51600: haftmann@51600: hide_const (open) msetify haftmann@51600: blanchet@55129: blanchet@55129: subsection {* BNF setup *} blanchet@55129: blanchet@55129: lemma setsum_gt_0_iff: blanchet@55129: fixes f :: "'a \ nat" assumes "finite A" blanchet@55129: shows "setsum f A > 0 \ (\ a \ A. f a > 0)" blanchet@55129: (is "?L \ ?R") blanchet@55129: proof- blanchet@55129: have "?L \ \ setsum f A = 0" by fast blanchet@55129: also have "... \ (\ a \ A. f a \ 0)" using assms by simp blanchet@55129: also have "... \ ?R" by simp blanchet@55129: finally show ?thesis . blanchet@55129: qed blanchet@55129: blanchet@55129: lift_definition mmap :: "('a \ 'b) \ 'a multiset \ 'b multiset" is blanchet@55129: "\h f b. setsum f {a. h a = b \ f a > 0} :: nat" blanchet@55129: unfolding multiset_def proof safe blanchet@55129: fix h :: "'a \ 'b" and f :: "'a \ nat" blanchet@55129: assume fin: "finite {a. 0 < f a}" (is "finite ?A") blanchet@55129: show "finite {b. 0 < setsum f {a. h a = b \ 0 < f a}}" blanchet@55129: (is "finite {b. 0 < setsum f (?As b)}") blanchet@55129: proof- let ?B = "{b. 0 < setsum f (?As b)}" blanchet@55129: have "\ b. finite (?As b)" using fin by simp blanchet@55129: hence B: "?B = {b. ?As b \ {}}" by (auto simp add: setsum_gt_0_iff) blanchet@55129: hence "?B \ h ` ?A" by auto blanchet@55129: thus ?thesis using finite_surj[OF fin] by auto blanchet@55129: qed blanchet@55129: qed blanchet@55129: blanchet@55129: lemma mmap_id0: "mmap id = id" blanchet@55129: proof (intro ext multiset_eqI) blanchet@55129: fix f a show "count (mmap id f) a = count (id f) a" blanchet@55129: proof (cases "count f a = 0") blanchet@55129: case False blanchet@55129: hence 1: "{aa. aa = a \ aa \# f} = {a}" by auto blanchet@55129: thus ?thesis by transfer auto blanchet@55129: qed (transfer, simp) blanchet@55129: qed blanchet@55129: blanchet@55129: lemma inj_on_setsum_inv: blanchet@55129: assumes 1: "(0::nat) < setsum (count f) {a. h a = b' \ a \# f}" (is "0 < setsum (count f) ?A'") blanchet@55129: and 2: "{a. h a = b \ a \# f} = {a. h a = b' \ a \# f}" (is "?A = ?A'") blanchet@55129: shows "b = b'" blanchet@55129: using assms by (auto simp add: setsum_gt_0_iff) blanchet@55129: blanchet@55129: lemma mmap_comp: blanchet@55129: fixes h1 :: "'a \ 'b" and h2 :: "'b \ 'c" blanchet@55129: shows "mmap (h2 o h1) = mmap h2 o mmap h1" blanchet@55129: proof (intro ext multiset_eqI) blanchet@55129: fix f :: "'a multiset" fix c :: 'c blanchet@55129: let ?A = "{a. h2 (h1 a) = c \ a \# f}" blanchet@55129: let ?As = "\ b. {a. h1 a = b \ a \# f}" blanchet@55129: let ?B = "{b. h2 b = c \ 0 < setsum (count f) (?As b)}" blanchet@55129: have 0: "{?As b | b. b \ ?B} = ?As ` ?B" by auto blanchet@55129: have "\ b. finite (?As b)" by transfer (simp add: multiset_def) blanchet@55129: hence "?B = {b. h2 b = c \ ?As b \ {}}" by (auto simp add: setsum_gt_0_iff) blanchet@55129: hence A: "?A = \ {?As b | b. b \ ?B}" by auto blanchet@55129: have "setsum (count f) ?A = setsum (setsum (count f)) {?As b | b. b \ ?B}" haftmann@57418: unfolding A by transfer (intro setsum.Union_disjoint [simplified], auto simp: multiset_def setsum.Union_disjoint) blanchet@55129: also have "... = setsum (setsum (count f)) (?As ` ?B)" unfolding 0 .. blanchet@55129: also have "... = setsum (setsum (count f) o ?As) ?B" haftmann@57418: by (intro setsum.reindex) (auto simp add: setsum_gt_0_iff inj_on_def) blanchet@55129: also have "... = setsum (\ b. setsum (count f) (?As b)) ?B" unfolding comp_def .. blanchet@55129: finally have "setsum (count f) ?A = setsum (\ b. setsum (count f) (?As b)) ?B" . blanchet@55129: thus "count (mmap (h2 \ h1) f) c = count ((mmap h2 \ mmap h1) f) c" blanchet@55129: by transfer (unfold comp_apply, blast) blanchet@55129: qed blanchet@55129: blanchet@55129: lemma mmap_cong: blanchet@55129: assumes "\a. a \# M \ f a = g a" blanchet@55129: shows "mmap f M = mmap g M" haftmann@57418: using assms by transfer (auto intro!: setsum.cong) blanchet@55129: blanchet@55129: context blanchet@55129: begin blanchet@55129: interpretation lifting_syntax . blanchet@55129: blanchet@55129: lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\f. {a. 0 < f a}) set_of" blanchet@55945: unfolding set_of_def pcr_multiset_def cr_multiset_def rel_fun_def by auto blanchet@55129: haftmann@51600: end haftmann@51600: blanchet@55129: lemma set_of_mmap: "set_of o mmap h = image h o set_of" blanchet@55129: proof (rule ext, unfold comp_apply) blanchet@55129: fix M show "set_of (mmap h M) = h ` set_of M" blanchet@55129: by transfer (auto simp add: multiset_def setsum_gt_0_iff) blanchet@55129: qed blanchet@55129: blanchet@55129: lemma multiset_of_surj: blanchet@55129: "multiset_of ` {as. set as \ A} = {M. set_of M \ A}" blanchet@55129: proof safe blanchet@55129: fix M assume M: "set_of M \ A" blanchet@55129: obtain as where eq: "M = multiset_of as" using surj_multiset_of unfolding surj_def by auto blanchet@55129: hence "set as \ A" using M by auto blanchet@55129: thus "M \ multiset_of ` {as. set as \ A}" using eq by auto blanchet@55129: next blanchet@55129: show "\x xa xb. \set xa \ A; xb \ set_of (multiset_of xa)\ \ xb \ A" blanchet@55129: by (erule set_mp) (unfold set_of_multiset_of) blanchet@55129: qed blanchet@55129: blanchet@55129: lemma card_of_set_of: blanchet@55129: "(card_of {M. set_of M \ A}, card_of {as. set as \ A}) \ ordLeq" traytel@55811: apply(rule surj_imp_ordLeq[of _ multiset_of]) using multiset_of_surj by auto blanchet@55129: blanchet@55129: lemma nat_sum_induct: blanchet@55129: assumes "\n1 n2. (\ m1 m2. m1 + m2 < n1 + n2 \ phi m1 m2) \ phi n1 n2" blanchet@55129: shows "phi (n1::nat) (n2::nat)" blanchet@55129: proof- blanchet@55129: let ?chi = "\ n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)" blanchet@55129: have "?chi (n1,n2)" blanchet@55129: apply(induct rule: measure_induct[of "\ n1n2. fst n1n2 + snd n1n2" ?chi]) blanchet@55129: using assms by (metis fstI sndI) blanchet@55129: thus ?thesis by simp blanchet@55129: qed blanchet@55129: blanchet@55129: lemma matrix_count: blanchet@55129: fixes ct1 ct2 :: "nat \ nat" blanchet@55129: assumes "setsum ct1 {.. ct. (\ i1 \ n1. setsum (\ i2. ct i1 i2) {.. blanchet@55129: (\ i2 \ n2. setsum (\ i1. ct i1 i2) {.. ct1 ct2 :: nat \ nat. blanchet@55129: setsum ct1 {.. ?phi ct1 ct2 n1 n2" blanchet@55129: proof(induct rule: nat_sum_induct[of blanchet@55129: "\ n1 n2. \ ct1 ct2 :: nat \ nat. blanchet@55129: setsum ct1 {.. ?phi ct1 ct2 n1 n2"], blanchet@55129: clarify) blanchet@55129: fix n1 n2 :: nat and ct1 ct2 :: "nat \ nat" blanchet@55129: assume IH: "\ m1 m2. m1 + m2 < n1 + n2 \ blanchet@55129: \ dt1 dt2 :: nat \ nat. blanchet@55129: setsum dt1 {.. ?phi dt1 dt2 m1 m2" blanchet@55129: and ss: "setsum ct1 {.. ct2 n2") blanchet@55129: case True blanchet@55129: def dt2 \ "\ i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2" blanchet@55129: have "setsum ct1 {.. i1. i1 \ m1 \ setsum (\ i2. dt i1 i2) {.. i2. i2 \ n2 \ setsum (\ i1. dt i1 i2) {.. "\ i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1" blanchet@55129: have "setsum dt1 {.. i1. i1 \ n1 \ setsum (\ i2. dt i1 i2) {.. i2. i2 \ m2 \ setsum (\ i1. dt i1 i2) {.. blanchet@55129: \ b1 b1' b2 b2'. {b1,b1'} \ B1 \ {b2,b2'} \ B2 \ u b1 b2 = u b1' b2' blanchet@55129: \ b1 = b1' \ b2 = b2'" blanchet@55129: blanchet@55129: lemma matrix_setsum_finite: blanchet@55129: assumes B1: "B1 \ {}" "finite B1" and B2: "B2 \ {}" "finite B2" and u: "inj2 u B1 B2" blanchet@55129: and ss: "setsum N1 B1 = setsum N2 B2" blanchet@55129: shows "\ M :: 'a \ nat. blanchet@55129: (\ b1 \ B1. setsum (\ b2. M (u b1 b2)) B2 = N1 b1) \ blanchet@55129: (\ b2 \ B2. setsum (\ b1. M (u b1 b2)) B1 = N2 b2)" blanchet@55129: proof- blanchet@55129: obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps) blanchet@55129: then obtain e1 where e1: "bij_betw e1 {.. "inv_into {.. i1. i1 < Suc n1 \ f1 (e1 i1) = i1" blanchet@55129: and e1f1[simp]: "\ b1. b1 \ B1 \ e1 (f1 b1) = b1" unfolding f1_def blanchet@55129: apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff) blanchet@55129: by (metis e1_surj f_inv_into_f) blanchet@55129: (* *) blanchet@55129: obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps) blanchet@55129: then obtain e2 where e2: "bij_betw e2 {.. "inv_into {.. i2. i2 < Suc n2 \ f2 (e2 i2) = i2" blanchet@55129: and e2f2[simp]: "\ b2. b2 \ B2 \ e2 (f2 b2) = b2" unfolding f2_def blanchet@55129: apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff) blanchet@55129: by (metis e2_surj f_inv_into_f) blanchet@55129: (* *) blanchet@55129: let ?ct1 = "N1 o e1" let ?ct2 = "N2 o e2" blanchet@55129: have ss: "setsum ?ct1 {.. i1. i1 \ n1 \ setsum (\ i2. ct i1 i2) {.. i2. i2 \ n2 \ setsum (\ i1. ct i1 i2) {.. "{u b1 b2 | b1 b2. b1 \ B1 \ b2 \ B2}" blanchet@55129: have "\ a \ A. \ b1b2 \ B1 <*> B2. u (fst b1b2) (snd b1b2) = a" blanchet@55129: unfolding A_def Ball_def mem_Collect_eq by auto blanchet@55129: then obtain h1h2 where h12: blanchet@55129: "\a. a \ A \ u (fst (h1h2 a)) (snd (h1h2 a)) = a \ h1h2 a \ B1 <*> B2" by metis blanchet@55129: def h1 \ "fst o h1h2" def h2 \ "snd o h1h2" blanchet@55129: have h12[simp]: "\a. a \ A \ u (h1 a) (h2 a) = a" blanchet@55129: "\ a. a \ A \ h1 a \ B1" "\ a. a \ A \ h2 a \ B2" blanchet@55129: using h12 unfolding h1_def h2_def by force+ blanchet@55129: {fix b1 b2 assume b1: "b1 \ B1" and b2: "b2 \ B2" blanchet@55129: hence inA: "u b1 b2 \ A" unfolding A_def by auto blanchet@55129: hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto blanchet@55129: moreover have "h1 (u b1 b2) \ B1" "h2 (u b1 b2) \ B2" using inA by auto blanchet@55129: ultimately have "h1 (u b1 b2) = b1 \ h2 (u b1 b2) = b2" blanchet@55129: using u b1 b2 unfolding inj2_def by fastforce blanchet@55129: } blanchet@55129: hence h1[simp]: "\ b1 b2. \b1 \ B1; b2 \ B2\ \ h1 (u b1 b2) = b1" and blanchet@55129: h2[simp]: "\ b1 b2. \b1 \ B1; b2 \ B2\ \ h2 (u b1 b2) = b2" by auto blanchet@55129: def M \ "\ a. ct (f1 (h1 a)) (f2 (h2 a))" blanchet@55129: show ?thesis blanchet@55129: apply(rule exI[of _ M]) proof safe blanchet@55129: fix b1 assume b1: "b1 \ B1" blanchet@55129: hence f1b1: "f1 b1 \ n1" using f1 unfolding bij_betw_def blanchet@55129: by (metis image_eqI lessThan_iff less_Suc_eq_le) blanchet@55129: have "(\b2\B2. M (u b1 b2)) = (\i2b2\B2. M (u b1 b2)) = N1 b1" . blanchet@55129: next blanchet@55129: fix b2 assume b2: "b2 \ B2" blanchet@55129: hence f2b2: "f2 b2 \ n2" using f2 unfolding bij_betw_def blanchet@55129: by (metis image_eqI lessThan_iff less_Suc_eq_le) blanchet@55129: have "(\b1\B1. M (u b1 b2)) = (\i1b1\B1. M (u b1 b2)) = N2 b2" . blanchet@55129: qed blanchet@55129: qed blanchet@55129: blanchet@55129: lemma supp_vimage_mmap: "set_of M \ f -` (set_of (mmap f M))" blanchet@55129: by transfer (auto simp: multiset_def setsum_gt_0_iff) blanchet@55129: blanchet@55129: lemma mmap_ge_0: "b \# mmap f M \ (\a. a \# M \ f a = b)" blanchet@55129: by transfer (auto simp: multiset_def setsum_gt_0_iff) blanchet@55129: blanchet@55129: lemma finite_twosets: blanchet@55129: assumes "finite B1" and "finite B2" blanchet@55129: shows "finite {u b1 b2 |b1 b2. b1 \ B1 \ b2 \ B2}" (is "finite ?A") blanchet@55129: proof- blanchet@55129: have A: "?A = (\ b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force blanchet@55129: show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto blanchet@55129: qed blanchet@55129: blanchet@55129: (* Weak pullbacks: *) blanchet@55129: definition wpull where blanchet@55129: "wpull A B1 B2 f1 f2 p1 p2 \ blanchet@55129: (\ b1 b2. b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2 \ (\ a \ A. p1 a = b1 \ p2 a = b2))" blanchet@55129: blanchet@55129: (* Weak pseudo-pullbacks *) blanchet@55129: definition wppull where blanchet@55129: "wppull A B1 B2 f1 f2 e1 e2 p1 p2 \ blanchet@55129: (\ b1 b2. b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2 \ blanchet@55129: (\ a \ A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2))" blanchet@55129: blanchet@55129: blanchet@55129: (* The pullback of sets *) blanchet@55129: definition thePull where blanchet@55129: "thePull B1 B2 f1 f2 = {(b1,b2). b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2}" blanchet@55129: blanchet@55129: lemma wpull_thePull: blanchet@55129: "wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd" blanchet@55129: unfolding wpull_def thePull_def by auto blanchet@55129: blanchet@55129: lemma wppull_thePull: blanchet@55129: assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" blanchet@55129: shows blanchet@55129: "\ j. \ a' \ thePull B1 B2 f1 f2. blanchet@55129: j a' \ A \ blanchet@55129: e1 (p1 (j a')) = e1 (fst a') \ e2 (p2 (j a')) = e2 (snd a')" blanchet@55129: (is "\ j. \ a' \ ?A'. ?phi a' (j a')") blanchet@55129: proof(rule bchoice[of ?A' ?phi], default) blanchet@55129: fix a' assume a': "a' \ ?A'" blanchet@55129: hence "fst a' \ B1" unfolding thePull_def by auto blanchet@55129: moreover blanchet@55129: from a' have "snd a' \ B2" unfolding thePull_def by auto blanchet@55129: moreover have "f1 (fst a') = f2 (snd a')" blanchet@55129: using a' unfolding csquare_def thePull_def by auto blanchet@55129: ultimately show "\ ja'. ?phi a' ja'" blanchet@55129: using assms unfolding wppull_def by blast blanchet@55129: qed blanchet@55129: blanchet@55129: lemma wpull_wppull: blanchet@55129: assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and blanchet@55129: 1: "\ a' \ A'. j a' \ A \ e1 (p1 (j a')) = e1 (p1' a') \ e2 (p2 (j a')) = e2 (p2' a')" blanchet@55129: shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2" blanchet@55129: unfolding wppull_def proof safe blanchet@55129: fix b1 b2 blanchet@55129: assume b1: "b1 \ B1" and b2: "b2 \ B2" and f: "f1 b1 = f2 b2" blanchet@55129: then obtain a' where a': "a' \ A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'" blanchet@55129: using wp unfolding wpull_def by blast blanchet@55129: show "\a\A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2" blanchet@55129: apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto blanchet@55129: qed blanchet@55129: blanchet@55129: lemma wppull_fstOp_sndOp: blanchet@55129: shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q)) blanchet@55129: snd fst fst snd (BNF_Def.fstOp P Q) (BNF_Def.sndOp P Q)" blanchet@55129: using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto blanchet@55129: blanchet@55129: lemma wpull_mmap: blanchet@55129: fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set" blanchet@55129: assumes wp: "wpull A B1 B2 f1 f2 p1 p2" blanchet@55129: shows blanchet@55129: "wpull {M. set_of M \ A} blanchet@55129: {N1. set_of N1 \ B1} {N2. set_of N2 \ B2} blanchet@55129: (mmap f1) (mmap f2) (mmap p1) (mmap p2)" blanchet@55129: unfolding wpull_def proof (safe, unfold Bex_def mem_Collect_eq) blanchet@55129: fix N1 :: "'b1 multiset" and N2 :: "'b2 multiset" blanchet@55129: assume mmap': "mmap f1 N1 = mmap f2 N2" blanchet@55129: and N1[simp]: "set_of N1 \ B1" blanchet@55129: and N2[simp]: "set_of N2 \ B2" blanchet@55129: def P \ "mmap f1 N1" blanchet@55129: have P1: "P = mmap f1 N1" and P2: "P = mmap f2 N2" unfolding P_def using mmap' by auto blanchet@55129: note P = P1 P2 blanchet@55129: have fin_N1[simp]: "finite (set_of N1)" blanchet@55129: and fin_N2[simp]: "finite (set_of N2)" blanchet@55129: and fin_P[simp]: "finite (set_of P)" by auto blanchet@55129: blanchet@55129: def set1 \ "\ c. {b1 \ set_of N1. f1 b1 = c}" blanchet@55129: have set1[simp]: "\ c b1. b1 \ set1 c \ f1 b1 = c" unfolding set1_def by auto blanchet@55129: have fin_set1: "\ c. c \ set_of P \ finite (set1 c)" blanchet@55129: using N1(1) unfolding set1_def multiset_def by auto blanchet@55129: have set1_NE: "\ c. c \ set_of P \ set1 c \ {}" blanchet@55129: unfolding set1_def set_of_def P mmap_ge_0 by auto blanchet@55129: have supp_N1_set1: "set_of N1 = (\ c \ set_of P. set1 c)" blanchet@55129: using supp_vimage_mmap[of N1 f1] unfolding set1_def P1 by auto blanchet@55129: hence set1_inclN1: "\c. c \ set_of P \ set1 c \ set_of N1" by auto blanchet@55129: hence set1_incl: "\ c. c \ set_of P \ set1 c \ B1" using N1 by blast blanchet@55129: have set1_disj: "\ c c'. c \ c' \ set1 c \ set1 c' = {}" blanchet@55129: unfolding set1_def by auto blanchet@55129: have setsum_set1: "\ c. setsum (count N1) (set1 c) = count P c" haftmann@57418: unfolding P1 set1_def by transfer (auto intro: setsum.cong) blanchet@55129: blanchet@55129: def set2 \ "\ c. {b2 \ set_of N2. f2 b2 = c}" blanchet@55129: have set2[simp]: "\ c b2. b2 \ set2 c \ f2 b2 = c" unfolding set2_def by auto blanchet@55129: have fin_set2: "\ c. c \ set_of P \ finite (set2 c)" blanchet@55129: using N2(1) unfolding set2_def multiset_def by auto blanchet@55129: have set2_NE: "\ c. c \ set_of P \ set2 c \ {}" blanchet@55129: unfolding set2_def P2 mmap_ge_0 set_of_def by auto blanchet@55129: have supp_N2_set2: "set_of N2 = (\ c \ set_of P. set2 c)" blanchet@55129: using supp_vimage_mmap[of N2 f2] unfolding set2_def P2 by auto blanchet@55129: hence set2_inclN2: "\c. c \ set_of P \ set2 c \ set_of N2" by auto blanchet@55129: hence set2_incl: "\ c. c \ set_of P \ set2 c \ B2" using N2 by blast blanchet@55129: have set2_disj: "\ c c'. c \ c' \ set2 c \ set2 c' = {}" blanchet@55129: unfolding set2_def by auto blanchet@55129: have setsum_set2: "\ c. setsum (count N2) (set2 c) = count P c" haftmann@57418: unfolding P2 set2_def by transfer (auto intro: setsum.cong) blanchet@55129: blanchet@55129: have ss: "\ c. c \ set_of P \ setsum (count N1) (set1 c) = setsum (count N2) (set2 c)" blanchet@55129: unfolding setsum_set1 setsum_set2 .. blanchet@55129: have "\ c \ set_of P. \ b1b2 \ (set1 c) \ (set2 c). blanchet@55129: \ a \ A. p1 a = fst b1b2 \ p2 a = snd b1b2" blanchet@55129: using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq blanchet@55129: by simp (metis set1 set2 set_rev_mp) blanchet@55129: then obtain uu where uu: blanchet@55129: "\ c \ set_of P. \ b1b2 \ (set1 c) \ (set2 c). blanchet@55129: uu c b1b2 \ A \ p1 (uu c b1b2) = fst b1b2 \ p2 (uu c b1b2) = snd b1b2" by metis blanchet@55129: def u \ "\ c b1 b2. uu c (b1,b2)" blanchet@55129: have u[simp]: blanchet@55129: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ u c b1 b2 \ A" blanchet@55129: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ p1 (u c b1 b2) = b1" blanchet@55129: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ p2 (u c b1 b2) = b2" blanchet@55129: using uu unfolding u_def by auto blanchet@55129: {fix c assume c: "c \ set_of P" blanchet@55129: have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify blanchet@55129: fix b1 b1' b2 b2' blanchet@55129: assume "{b1, b1'} \ set1 c" "{b2, b2'} \ set2 c" and 0: "u c b1 b2 = u c b1' b2'" blanchet@55129: hence "p1 (u c b1 b2) = b1 \ p2 (u c b1 b2) = b2 \ blanchet@55129: p1 (u c b1' b2') = b1' \ p2 (u c b1' b2') = b2'" blanchet@55129: using u(2)[OF c] u(3)[OF c] by simp metis blanchet@55129: thus "b1 = b1' \ b2 = b2'" using 0 by auto blanchet@55129: qed blanchet@55129: } note inj = this blanchet@55129: def sset \ "\ c. {u c b1 b2 | b1 b2. b1 \ set1 c \ b2 \ set2 c}" blanchet@55129: have fin_sset[simp]: "\ c. c \ set_of P \ finite (sset c)" unfolding sset_def blanchet@55129: using fin_set1 fin_set2 finite_twosets by blast blanchet@55129: have sset_A: "\ c. c \ set_of P \ sset c \ A" unfolding sset_def by auto blanchet@55129: {fix c a assume c: "c \ set_of P" and ac: "a \ sset c" blanchet@55129: then obtain b1 b2 where b1: "b1 \ set1 c" and b2: "b2 \ set2 c" blanchet@55129: and a: "a = u c b1 b2" unfolding sset_def by auto blanchet@55129: have "p1 a \ set1 c" and p2a: "p2 a \ set2 c" blanchet@55129: using ac a b1 b2 c u(2) u(3) by simp+ blanchet@55129: hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c] blanchet@55129: unfolding inj2_def by (metis c u(2) u(3)) blanchet@55129: } note u_p12[simp] = this blanchet@55129: {fix c a assume c: "c \ set_of P" and ac: "a \ sset c" blanchet@55129: hence "p1 a \ set1 c" unfolding sset_def by auto blanchet@55129: }note p1[simp] = this blanchet@55129: {fix c a assume c: "c \ set_of P" and ac: "a \ sset c" blanchet@55129: hence "p2 a \ set2 c" unfolding sset_def by auto blanchet@55129: }note p2[simp] = this blanchet@55129: blanchet@55129: {fix c assume c: "c \ set_of P" blanchet@55129: hence "\ M. (\ b1 \ set1 c. setsum (\ b2. M (u c b1 b2)) (set2 c) = count N1 b1) \ blanchet@55129: (\ b2 \ set2 c. setsum (\ b1. M (u c b1 b2)) (set1 c) = count N2 b2)" blanchet@55129: unfolding sset_def blanchet@55129: using matrix_setsum_finite[OF set1_NE[OF c] fin_set1[OF c] blanchet@55129: set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto blanchet@55129: } blanchet@55129: then obtain Ms where blanchet@55129: ss1: "\ c b1. \c \ set_of P; b1 \ set1 c\ \ blanchet@55129: setsum (\ b2. Ms c (u c b1 b2)) (set2 c) = count N1 b1" and blanchet@55129: ss2: "\ c b2. \c \ set_of P; b2 \ set2 c\ \ blanchet@55129: setsum (\ b1. Ms c (u c b1 b2)) (set1 c) = count N2 b2" blanchet@55129: by metis blanchet@55129: def SET \ "\ c \ set_of P. sset c" blanchet@55129: have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto blanchet@55129: have SET_A: "SET \ A" unfolding SET_def using sset_A by blast blanchet@55129: have u_SET[simp]: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ u c b1 b2 \ SET" blanchet@55129: unfolding SET_def sset_def by blast blanchet@55129: {fix c a assume c: "c \ set_of P" and a: "a \ SET" and p1a: "p1 a \ set1 c" blanchet@55129: then obtain c' where c': "c' \ set_of P" and ac': "a \ sset c'" blanchet@55129: unfolding SET_def by auto blanchet@55129: hence "p1 a \ set1 c'" unfolding sset_def by auto blanchet@55129: hence eq: "c = c'" using p1a c c' set1_disj by auto blanchet@55129: hence "a \ sset c" using ac' by simp blanchet@55129: } note p1_rev = this blanchet@55129: {fix c a assume c: "c \ set_of P" and a: "a \ SET" and p2a: "p2 a \ set2 c" blanchet@55129: then obtain c' where c': "c' \ set_of P" and ac': "a \ sset c'" blanchet@55129: unfolding SET_def by auto blanchet@55129: hence "p2 a \ set2 c'" unfolding sset_def by auto blanchet@55129: hence eq: "c = c'" using p2a c c' set2_disj by auto blanchet@55129: hence "a \ sset c" using ac' by simp blanchet@55129: } note p2_rev = this blanchet@55129: blanchet@55129: have "\ a \ SET. \ c \ set_of P. a \ sset c" unfolding SET_def by auto blanchet@55129: then obtain h where h: "\ a \ SET. h a \ set_of P \ a \ sset (h a)" by metis blanchet@55129: have h_u[simp]: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ blanchet@55129: \ h (u c b1 b2) = c" blanchet@55129: by (metis h p2 set2 u(3) u_SET) blanchet@55129: have h_u1: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ blanchet@55129: \ h (u c b1 b2) = f1 b1" blanchet@55129: using h unfolding sset_def by auto blanchet@55129: have h_u2: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ blanchet@55129: \ h (u c b1 b2) = f2 b2" blanchet@55129: using h unfolding sset_def by auto blanchet@55129: def M \ blanchet@55129: "Abs_multiset (\ a. if a \ SET \ p1 a \ set_of N1 \ p2 a \ set_of N2 then Ms (h a) a else 0)" blanchet@55129: have "(\ a. if a \ SET \ p1 a \ set_of N1 \ p2 a \ set_of N2 then Ms (h a) a else 0) \ multiset" blanchet@55129: unfolding multiset_def by auto blanchet@55129: hence [transfer_rule]: "pcr_multiset op = (\ a. if a \ SET \ p1 a \ set_of N1 \ p2 a \ set_of N2 then Ms (h a) a else 0) M" blanchet@55129: unfolding M_def pcr_multiset_def cr_multiset_def by (auto simp: Abs_multiset_inverse) blanchet@55129: have sM: "set_of M \ SET" "set_of M \ p1 -` (set_of N1)" "set_of M \ p2 -` set_of N2" blanchet@55129: by (transfer, auto split: split_if_asm)+ blanchet@55129: show "\M. set_of M \ A \ mmap p1 M = N1 \ mmap p2 M = N2" blanchet@55129: proof(rule exI[of _ M], safe) blanchet@55129: fix a assume *: "a \ set_of M" blanchet@55129: from SET_A show "a \ A" blanchet@55129: proof (cases "a \ SET") blanchet@55129: case False thus ?thesis using * by transfer' auto blanchet@55129: qed blast blanchet@55129: next blanchet@55129: show "mmap p1 M = N1" blanchet@55129: proof(intro multiset_eqI) blanchet@55129: fix b1 blanchet@55129: let ?K = "{a. p1 a = b1 \ a \# M}" blanchet@55129: have "setsum (count M) ?K = count N1 b1" blanchet@55129: proof(cases "b1 \ set_of N1") blanchet@55129: case False blanchet@55129: hence "?K = {}" using sM(2) by auto blanchet@55129: thus ?thesis using False by auto blanchet@55129: next blanchet@55129: case True blanchet@55129: def c \ "f1 b1" blanchet@55129: have c: "c \ set_of P" and b1: "b1 \ set1 c" blanchet@55129: unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap]) blanchet@55129: with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \ a \ SET}" haftmann@57418: by transfer (force intro: setsum.mono_neutral_cong_left split: split_if_asm) blanchet@55129: also have "... = setsum (count M) ((\ b2. u c b1 b2) ` (set2 c))" haftmann@57418: apply(rule setsum.cong) using c b1 proof safe blanchet@55129: fix a assume p1a: "p1 a \ set1 c" and "c \ set_of P" and "a \ SET" blanchet@55129: hence ac: "a \ sset c" using p1_rev by auto blanchet@55129: hence "a = u c (p1 a) (p2 a)" using c by auto blanchet@55129: moreover have "p2 a \ set2 c" using ac c by auto blanchet@55129: ultimately show "a \ u c (p1 a) ` set2 c" by auto blanchet@55129: qed auto blanchet@55129: also have "... = setsum (\ b2. count M (u c b1 b2)) (set2 c)" haftmann@57418: unfolding comp_def[symmetric] apply(rule setsum.reindex) blanchet@55129: using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast blanchet@55129: also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric] haftmann@57418: apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b1 set2) thomas@57492: using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] thomas@57492: [[hypsubst_thin = true]] thomas@57492: by fastforce blanchet@55129: finally show ?thesis . blanchet@55129: qed blanchet@55129: thus "count (mmap p1 M) b1 = count N1 b1" by transfer blanchet@55129: qed blanchet@55129: next blanchet@55129: show "mmap p2 M = N2" blanchet@55129: proof(intro multiset_eqI) blanchet@55129: fix b2 blanchet@55129: let ?K = "{a. p2 a = b2 \ a \# M}" blanchet@55129: have "setsum (count M) ?K = count N2 b2" blanchet@55129: proof(cases "b2 \ set_of N2") blanchet@55129: case False blanchet@55129: hence "?K = {}" using sM(3) by auto blanchet@55129: thus ?thesis using False by auto blanchet@55129: next blanchet@55129: case True blanchet@55129: def c \ "f2 b2" blanchet@55129: have c: "c \ set_of P" and b2: "b2 \ set2 c" blanchet@55129: unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap]) blanchet@55129: with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \ a \ SET}" haftmann@57418: by transfer (force intro: setsum.mono_neutral_cong_left split: split_if_asm) blanchet@55129: also have "... = setsum (count M) ((\ b1. u c b1 b2) ` (set1 c))" haftmann@57418: apply(rule setsum.cong) using c b2 proof safe blanchet@55129: fix a assume p2a: "p2 a \ set2 c" and "c \ set_of P" and "a \ SET" blanchet@55129: hence ac: "a \ sset c" using p2_rev by auto blanchet@55129: hence "a = u c (p1 a) (p2 a)" using c by auto blanchet@55129: moreover have "p1 a \ set1 c" using ac c by auto blanchet@55129: ultimately show "a \ (\x. u c x (p2 a)) ` set1 c" by auto blanchet@55129: qed auto blanchet@55129: also have "... = setsum (count M o (\ b1. u c b1 b2)) (set1 c)" haftmann@57418: apply(rule setsum.reindex) blanchet@55129: using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast blanchet@55129: also have "... = setsum (\ b1. count M (u c b1 b2)) (set1 c)" by simp blanchet@55129: also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def haftmann@57418: apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b2 set1) thomas@57492: using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def thomas@57492: [[hypsubst_thin = true]] thomas@57492: by fastforce blanchet@55129: finally show ?thesis . blanchet@55129: qed blanchet@55129: thus "count (mmap p2 M) b2 = count N2 b2" by transfer blanchet@55129: qed blanchet@55129: qed blanchet@55129: qed blanchet@55129: blanchet@55129: lemma set_of_bd: "(card_of (set_of x), natLeq) \ ordLeq" blanchet@55129: by transfer blanchet@55129: (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def) blanchet@55129: blanchet@55129: lemma wppull_mmap: blanchet@55129: assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" blanchet@55129: shows "wppull {M. set_of M \ A} {N1. set_of N1 \ B1} {N2. set_of N2 \ B2} blanchet@55129: (mmap f1) (mmap f2) (mmap e1) (mmap e2) (mmap p1) (mmap p2)" blanchet@55129: proof - blanchet@55129: from assms obtain j where j: "\a'\thePull B1 B2 f1 f2. blanchet@55129: j a' \ A \ e1 (p1 (j a')) = e1 (fst a') \ e2 (p2 (j a')) = e2 (snd a')" blanchet@55129: by (blast dest: wppull_thePull) blanchet@55129: then show ?thesis blanchet@55129: by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"]) blanchet@55129: (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap] blanchet@55129: intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric]) blanchet@55129: qed blanchet@55129: blanchet@55129: bnf "'a multiset" blanchet@55129: map: mmap blanchet@55129: sets: set_of blanchet@55129: bd: natLeq blanchet@55129: wits: "{#}" blanchet@55129: by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd blanchet@55129: Grp_def relcompp.simps intro: mmap_cong) blanchet@55129: (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def blanchet@55129: o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified]) blanchet@55129: blanchet@55129: inductive rel_multiset' where blanchet@55129: Zero[intro]: "rel_multiset' R {#} {#}" blanchet@55129: | Plus[intro]: "\R a b; rel_multiset' R M N\ \ rel_multiset' R (M + {#a#}) (N + {#b#})" blanchet@55129: blanchet@55129: lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \ M = {#}" blanchet@55129: by (metis image_is_empty multiset.set_map set_of_eq_empty_iff) blanchet@55129: blanchet@55129: lemma map_multiset_Zero[simp]: "mmap f {#} = {#}" by simp blanchet@55129: blanchet@55129: lemma rel_multiset_Zero: "rel_multiset R {#} {#}" blanchet@55129: unfolding rel_multiset_def Grp_def by auto blanchet@55129: blanchet@55129: declare multiset.count[simp] blanchet@55129: declare Abs_multiset_inverse[simp] blanchet@55129: declare multiset.count_inverse[simp] blanchet@55129: declare union_preserves_multiset[simp] blanchet@55129: blanchet@55129: lemma map_multiset_Plus[simp]: "mmap f (M1 + M2) = mmap f M1 + mmap f M2" blanchet@55129: proof (intro multiset_eqI, transfer fixing: f) blanchet@55129: fix x :: 'a and M1 M2 :: "'b \ nat" blanchet@55129: assume "M1 \ multiset" "M2 \ multiset" blanchet@55129: hence "setsum M1 {a. f a = x \ 0 < M1 a} = setsum M1 {a. f a = x \ 0 < M1 a + M2 a}" blanchet@55129: "setsum M2 {a. f a = x \ 0 < M2 a} = setsum M2 {a. f a = x \ 0 < M1 a + M2 a}" haftmann@57418: by (auto simp: multiset_def intro!: setsum.mono_neutral_cong_left) blanchet@55129: then show "(\a | f a = x \ 0 < M1 a + M2 a. M1 a + M2 a) = blanchet@55129: setsum M1 {a. f a = x \ 0 < M1 a} + blanchet@55129: setsum M2 {a. f a = x \ 0 < M2 a}" blanchet@55129: by (auto simp: setsum.distrib[symmetric]) blanchet@55129: qed blanchet@55129: blanchet@55129: lemma map_multiset_single[simp]: "mmap f {#a#} = {#f a#}" blanchet@55129: by transfer auto blanchet@55129: blanchet@55129: lemma rel_multiset_Plus: blanchet@55129: assumes ab: "R a b" and MN: "rel_multiset R M N" blanchet@55129: shows "rel_multiset R (M + {#a#}) (N + {#b#})" blanchet@55129: proof- blanchet@55129: {fix y assume "R a b" and "set_of y \ {(x, y). R x y}" blanchet@55129: hence "\ya. mmap fst y + {#a#} = mmap fst ya \ blanchet@55129: mmap snd y + {#b#} = mmap snd ya \ blanchet@55129: set_of ya \ {(x, y). R x y}" blanchet@55129: apply(intro exI[of _ "y + {#(a,b)#}"]) by auto blanchet@55129: } blanchet@55129: thus ?thesis blanchet@55129: using assms blanchet@55129: unfolding rel_multiset_def Grp_def by force blanchet@55129: qed blanchet@55129: blanchet@55129: lemma rel_multiset'_imp_rel_multiset: blanchet@55129: "rel_multiset' R M N \ rel_multiset R M N" blanchet@55129: apply(induct rule: rel_multiset'.induct) blanchet@55129: using rel_multiset_Zero rel_multiset_Plus by auto blanchet@55129: blanchet@55129: lemma mcard_mmap[simp]: "mcard (mmap f M) = mcard M" blanchet@55129: proof - blanchet@55129: def A \ "\ b. {a. f a = b \ a \# M}" blanchet@55129: let ?B = "{b. 0 < setsum (count M) (A b)}" blanchet@55129: have "{b. \a. f a = b \ a \# M} \ f ` {a. a \# M}" by auto blanchet@55129: moreover have "finite (f ` {a. a \# M})" apply(rule finite_imageI) blanchet@55129: using finite_Collect_mem . blanchet@55129: ultimately have fin: "finite {b. \a. f a = b \ a \# M}" by(rule finite_subset) blanchet@55129: have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp blanchet@55129: by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral) blanchet@55129: have 0: "\ b. 0 < setsum (count M) (A b) \ (\ a \ A b. count M a > 0)" blanchet@55129: apply safe haftmann@57418: apply (metis less_not_refl setsum_gt_0_iff setsum.infinite) blanchet@55129: by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff) blanchet@55129: hence AB: "A ` ?B = {A b | b. \ a \ A b. count M a > 0}" by auto blanchet@55129: blanchet@55129: have "setsum (\ x. setsum (count M) (A x)) ?B = setsum (setsum (count M) o A) ?B" blanchet@55129: unfolding comp_def .. blanchet@55129: also have "... = (\x\ A ` ?B. setsum (count M) x)" blanchet@55129: unfolding setsum.reindex [OF i, symmetric] .. blanchet@55129: also have "... = setsum (count M) (\x\A ` {b. 0 < setsum (count M) (A b)}. x)" blanchet@55129: (is "_ = setsum (count M) ?J") blanchet@55129: apply(rule setsum.UNION_disjoint[symmetric]) blanchet@55129: using 0 fin unfolding A_def by auto blanchet@55129: also have "?J = {a. a \# M}" unfolding AB unfolding A_def by auto blanchet@55129: finally have "setsum (\ x. setsum (count M) (A x)) ?B = blanchet@55129: setsum (count M) {a. a \# M}" . blanchet@55129: then show ?thesis unfolding mcard_unfold_setsum A_def by transfer blanchet@55129: qed blanchet@55129: blanchet@55129: lemma rel_multiset_mcard: blanchet@55129: assumes "rel_multiset R M N" blanchet@55129: shows "mcard M = mcard N" blanchet@55129: using assms unfolding rel_multiset_def Grp_def by auto blanchet@55129: blanchet@55129: lemma multiset_induct2[case_names empty addL addR]: blanchet@55129: assumes empty: "P {#} {#}" blanchet@55129: and addL: "\M N a. P M N \ P (M + {#a#}) N" blanchet@55129: and addR: "\M N a. P M N \ P M (N + {#a#})" blanchet@55129: shows "P M N" blanchet@55129: apply(induct N rule: multiset_induct) blanchet@55129: apply(induct M rule: multiset_induct, rule empty, erule addL) blanchet@55129: apply(induct M rule: multiset_induct, erule addR, erule addR) blanchet@55129: done blanchet@55129: blanchet@55129: lemma multiset_induct2_mcard[consumes 1, case_names empty add]: blanchet@55129: assumes c: "mcard M = mcard N" blanchet@55129: and empty: "P {#} {#}" blanchet@55129: and add: "\M N a b. P M N \ P (M + {#a#}) (N + {#b#})" blanchet@55129: shows "P M N" blanchet@55129: using c proof(induct M arbitrary: N rule: measure_induct_rule[of mcard]) blanchet@55129: case (less M) show ?case blanchet@55129: proof(cases "M = {#}") blanchet@55129: case True hence "N = {#}" using less.prems by auto blanchet@55129: thus ?thesis using True empty by auto blanchet@55129: next blanchet@55129: case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split) blanchet@55129: have "N \ {#}" using False less.prems by auto blanchet@55129: then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split) blanchet@55129: have "mcard M1 = mcard N1" using less.prems unfolding M N by auto blanchet@55129: thus ?thesis using M N less.hyps add by auto blanchet@55129: qed blanchet@55129: qed blanchet@55129: blanchet@55129: lemma msed_map_invL: blanchet@55129: assumes "mmap f (M + {#a#}) = N" blanchet@55129: shows "\ N1. N = N1 + {#f a#} \ mmap f M = N1" blanchet@55129: proof- blanchet@55129: have "f a \# N" blanchet@55129: using assms multiset.set_map[of f "M + {#a#}"] by auto blanchet@55129: then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis blanchet@55129: have "mmap f M = N1" using assms unfolding N by simp blanchet@55129: thus ?thesis using N by blast blanchet@55129: qed blanchet@55129: blanchet@55129: lemma msed_map_invR: blanchet@55129: assumes "mmap f M = N + {#b#}" blanchet@55129: shows "\ M1 a. M = M1 + {#a#} \ f a = b \ mmap f M1 = N" blanchet@55129: proof- blanchet@55129: obtain a where a: "a \# M" and fa: "f a = b" blanchet@55129: using multiset.set_map[of f M] unfolding assms blanchet@55129: by (metis image_iff mem_set_of_iff union_single_eq_member) blanchet@55129: then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis blanchet@55129: have "mmap f M1 = N" using assms unfolding M fa[symmetric] by simp blanchet@55129: thus ?thesis using M fa by blast blanchet@55129: qed blanchet@55129: blanchet@55129: lemma msed_rel_invL: blanchet@55129: assumes "rel_multiset R (M + {#a#}) N" blanchet@55129: shows "\ N1 b. N = N1 + {#b#} \ R a b \ rel_multiset R M N1" blanchet@55129: proof- blanchet@55129: obtain K where KM: "mmap fst K = M + {#a#}" blanchet@55129: and KN: "mmap snd K = N" and sK: "set_of K \ {(a, b). R a b}" blanchet@55129: using assms blanchet@55129: unfolding rel_multiset_def Grp_def by auto blanchet@55129: obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a" blanchet@55129: and K1M: "mmap fst K1 = M" using msed_map_invR[OF KM] by auto blanchet@55129: obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "mmap snd K1 = N1" blanchet@55129: using msed_map_invL[OF KN[unfolded K]] by auto blanchet@55129: have Rab: "R a (snd ab)" using sK a unfolding K by auto blanchet@55129: have "rel_multiset R M N1" using sK K1M K1N1 blanchet@55129: unfolding K rel_multiset_def Grp_def by auto blanchet@55129: thus ?thesis using N Rab by auto blanchet@55129: qed blanchet@55129: blanchet@55129: lemma msed_rel_invR: blanchet@55129: assumes "rel_multiset R M (N + {#b#})" blanchet@55129: shows "\ M1 a. M = M1 + {#a#} \ R a b \ rel_multiset R M1 N" blanchet@55129: proof- blanchet@55129: obtain K where KN: "mmap snd K = N + {#b#}" blanchet@55129: and KM: "mmap fst K = M" and sK: "set_of K \ {(a, b). R a b}" blanchet@55129: using assms blanchet@55129: unfolding rel_multiset_def Grp_def by auto blanchet@55129: obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b" blanchet@55129: and K1N: "mmap snd K1 = N" using msed_map_invR[OF KN] by auto blanchet@55129: obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "mmap fst K1 = M1" blanchet@55129: using msed_map_invL[OF KM[unfolded K]] by auto blanchet@55129: have Rab: "R (fst ab) b" using sK b unfolding K by auto blanchet@55129: have "rel_multiset R M1 N" using sK K1N K1M1 blanchet@55129: unfolding K rel_multiset_def Grp_def by auto blanchet@55129: thus ?thesis using M Rab by auto blanchet@55129: qed blanchet@55129: blanchet@55129: lemma rel_multiset_imp_rel_multiset': blanchet@55129: assumes "rel_multiset R M N" blanchet@55129: shows "rel_multiset' R M N" blanchet@55129: using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard]) blanchet@55129: case (less M) blanchet@55129: have c: "mcard M = mcard N" using rel_multiset_mcard[OF less.prems] . blanchet@55129: show ?case blanchet@55129: proof(cases "M = {#}") blanchet@55129: case True hence "N = {#}" using c by simp blanchet@55129: thus ?thesis using True rel_multiset'.Zero by auto blanchet@55129: next blanchet@55129: case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split) blanchet@55129: obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "rel_multiset R M1 N1" blanchet@55129: using msed_rel_invL[OF less.prems[unfolded M]] by auto blanchet@55129: have "rel_multiset' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp blanchet@55129: thus ?thesis using rel_multiset'.Plus[of R a b, OF R] unfolding M N by simp blanchet@55129: qed blanchet@55129: qed blanchet@55129: blanchet@55129: lemma rel_multiset_rel_multiset': blanchet@55129: "rel_multiset R M N = rel_multiset' R M N" blanchet@55129: using rel_multiset_imp_rel_multiset' rel_multiset'_imp_rel_multiset by auto blanchet@55129: blanchet@55129: (* The main end product for rel_multiset: inductive characterization *) blanchet@55129: theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] = blanchet@55129: rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]] blanchet@55129: blanchet@56656: blanchet@56656: subsection {* Size setup *} blanchet@56656: blanchet@56656: lemma multiset_size_o_map: "size_multiset g \ mmap f = size_multiset (g \ f)" blanchet@56656: apply (rule ext) blanchet@56656: apply (unfold o_apply) blanchet@56656: apply (induct_tac x) blanchet@56656: apply auto blanchet@56656: done blanchet@56656: blanchet@56656: setup {* blanchet@56656: BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset} blanchet@56656: @{thms size_multiset_empty size_multiset_single size_multiset_union size_empty size_single blanchet@56656: size_union} blanchet@56656: @{thms multiset_size_o_map} blanchet@56656: *} blanchet@56656: blanchet@56656: hide_const (open) wcount blanchet@56656: blanchet@55129: end