uniform naming conventions for CG theories
authorhaftmann
Thu Jul 19 21:47:39 2007 +0200 (2007-07-19)
changeset 23854688a8a7bcd4e
parent 23853 2c69bb1374b8
child 23855 b1a754e544b6
uniform naming conventions for CG theories
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Extraction/Pigeonhole.thy
src/HOL/Extraction/ROOT.ML
src/HOL/IsaMakefile
src/HOL/Library/EfficientNat.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/ExecutableRat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Library/Executable_Rat.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Library/Graphs.thy
src/HOL/Library/Library.thy
src/HOL/Library/MLString.thy
src/HOL/Library/ML_String.thy
src/HOL/Library/Pure_term.thy
src/HOL/Library/SCT_Implementation.thy
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/ex/Codegenerator_Rat.thy
src/HOL/ex/NBE.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/Reflected_Presburger.thy
     1.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Thu Jul 19 21:47:38 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Thu Jul 19 21:47:39 2007 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Quatifier elimination for R(0,1,+,<) *}
     1.5  
     1.6  theory ReflectedFerrack
     1.7 -  imports GCD Real EfficientNat
     1.8 +  imports GCD Real Efficient_Nat
     1.9    uses ("linreif.ML") ("linrtac.ML")
    1.10  begin
    1.11  
     2.1 --- a/src/HOL/Extraction/Pigeonhole.thy	Thu Jul 19 21:47:38 2007 +0200
     2.2 +++ b/src/HOL/Extraction/Pigeonhole.thy	Thu Jul 19 21:47:39 2007 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* The pigeonhole principle *}
     2.5  
     2.6  theory Pigeonhole
     2.7 -imports EfficientNat
     2.8 +imports Efficient_Nat
     2.9  begin
    2.10  
    2.11  text {*
     3.1 --- a/src/HOL/Extraction/ROOT.ML	Thu Jul 19 21:47:38 2007 +0200
     3.2 +++ b/src/HOL/Extraction/ROOT.ML	Thu Jul 19 21:47:39 2007 +0200
     3.3 @@ -11,5 +11,5 @@
     3.4     time_use_thy "QuotRem";
     3.5     time_use_thy "Warshall";
     3.6     time_use_thy "Higman";
     3.7 -   no_document time_use_thy "EfficientNat";
     3.8 +   no_document time_use_thy "Efficient_Nat";
     3.9     time_use_thy "Pigeonhole");
     4.1 --- a/src/HOL/IsaMakefile	Thu Jul 19 21:47:38 2007 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Thu Jul 19 21:47:39 2007 +0200
     4.3 @@ -201,10 +201,9 @@
     4.4  
     4.5  $(LOG)/HOL-Library.gz: $(OUT)/HOL \
     4.6    Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
     4.7 -  Library/EfficientNat.thy Library/ExecutableSet.thy \
     4.8 -  Library/ExecutableRat.thy \
     4.9 -  Library/Executable_Real.thy \
    4.10 -  Library/MLString.thy Library/Infinite_Set.thy \
    4.11 +  Library/Efficient_Nat.thy Library/Executable_Set.thy \
    4.12 +  Library/Executable_Rat.thy Library/Executable_Real.thy \
    4.13 +  Library/ML_Int.thy Library/ML_String.thy Library/Infinite_Set.thy \
    4.14    Library/FuncSet.thy Library/Library.thy \
    4.15    Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \
    4.16    Library/NatPair.thy \
    4.17 @@ -538,7 +537,7 @@
    4.18  
    4.19  HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
    4.20  
    4.21 -$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/ExecutableSet.thy \
    4.22 +$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \
    4.23    MicroJava/ROOT.ML \
    4.24    MicroJava/Comp/AuxLemmas.thy \
    4.25    MicroJava/Comp/CorrComp.thy \
    4.26 @@ -604,7 +603,7 @@
    4.27  
    4.28  HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
    4.29  
    4.30 -$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/EfficientNat.thy \
    4.31 +$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy \
    4.32    Extraction/Higman.thy Extraction/ROOT.ML Extraction/Pigeonhole.thy \
    4.33    Extraction/QuotRem.thy \
    4.34    Extraction/Warshall.thy Extraction/document/root.tex \
     5.1 --- a/src/HOL/Library/EfficientNat.thy	Thu Jul 19 21:47:38 2007 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,407 +0,0 @@
     5.4 -(*  Title:      HOL/Library/EfficientNat.thy
     5.5 -    ID:         $Id$
     5.6 -    Author:     Stefan Berghofer, TU Muenchen
     5.7 -*)
     5.8 -
     5.9 -header {* Implementation of natural numbers by integers *}
    5.10 -
    5.11 -theory EfficientNat
    5.12 -imports Main Pretty_Int
    5.13 -begin
    5.14 -
    5.15 -text {*
    5.16 -When generating code for functions on natural numbers, the canonical
    5.17 -representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for
    5.18 -computations involving large numbers. The efficiency of the generated
    5.19 -code can be improved drastically by implementing natural numbers by
    5.20 -integers. To do this, just include this theory.
    5.21 -*}
    5.22 -
    5.23 -subsection {* Logical rewrites *}
    5.24 -
    5.25 -text {*
    5.26 -  An int-to-nat conversion
    5.27 -  restricted to non-negative ints (in contrast to @{const nat}).
    5.28 -  Note that this restriction has no logical relevance and
    5.29 -  is just a kind of proof hint -- nothing prevents you from 
    5.30 -  writing nonsense like @{term "nat_of_int (-4)"}
    5.31 -*}
    5.32 -
    5.33 -definition
    5.34 -  nat_of_int :: "int \<Rightarrow> nat" where
    5.35 -  "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
    5.36 -
    5.37 -definition
    5.38 -  int' :: "nat \<Rightarrow> int" where
    5.39 -  "int' n = of_nat n"
    5.40 -
    5.41 -lemma int'_Suc [simp]: "int' (Suc n) = 1 + int' n"
    5.42 -unfolding int'_def by simp
    5.43 -
    5.44 -lemma int'_add: "int' (m + n) = int' m + int' n"
    5.45 -unfolding int'_def by (rule of_nat_add)
    5.46 -
    5.47 -lemma int'_mult: "int' (m * n) = int' m * int' n"
    5.48 -unfolding int'_def by (rule of_nat_mult)
    5.49 -
    5.50 -lemma nat_of_int_of_number_of:
    5.51 -  fixes k
    5.52 -  assumes "k \<ge> 0"
    5.53 -  shows "number_of k = nat_of_int (number_of k)"
    5.54 -  unfolding nat_of_int_def [OF assms] nat_number_of_def number_of_is_id ..
    5.55 -
    5.56 -lemma nat_of_int_of_number_of_aux:
    5.57 -  fixes k
    5.58 -  assumes "Numeral.Pls \<le> k \<equiv> True"
    5.59 -  shows "k \<ge> 0"
    5.60 -  using assms unfolding Pls_def by simp
    5.61 -
    5.62 -lemma nat_of_int_int:
    5.63 -  "nat_of_int (int' n) = n"
    5.64 -  using nat_of_int_def int'_def by simp
    5.65 -
    5.66 -lemma eq_nat_of_int: "int' n = x \<Longrightarrow> n = nat_of_int x"
    5.67 -by (erule subst, simp only: nat_of_int_int)
    5.68 -
    5.69 -text {*
    5.70 -  Case analysis on natural numbers is rephrased using a conditional
    5.71 -  expression:
    5.72 -*}
    5.73 -
    5.74 -lemma [code unfold, code inline del]:
    5.75 -  "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
    5.76 -proof -
    5.77 -  have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))"
    5.78 -  proof -
    5.79 -    fix f g n
    5.80 -    show "nat_case f g n = (if n = 0 then f else g (n - 1))"
    5.81 -      by (cases n) simp_all
    5.82 -  qed
    5.83 -  show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
    5.84 -    by (rule eq_reflection ext rewrite)+ 
    5.85 -qed
    5.86 -
    5.87 -lemma [code inline]:
    5.88 -  "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int' n - 1)))"
    5.89 -proof (rule ext)+
    5.90 -  fix f g n
    5.91 -  show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int' n - 1)))"
    5.92 -  by (cases n) (simp_all add: nat_of_int_int)
    5.93 -qed
    5.94 -
    5.95 -text {*
    5.96 -  Most standard arithmetic functions on natural numbers are implemented
    5.97 -  using their counterparts on the integers:
    5.98 -*}
    5.99 -
   5.100 -lemma [code func]: "0 = nat_of_int 0"
   5.101 -  by (simp add: nat_of_int_def)
   5.102 -lemma [code func, code inline]:  "1 = nat_of_int 1"
   5.103 -  by (simp add: nat_of_int_def)
   5.104 -lemma [code func]: "Suc n = nat_of_int (int' n + 1)"
   5.105 -  by (simp add: eq_nat_of_int)
   5.106 -lemma [code]: "m + n = nat (int' m + int' n)"
   5.107 -  by (simp add: int'_def nat_eq_iff2)
   5.108 -lemma [code func, code inline]: "m + n = nat_of_int (int' m + int' n)"
   5.109 -  by (simp add: eq_nat_of_int int'_add)
   5.110 -lemma [code, code inline]: "m - n = nat (int' m - int' n)"
   5.111 -  by (simp add: int'_def nat_eq_iff2 of_nat_diff)
   5.112 -lemma [code]: "m * n = nat (int' m * int' n)"
   5.113 -  unfolding int'_def
   5.114 -  by (simp add: of_nat_mult [symmetric] del: of_nat_mult)
   5.115 -lemma [code func, code inline]: "m * n = nat_of_int (int' m * int' n)"
   5.116 -  by (simp add: eq_nat_of_int int'_mult)
   5.117 -lemma [code]: "m div n = nat (int' m div int' n)"
   5.118 -  unfolding int'_def zdiv_int [symmetric] by simp
   5.119 -lemma [code func]: "m div n = fst (Divides.divmod m n)"
   5.120 -  unfolding divmod_def by simp
   5.121 -lemma [code]: "m mod n = nat (int' m mod int' n)"
   5.122 -  unfolding int'_def zmod_int [symmetric] by simp
   5.123 -lemma [code func]: "m mod n = snd (Divides.divmod m n)"
   5.124 -  unfolding divmod_def by simp
   5.125 -lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int' m < int' n)"
   5.126 -  unfolding int'_def by simp
   5.127 -lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int' m \<le> int' n)"
   5.128 -  unfolding int'_def by simp
   5.129 -lemma [code func, code inline]: "m = n \<longleftrightarrow> int' m = int' n"
   5.130 -  unfolding int'_def by simp
   5.131 -lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
   5.132 -proof (cases "k < 0")
   5.133 -  case True then show ?thesis by simp
   5.134 -next
   5.135 -  case False then show ?thesis by (simp add: nat_of_int_def)
   5.136 -qed
   5.137 -lemma [code func]:
   5.138 -  "int_aux i n = (if int' n = 0 then i else int_aux (i + 1) (nat_of_int (int' n - 1)))"
   5.139 -proof -
   5.140 -  have "0 < n \<Longrightarrow> int' n = 1 + int' (nat_of_int (int' n - 1))"
   5.141 -  proof -
   5.142 -    assume prem: "n > 0"
   5.143 -    then have "int' n - 1 \<ge> 0" unfolding int'_def by auto
   5.144 -    then have "nat_of_int (int' n - 1) = nat (int' n - 1)" by (simp add: nat_of_int_def)
   5.145 -    with prem show "int' n = 1 + int' (nat_of_int (int' n - 1))" unfolding int'_def by simp
   5.146 -  qed
   5.147 -  then show ?thesis unfolding int_aux_def int'_def by simp
   5.148 -qed
   5.149 -
   5.150 -lemma div_nat_code [code func]:
   5.151 -  "m div k = nat_of_int (fst (divAlg (int' m, int' k)))"
   5.152 -  unfolding div_def [symmetric] int'_def zdiv_int [symmetric]
   5.153 -  unfolding int'_def [symmetric] nat_of_int_int ..
   5.154 -
   5.155 -lemma mod_nat_code [code func]:
   5.156 -  "m mod k = nat_of_int (snd (divAlg (int' m, int' k)))"
   5.157 -  unfolding mod_def [symmetric] int'_def zmod_int [symmetric]
   5.158 -  unfolding int'_def [symmetric] nat_of_int_int ..
   5.159 -
   5.160 -subsection {* Code generator setup for basic functions *}
   5.161 -
   5.162 -text {*
   5.163 -  @{typ nat} is no longer a datatype but embedded into the integers.
   5.164 -*}
   5.165 -
   5.166 -code_datatype nat_of_int
   5.167 -
   5.168 -code_type nat
   5.169 -  (SML "IntInf.int")
   5.170 -  (OCaml "Big'_int.big'_int")
   5.171 -  (Haskell "Integer")
   5.172 -
   5.173 -types_code
   5.174 -  nat ("int")
   5.175 -attach (term_of) {*
   5.176 -val term_of_nat = HOLogic.mk_number HOLogic.natT o IntInf.fromInt;
   5.177 -*}
   5.178 -attach (test) {*
   5.179 -fun gen_nat i = random_range 0 i;
   5.180 -*}
   5.181 -
   5.182 -consts_code
   5.183 -  "0 \<Colon> nat" ("0")
   5.184 -  Suc ("(_ + 1)")
   5.185 -
   5.186 -text {*
   5.187 -  Since natural numbers are implemented
   5.188 -  using integers, the coercion function @{const "int"} of type
   5.189 -  @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function,
   5.190 -  likewise @{const nat_of_int} of type @{typ "int \<Rightarrow> nat"}.
   5.191 -  For the @{const "nat"} function for converting an integer to a natural
   5.192 -  number, we give a specific implementation using an ML function that
   5.193 -  returns its input value, provided that it is non-negative, and otherwise
   5.194 -  returns @{text "0"}.
   5.195 -*}
   5.196 -
   5.197 -consts_code
   5.198 -  int' ("(_)")
   5.199 -  nat ("\<module>nat")
   5.200 -attach {*
   5.201 -fun nat i = if i < 0 then 0 else i;
   5.202 -*}
   5.203 -
   5.204 -code_const int'
   5.205 -  (SML "_")
   5.206 -  (OCaml "_")
   5.207 -  (Haskell "_")
   5.208 -
   5.209 -code_const nat_of_int
   5.210 -  (SML "_")
   5.211 -  (OCaml "_")
   5.212 -  (Haskell "_")
   5.213 -
   5.214 -
   5.215 -subsection {* Preprocessors *}
   5.216 -
   5.217 -text {*
   5.218 -  Natural numerals should be expressed using @{const nat_of_int}.
   5.219 -*}
   5.220 -
   5.221 -lemmas [code inline del] = nat_number_of_def
   5.222 -
   5.223 -ML {*
   5.224 -fun nat_of_int_of_number_of thy cts =
   5.225 -  let
   5.226 -    val simplify_less = Simplifier.rewrite 
   5.227 -      (HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code}));
   5.228 -    fun mk_rew (t, ty) =
   5.229 -      if ty = HOLogic.natT andalso IntInf.<= (0, HOLogic.dest_numeral t) then
   5.230 -        Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t)
   5.231 -        |> simplify_less
   5.232 -        |> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm])
   5.233 -        |> (fn thm => @{thm nat_of_int_of_number_of} OF [thm])
   5.234 -        |> (fn thm => @{thm eq_reflection} OF [thm])
   5.235 -        |> SOME
   5.236 -      else NONE
   5.237 -  in
   5.238 -    fold (HOLogic.add_numerals o Thm.term_of) cts []
   5.239 -    |> map_filter mk_rew
   5.240 -  end;
   5.241 -*}
   5.242 -
   5.243 -setup {*
   5.244 -  CodegenData.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of)
   5.245 -*}
   5.246 -
   5.247 -text {*
   5.248 -  In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
   5.249 -  a constructor term. Therefore, all occurrences of this term in a position
   5.250 -  where a pattern is expected (i.e.\ on the left-hand side of a recursion
   5.251 -  equation or in the arguments of an inductive relation in an introduction
   5.252 -  rule) must be eliminated.
   5.253 -  This can be accomplished by applying the following transformation rules:
   5.254 -*}
   5.255 -
   5.256 -theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
   5.257 -  f n = (if n = 0 then g else h (n - 1))"
   5.258 -  by (case_tac n) simp_all
   5.259 -
   5.260 -theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
   5.261 -  by (case_tac n) simp_all
   5.262 -
   5.263 -text {*
   5.264 -  The rules above are built into a preprocessor that is plugged into
   5.265 -  the code generator. Since the preprocessor for introduction rules
   5.266 -  does not know anything about modes, some of the modes that worked
   5.267 -  for the canonical representation of natural numbers may no longer work.
   5.268 -*}
   5.269 -
   5.270 -(*<*)
   5.271 -
   5.272 -ML {*
   5.273 -local
   5.274 -  val Suc_if_eq = thm "Suc_if_eq";
   5.275 -  val Suc_clause = thm "Suc_clause";
   5.276 -  fun contains_suc t = member (op =) (term_consts t) "Suc";
   5.277 -in
   5.278 -
   5.279 -fun remove_suc thy thms =
   5.280 -  let
   5.281 -    val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
   5.282 -    val vname = Name.variant (map fst
   5.283 -      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
   5.284 -    val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
   5.285 -    fun lhs_of th = snd (Thm.dest_comb
   5.286 -      (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
   5.287 -    fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
   5.288 -    fun find_vars ct = (case term_of ct of
   5.289 -        (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
   5.290 -      | _ $ _ =>
   5.291 -        let val (ct1, ct2) = Thm.dest_comb ct
   5.292 -        in 
   5.293 -          map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
   5.294 -          map (apfst (Thm.capply ct1)) (find_vars ct2)
   5.295 -        end
   5.296 -      | _ => []);
   5.297 -    val eqs = maps
   5.298 -      (fn th => map (pair th) (find_vars (lhs_of th))) thms;
   5.299 -    fun mk_thms (th, (ct, cv')) =
   5.300 -      let
   5.301 -        val th' =
   5.302 -          Thm.implies_elim
   5.303 -           (Conv.fconv_rule (Thm.beta_conversion true)
   5.304 -             (Drule.instantiate'
   5.305 -               [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
   5.306 -                 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
   5.307 -               Suc_if_eq')) (Thm.forall_intr cv' th)
   5.308 -      in
   5.309 -        case map_filter (fn th'' =>
   5.310 -            SOME (th'', singleton
   5.311 -              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
   5.312 -          handle THM _ => NONE) thms of
   5.313 -            [] => NONE
   5.314 -          | thps =>
   5.315 -              let val (ths1, ths2) = split_list thps
   5.316 -              in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
   5.317 -      end
   5.318 -  in
   5.319 -    case get_first mk_thms eqs of
   5.320 -      NONE => thms
   5.321 -    | SOME x => remove_suc thy x
   5.322 -  end;
   5.323 -
   5.324 -fun eqn_suc_preproc thy ths =
   5.325 -  let
   5.326 -    val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
   5.327 -  in
   5.328 -    if forall (can dest) ths andalso
   5.329 -      exists (contains_suc o dest) ths
   5.330 -    then remove_suc thy ths else ths
   5.331 -  end;
   5.332 -
   5.333 -fun remove_suc_clause thy thms =
   5.334 -  let
   5.335 -    val Suc_clause' = Thm.transfer thy Suc_clause;
   5.336 -    val vname = Name.variant (map fst
   5.337 -      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
   5.338 -    fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
   5.339 -      | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
   5.340 -      | find_var _ = NONE;
   5.341 -    fun find_thm th =
   5.342 -      let val th' = Conv.fconv_rule ObjectLogic.atomize th
   5.343 -      in Option.map (pair (th, th')) (find_var (prop_of th')) end
   5.344 -  in
   5.345 -    case get_first find_thm thms of
   5.346 -      NONE => thms
   5.347 -    | SOME ((th, th'), (Sucv, v)) =>
   5.348 -        let
   5.349 -          val cert = cterm_of (Thm.theory_of_thm th);
   5.350 -          val th'' = ObjectLogic.rulify (Thm.implies_elim
   5.351 -            (Conv.fconv_rule (Thm.beta_conversion true)
   5.352 -              (Drule.instantiate' []
   5.353 -                [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
   5.354 -                   abstract_over (Sucv,
   5.355 -                     HOLogic.dest_Trueprop (prop_of th')))))),
   5.356 -                 SOME (cert v)] Suc_clause'))
   5.357 -            (Thm.forall_intr (cert v) th'))
   5.358 -        in
   5.359 -          remove_suc_clause thy (map (fn th''' =>
   5.360 -            if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
   5.361 -        end
   5.362 -  end;
   5.363 -
   5.364 -fun clause_suc_preproc thy ths =
   5.365 -  let
   5.366 -    val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
   5.367 -  in
   5.368 -    if forall (can (dest o concl_of)) ths andalso
   5.369 -      exists (fn th => member (op =) (foldr add_term_consts
   5.370 -        [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
   5.371 -    then remove_suc_clause thy ths else ths
   5.372 -  end;
   5.373 -
   5.374 -end; (*local*)
   5.375 -
   5.376 -fun lift_obj_eq f thy =
   5.377 -  map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
   5.378 -  #> f thy
   5.379 -  #> map (fn thm => thm RS @{thm eq_reflection})
   5.380 -  #> map (Conv.fconv_rule Drule.beta_eta_conversion)
   5.381 -*}
   5.382 -
   5.383 -setup {*
   5.384 -  Codegen.add_preprocessor eqn_suc_preproc
   5.385 -  #> Codegen.add_preprocessor clause_suc_preproc
   5.386 -  #> CodegenData.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
   5.387 -  #> CodegenData.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc)
   5.388 -*}
   5.389 -(*>*)
   5.390 -
   5.391 -
   5.392 -subsection {* Module names *}
   5.393 -
   5.394 -code_modulename SML
   5.395 -  Nat Integer
   5.396 -  Divides Integer
   5.397 -  EfficientNat Integer
   5.398 -
   5.399 -code_modulename OCaml
   5.400 -  Nat Integer
   5.401 -  Divides Integer
   5.402 -  EfficientNat Integer
   5.403 -
   5.404 -code_modulename Haskell
   5.405 -  Nat Integer
   5.406 -  EfficientNat Integer
   5.407 -
   5.408 -hide const nat_of_int int'
   5.409 -
   5.410 -end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jul 19 21:47:39 2007 +0200
     6.3 @@ -0,0 +1,408 @@
     6.4 +(*  Title:      HOL/Library/Efficient_Nat.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Stefan Berghofer, TU Muenchen
     6.7 +*)
     6.8 +
     6.9 +header {* Implementation of natural numbers by integers *}
    6.10 +
    6.11 +theory Efficient_Nat
    6.12 +imports Main Pretty_Int
    6.13 +begin
    6.14 +
    6.15 +text {*
    6.16 +When generating code for functions on natural numbers, the canonical
    6.17 +representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for
    6.18 +computations involving large numbers. The efficiency of the generated
    6.19 +code can be improved drastically by implementing natural numbers by
    6.20 +integers. To do this, just include this theory.
    6.21 +*}
    6.22 +
    6.23 +subsection {* Logical rewrites *}
    6.24 +
    6.25 +text {*
    6.26 +  An int-to-nat conversion
    6.27 +  restricted to non-negative ints (in contrast to @{const nat}).
    6.28 +  Note that this restriction has no logical relevance and
    6.29 +  is just a kind of proof hint -- nothing prevents you from 
    6.30 +  writing nonsense like @{term "nat_of_int (-4)"}
    6.31 +*}
    6.32 +
    6.33 +definition
    6.34 +  nat_of_int :: "int \<Rightarrow> nat" where
    6.35 +  "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
    6.36 +
    6.37 +definition
    6.38 +  int' :: "nat \<Rightarrow> int" where
    6.39 +  "int' n = of_nat n"
    6.40 +
    6.41 +lemma int'_Suc [simp]: "int' (Suc n) = 1 + int' n"
    6.42 +unfolding int'_def by simp
    6.43 +
    6.44 +lemma int'_add: "int' (m + n) = int' m + int' n"
    6.45 +unfolding int'_def by (rule of_nat_add)
    6.46 +
    6.47 +lemma int'_mult: "int' (m * n) = int' m * int' n"
    6.48 +unfolding int'_def by (rule of_nat_mult)
    6.49 +
    6.50 +lemma nat_of_int_of_number_of:
    6.51 +  fixes k
    6.52 +  assumes "k \<ge> 0"
    6.53 +  shows "number_of k = nat_of_int (number_of k)"
    6.54 +  unfolding nat_of_int_def [OF assms] nat_number_of_def number_of_is_id ..
    6.55 +
    6.56 +lemma nat_of_int_of_number_of_aux:
    6.57 +  fixes k
    6.58 +  assumes "Numeral.Pls \<le> k \<equiv> True"
    6.59 +  shows "k \<ge> 0"
    6.60 +  using assms unfolding Pls_def by simp
    6.61 +
    6.62 +lemma nat_of_int_int:
    6.63 +  "nat_of_int (int' n) = n"
    6.64 +  using nat_of_int_def int'_def by simp
    6.65 +
    6.66 +lemma eq_nat_of_int: "int' n = x \<Longrightarrow> n = nat_of_int x"
    6.67 +by (erule subst, simp only: nat_of_int_int)
    6.68 +
    6.69 +text {*
    6.70 +  Case analysis on natural numbers is rephrased using a conditional
    6.71 +  expression:
    6.72 +*}
    6.73 +
    6.74 +lemma [code unfold, code inline del]:
    6.75 +  "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
    6.76 +proof -
    6.77 +  have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))"
    6.78 +  proof -
    6.79 +    fix f g n
    6.80 +    show "nat_case f g n = (if n = 0 then f else g (n - 1))"
    6.81 +      by (cases n) simp_all
    6.82 +  qed
    6.83 +  show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
    6.84 +    by (rule eq_reflection ext rewrite)+ 
    6.85 +qed
    6.86 +
    6.87 +lemma [code inline]:
    6.88 +  "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int' n - 1)))"
    6.89 +proof (rule ext)+
    6.90 +  fix f g n
    6.91 +  show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int' n - 1)))"
    6.92 +  by (cases n) (simp_all add: nat_of_int_int)
    6.93 +qed
    6.94 +
    6.95 +text {*
    6.96 +  Most standard arithmetic functions on natural numbers are implemented
    6.97 +  using their counterparts on the integers:
    6.98 +*}
    6.99 +
   6.100 +lemma [code func]: "0 = nat_of_int 0"
   6.101 +  by (simp add: nat_of_int_def)
   6.102 +lemma [code func, code inline]:  "1 = nat_of_int 1"
   6.103 +  by (simp add: nat_of_int_def)
   6.104 +lemma [code func]: "Suc n = nat_of_int (int' n + 1)"
   6.105 +  by (simp add: eq_nat_of_int)
   6.106 +lemma [code]: "m + n = nat (int' m + int' n)"
   6.107 +  by (simp add: int'_def nat_eq_iff2)
   6.108 +lemma [code func, code inline]: "m + n = nat_of_int (int' m + int' n)"
   6.109 +  by (simp add: eq_nat_of_int int'_add)
   6.110 +lemma [code, code inline]: "m - n = nat (int' m - int' n)"
   6.111 +  by (simp add: int'_def nat_eq_iff2 of_nat_diff)
   6.112 +lemma [code]: "m * n = nat (int' m * int' n)"
   6.113 +  unfolding int'_def
   6.114 +  by (simp add: of_nat_mult [symmetric] del: of_nat_mult)
   6.115 +lemma [code func, code inline]: "m * n = nat_of_int (int' m * int' n)"
   6.116 +  by (simp add: eq_nat_of_int int'_mult)
   6.117 +lemma [code]: "m div n = nat (int' m div int' n)"
   6.118 +  unfolding int'_def zdiv_int [symmetric] by simp
   6.119 +lemma [code func]: "m div n = fst (Divides.divmod m n)"
   6.120 +  unfolding divmod_def by simp
   6.121 +lemma [code]: "m mod n = nat (int' m mod int' n)"
   6.122 +  unfolding int'_def zmod_int [symmetric] by simp
   6.123 +lemma [code func]: "m mod n = snd (Divides.divmod m n)"
   6.124 +  unfolding divmod_def by simp
   6.125 +lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int' m < int' n)"
   6.126 +  unfolding int'_def by simp
   6.127 +lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int' m \<le> int' n)"
   6.128 +  unfolding int'_def by simp
   6.129 +lemma [code func, code inline]: "m = n \<longleftrightarrow> int' m = int' n"
   6.130 +  unfolding int'_def by simp
   6.131 +lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
   6.132 +proof (cases "k < 0")
   6.133 +  case True then show ?thesis by simp
   6.134 +next
   6.135 +  case False then show ?thesis by (simp add: nat_of_int_def)
   6.136 +qed
   6.137 +lemma [code func]:
   6.138 +  "int_aux n i = (if int' n = 0 then i else int_aux (nat_of_int (int' n - 1)) (i + 1))"
   6.139 +proof -
   6.140 +  have "0 < n \<Longrightarrow> int' n = 1 + int' (nat_of_int (int' n - 1))"
   6.141 +  proof -
   6.142 +    assume prem: "n > 0"
   6.143 +    then have "int' n - 1 \<ge> 0" unfolding int'_def by auto
   6.144 +    then have "nat_of_int (int' n - 1) = nat (int' n - 1)" by (simp add: nat_of_int_def)
   6.145 +    with prem show "int' n = 1 + int' (nat_of_int (int' n - 1))" unfolding int'_def by simp
   6.146 +  qed
   6.147 +  then show ?thesis unfolding int_aux_def int'_def by auto
   6.148 +qed
   6.149 +
   6.150 +lemma div_nat_code [code func]:
   6.151 +  "m div k = nat_of_int (fst (divAlg (int' m, int' k)))"
   6.152 +  unfolding div_def [symmetric] int'_def zdiv_int [symmetric]
   6.153 +  unfolding int'_def [symmetric] nat_of_int_int ..
   6.154 +
   6.155 +lemma mod_nat_code [code func]:
   6.156 +  "m mod k = nat_of_int (snd (divAlg (int' m, int' k)))"
   6.157 +  unfolding mod_def [symmetric] int'_def zmod_int [symmetric]
   6.158 +  unfolding int'_def [symmetric] nat_of_int_int ..
   6.159 +
   6.160 +
   6.161 +subsection {* Code generator setup for basic functions *}
   6.162 +
   6.163 +text {*
   6.164 +  @{typ nat} is no longer a datatype but embedded into the integers.
   6.165 +*}
   6.166 +
   6.167 +code_datatype nat_of_int
   6.168 +
   6.169 +code_type nat
   6.170 +  (SML "IntInf.int")
   6.171 +  (OCaml "Big'_int.big'_int")
   6.172 +  (Haskell "Integer")
   6.173 +
   6.174 +types_code
   6.175 +  nat ("int")
   6.176 +attach (term_of) {*
   6.177 +val term_of_nat = HOLogic.mk_number HOLogic.natT o IntInf.fromInt;
   6.178 +*}
   6.179 +attach (test) {*
   6.180 +fun gen_nat i = random_range 0 i;
   6.181 +*}
   6.182 +
   6.183 +consts_code
   6.184 +  "0 \<Colon> nat" ("0")
   6.185 +  Suc ("(_ + 1)")
   6.186 +
   6.187 +text {*
   6.188 +  Since natural numbers are implemented
   6.189 +  using integers, the coercion function @{const "int"} of type
   6.190 +  @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function,
   6.191 +  likewise @{const nat_of_int} of type @{typ "int \<Rightarrow> nat"}.
   6.192 +  For the @{const "nat"} function for converting an integer to a natural
   6.193 +  number, we give a specific implementation using an ML function that
   6.194 +  returns its input value, provided that it is non-negative, and otherwise
   6.195 +  returns @{text "0"}.
   6.196 +*}
   6.197 +
   6.198 +consts_code
   6.199 +  int' ("(_)")
   6.200 +  nat ("\<module>nat")
   6.201 +attach {*
   6.202 +fun nat i = if i < 0 then 0 else i;
   6.203 +*}
   6.204 +
   6.205 +code_const int'
   6.206 +  (SML "_")
   6.207 +  (OCaml "_")
   6.208 +  (Haskell "_")
   6.209 +
   6.210 +code_const nat_of_int
   6.211 +  (SML "_")
   6.212 +  (OCaml "_")
   6.213 +  (Haskell "_")
   6.214 +
   6.215 +
   6.216 +subsection {* Preprocessors *}
   6.217 +
   6.218 +text {*
   6.219 +  Natural numerals should be expressed using @{const nat_of_int}.
   6.220 +*}
   6.221 +
   6.222 +lemmas [code inline del] = nat_number_of_def
   6.223 +
   6.224 +ML {*
   6.225 +fun nat_of_int_of_number_of thy cts =
   6.226 +  let
   6.227 +    val simplify_less = Simplifier.rewrite 
   6.228 +      (HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code}));
   6.229 +    fun mk_rew (t, ty) =
   6.230 +      if ty = HOLogic.natT andalso IntInf.<= (0, HOLogic.dest_numeral t) then
   6.231 +        Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t)
   6.232 +        |> simplify_less
   6.233 +        |> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm])
   6.234 +        |> (fn thm => @{thm nat_of_int_of_number_of} OF [thm])
   6.235 +        |> (fn thm => @{thm eq_reflection} OF [thm])
   6.236 +        |> SOME
   6.237 +      else NONE
   6.238 +  in
   6.239 +    fold (HOLogic.add_numerals o Thm.term_of) cts []
   6.240 +    |> map_filter mk_rew
   6.241 +  end;
   6.242 +*}
   6.243 +
   6.244 +setup {*
   6.245 +  CodegenData.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of)
   6.246 +*}
   6.247 +
   6.248 +text {*
   6.249 +  In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
   6.250 +  a constructor term. Therefore, all occurrences of this term in a position
   6.251 +  where a pattern is expected (i.e.\ on the left-hand side of a recursion
   6.252 +  equation or in the arguments of an inductive relation in an introduction
   6.253 +  rule) must be eliminated.
   6.254 +  This can be accomplished by applying the following transformation rules:
   6.255 +*}
   6.256 +
   6.257 +theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
   6.258 +  f n = (if n = 0 then g else h (n - 1))"
   6.259 +  by (case_tac n) simp_all
   6.260 +
   6.261 +theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
   6.262 +  by (case_tac n) simp_all
   6.263 +
   6.264 +text {*
   6.265 +  The rules above are built into a preprocessor that is plugged into
   6.266 +  the code generator. Since the preprocessor for introduction rules
   6.267 +  does not know anything about modes, some of the modes that worked
   6.268 +  for the canonical representation of natural numbers may no longer work.
   6.269 +*}
   6.270 +
   6.271 +(*<*)
   6.272 +
   6.273 +ML {*
   6.274 +local
   6.275 +  val Suc_if_eq = thm "Suc_if_eq";
   6.276 +  val Suc_clause = thm "Suc_clause";
   6.277 +  fun contains_suc t = member (op =) (term_consts t) "Suc";
   6.278 +in
   6.279 +
   6.280 +fun remove_suc thy thms =
   6.281 +  let
   6.282 +    val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
   6.283 +    val vname = Name.variant (map fst
   6.284 +      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
   6.285 +    val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
   6.286 +    fun lhs_of th = snd (Thm.dest_comb
   6.287 +      (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
   6.288 +    fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
   6.289 +    fun find_vars ct = (case term_of ct of
   6.290 +        (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
   6.291 +      | _ $ _ =>
   6.292 +        let val (ct1, ct2) = Thm.dest_comb ct
   6.293 +        in 
   6.294 +          map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
   6.295 +          map (apfst (Thm.capply ct1)) (find_vars ct2)
   6.296 +        end
   6.297 +      | _ => []);
   6.298 +    val eqs = maps
   6.299 +      (fn th => map (pair th) (find_vars (lhs_of th))) thms;
   6.300 +    fun mk_thms (th, (ct, cv')) =
   6.301 +      let
   6.302 +        val th' =
   6.303 +          Thm.implies_elim
   6.304 +           (Conv.fconv_rule (Thm.beta_conversion true)
   6.305 +             (Drule.instantiate'
   6.306 +               [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
   6.307 +                 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
   6.308 +               Suc_if_eq')) (Thm.forall_intr cv' th)
   6.309 +      in
   6.310 +        case map_filter (fn th'' =>
   6.311 +            SOME (th'', singleton
   6.312 +              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
   6.313 +          handle THM _ => NONE) thms of
   6.314 +            [] => NONE
   6.315 +          | thps =>
   6.316 +              let val (ths1, ths2) = split_list thps
   6.317 +              in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
   6.318 +      end
   6.319 +  in
   6.320 +    case get_first mk_thms eqs of
   6.321 +      NONE => thms
   6.322 +    | SOME x => remove_suc thy x
   6.323 +  end;
   6.324 +
   6.325 +fun eqn_suc_preproc thy ths =
   6.326 +  let
   6.327 +    val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
   6.328 +  in
   6.329 +    if forall (can dest) ths andalso
   6.330 +      exists (contains_suc o dest) ths
   6.331 +    then remove_suc thy ths else ths
   6.332 +  end;
   6.333 +
   6.334 +fun remove_suc_clause thy thms =
   6.335 +  let
   6.336 +    val Suc_clause' = Thm.transfer thy Suc_clause;
   6.337 +    val vname = Name.variant (map fst
   6.338 +      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
   6.339 +    fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
   6.340 +      | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
   6.341 +      | find_var _ = NONE;
   6.342 +    fun find_thm th =
   6.343 +      let val th' = Conv.fconv_rule ObjectLogic.atomize th
   6.344 +      in Option.map (pair (th, th')) (find_var (prop_of th')) end
   6.345 +  in
   6.346 +    case get_first find_thm thms of
   6.347 +      NONE => thms
   6.348 +    | SOME ((th, th'), (Sucv, v)) =>
   6.349 +        let
   6.350 +          val cert = cterm_of (Thm.theory_of_thm th);
   6.351 +          val th'' = ObjectLogic.rulify (Thm.implies_elim
   6.352 +            (Conv.fconv_rule (Thm.beta_conversion true)
   6.353 +              (Drule.instantiate' []
   6.354 +                [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
   6.355 +                   abstract_over (Sucv,
   6.356 +                     HOLogic.dest_Trueprop (prop_of th')))))),
   6.357 +                 SOME (cert v)] Suc_clause'))
   6.358 +            (Thm.forall_intr (cert v) th'))
   6.359 +        in
   6.360 +          remove_suc_clause thy (map (fn th''' =>
   6.361 +            if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
   6.362 +        end
   6.363 +  end;
   6.364 +
   6.365 +fun clause_suc_preproc thy ths =
   6.366 +  let
   6.367 +    val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
   6.368 +  in
   6.369 +    if forall (can (dest o concl_of)) ths andalso
   6.370 +      exists (fn th => member (op =) (foldr add_term_consts
   6.371 +        [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
   6.372 +    then remove_suc_clause thy ths else ths
   6.373 +  end;
   6.374 +
   6.375 +end; (*local*)
   6.376 +
   6.377 +fun lift_obj_eq f thy =
   6.378 +  map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
   6.379 +  #> f thy
   6.380 +  #> map (fn thm => thm RS @{thm eq_reflection})
   6.381 +  #> map (Conv.fconv_rule Drule.beta_eta_conversion)
   6.382 +*}
   6.383 +
   6.384 +setup {*
   6.385 +  Codegen.add_preprocessor eqn_suc_preproc
   6.386 +  #> Codegen.add_preprocessor clause_suc_preproc
   6.387 +  #> CodegenData.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
   6.388 +  #> CodegenData.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc)
   6.389 +*}
   6.390 +(*>*)
   6.391 +
   6.392 +
   6.393 +subsection {* Module names *}
   6.394 +
   6.395 +code_modulename SML
   6.396 +  Nat Integer
   6.397 +  Divides Integer
   6.398 +  Efficient_Nat Integer
   6.399 +
   6.400 +code_modulename OCaml
   6.401 +  Nat Integer
   6.402 +  Divides Integer
   6.403 +  Efficient_Nat Integer
   6.404 +
   6.405 +code_modulename Haskell
   6.406 +  Nat Integer
   6.407 +  Efficient_Nat Integer
   6.408 +
   6.409 +hide const nat_of_int int'
   6.410 +
   6.411 +end
     7.1 --- a/src/HOL/Library/ExecutableRat.thy	Thu Jul 19 21:47:38 2007 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,150 +0,0 @@
     7.4 -(*  Title:      HOL/Library/ExecutableRat.thy
     7.5 -    ID:         $Id$
     7.6 -    Author:     Florian Haftmann, TU Muenchen
     7.7 -*)
     7.8 -
     7.9 -header {* Executable implementation of rational numbers in HOL *}
    7.10 -
    7.11 -theory ExecutableRat
    7.12 -imports "~~/src/HOL/Real/Rational" "~~/src/HOL/NumberTheory/IntPrimes"
    7.13 -begin
    7.14 -
    7.15 -text {*
    7.16 -  Actually \emph{nothing} is proved about this implementation.
    7.17 -*}
    7.18 -
    7.19 -subsection {* Representation and operations of executable rationals *}
    7.20 -
    7.21 -datatype erat = Rat bool nat nat
    7.22 -
    7.23 -axiomatization
    7.24 -  div_zero :: erat
    7.25 -
    7.26 -fun
    7.27 -  common :: "(nat * nat) \<Rightarrow> (nat * nat) \<Rightarrow> (nat * nat) * nat" where
    7.28 -  "common (p1, q1) (p2, q2) = (
    7.29 -     let
    7.30 -       q' = q1 * q2 div gcd (q1, q2)
    7.31 -     in ((p1 * (q' div q1), p2 * (q' div q2)), q'))"
    7.32 -
    7.33 -definition
    7.34 -  minus_sign :: "nat \<Rightarrow> nat \<Rightarrow> bool * nat" where
    7.35 -  "minus_sign n m = (if n < m then (False, m - n) else (True, n - m))"
    7.36 -
    7.37 -fun
    7.38 -  add_sign :: "bool * nat \<Rightarrow> bool * nat \<Rightarrow> bool * nat" where
    7.39 -  "add_sign (True, n) (True, m) = (True, n + m)"
    7.40 -| "add_sign (False, n) (False, m) = (False, n + m)"
    7.41 -| "add_sign (True, n) (False, m) = minus_sign n m"
    7.42 -| "add_sign (False, n) (True, m) = minus_sign m n"
    7.43 -
    7.44 -definition
    7.45 -  erat_of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" where
    7.46 -  "erat_of_quotient k1 k2 = (
    7.47 -    let
    7.48 -      l1 = nat (abs k1);
    7.49 -      l2 = nat (abs k2);
    7.50 -      m = gcd (l1, l2)
    7.51 -    in Rat (k1 \<le> 0 \<longleftrightarrow> k2 \<le> 0) (l1 div m) (l2 div m))"
    7.52 -
    7.53 -instance erat :: zero
    7.54 -  zero_rat_def: "0 \<equiv> Rat True 0 1" ..
    7.55 -
    7.56 -instance erat :: one
    7.57 -  one_rat_def: "1 \<equiv> Rat True 1 1" ..
    7.58 -
    7.59 -instance erat :: plus
    7.60 -  add_rat_def: "r + s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
    7.61 -        let
    7.62 -          ((r1, r2), den) = common (p1, q1) (p2, q2);
    7.63 -          (sign, num) = add_sign (a1, r1) (a2, r2)
    7.64 -        in Rat sign num den" ..
    7.65 -
    7.66 -instance erat :: minus
    7.67 -  uminus_rat_def: "- r \<equiv> case r of Rat a p q \<Rightarrow>
    7.68 -        if p = 0 then Rat True 0 1
    7.69 -        else Rat (\<not> a) p q" ..
    7.70 -  
    7.71 -instance erat :: times
    7.72 -  times_rat_def: "r * s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
    7.73 -        let
    7.74 -          p = p1 * p2;
    7.75 -          q = q1 * q2;
    7.76 -          m = gcd (p, q)
    7.77 -        in Rat (a1 = a2) (p div m) (q div m)" ..
    7.78 -
    7.79 -instance erat :: inverse
    7.80 -  inverse_rat_def: "inverse r \<equiv> case r of Rat a p q \<Rightarrow>
    7.81 -        if p = 0 then div_zero
    7.82 -        else Rat a q p" ..
    7.83 -
    7.84 -instance erat :: ord
    7.85 -  le_rat_def: "r1 \<le> r2 \<equiv> case r1 of Rat a1 p1 q1 \<Rightarrow> case r2 of Rat a2 p2 q2 \<Rightarrow>
    7.86 -        (\<not> a1 \<and> a2) \<or>
    7.87 -        (\<not> (a1 \<and> \<not> a2) \<and>
    7.88 -          (let
    7.89 -            ((r1, r2), dummy) = common (p1, q1) (p2, q2)
    7.90 -          in if a1 then r1 \<le> r2 else r2 \<le> r1))" ..
    7.91 -
    7.92 -
    7.93 -subsection {* Code generator setup *}
    7.94 -
    7.95 -subsubsection {* code lemmas *}
    7.96 -
    7.97 -lemma number_of_rat [code unfold]:
    7.98 -  "(number_of k \<Colon> rat) = Fract k 1"
    7.99 -  unfolding Fract_of_int_eq rat_number_of_def by simp
   7.100 -
   7.101 -lemma rat_minus [code func]:
   7.102 -  "(a\<Colon>rat) - b = a + (- b)" unfolding diff_minus ..
   7.103 -
   7.104 -lemma rat_divide [code func]:
   7.105 -  "(a\<Colon>rat) / b = a * inverse b" unfolding divide_inverse ..
   7.106 -
   7.107 -instance rat :: eq ..
   7.108 -
   7.109 -subsubsection {* names *}
   7.110 -
   7.111 -code_modulename SML
   7.112 -  ExecutableRat Rational
   7.113 -
   7.114 -code_modulename OCaml
   7.115 -  ExecutableRat Rational
   7.116 -
   7.117 -code_modulename Haskell
   7.118 -  ExecutableRat Rational
   7.119 -
   7.120 -subsubsection {* rat as abstype *}
   7.121 -
   7.122 -code_const div_zero
   7.123 -  (SML "raise/ Fail/ \"Division by zero\"")
   7.124 -  (OCaml "failwith \"Division by zero\"")
   7.125 -  (Haskell "error/ \"Division by zero\"")
   7.126 -
   7.127 -code_abstype rat erat where
   7.128 -  Fract \<equiv> erat_of_quotient
   7.129 -  "0 \<Colon> rat" \<equiv> "0 \<Colon> erat"
   7.130 -  "1 \<Colon> rat" \<equiv> "1 \<Colon> erat"
   7.131 -  "op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
   7.132 -  "uminus \<Colon> rat \<Rightarrow> rat" \<equiv> "uminus \<Colon> erat \<Rightarrow> erat"
   7.133 -  "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
   7.134 -  "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
   7.135 -  "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv>  "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
   7.136 -  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
   7.137 -
   7.138 -types_code
   7.139 -  rat ("{*erat*}")
   7.140 -
   7.141 -consts_code
   7.142 -  div_zero ("(raise/ (Fail/ \"Division by zero\"))")
   7.143 -  Fract ("({*erat_of_quotient*} (_) (_))")
   7.144 -  "0 \<Colon> rat" ("({*Rat True 0 1*})")
   7.145 -  "1 \<Colon> rat" ("({*Rat True 1 1*})")
   7.146 -  "plus \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   7.147 -  "uminus \<Colon> rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))")
   7.148 -  "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   7.149 -  "inverse \<Colon> rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))")
   7.150 -  "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   7.151 -  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   7.152 -
   7.153 -end
     8.1 --- a/src/HOL/Library/ExecutableSet.thy	Thu Jul 19 21:47:38 2007 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,360 +0,0 @@
     8.4 -(*  Title:      HOL/Library/ExecutableSet.thy
     8.5 -    ID:         $Id$
     8.6 -    Author:     Stefan Berghofer, TU Muenchen
     8.7 -*)
     8.8 -
     8.9 -header {* Implementation of finite sets by lists *}
    8.10 -
    8.11 -theory ExecutableSet
    8.12 -imports Main
    8.13 -begin
    8.14 -
    8.15 -subsection {* Definitional rewrites *}
    8.16 -
    8.17 -instance set :: (eq) eq ..
    8.18 -
    8.19 -lemma [code target: Set]:
    8.20 -  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    8.21 -  by blast
    8.22 -
    8.23 -lemma [code func]:
    8.24 -  "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    8.25 -  by blast
    8.26 -
    8.27 -lemma [code func]:
    8.28 -  "(A\<Colon>'a\<Colon>eq set) \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    8.29 -  unfolding subset_def ..
    8.30 -
    8.31 -lemma [code func]:
    8.32 -  "(A\<Colon>'a\<Colon>eq set) \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
    8.33 -  by blast
    8.34 -
    8.35 -lemma [code]:
    8.36 -  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
    8.37 -  unfolding bex_triv_one_point1 ..
    8.38 -
    8.39 -definition
    8.40 -  filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    8.41 -  "filter_set P xs = {x\<in>xs. P x}"
    8.42 -
    8.43 -lemmas [symmetric, code inline] = filter_set_def
    8.44 -
    8.45 -
    8.46 -subsection {* Operations on lists *}
    8.47 -
    8.48 -subsubsection {* Basic definitions *}
    8.49 -
    8.50 -definition
    8.51 -  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    8.52 -  "flip f a b = f b a"
    8.53 -
    8.54 -definition
    8.55 -  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
    8.56 -  "member xs x \<longleftrightarrow> x \<in> set xs"
    8.57 -
    8.58 -definition
    8.59 -  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    8.60 -  "insertl x xs = (if member xs x then xs else x#xs)"
    8.61 -
    8.62 -lemma [code target: List]: "member [] y \<longleftrightarrow> False"
    8.63 -  and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
    8.64 -  unfolding member_def by (induct xs) simp_all
    8.65 -
    8.66 -fun
    8.67 -  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    8.68 -  "drop_first f [] = []"
    8.69 -| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
    8.70 -declare drop_first.simps [code del]
    8.71 -declare drop_first.simps [code target: List]
    8.72 -
    8.73 -declare remove1.simps [code del]
    8.74 -lemma [code target: List]:
    8.75 -  "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
    8.76 -proof (cases "member xs x")
    8.77 -  case False thus ?thesis unfolding member_def by (induct xs) auto
    8.78 -next
    8.79 -  case True
    8.80 -  have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
    8.81 -  with True show ?thesis by simp
    8.82 -qed
    8.83 -
    8.84 -lemma member_nil [simp]:
    8.85 -  "member [] = (\<lambda>x. False)"
    8.86 -proof
    8.87 -  fix x
    8.88 -  show "member [] x = False" unfolding member_def by simp
    8.89 -qed
    8.90 -
    8.91 -lemma member_insertl [simp]:
    8.92 -  "x \<in> set (insertl x xs)"
    8.93 -  unfolding insertl_def member_def mem_iff by simp
    8.94 -
    8.95 -lemma insertl_member [simp]:
    8.96 -  fixes xs x
    8.97 -  assumes member: "member xs x"
    8.98 -  shows "insertl x xs = xs"
    8.99 -  using member unfolding insertl_def by simp
   8.100 -
   8.101 -lemma insertl_not_member [simp]:
   8.102 -  fixes xs x
   8.103 -  assumes member: "\<not> (member xs x)"
   8.104 -  shows "insertl x xs = x # xs"
   8.105 -  using member unfolding insertl_def by simp
   8.106 -
   8.107 -lemma foldr_remove1_empty [simp]:
   8.108 -  "foldr remove1 xs [] = []"
   8.109 -  by (induct xs) simp_all
   8.110 -
   8.111 -
   8.112 -subsubsection {* Derived definitions *}
   8.113 -
   8.114 -function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   8.115 -where
   8.116 -  "unionl [] ys = ys"
   8.117 -| "unionl xs ys = foldr insertl xs ys"
   8.118 -by pat_completeness auto
   8.119 -termination by lexicographic_order
   8.120 -
   8.121 -lemmas unionl_def = unionl.simps(2)
   8.122 -
   8.123 -function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   8.124 -where
   8.125 -  "intersect [] ys = []"
   8.126 -| "intersect xs [] = []"
   8.127 -| "intersect xs ys = filter (member xs) ys"
   8.128 -by pat_completeness auto
   8.129 -termination by lexicographic_order
   8.130 -
   8.131 -lemmas intersect_def = intersect.simps(3)
   8.132 -
   8.133 -function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   8.134 -where
   8.135 -  "subtract [] ys = ys"
   8.136 -| "subtract xs [] = []"
   8.137 -| "subtract xs ys = foldr remove1 xs ys"
   8.138 -by pat_completeness auto
   8.139 -termination by lexicographic_order
   8.140 -
   8.141 -lemmas subtract_def = subtract.simps(3)
   8.142 -
   8.143 -function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   8.144 -where
   8.145 -  "map_distinct f [] = []"
   8.146 -| "map_distinct f xs = foldr (insertl o f) xs []"
   8.147 -by pat_completeness auto
   8.148 -termination by lexicographic_order
   8.149 -
   8.150 -lemmas map_distinct_def = map_distinct.simps(2)
   8.151 -
   8.152 -function unions :: "'a list list \<Rightarrow> 'a list"
   8.153 -where
   8.154 -  "unions [] = []"
   8.155 -| "unions xs = foldr unionl xs []"
   8.156 -by pat_completeness auto
   8.157 -termination by lexicographic_order
   8.158 -
   8.159 -lemmas unions_def = unions.simps(2)
   8.160 -
   8.161 -consts intersects :: "'a list list \<Rightarrow> 'a list"
   8.162 -primrec
   8.163 -  "intersects (x#xs) = foldr intersect xs x"
   8.164 -
   8.165 -definition
   8.166 -  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   8.167 -  "map_union xs f = unions (map f xs)"
   8.168 -
   8.169 -definition
   8.170 -  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   8.171 -  "map_inter xs f = intersects (map f xs)"
   8.172 -
   8.173 -
   8.174 -subsection {* Isomorphism proofs *}
   8.175 -
   8.176 -lemma iso_member:
   8.177 -  "member xs x \<longleftrightarrow> x \<in> set xs"
   8.178 -  unfolding member_def mem_iff ..
   8.179 -
   8.180 -lemma iso_insert:
   8.181 -  "set (insertl x xs) = insert x (set xs)"
   8.182 -  unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
   8.183 -
   8.184 -lemma iso_remove1:
   8.185 -  assumes distnct: "distinct xs"
   8.186 -  shows "set (remove1 x xs) = set xs - {x}"
   8.187 -  using distnct set_remove1_eq by auto
   8.188 -
   8.189 -lemma iso_union:
   8.190 -  "set (unionl xs ys) = set xs \<union> set ys"
   8.191 -  unfolding unionl_def
   8.192 -  by (induct xs arbitrary: ys) (simp_all add: iso_insert)
   8.193 -
   8.194 -lemma iso_intersect:
   8.195 -  "set (intersect xs ys) = set xs \<inter> set ys"
   8.196 -  unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
   8.197 -
   8.198 -definition
   8.199 -  subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   8.200 -  "subtract' = flip subtract"
   8.201 -
   8.202 -lemma iso_subtract:
   8.203 -  fixes ys
   8.204 -  assumes distnct: "distinct ys"
   8.205 -  shows "set (subtract' ys xs) = set ys - set xs"
   8.206 -    and "distinct (subtract' ys xs)"
   8.207 -  unfolding subtract'_def flip_def subtract_def
   8.208 -  using distnct by (induct xs arbitrary: ys) auto
   8.209 -
   8.210 -lemma iso_map_distinct:
   8.211 -  "set (map_distinct f xs) = image f (set xs)"
   8.212 -  unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
   8.213 -
   8.214 -lemma iso_unions:
   8.215 -  "set (unions xss) = \<Union> set (map set xss)"
   8.216 -  unfolding unions_def
   8.217 -proof (induct xss)
   8.218 -  case Nil show ?case by simp
   8.219 -next
   8.220 -  case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
   8.221 -qed
   8.222 -
   8.223 -lemma iso_intersects:
   8.224 -  "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
   8.225 -  by (induct xss) (simp_all add: Int_def iso_member, auto)
   8.226 -
   8.227 -lemma iso_UNION:
   8.228 -  "set (map_union xs f) = UNION (set xs) (set o f)"
   8.229 -  unfolding map_union_def iso_unions by simp
   8.230 -
   8.231 -lemma iso_INTER:
   8.232 -  "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
   8.233 -  unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
   8.234 -
   8.235 -definition
   8.236 -  Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   8.237 -  "Blall = flip list_all"
   8.238 -definition
   8.239 -  Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   8.240 -  "Blex = flip list_ex"
   8.241 -
   8.242 -lemma iso_Ball:
   8.243 -  "Blall xs f = Ball (set xs) f"
   8.244 -  unfolding Blall_def flip_def by (induct xs) simp_all
   8.245 -
   8.246 -lemma iso_Bex:
   8.247 -  "Blex xs f = Bex (set xs) f"
   8.248 -  unfolding Blex_def flip_def by (induct xs) simp_all
   8.249 -
   8.250 -lemma iso_filter:
   8.251 -  "set (filter P xs) = filter_set P (set xs)"
   8.252 -  unfolding filter_set_def by (induct xs) auto
   8.253 -
   8.254 -subsection {* code generator setup *}
   8.255 -
   8.256 -ML {*
   8.257 -nonfix inter;
   8.258 -nonfix union;
   8.259 -nonfix subset;
   8.260 -*}
   8.261 -
   8.262 -code_modulename SML
   8.263 -  ExecutableSet List
   8.264 -  Set List
   8.265 -
   8.266 -code_modulename OCaml
   8.267 -  ExecutableSet List
   8.268 -  Set List
   8.269 -
   8.270 -code_modulename Haskell
   8.271 -  ExecutableSet List
   8.272 -  Set List
   8.273 -
   8.274 -definition [code inline]:
   8.275 -  "empty_list = []"
   8.276 -
   8.277 -lemma [code func]:
   8.278 -  "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
   8.279 -
   8.280 -lemma [code func]:
   8.281 -  "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
   8.282 -
   8.283 -lemma [code func]:
   8.284 -  "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
   8.285 -
   8.286 -lemma [code func]:
   8.287 -  "(op -) (xs \<Colon> 'a\<Colon>eq set) = (op -) (xs \<Colon> 'a\<Colon>eq set)" ..
   8.288 -
   8.289 -lemma [code func]:
   8.290 -  "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
   8.291 -
   8.292 -lemma [code func]:
   8.293 -  "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
   8.294 -
   8.295 -lemma [code func]:
   8.296 -  "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
   8.297 -
   8.298 -lemma [code func]:
   8.299 -  "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
   8.300 -
   8.301 -lemma [code func]:
   8.302 -  "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
   8.303 -
   8.304 -lemma [code func]:
   8.305 -  "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
   8.306 -
   8.307 -lemma [code func]:
   8.308 -  "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
   8.309 -
   8.310 -lemma [code func]:
   8.311 -  "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
   8.312 -
   8.313 -
   8.314 -code_abstype "'a set" "'a list" where
   8.315 -  "{}" \<equiv> empty_list
   8.316 -  insert \<equiv> insertl
   8.317 -  "op \<union>" \<equiv> unionl
   8.318 -  "op \<inter>" \<equiv> intersect
   8.319 -  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
   8.320 -  image \<equiv> map_distinct
   8.321 -  Union \<equiv> unions
   8.322 -  Inter \<equiv> intersects
   8.323 -  UNION \<equiv> map_union
   8.324 -  INTER \<equiv> map_inter
   8.325 -  Ball \<equiv> Blall
   8.326 -  Bex \<equiv> Blex
   8.327 -  filter_set \<equiv> filter
   8.328 -
   8.329 -
   8.330 -subsubsection {* type serializations *}
   8.331 -
   8.332 -types_code
   8.333 -  set ("_ list")
   8.334 -attach (term_of) {*
   8.335 -fun term_of_set f T [] = Const ("{}", Type ("set", [T]))
   8.336 -  | term_of_set f T (x :: xs) = Const ("insert",
   8.337 -      T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs;
   8.338 -*}
   8.339 -attach (test) {*
   8.340 -fun gen_set' aG i j = frequency
   8.341 -  [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] ()
   8.342 -and gen_set aG i = gen_set' aG i i;
   8.343 -*}
   8.344 -
   8.345 -
   8.346 -subsubsection {* const serializations *}
   8.347 -
   8.348 -consts_code
   8.349 -  "{}" ("{*[]*}")
   8.350 -  insert ("{*insertl*}")
   8.351 -  "op \<union>" ("{*unionl*}")
   8.352 -  "op \<inter>" ("{*intersect*}")
   8.353 -  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
   8.354 -  image ("{*map_distinct*}")
   8.355 -  Union ("{*unions*}")
   8.356 -  Inter ("{*intersects*}")
   8.357 -  UNION ("{*map_union*}")
   8.358 -  INTER ("{*map_inter*}")
   8.359 -  Ball ("{*Blall*}")
   8.360 -  Bex ("{*Blex*}")
   8.361 -  filter_set ("{*filter*}")
   8.362 -
   8.363 -end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Library/Executable_Rat.thy	Thu Jul 19 21:47:39 2007 +0200
     9.3 @@ -0,0 +1,150 @@
     9.4 +(*  Title:      HOL/Library/Executable_Rat.thy
     9.5 +    ID:         $Id$
     9.6 +    Author:     Florian Haftmann, TU Muenchen
     9.7 +*)
     9.8 +
     9.9 +header {* Executable implementation of rational numbers in HOL *}
    9.10 +
    9.11 +theory Executable_Rat
    9.12 +imports "~~/src/HOL/Real/Rational" "~~/src/HOL/NumberTheory/IntPrimes"
    9.13 +begin
    9.14 +
    9.15 +text {*
    9.16 +  Actually \emph{nothing} is proved about this implementation.
    9.17 +*}
    9.18 +
    9.19 +subsection {* Representation and operations of executable rationals *}
    9.20 +
    9.21 +datatype erat = Rat bool nat nat
    9.22 +
    9.23 +axiomatization
    9.24 +  div_zero :: erat
    9.25 +
    9.26 +fun
    9.27 +  common :: "(nat * nat) \<Rightarrow> (nat * nat) \<Rightarrow> (nat * nat) * nat" where
    9.28 +  "common (p1, q1) (p2, q2) = (
    9.29 +     let
    9.30 +       q' = q1 * q2 div gcd (q1, q2)
    9.31 +     in ((p1 * (q' div q1), p2 * (q' div q2)), q'))"
    9.32 +
    9.33 +definition
    9.34 +  minus_sign :: "nat \<Rightarrow> nat \<Rightarrow> bool * nat" where
    9.35 +  "minus_sign n m = (if n < m then (False, m - n) else (True, n - m))"
    9.36 +
    9.37 +fun
    9.38 +  add_sign :: "bool * nat \<Rightarrow> bool * nat \<Rightarrow> bool * nat" where
    9.39 +  "add_sign (True, n) (True, m) = (True, n + m)"
    9.40 +| "add_sign (False, n) (False, m) = (False, n + m)"
    9.41 +| "add_sign (True, n) (False, m) = minus_sign n m"
    9.42 +| "add_sign (False, n) (True, m) = minus_sign m n"
    9.43 +
    9.44 +definition
    9.45 +  erat_of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" where
    9.46 +  "erat_of_quotient k1 k2 = (
    9.47 +    let
    9.48 +      l1 = nat (abs k1);
    9.49 +      l2 = nat (abs k2);
    9.50 +      m = gcd (l1, l2)
    9.51 +    in Rat (k1 \<le> 0 \<longleftrightarrow> k2 \<le> 0) (l1 div m) (l2 div m))"
    9.52 +
    9.53 +instance erat :: zero
    9.54 +  zero_rat_def: "0 \<equiv> Rat True 0 1" ..
    9.55 +
    9.56 +instance erat :: one
    9.57 +  one_rat_def: "1 \<equiv> Rat True 1 1" ..
    9.58 +
    9.59 +instance erat :: plus
    9.60 +  add_rat_def: "r + s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
    9.61 +        let
    9.62 +          ((r1, r2), den) = common (p1, q1) (p2, q2);
    9.63 +          (sign, num) = add_sign (a1, r1) (a2, r2)
    9.64 +        in Rat sign num den" ..
    9.65 +
    9.66 +instance erat :: minus
    9.67 +  uminus_rat_def: "- r \<equiv> case r of Rat a p q \<Rightarrow>
    9.68 +        if p = 0 then Rat True 0 1
    9.69 +        else Rat (\<not> a) p q" ..
    9.70 +  
    9.71 +instance erat :: times
    9.72 +  times_rat_def: "r * s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
    9.73 +        let
    9.74 +          p = p1 * p2;
    9.75 +          q = q1 * q2;
    9.76 +          m = gcd (p, q)
    9.77 +        in Rat (a1 = a2) (p div m) (q div m)" ..
    9.78 +
    9.79 +instance erat :: inverse
    9.80 +  inverse_rat_def: "inverse r \<equiv> case r of Rat a p q \<Rightarrow>
    9.81 +        if p = 0 then div_zero
    9.82 +        else Rat a q p" ..
    9.83 +
    9.84 +instance erat :: ord
    9.85 +  le_rat_def: "r1 \<le> r2 \<equiv> case r1 of Rat a1 p1 q1 \<Rightarrow> case r2 of Rat a2 p2 q2 \<Rightarrow>
    9.86 +        (\<not> a1 \<and> a2) \<or>
    9.87 +        (\<not> (a1 \<and> \<not> a2) \<and>
    9.88 +          (let
    9.89 +            ((r1, r2), dummy) = common (p1, q1) (p2, q2)
    9.90 +          in if a1 then r1 \<le> r2 else r2 \<le> r1))" ..
    9.91 +
    9.92 +
    9.93 +subsection {* Code generator setup *}
    9.94 +
    9.95 +subsubsection {* code lemmas *}
    9.96 +
    9.97 +lemma number_of_rat [code unfold]:
    9.98 +  "(number_of k \<Colon> rat) = Fract k 1"
    9.99 +  unfolding Fract_of_int_eq rat_number_of_def by simp
   9.100 +
   9.101 +lemma rat_minus [code func]:
   9.102 +  "(a\<Colon>rat) - b = a + (- b)" unfolding diff_minus ..
   9.103 +
   9.104 +lemma rat_divide [code func]:
   9.105 +  "(a\<Colon>rat) / b = a * inverse b" unfolding divide_inverse ..
   9.106 +
   9.107 +instance rat :: eq ..
   9.108 +
   9.109 +subsubsection {* names *}
   9.110 +
   9.111 +code_modulename SML
   9.112 +  Executable_Rat Rational
   9.113 +
   9.114 +code_modulename OCaml
   9.115 +  Executable_Rat Rational
   9.116 +
   9.117 +code_modulename Haskell
   9.118 +  Executable_Rat Rational
   9.119 +
   9.120 +subsubsection {* rat as abstype *}
   9.121 +
   9.122 +code_const div_zero
   9.123 +  (SML "raise/ Fail/ \"Division by zero\"")
   9.124 +  (OCaml "failwith \"Division by zero\"")
   9.125 +  (Haskell "error/ \"Division by zero\"")
   9.126 +
   9.127 +code_abstype rat erat where
   9.128 +  Fract \<equiv> erat_of_quotient
   9.129 +  "0 \<Colon> rat" \<equiv> "0 \<Colon> erat"
   9.130 +  "1 \<Colon> rat" \<equiv> "1 \<Colon> erat"
   9.131 +  "op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
   9.132 +  "uminus \<Colon> rat \<Rightarrow> rat" \<equiv> "uminus \<Colon> erat \<Rightarrow> erat"
   9.133 +  "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
   9.134 +  "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
   9.135 +  "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv>  "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
   9.136 +  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
   9.137 +
   9.138 +types_code
   9.139 +  rat ("{*erat*}")
   9.140 +
   9.141 +consts_code
   9.142 +  div_zero ("(raise/ (Fail/ \"Division by zero\"))")
   9.143 +  Fract ("({*erat_of_quotient*} (_) (_))")
   9.144 +  "0 \<Colon> rat" ("({*Rat True 0 1*})")
   9.145 +  "1 \<Colon> rat" ("({*Rat True 1 1*})")
   9.146 +  "plus \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   9.147 +  "uminus \<Colon> rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))")
   9.148 +  "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   9.149 +  "inverse \<Colon> rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))")
   9.150 +  "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   9.151 +  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   9.152 +
   9.153 +end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Library/Executable_Set.thy	Thu Jul 19 21:47:39 2007 +0200
    10.3 @@ -0,0 +1,360 @@
    10.4 +(*  Title:      HOL/Library/Executable_Set.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     Stefan Berghofer, TU Muenchen
    10.7 +*)
    10.8 +
    10.9 +header {* Implementation of finite sets by lists *}
   10.10 +
   10.11 +theory Executable_Set
   10.12 +imports Main
   10.13 +begin
   10.14 +
   10.15 +subsection {* Definitional rewrites *}
   10.16 +
   10.17 +instance set :: (eq) eq ..
   10.18 +
   10.19 +lemma [code target: Set]:
   10.20 +  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   10.21 +  by blast
   10.22 +
   10.23 +lemma [code func]:
   10.24 +  "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   10.25 +  by blast
   10.26 +
   10.27 +lemma [code func]:
   10.28 +  "(A\<Colon>'a\<Colon>eq set) \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   10.29 +  unfolding subset_def ..
   10.30 +
   10.31 +lemma [code func]:
   10.32 +  "(A\<Colon>'a\<Colon>eq set) \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
   10.33 +  by blast
   10.34 +
   10.35 +lemma [code]:
   10.36 +  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
   10.37 +  unfolding bex_triv_one_point1 ..
   10.38 +
   10.39 +definition
   10.40 +  filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   10.41 +  "filter_set P xs = {x\<in>xs. P x}"
   10.42 +
   10.43 +lemmas [symmetric, code inline] = filter_set_def
   10.44 +
   10.45 +
   10.46 +subsection {* Operations on lists *}
   10.47 +
   10.48 +subsubsection {* Basic definitions *}
   10.49 +
   10.50 +definition
   10.51 +  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
   10.52 +  "flip f a b = f b a"
   10.53 +
   10.54 +definition
   10.55 +  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
   10.56 +  "member xs x \<longleftrightarrow> x \<in> set xs"
   10.57 +
   10.58 +definition
   10.59 +  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   10.60 +  "insertl x xs = (if member xs x then xs else x#xs)"
   10.61 +
   10.62 +lemma [code target: List]: "member [] y \<longleftrightarrow> False"
   10.63 +  and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
   10.64 +  unfolding member_def by (induct xs) simp_all
   10.65 +
   10.66 +fun
   10.67 +  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   10.68 +  "drop_first f [] = []"
   10.69 +| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
   10.70 +declare drop_first.simps [code del]
   10.71 +declare drop_first.simps [code target: List]
   10.72 +
   10.73 +declare remove1.simps [code del]
   10.74 +lemma [code target: List]:
   10.75 +  "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
   10.76 +proof (cases "member xs x")
   10.77 +  case False thus ?thesis unfolding member_def by (induct xs) auto
   10.78 +next
   10.79 +  case True
   10.80 +  have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
   10.81 +  with True show ?thesis by simp
   10.82 +qed
   10.83 +
   10.84 +lemma member_nil [simp]:
   10.85 +  "member [] = (\<lambda>x. False)"
   10.86 +proof
   10.87 +  fix x
   10.88 +  show "member [] x = False" unfolding member_def by simp
   10.89 +qed
   10.90 +
   10.91 +lemma member_insertl [simp]:
   10.92 +  "x \<in> set (insertl x xs)"
   10.93 +  unfolding insertl_def member_def mem_iff by simp
   10.94 +
   10.95 +lemma insertl_member [simp]:
   10.96 +  fixes xs x
   10.97 +  assumes member: "member xs x"
   10.98 +  shows "insertl x xs = xs"
   10.99 +  using member unfolding insertl_def by simp
  10.100 +
  10.101 +lemma insertl_not_member [simp]:
  10.102 +  fixes xs x
  10.103 +  assumes member: "\<not> (member xs x)"
  10.104 +  shows "insertl x xs = x # xs"
  10.105 +  using member unfolding insertl_def by simp
  10.106 +
  10.107 +lemma foldr_remove1_empty [simp]:
  10.108 +  "foldr remove1 xs [] = []"
  10.109 +  by (induct xs) simp_all
  10.110 +
  10.111 +
  10.112 +subsubsection {* Derived definitions *}
  10.113 +
  10.114 +function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  10.115 +where
  10.116 +  "unionl [] ys = ys"
  10.117 +| "unionl xs ys = foldr insertl xs ys"
  10.118 +by pat_completeness auto
  10.119 +termination by lexicographic_order
  10.120 +
  10.121 +lemmas unionl_def = unionl.simps(2)
  10.122 +
  10.123 +function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  10.124 +where
  10.125 +  "intersect [] ys = []"
  10.126 +| "intersect xs [] = []"
  10.127 +| "intersect xs ys = filter (member xs) ys"
  10.128 +by pat_completeness auto
  10.129 +termination by lexicographic_order
  10.130 +
  10.131 +lemmas intersect_def = intersect.simps(3)
  10.132 +
  10.133 +function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  10.134 +where
  10.135 +  "subtract [] ys = ys"
  10.136 +| "subtract xs [] = []"
  10.137 +| "subtract xs ys = foldr remove1 xs ys"
  10.138 +by pat_completeness auto
  10.139 +termination by lexicographic_order
  10.140 +
  10.141 +lemmas subtract_def = subtract.simps(3)
  10.142 +
  10.143 +function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
  10.144 +where
  10.145 +  "map_distinct f [] = []"
  10.146 +| "map_distinct f xs = foldr (insertl o f) xs []"
  10.147 +by pat_completeness auto
  10.148 +termination by lexicographic_order
  10.149 +
  10.150 +lemmas map_distinct_def = map_distinct.simps(2)
  10.151 +
  10.152 +function unions :: "'a list list \<Rightarrow> 'a list"
  10.153 +where
  10.154 +  "unions [] = []"
  10.155 +| "unions xs = foldr unionl xs []"
  10.156 +by pat_completeness auto
  10.157 +termination by lexicographic_order
  10.158 +
  10.159 +lemmas unions_def = unions.simps(2)
  10.160 +
  10.161 +consts intersects :: "'a list list \<Rightarrow> 'a list"
  10.162 +primrec
  10.163 +  "intersects (x#xs) = foldr intersect xs x"
  10.164 +
  10.165 +definition
  10.166 +  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
  10.167 +  "map_union xs f = unions (map f xs)"
  10.168 +
  10.169 +definition
  10.170 +  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
  10.171 +  "map_inter xs f = intersects (map f xs)"
  10.172 +
  10.173 +
  10.174 +subsection {* Isomorphism proofs *}
  10.175 +
  10.176 +lemma iso_member:
  10.177 +  "member xs x \<longleftrightarrow> x \<in> set xs"
  10.178 +  unfolding member_def mem_iff ..
  10.179 +
  10.180 +lemma iso_insert:
  10.181 +  "set (insertl x xs) = insert x (set xs)"
  10.182 +  unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
  10.183 +
  10.184 +lemma iso_remove1:
  10.185 +  assumes distnct: "distinct xs"
  10.186 +  shows "set (remove1 x xs) = set xs - {x}"
  10.187 +  using distnct set_remove1_eq by auto
  10.188 +
  10.189 +lemma iso_union:
  10.190 +  "set (unionl xs ys) = set xs \<union> set ys"
  10.191 +  unfolding unionl_def
  10.192 +  by (induct xs arbitrary: ys) (simp_all add: iso_insert)
  10.193 +
  10.194 +lemma iso_intersect:
  10.195 +  "set (intersect xs ys) = set xs \<inter> set ys"
  10.196 +  unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
  10.197 +
  10.198 +definition
  10.199 +  subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  10.200 +  "subtract' = flip subtract"
  10.201 +
  10.202 +lemma iso_subtract:
  10.203 +  fixes ys
  10.204 +  assumes distnct: "distinct ys"
  10.205 +  shows "set (subtract' ys xs) = set ys - set xs"
  10.206 +    and "distinct (subtract' ys xs)"
  10.207 +  unfolding subtract'_def flip_def subtract_def
  10.208 +  using distnct by (induct xs arbitrary: ys) auto
  10.209 +
  10.210 +lemma iso_map_distinct:
  10.211 +  "set (map_distinct f xs) = image f (set xs)"
  10.212 +  unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
  10.213 +
  10.214 +lemma iso_unions:
  10.215 +  "set (unions xss) = \<Union> set (map set xss)"
  10.216 +  unfolding unions_def
  10.217 +proof (induct xss)
  10.218 +  case Nil show ?case by simp
  10.219 +next
  10.220 +  case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
  10.221 +qed
  10.222 +
  10.223 +lemma iso_intersects:
  10.224 +  "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
  10.225 +  by (induct xss) (simp_all add: Int_def iso_member, auto)
  10.226 +
  10.227 +lemma iso_UNION:
  10.228 +  "set (map_union xs f) = UNION (set xs) (set o f)"
  10.229 +  unfolding map_union_def iso_unions by simp
  10.230 +
  10.231 +lemma iso_INTER:
  10.232 +  "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
  10.233 +  unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
  10.234 +
  10.235 +definition
  10.236 +  Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
  10.237 +  "Blall = flip list_all"
  10.238 +definition
  10.239 +  Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
  10.240 +  "Blex = flip list_ex"
  10.241 +
  10.242 +lemma iso_Ball:
  10.243 +  "Blall xs f = Ball (set xs) f"
  10.244 +  unfolding Blall_def flip_def by (induct xs) simp_all
  10.245 +
  10.246 +lemma iso_Bex:
  10.247 +  "Blex xs f = Bex (set xs) f"
  10.248 +  unfolding Blex_def flip_def by (induct xs) simp_all
  10.249 +
  10.250 +lemma iso_filter:
  10.251 +  "set (filter P xs) = filter_set P (set xs)"
  10.252 +  unfolding filter_set_def by (induct xs) auto
  10.253 +
  10.254 +subsection {* code generator setup *}
  10.255 +
  10.256 +ML {*
  10.257 +nonfix inter;
  10.258 +nonfix union;
  10.259 +nonfix subset;
  10.260 +*}
  10.261 +
  10.262 +code_modulename SML
  10.263 +  Executable_Set List
  10.264 +  Set List
  10.265 +
  10.266 +code_modulename OCaml
  10.267 +  Executable_Set List
  10.268 +  Set List
  10.269 +
  10.270 +code_modulename Haskell
  10.271 +  Executable_Set List
  10.272 +  Set List
  10.273 +
  10.274 +definition [code inline]:
  10.275 +  "empty_list = []"
  10.276 +
  10.277 +lemma [code func]:
  10.278 +  "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
  10.279 +
  10.280 +lemma [code func]:
  10.281 +  "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
  10.282 +
  10.283 +lemma [code func]:
  10.284 +  "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
  10.285 +
  10.286 +lemma [code func]:
  10.287 +  "(op -) (xs \<Colon> 'a\<Colon>eq set) = (op -) (xs \<Colon> 'a\<Colon>eq set)" ..
  10.288 +
  10.289 +lemma [code func]:
  10.290 +  "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
  10.291 +
  10.292 +lemma [code func]:
  10.293 +  "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
  10.294 +
  10.295 +lemma [code func]:
  10.296 +  "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
  10.297 +
  10.298 +lemma [code func]:
  10.299 +  "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
  10.300 +
  10.301 +lemma [code func]:
  10.302 +  "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
  10.303 +
  10.304 +lemma [code func]:
  10.305 +  "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
  10.306 +
  10.307 +lemma [code func]:
  10.308 +  "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
  10.309 +
  10.310 +lemma [code func]:
  10.311 +  "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
  10.312 +
  10.313 +
  10.314 +code_abstype "'a set" "'a list" where
  10.315 +  "{}" \<equiv> empty_list
  10.316 +  insert \<equiv> insertl
  10.317 +  "op \<union>" \<equiv> unionl
  10.318 +  "op \<inter>" \<equiv> intersect
  10.319 +  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
  10.320 +  image \<equiv> map_distinct
  10.321 +  Union \<equiv> unions
  10.322 +  Inter \<equiv> intersects
  10.323 +  UNION \<equiv> map_union
  10.324 +  INTER \<equiv> map_inter
  10.325 +  Ball \<equiv> Blall
  10.326 +  Bex \<equiv> Blex
  10.327 +  filter_set \<equiv> filter
  10.328 +
  10.329 +
  10.330 +subsubsection {* type serializations *}
  10.331 +
  10.332 +types_code
  10.333 +  set ("_ list")
  10.334 +attach (term_of) {*
  10.335 +fun term_of_set f T [] = Const ("{}", Type ("set", [T]))
  10.336 +  | term_of_set f T (x :: xs) = Const ("insert",
  10.337 +      T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs;
  10.338 +*}
  10.339 +attach (test) {*
  10.340 +fun gen_set' aG i j = frequency
  10.341 +  [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] ()
  10.342 +and gen_set aG i = gen_set' aG i i;
  10.343 +*}
  10.344 +
  10.345 +
  10.346 +subsubsection {* const serializations *}
  10.347 +
  10.348 +consts_code
  10.349 +  "{}" ("{*[]*}")
  10.350 +  insert ("{*insertl*}")
  10.351 +  "op \<union>" ("{*unionl*}")
  10.352 +  "op \<inter>" ("{*intersect*}")
  10.353 +  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
  10.354 +  image ("{*map_distinct*}")
  10.355 +  Union ("{*unions*}")
  10.356 +  Inter ("{*intersects*}")
  10.357 +  UNION ("{*map_union*}")
  10.358 +  INTER ("{*map_inter*}")
  10.359 +  Ball ("{*Blall*}")
  10.360 +  Bex ("{*Blex*}")
  10.361 +  filter_set ("{*filter*}")
  10.362 +
  10.363 +end
    11.1 --- a/src/HOL/Library/Graphs.thy	Thu Jul 19 21:47:38 2007 +0200
    11.2 +++ b/src/HOL/Library/Graphs.thy	Thu Jul 19 21:47:39 2007 +0200
    11.3 @@ -6,7 +6,7 @@
    11.4  header {* General Graphs as Sets *}
    11.5  
    11.6  theory Graphs
    11.7 -imports Main SCT_Misc Kleene_Algebras ExecutableSet
    11.8 +imports Main SCT_Misc Kleene_Algebras Executable_Set
    11.9  begin
   11.10  
   11.11  subsection {* Basic types, Size Change Graphs *}
    12.1 --- a/src/HOL/Library/Library.thy	Thu Jul 19 21:47:38 2007 +0200
    12.2 +++ b/src/HOL/Library/Library.thy	Thu Jul 19 21:47:39 2007 +0200
    12.3 @@ -9,15 +9,15 @@
    12.4    Coinductive_List
    12.5    Commutative_Ring
    12.6    Continuity
    12.7 -  EfficientNat
    12.8 +  Efficient_Nat
    12.9    Eval
   12.10 -  ExecutableRat
   12.11 +  Executable_Rat
   12.12    Executable_Real
   12.13 -  ExecutableSet
   12.14 +  Executable_Set
   12.15    FuncSet
   12.16    GCD
   12.17    Infinite_Set
   12.18 -  MLString
   12.19 +  ML_String
   12.20    Multiset
   12.21    NatPair
   12.22    Nat_Infinity
    13.1 --- a/src/HOL/Library/MLString.thy	Thu Jul 19 21:47:38 2007 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,73 +0,0 @@
    13.4 -(*  ID:         $Id$
    13.5 -    Author:     Florian Haftmann, TU Muenchen
    13.6 -*)
    13.7 -
    13.8 -header {* Monolithic strings for ML *}
    13.9 -
   13.10 -theory MLString
   13.11 -imports List
   13.12 -begin
   13.13 -
   13.14 -subsection {* Motivation *}
   13.15 -
   13.16 -text {*
   13.17 -  Strings are represented in HOL as list of characters.
   13.18 -  For code generation to Haskell, this is no problem
   13.19 -  since in Haskell "abc" is equivalent to ['a', 'b', 'c'].
   13.20 -  On the other hand, in ML all strings have to
   13.21 -  be represented as list of characters which
   13.22 -  is awkward to read. This theory provides a distinguished
   13.23 -  datatype for strings which then by convention
   13.24 -  are serialized as monolithic ML strings.
   13.25 -*}
   13.26 -
   13.27 -
   13.28 -subsection {* Datatype of monolithic strings *}
   13.29 -
   13.30 -datatype ml_string = STR string
   13.31 -
   13.32 -lemmas [code func del] = ml_string.recs ml_string.cases
   13.33 -
   13.34 -lemma [code func]: "size (s\<Colon>ml_string) = 0"
   13.35 -  by (cases s) simp_all
   13.36 -
   13.37 -subsection {* ML interface *}
   13.38 -
   13.39 -ML {*
   13.40 -structure MLString =
   13.41 -struct
   13.42 -
   13.43 -fun mk s = @{term STR} $ HOLogic.mk_string s;
   13.44 -
   13.45 -end;
   13.46 -*}
   13.47 -
   13.48 -
   13.49 -subsection {* Code serialization *}
   13.50 -
   13.51 -code_type ml_string
   13.52 -  (SML "string")
   13.53 -
   13.54 -setup {*
   13.55 -let
   13.56 -  val charr = @{const_name Char}
   13.57 -  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
   13.58 -    @{const_name Nibble2}, @{const_name Nibble3},
   13.59 -    @{const_name Nibble4}, @{const_name Nibble5},
   13.60 -    @{const_name Nibble6}, @{const_name Nibble7},
   13.61 -    @{const_name Nibble8}, @{const_name Nibble9},
   13.62 -    @{const_name NibbleA}, @{const_name NibbleB},
   13.63 -    @{const_name NibbleC}, @{const_name NibbleD},
   13.64 -    @{const_name NibbleE}, @{const_name NibbleF}];
   13.65 -in
   13.66 -  CodegenSerializer.add_pretty_ml_string "SML"
   13.67 -    charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
   13.68 -end
   13.69 -*}
   13.70 -
   13.71 -code_reserved SML string
   13.72 -
   13.73 -code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
   13.74 -  (SML "!((_ : string) = _)")
   13.75 -
   13.76 -end
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Library/ML_String.thy	Thu Jul 19 21:47:39 2007 +0200
    14.3 @@ -0,0 +1,73 @@
    14.4 +(*  ID:         $Id$
    14.5 +    Author:     Florian Haftmann, TU Muenchen
    14.6 +*)
    14.7 +
    14.8 +header {* Monolithic strings for ML *}
    14.9 +
   14.10 +theory ML_String
   14.11 +imports List
   14.12 +begin
   14.13 +
   14.14 +subsection {* Motivation *}
   14.15 +
   14.16 +text {*
   14.17 +  Strings are represented in HOL as list of characters.
   14.18 +  For code generation to Haskell, this is no problem
   14.19 +  since in Haskell "abc" is equivalent to ['a', 'b', 'c'].
   14.20 +  On the other hand, in ML all strings have to
   14.21 +  be represented as list of characters which
   14.22 +  is awkward to read. This theory provides a distinguished
   14.23 +  datatype for strings which then by convention
   14.24 +  are serialized as monolithic ML strings.
   14.25 +*}
   14.26 +
   14.27 +
   14.28 +subsection {* Datatype of monolithic strings *}
   14.29 +
   14.30 +datatype ml_string = STR string
   14.31 +
   14.32 +lemmas [code func del] = ml_string.recs ml_string.cases
   14.33 +
   14.34 +lemma [code func]: "size (s\<Colon>ml_string) = 0"
   14.35 +  by (cases s) simp_all
   14.36 +
   14.37 +subsection {* ML interface *}
   14.38 +
   14.39 +ML {*
   14.40 +structure ML_String =
   14.41 +struct
   14.42 +
   14.43 +fun mk s = @{term STR} $ HOLogic.mk_string s;
   14.44 +
   14.45 +end;
   14.46 +*}
   14.47 +
   14.48 +
   14.49 +subsection {* Code serialization *}
   14.50 +
   14.51 +code_type ml_string
   14.52 +  (SML "string")
   14.53 +
   14.54 +setup {*
   14.55 +let
   14.56 +  val charr = @{const_name Char}
   14.57 +  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
   14.58 +    @{const_name Nibble2}, @{const_name Nibble3},
   14.59 +    @{const_name Nibble4}, @{const_name Nibble5},
   14.60 +    @{const_name Nibble6}, @{const_name Nibble7},
   14.61 +    @{const_name Nibble8}, @{const_name Nibble9},
   14.62 +    @{const_name NibbleA}, @{const_name NibbleB},
   14.63 +    @{const_name NibbleC}, @{const_name NibbleD},
   14.64 +    @{const_name NibbleE}, @{const_name NibbleF}];
   14.65 +in
   14.66 +  CodegenSerializer.add_pretty_ml_string "SML"
   14.67 +    charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
   14.68 +end
   14.69 +*}
   14.70 +
   14.71 +code_reserved SML string
   14.72 +
   14.73 +code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
   14.74 +  (SML "!((_ : string) = _)")
   14.75 +
   14.76 +end
    15.1 --- a/src/HOL/Library/Pure_term.thy	Thu Jul 19 21:47:38 2007 +0200
    15.2 +++ b/src/HOL/Library/Pure_term.thy	Thu Jul 19 21:47:39 2007 +0200
    15.3 @@ -6,7 +6,7 @@
    15.4  header {* Embedding (a subset of) the Pure term algebra in HOL *}
    15.5  
    15.6  theory Pure_term
    15.7 -imports MLString
    15.8 +imports ML_String
    15.9  begin
   15.10  
   15.11  subsection {* Definitions *}
   15.12 @@ -47,16 +47,16 @@
   15.13  structure Pure_term =
   15.14  struct
   15.15  
   15.16 -val mk_sort = HOLogic.mk_list @{typ class} o map MLString.mk;
   15.17 +val mk_sort = HOLogic.mk_list @{typ class} o map ML_String.mk;
   15.18  
   15.19  fun mk_typ f (Type (tyco, tys)) =
   15.20 -      @{term Type} $ MLString.mk tyco
   15.21 +      @{term Type} $ ML_String.mk tyco
   15.22          $ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys)
   15.23    | mk_typ f (TFree v) =
   15.24        f v;
   15.25  
   15.26  fun mk_term f g (Const (c, ty)) =
   15.27 -      @{term Const} $ MLString.mk c $ g ty
   15.28 +      @{term Const} $ ML_String.mk c $ g ty
   15.29    | mk_term f g (t1 $ t2) =
   15.30        @{term App} $ mk_term f g t1 $ mk_term f g t2
   15.31    | mk_term f g (Free v) = f v;
    16.1 --- a/src/HOL/Library/SCT_Implementation.thy	Thu Jul 19 21:47:38 2007 +0200
    16.2 +++ b/src/HOL/Library/SCT_Implementation.thy	Thu Jul 19 21:47:39 2007 +0200
    16.3 @@ -6,7 +6,7 @@
    16.4  header {* Implemtation of the SCT criterion *}
    16.5  
    16.6  theory SCT_Implementation
    16.7 -imports ExecutableSet SCT_Definition SCT_Theorem
    16.8 +imports Executable_Set SCT_Definition SCT_Theorem
    16.9  begin
   16.10  
   16.11  fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool"
    17.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Thu Jul 19 21:47:38 2007 +0200
    17.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu Jul 19 21:47:39 2007 +0200
    17.3 @@ -6,7 +6,7 @@
    17.4  header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
    17.5  
    17.6  theory BVExample
    17.7 -imports JVMListExample BVSpecTypeSafe JVM ExecutableSet
    17.8 +imports JVMListExample BVSpecTypeSafe JVM Executable_Set
    17.9  begin
   17.10  
   17.11  text {*
    18.1 --- a/src/HOL/ex/Codegenerator_Rat.thy	Thu Jul 19 21:47:38 2007 +0200
    18.2 +++ b/src/HOL/ex/Codegenerator_Rat.thy	Thu Jul 19 21:47:39 2007 +0200
    18.3 @@ -6,7 +6,7 @@
    18.4  header {* Simple example for executable rational numbers *}
    18.5  
    18.6  theory Codegenerator_Rat
    18.7 -imports ExecutableRat EfficientNat
    18.8 +imports Executable_Rat Efficient_Nat
    18.9  begin
   18.10  
   18.11  definition
    19.1 --- a/src/HOL/ex/NBE.thy	Thu Jul 19 21:47:38 2007 +0200
    19.2 +++ b/src/HOL/ex/NBE.thy	Thu Jul 19 21:47:39 2007 +0200
    19.3 @@ -3,7 +3,7 @@
    19.4      Work in progress
    19.5  *)
    19.6  
    19.7 -theory NBE imports Main ExecutableSet begin
    19.8 +theory NBE imports Main Executable_Set begin
    19.9  
   19.10  ML"set quick_and_dirty"
   19.11  
    20.1 --- a/src/HOL/ex/ROOT.ML	Thu Jul 19 21:47:38 2007 +0200
    20.2 +++ b/src/HOL/ex/ROOT.ML	Thu Jul 19 21:47:39 2007 +0200
    20.3 @@ -16,8 +16,8 @@
    20.4  no_document time_use_thy "Pretty_Int";
    20.5  time_use_thy "Random";
    20.6  
    20.7 -no_document time_use_thy "ExecutableRat";
    20.8 -no_document time_use_thy "EfficientNat";
    20.9 +no_document time_use_thy "Executable_Rat";
   20.10 +no_document time_use_thy "Efficient_Nat";
   20.11  time_use_thy "Codegenerator_Rat";
   20.12  no_document time_use_thy "Codegenerator";
   20.13  
    21.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Thu Jul 19 21:47:38 2007 +0200
    21.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Thu Jul 19 21:47:39 2007 +0200
    21.3 @@ -1,5 +1,5 @@
    21.4  theory Reflected_Presburger
    21.5 -imports GCD EfficientNat
    21.6 +imports GCD Efficient_Nat
    21.7  uses ("coopereif.ML") ("coopertac.ML")
    21.8  begin
    21.9