src/HOL/Quickcheck_Exhaustive.thy
changeset 59484 a130ae7a9398
parent 58889 5b7a9633cfa8
child 60758 d8d85a8172b5
--- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Feb 05 19:44:13 2015 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Feb 05 19:44:14 2015 +0100
@@ -624,6 +624,25 @@
 
 ML_file "Tools/Quickcheck/abstract_generators.ML"
 
+lemma check_all_char [code]:
+  "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
+     f (char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y), \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
+       (Code_Evaluation.term_of (\<lambda>x y. char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y))) (t1 ())) (t2 ()))))"
+  by (simp add: check_all_char_def)
+
+lemma full_exhaustive_char_code [code]:
+  "full_exhaustive_class.full_exhaustive f i =
+     (if 0 < i then full_exhaustive_class.full_exhaustive
+       (\<lambda>(a, b). full_exhaustive_class.full_exhaustive
+          (\<lambda>(c, d).
+            f (char_of_nat (nat_of_nibble a * 16 + nat_of_nibble c),
+              \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
+                 (Code_Evaluation.Const (STR ''String.char.Char'')
+                   (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
+                      (b ())) (d ()))) (i - 1)) (i - 1)
+    else None)"
+  by (simp add: typerep_fun_def typerep_char_def typerep_nibble_def String.char.full_exhaustive_char.simps)
+
 hide_fact (open) orelse_def
 no_notation orelse (infixr "orelse" 55)