src/HOL/Main.thy
author paulson
Mon Mar 08 11:12:06 2004 +0100 (2004-03-08)
changeset 14443 75910c7557c5
parent 14350 41b32020d0b3
child 14458 c2b96948730d
permissions -rw-r--r--
generic theorems about exponentials; general tidying up
nipkow@10519
     1
(*  Title:      HOL/Main.thy
nipkow@10519
     2
    ID:         $Id$
webertj@14350
     3
    Author:     Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
wenzelm@12024
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@10519
     5
*)
wenzelm@9619
     6
wenzelm@12024
     7
header {* Main HOL *}
wenzelm@12024
     8
paulson@14443
     9
theory Main = Map + Infinite_Set + Extraction + Refute:
wenzelm@9650
    10
wenzelm@12024
    11
text {*
wenzelm@12024
    12
  Theory @{text Main} includes everything.  Note that theory @{text
wenzelm@12024
    13
  PreList} already includes most HOL theories.
wenzelm@12024
    14
*}
wenzelm@12024
    15
wenzelm@12024
    16
subsection {* Configuration of the code generator *}
berghofe@11533
    17
berghofe@11533
    18
types_code
berghofe@11533
    19
  "bool"  ("bool")
berghofe@12439
    20
  "*"     ("(_ */ _)")
berghofe@12439
    21
  "list"  ("_ list")
berghofe@11533
    22
berghofe@11533
    23
consts_code
berghofe@11533
    24
  "True"    ("true")
berghofe@11533
    25
  "False"   ("false")
berghofe@11533
    26
  "Not"     ("not")
berghofe@11533
    27
  "op |"    ("(_ orelse/ _)")
berghofe@11533
    28
  "op &"    ("(_ andalso/ _)")
berghofe@11533
    29
  "If"      ("(if _/ then _/ else _)")
berghofe@11533
    30
berghofe@11533
    31
  "Pair"    ("(_,/ _)")
berghofe@11533
    32
  "fst"     ("fst")
berghofe@11533
    33
  "snd"     ("snd")
berghofe@11533
    34
berghofe@11533
    35
  "Nil"     ("[]")
berghofe@11533
    36
  "Cons"    ("(_ ::/ _)")
berghofe@12439
    37
berghofe@13093
    38
  "wfrec"   ("wf'_rec?")
berghofe@13093
    39
berghofe@14102
    40
quickcheck_params [default_type = int]
berghofe@14102
    41
berghofe@13755
    42
ML {*
berghofe@13755
    43
fun wf_rec f x = f (wf_rec f) x;
berghofe@13755
    44
berghofe@14102
    45
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
berghofe@13755
    46
val term_of_list = HOLogic.mk_list;
berghofe@13755
    47
val term_of_int = HOLogic.mk_int;
berghofe@14049
    48
fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
berghofe@14102
    49
fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
berghofe@14102
    50
berghofe@14102
    51
val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
berghofe@14102
    52
  (fn thy => fn gr => fn dep => fn b => fn t =>
berghofe@14102
    53
    (case strip_comb t of
berghofe@14102
    54
       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => None
berghofe@14102
    55
     | (Const ("op =", _), [t, u]) =>
berghofe@14102
    56
          let
berghofe@14102
    57
            val (gr', pt) = Codegen.invoke_codegen thy dep false (gr, t);
berghofe@14102
    58
            val (gr'', pu) = Codegen.invoke_codegen thy dep false (gr', u)
berghofe@14102
    59
          in
berghofe@14102
    60
            Some (gr'', Codegen.parens
berghofe@14102
    61
              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
berghofe@14102
    62
          end
berghofe@14102
    63
     | (t as Const ("op =", _), ts) => Some (Codegen.invoke_codegen
berghofe@14102
    64
         thy dep b (gr, Codegen.eta_expand t ts 2))
berghofe@14102
    65
     | _ => None))];
berghofe@14102
    66
berghofe@14102
    67
fun gen_bool i = one_of [false, true];
berghofe@14102
    68
berghofe@14102
    69
fun gen_list' aG i j = frequency
berghofe@14102
    70
  [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
berghofe@14102
    71
and gen_list aG i = gen_list' aG i i;
berghofe@14102
    72
berghofe@14102
    73
fun gen_int i = one_of [~1, 1] * random_range 0 i;
berghofe@14102
    74
berghofe@14102
    75
fun gen_id_42 aG bG i = (aG i, bG i);
berghofe@14102
    76
berghofe@14102
    77
fun gen_fun_type _ G i =
berghofe@14102
    78
  let
berghofe@14102
    79
    val f = ref (fn x => raise ERROR);
berghofe@14102
    80
    val _ = (f := (fn x =>
berghofe@14102
    81
      let
berghofe@14102
    82
        val y = G i;
berghofe@14102
    83
        val f' = !f
berghofe@14102
    84
      in (f := (fn x' => if x = x' then y else f' x'); y) end))
berghofe@14102
    85
  in (fn x => !f x) end;
berghofe@13755
    86
*}
berghofe@13093
    87
berghofe@14102
    88
setup eq_codegen_setup
berghofe@14102
    89
berghofe@12554
    90
lemma [code]: "((n::nat) < 0) = False" by simp
berghofe@14192
    91
lemma [code]: "(0 < Suc n) = True" by simp
berghofe@14192
    92
lemmas [code] = Suc_less_eq imp_conv_disj
berghofe@12554
    93
webertj@14350
    94
subsection {* Configuration of the 'refute' command *}
webertj@14350
    95
webertj@14350
    96
text {*
webertj@14350
    97
  The following are reasonable default parameters (for use with
webertj@14350
    98
  ZChaff 2003.12.04).  For an explanation of these parameters,
webertj@14350
    99
  see 'HOL/Refute.thy'.
webertj@14350
   100
webertj@14350
   101
  \emph{Note}: If you want to use a different SAT solver (or
webertj@14350
   102
  install ZChaff to a different location), you will need to
webertj@14350
   103
  override at least the values for 'command' and (probably)
webertj@14350
   104
  'success' in your own theory file.
webertj@14350
   105
*}
webertj@14350
   106
webertj@14350
   107
refute_params [minsize=1,
webertj@14350
   108
               maxsize=8,
webertj@14350
   109
               maxvars=200,
webertj@14350
   110
               satfile="refute.cnf",
webertj@14350
   111
               satformat="defcnf",
webertj@14350
   112
               resultfile="refute.out",
webertj@14350
   113
               success="Verify Solution successful. Instance satisfiable",
webertj@14350
   114
               command="$HOME/bin/zchaff refute.cnf 60 > refute.out"]
webertj@14350
   115
wenzelm@9650
   116
end