diff -r 69c9fc1d11f2 -r 07f75bf77a33 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Dec 21 10:11:10 2000 +0100 +++ b/src/HOL/Library/Multiset.thy Thu Dec 21 10:16:07 2000 +0100 @@ -16,7 +16,7 @@ typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}" proof - show "(\x. 0::nat) \ ?multiset" by simp + show "(\\x. 0::nat) \\ ?multiset" by simp qed lemmas multiset_typedef [simp] = @@ -25,23 +25,23 @@ constdefs Mempty :: "'a multiset" ("{#}") - "{#} == Abs_multiset (\a. 0)" + "{#} == Abs_multiset (\\a. 0)" single :: "'a => 'a multiset" ("{#_#}") - "{#a#} == Abs_multiset (\b. if b = a then 1 else 0)" + "{#a#} == Abs_multiset (\\b. if b = a then 1 else 0)" count :: "'a multiset => 'a => nat" "count == Rep_multiset" MCollect :: "'a multiset => ('a => bool) => 'a multiset" - "MCollect M P == Abs_multiset (\x. if P x then Rep_multiset M x else 0)" + "MCollect M P == Abs_multiset (\\x. if P x then Rep_multiset M x else 0)" syntax "_Melem" :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})") translations "a :# M" == "0 < count M a" - "{#x:M. P#}" == "MCollect M (\x. P)" + "{#x:M. P#}" == "MCollect M (\\x. P)" constdefs set_of :: "'a multiset => 'a set" @@ -52,8 +52,8 @@ instance multiset :: ("term") zero .. defs (overloaded) - union_def: "M + N == Abs_multiset (\a. Rep_multiset M a + Rep_multiset N a)" - diff_def: "M - N == Abs_multiset (\a. Rep_multiset M a - Rep_multiset N a)" + union_def: "M + N == Abs_multiset (\\a. Rep_multiset M a + Rep_multiset N a)" + diff_def: "M - N == Abs_multiset (\\a. Rep_multiset M a - Rep_multiset N a)" Zero_def [simp]: "0 == {#}" size_def: "size M == setsum (count M) (set_of M)" @@ -62,16 +62,16 @@ \medskip Preservation of the representing set @{term multiset}. *} -lemma const0_in_multiset [simp]: "(\a. 0) \ multiset" +lemma const0_in_multiset [simp]: "(\\a. 0) \\ multiset" apply (simp add: multiset_def) done -lemma only1_in_multiset [simp]: "(\b. if b = a then 1 else 0) \ multiset" +lemma only1_in_multiset [simp]: "(\\b. if b = a then 1 else 0) \\ multiset" apply (simp add: multiset_def) done lemma union_preserves_multiset [simp]: - "M \ multiset ==> N \ multiset ==> (\a. M a + N a) \ multiset" + "M \\ multiset ==> N \\ multiset ==> (\\a. M a + N a) \\ multiset" apply (unfold multiset_def) apply simp apply (drule finite_UnI) @@ -80,7 +80,7 @@ done lemma diff_preserves_multiset [simp]: - "M \ multiset ==> (\a. M a - N a) \ multiset" + "M \\ multiset ==> (\\a. M a - N a) \\ multiset" apply (unfold multiset_def) apply simp apply (rule finite_subset) @@ -94,7 +94,7 @@ subsubsection {* Union *} -theorem union_empty [simp]: "M + {#} = M \ {#} + M = M" +theorem union_empty [simp]: "M + {#} = M \\ {#} + M = M" apply (simp add: union_def Mempty_def) done @@ -124,7 +124,7 @@ subsubsection {* Difference *} -theorem diff_empty [simp]: "M - {#} = M \ {#} - M = {#}" +theorem diff_empty [simp]: "M - {#} = M \\ {#} - M = {#}" apply (simp add: Mempty_def diff_def) done @@ -162,7 +162,7 @@ apply (simp add: set_of_def) done -theorem set_of_union [simp]: "set_of (M + N) = set_of M \ set_of N" +theorem set_of_union [simp]: "set_of (M + N) = set_of M \\ set_of N" apply (auto simp add: set_of_def) done @@ -170,7 +170,7 @@ apply (auto simp add: set_of_def Mempty_def count_def expand_fun_eq) done -theorem mem_set_of_iff [simp]: "(x \ set_of M) = (x :# M)" +theorem mem_set_of_iff [simp]: "(x \\ set_of M) = (x :# M)" apply (auto simp add: set_of_def) done @@ -191,7 +191,7 @@ done theorem setsum_count_Int: - "finite A ==> setsum (count N) (A \ set_of N) = setsum (count N) A" + "finite A ==> setsum (count N) (A \\ set_of N) = setsum (count N) A" apply (erule finite_induct) apply simp apply (simp add: Int_insert_left set_of_def) @@ -199,7 +199,7 @@ theorem size_union [simp]: "size (M + N::'a multiset) = size M + size N" apply (unfold size_def) - apply (subgoal_tac "count (M + N) = (\a. count M a + count N a)") + apply (subgoal_tac "count (M + N) = (\\a. count M a + count N a)") prefer 2 apply (rule ext) apply simp @@ -214,7 +214,7 @@ apply (simp add: set_of_def count_def expand_fun_eq) done -theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \a. a :# M" +theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \\a. a :# M" apply (unfold size_def) apply (drule setsum_SucD) apply auto @@ -223,11 +223,11 @@ subsubsection {* Equality of multisets *} -theorem multiset_eq_conv_count_eq: "(M = N) = (\a. count M a = count N a)" +theorem multiset_eq_conv_count_eq: "(M = N) = (\\a. count M a = count N a)" apply (simp add: count_def expand_fun_eq) done -theorem single_not_empty [simp]: "{#a#} \ {#} \ {#} \ {#a#}" +theorem single_not_empty [simp]: "{#a#} \\ {#} \\ {#} \\ {#a#}" apply (simp add: single_def Mempty_def expand_fun_eq) done @@ -235,11 +235,11 @@ apply (auto simp add: single_def expand_fun_eq) done -theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \ N = {#})" +theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \\ N = {#})" apply (auto simp add: union_def Mempty_def expand_fun_eq) done -theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \ N = {#})" +theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \\ N = {#})" apply (auto simp add: union_def Mempty_def expand_fun_eq) done @@ -252,7 +252,7 @@ done theorem union_is_single: - "(M + N = {#a#}) = (M = {#a#} \ N={#} \ M = {#} \ N = {#a#})" + "(M + N = {#a#}) = (M = {#a#} \\ N={#} \\ M = {#} \\ N = {#a#})" apply (unfold Mempty_def single_def union_def) apply (simp add: add_is_1 expand_fun_eq) apply blast @@ -260,16 +260,16 @@ theorem single_is_union: "({#a#} = M + N) = - ({#a#} = M \ N = {#} \ M = {#} \ {#a#} = N)" + ({#a#} = M \\ N = {#} \\ M = {#} \\ {#a#} = N)" apply (unfold Mempty_def single_def union_def) - apply (simp add: one_is_add expand_fun_eq) + apply (simp add: add_is_1 expand_fun_eq) apply (blast dest: sym) done theorem add_eq_conv_diff: "(M + {#a#} = N + {#b#}) = - (M = N \ a = b \ - M = N - {#a#} + {#b#} \ N = M - {#b#} + {#a#})" + (M = N \\ a = b \\ + M = N - {#a#} + {#b#} \\ N = M - {#b#} + {#a#})" apply (unfold single_def union_def diff_def) apply (simp (no_asm) add: expand_fun_eq) apply (rule conjI) @@ -291,7 +291,7 @@ (* val prems = Goal "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F"; -by (res_inst_tac [("a","F"),("f","\A. if finite A then card A else 0")] +by (res_inst_tac [("a","F"),("f","\\A. if finite A then card A else 0")] measure_induct 1); by (Clarify_tac 1); by (resolve_tac prems 1); @@ -320,7 +320,7 @@ lemma setsum_decr: "finite F ==> 0 < f a ==> - setsum (f (a := f a - 1)) F = (if a \ F then setsum f F - 1 else setsum f F)" + setsum (f (a := f a - 1)) F = (if a \\ F then setsum f F - 1 else setsum f F)" apply (erule finite_induct) apply auto apply (drule_tac a = a in mk_disjoint_insert) @@ -328,8 +328,8 @@ done lemma rep_multiset_induct_aux: - "P (\a. 0) ==> (!!f b. f \ multiset ==> P f ==> P (f (b := f b + 1))) - ==> \f. f \ multiset --> setsum f {x. 0 < f x} = n --> P f" + "P (\\a. 0) ==> (!!f b. f \\ multiset ==> P f ==> P (f (b := f b + 1))) + ==> \\f. f \\ multiset --> setsum f {x. 0 < f x} = n --> P f" proof - case antecedent note prems = this [unfolded multiset_def] @@ -338,7 +338,7 @@ apply (induct_tac n) apply simp apply clarify - apply (subgoal_tac "f = (\a.0)") + apply (subgoal_tac "f = (\\a.0)") apply simp apply (rule prems) apply (rule ext) @@ -363,10 +363,10 @@ apply (erule allE, erule impE, erule_tac [2] mp) apply blast apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply) - apply (subgoal_tac "{x. x \ a --> 0 < f x} = {x. 0 < f x}") + apply (subgoal_tac "{x. x \\ a --> 0 < f x} = {x. 0 < f x}") prefer 2 apply blast - apply (subgoal_tac "{x. x \ a \ 0 < f x} = {x. 0 < f x} - {a}") + apply (subgoal_tac "{x. x \\ a \\ 0 < f x} = {x. 0 < f x} - {a}") prefer 2 apply blast apply (simp add: le_imp_diff_is_add setsum_diff1 cong: conj_cong) @@ -374,8 +374,8 @@ qed theorem rep_multiset_induct: - "f \ multiset ==> P (\a. 0) ==> - (!!f b. f \ multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" + "f \\ multiset ==> P (\\a. 0) ==> + (!!f b. f \\ multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" apply (insert rep_multiset_induct_aux) apply blast done @@ -390,7 +390,7 @@ apply (rule Rep_multiset_inverse [THEN subst]) apply (rule Rep_multiset [THEN rep_multiset_induct]) apply (rule prem1) - apply (subgoal_tac "f (b := f b + 1) = (\a. f a + (if a = b then 1 else 0))") + apply (subgoal_tac "f (b := f b + 1) = (\\a. f a + (if a = b then 1 else 0))") prefer 2 apply (simp add: expand_fun_eq) apply (erule ssubst) @@ -401,7 +401,7 @@ lemma MCollect_preserves_multiset: - "M \ multiset ==> (\x. if P x then M x else 0) \ multiset" + "M \\ multiset ==> (\\x. if P x then M x else 0) \\ multiset" apply (simp add: multiset_def) apply (rule finite_subset) apply auto @@ -413,11 +413,11 @@ apply (simp add: MCollect_preserves_multiset) done -theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \ {x. P x}" +theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \\ {x. P x}" apply (auto simp add: set_of_def) done -theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \ P x #}" +theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \\ P x #}" apply (subst multiset_eq_conv_count_eq) apply auto done @@ -427,7 +427,7 @@ theorem add_eq_conv_ex: "(M + {#a#} = N + {#b#}) = - (M = N \ a = b \ (\K. M = K + {#b#} \ N = K + {#a#}))" + (M = N \\ a = b \\ (\\K. M = K + {#b#} \\ N = K + {#a#}))" apply (auto simp add: add_eq_conv_diff) done @@ -437,41 +437,41 @@ subsubsection {* Well-foundedness *} constdefs - mult1 :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" + mult1 :: "('a \\ 'a) set => ('a multiset \\ 'a multiset) set" "mult1 r == - {(N, M). \a M0 K. M = M0 + {#a#} \ N = M0 + K \ - (\b. b :# K --> (b, a) \ r)}" + {(N, M). \\a M0 K. M = M0 + {#a#} \\ N = M0 + K \\ + (\\b. b :# K --> (b, a) \\ r)}" - mult :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" + mult :: "('a \\ 'a) set => ('a multiset \\ 'a multiset) set" "mult r == (mult1 r)\<^sup>+" -lemma not_less_empty [iff]: "(M, {#}) \ mult1 r" +lemma not_less_empty [iff]: "(M, {#}) \\ mult1 r" by (simp add: mult1_def) -lemma less_add: "(N, M0 + {#a#}) \ mult1 r ==> - (\M. (M, M0) \ mult1 r \ N = M + {#a#}) \ - (\K. (\b. b :# K --> (b, a) \ r) \ N = M0 + K)" - (concl is "?case1 (mult1 r) \ ?case2") +lemma less_add: "(N, M0 + {#a#}) \\ mult1 r ==> + (\\M. (M, M0) \\ mult1 r \\ N = M + {#a#}) \\ + (\\K. (\\b. b :# K --> (b, a) \\ r) \\ N = M0 + K)" + (concl is "?case1 (mult1 r) \\ ?case2") proof (unfold mult1_def) - let ?r = "\K a. \b. b :# K --> (b, a) \ r" - let ?R = "\N M. \a M0 K. M = M0 + {#a#} \ N = M0 + K \ ?r K a" + let ?r = "\\K a. \\b. b :# K --> (b, a) \\ r" + let ?R = "\\N M. \\a M0 K. M = M0 + {#a#} \\ N = M0 + K \\ ?r K a" let ?case1 = "?case1 {(N, M). ?R N M}" - assume "(N, M0 + {#a#}) \ {(N, M). ?R N M}" - hence "\a' M0' K. - M0 + {#a#} = M0' + {#a'#} \ N = M0' + K \ ?r K a'" by simp - thus "?case1 \ ?case2" + assume "(N, M0 + {#a#}) \\ {(N, M). ?R N M}" + hence "\\a' M0' K. + M0 + {#a#} = M0' + {#a'#} \\ N = M0' + K \\ ?r K a'" by simp + thus "?case1 \\ ?case2" proof (elim exE conjE) fix a' M0' K assume N: "N = M0' + K" and r: "?r K a'" assume "M0 + {#a#} = M0' + {#a'#}" - hence "M0 = M0' \ a = a' \ - (\K'. M0 = K' + {#a'#} \ M0' = K' + {#a#})" + hence "M0 = M0' \\ a = a' \\ + (\\K'. M0 = K' + {#a'#} \\ M0' = K' + {#a#})" by (simp only: add_eq_conv_ex) thus ?thesis proof (elim disjE conjE exE) assume "M0 = M0'" "a = a'" - with N r have "?r K a \ N = M0 + K" by simp + with N r have "?r K a \\ N = M0 + K" by simp hence ?case2 .. thus ?thesis .. next fix K' @@ -485,78 +485,78 @@ qed qed -lemma all_accessible: "wf r ==> \M. M \ acc (mult1 r)" +lemma all_accessible: "wf r ==> \\M. M \\ acc (mult1 r)" proof let ?R = "mult1 r" let ?W = "acc ?R" { fix M M0 a - assume M0: "M0 \ ?W" - and wf_hyp: "\b. (b, a) \ r --> (\M \ ?W. M + {#b#} \ ?W)" - and acc_hyp: "\M. (M, M0) \ ?R --> M + {#a#} \ ?W" - have "M0 + {#a#} \ ?W" + assume M0: "M0 \\ ?W" + and wf_hyp: "\\b. (b, a) \\ r --> (\\M \\ ?W. M + {#b#} \\ ?W)" + and acc_hyp: "\\M. (M, M0) \\ ?R --> M + {#a#} \\ ?W" + have "M0 + {#a#} \\ ?W" proof (rule accI [of "M0 + {#a#}"]) fix N - assume "(N, M0 + {#a#}) \ ?R" - hence "((\M. (M, M0) \ ?R \ N = M + {#a#}) \ - (\K. (\b. b :# K --> (b, a) \ r) \ N = M0 + K))" + assume "(N, M0 + {#a#}) \\ ?R" + hence "((\\M. (M, M0) \\ ?R \\ N = M + {#a#}) \\ + (\\K. (\\b. b :# K --> (b, a) \\ r) \\ N = M0 + K))" by (rule less_add) - thus "N \ ?W" + thus "N \\ ?W" proof (elim exE disjE conjE) - fix M assume "(M, M0) \ ?R" and N: "N = M + {#a#}" - from acc_hyp have "(M, M0) \ ?R --> M + {#a#} \ ?W" .. - hence "M + {#a#} \ ?W" .. - thus "N \ ?W" by (simp only: N) + fix M assume "(M, M0) \\ ?R" and N: "N = M + {#a#}" + from acc_hyp have "(M, M0) \\ ?R --> M + {#a#} \\ ?W" .. + hence "M + {#a#} \\ ?W" .. + thus "N \\ ?W" by (simp only: N) next fix K assume N: "N = M0 + K" - assume "\b. b :# K --> (b, a) \ r" - have "?this --> M0 + K \ ?W" (is "?P K") + assume "\\b. b :# K --> (b, a) \\ r" + have "?this --> M0 + K \\ ?W" (is "?P K") proof (induct K) - from M0 have "M0 + {#} \ ?W" by simp + from M0 have "M0 + {#} \\ ?W" by simp thus "?P {#}" .. fix K x assume hyp: "?P K" show "?P (K + {#x#})" proof - assume a: "\b. b :# (K + {#x#}) --> (b, a) \ r" - hence "(x, a) \ r" by simp - with wf_hyp have b: "\M \ ?W. M + {#x#} \ ?W" by blast + assume a: "\\b. b :# (K + {#x#}) --> (b, a) \\ r" + hence "(x, a) \\ r" by simp + with wf_hyp have b: "\\M \\ ?W. M + {#x#} \\ ?W" by blast - from a hyp have "M0 + K \ ?W" by simp - with b have "(M0 + K) + {#x#} \ ?W" .. - thus "M0 + (K + {#x#}) \ ?W" by (simp only: union_assoc) + from a hyp have "M0 + K \\ ?W" by simp + with b have "(M0 + K) + {#x#} \\ ?W" .. + thus "M0 + (K + {#x#}) \\ ?W" by (simp only: union_assoc) qed qed - hence "M0 + K \ ?W" .. - thus "N \ ?W" by (simp only: N) + hence "M0 + K \\ ?W" .. + thus "N \\ ?W" by (simp only: N) qed qed } note tedious_reasoning = this assume wf: "wf r" fix M - show "M \ ?W" + show "M \\ ?W" proof (induct M) - show "{#} \ ?W" + show "{#} \\ ?W" proof (rule accI) - fix b assume "(b, {#}) \ ?R" - with not_less_empty show "b \ ?W" by contradiction + fix b assume "(b, {#}) \\ ?R" + with not_less_empty show "b \\ ?W" by contradiction qed - fix M a assume "M \ ?W" - from wf have "\M \ ?W. M + {#a#} \ ?W" + fix M a assume "M \\ ?W" + from wf have "\\M \\ ?W. M + {#a#} \\ ?W" proof induct fix a - assume "\b. (b, a) \ r --> (\M \ ?W. M + {#b#} \ ?W)" - show "\M \ ?W. M + {#a#} \ ?W" + assume "\\b. (b, a) \\ r --> (\\M \\ ?W. M + {#b#} \\ ?W)" + show "\\M \\ ?W. M + {#a#} \\ ?W" proof - fix M assume "M \ ?W" - thus "M + {#a#} \ ?W" + fix M assume "M \\ ?W" + thus "M + {#a#} \\ ?W" by (rule acc_induct) (rule tedious_reasoning) qed qed - thus "M + {#a#} \ ?W" .. + thus "M + {#a#} \\ ?W" .. qed qed @@ -578,9 +578,9 @@ text {* One direction. *} lemma mult_implies_one_step: - "trans r ==> (M, N) \ mult r ==> - \I J K. N = I + J \ M = I + K \ J \ {#} \ - (\k \ set_of K. \j \ set_of J. (k, j) \ r)" + "trans r ==> (M, N) \\ mult r ==> + \\I J K. N = I + J \\ M = I + K \\ J \\ {#} \\ + (\\k \\ set_of K. \\j \\ set_of J. (k, j) \\ r)" apply (unfold mult_def mult1_def set_of_def) apply (erule converse_trancl_induct) apply clarify @@ -592,7 +592,7 @@ apply (simp (no_asm)) apply (rule_tac x = "(K - {#a#}) + Ka" in exI) apply (simp (no_asm_simp) add: union_assoc [symmetric]) - apply (drule_tac f = "\M. M - {#a#}" in arg_cong) + apply (drule_tac f = "\\M. M - {#a#}" in arg_cong) apply (simp add: diff_union_single_conv) apply (simp (no_asm_use) add: trans_def) apply blast @@ -603,7 +603,7 @@ apply (rule conjI) apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) apply (rule conjI) - apply (drule_tac f = "\M. M - {#a#}" in arg_cong) + apply (drule_tac f = "\\M. M - {#a#}" in arg_cong) apply simp apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) apply (simp (no_asm_use) add: trans_def) @@ -617,7 +617,7 @@ apply (simp add: multiset_eq_conv_count_eq) done -lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \a N. M = N + {#a#}" +lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \\a N. M = N + {#a#}" apply (erule size_eq_Suc_imp_elem [THEN exE]) apply (drule elem_imp_eq_diff_union) apply auto @@ -625,8 +625,8 @@ lemma one_step_implies_mult_aux: "trans r ==> - \I J K. (size J = n \ J \ {#} \ (\k \ set_of K. \j \ set_of J. (k, j) \ r)) - --> (I + K, I + J) \ mult r" + \\I J K. (size J = n \\ J \\ {#} \\ (\\k \\ set_of K. \\j \\ set_of J. (k, j) \\ r)) + --> (I + K, I + J) \\ mult r" apply (induct_tac n) apply auto apply (frule size_eq_Suc_imp_eq_union) @@ -640,15 +640,15 @@ apply (rule r_into_trancl) apply (simp add: mult1_def set_of_def) apply blast - txt {* Now we know @{term "J' \ {#}"}. *} - apply (cut_tac M = K and P = "\x. (x, a) \ r" in multiset_partition) - apply (erule_tac P = "\k \ set_of K. ?P k" in rev_mp) + txt {* Now we know @{term "J' \\ {#}"}. *} + apply (cut_tac M = K and P = "\\x. (x, a) \\ r" in multiset_partition) + apply (erule_tac P = "\\k \\ set_of K. ?P k" in rev_mp) apply (erule ssubst) apply (simp add: Ball_def) apply auto apply (subgoal_tac - "((I + {# x : K. (x, a) \ r #}) + {# x : K. (x, a) \ r #}, - (I + {# x : K. (x, a) \ r #}) + J') \ mult r") + "((I + {# x : K. (x, a) \\ r #}) + {# x : K. (x, a) \\ r #}, + (I + {# x : K. (x, a) \\ r #}) + J') \\ mult r") prefer 2 apply force apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def) @@ -661,8 +661,8 @@ done theorem one_step_implies_mult: - "trans r ==> J \ {#} ==> \k \ set_of K. \j \ set_of J. (k, j) \ r - ==> (I + K, I + J) \ mult r" + "trans r ==> J \\ {#} ==> \\k \\ set_of K. \\