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