1 (* Title: HOL/Main.thy |
1 (* $Id$ *) |
2 ID: $Id$ |
|
3 Author: Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen) |
|
4 *) |
|
5 |
2 |
6 header {* Main HOL *} |
3 header {* Main HOL *} |
7 |
4 |
8 theory Main |
5 theory Main |
9 imports Refute Reconstruction |
6 imports Refute Reconstruction |
10 (*other theores need to be ancestors of Reconstruction, not Main!!*) |
|
11 |
|
12 begin |
7 begin |
13 |
8 |
14 text {* |
9 text {* |
15 Theory @{text Main} includes everything. Note that theory @{text |
10 Theory @{text Main} includes everything. Note that theory @{text |
16 PreList} already includes most HOL theories. |
11 PreList} already includes most HOL theories. |
17 *} |
12 *} |
18 |
13 |
19 |
14 |
20 subsection {* Misc *} |
15 subsection {* Special hacks, late package setup etc. *} |
21 |
16 |
22 text {* Hide the rather generic names used in theory @{text Commutative_Ring}. *} |
17 text {* \medskip Hide the rather generic names used in theory @{text |
|
18 Commutative_Ring}. *} |
23 |
19 |
24 hide (open) const |
20 hide (open) const |
25 Pc Pinj PX |
21 Pc Pinj PX |
26 Pol Add Sub Mul Pow Neg |
22 Pol Add Sub Mul Pow Neg |
27 add mul neg sqr pow sub |
23 add mul neg sqr pow sub |
28 norm |
24 norm |
29 |
25 |
30 |
26 |
31 subsection {* Configuration of the code generator *} |
27 text {* \medskip Default values for rufute, see also theory @{text |
32 |
28 Refute}. |
33 types_code |
|
34 "bool" ("bool") |
|
35 attach (term_of) {* |
|
36 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; |
|
37 *} |
|
38 attach (test) {* |
|
39 fun gen_bool i = one_of [false, true]; |
|
40 *} |
29 *} |
41 |
30 |
42 consts_code |
31 refute_params |
43 "True" ("true") |
32 ["itself"=1, |
44 "False" ("false") |
33 minsize=1, |
45 "Not" ("not") |
34 maxsize=8, |
46 "op |" ("(_ orelse/ _)") |
35 maxvars=10000, |
47 "op &" ("(_ andalso/ _)") |
36 maxtime=60, |
48 "HOL.If" ("(if _/ then _/ else _)") |
37 satsolver="auto"] |
49 |
|
50 "wfrec" ("\<module>wf'_rec?") |
|
51 attach {* |
|
52 fun wf_rec f x = f (wf_rec f) x; |
|
53 *} |
|
54 |
|
55 quickcheck_params [default_type = int] |
|
56 |
|
57 ML {* |
|
58 local |
|
59 |
|
60 fun eq_codegen thy defs gr dep thyname b t = |
|
61 (case strip_comb t of |
|
62 (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE |
|
63 | (Const ("op =", _), [t, u]) => |
|
64 let |
|
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) |
|
67 in |
|
68 SOME (gr'', Codegen.parens |
|
69 (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu])) |
|
70 end |
|
71 | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen |
|
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; |
|
80 *} |
|
81 |
|
82 setup eq_codegen_setup |
|
83 |
|
84 lemmas [code] = imp_conv_disj |
|
85 |
38 |
86 |
39 |
87 subsection {* Configuration of the 'refute' command *} |
40 text {* \medskip Clause setup: installs \emph{all} simprules and |
|
41 claset rules into the clause cache; cf.\ theory @{text |
|
42 Reconstruction}. *} |
88 |
43 |
89 text {* |
44 setup ResAxioms.clause_setup |
90 The following are fairly reasonable default values. For an |
|
91 explanation of these parameters, see 'HOL/Refute.thy'. |
|
92 *} |
|
93 |
|
94 refute_params ["itself"=1, |
|
95 minsize=1, |
|
96 maxsize=8, |
|
97 maxvars=10000, |
|
98 maxtime=60, |
|
99 satsolver="auto"] |
|
100 |
45 |
101 end |
46 end |