src/HOL/Main.thy
author wenzelm
Wed, 14 Sep 2005 22:04:37 +0200
changeset 17386 b110730a24fd
parent 16770 1f1b1fae30e4
child 17395 a05e20f6a31a
permissions -rw-r--r--
imports Commutative_Ring;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10519
ade64af4c57c hide many names from Datatype_Universe.
nipkow
parents: 10386
diff changeset
     1
(*  Title:      HOL/Main.thy
ade64af4c57c hide many names from Datatype_Universe.
nipkow
parents: 10386
diff changeset
     2
    ID:         $Id$
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents: 14192
diff changeset
     3
    Author:     Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
10519
ade64af4c57c hide many names from Datatype_Universe.
nipkow
parents: 10386
diff changeset
     4
*)
9619
6125cc9efc18 fixed deps;
wenzelm
parents: 9447
diff changeset
     5
12024
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
     6
header {* Main HOL *}
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
     7
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15063
diff changeset
     8
theory Main
17386
b110730a24fd imports Commutative_Ring;
wenzelm
parents: 16770
diff changeset
     9
imports Commutative_Ring Refute Reconstruction
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents: 15140
diff changeset
    10
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15063
diff changeset
    11
begin
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
    12
12024
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    13
text {*
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    14
  Theory @{text Main} includes everything.  Note that theory @{text
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    15
  PreList} already includes most HOL theories.
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    16
*}
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    17
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    18
subsection {* Configuration of the code generator *}
11533
0c0d2332e8f0 Added code generator setup.
berghofe
parents: 11483
diff changeset
    19
0c0d2332e8f0 Added code generator setup.
berghofe
parents: 11483
diff changeset
    20
types_code
0c0d2332e8f0 Added code generator setup.
berghofe
parents: 11483
diff changeset
    21
  "bool"  ("bool")
16770
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16635
diff changeset
    22
attach (term_of) {*
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16635
diff changeset
    23
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16635
diff changeset
    24
*}
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16635
diff changeset
    25
attach (test) {*
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16635
diff changeset
    26
fun gen_bool i = one_of [false, true];
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16635
diff changeset
    27
*}
11533
0c0d2332e8f0 Added code generator setup.
berghofe
parents: 11483
diff changeset
    28
0c0d2332e8f0 Added code generator setup.
berghofe
parents: 11483
diff changeset
    29
consts_code
0c0d2332e8f0 Added code generator setup.
berghofe
parents: 11483
diff changeset
    30
  "True"    ("true")
0c0d2332e8f0 Added code generator setup.
berghofe
parents: 11483
diff changeset
    31
  "False"   ("false")
0c0d2332e8f0 Added code generator setup.
berghofe
parents: 11483
diff changeset
    32
  "Not"     ("not")
0c0d2332e8f0 Added code generator setup.
berghofe
parents: 11483
diff changeset
    33
  "op |"    ("(_ orelse/ _)")
0c0d2332e8f0 Added code generator setup.
berghofe
parents: 11483
diff changeset
    34
  "op &"    ("(_ andalso/ _)")
16587
b34c8aa657a5 Constant "If" is now local
paulson
parents: 15965
diff changeset
    35
  "HOL.If"      ("(if _/ then _/ else _)")
11533
0c0d2332e8f0 Added code generator setup.
berghofe
parents: 11483
diff changeset
    36
16770
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16635
diff changeset
    37
  "wfrec"   ("\<module>wf'_rec?")
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16635
diff changeset
    38
attach {*
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16635
diff changeset
    39
fun wf_rec f x = f (wf_rec f) x;
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16635
diff changeset
    40
*}
13093
ab0335307905 code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents: 12554
diff changeset
    41
14102
8af7334af4b3 - Installed specific code generator for equality enforcing that
berghofe
parents: 14049
diff changeset
    42
quickcheck_params [default_type = int]
8af7334af4b3 - Installed specific code generator for equality enforcing that
berghofe
parents: 14049
diff changeset
    43
13755
a9bb54a3cfb7 Added mk_int and mk_list.
berghofe
parents: 13403
diff changeset
    44
ML {*
16635
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    45
local
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    46
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    47
fun eq_codegen thy defs gr dep thyname b t =
14102
8af7334af4b3 - Installed specific code generator for equality enforcing that
berghofe
parents: 14049
diff changeset
    48
    (case strip_comb t of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15395
diff changeset
    49
       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
14102
8af7334af4b3 - Installed specific code generator for equality enforcing that
berghofe
parents: 14049
diff changeset
    50
     | (Const ("op =", _), [t, u]) =>
8af7334af4b3 - Installed specific code generator for equality enforcing that
berghofe
parents: 14049
diff changeset
    51
          let
16635
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    52
            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    53
            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u)
14102
8af7334af4b3 - Installed specific code generator for equality enforcing that
berghofe
parents: 14049
diff changeset
    54
          in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15395
diff changeset
    55
            SOME (gr'', Codegen.parens
14102
8af7334af4b3 - Installed specific code generator for equality enforcing that
berghofe
parents: 14049
diff changeset
    56
              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
8af7334af4b3 - Installed specific code generator for equality enforcing that
berghofe
parents: 14049
diff changeset
    57
          end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15395
diff changeset
    58
     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
16635
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    59
         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    60
     | _ => NONE);
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    61
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    62
in
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    63
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    64
val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    65
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    66
end;
13755
a9bb54a3cfb7 Added mk_int and mk_list.
berghofe
parents: 13403
diff changeset
    67
*}
13093
ab0335307905 code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents: 12554
diff changeset
    68
14102
8af7334af4b3 - Installed specific code generator for equality enforcing that
berghofe
parents: 14049
diff changeset
    69
setup eq_codegen_setup
8af7334af4b3 - Installed specific code generator for equality enforcing that
berghofe
parents: 14049
diff changeset
    70
16635
bf7de5723c60 Moved some code lemmas from Main to Nat.
berghofe
parents: 16587
diff changeset
    71
lemmas [code] = imp_conv_disj
12554
671b4d632c34 Declared characteristic equations for < on nat for code generation.
berghofe
parents: 12439
diff changeset
    72
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents: 14192
diff changeset
    73
subsection {* Configuration of the 'refute' command *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents: 14192
diff changeset
    74
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents: 14192
diff changeset
    75
text {*
14458
c2b96948730d changed default values for refute
webertj
parents: 14443
diff changeset
    76
  The following are fairly reasonable default values.  For an
c2b96948730d changed default values for refute
webertj
parents: 14443
diff changeset
    77
  explanation of these parameters, see 'HOL/Refute.thy'.
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents: 14192
diff changeset
    78
*}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents: 14192
diff changeset
    79
15584
3478bb4f93ff refute_params: default value itself=1 added (for type classes)
webertj
parents: 15531
diff changeset
    80
refute_params ["itself"=1,
3478bb4f93ff refute_params: default value itself=1 added (for type classes)
webertj
parents: 15531
diff changeset
    81
               minsize=1,
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents: 14192
diff changeset
    82
               maxsize=8,
14806
b42ad431cbae new default parameters for refute
webertj
parents: 14489
diff changeset
    83
               maxvars=10000,
b42ad431cbae new default parameters for refute
webertj
parents: 14489
diff changeset
    84
               maxtime=60,
b42ad431cbae new default parameters for refute
webertj
parents: 14489
diff changeset
    85
               satsolver="auto"]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents: 14192
diff changeset
    86
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
    87
end