src/HOL/Main.thy
author berghofe
Fri Jul 01 13:56:34 2005 +0200 (2005-07-01)
changeset 16635 bf7de5723c60
parent 16587 b34c8aa657a5
child 16770 1f1b1fae30e4
permissions -rw-r--r--
Moved some code lemmas from Main to Nat.
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
paulson@15872
     9
    imports 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@11533
    22
berghofe@11533
    23
consts_code
berghofe@11533
    24
  "True"    ("true")
berghofe@11533
    25
  "False"   ("false")
berghofe@11533
    26
  "Not"     ("not")
berghofe@11533
    27
  "op |"    ("(_ orelse/ _)")
berghofe@11533
    28
  "op &"    ("(_ andalso/ _)")
paulson@16587
    29
  "HOL.If"      ("(if _/ then _/ else _)")
berghofe@11533
    30
berghofe@13093
    31
  "wfrec"   ("wf'_rec?")
berghofe@13093
    32
berghofe@14102
    33
quickcheck_params [default_type = int]
berghofe@14102
    34
paulson@15965
    35
(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
berghofe@13755
    36
ML {*
berghofe@13755
    37
fun wf_rec f x = f (wf_rec f) x;
berghofe@13755
    38
berghofe@14102
    39
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
paulson@15965
    40
val term_of_int = HOLogic.mk_int o IntInf.fromInt;
berghofe@14102
    41
fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
berghofe@14102
    42
berghofe@16635
    43
local
berghofe@16635
    44
berghofe@16635
    45
fun eq_codegen thy defs gr dep thyname b t =
berghofe@14102
    46
    (case strip_comb t of
skalberg@15531
    47
       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
berghofe@14102
    48
     | (Const ("op =", _), [t, u]) =>
berghofe@14102
    49
          let
berghofe@16635
    50
            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
berghofe@16635
    51
            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u)
berghofe@14102
    52
          in
skalberg@15531
    53
            SOME (gr'', Codegen.parens
berghofe@14102
    54
              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
berghofe@14102
    55
          end
skalberg@15531
    56
     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
berghofe@16635
    57
         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
berghofe@16635
    58
     | _ => NONE);
berghofe@16635
    59
berghofe@16635
    60
in
berghofe@16635
    61
berghofe@16635
    62
val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
berghofe@16635
    63
berghofe@16635
    64
end;
berghofe@14102
    65
berghofe@14102
    66
fun gen_bool i = one_of [false, true];
berghofe@14102
    67
berghofe@14102
    68
fun gen_int i = one_of [~1, 1] * random_range 0 i;
berghofe@14102
    69
berghofe@14102
    70
fun gen_fun_type _ G i =
berghofe@14102
    71
  let
berghofe@14102
    72
    val f = ref (fn x => raise ERROR);
berghofe@14102
    73
    val _ = (f := (fn x =>
berghofe@14102
    74
      let
berghofe@14102
    75
        val y = G i;
berghofe@14102
    76
        val f' = !f
berghofe@14102
    77
      in (f := (fn x' => if x = x' then y else f' x'); y) end))
berghofe@14102
    78
  in (fn x => !f x) end;
berghofe@13755
    79
*}
berghofe@13093
    80
berghofe@14102
    81
setup eq_codegen_setup
berghofe@14102
    82
berghofe@16635
    83
lemmas [code] = imp_conv_disj
berghofe@12554
    84
webertj@14350
    85
subsection {* Configuration of the 'refute' command *}
webertj@14350
    86
webertj@14350
    87
text {*
webertj@14458
    88
  The following are fairly reasonable default values.  For an
webertj@14458
    89
  explanation of these parameters, see 'HOL/Refute.thy'.
webertj@14350
    90
*}
webertj@14350
    91
webertj@15584
    92
refute_params ["itself"=1,
webertj@15584
    93
               minsize=1,
webertj@14350
    94
               maxsize=8,
webertj@14806
    95
               maxvars=10000,
webertj@14806
    96
               maxtime=60,
webertj@14806
    97
               satsolver="auto"]
webertj@14350
    98
wenzelm@9650
    99
end