author  wenzelm 
Wed, 14 Sep 2005 22:04:37 +0200  
changeset 17386  b110730a24fd 
parent 16770  1f1b1fae30e4 
child 17395  a05e20f6a31a 
permissions  rwrr 
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 
17386  9 
imports Commutative_Ring Refute Reconstruction 
15151  10 

15131  11 
begin 
9650
6f0b89f2a1f9
Main now newstyle theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset

12 

12024  13 
text {* 
14 
Theory @{text Main} includes everything. Note that theory @{text 

15 
PreList} already includes most HOL theories. 

16 
*} 

17 

18 
subsection {* Configuration of the code generator *} 

11533  19 

20 
types_code 

21 
"bool" ("bool") 

16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset

22 
attach (term_of) {* 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset

23 
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

24 
*} 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset

25 
attach (test) {* 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset

26 
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

27 
*} 
11533  28 

29 
consts_code 

30 
"True" ("true") 

31 
"False" ("false") 

32 
"Not" ("not") 

33 
"op " ("(_ orelse/ _)") 

34 
"op &" ("(_ andalso/ _)") 

16587  35 
"HOL.If" ("(if _/ then _/ else _)") 
11533  36 

16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset

37 
"wfrec" ("\<module>wf'_rec?") 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset

38 
attach {* 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset

39 
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

40 
*} 
13093
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset

41 

14102
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

42 
quickcheck_params [default_type = int] 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

43 

13755  44 
ML {* 
16635  45 
local 
46 

47 
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

48 
(case strip_comb t of 
15531  49 
(Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE 
14102
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

50 
 (Const ("op =", _), [t, u]) => 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

51 
let 
16635  52 
val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t); 
53 
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

54 
in 
15531  55 
SOME (gr'', Codegen.parens 
14102
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

56 
(Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu])) 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

57 
end 
15531  58 
 (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen 
16635  59 
thy defs dep thyname b (gr, Codegen.eta_expand t ts 2)) 
60 
 _ => NONE); 

61 

62 
in 

63 

64 
val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen]; 

65 

66 
end; 

13755  67 
*} 
13093
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset

68 

14102
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

69 
setup eq_codegen_setup 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

70 

16635  71 
lemmas [code] = imp_conv_disj 
12554
671b4d632c34
Declared characteristic equations for < on nat for code generation.
berghofe
parents:
12439
diff
changeset

72 

14350  73 
subsection {* Configuration of the 'refute' command *} 
74 

75 
text {* 

14458  76 
The following are fairly reasonable default values. For an 
77 
explanation of these parameters, see 'HOL/Refute.thy'. 

14350  78 
*} 
79 

15584
3478bb4f93ff
refute_params: default value itself=1 added (for type classes)
webertj
parents:
15531
diff
changeset

80 
refute_params ["itself"=1, 
3478bb4f93ff
refute_params: default value itself=1 added (for type classes)
webertj
parents:
15531
diff
changeset

81 
minsize=1, 
14350  82 
maxsize=8, 
14806  83 
maxvars=10000, 
84 
maxtime=60, 

85 
satsolver="auto"] 

14350  86 

9650
6f0b89f2a1f9
Main now newstyle theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset

87 
end 