author | paulson |
Thu, 15 Sep 2005 17:45:17 +0200 | |
changeset 17421 | 0382f6877b98 |
parent 17395 | a05e20f6a31a |
child 17461 | 83f1dd9d901d |
permissions | -rw-r--r-- |
10519 | 1 |
(* Title: HOL/Main.thy |
2 |
ID: $Id$ |
|
14350 | 3 |
Author: Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen) |
10519 | 4 |
*) |
9619 | 5 |
|
12024 | 6 |
header {* Main HOL *} |
7 |
||
15131 | 8 |
theory Main |
17421 | 9 |
imports Refute Reconstruction |
10 |
(*other theores need to be ancestors of Reconstruction, not Main!!*) |
|
15151 | 11 |
|
15131 | 12 |
begin |
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
13 |
|
12024 | 14 |
text {* |
15 |
Theory @{text Main} includes everything. Note that theory @{text |
|
16 |
PreList} already includes most HOL theories. |
|
17 |
*} |
|
18 |
||
17395
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
19 |
|
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
20 |
subsection {* Misc *} |
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
21 |
|
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
22 |
text {* Hide the rather generic names used in theory @{text Commutative_Ring}. *} |
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
23 |
|
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
24 |
hide (open) const |
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
25 |
Pc Pinj PX |
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
26 |
Pol Add Sub Mul Pow Neg |
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
27 |
add mul neg sqr pow sub |
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
28 |
norm |
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
29 |
|
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
30 |
|
12024 | 31 |
subsection {* Configuration of the code generator *} |
11533 | 32 |
|
33 |
types_code |
|
34 |
"bool" ("bool") |
|
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset
|
35 |
attach (term_of) {* |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset
|
36 |
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
|
37 |
*} |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset
|
38 |
attach (test) {* |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset
|
39 |
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
|
40 |
*} |
11533 | 41 |
|
42 |
consts_code |
|
43 |
"True" ("true") |
|
44 |
"False" ("false") |
|
45 |
"Not" ("not") |
|
46 |
"op |" ("(_ orelse/ _)") |
|
47 |
"op &" ("(_ andalso/ _)") |
|
16587 | 48 |
"HOL.If" ("(if _/ then _/ else _)") |
11533 | 49 |
|
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset
|
50 |
"wfrec" ("\<module>wf'_rec?") |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset
|
51 |
attach {* |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset
|
52 |
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
|
53 |
*} |
13093
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset
|
54 |
|
14102
8af7334af4b3
- Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset
|
55 |
quickcheck_params [default_type = int] |
8af7334af4b3
- Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset
|
56 |
|
13755 | 57 |
ML {* |
16635 | 58 |
local |
59 |
||
60 |
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
|
61 |
(case strip_comb t of |
15531 | 62 |
(Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE |
14102
8af7334af4b3
- Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset
|
63 |
| (Const ("op =", _), [t, u]) => |
8af7334af4b3
- Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset
|
64 |
let |
16635 | 65 |
val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t); |
66 |
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
|
67 |
in |
15531 | 68 |
SOME (gr'', Codegen.parens |
14102
8af7334af4b3
- Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset
|
69 |
(Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu])) |
8af7334af4b3
- Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset
|
70 |
end |
15531 | 71 |
| (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen |
16635 | 72 |
thy defs dep thyname b (gr, Codegen.eta_expand t ts 2)) |
73 |
| _ => NONE); |
|
74 |
||
75 |
in |
|
76 |
||
77 |
val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen]; |
|
78 |
||
79 |
end; |
|
13755 | 80 |
*} |
13093
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset
|
81 |
|
14102
8af7334af4b3
- Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset
|
82 |
setup eq_codegen_setup |
8af7334af4b3
- Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset
|
83 |
|
16635 | 84 |
lemmas [code] = imp_conv_disj |
12554
671b4d632c34
Declared characteristic equations for < on nat for code generation.
berghofe
parents:
12439
diff
changeset
|
85 |
|
17395
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
86 |
|
14350 | 87 |
subsection {* Configuration of the 'refute' command *} |
88 |
||
89 |
text {* |
|
14458 | 90 |
The following are fairly reasonable default values. For an |
91 |
explanation of these parameters, see 'HOL/Refute.thy'. |
|
14350 | 92 |
*} |
93 |
||
15584
3478bb4f93ff
refute_params: default value itself=1 added (for type classes)
webertj
parents:
15531
diff
changeset
|
94 |
refute_params ["itself"=1, |
3478bb4f93ff
refute_params: default value itself=1 added (for type classes)
webertj
parents:
15531
diff
changeset
|
95 |
minsize=1, |
14350 | 96 |
maxsize=8, |
14806 | 97 |
maxvars=10000, |
98 |
maxtime=60, |
|
99 |
satsolver="auto"] |
|
14350 | 100 |
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
101 |
end |