src/HOL/Main.thy
author webertj
Fri Mar 26 19:58:43 2004 +0100 (2004-03-26)
changeset 14489 3676def6b8b9
parent 14458 c2b96948730d
child 14806 b42ad431cbae
permissions -rw-r--r--
satsolver=dpll
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 header {* Main HOL *}
     8 
     9 theory Main = Map + Infinite_Set + Extraction + Refute:
    10 
    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 *}
    17 
    18 types_code
    19   "bool"  ("bool")
    20   "*"     ("(_ */ _)")
    21   "list"  ("_ list")
    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"    ("(_ ::/ _)")
    37 
    38   "wfrec"   ("wf'_rec?")
    39 
    40 quickcheck_params [default_type = int]
    41 
    42 ML {*
    43 fun wf_rec f x = f (wf_rec f) x;
    44 
    45 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    46 val term_of_list = HOLogic.mk_list;
    47 val term_of_int = HOLogic.mk_int;
    48 fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
    49 fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    50 
    51 val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
    52   (fn thy => fn gr => fn dep => fn b => fn t =>
    53     (case strip_comb t of
    54        (Const ("op =", Type (_, [Type ("fun", _), _])), _) => None
    55      | (Const ("op =", _), [t, u]) =>
    56           let
    57             val (gr', pt) = Codegen.invoke_codegen thy dep false (gr, t);
    58             val (gr'', pu) = Codegen.invoke_codegen thy dep false (gr', u)
    59           in
    60             Some (gr'', Codegen.parens
    61               (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    62           end
    63      | (t as Const ("op =", _), ts) => Some (Codegen.invoke_codegen
    64          thy dep b (gr, Codegen.eta_expand t ts 2))
    65      | _ => None))];
    66 
    67 fun gen_bool i = one_of [false, true];
    68 
    69 fun gen_list' aG i j = frequency
    70   [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
    71 and gen_list aG i = gen_list' aG i i;
    72 
    73 fun gen_int i = one_of [~1, 1] * random_range 0 i;
    74 
    75 fun gen_id_42 aG bG i = (aG i, bG i);
    76 
    77 fun gen_fun_type _ G i =
    78   let
    79     val f = ref (fn x => raise ERROR);
    80     val _ = (f := (fn x =>
    81       let
    82         val y = G i;
    83         val f' = !f
    84       in (f := (fn x' => if x = x' then y else f' x'); y) end))
    85   in (fn x => !f x) end;
    86 *}
    87 
    88 setup eq_codegen_setup
    89 
    90 lemma [code]: "((n::nat) < 0) = False" by simp
    91 lemma [code]: "(0 < Suc n) = True" by simp
    92 lemmas [code] = Suc_less_eq imp_conv_disj
    93 
    94 subsection {* Configuration of the 'refute' command *}
    95 
    96 text {*
    97   The following are fairly reasonable default values.  For an
    98   explanation of these parameters, see 'HOL/Refute.thy'.
    99 *}
   100 
   101 refute_params [minsize=1,
   102                maxsize=8,
   103                maxvars=100,
   104                satsolver="dpll"]
   105 
   106 end