Theory HOL.Quickcheck_Exhaustive

(*  Title:      HOL/Quickcheck_Exhaustive.thy
    Author:     Lukas Bulwahn, TU Muenchen
*)

section ‹A simple counterexample generator performing exhaustive testing›

theory Quickcheck_Exhaustive
imports Quickcheck_Random
keywords "quickcheck_generator" :: thy_decl
begin

subsection ‹Basic operations for exhaustive generators›

definition orelse :: "'a option ⇒ 'a option ⇒ 'a option"  (infixr "orelse" 55)
  where [code_unfold]: "x orelse y = (case x of Some x' ⇒ Some x' | None ⇒ y)"


subsection ‹Exhaustive generator type classes›

class exhaustive = term_of +
  fixes exhaustive :: "('a ⇒ (bool × term list) option) ⇒ natural ⇒ (bool × term list) option"

class full_exhaustive = term_of +
  fixes full_exhaustive ::
    "('a × (unit ⇒ term) ⇒ (bool × term list) option) ⇒ natural ⇒ (bool × term list) option"

instantiation natural :: full_exhaustive
begin

function full_exhaustive_natural' ::
    "(natural × (unit ⇒ term) ⇒ (bool × term list) option) ⇒
      natural ⇒ natural ⇒ (bool × term list) option"
  where "full_exhaustive_natural' f d i =
    (if d < i then None
     else (f (i, λ_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))"
by pat_completeness auto

termination
  by (relation "measure (λ(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def)

definition "full_exhaustive f d = full_exhaustive_natural' f d 0"

instance ..

end

instantiation natural :: exhaustive
begin

function exhaustive_natural' ::
    "(natural ⇒ (bool × term list) option) ⇒ natural ⇒ natural ⇒ (bool × term list) option"
  where "exhaustive_natural' f d i =
    (if d < i then None
     else (f i orelse exhaustive_natural' f d (i + 1)))"
by pat_completeness auto

termination
  by (relation "measure (λ(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def)

definition "exhaustive f d = exhaustive_natural' f d 0"

instance ..

end

instantiation integer :: exhaustive
begin

function exhaustive_integer' ::
    "(integer ⇒ (bool × term list) option) ⇒ integer ⇒ integer ⇒ (bool × term list) option"
  where "exhaustive_integer' f d i =
    (if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))"
by pat_completeness auto

termination
  by (relation "measure (λ(_, d, i). nat_of_integer (d + 1 - i))")
    (auto simp add: less_integer_def nat_of_integer_def)

definition "exhaustive f d = exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"

instance ..

end

instantiation integer :: full_exhaustive
begin

function full_exhaustive_integer' ::
    "(integer × (unit ⇒ term) ⇒ (bool × term list) option) ⇒
      integer ⇒ integer ⇒ (bool × term list) option"
  where "full_exhaustive_integer' f d i =
    (if d < i then None
     else
      (case f (i, λ_. Code_Evaluation.term_of i) of
        Some t ⇒ Some t
      | None ⇒ full_exhaustive_integer' f d (i + 1)))"
by pat_completeness auto

termination
  by (relation "measure (λ(_, d, i). nat_of_integer (d + 1 - i))")
    (auto simp add: less_integer_def nat_of_integer_def)

definition "full_exhaustive f d =
  full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"

instance ..

end

instantiation nat :: exhaustive
begin

definition "exhaustive f d = exhaustive (λx. f (nat_of_natural x)) d"

instance ..

end

instantiation nat :: full_exhaustive
begin

definition "full_exhaustive f d =
  full_exhaustive (λ(x, xt). f (nat_of_natural x, λ_. Code_Evaluation.term_of (nat_of_natural x))) d"

instance ..

end

instantiation int :: exhaustive
begin

function exhaustive_int' ::
    "(int ⇒ (bool × term list) option) ⇒ int ⇒ int ⇒ (bool × term list) option"
  where "exhaustive_int' f d i =
    (if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))"
by pat_completeness auto

termination
  by (relation "measure (λ(_, d, i). nat (d + 1 - i))") auto

definition "exhaustive f d =
  exhaustive_int' f (int_of_integer (integer_of_natural d))
    (- (int_of_integer (integer_of_natural d)))"

instance ..

end

instantiation int :: full_exhaustive
begin

function full_exhaustive_int' ::
    "(int × (unit ⇒ term) ⇒ (bool × term list) option) ⇒
      int ⇒ int ⇒ (bool × term list) option"
  where "full_exhaustive_int' f d i =
    (if d < i then None
     else
      (case f (i, λ_. Code_Evaluation.term_of i) of
        Some t ⇒ Some t
       | None ⇒ full_exhaustive_int' f d (i + 1)))"
by pat_completeness auto

termination
  by (relation "measure (λ(_, d, i). nat (d + 1 - i))") auto

definition "full_exhaustive f d =
  full_exhaustive_int' f (int_of_integer (integer_of_natural d))
    (- (int_of_integer (integer_of_natural d)))"

instance ..

end

instantiation prod :: (exhaustive, exhaustive) exhaustive
begin

definition "exhaustive f d = exhaustive (λx. exhaustive (λy. f ((x, y))) d) d"

instance ..

end

context
  includes term_syntax
begin

definition
  [code_unfold]: "valtermify_pair x y =
    Code_Evaluation.valtermify (Pair :: 'a::typerep ⇒ 'b::typerep ⇒ 'a × 'b) {⋅} x {⋅} y"

end

instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
begin

definition "full_exhaustive f d =
  full_exhaustive (λx. full_exhaustive (λy. f (valtermify_pair x y)) d) d"

instance ..

end

instantiation set :: (exhaustive) exhaustive
begin

fun exhaustive_set
where
  "exhaustive_set f i =
    (if i = 0 then None
     else
      f {} orelse
      exhaustive_set
        (λA. f A orelse exhaustive (λx. if x ∈ A then None else f (insert x A)) (i - 1)) (i - 1))"

instance ..

end

instantiation set :: (full_exhaustive) full_exhaustive
begin

fun full_exhaustive_set
where
  "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 ∈ fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1))"

instance ..

end

instantiation "fun" :: ("{equal,exhaustive}", exhaustive) exhaustive
begin

fun exhaustive_fun' ::
  "(('a ⇒ 'b) ⇒ (bool × term list) option) ⇒ natural ⇒ natural ⇒ (bool × term list) option"
where
  "exhaustive_fun' f i d =
    (exhaustive (λb. f (λ_. b)) d) orelse
      (if i > 1 then
        exhaustive_fun'
          (λg. exhaustive (λa. exhaustive (λb. f (g(a := b))) d) d) (i - 1) d else None)"

definition exhaustive_fun ::
  "(('a ⇒ 'b) ⇒ (bool × term list) option) ⇒ natural ⇒ (bool × term list) option"
  where "exhaustive_fun f d = exhaustive_fun' f d d"

instance ..

end

definition [code_unfold]:
  "valtermify_absdummy =
    (λ(v, t).
      (λ_::'a. v,
        λu::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"

context
  includes term_syntax
begin

definition
  [code_unfold]: "valtermify_fun_upd g a b =
    Code_Evaluation.valtermify
      (fun_upd :: ('a::typerep ⇒ 'b::typerep) ⇒ 'a ⇒ 'b ⇒ 'a ⇒ 'b) {⋅} g {⋅} a {⋅} b"

end

instantiation "fun" :: ("{equal,full_exhaustive}", full_exhaustive) full_exhaustive
begin

fun full_exhaustive_fun' ::
  "(('a ⇒ 'b) × (unit ⇒ term) ⇒ (bool × term list) option) ⇒
    natural ⇒ natural ⇒ (bool × term list) option"
where
  "full_exhaustive_fun' f i d =
    full_exhaustive (λv. f (valtermify_absdummy v)) d orelse
    (if i > 1 then
      full_exhaustive_fun'
        (λg. full_exhaustive
          (λa. full_exhaustive (λb. f (valtermify_fun_upd g a b)) d) d) (i - 1) d
     else None)"

definition full_exhaustive_fun ::
  "(('a ⇒ 'b) × (unit ⇒ term) ⇒ (bool × term list) option) ⇒
    natural ⇒ (bool × term list) option"
  where "full_exhaustive_fun f d = full_exhaustive_fun' f d d"

instance ..

end

subsubsection ‹A smarter enumeration scheme for functions over finite datatypes›

class check_all = enum + term_of +
  fixes check_all :: "('a × (unit ⇒ term) ⇒ (bool × term list) option) ⇒ (bool * term list) option"
  fixes enum_term_of :: "'a itself ⇒ unit ⇒ term list"

fun check_all_n_lists :: "('a::check_all list × (unit ⇒ term list) ⇒
  (bool × term list) option) ⇒ natural ⇒ (bool * term list) option"
where
  "check_all_n_lists f n =
    (if n = 0 then f ([], (λ_. []))
     else check_all (λ(x, xt).
      check_all_n_lists (λ(xs, xst). f ((x # xs), (λ_. (xt () # xst ())))) (n - 1)))"

context
  includes term_syntax
begin

definition
  [code_unfold]: "termify_fun_upd g a b =
    (Code_Evaluation.termify
      (fun_upd :: ('a::typerep ⇒ 'b::typerep) ⇒ 'a ⇒ 'b ⇒ 'a ⇒ 'b) <⋅> g <⋅> a <⋅> b)"

end

definition mk_map_term ::
  "(unit ⇒ typerep) ⇒ (unit ⇒ typerep) ⇒
    (unit ⇒ term list) ⇒ (unit ⇒ term list) ⇒ unit ⇒ term"
  where "mk_map_term T1 T2 domm rng =
    (λ_.
      let
        T1 = T1 ();
        T2 = T2 ();
        update_term =
          (λg (a, b).
            Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
             (Code_Evaluation.Const (STR ''Fun.fun_upd'')
               (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
                  Typerep.Typerep (STR ''fun'') [T1,
                    Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
                    g) a) b)
      in
        List.foldl update_term
          (Code_Evaluation.Abs (STR ''x'') T1
            (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"

instantiation "fun" :: ("{equal,check_all}", check_all) check_all
begin

definition
  "check_all f =
    (let
      mk_term =
        mk_map_term
          (λ_. Typerep.typerep (TYPE('a)))
          (λ_. Typerep.typerep (TYPE('b)))
          (enum_term_of (TYPE('a)));
      enum = (Enum.enum :: 'a list)
    in
      check_all_n_lists
        (λ(ys, yst). f (the ∘ map_of (zip enum ys), mk_term yst))
        (natural_of_nat (length enum)))"

definition enum_term_of_fun :: "('a ⇒ 'b) itself ⇒ unit ⇒ term list"
  where "enum_term_of_fun =
    (λ_ _.
      let
        enum_term_of_a = enum_term_of (TYPE('a));
        mk_term =
          mk_map_term
            (λ_. Typerep.typerep (TYPE('a)))
            (λ_. Typerep.typerep (TYPE('b)))
            enum_term_of_a
      in
        map (λys. mk_term (λ_. ys) ())
          (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"

instance ..

end

context
  includes term_syntax
begin

fun check_all_subsets ::
  "(('a::typerep) set × (unit ⇒ term) ⇒ (bool × term list) option) ⇒
    ('a × (unit ⇒ term)) list ⇒ (bool × term list) option"
where
  "check_all_subsets f [] = f valterm_emptyset"
| "check_all_subsets f (x # xs) =
    check_all_subsets (λs. case f s of Some ts ⇒ Some ts | None ⇒ f (valtermify_insert x s)) xs"

definition
  [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a::typerep) set)"

definition
  [code_unfold]: "termify_insert x s =
    Code_Evaluation.termify (insert :: ('a::typerep) ⇒ 'a set ⇒ 'a set)  <⋅> x <⋅> s"

definition setify :: "('a::typerep) itself ⇒ term list ⇒ term"
where
  "setify T ts = foldr (termify_insert T) ts (term_emptyset T)"

end

instantiation set :: (check_all) check_all
begin

definition
  "check_all_set f =
     check_all_subsets f
      (zip (Enum.enum :: 'a list)
        (map (λa. λu :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"

definition enum_term_of_set :: "'a set itself ⇒ unit ⇒ term list"
  where "enum_term_of_set _ _ =
    map (setify (TYPE('a))) (subseqs (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"

instance ..

end

instantiation unit :: check_all
begin

definition "check_all f = f (Code_Evaluation.valtermify ())"

definition enum_term_of_unit :: "unit itself ⇒ unit ⇒ term list"
  where "enum_term_of_unit = (λ_ _. [Code_Evaluation.term_of ()])"

instance ..

end


instantiation bool :: check_all
begin

definition
  "check_all f =
    (case f (Code_Evaluation.valtermify False) of
      Some x' ⇒ Some x'
    | None ⇒ f (Code_Evaluation.valtermify True))"

definition enum_term_of_bool :: "bool itself ⇒ unit ⇒ term list"
  where "enum_term_of_bool = (λ_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"

instance ..

end

context
  includes term_syntax
begin

definition [code_unfold]:
  "termify_pair x y =
    Code_Evaluation.termify (Pair :: 'a::typerep ⇒ 'b :: typerep ⇒ 'a * 'b) <⋅> x <⋅> y"

end

instantiation prod :: (check_all, check_all) check_all
begin

definition "check_all f = check_all (λx. check_all (λy. f (valtermify_pair x y)))"

definition enum_term_of_prod :: "('a * 'b) itself ⇒ unit ⇒ term list"
  where "enum_term_of_prod =
    (λ_ _.
      map (λ(x, y). termify_pair TYPE('a) TYPE('b) x y)
        (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"

instance ..

end

context
  includes term_syntax
begin

definition
  [code_unfold]: "valtermify_Inl x =
    Code_Evaluation.valtermify (Inl :: 'a::typerep ⇒ 'a + 'b :: typerep) {⋅} x"

definition
  [code_unfold]: "valtermify_Inr x =
    Code_Evaluation.valtermify (Inr :: 'b::typerep ⇒ 'a::typerep + 'b) {⋅} x"

end

instantiation sum :: (check_all, check_all) check_all
begin

definition
  "check_all f = check_all (λa. f (valtermify_Inl a)) orelse check_all (λb. f (valtermify_Inr b))"

definition enum_term_of_sum :: "('a + 'b) itself ⇒ unit ⇒ term list"
  where "enum_term_of_sum =
    (λ_ _.
      let
        T1 = Typerep.typerep (TYPE('a));
        T2 = Typerep.typerep (TYPE('b))
      in
        map
          (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'')
            (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
          (enum_term_of (TYPE('a)) ()) @
        map
          (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'')
            (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
          (enum_term_of (TYPE('b)) ()))"

instance ..

end

instantiation char :: check_all
begin

primrec check_all_char' ::
  "(char × (unit ⇒ term) ⇒ (bool × term list) option) ⇒ char list ⇒ (bool × term list) option"
  where "check_all_char' f [] = None"
  | "check_all_char' f (c # cs) = f (c, λ_. Code_Evaluation.term_of c)
      orelse check_all_char' f cs"

definition check_all_char ::
  "(char × (unit ⇒ term) ⇒ (bool × term list) option) ⇒ (bool × term list) option"
  where "check_all f = check_all_char' f Enum.enum"

definition enum_term_of_char :: "char itself ⇒ unit ⇒ term list"
where
  "enum_term_of_char = (λ_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"

instance ..

end

instantiation option :: (check_all) check_all
begin

definition
  "check_all f =
    f (Code_Evaluation.valtermify (None :: 'a option)) orelse
    check_all
      (λ(x, t).
        f
          (Some x,
            λ_. Code_Evaluation.App
              (Code_Evaluation.Const (STR ''Option.option.Some'')
                (Typerep.Typerep (STR ''fun'')
                [Typerep.typerep TYPE('a),
                 Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"

definition enum_term_of_option :: "'a option itself ⇒ unit ⇒ term list"
  where "enum_term_of_option =
    (λ _ _.
      Code_Evaluation.term_of (None :: 'a option) #
      (map
        (Code_Evaluation.App
          (Code_Evaluation.Const (STR ''Option.option.Some'')
            (Typerep.Typerep (STR ''fun'')
              [Typerep.typerep TYPE('a),
               Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])))
        (enum_term_of (TYPE('a)) ())))"

instance ..

end


instantiation Enum.finite_1 :: check_all
begin

definition "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a⇩1)"

definition enum_term_of_finite_1 :: "Enum.finite_1 itself ⇒ unit ⇒ term list"
  where "enum_term_of_finite_1 = (λ_ _. [Code_Evaluation.term_of Enum.finite_1.a⇩1])"

instance ..

end

instantiation Enum.finite_2 :: check_all
begin

definition
  "check_all f =
    (f (Code_Evaluation.valtermify Enum.finite_2.a⇩1) orelse
     f (Code_Evaluation.valtermify Enum.finite_2.a⇩2))"

definition enum_term_of_finite_2 :: "Enum.finite_2 itself ⇒ unit ⇒ term list"
  where "enum_term_of_finite_2 =
    (λ_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"

instance ..

end

instantiation Enum.finite_3 :: check_all
begin

definition
  "check_all f =
    (f (Code_Evaluation.valtermify Enum.finite_3.a⇩1) orelse
     f (Code_Evaluation.valtermify Enum.finite_3.a⇩2) orelse
     f (Code_Evaluation.valtermify Enum.finite_3.a⇩3))"

definition enum_term_of_finite_3 :: "Enum.finite_3 itself ⇒ unit ⇒ term list"
  where "enum_term_of_finite_3 =
    (λ_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"

instance ..

end

instantiation Enum.finite_4 :: check_all
begin

definition
  "check_all f =
    f (Code_Evaluation.valtermify Enum.finite_4.a⇩1) orelse
    f (Code_Evaluation.valtermify Enum.finite_4.a⇩2) orelse
    f (Code_Evaluation.valtermify Enum.finite_4.a⇩3) orelse
    f (Code_Evaluation.valtermify Enum.finite_4.a⇩4)"

definition enum_term_of_finite_4 :: "Enum.finite_4 itself ⇒ unit ⇒ term list"
  where "enum_term_of_finite_4 =
    (λ_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"

instance ..

end

subsection ‹Bounded universal quantifiers›

class bounded_forall =
  fixes bounded_forall :: "('a ⇒ bool) ⇒ natural ⇒ bool"


subsection ‹Fast exhaustive combinators›

class fast_exhaustive = term_of +
  fixes fast_exhaustive :: "('a ⇒ unit) ⇒ natural ⇒ unit"

axiomatization throw_Counterexample :: "term list ⇒ unit"
axiomatization catch_Counterexample :: "unit ⇒ term list option"

code_printing
  constant throw_Counterexample ⇀
    (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)"
| constant catch_Counterexample ⇀
    (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts ⇒ SOME ts)"


subsection ‹Continuation passing style functions as plus monad›

type_synonym 'a cps = "('a ⇒ term list option) ⇒ term list option"

definition cps_empty :: "'a cps"
  where "cps_empty = (λcont. None)"

definition cps_single :: "'a ⇒ 'a cps"
  where "cps_single v = (λcont. cont v)"

definition cps_bind :: "'a cps ⇒ ('a ⇒ 'b cps) ⇒ 'b cps"
  where "cps_bind m f = (λcont. m (λa. (f a) cont))"

definition cps_plus :: "'a cps ⇒ 'a cps ⇒ 'a cps"
  where "cps_plus a b = (λc. case a c of None ⇒ b c | Some x ⇒ Some x)"

definition cps_if :: "bool ⇒ unit cps"
  where "cps_if b = (if b then cps_single () else cps_empty)"

definition cps_not :: "unit cps ⇒ unit cps"
  where "cps_not n = (λc. case n (λu. Some []) of None ⇒ c () | Some _ ⇒ None)"

type_synonym 'a pos_bound_cps =
  "('a ⇒ (bool * term list) option) ⇒ natural ⇒ (bool * term list) option"

definition pos_bound_cps_empty :: "'a pos_bound_cps"
  where "pos_bound_cps_empty = (λcont i. None)"

definition pos_bound_cps_single :: "'a ⇒ 'a pos_bound_cps"
  where "pos_bound_cps_single v = (λcont i. cont v)"

definition pos_bound_cps_bind :: "'a pos_bound_cps ⇒ ('a ⇒ 'b pos_bound_cps) ⇒ 'b pos_bound_cps"
  where "pos_bound_cps_bind m f = (λcont i. if i = 0 then None else (m (λa. (f a) cont i) (i - 1)))"

definition pos_bound_cps_plus :: "'a pos_bound_cps ⇒ 'a pos_bound_cps ⇒ 'a pos_bound_cps"
  where "pos_bound_cps_plus a b = (λc i. case a c i of None ⇒ b c i | Some x ⇒ Some x)"

definition pos_bound_cps_if :: "bool ⇒ unit pos_bound_cps"
  where "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"

datatype (plugins only: code extraction) (dead 'a) unknown =
  Unknown | Known 'a

datatype (plugins only: code extraction) (dead 'a) three_valued =
  Unknown_value | Value 'a | No_value

type_synonym 'a neg_bound_cps =
  "('a unknown ⇒ term list three_valued) ⇒ natural ⇒ term list three_valued"

definition neg_bound_cps_empty :: "'a neg_bound_cps"
  where "neg_bound_cps_empty = (λcont i. No_value)"

definition neg_bound_cps_single :: "'a ⇒ 'a neg_bound_cps"
  where "neg_bound_cps_single v = (λcont i. cont (Known v))"

definition neg_bound_cps_bind :: "'a neg_bound_cps ⇒ ('a ⇒ 'b neg_bound_cps) ⇒ 'b neg_bound_cps"
  where "neg_bound_cps_bind m f =
    (λcont i.
      if i = 0 then cont Unknown
      else m (λa. case a of Unknown ⇒ cont Unknown | Known a' ⇒ f a' cont i) (i - 1))"

definition neg_bound_cps_plus :: "'a neg_bound_cps ⇒ 'a neg_bound_cps ⇒ 'a neg_bound_cps"
  where "neg_bound_cps_plus a b =
    (λc i.
      case a c i of
        No_value ⇒ b c i
      | Value x ⇒ Value x
      | Unknown_value ⇒
          (case b c i of
            No_value ⇒ Unknown_value
          | Value x ⇒ Value x
          | Unknown_value ⇒ Unknown_value))"

definition neg_bound_cps_if :: "bool ⇒ unit neg_bound_cps"
  where "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"

definition neg_bound_cps_not :: "unit pos_bound_cps ⇒ unit neg_bound_cps"
  where "neg_bound_cps_not n =
    (λc i. case n (λu. Some (True, [])) i of None ⇒ c (Known ()) | Some _ ⇒ No_value)"

definition pos_bound_cps_not :: "unit neg_bound_cps ⇒ unit pos_bound_cps"
  where "pos_bound_cps_not n =
    (λc i. case n (λu. Value []) i of No_value ⇒ c () | Value _ ⇒ None | Unknown_value ⇒ None)"


subsection ‹Defining generators for any first-order data type›

axiomatization unknown :: 'a

notation (output) unknown  ("?")

ML_file ‹Tools/Quickcheck/exhaustive_generators.ML›

declare [[quickcheck_batch_tester = exhaustive]]


subsection ‹Defining generators for abstract types›

ML_file ‹Tools/Quickcheck/abstract_generators.ML›

hide_fact (open) orelse_def
no_notation orelse  (infixr "orelse" 55)

hide_const valtermify_absdummy valtermify_fun_upd
  valterm_emptyset valtermify_insert
  valtermify_pair valtermify_Inl valtermify_Inr
  termify_fun_upd term_emptyset termify_insert termify_pair setify

hide_const (open)
  exhaustive full_exhaustive
  exhaustive_int' full_exhaustive_int'
  exhaustive_integer' full_exhaustive_integer'
  exhaustive_natural' full_exhaustive_natural'
  throw_Counterexample catch_Counterexample
  check_all enum_term_of
  orelse unknown mk_map_term check_all_n_lists check_all_subsets

hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued

hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
  pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind
  pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
  neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind
  neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
  Unknown Known Unknown_value Value No_value

end