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