| author | kleing |
| Sun, 06 Apr 2003 21:16:50 +0200 | |
| changeset 13901 | af38553e61ee |
| parent 13755 | a9bb54a3cfb7 |
| child 14049 | ef1da11a64b9 |
| permissions | -rw-r--r-- |
| 10519 | 1 |
(* Title: HOL/Main.thy |
2 |
ID: $Id$ |
|
| 12024 | 3 |
Author: Stefan Berghofer, Tobias Nipkow and Markus Wenzel, TU Muenchen |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
| 10519 | 5 |
*) |
| 9619 | 6 |
|
| 12024 | 7 |
header {* Main HOL *}
|
8 |
||
| 13403 | 9 |
theory Main = Map + Hilbert_Choice + Extraction: |
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
10 |
|
| 12024 | 11 |
text {*
|
12 |
Theory @{text Main} includes everything. Note that theory @{text
|
|
13 |
PreList} already includes most HOL theories. |
|
14 |
*} |
|
15 |
||
16 |
subsection {* Configuration of the code generator *}
|
|
| 11533 | 17 |
|
18 |
types_code |
|
19 |
"bool" ("bool")
|
|
| 12439 | 20 |
"*" ("(_ */ _)")
|
21 |
"list" ("_ list")
|
|
| 11533 | 22 |
|
23 |
consts_code |
|
24 |
"op =" ("(_ =/ _)")
|
|
25 |
||
26 |
"True" ("true")
|
|
27 |
"False" ("false")
|
|
28 |
"Not" ("not")
|
|
29 |
"op |" ("(_ orelse/ _)")
|
|
30 |
"op &" ("(_ andalso/ _)")
|
|
31 |
"If" ("(if _/ then _/ else _)")
|
|
32 |
||
33 |
"Pair" ("(_,/ _)")
|
|
34 |
"fst" ("fst")
|
|
35 |
"snd" ("snd")
|
|
36 |
||
37 |
"Nil" ("[]")
|
|
38 |
"Cons" ("(_ ::/ _)")
|
|
| 12439 | 39 |
|
|
13093
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset
|
40 |
"wfrec" ("wf'_rec?")
|
|
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset
|
41 |
|
| 13755 | 42 |
ML {*
|
43 |
fun wf_rec f x = f (wf_rec f) x; |
|
44 |
||
45 |
val term_of_list = HOLogic.mk_list; |
|
46 |
val term_of_int = HOLogic.mk_int; |
|
47 |
*} |
|
|
13093
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset
|
48 |
|
|
12554
671b4d632c34
Declared characteristic equations for < on nat for code generation.
berghofe
parents:
12439
diff
changeset
|
49 |
lemma [code]: "((n::nat) < 0) = False" by simp |
|
671b4d632c34
Declared characteristic equations for < on nat for code generation.
berghofe
parents:
12439
diff
changeset
|
50 |
declare less_Suc_eq [code] |
|
671b4d632c34
Declared characteristic equations for < on nat for code generation.
berghofe
parents:
12439
diff
changeset
|
51 |
|
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
52 |
end |