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 {*