src/HOL/ex/Quickcheck.thy
changeset 28335 25326092cf9a
parent 28315 d3cf88fe77bc
child 28360 cf3542e34726
equal deleted inserted replaced
28334:7c693bb76366 28335:25326092cf9a
     8 imports Random Code_Eval
     8 imports Random Code_Eval
     9 begin
     9 begin
    10 
    10 
    11 subsection {* The @{text random} class *}
    11 subsection {* The @{text random} class *}
    12 
    12 
    13 class random = rtype +
    13 class random = typerep +
    14   fixes random :: "index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
    14   fixes random :: "index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
    15 
    15 
    16 text {* Type @{typ "'a itself"} *}
    16 text {* Type @{typ "'a itself"} *}
    17 
    17 
    18 instantiation itself :: ("{type, rtype}") random
    18 instantiation itself :: ("{type, typerep}") random
    19 begin
    19 begin
    20 
    20 
    21 definition
    21 definition
    22   "random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') RTYPE('a))"
    22   "random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))"
    23 
    23 
    24 instance ..
    24 instance ..
    25 
    25 
    26 end
    26 end
    27 
    27 
    70       val c_ty = tys ---> this_ty;
    70       val c_ty = tys ---> this_ty;
    71       val c = Const (c, tys ---> this_ty);
    71       val c = Const (c, tys ---> this_ty);
    72       val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0);
    72       val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0);
    73       val c_indices = map (curry ( op + ) 1) t_indices;
    73       val c_indices = map (curry ( op + ) 1) t_indices;
    74       val c_t = list_comb (c, map Bound c_indices);
    74       val c_t = list_comb (c, map Bound c_indices);
    75       val t_t = Abs ("", @{typ unit}, Eval.mk_term Free RType.rtype
    75       val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep
    76         (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
    76         (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
    77         |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
    77         |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
    78       val return = StateMonad.return (term_ty this_ty) @{typ seed}
    78       val return = StateMonad.return (term_ty this_ty) @{typ seed}
    79         (HOLogic.mk_prod (c_t, t_t));
    79         (HOLogic.mk_prod (c_t, t_t));
    80       val t = fold_rev (fn ((ty, _), random) =>
    80       val t = fold_rev (fn ((ty, _), random) =>
   171 
   171 
   172 definition
   172 definition
   173   "random n = (do
   173   "random n = (do
   174      (b, _) \<leftarrow> random n;
   174      (b, _) \<leftarrow> random n;
   175      (m, t) \<leftarrow> random n;
   175      (m, t) \<leftarrow> random n;
   176      return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))
   176      return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))
   177        else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') RTYPE(int \<Rightarrow> int))
   177        else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \<Rightarrow> int))
   178          (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))))
   178          (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))))
   179    done)"
   179    done)"
   180 
   180 
   181 instance ..
   181 instance ..
   182 
   182 
   183 end
   183 end
   217 
   217 
   218 end
   218 end
   219 *}
   219 *}
   220 
   220 
   221 axiomatization
   221 axiomatization
   222   random_fun_aux :: "rtype \<Rightarrow> rtype \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   222   random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   223     \<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed)
   223     \<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed)
   224     \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed"
   224     \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed"
   225 
   225 
   226 code_const random_fun_aux (SML "Random'_Engine.random'_fun")
   226 code_const random_fun_aux (SML "Random'_Engine.random'_fun")
   227 
   227 
   228 instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
   228 instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
   229 begin
   229 begin
   230 
   230 
   231 definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where
   231 definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where
   232   "random n = random_fun_aux RTYPE('a) RTYPE('b) (op =) Code_Eval.term_of (random n) split_seed"
   232   "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed"
   233 
   233 
   234 instance ..
   234 instance ..
   235 
   235 
   236 end
   236 end
   237 
   237