author  paulson 
Fri, 20 Aug 2004 12:21:03 +0200  
changeset 15151  429666b09783 
parent 15140  322485b816ac 
child 15382  e56ce5cefe9c 
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 
15151  9 
imports Map Infinite_Set Extraction Refute Reconstruction 
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") 

12439  22 
"*" ("(_ */ _)") 
11533  23 

24 
consts_code 

25 
"True" ("true") 

26 
"False" ("false") 

27 
"Not" ("not") 

28 
"op " ("(_ orelse/ _)") 

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

30 
"If" ("(if _/ then _/ else _)") 

31 

32 
"Pair" ("(_,/ _)") 

33 
"fst" ("fst") 

34 
"snd" ("snd") 

35 

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

36 
"wfrec" ("wf'_rec?") 
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset

37 

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

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

39 

13755  40 
ML {* 
41 
fun wf_rec f x = f (wf_rec f) x; 

42 

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

43 
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; 
13755  44 
val term_of_int = HOLogic.mk_int; 
14049  45 
fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y; 
14102
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

46 
fun term_of_fun_type _ T _ U _ = Free ("<function>", T > U); 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

47 

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

48 
val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

49 
(fn thy => fn gr => fn dep => fn b => fn t => 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

50 
(case strip_comb t of 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

51 
(Const ("op =", Type (_, [Type ("fun", _), _])), _) => None 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

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

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

54 
val (gr', pt) = Codegen.invoke_codegen thy dep false (gr, t); 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

55 
val (gr'', pu) = Codegen.invoke_codegen thy dep false (gr', u) 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

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

57 
Some (gr'', Codegen.parens 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

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

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

60 
 (t as Const ("op =", _), ts) => Some (Codegen.invoke_codegen 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

61 
thy dep b (gr, Codegen.eta_expand t ts 2)) 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

62 
 _ => None))]; 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

63 

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

64 
fun gen_bool i = one_of [false, true]; 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

65 

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

66 
fun gen_int i = one_of [~1, 1] * random_range 0 i; 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

67 

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

68 
fun gen_id_42 aG bG i = (aG i, bG i); 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

69 

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

70 
fun gen_fun_type _ G i = 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

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

72 
val f = ref (fn x => raise ERROR); 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

73 
val _ = (f := (fn x => 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

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

75 
val y = G i; 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

76 
val f' = !f 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

77 
in (f := (fn x' => if x = x' then y else f' x'); y) end)) 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

78 
in (fn x => !f x) end; 
13755  79 
*} 
13093
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset

80 

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

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

82 

12554
671b4d632c34
Declared characteristic equations for < on nat for code generation.
berghofe
parents:
12439
diff
changeset

83 
lemma [code]: "((n::nat) < 0) = False" by simp 
14192
d6cb80cc1d20
Improved efficiency of code generated for < predicate on natural numbers.
berghofe
parents:
14102
diff
changeset

84 
lemma [code]: "(0 < Suc n) = True" by simp 
d6cb80cc1d20
Improved efficiency of code generated for < predicate on natural numbers.
berghofe
parents:
14102
diff
changeset

85 
lemmas [code] = Suc_less_eq imp_conv_disj 
12554
671b4d632c34
Declared characteristic equations for < on nat for code generation.
berghofe
parents:
12439
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 

94 
refute_params [minsize=1, 

95 
maxsize=8, 

14806  96 
maxvars=10000, 
97 
maxtime=60, 

98 
satsolver="auto"] 

14350  99 

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

100 
end 