src/HOL/Main.thy
author berghofe
Mon Jul 19 18:15:46 2004 +0200 (2004-07-19)
changeset 15063 a43d771c18ac
parent 14981 e73f8140af78
child 15131 c69542757a4d
permissions -rw-r--r--
Moved code generator setup for lists to List.thy
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
     4 *)
     5 
     6 header {* Main HOL *}
     7 
     8 theory Main = Map + Infinite_Set + Extraction + Refute:
     9 
    10 text {*
    11   Theory @{text Main} includes everything.  Note that theory @{text
    12   PreList} already includes most HOL theories.
    13 *}
    14 
    15 subsection {* Configuration of the code generator *}
    16 
    17 types_code
    18   "bool"  ("bool")
    19   "*"     ("(_ */ _)")
    20 
    21 consts_code
    22   "True"    ("true")
    23   "False"   ("false")
    24   "Not"     ("not")
    25   "op |"    ("(_ orelse/ _)")
    26   "op &"    ("(_ andalso/ _)")
    27   "If"      ("(if _/ then _/ else _)")
    28 
    29   "Pair"    ("(_,/ _)")
    30   "fst"     ("fst")
    31   "snd"     ("snd")
    32 
    33   "wfrec"   ("wf'_rec?")
    34 
    35 quickcheck_params [default_type = int]
    36 
    37 ML {*
    38 fun wf_rec f x = f (wf_rec f) x;
    39 
    40 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    41 val term_of_int = HOLogic.mk_int;
    42 fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
    43 fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    44 
    45 val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
    46   (fn thy => fn gr => fn dep => fn b => fn t =>
    47     (case strip_comb t of
    48        (Const ("op =", Type (_, [Type ("fun", _), _])), _) => None
    49      | (Const ("op =", _), [t, u]) =>
    50           let
    51             val (gr', pt) = Codegen.invoke_codegen thy dep false (gr, t);
    52             val (gr'', pu) = Codegen.invoke_codegen thy dep false (gr', u)
    53           in
    54             Some (gr'', Codegen.parens
    55               (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    56           end
    57      | (t as Const ("op =", _), ts) => Some (Codegen.invoke_codegen
    58          thy dep b (gr, Codegen.eta_expand t ts 2))
    59      | _ => None))];
    60 
    61 fun gen_bool i = one_of [false, true];
    62 
    63 fun gen_int i = one_of [~1, 1] * random_range 0 i;
    64 
    65 fun gen_id_42 aG bG i = (aG i, bG i);
    66 
    67 fun gen_fun_type _ G i =
    68   let
    69     val f = ref (fn x => raise ERROR);
    70     val _ = (f := (fn x =>
    71       let
    72         val y = G i;
    73         val f' = !f
    74       in (f := (fn x' => if x = x' then y else f' x'); y) end))
    75   in (fn x => !f x) end;
    76 *}
    77 
    78 setup eq_codegen_setup
    79 
    80 lemma [code]: "((n::nat) < 0) = False" by simp
    81 lemma [code]: "(0 < Suc n) = True" by simp
    82 lemmas [code] = Suc_less_eq imp_conv_disj
    83 
    84 subsection {* Configuration of the 'refute' command *}
    85 
    86 text {*
    87   The following are fairly reasonable default values.  For an
    88   explanation of these parameters, see 'HOL/Refute.thy'.
    89 *}
    90 
    91 refute_params [minsize=1,
    92                maxsize=8,
    93                maxvars=10000,
    94                maxtime=60,
    95                satsolver="auto"]
    96 
    97 end