src/HOL/Quickcheck_Exhaustive.thy
changeset 46193 55a4769d0abe
parent 45925 cd4243c025bb
child 46305 8ea02e499d53
equal deleted inserted replaced
46192:93eaaacc1955 46193:55a4769d0abe
   132       (t1 ())) (t2 ()))) d) d"
   132       (t1 ())) (t2 ()))) d) d"
   133 
   133 
   134 instance ..
   134 instance ..
   135 
   135 
   136 end
   136 end
       
   137 
       
   138 instantiation set :: (exhaustive) exhaustive
       
   139 begin
       
   140 
       
   141 fun exhaustive_set
       
   142 where
       
   143   "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse Quickcheck_Exhaustive.exhaustive (%x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1)))"
       
   144 
       
   145 instance ..
       
   146 
       
   147 end
       
   148 
       
   149 definition (in term_syntax) "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
       
   150 definition (in term_syntax) "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
       
   151 
       
   152 instantiation set :: (full_exhaustive) full_exhaustive
       
   153 begin
       
   154 
       
   155 fun full_exhaustive_set 
       
   156 where
       
   157   "full_exhaustive_set f i = (if i = 0 then None else (f valterm_emptyset orelse full_exhaustive_set (%A. f A orelse Quickcheck_Exhaustive.full_exhaustive (%x. if fst x \<in> fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1)))"
       
   158 
       
   159 instance ..
       
   160 
       
   161 end
       
   162 
       
   163 hide_const valterm_emptyset valtermify_insert
   137 
   164 
   138 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
   165 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
   139 begin
   166 begin
   140 
   167 
   141 fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
   168 fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"