src/HOL/Main.thy
changeset 14102 8af7334af4b3
parent 14049 ef1da11a64b9
child 14192 d6cb80cc1d20
     1.1 --- a/src/HOL/Main.thy	Fri Jul 11 14:12:41 2003 +0200
     1.2 +++ b/src/HOL/Main.thy	Fri Jul 11 14:55:17 2003 +0200
     1.3 @@ -21,8 +21,6 @@
     1.4    "list"  ("_ list")
     1.5  
     1.6  consts_code
     1.7 -  "op ="    ("(_ =/ _)")
     1.8 -
     1.9    "True"    ("true")
    1.10    "False"   ("false")
    1.11    "Not"     ("not")
    1.12 @@ -39,15 +37,57 @@
    1.13  
    1.14    "wfrec"   ("wf'_rec?")
    1.15  
    1.16 +quickcheck_params [default_type = int]
    1.17 +
    1.18  ML {*
    1.19  fun wf_rec f x = f (wf_rec f) x;
    1.20  
    1.21 +fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    1.22  val term_of_list = HOLogic.mk_list;
    1.23  val term_of_int = HOLogic.mk_int;
    1.24  fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
    1.25 +fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    1.26 +
    1.27 +val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
    1.28 +  (fn thy => fn gr => fn dep => fn b => fn t =>
    1.29 +    (case strip_comb t of
    1.30 +       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => None
    1.31 +     | (Const ("op =", _), [t, u]) =>
    1.32 +          let
    1.33 +            val (gr', pt) = Codegen.invoke_codegen thy dep false (gr, t);
    1.34 +            val (gr'', pu) = Codegen.invoke_codegen thy dep false (gr', u)
    1.35 +          in
    1.36 +            Some (gr'', Codegen.parens
    1.37 +              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    1.38 +          end
    1.39 +     | (t as Const ("op =", _), ts) => Some (Codegen.invoke_codegen
    1.40 +         thy dep b (gr, Codegen.eta_expand t ts 2))
    1.41 +     | _ => None))];
    1.42 +
    1.43 +fun gen_bool i = one_of [false, true];
    1.44 +
    1.45 +fun gen_list' aG i j = frequency
    1.46 +  [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
    1.47 +and gen_list aG i = gen_list' aG i i;
    1.48 +
    1.49 +fun gen_int i = one_of [~1, 1] * random_range 0 i;
    1.50 +
    1.51 +fun gen_id_42 aG bG i = (aG i, bG i);
    1.52 +
    1.53 +fun gen_fun_type _ G i =
    1.54 +  let
    1.55 +    val f = ref (fn x => raise ERROR);
    1.56 +    val _ = (f := (fn x =>
    1.57 +      let
    1.58 +        val y = G i;
    1.59 +        val f' = !f
    1.60 +      in (f := (fn x' => if x = x' then y else f' x'); y) end))
    1.61 +  in (fn x => !f x) end;
    1.62  *}
    1.63  
    1.64 +setup eq_codegen_setup
    1.65 +
    1.66  lemma [code]: "((n::nat) < 0) = False" by simp
    1.67 -declare less_Suc_eq [code]
    1.68 +lemmas [code] = less_Suc_eq imp_conv_disj
    1.69  
    1.70  end