Moved some code lemmas from Main to Nat.
authorberghofe
Fri Jul 01 13:56:34 2005 +0200 (2005-07-01)
changeset 16635bf7de5723c60
parent 16634 f19d58cfb47a
child 16636 1ed737a98198
Moved some code lemmas from Main to Nat.
src/HOL/Main.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Main.thy	Fri Jul 01 13:54:57 2005 +0200
     1.2 +++ b/src/HOL/Main.thy	Fri Jul 01 13:56:34 2005 +0200
     1.3 @@ -40,21 +40,28 @@
     1.4  val term_of_int = HOLogic.mk_int o IntInf.fromInt;
     1.5  fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
     1.6  
     1.7 -val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
     1.8 -  (fn thy => fn gr => fn dep => fn b => fn t =>
     1.9 +local
    1.10 +
    1.11 +fun eq_codegen thy defs gr dep thyname b t =
    1.12      (case strip_comb t of
    1.13         (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    1.14       | (Const ("op =", _), [t, u]) =>
    1.15            let
    1.16 -            val (gr', pt) = Codegen.invoke_codegen thy dep false (gr, t);
    1.17 -            val (gr'', pu) = Codegen.invoke_codegen thy dep false (gr', u)
    1.18 +            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    1.19 +            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u)
    1.20            in
    1.21              SOME (gr'', Codegen.parens
    1.22                (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    1.23            end
    1.24       | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    1.25 -         thy dep b (gr, Codegen.eta_expand t ts 2))
    1.26 -     | _ => NONE))];
    1.27 +         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    1.28 +     | _ => NONE);
    1.29 +
    1.30 +in
    1.31 +
    1.32 +val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
    1.33 +
    1.34 +end;
    1.35  
    1.36  fun gen_bool i = one_of [false, true];
    1.37  
    1.38 @@ -73,9 +80,7 @@
    1.39  
    1.40  setup eq_codegen_setup
    1.41  
    1.42 -lemma [code]: "((n::nat) < 0) = False" by simp
    1.43 -lemma [code]: "(0 < Suc n) = True" by simp
    1.44 -lemmas [code] = Suc_less_eq imp_conv_disj
    1.45 +lemmas [code] = imp_conv_disj
    1.46  
    1.47  subsection {* Configuration of the 'refute' command *}
    1.48  
     2.1 --- a/src/HOL/Nat.thy	Fri Jul 01 13:54:57 2005 +0200
     2.2 +++ b/src/HOL/Nat.thy	Fri Jul 01 13:56:34 2005 +0200
     2.3 @@ -286,7 +286,7 @@
     2.4  lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
     2.5    by (blast elim: lessE dest: Suc_lessD)
     2.6  
     2.7 -lemma Suc_less_eq [iff]: "(Suc m < Suc n) = (m < n)"
     2.8 +lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)"
     2.9    apply (rule iffI)
    2.10    apply (erule Suc_less_SucD)
    2.11    apply (erule Suc_mono)
    2.12 @@ -300,6 +300,9 @@
    2.13    apply (blast dest: Suc_lessD)
    2.14    done
    2.15  
    2.16 +lemma [code]: "((n::nat) < 0) = False" by simp
    2.17 +lemma [code]: "(0 < Suc n) = True" by simp
    2.18 +
    2.19  text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
    2.20  lemma not_less_eq: "(~ m < n) = (n < Suc m)"
    2.21  by (rule_tac m = m and n = n in diff_induct, simp_all)