src/HOL/ex/ROOT.ML
author wenzelm
Wed, 02 Jun 2010 13:18:21 +0200
changeset 37280 0fb011773adc
parent 36962 5fb251d1c32f
child 37695 71e84a203c19
permissions -rw-r--r--
Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
     1
(*  Title:      HOL/ex/ROOT.ML
11586
wenzelm
parents: 11445
diff changeset
     2
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
     3
Miscellaneous examples for Higher-Order Logic.
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
     4
*)
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
     5
24528
wenzelm
parents: 24478
diff changeset
     6
no_document use_thys [
24740
36750aca7a77 some more simultaneous use_thys;
wenzelm
parents: 24615
diff changeset
     7
  "State_Monad",
25963
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25738
diff changeset
     8
  "Efficient_Nat_examples",
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25738
diff changeset
     9
  "FuncSet",
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25738
diff changeset
    10
  "Eval_Examples",
31378
d1cbf6393964 tuned code generator test theories
haftmann
parents: 31181
diff changeset
    11
  "Codegenerator_Test",
d1cbf6393964 tuned code generator test theories
haftmann
parents: 31181
diff changeset
    12
  "Codegenerator_Pretty_Test",
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents: 35950
diff changeset
    13
  "NormalForm"
25963
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25738
diff changeset
    14
];
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25738
diff changeset
    15
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    16
use_thys [
28021
32acf3c6cd12 added HOL/ex/Numeral.thy
haftmann
parents: 27742
diff changeset
    17
  "Numeral",
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    18
  "Higher_Order_Logic",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    19
  "Abstract_NAT",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    20
  "Guess",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    21
  "Binary",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    22
  "Recdefs",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    23
  "Fundefs",
33471
5aef13872723 renamed method induct_scheme to induction_schema
krauss
parents: 33436
diff changeset
    24
  "Induction_Schema",
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    25
  "InductiveInvariant_examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    26
  "LocaleTest2",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    27
  "Records",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    28
  "MonoidGroup",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    29
  "BinEx",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    30
  "Hex_Bin_Examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    31
  "Antiquote",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    32
  "Multiquote",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    33
  "PER",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    34
  "NatSum",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    35
  "ThreeDivides",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    36
  "Intuitionistic",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    37
  "CTL",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    38
  "Arith_Examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    39
  "BT",
33436
nipkow
parents: 33356
diff changeset
    40
  "Tree23",
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    41
  "MergeSort",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    42
  "Lagrange",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    43
  "Groebner_Examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    44
  "MT",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    45
  "Unification",
24740
36750aca7a77 some more simultaneous use_thys;
wenzelm
parents: 24615
diff changeset
    46
  "Primrec",
36750aca7a77 some more simultaneous use_thys;
wenzelm
parents: 24615
diff changeset
    47
  "Tarski",
25738
b091cbae3e2a included meson/metis tests in simultaneous use_thys;
wenzelm
parents: 25568
diff changeset
    48
  "Classical",
b091cbae3e2a included meson/metis tests in simultaneous use_thys;
wenzelm
parents: 25568
diff changeset
    49
  "set",
27436
9581777503e9 code antiquotation roaring ahead
haftmann
parents: 27421
diff changeset
    50
  "Meson_Test",
29181
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents: 28952
diff changeset
    51
  "Termination",
29376
2071939cf0fc more parallel loading;
wenzelm
parents: 29181
diff changeset
    52
  "Coherent",
2071939cf0fc more parallel loading;
wenzelm
parents: 29181
diff changeset
    53
  "PresburgerEx",
29377
e6439dbfeee1 more parallel loading;
wenzelm
parents: 29376
diff changeset
    54
  "ReflectionEx",
e6439dbfeee1 more parallel loading;
wenzelm
parents: 29376
diff changeset
    55
  "BinEx",
e6439dbfeee1 more parallel loading;
wenzelm
parents: 29376
diff changeset
    56
  "Sqrt",
e6439dbfeee1 more parallel loading;
wenzelm
parents: 29376
diff changeset
    57
  "Sqrt_Script",
32560
c83dab2c5988 corrected upper/lowercase
haftmann
parents: 32556
diff changeset
    58
  "Transfer_Ex",
29377
e6439dbfeee1 more parallel loading;
wenzelm
parents: 29376
diff changeset
    59
  "Arithmetic_Series_Complex",
e6439dbfeee1 more parallel loading;
wenzelm
parents: 29376
diff changeset
    60
  "HarmonicSeries",
e6439dbfeee1 more parallel loading;
wenzelm
parents: 29376
diff changeset
    61
  "Refute_Examples",
29697
e8785144719d Added Formal_Power_Series_Examples to HOL-ex image
chaieb
parents: 29650
diff changeset
    62
  "Quickcheck_Examples",
35160
6eb2b6c1d2d5 a draft for an example how to turn specifications involving choice executable
haftmann
parents: 33651
diff changeset
    63
  "Landau",
35163
2e0966d6f951 added simple theory about discrete summation
haftmann
parents: 35160
diff changeset
    64
  "Execute_Choice",
35328
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 35163
diff changeset
    65
  "Summation",
36793
27da0a27b76f put construction of reals using Dedekind cuts in HOL/ex
huffman
parents: 35953
diff changeset
    66
  "Gauge_Integration",
27da0a27b76f put construction of reals using Dedekind cuts in HOL/ex
huffman
parents: 35953
diff changeset
    67
  "Dedekind_Real"
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    68
];
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 20866
diff changeset
    69
33546
5e2d381b0695 try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents: 33471
diff changeset
    70
HTML.with_charset "utf-8" (no_document use_thys)
5e2d381b0695 try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents: 33471
diff changeset
    71
  ["Hebrew", "Chinese", "Serbian"];
5e2d381b0695 try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents: 33471
diff changeset
    72
37280
0fb011773adc Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;
wenzelm
parents: 36962
diff changeset
    73
(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
32256
8721c74c5382 Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
wenzelm
parents: 32254
diff changeset
    74
  "Hilbert_Classical";
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    75
29376
2071939cf0fc more parallel loading;
wenzelm
parents: 29181
diff changeset
    76
use_thy "SVC_Oracle";
32428
700ed1f4c576 SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
wenzelm
parents: 32259
diff changeset
    77
if getenv "SVC_HOME" = "" then ()
700ed1f4c576 SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
wenzelm
parents: 32259
diff changeset
    78
else use_thy "svc_test";
29376
2071939cf0fc more parallel loading;
wenzelm
parents: 29181
diff changeset
    79
32428
700ed1f4c576 SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
wenzelm
parents: 32259
diff changeset
    80
(*requires zChaff (or some other reasonably fast SAT solver)*)
700ed1f4c576 SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
wenzelm
parents: 32259
diff changeset
    81
if getenv "ZCHAFF_HOME" = "" then ()
700ed1f4c576 SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
wenzelm
parents: 32259
diff changeset
    82
else use_thy "Sudoku";
18408
07da804d1119 ex/Sudoku.thy
webertj
parents: 17783
diff changeset
    83
33546
5e2d381b0695 try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents: 33471
diff changeset
    84
(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
5e2d381b0695 try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents: 33471
diff changeset
    85
(*global side-effects ahead!*)
5e2d381b0695 try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents: 33471
diff changeset
    86
try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)