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;
nipkow@10519
     1
(*  Title:      HOL/Main.thy
nipkow@10519
     2
    ID:         $Id$
webertj@14350
     3
    Author:     Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
nipkow@10519
     4
*)
wenzelm@9619
     5
wenzelm@12024
     6
header {* Main HOL *}
wenzelm@12024
     7
nipkow@15131
     8
theory Main
wenzelm@17386
     9
imports Commutative_Ring Refute Reconstruction
paulson@15151
    10
nipkow@15131
    11
begin
wenzelm@9650
    12
wenzelm@12024
    13
text {*
wenzelm@12024
    14
  Theory @{text Main} includes everything.  Note that theory @{text
wenzelm@12024
    15
  PreList} already includes most HOL theories.
wenzelm@12024
    16
*}
wenzelm@12024
    17
wenzelm@12024
    18
subsection {* Configuration of the code generator *}
berghofe@11533
    19
berghofe@11533
    20
types_code
berghofe@11533
    21
  "bool"  ("bool")
berghofe@16770
    22
attach (term_of) {*
berghofe@16770
    23
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
berghofe@16770
    24
*}
berghofe@16770
    25
attach (test) {*
berghofe@16770
    26
fun gen_bool i = one_of [false, true];
berghofe@16770
    27
*}
berghofe@11533
    28
berghofe@11533
    29
consts_code
berghofe@11533
    30
  "True"    ("true")
berghofe@11533
    31
  "False"   ("false")
berghofe@11533
    32
  "Not"     ("not")
berghofe@11533
    33
  "op |"    ("(_ orelse/ _)")
berghofe@11533
    34
  "op &"    ("(_ andalso/ _)")
paulson@16587
    35
  "HOL.If"      ("(if _/ then _/ else _)")
berghofe@11533
    36
berghofe@16770
    37
  "wfrec"   ("\<module>wf'_rec?")
berghofe@16770
    38
attach {*
berghofe@16770
    39
fun wf_rec f x = f (wf_rec f) x;
berghofe@16770
    40
*}
berghofe@13093
    41
berghofe@14102
    42
quickcheck_params [default_type = int]
berghofe@14102
    43
berghofe@13755
    44
ML {*
berghofe@16635
    45
local
berghofe@16635
    46
berghofe@16635
    47
fun eq_codegen thy defs gr dep thyname b t =
berghofe@14102
    48
    (case strip_comb t of
skalberg@15531
    49
       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
berghofe@14102
    50
     | (Const ("op =", _), [t, u]) =>
berghofe@14102
    51
          let
berghofe@16635
    52
            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
berghofe@16635
    53
            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u)
berghofe@14102
    54
          in
skalberg@15531
    55
            SOME (gr'', Codegen.parens
berghofe@14102
    56
              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
berghofe@14102
    57
          end
skalberg@15531
    58
     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
berghofe@16635
    59
         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
berghofe@16635
    60
     | _ => NONE);
berghofe@16635
    61
berghofe@16635
    62
in
berghofe@16635
    63
berghofe@16635
    64
val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
berghofe@16635
    65
berghofe@16635
    66
end;
berghofe@13755
    67
*}
berghofe@13093
    68
berghofe@14102
    69
setup eq_codegen_setup
berghofe@14102
    70
berghofe@16635
    71
lemmas [code] = imp_conv_disj
berghofe@12554
    72
webertj@14350
    73
subsection {* Configuration of the 'refute' command *}
webertj@14350
    74
webertj@14350
    75
text {*
webertj@14458
    76
  The following are fairly reasonable default values.  For an
webertj@14458
    77
  explanation of these parameters, see 'HOL/Refute.thy'.
webertj@14350
    78
*}
webertj@14350
    79
webertj@15584
    80
refute_params ["itself"=1,
webertj@15584
    81
               minsize=1,
webertj@14350
    82
               maxsize=8,
webertj@14806
    83
               maxvars=10000,
webertj@14806
    84
               maxtime=60,
webertj@14806
    85
               satsolver="auto"]
webertj@14350
    86
wenzelm@9650
    87
end