deriving bounded_forall instances in quickcheck_exhaustive
authorbulwahn
Tue Apr 05 09:38:23 2011 +0200 (2011-04-05)
changeset 42230594480d25aaa
parent 42229 1491b7209e76
child 42231 bc1891226d00
deriving bounded_forall instances in quickcheck_exhaustive
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Tue Apr 05 08:53:52 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Tue Apr 05 09:38:23 2011 +0200
     1.3 @@ -360,18 +360,6 @@
     1.4  class bounded_forall =
     1.5    fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
     1.6  
     1.7 -
     1.8 -instantiation nat :: bounded_forall
     1.9 -begin
    1.10 -
    1.11 -fun bounded_forall_nat :: "(nat => bool) => code_numeral => bool"
    1.12 -where
    1.13 -  "bounded_forall P d = ((P 0) \<and> (if d > 0 then bounded_forall (%n. P (Suc n)) (d - 1) else True))"
    1.14 -
    1.15 -instance ..
    1.16 -
    1.17 -end
    1.18 -
    1.19  subsection {* Defining combinators for any first-order data type *}
    1.20  
    1.21  definition catch_match :: "term list option => term list option => term list option"
     2.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Apr 05 08:53:52 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Apr 05 09:38:23 2011 +0200
     2.3 @@ -156,7 +156,7 @@
     2.4  
     2.5  fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
     2.6    let
     2.7 -    val _ = Datatype_Aux.message config "Creating exhaustive generators ...";
     2.8 +    val _ = Datatype_Aux.message config "Creating exhaustive generators...";
     2.9      val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames);
    2.10    in
    2.11      thy
    2.12 @@ -170,6 +170,71 @@
    2.13        "Creation of exhaustive generators failed because the datatype contains a function type";
    2.14      thy)
    2.15  
    2.16 +(* constructing bounded_forall instances on datatypes *)
    2.17 +
    2.18 +val bounded_forallN = "bounded_forall";
    2.19 +
    2.20 +fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
    2.21 +
    2.22 +fun mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us) =
    2.23 +  let
    2.24 +    fun mk_call T =
    2.25 +      let
    2.26 +        val bounded_forall =
    2.27 +          Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
    2.28 +            bounded_forallT T)
    2.29 +      in
    2.30 +        (T, (fn t => bounded_forall $ absdummy (T, t) $ size_pred))
    2.31 +      end
    2.32 +    fun mk_aux_call fTs (k, _) (tyco, Ts) =
    2.33 +      let
    2.34 +        val T = Type (tyco, Ts)
    2.35 +        val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
    2.36 +      in
    2.37 +        (T, (fn t => nth bounded_foralls k $ absdummy (T, t) $ size_pred))
    2.38 +      end
    2.39 +    fun mk_consexpr simpleT (c, xs) =
    2.40 +      let
    2.41 +        val (Ts, fns) = split_list xs
    2.42 +        val constr = Const (c, Ts ---> simpleT)
    2.43 +        val bounds = map Bound (((length xs) - 1) downto 0)
    2.44 +        val start_term = Free ("P", simpleT --> @{typ bool}) $ list_comb (constr, bounds)
    2.45 +      in fold_rev (fn f => fn t => f t) fns start_term end
    2.46 +    fun mk_rhs exprs =
    2.47 +      @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
    2.48 +        (foldr1 HOLogic.mk_disj exprs) $ @{term "True"}
    2.49 +    val rhss =
    2.50 +      Datatype_Aux.interpret_construction descr vs
    2.51 +        { atyp = mk_call, dtyp = mk_aux_call }
    2.52 +      |> (map o apfst) Type
    2.53 +      |> map (fn (T, cs) => map (mk_consexpr T) cs)
    2.54 +      |> map mk_rhs
    2.55 +    val lhss =
    2.56 +      map2 (fn t => fn T => t $ Free ("P", T --> @{typ bool}) $ size) bounded_foralls (Ts @ Us)
    2.57 +    val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
    2.58 +  in
    2.59 +    eqs
    2.60 +  end
    2.61 +
    2.62 +(* creating the bounded_forall instances *)
    2.63 +
    2.64 +fun instantiate_bounded_forall_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    2.65 +  let
    2.66 +    val _ = Datatype_Aux.message config "Creating bounded universal quantifiers...";
    2.67 +    val bounded_forallsN = map (prefix (bounded_forallN ^ "_")) (names @ auxnames);
    2.68 +  in
    2.69 +    thy
    2.70 +    |> Class.instantiation (tycos, vs, @{sort bounded_forall})
    2.71 +    |> Quickcheck_Common.define_functions
    2.72 +        (fn bounded_foralls => 
    2.73 +          mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us), NONE)
    2.74 +        prfx ["P", "i"] bounded_forallsN (map bounded_forallT (Ts @ Us))
    2.75 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    2.76 +  end handle FUNCTION_TYPE =>
    2.77 +    (Datatype_Aux.message config
    2.78 +      "Creation of bounded universal quantifiers failed because the datatype contains a function type";
    2.79 +    thy)
    2.80 +    
    2.81  (** building and compiling generator expressions **)
    2.82  
    2.83  fun mk_generator_expr ctxt (t, eval_terms) =
    2.84 @@ -334,6 +399,8 @@
    2.85  val setup =
    2.86    Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.87        (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
    2.88 +  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.89 +      (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
    2.90    #> setup_smart_quantifier
    2.91    #> setup_quickcheck_pretty
    2.92    #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))