nipkow@10519: (*  Title:      HOL/Main.thy
nipkow@10519:     ID:         $Id$
wenzelm@12024:     Author:     Stefan Berghofer, Tobias Nipkow and Markus Wenzel, TU Muenchen
wenzelm@12024:     License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@10519: *)
wenzelm@9619: 
wenzelm@12024: header {* Main HOL *}
wenzelm@12024: 
berghofe@13403: theory Main = Map + Hilbert_Choice + Extraction:
wenzelm@9650: 
wenzelm@12024: text {*
wenzelm@12024:   Theory @{text Main} includes everything.  Note that theory @{text
wenzelm@12024:   PreList} already includes most HOL theories.
wenzelm@12024: *}
wenzelm@12024: 
wenzelm@12024: subsection {* Configuration of the code generator *}
berghofe@11533: 
berghofe@11533: types_code
berghofe@11533:   "bool"  ("bool")
berghofe@12439:   "*"     ("(_ */ _)")
berghofe@12439:   "list"  ("_ list")
berghofe@11533: 
berghofe@11533: consts_code
berghofe@11533:   "True"    ("true")
berghofe@11533:   "False"   ("false")
berghofe@11533:   "Not"     ("not")
berghofe@11533:   "op |"    ("(_ orelse/ _)")
berghofe@11533:   "op &"    ("(_ andalso/ _)")
berghofe@11533:   "If"      ("(if _/ then _/ else _)")
berghofe@11533: 
berghofe@11533:   "Pair"    ("(_,/ _)")
berghofe@11533:   "fst"     ("fst")
berghofe@11533:   "snd"     ("snd")
berghofe@11533: 
berghofe@11533:   "Nil"     ("[]")
berghofe@11533:   "Cons"    ("(_ ::/ _)")
berghofe@12439: 
berghofe@13093:   "wfrec"   ("wf'_rec?")
berghofe@13093: 
berghofe@14102: quickcheck_params [default_type = int]
berghofe@14102: 
berghofe@13755: ML {*
berghofe@13755: fun wf_rec f x = f (wf_rec f) x;
berghofe@13755: 
berghofe@14102: fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
berghofe@13755: val term_of_list = HOLogic.mk_list;
berghofe@13755: val term_of_int = HOLogic.mk_int;
berghofe@14049: fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
berghofe@14102: fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
berghofe@14102: 
berghofe@14102: val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
berghofe@14102:   (fn thy => fn gr => fn dep => fn b => fn t =>
berghofe@14102:     (case strip_comb t of
berghofe@14102:        (Const ("op =", Type (_, [Type ("fun", _), _])), _) => None
berghofe@14102:      | (Const ("op =", _), [t, u]) =>
berghofe@14102:           let
berghofe@14102:             val (gr', pt) = Codegen.invoke_codegen thy dep false (gr, t);
berghofe@14102:             val (gr'', pu) = Codegen.invoke_codegen thy dep false (gr', u)
berghofe@14102:           in
berghofe@14102:             Some (gr'', Codegen.parens
berghofe@14102:               (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
berghofe@14102:           end
berghofe@14102:      | (t as Const ("op =", _), ts) => Some (Codegen.invoke_codegen
berghofe@14102:          thy dep b (gr, Codegen.eta_expand t ts 2))
berghofe@14102:      | _ => None))];
berghofe@14102: 
berghofe@14102: fun gen_bool i = one_of [false, true];
berghofe@14102: 
berghofe@14102: fun gen_list' aG i j = frequency
berghofe@14102:   [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
berghofe@14102: and gen_list aG i = gen_list' aG i i;
berghofe@14102: 
berghofe@14102: fun gen_int i = one_of [~1, 1] * random_range 0 i;
berghofe@14102: 
berghofe@14102: fun gen_id_42 aG bG i = (aG i, bG i);
berghofe@14102: 
berghofe@14102: fun gen_fun_type _ G i =
berghofe@14102:   let
berghofe@14102:     val f = ref (fn x => raise ERROR);
berghofe@14102:     val _ = (f := (fn x =>
berghofe@14102:       let
berghofe@14102:         val y = G i;
berghofe@14102:         val f' = !f
berghofe@14102:       in (f := (fn x' => if x = x' then y else f' x'); y) end))
berghofe@14102:   in (fn x => !f x) end;
berghofe@13755: *}
berghofe@13093: 
berghofe@14102: setup eq_codegen_setup
berghofe@14102: 
berghofe@12554: lemma [code]: "((n::nat) < 0) = False" by simp
berghofe@14102: lemmas [code] = less_Suc_eq imp_conv_disj
berghofe@12554: 
wenzelm@9650: end