# HG changeset patch # User nipkow # Date 1201885266 -3600 # Node ID 278025d5282dd19eef9bbdd5e25c7d2fc83e9125 # Parent 377b7aa0b5b50ca6483f2593aec71f0e11c55873 modified MCollect syntax diff -r 377b7aa0b5b5 -r 278025d5282d src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Feb 01 08:35:58 2008 +0100 +++ b/src/HOL/Library/Multiset.thy Fri Feb 01 18:01:06 2008 +0100 @@ -46,9 +46,9 @@ notation (xsymbols) Melem (infix "\#" 50) syntax - "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})") + "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ :# _./ _#})") translations - "{#x:M. P#}" == "CONST MCollect M (\x. P)" + "{#x :# M. P#}" == "CONST MCollect M (\x. P)" definition set_of :: "'a multiset => 'a set" where @@ -178,7 +178,7 @@ by (simp add: count_def diff_def in_multiset) lemma count_MCollect [simp]: - "count {# x:M. P x #} a = (if P a then count M a else 0)" + "count {# x:#M. P x #} a = (if P a then count M a else 0)" by (simp add: count_def MCollect_def in_multiset) @@ -199,7 +199,7 @@ lemma mem_set_of_iff [simp]: "(x \ set_of M) = (x :# M)" by (auto simp add: set_of_def) -lemma set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \ {x. P x}" +lemma set_of_MCollect [simp]: "set_of {# x:#M. P x #} = set_of M \ {x. P x}" by (auto simp add: set_of_def) @@ -473,7 +473,7 @@ apply (rule_tac x="M - {#x#}" in exI, simp) done -lemma multiset_partition: "M = {# x:M. P x #} + {# x:M. \ P x #}" +lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \ P x #}" by (subst multiset_eq_conv_count_eq, auto) declare multiset_typedef [simp del] @@ -678,8 +678,8 @@ apply (erule ssubst) apply (simp add: Ball_def, 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) @@ -1334,9 +1334,9 @@ syntax comprehension2_mset :: "'a \ 'b \ 'b multiset \ bool \ 'a multiset" ("({#_/ | _ :# _./ _#})") translations - "{#e | x:#M. P#}" => "{#e. x :# {# x:M. P#}#}" + "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}" -text{* This allows to write not just filters like @{term"{#x:M. x