src/HOL/ex/ROOT.ML
author haftmann
Wed, 03 Dec 2008 15:58:44 +0100
changeset 28952 15a4b2cf8c34
parent 28866 30cd9d89a0fb
child 29181 cc177742e607
permissions -rw-r--r--
made repository layout more coherent with logical distribution structure; stripped some $Id$s
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
  "ExecutableContent",
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25738
diff changeset
    10
  "FuncSet",
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25738
diff changeset
    11
  "Word",
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25738
diff changeset
    12
  "Eval_Examples",
28243
84d90ec67059 moved term_of syntax to separate theory
haftmann
parents: 28228
diff changeset
    13
  "Quickcheck",
84d90ec67059 moved term_of syntax to separate theory
haftmann
parents: 28228
diff changeset
    14
  "Term_Of_Syntax"
25963
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25738
diff changeset
    15
];
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25738
diff changeset
    16
25975
bcb1e9b7644b Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents: 25963
diff changeset
    17
no_document use_thy "Codegenerator";
28353
40306cc4d16a (temporary workaround)
haftmann
parents: 28352
diff changeset
    18
no_document use_thy "Codegenerator_Pretty";
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    19
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    20
use_thys [
28021
32acf3c6cd12 added HOL/ex/Numeral.thy
haftmann
parents: 27742
diff changeset
    21
  "Numeral",
27679
haftmann
parents: 27482
diff changeset
    22
  "ImperativeQuicksort",
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    23
  "Higher_Order_Logic",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    24
  "Abstract_NAT",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    25
  "Guess",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    26
  "Binary",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    27
  "Recdefs",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    28
  "Fundefs",
25568
7bb10db582cf Adding "ex/Induction_Scheme.thy" to tests
krauss
parents: 25543
diff changeset
    29
  "Induction_Scheme",
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    30
  "InductiveInvariant_examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    31
  "LocaleTest2",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    32
  "Records",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    33
  "MonoidGroup",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    34
  "BinEx",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    35
  "Hex_Bin_Examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    36
  "Antiquote",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    37
  "Multiquote",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    38
  "PER",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    39
  "NatSum",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    40
  "ThreeDivides",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    41
  "Intuitionistic",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    42
  "CTL",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    43
  "Arith_Examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    44
  "BT",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    45
  "MergeSort",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    46
  "Lagrange",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    47
  "Groebner_Examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    48
  "MT",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    49
  "Unification",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    50
  "Commutative_RingEx",
24740
36750aca7a77 some more simultaneous use_thys;
wenzelm
parents: 24615
diff changeset
    51
  "Commutative_Ring_Complete",
36750aca7a77 some more simultaneous use_thys;
wenzelm
parents: 24615
diff changeset
    52
  "Primrec",
36750aca7a77 some more simultaneous use_thys;
wenzelm
parents: 24615
diff changeset
    53
  "Tarski",
25738
b091cbae3e2a included meson/metis tests in simultaneous use_thys;
wenzelm
parents: 25568
diff changeset
    54
  "Adder",
b091cbae3e2a included meson/metis tests in simultaneous use_thys;
wenzelm
parents: 25568
diff changeset
    55
  "Classical",
b091cbae3e2a included meson/metis tests in simultaneous use_thys;
wenzelm
parents: 25568
diff changeset
    56
  "set",
27436
9581777503e9 code antiquotation roaring ahead
haftmann
parents: 27421
diff changeset
    57
  "Meson_Test",
27742
df552e6027cf fix HOL/ex/LexOrds.thy; add to regression
krauss
parents: 27679
diff changeset
    58
  "Code_Antiq",
28324
0dd1a0b16a37 Added examples for coherent logic prover.
berghofe
parents: 28263
diff changeset
    59
  "LexOrds",
0dd1a0b16a37 Added examples for coherent logic prover.
berghofe
parents: 28263
diff changeset
    60
  "Coherent"
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    61
];
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 20866
diff changeset
    62
25374
7657a081fcb4 qualified Proofterm.proofs;
wenzelm
parents: 24994
diff changeset
    63
setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical";
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    64
23454
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23302
diff changeset
    65
time_use_thy "Dense_Linear_Order_Ex";
13880
4f7f30f68926 Added examples for Presburger arithmetic.
berghofe
parents: 13200
diff changeset
    66
time_use_thy "PresburgerEx";
23808
4e4b92e76219 fixed SML/NJ int problem
haftmann
parents: 23502
diff changeset
    67
time_use_thy "Reflected_Presburger";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    68
28866
30cd9d89a0fb reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents: 28630
diff changeset
    69
use_thys ["Reflection", "ReflectionEx"];
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    70
12869
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents: 12450
diff changeset
    71
time_use_thy "SVC_Oracle";
28263
69eaa97e7e96 moved global ML bindings to global place;
wenzelm
parents: 28243
diff changeset
    72
69eaa97e7e96 moved global ML bindings to global place;
wenzelm
parents: 28243
diff changeset
    73
(*check if user has SVC installed*)
69eaa97e7e96 moved global ML bindings to global place;
wenzelm
parents: 28243
diff changeset
    74
fun svc_enabled () = getenv "SVC_HOME" <> "";
69eaa97e7e96 moved global ML bindings to global place;
wenzelm
parents: 28243
diff changeset
    75
fun if_svc_enabled f x = if svc_enabled () then f x else ();
69eaa97e7e96 moved global ML bindings to global place;
wenzelm
parents: 28243
diff changeset
    76
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    77
if_svc_enabled time_use_thy "svc_test";
14459
0a8619367a61 added Refute_Examples.thy
webertj
parents: 14244
diff changeset
    78
23191
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    79
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    80
(* installed:                                                       *)
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18408
diff changeset
    81
try time_use_thy "SAT_Examples";
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents: 17505
diff changeset
    82
23191
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    83
(* requires zChaff (or some other reasonably fast SAT solver) to be *)
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    84
(* installed:                                                       *)
18408
07da804d1119 ex/Sudoku.thy
webertj
parents: 17783
diff changeset
    85
if getenv "ZCHAFF_HOME" <> "" then
07da804d1119 ex/Sudoku.thy
webertj
parents: 17783
diff changeset
    86
  time_use_thy "Sudoku"
23191
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    87
else ();
18408
07da804d1119 ex/Sudoku.thy
webertj
parents: 17783
diff changeset
    88
14462
e6550f190fe9 Refute_Examples added/fixed
webertj
parents: 14459
diff changeset
    89
time_use_thy "Refute_Examples";
14592
dd1a2905ea73 Added theory with examples for quickcheck command.
berghofe
parents: 14569
diff changeset
    90
time_use_thy "Quickcheck_Examples";
19832
1a09f25410da nbe -> NormalForm
nipkow
parents: 19438
diff changeset
    91
no_document time_use_thy "NormalForm";
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents: 14482
diff changeset
    92
25975
bcb1e9b7644b Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents: 25963
diff changeset
    93
HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"];
bcb1e9b7644b Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents: 25963
diff changeset
    94
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 26265
diff changeset
    95
no_document use_thys [
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 26265
diff changeset
    96
  "../NumberTheory/Factorization",
28098
c92850d2d16c Replaced Library/NatPair by Nat_Int_Bij.
nipkow
parents: 28021
diff changeset
    97
  "../Library/BigO"
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 26265
diff changeset
    98
];
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 26265
diff changeset
    99
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 26265
diff changeset
   100
use_thys [
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28866
diff changeset
   101
  "BinEx",
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28866
diff changeset
   102
  "Sqrt",
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28866
diff changeset
   103
  "Sqrt_Script",
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28866
diff changeset
   104
  "BigO_Complex",
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 26265
diff changeset
   105
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28866
diff changeset
   106
  "Arithmetic_Series_Complex",
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28866
diff changeset
   107
  "HarmonicSeries",
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 26265
diff changeset
   108
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28866
diff changeset
   109
  "MIR",
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28866
diff changeset
   110
  "ReflectedFerrack"
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 26265
diff changeset
   111
];
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 26265
diff changeset
   112