src/HOL/Quickcheck_Exhaustive.thy
changeset 62597 b3f2b8c906a6
parent 62364 9209770bdcdf
child 62979 1e527c40ae40
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 17:20:14 2016 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sat Mar 12 22:04:52 2016 +0100
     1.3 @@ -379,42 +379,13 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instantiation nibble :: check_all
     1.8 +(* FIXME instantiation char :: check_all
     1.9  begin
    1.10  
    1.11  definition
    1.12 -  "check_all f =
    1.13 -    f (Code_Evaluation.valtermify Nibble0) orelse
    1.14 -    f (Code_Evaluation.valtermify Nibble1) orelse
    1.15 -    f (Code_Evaluation.valtermify Nibble2) orelse
    1.16 -    f (Code_Evaluation.valtermify Nibble3) orelse
    1.17 -    f (Code_Evaluation.valtermify Nibble4) orelse
    1.18 -    f (Code_Evaluation.valtermify Nibble5) orelse
    1.19 -    f (Code_Evaluation.valtermify Nibble6) orelse
    1.20 -    f (Code_Evaluation.valtermify Nibble7) orelse
    1.21 -    f (Code_Evaluation.valtermify Nibble8) orelse
    1.22 -    f (Code_Evaluation.valtermify Nibble9) orelse
    1.23 -    f (Code_Evaluation.valtermify NibbleA) orelse
    1.24 -    f (Code_Evaluation.valtermify NibbleB) orelse
    1.25 -    f (Code_Evaluation.valtermify NibbleC) orelse
    1.26 -    f (Code_Evaluation.valtermify NibbleD) orelse
    1.27 -    f (Code_Evaluation.valtermify NibbleE) orelse
    1.28 -    f (Code_Evaluation.valtermify NibbleF)"
    1.29 -
    1.30 -definition enum_term_of_nibble :: "nibble itself => unit => term list"
    1.31 -where
    1.32 -  "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
    1.33 -
    1.34 -instance ..
    1.35 -
    1.36 -end
    1.37 -
    1.38 -
    1.39 -instantiation char :: check_all
    1.40 -begin
    1.41 -
    1.42 -definition
    1.43 -  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f (Char x y, %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
    1.44 +  "check_all f = check_all (%(x, t1). check_all (%(y, t2).
    1.45 +     f (Char x y, %_. Code_Evaluation.App
    1.46 +       (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
    1.47  
    1.48  definition enum_term_of_char :: "char itself => unit => term list"
    1.49  where
    1.50 @@ -422,8 +393,7 @@
    1.51  
    1.52  instance ..
    1.53  
    1.54 -end
    1.55 -
    1.56 +end *)
    1.57  
    1.58  instantiation option :: (check_all) check_all
    1.59  begin
    1.60 @@ -624,13 +594,7 @@
    1.61  
    1.62  ML_file "Tools/Quickcheck/abstract_generators.ML"
    1.63  
    1.64 -lemma check_all_char [code]:
    1.65 -  "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
    1.66 -     f (char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y), \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
    1.67 -       (Code_Evaluation.term_of (\<lambda>x y. char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y))) (t1 ())) (t2 ()))))"
    1.68 -  by (simp add: check_all_char_def)
    1.69 -
    1.70 -instantiation char :: full_exhaustive
    1.71 +(* FIXME instantiation char :: full_exhaustive
    1.72  begin
    1.73  
    1.74  definition full_exhaustive_char
    1.75 @@ -648,7 +612,7 @@
    1.76  
    1.77  instance ..
    1.78  
    1.79 -end
    1.80 +end *)
    1.81  
    1.82  hide_fact (open) orelse_def
    1.83  no_notation orelse (infixr "orelse" 55)