src/HOL/Main.thy
author wenzelm
Wed Sep 14 22:04:37 2005 +0200 (2005-09-14)
changeset 17386 b110730a24fd
parent 16770 1f1b1fae30e4
child 17395 a05e20f6a31a
permissions -rw-r--r--
imports Commutative_Ring;
     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 Commutative_Ring 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 attach (term_of) {*
    23 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    24 *}
    25 attach (test) {*
    26 fun gen_bool i = one_of [false, true];
    27 *}
    28 
    29 consts_code
    30   "True"    ("true")
    31   "False"   ("false")
    32   "Not"     ("not")
    33   "op |"    ("(_ orelse/ _)")
    34   "op &"    ("(_ andalso/ _)")
    35   "HOL.If"      ("(if _/ then _/ else _)")
    36 
    37   "wfrec"   ("\<module>wf'_rec?")
    38 attach {*
    39 fun wf_rec f x = f (wf_rec f) x;
    40 *}
    41 
    42 quickcheck_params [default_type = int]
    43 
    44 ML {*
    45 local
    46 
    47 fun eq_codegen thy defs gr dep thyname b t =
    48     (case strip_comb t of
    49        (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    50      | (Const ("op =", _), [t, u]) =>
    51           let
    52             val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    53             val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u)
    54           in
    55             SOME (gr'', Codegen.parens
    56               (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    57           end
    58      | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    59          thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    60      | _ => NONE);
    61 
    62 in
    63 
    64 val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
    65 
    66 end;
    67 *}
    68 
    69 setup eq_codegen_setup
    70 
    71 lemmas [code] = imp_conv_disj
    72 
    73 subsection {* Configuration of the 'refute' command *}
    74 
    75 text {*
    76   The following are fairly reasonable default values.  For an
    77   explanation of these parameters, see 'HOL/Refute.thy'.
    78 *}
    79 
    80 refute_params ["itself"=1,
    81                minsize=1,
    82                maxsize=8,
    83                maxvars=10000,
    84                maxtime=60,
    85                satsolver="auto"]
    86 
    87 end