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