instantiation char :: full_exhaustive by Andreas Lochbihler
authorLars Hupel <lars.hupel@mytum.de>
Tue Nov 14 16:09:59 2017 +0100 (3 months ago)
changeset 67076fc877448602e
parent 67069 f11486d31586
child 67077 8fa951baba0d
instantiation char :: full_exhaustive by Andreas Lochbihler
src/HOL/Quickcheck_Exhaustive.thy
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Mon Nov 13 15:07:03 2017 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Tue Nov 14 16:09:59 2017 +0100
     1.3 @@ -714,25 +714,23 @@
     1.4  
     1.5  ML_file "Tools/Quickcheck/abstract_generators.ML"
     1.6  
     1.7 -(* FIXME instantiation char :: full_exhaustive
     1.8 +instantiation char :: full_exhaustive
     1.9  begin
    1.10  
    1.11  definition full_exhaustive_char
    1.12  where
    1.13 -  "full_exhaustive f i =
    1.14 -     (if 0 < i then full_exhaustive_class.full_exhaustive
    1.15 -       (\<lambda>(a, b). full_exhaustive_class.full_exhaustive
    1.16 -          (\<lambda>(c, d).
    1.17 -            f (char_of_nat (nat_of_nibble a * 16 + nat_of_nibble c),
    1.18 -              \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
    1.19 -                 (Code_Evaluation.Const (STR ''String.char.Char'')
    1.20 -                   (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
    1.21 -                      (b ())) (d ()))) (i - 1)) (i - 1)
    1.22 -    else None)"
    1.23 +  "full_exhaustive_char f i =
    1.24 +     (if 0 < i then
    1.25 +      case f (0, \<lambda>_ :: unit. Code_Evaluation.Const (STR ''Groups.zero_class.zero'') (TYPEREP(char))) of
    1.26 +          Some x \<Rightarrow> Some x
    1.27 +      | None \<Rightarrow> full_exhaustive_class.full_exhaustive
    1.28 +          (\<lambda>(num, t). f (char_of_nat (nat_of_num num), \<lambda>_ :: unit. Code_Evaluation.App (Code_Evaluation.Const (STR ''String.Char'') TYPEREP(num \<Rightarrow> char)) (t ())))
    1.29 +          (min (i - 1) 8) (* generate at most 8 bits *)
    1.30 +      else None)"
    1.31  
    1.32  instance ..
    1.33  
    1.34 -end *)
    1.35 +end
    1.36  
    1.37  hide_fact (open) orelse_def
    1.38  no_notation orelse  (infixr "orelse" 55)