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