--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Apr 04 14:37:20 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Apr 04 14:44:11 2011 +0200
@@ -23,10 +23,6 @@
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
struct
-(* static options *)
-
-val define_foundationally = false
-
(* dynamic options *)
val (smart_quantifier, setup_smart_quantifier) =
@@ -71,8 +67,7 @@
let
val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
in
- Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T)
- $ x $ y
+ Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y
end
(** datatypes **)
@@ -157,11 +152,6 @@
(HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
@{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
-fun pat_completeness_auto ctxt =
- Pat_Completeness.pat_completeness_tac ctxt 1
- THEN auto_tac (clasimpset_of ctxt)
-
-
(* creating the instances *)
fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
@@ -171,39 +161,9 @@
in
thy
|> Class.instantiation (tycos, vs, @{sort exhaustive})
- |> (if define_foundationally then
- let
- val exhaustives = map2 (fn name => fn T => Free (name, exhaustiveT T)) exhaustivesN (Ts @ Us)
- val eqs = mk_equations descr vs tycos exhaustives (Ts, Us)
- in
- Function.add_function
- (map (fn (name, T) =>
- Syntax.no_syn (Binding.conceal (Binding.name name), SOME (exhaustiveT T)))
- (exhaustivesN ~~ (Ts @ Us)))
- (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs)
- Function_Common.default_config pat_completeness_auto
- #> snd
- #> Local_Theory.restore
- #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
- #> snd
- end
- else
- fold_map (fn (name, T) => Local_Theory.define
- ((Binding.conceal (Binding.name name), NoSyn),
- (apfst Binding.conceal Attrib.empty_binding, mk_undefined (exhaustiveT T)))
- #> apfst fst) (exhaustivesN ~~ (Ts @ Us))
- #> (fn (exhaustives, lthy) =>
- let
- val eqs_t = mk_equations descr vs tycos exhaustives (Ts, Us)
- val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
- (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
- in
- fold (fn (name, eq) => Local_Theory.note
- ((Binding.conceal (Binding.qualify true prfx
- (Binding.qualify true name (Binding.name "simps"))),
- Code.add_default_eqn_attrib :: map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (exhaustivesN ~~ eqs) lthy
- end))
+ |> Quickcheck_Common.define_functions
+ (fn exhaustives => mk_equations descr vs tycos exhaustives (Ts, Us), SOME termination_tac)
+ prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us))
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
end handle FUNCTION_TYPE =>
(Datatype_Aux.message config
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Apr 04 14:37:20 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Apr 04 14:44:11 2011 +0200
@@ -21,9 +21,6 @@
val (finite_functions, setup_finite_functions) =
Attrib.config_bool "quickcheck_finite_functions" (K true)
-
-fun mk_undefined T = Const(@{const_name undefined}, T)
-
(* narrowing specific names and types *)
exception FUNCTION_TYPE;
@@ -57,12 +54,7 @@
fun mk_equations descr vs tycos narrowings (Ts, Us) =
let
fun mk_call T =
- let
- val narrowing =
- Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T)
- in
- (T, narrowing)
- end
+ (T, Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T))
fun mk_aux_call fTs (k, _) (tyco, Ts) =
let
val T = Type (tyco, Ts)
@@ -86,8 +78,7 @@
in
eqs
end
-
-
+
fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
val _ = Datatype_Aux.message config "Creating narrowing generators ...";
@@ -95,22 +86,9 @@
in
thy
|> Class.instantiation (tycos, vs, @{sort narrowing})
- |> (fold_map (fn (name, T) => Local_Theory.define
- ((Binding.conceal (Binding.name name), NoSyn),
- (apfst Binding.conceal Attrib.empty_binding, mk_undefined (narrowingT T)))
- #> apfst fst) (narrowingsN ~~ (Ts @ Us))
- #> (fn (narrowings, lthy) =>
- let
- val eqs_t = mk_equations descr vs tycos narrowings (Ts, Us)
- val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
- (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
- in
- fold (fn (name, eq) => Local_Theory.note
- ((Binding.conceal (Binding.qualify true prfx
- (Binding.qualify true name (Binding.name "simps"))),
- Code.add_default_eqn_attrib :: map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (narrowingsN ~~ eqs) lthy
- end))
+ |> Quickcheck_Common.define_functions
+ (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE)
+ prfx [] narrowingsN (map narrowingT (Ts @ Us))
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
end;
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Apr 04 14:37:20 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Apr 04 14:44:11 2011 +0200
@@ -7,6 +7,8 @@
signature QUICKCHECK_COMMON =
sig
val strip_imp : term -> (term list * term)
+ val define_functions : ((term list -> term list) * (Proof.context -> tactic) option)
+ -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context
val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
-> (string * sort -> string * sort) option
val ensure_sort_datatype:
@@ -21,11 +23,57 @@
structure Quickcheck_Common : QUICKCHECK_COMMON =
struct
+(* static options *)
+
+val define_foundationally = false
+
(* HOLogic's term functions *)
fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
| strip_imp A = ([], A)
+fun mk_undefined T = Const(@{const_name undefined}, T)
+
+(* defining functions *)
+
+fun pat_completeness_auto ctxt =
+ Pat_Completeness.pat_completeness_tac ctxt 1
+ THEN auto_tac (clasimpset_of ctxt)
+
+fun define_functions (mk_equations, termination_tac) prfx argnames names Ts =
+ if define_foundationally andalso is_some termination_tac then
+ let
+ val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts)
+ in
+ Function.add_function
+ (map (fn (name, T) =>
+ Syntax.no_syn (Binding.conceal (Binding.name name), SOME T))
+ (names ~~ Ts))
+ (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
+ Function_Common.default_config pat_completeness_auto
+ #> snd
+ #> Local_Theory.restore
+ #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
+ #> snd
+ end
+ else
+ fold_map (fn (name, T) => Local_Theory.define
+ ((Binding.conceal (Binding.name name), NoSyn),
+ (apfst Binding.conceal Attrib.empty_binding, mk_undefined T))
+ #> apfst fst) (names ~~ Ts)
+ #> (fn (consts, lthy) =>
+ let
+ val eqs_t = mk_equations consts
+ val eqs = map (fn eq => Goal.prove lthy argnames [] eq
+ (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
+ in
+ fold (fn (name, eq) => Local_Theory.note
+ ((Binding.conceal (Binding.qualify true prfx
+ (Binding.qualify true name (Binding.name "simps"))),
+ Code.add_default_eqn_attrib :: map (Attrib.internal o K)
+ [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (names ~~ eqs) lthy
+ end)
+
(** ensuring sort constraints **)
fun perhaps_constrain thy insts raw_vs =