src/HOL/Smallcheck.thy
changeset 41719 91c2510e19c5
parent 41231 2e901158675e
child 41722 9575694d2da5
equal deleted inserted replaced
41711:3422ae5aff3a 41719:91c2510e19c5
   111 instantiation prod :: (full_small, full_small) full_small
   111 instantiation prod :: (full_small, full_small) full_small
   112 begin
   112 begin
   113 
   113 
   114 definition
   114 definition
   115   "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
   115   "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
   116     %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
   116     %u. let T1 = (Typerep.typerep (TYPE('a)));
       
   117             T2 = (Typerep.typerep (TYPE('b)))
       
   118     in Code_Evaluation.App (Code_Evaluation.App (
       
   119       Code_Evaluation.Const (STR ''Product_Type.Pair'') 
       
   120       (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
       
   121       (t1 ())) (t2 ()))) d) d"
   117 
   122 
   118 instance ..
   123 instance ..
   119 
   124 
   120 end
   125 end
   121 
   126 
   227 
   232 
   228 instantiation prod :: (check_all, check_all) check_all
   233 instantiation prod :: (check_all, check_all) check_all
   229 begin
   234 begin
   230 
   235 
   231 definition
   236 definition
   232   "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))))"
   237   "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y),
       
   238     %u. let T1 = (Typerep.typerep (TYPE('a)));
       
   239             T2 = (Typerep.typerep (TYPE('b)))
       
   240     in Code_Evaluation.App (Code_Evaluation.App (
       
   241       Code_Evaluation.Const (STR ''Product_Type.Pair'') 
       
   242       (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
       
   243       (t1 ())) (t2 ()))))"
   233 
   244 
   234 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
   245 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
   235 where
   246 where
   236   "enum_term_of_prod = (%_ _. map (%(x, y). Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) x) y) (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
   247   "enum_term_of_prod = (%_ _. map (%(x, y).
       
   248        let T1 = (Typerep.typerep (TYPE('a)));
       
   249            T2 = (Typerep.typerep (TYPE('b)))
       
   250        in Code_Evaluation.App (Code_Evaluation.App (
       
   251          Code_Evaluation.Const (STR ''Product_Type.Pair'') 
       
   252            (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y)
       
   253      (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))  "
   237 
   254 
   238 instance ..
   255 instance ..
   239 
   256 
   240 end
   257 end
   241 
   258