src/HOL/Set.thy
 changeset 27824 97d2a3797ce0 parent 27418 564117b58d73 child 28562 4e74209f113e
```     1.1 --- a/src/HOL/Set.thy	Mon Aug 11 14:49:53 2008 +0200
1.2 +++ b/src/HOL/Set.thy	Mon Aug 11 14:50:00 2008 +0200
1.3 @@ -324,8 +324,8 @@
1.4  text {* Isomorphisms between predicates and sets. *}
1.5
1.6  defs
1.7 -  mem_def: "x : S == S x"
1.8 -  Collect_def: "Collect P == P"
1.9 +  mem_def [code func]: "x : S == S x"
1.10 +  Collect_def [code func]: "Collect P == P"
1.11
1.12  defs
1.13    Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
1.14 @@ -2061,7 +2061,7 @@
1.15
1.16  constdefs
1.17    vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
1.18 -  "f -` B == {x. f x : B}"
1.19 +  [code func del]: "f -` B == {x. f x : B}"
1.20
1.21
1.22  subsubsection {* Basic rules *}
1.23 @@ -2174,22 +2174,6 @@
1.24    order_trans_rules set_rev_mp set_mp
1.25
1.26
1.27 -subsection {* Dense orders *}
1.28 -
1.29 -class dense_linear_order = linorder +
1.30 -  assumes gt_ex: "\<exists>y. x < y"
1.31 -  and lt_ex: "\<exists>y. y < x"
1.32 -  and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
1.33 -  (*see further theory Dense_Linear_Order*)
1.34 -begin
1.35 -
1.36 -lemma interval_empty_iff:
1.37 -  "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
1.38 -  by (auto dest: dense)
1.39 -
1.40 -end
1.41 -
1.42 -
1.43  subsection {* Least value operator *}
1.44
1.45  lemma Least_mono:
1.46 @@ -2203,6 +2187,28 @@
1.47    done
1.48
1.49
1.50 +subsection {* Rudimentary code generation *}
1.51 +
1.52 +lemma empty_code [code func]: "{} x \<longleftrightarrow> False"
1.53 +  unfolding empty_def Collect_def ..
1.54 +
1.55 +lemma UNIV_code [code func]: "UNIV x \<longleftrightarrow> True"
1.56 +  unfolding UNIV_def Collect_def ..
1.57 +
1.58 +lemma insert_code [code func]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
1.59 +  unfolding insert_def Collect_def mem_def Un_def by auto
1.60 +
1.61 +lemma inter_code [code func]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
1.62 +  unfolding Int_def Collect_def mem_def ..
1.63 +
1.64 +lemma union_code [code func]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
1.65 +  unfolding Un_def Collect_def mem_def ..
1.66 +
1.67 +lemma vimage_code [code func]: "(f -` A) x = A (f x)"
1.68 +  unfolding vimage_def Collect_def mem_def ..
1.69 +
1.70 +
1.71 +
1.72  subsection {* Basic ML bindings *}
1.73
1.74  ML {*
```