src/HOL/Main.thy
changeset 14102 8af7334af4b3
parent 14049 ef1da11a64b9
child 14192 d6cb80cc1d20
equal deleted inserted replaced
14101:d25c23e46173 14102:8af7334af4b3
    19   "bool"  ("bool")
    19   "bool"  ("bool")
    20   "*"     ("(_ */ _)")
    20   "*"     ("(_ */ _)")
    21   "list"  ("_ list")
    21   "list"  ("_ list")
    22 
    22 
    23 consts_code
    23 consts_code
    24   "op ="    ("(_ =/ _)")
       
    25 
       
    26   "True"    ("true")
    24   "True"    ("true")
    27   "False"   ("false")
    25   "False"   ("false")
    28   "Not"     ("not")
    26   "Not"     ("not")
    29   "op |"    ("(_ orelse/ _)")
    27   "op |"    ("(_ orelse/ _)")
    30   "op &"    ("(_ andalso/ _)")
    28   "op &"    ("(_ andalso/ _)")
    37   "Nil"     ("[]")
    35   "Nil"     ("[]")
    38   "Cons"    ("(_ ::/ _)")
    36   "Cons"    ("(_ ::/ _)")
    39 
    37 
    40   "wfrec"   ("wf'_rec?")
    38   "wfrec"   ("wf'_rec?")
    41 
    39 
       
    40 quickcheck_params [default_type = int]
       
    41 
    42 ML {*
    42 ML {*
    43 fun wf_rec f x = f (wf_rec f) x;
    43 fun wf_rec f x = f (wf_rec f) x;
    44 
    44 
       
    45 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    45 val term_of_list = HOLogic.mk_list;
    46 val term_of_list = HOLogic.mk_list;
    46 val term_of_int = HOLogic.mk_int;
    47 val term_of_int = HOLogic.mk_int;
    47 fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
    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;
    48 *}
    86 *}
    49 
    87 
       
    88 setup eq_codegen_setup
       
    89 
    50 lemma [code]: "((n::nat) < 0) = False" by simp
    90 lemma [code]: "((n::nat) < 0) = False" by simp
    51 declare less_Suc_eq [code]
    91 lemmas [code] = less_Suc_eq imp_conv_disj
    52 
    92 
    53 end
    93 end