src/HOL/Library/Executable_Set.thy
changeset 24423 ae9cd0e92423
parent 23854 688a8a7bcd4e
child 25595 6c48275f9c76
     1.1 --- a/src/HOL/Library/Executable_Set.thy	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -11,24 +11,10 @@
     1.4  
     1.5  subsection {* Definitional rewrites *}
     1.6  
     1.7 -instance set :: (eq) eq ..
     1.8 -
     1.9  lemma [code target: Set]:
    1.10    "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    1.11    by blast
    1.12  
    1.13 -lemma [code func]:
    1.14 -  "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    1.15 -  by blast
    1.16 -
    1.17 -lemma [code func]:
    1.18 -  "(A\<Colon>'a\<Colon>eq set) \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    1.19 -  unfolding subset_def ..
    1.20 -
    1.21 -lemma [code func]:
    1.22 -  "(A\<Colon>'a\<Colon>eq set) \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
    1.23 -  by blast
    1.24 -
    1.25  lemma [code]:
    1.26    "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
    1.27    unfolding bex_triv_one_point1 ..
    1.28 @@ -37,8 +23,6 @@
    1.29    filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.30    "filter_set P xs = {x\<in>xs. P x}"
    1.31  
    1.32 -lemmas [symmetric, code inline] = filter_set_def
    1.33 -
    1.34  
    1.35  subsection {* Operations on lists *}
    1.36  
    1.37 @@ -256,74 +240,6 @@
    1.38  nonfix subset;
    1.39  *}
    1.40  
    1.41 -code_modulename SML
    1.42 -  Executable_Set List
    1.43 -  Set List
    1.44 -
    1.45 -code_modulename OCaml
    1.46 -  Executable_Set List
    1.47 -  Set List
    1.48 -
    1.49 -code_modulename Haskell
    1.50 -  Executable_Set List
    1.51 -  Set List
    1.52 -
    1.53 -definition [code inline]:
    1.54 -  "empty_list = []"
    1.55 -
    1.56 -lemma [code func]:
    1.57 -  "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
    1.58 -
    1.59 -lemma [code func]:
    1.60 -  "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
    1.61 -
    1.62 -lemma [code func]:
    1.63 -  "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
    1.64 -
    1.65 -lemma [code func]:
    1.66 -  "(op -) (xs \<Colon> 'a\<Colon>eq set) = (op -) (xs \<Colon> 'a\<Colon>eq set)" ..
    1.67 -
    1.68 -lemma [code func]:
    1.69 -  "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
    1.70 -
    1.71 -lemma [code func]:
    1.72 -  "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
    1.73 -
    1.74 -lemma [code func]:
    1.75 -  "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
    1.76 -
    1.77 -lemma [code func]:
    1.78 -  "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
    1.79 -
    1.80 -lemma [code func]:
    1.81 -  "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
    1.82 -
    1.83 -lemma [code func]:
    1.84 -  "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
    1.85 -
    1.86 -lemma [code func]:
    1.87 -  "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
    1.88 -
    1.89 -lemma [code func]:
    1.90 -  "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
    1.91 -
    1.92 -
    1.93 -code_abstype "'a set" "'a list" where
    1.94 -  "{}" \<equiv> empty_list
    1.95 -  insert \<equiv> insertl
    1.96 -  "op \<union>" \<equiv> unionl
    1.97 -  "op \<inter>" \<equiv> intersect
    1.98 -  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
    1.99 -  image \<equiv> map_distinct
   1.100 -  Union \<equiv> unions
   1.101 -  Inter \<equiv> intersects
   1.102 -  UNION \<equiv> map_union
   1.103 -  INTER \<equiv> map_inter
   1.104 -  Ball \<equiv> Blall
   1.105 -  Bex \<equiv> Blex
   1.106 -  filter_set \<equiv> filter
   1.107 -
   1.108 -
   1.109  subsubsection {* type serializations *}
   1.110  
   1.111  types_code