# HG changeset patch
# User bulwahn
# Date 1319008275 -7200
# Node ID 3a0c63c0ed48c6aef7f4d630da632f46049c0973
# Parent  426dbd896c9e0ada81b7fa7e51d635012e351319
removing old code generator setup for efficient natural numbers; cleaned typo

diff -r 426dbd896c9e -r 3a0c63c0ed48 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Oct 19 09:11:14 2011 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Oct 19 09:11:15 2011 +0200
@@ -164,49 +164,9 @@
 
 val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
 
-fun remove_suc_clause thy thms =
-  let
-    val vname = singleton (Name.variant_list (map fst
-      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "x";
-    fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
-      | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
-      | find_var _ = NONE;
-    fun find_thm th =
-      let val th' = Conv.fconv_rule Object_Logic.atomize th
-      in Option.map (pair (th, th')) (find_var (prop_of th')) end
-  in
-    case get_first find_thm thms of
-      NONE => thms
-    | SOME ((th, th'), (Sucv, v)) =>
-        let
-          val cert = cterm_of (Thm.theory_of_thm th);
-          val th'' = Object_Logic.rulify (Thm.implies_elim
-            (Conv.fconv_rule (Thm.beta_conversion true)
-              (Drule.instantiate' []
-                [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
-                   abstract_over (Sucv,
-                     HOLogic.dest_Trueprop (prop_of th')))))),
-                 SOME (cert v)] @{thm Suc_clause}))
-            (Thm.forall_intr (cert v) th'))
-        in
-          remove_suc_clause thy (map (fn th''' =>
-            if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
-        end
-  end;
-
-fun clause_suc_preproc thy ths =
-  let
-    val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
-  in
-    if forall (can (dest o concl_of)) ths andalso
-      exists (fn th => exists (exists_Const (fn (c, _) => c = @{const_name Suc}))
-        (map_filter (try dest) (concl_of th :: prems_of th))) ths
-    then remove_suc_clause thy ths else ths
-  end;
 in
 
   Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
-  #> Codegen.add_preprocessor clause_suc_preproc
 
 end;
 *}
@@ -225,19 +185,8 @@
   (OCaml "Big'_int.big'_int")
   (Eval "int")
 
-types_code
-  nat ("int")
-attach (term_of) {*
-val term_of_nat = HOLogic.mk_number HOLogic.natT;
-*}
-attach (test) {*
-fun gen_nat i =
-  let val n = random_range 0 i
-  in (n, fn () => term_of_nat n) end;
-*}
-
 text {*
-  For Haskell ans Scala we define our own @{typ nat} type.  The reason
+  For Haskell and Scala we define our own @{typ nat} type.  The reason
   is that we have to distinguish type class instances for @{typ nat}
   and @{typ int}.
 *}
@@ -379,13 +328,6 @@
   (SML "_")
   (OCaml "_")
 
-consts_code
-  int ("(_)")
-  nat ("\<module>nat")
-attach {*
-fun nat i = if i < 0 then 0 else i;
-*}
-
 code_const nat
   (SML "IntInf.max/ (0,/ _)")
   (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
@@ -461,15 +403,6 @@
   (Scala infixl 4 "<")
   (Eval infixl 6 "<")
 
-consts_code
-  "0::nat"                     ("0")
-  "1::nat"                     ("1")
-  Suc                          ("(_ +/ 1)")
-  "op + \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ +/ _)")
-  "op * \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ */ _)")
-  "op \<le> \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ <=/ _)")
-  "op < \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ </ _)")
-
 
 text {* Evaluation *}