isabelle: src/HOL/ex/ROOT.ML@40306cc4d16a (annotated)

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

author	haftmann
	Thu, 25 Sep 2008 11:14:01 +0200
changeset 28353	40306cc4d16a
parent 28352	cab797b79421
child 28630	3a4ed60b6b7e
permissions	-rw-r--r--