1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Oct 19 09:11:14 2011 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Oct 19 09:11:15 2011 +0200
     1.3 @@ -164,49 +164,9 @@
     1.4  
     1.5  val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
     1.6  
     1.7 -fun remove_suc_clause thy thms =
     1.8 -  let
     1.9 -    val vname = singleton (Name.variant_list (map fst
    1.10 -      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "x";
    1.11 -    fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
    1.12 -      | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
    1.13 -      | find_var _ = NONE;
    1.14 -    fun find_thm th =
    1.15 -      let val th' = Conv.fconv_rule Object_Logic.atomize th
    1.16 -      in Option.map (pair (th, th')) (find_var (prop_of th')) end
    1.17 -  in
    1.18 -    case get_first find_thm thms of
    1.19 -      NONE => thms
    1.20 -    | SOME ((th, th'), (Sucv, v)) =>
    1.21 -        let
    1.22 -          val cert = cterm_of (Thm.theory_of_thm th);
    1.23 -          val th'' = Object_Logic.rulify (Thm.implies_elim
    1.24 -            (Conv.fconv_rule (Thm.beta_conversion true)
    1.25 -              (Drule.instantiate' []
    1.26 -                [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
    1.27 -                   abstract_over (Sucv,
    1.28 -                     HOLogic.dest_Trueprop (prop_of th')))))),
    1.29 -                 SOME (cert v)] @{thm Suc_clause}))
    1.30 -            (Thm.forall_intr (cert v) th'))
    1.31 -        in
    1.32 -          remove_suc_clause thy (map (fn th''' =>
    1.33 -            if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
    1.34 -        end
    1.35 -  end;
    1.36 -
    1.37 -fun clause_suc_preproc thy ths =
    1.38 -  let
    1.39 -    val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
    1.40 -  in
    1.41 -    if forall (can (dest o concl_of)) ths andalso
    1.42 -      exists (fn th => exists (exists_Const (fn (c, _) => c = @{const_name Suc}))
    1.43 -        (map_filter (try dest) (concl_of th :: prems_of th))) ths
    1.44 -    then remove_suc_clause thy ths else ths
    1.45 -  end;
    1.46  in
    1.47  
    1.48    Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
    1.49 -  #> Codegen.add_preprocessor clause_suc_preproc
    1.50  
    1.51  end;
    1.52  *}
    1.53 @@ -225,19 +185,8 @@
    1.54    (OCaml "Big'_int.big'_int")
    1.55    (Eval "int")
    1.56  
    1.57 -types_code
    1.58 -  nat ("int")
    1.59 -attach (term_of) {*
    1.60 -val term_of_nat = HOLogic.mk_number HOLogic.natT;
    1.61 -*}
    1.62 -attach (test) {*
    1.63 -fun gen_nat i =
    1.64 -  let val n = random_range 0 i
    1.65 -  in (n, fn () => term_of_nat n) end;
    1.66 -*}
    1.67 -
    1.68  text {*
    1.69 -  For Haskell ans Scala we define our own @{typ nat} type.  The reason
    1.70 +  For Haskell and Scala we define our own @{typ nat} type.  The reason
    1.71    is that we have to distinguish type class instances for @{typ nat}
    1.72    and @{typ int}.
    1.73  *}
    1.74 @@ -379,13 +328,6 @@
    1.75    (SML "_")
    1.76    (OCaml "_")
    1.77  
    1.78 -consts_code
    1.79 -  int ("(_)")
    1.80 -  nat ("\<module>nat")
    1.81 -attach {*
    1.82 -fun nat i = if i < 0 then 0 else i;
    1.83 -*}
    1.84 -
    1.85  code_const nat
    1.86    (SML "IntInf.max/ (0,/ _)")
    1.87    (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
    1.88 @@ -461,15 +403,6 @@
    1.89    (Scala infixl 4 "<")
    1.90    (Eval infixl 6 "<")
    1.91  
    1.92 -consts_code
    1.93 -  "0::nat"                     ("0")
    1.94 -  "1::nat"                     ("1")
    1.95 -  Suc                          ("(_ +/ 1)")
    1.96 -  "op + \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ +/ _)")
    1.97 -  "op * \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ */ _)")
    1.98 -  "op \<le> \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ <=/ _)")
    1.99 -  "op < \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ </ _)")
   1.100 -
   1.101  
   1.102  text {* Evaluation *}
   1.103