author  berghofe 
Mon, 22 Sep 2003 16:01:36 +0200  
changeset 14192  d6cb80cc1d20 
parent 14102  8af7334af4b3 
child 14350  41b32020d0b3 
permissions  rwrr 
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 newstyle 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 
"True" ("true") 

25 
"False" ("false") 

26 
"Not" ("not") 

27 
"op " ("(_ orelse/ _)") 

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

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

30 

31 
"Pair" ("(_,/ _)") 

32 
"fst" ("fst") 

33 
"snd" ("snd") 

34 

35 
"Nil" ("[]") 

36 
"Cons" ("(_ ::/ _)") 

12439  37 

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

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

39 

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

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

41 

13755  42 
ML {* 
43 
fun wf_rec f x = f (wf_rec f) x; 

44 

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

45 
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; 
13755  46 
val term_of_list = HOLogic.mk_list; 
47 
val term_of_int = HOLogic.mk_int; 

14049  48 
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

49 
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

50 

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

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

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

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

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

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

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

57 
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

58 
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

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

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

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

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

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

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

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

66 

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

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

68 

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

69 
fun gen_list' aG i j = frequency 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

70 
[(i, fn () => aG j :: gen_list' aG (i1) j), (1, fn () => [])] () 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

71 
and gen_list aG i = gen_list' aG i i; 
8af7334af4b3
 Installed specific code generator for equality enforcing that
berghofe
parents:
14049
diff
changeset

72 

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

73 
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

74 

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

75 
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

76 

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

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

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

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

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

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

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

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

84 
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

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

87 

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

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

89 

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

90 
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

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

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

93 

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

94 
end 