# HG changeset patch
# User berghofe
# Date 1120218994 -7200
# Node ID bf7de5723c60297d180fc49b570ecd229692fd17
# Parent  f19d58cfb47a92ca3141383f82801e85a21913ae
Moved some code lemmas from Main to Nat.

diff -r f19d58cfb47a -r bf7de5723c60 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Fri Jul 01 13:54:57 2005 +0200
+++ b/src/HOL/Main.thy	Fri Jul 01 13:56:34 2005 +0200
@@ -40,21 +40,28 @@
 val term_of_int = HOLogic.mk_int o IntInf.fromInt;
 fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
 
-val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
-  (fn thy => fn gr => fn dep => fn b => fn t =>
+local
+
+fun eq_codegen thy defs gr dep thyname b t =
     (case strip_comb t of
        (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
      | (Const ("op =", _), [t, u]) =>
           let
-            val (gr', pt) = Codegen.invoke_codegen thy dep false (gr, t);
-            val (gr'', pu) = Codegen.invoke_codegen thy dep false (gr', u)
+            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
+            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u)
           in
             SOME (gr'', Codegen.parens
               (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
           end
      | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
-         thy dep b (gr, Codegen.eta_expand t ts 2))
-     | _ => NONE))];
+         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
+     | _ => NONE);
+
+in
+
+val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
+
+end;
 
 fun gen_bool i = one_of [false, true];
 
@@ -73,9 +80,7 @@
 
 setup eq_codegen_setup
 
-lemma [code]: "((n::nat) < 0) = False" by simp
-lemma [code]: "(0 < Suc n) = True" by simp
-lemmas [code] = Suc_less_eq imp_conv_disj
+lemmas [code] = imp_conv_disj
 
 subsection {* Configuration of the 'refute' command *}
 
diff -r f19d58cfb47a -r bf7de5723c60 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Jul 01 13:54:57 2005 +0200
+++ b/src/HOL/Nat.thy	Fri Jul 01 13:56:34 2005 +0200
@@ -286,7 +286,7 @@
 lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
   by (blast elim: lessE dest: Suc_lessD)
 
-lemma Suc_less_eq [iff]: "(Suc m < Suc n) = (m < n)"
+lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)"
   apply (rule iffI)
   apply (erule Suc_less_SucD)
   apply (erule Suc_mono)
@@ -300,6 +300,9 @@
   apply (blast dest: Suc_lessD)
   done
 
+lemma [code]: "((n::nat) < 0) = False" by simp
+lemma [code]: "(0 < Suc n) = True" by simp
+
 text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
 lemma not_less_eq: "(~ m < n) = (n < Suc m)"
 by (rule_tac m = m and n = n in diff_induct, simp_all)