src/HOL/Main.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 15965 f422f8283491
child 16635 bf7de5723c60
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
     4 *)
     5 
     6 header {* Main HOL *}
     7 
     8 theory Main
     9     imports Refute Reconstruction
    10 
    11 begin
    12 
    13 text {*
    14   Theory @{text Main} includes everything.  Note that theory @{text
    15   PreList} already includes most HOL theories.
    16 *}
    17 
    18 subsection {* Configuration of the code generator *}
    19 
    20 types_code
    21   "bool"  ("bool")
    22 
    23 consts_code
    24   "True"    ("true")
    25   "False"   ("false")
    26   "Not"     ("not")
    27   "op |"    ("(_ orelse/ _)")
    28   "op &"    ("(_ andalso/ _)")
    29   "HOL.If"      ("(if _/ then _/ else _)")
    30 
    31   "wfrec"   ("wf'_rec?")
    32 
    33 quickcheck_params [default_type = int]
    34 
    35 (*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
    36 ML {*
    37 fun wf_rec f x = f (wf_rec f) x;
    38 
    39 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    40 val term_of_int = HOLogic.mk_int o IntInf.fromInt;
    41 fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    42 
    43 val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
    44   (fn thy => fn gr => fn dep => fn b => fn t =>
    45     (case strip_comb t of
    46        (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    47      | (Const ("op =", _), [t, u]) =>
    48           let
    49             val (gr', pt) = Codegen.invoke_codegen thy dep false (gr, t);
    50             val (gr'', pu) = Codegen.invoke_codegen thy dep false (gr', u)
    51           in
    52             SOME (gr'', Codegen.parens
    53               (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    54           end
    55      | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    56          thy dep b (gr, Codegen.eta_expand t ts 2))
    57      | _ => NONE))];
    58 
    59 fun gen_bool i = one_of [false, true];
    60 
    61 fun gen_int i = one_of [~1, 1] * random_range 0 i;
    62 
    63 fun gen_fun_type _ G i =
    64   let
    65     val f = ref (fn x => raise ERROR);
    66     val _ = (f := (fn x =>
    67       let
    68         val y = G i;
    69         val f' = !f
    70       in (f := (fn x' => if x = x' then y else f' x'); y) end))
    71   in (fn x => !f x) end;
    72 *}
    73 
    74 setup eq_codegen_setup
    75 
    76 lemma [code]: "((n::nat) < 0) = False" by simp
    77 lemma [code]: "(0 < Suc n) = True" by simp
    78 lemmas [code] = Suc_less_eq imp_conv_disj
    79 
    80 subsection {* Configuration of the 'refute' command *}
    81 
    82 text {*
    83   The following are fairly reasonable default values.  For an
    84   explanation of these parameters, see 'HOL/Refute.thy'.
    85 *}
    86 
    87 refute_params ["itself"=1,
    88                minsize=1,
    89                maxsize=8,
    90                maxvars=10000,
    91                maxtime=60,
    92                satsolver="auto"]
    93 
    94 end