--- 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 \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
by blast
+declare subset_eq [code]
+
lemma [code]:
"a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
unfolding bex_triv_one_point1 ..
@@ -64,7 +66,7 @@
lemma member_nil [simp]:
"member [] = (\<lambda>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