# HG changeset patch
# User haftmann
# Date 1218459000 -7200
# Node ID 97d2a3797ce0cb8b9826dc12a687fadc2815dc73
# Parent  52971512d1a226421a5663ad2e046f55804c3107
rudimentary code setup for set operations

diff -r 52971512d1a2 -r 97d2a3797ce0 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Aug 11 14:49:53 2008 +0200
+++ b/src/HOL/Set.thy	Mon Aug 11 14:50:00 2008 +0200
@@ -324,8 +324,8 @@
 text {* Isomorphisms between predicates and sets. *}
 
 defs
-  mem_def: "x : S == S x"
-  Collect_def: "Collect P == P"
+  mem_def [code func]: "x : S == S x"
+  Collect_def [code func]: "Collect P == P"
 
 defs
   Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
@@ -2061,7 +2061,7 @@
 
 constdefs
   vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
-  "f -` B == {x. f x : B}"
+  [code func del]: "f -` B == {x. f x : B}"
 
 
 subsubsection {* Basic rules *}
@@ -2174,22 +2174,6 @@
   order_trans_rules set_rev_mp set_mp
 
 
-subsection {* Dense orders *}
-
-class dense_linear_order = linorder + 
-  assumes gt_ex: "\<exists>y. x < y" 
-  and lt_ex: "\<exists>y. y < x"
-  and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
-  (*see further theory Dense_Linear_Order*)
-begin
-
-lemma interval_empty_iff:
-  "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
-  by (auto dest: dense)
-
-end
-
-
 subsection {* Least value operator *}
 
 lemma Least_mono:
@@ -2203,6 +2187,28 @@
   done
 
 
+subsection {* Rudimentary code generation *}
+
+lemma empty_code [code func]: "{} x \<longleftrightarrow> False"
+  unfolding empty_def Collect_def ..
+
+lemma UNIV_code [code func]: "UNIV x \<longleftrightarrow> True"
+  unfolding UNIV_def Collect_def ..
+
+lemma insert_code [code func]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
+  unfolding insert_def Collect_def mem_def Un_def by auto
+
+lemma inter_code [code func]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
+  unfolding Int_def Collect_def mem_def ..
+
+lemma union_code [code func]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
+  unfolding Un_def Collect_def mem_def ..
+
+lemma vimage_code [code func]: "(f -` A) x = A (f x)"
+  unfolding vimage_def Collect_def mem_def ..
+
+
+
 subsection {* Basic ML bindings *}
 
 ML {*