# HG changeset patch # User berghofe # Date 1210150769 -7200 # Node ID e82229ee8f43e819dae92b542b6595dabe3dfd78 # Parent 0cb35f537c91a389912c86050fd5144f0c5f9647 - Declared subset_eq as code lemma - Deleted types_code declaration for sets diff -r 0cb35f537c91 -r e82229ee8f43 src/HOL/Library/Executable_Set.thy --- a/src/HOL/Library/Executable_Set.thy Wed May 07 10:59:27 2008 +0200 +++ b/src/HOL/Library/Executable_Set.thy Wed May 07 10:59:29 2008 +0200 @@ -15,6 +15,8 @@ "A = B \ A \ B \ B \ A" by blast +declare subset_eq [code] + lemma [code]: "a \ A \ (\x\A. x = a)" unfolding bex_triv_one_point1 .. @@ -64,7 +66,7 @@ lemma member_nil [simp]: "member [] = (\x. False)" -proof +proof (rule ext) fix x show "member [] x = False" unfolding member_def by simp qed @@ -240,30 +242,6 @@ nonfix subset; *} -subsubsection {* type serializations *} - -types_code - set ("_ list") -attach (term_of) {* -fun term_of_set f T [] = Const ("{}", Type ("set", [T])) - | term_of_set f T (x :: xs) = Const ("insert", - T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs; -*} -attach (test) {* -fun gen_set' aG aT i j = frequency - [(i, fn () => - let - val (x, t) = aG j; - val (xs, ts) = gen_set' aG aT (i-1) j - in - (x :: xs, fn () => Const ("insert", - aT --> Type ("set", [aT]) --> Type ("set", [aT])) $ t () $ ts ()) - end), - (1, fn () => ([], fn () => Const ("{}", Type ("set", [aT]))))] () -and gen_set aG aT i = gen_set' aG aT i i; -*} - - subsubsection {* const serializations *} consts_code