--- a/etc/isar-keywords.el Sat Dec 17 15:53:58 2011 +0100
+++ b/etc/isar-keywords.el Tue Dec 20 18:46:05 2011 +0100
@@ -196,6 +196,7 @@
"pwd"
"qed"
"quickcheck"
+ "quickcheck_generator"
"quickcheck_params"
"quit"
"quotient_definition"
@@ -505,6 +506,7 @@
"primrec"
"print_ast_translation"
"print_translation"
+ "quickcheck_generator"
"quickcheck_params"
"quotient_definition"
"realizability"
--- a/src/HOL/IMP/Collecting.thy Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/IMP/Collecting.thy Tue Dec 20 18:46:05 2011 +0100
@@ -63,30 +63,30 @@
end
-fun sub1 :: "'a acom \<Rightarrow> 'a acom" where
-"sub1(c1;c2) = c1" |
-"sub1(IF b THEN c1 ELSE c2 {S}) = c1" |
-"sub1({I} WHILE b DO c {P}) = c"
+fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where
+"sub\<^isub>1(c1;c2) = c1" |
+"sub\<^isub>1(IF b THEN c1 ELSE c2 {S}) = c1" |
+"sub\<^isub>1({I} WHILE b DO c {P}) = c"
-fun sub2 :: "'a acom \<Rightarrow> 'a acom" where
-"sub2(c1;c2) = c2" |
-"sub2(IF b THEN c1 ELSE c2 {S}) = c2"
+fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where
+"sub\<^isub>2(c1;c2) = c2" |
+"sub\<^isub>2(IF b THEN c1 ELSE c2 {S}) = c2"
fun invar :: "'a acom \<Rightarrow> 'a" where
"invar({I} WHILE b DO c {P}) = I"
-fun lift :: "('a set set \<Rightarrow> 'a set) \<Rightarrow> com \<Rightarrow> 'a set acom set \<Rightarrow> 'a set acom"
+fun lift :: "('a set \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'a acom"
where
"lift F com.SKIP M = (SKIP {F (post ` M)})" |
"lift F (x ::= a) M = (x ::= a {F (post ` M)})" |
"lift F (c1;c2) M =
- lift F c1 (sub1 ` M); lift F c2 (sub2 ` M)" |
+ lift F c1 (sub\<^isub>1 ` M); lift F c2 (sub\<^isub>2 ` M)" |
"lift F (IF b THEN c1 ELSE c2) M =
- IF b THEN lift F c1 (sub1 ` M) ELSE lift F c2 (sub2 ` M)
+ IF b THEN lift F c1 (sub\<^isub>1 ` M) ELSE lift F c2 (sub\<^isub>2 ` M)
{F (post ` M)}" |
"lift F (WHILE b DO c) M =
{F (invar ` M)}
- WHILE b DO lift F c (sub1 ` M)
+ WHILE b DO lift F c (sub\<^isub>1 ` M)
{F (post ` M)}"
interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
--- a/src/HOL/Library/Dlist.thy Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/Library/Dlist.thy Tue Dec 20 18:46:05 2011 +0100
@@ -180,6 +180,9 @@
enriched_type map: map
by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
+subsection {* Quickcheck generators *}
+
+quickcheck_generator dlist constructors: empty, insert
hide_const (open) member fold foldr empty insert remove map filter null member length fold
--- a/src/HOL/Library/Permutations.thy Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/Library/Permutations.thy Tue Dec 20 18:46:05 2011 +0100
@@ -742,7 +742,6 @@
apply metis
done
-term setsum
lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs")
proof-
let ?S = "{p . p permutes S}"
--- a/src/HOL/Library/Polynomial.thy Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/Library/Polynomial.thy Tue Dec 20 18:46:05 2011 +0100
@@ -1503,6 +1503,8 @@
code_datatype "0::'a::zero poly" pCons
+quickcheck_generator poly constructors: "0::'a::zero poly", pCons
+
declare pCons_0_0 [code_post]
instantiation poly :: ("{zero, equal}") equal
--- a/src/HOL/Library/RBT.thy Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/Library/RBT.thy Tue Dec 20 18:46:05 2011 +0100
@@ -169,5 +169,8 @@
"distinct (keys t)"
by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
+subsection {* Quickcheck generators *}
+
+quickcheck_generator rbt constructors: empty, insert
end
--- a/src/HOL/Quickcheck_Exhaustive.thy Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Tue Dec 20 18:46:05 2011 +0100
@@ -4,7 +4,9 @@
theory Quickcheck_Exhaustive
imports Quickcheck
-uses ("Tools/Quickcheck/exhaustive_generators.ML")
+uses
+ ("Tools/Quickcheck/exhaustive_generators.ML")
+ ("Tools/Quickcheck/abstract_generators.ML")
begin
subsection {* basic operations for exhaustive generators *}
@@ -521,7 +523,7 @@
where
"pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
-subsection {* Defining combinators for any first-order data type *}
+subsection {* Defining generators for any first-order data type *}
axiomatization unknown :: 'a
@@ -533,6 +535,10 @@
declare [[quickcheck_batch_tester = exhaustive]]
+subsection {* Defining generators for abstract types *}
+
+use "Tools/Quickcheck/abstract_generators.ML"
+
hide_fact orelse_def
no_notation orelse (infixr "orelse" 55)
--- a/src/HOL/Tools/ATP/atp_translate.ML Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Dec 20 18:46:05 2011 +0100
@@ -1563,8 +1563,8 @@
fun atype_of_type_vars (Simple_Types (_, Polymorphic, _)) = SOME atype_of_types
| atype_of_type_vars _ = NONE
-fun bound_tvars type_enc Ts =
- mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts)
+fun bound_tvars type_enc sorts Ts =
+ (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
#> mk_aquant AForall
(map_filter (fn TVar (x as (s, _), _) =>
SOME ((make_schematic_type_var x, s),
@@ -1575,7 +1575,7 @@
(if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
|> close_formula_universally
- |> bound_tvars type_enc atomic_Ts
+ |> bound_tvars type_enc true atomic_Ts
val type_tag = `(make_fixed_const NONE) type_tag_name
@@ -1889,7 +1889,7 @@
should_guard_var_in_formula
(if pos then SOME true else NONE)
|> close_formula_universally
- |> bound_tvars type_enc atomic_types,
+ |> bound_tvars type_enc true atomic_types,
NONE,
case locality of
Intro => isabelle_info format introN
@@ -1930,7 +1930,7 @@
|> formula_from_iformula ctxt format mono type_enc
should_guard_var_in_formula (SOME false)
|> close_formula_universally
- |> bound_tvars type_enc atomic_types, NONE, NONE)
+ |> bound_tvars type_enc true atomic_types, NONE, NONE)
fun formula_line_for_free_type j phi =
Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
@@ -2127,7 +2127,7 @@
|> formula_from_iformula ctxt format mono type_enc
(K (K (K (K (K (K true)))))) (SOME true)
|> close_formula_universally
- |> bound_tvars type_enc (atomic_types_of T),
+ |> bound_tvars type_enc true (atomic_types_of T),
isabelle_info format introN, NONE)
fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
@@ -2205,7 +2205,7 @@
|> formula_from_iformula ctxt format mono type_enc
(K (K (K (K (K (K true)))))) (SOME true)
|> close_formula_universally
- |> n > 1 ? bound_tvars type_enc (atomic_types_of T)
+ |> bound_tvars type_enc (n > 1) (atomic_types_of T)
|> maybe_negate,
isabelle_info format introN, NONE)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Tue Dec 20 18:46:05 2011 +0100
@@ -0,0 +1,64 @@
+(* Title: HOL/Tools/Quickcheck/abstract_generators.ML
+ Author: Lukas Bulwahn, TU Muenchen
+
+Quickcheck generators for abstract types.
+*)
+
+signature ABSTRACT_GENERATORS =
+sig
+ val quickcheck_generator : string -> term list -> theory -> theory
+end;
+
+structure Abstract_Generators : ABSTRACT_GENERATORS =
+struct
+
+fun check_constrs ctxt tyco constrs =
+ let
+ fun check_type c =
+ case try (dest_Type o body_type o fastype_of) c of
+ NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.")
+ | SOME (tyco', vs) => if not (tyco' = tyco) then
+ error (Syntax.string_of_term ctxt c ^ " has mismatching result type. " ^
+ "Expected type constructor " ^ quote tyco ^ ", but found " ^ quote tyco' ^ ".")
+ else
+ case try (map dest_TFree) vs of
+ NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.")
+ | SOME _ => ()
+ in
+ map check_type constrs
+ end
+
+fun gen_quickcheck_generator prep_tyco prep_term tyco_raw constrs_raw thy =
+ let
+ val ctxt = Proof_Context.init_global thy
+ val tyco = prep_tyco ctxt tyco_raw
+ val constrs = map (prep_term ctxt) constrs_raw
+ val _ = check_constrs ctxt tyco constrs
+ val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs)))))
+ val name = Long_Name.base_name tyco
+ fun mk_dconstrs (Const (s, T)) =
+ (s, map (Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T))
+ | mk_dconstrs t = error (Syntax.string_of_term ctxt t ^
+ " is not a valid constructor for quickcheck_generator, which expects a constant.")
+ fun the_descr thy _ =
+ let
+ val descr = [(0, (tyco, map Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))]
+ in
+ (descr, vs, [tyco], name, ([name], []), ([Type (tyco, map TFree vs)], []))
+ end
+ in
+ Quickcheck_Common.ensure_sort (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}),
+ (the_descr, Exhaustive_Generators.instantiate_full_exhaustive_datatype))
+ Datatype_Aux.default_config [tyco] thy
+ end
+
+val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
+
+val quickcheck_generator_cmd = gen_quickcheck_generator
+ (fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
+
+val _ = Outer_Syntax.command "quickcheck_generator" "define quickcheck generators for abstract types"
+ Keyword.thy_decl (Parse.type_const -- (Args.$$$ "constructors" |-- Parse.$$$ ":" |-- Parse.list1 Parse.term)
+ >> (fn (tyco, constrs) => Toplevel.theory (quickcheck_generator_cmd tyco constrs)))
+
+end;
\ No newline at end of file
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Dec 20 18:46:05 2011 +0100
@@ -20,6 +20,9 @@
val quickcheck_pretty : bool Config.T
val setup_exhaustive_datatype_interpretation : theory -> theory
val setup: theory -> theory
+
+ val instantiate_full_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
+ (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
end;
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
@@ -500,14 +503,12 @@
(* setup *)
val setup_exhaustive_datatype_interpretation =
- Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
- (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
+ Quickcheck_Common.datatype_interpretation (@{sort exhaustive}, instantiate_exhaustive_datatype)
val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
val setup =
- Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
- (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
+ Quickcheck_Common.datatype_interpretation (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
(* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
#> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Dec 20 18:46:05 2011 +0100
@@ -501,8 +501,7 @@
val setup =
Code.datatype_interpretation ensure_partial_term_of
#> Code.datatype_interpretation ensure_partial_term_of_code
- #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
- (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
+ #> Quickcheck_Common.datatype_interpretation (@{sort narrowing}, instantiate_narrowing_datatype)
#> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
end;
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Dec 20 18:46:05 2011 +0100
@@ -21,10 +21,16 @@
val generator_test_goal_terms :
string * compile_generator -> Proof.context -> bool -> (string * typ) list
-> (term * term list) list -> Quickcheck.result list
- val ensure_sort_datatype:
- ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list
- -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory)
+ type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
+ -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+ val ensure_sort :
+ (((sort * sort) * sort) *
+ ((theory -> string list -> Datatype_Aux.descr * (string * sort) list * string list
+ * string * (string list * string list) * (typ list * typ list)) * instantiation))
-> Datatype.config -> string list -> theory -> theory
+ val ensure_common_sort_datatype :
+ (sort * instantiation) -> Datatype.config -> string list -> theory -> theory
+ val datatype_interpretation : (sort * instantiation) -> theory -> theory
val gen_mk_parametric_generator_expr :
(((Proof.context -> term * term list -> term) * term) * typ)
-> Proof.context -> (term * term list) list -> term
@@ -199,7 +205,7 @@
!current_result)
| SOME test_fun =>
let
- val _ = Quickcheck.message ctxt ("Testing conjecture with with Quickcheck-" ^ name ^ "...");
+ val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...");
fun test genuine_only enum = case get_first (test_card_size test_fun genuine_only) enum of
SOME ((card, _), (true, ts)) =>
Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (true, ts)) current_result
@@ -379,6 +385,9 @@
(** ensuring sort constraints **)
+type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
+ -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+
fun perhaps_constrain thy insts raw_vs =
let
fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
@@ -389,10 +398,10 @@
in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
end handle Sorts.CLASS_ERROR _ => NONE;
-fun ensure_sort_datatype (((sort_vs, aux_sort), sort), instantiate_datatype) config raw_tycos thy =
+fun ensure_sort (((sort_vs, aux_sort), sort), (the_descr, instantiate)) config raw_tycos thy =
let
val algebra = Sign.classes_of thy;
- val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = Datatype.the_descr thy raw_tycos
+ val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos
val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd)
(Datatype_Aux.interpret_construction descr vs constr)
@@ -401,11 +410,16 @@
val has_inst = exists (fn tyco => can (Sorts.mg_domain algebra tyco) sort) tycos;
in if has_inst then thy
else case perhaps_constrain thy insts vs
- of SOME constrain => instantiate_datatype config descr
+ of SOME constrain => instantiate config descr
(map constrain vs) tycos prfx (names, auxnames)
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
| NONE => thy
end;
+
+fun ensure_common_sort_datatype (sort, instantiate) =
+ ensure_sort (((@{sort typerep}, @{sort term_of}), sort), (Datatype.the_descr, instantiate))
+
+val datatype_interpretation = Datatype.interpretation o ensure_common_sort_datatype
(** generic parametric compilation **)
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Tue Dec 20 18:46:05 2011 +0100
@@ -460,8 +460,7 @@
val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
val setup =
- Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
- (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
+ Quickcheck_Common.datatype_interpretation (@{sort random}, instantiate_random_datatype)
#> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
end;
--- a/src/HOL/Tools/Quotient/quotient_def.ML Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Dec 20 18:46:05 2011 +0100
@@ -89,7 +89,7 @@
Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
fun read_term' cnstr ctxt =
- check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
+ check_term' cnstr ctxt o Syntax.parse_term ctxt
val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term'
--- a/src/HOL/ex/Quickcheck_Examples.thy Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Tue Dec 20 18:46:05 2011 +0100
@@ -6,7 +6,7 @@
header {* Examples for the 'quickcheck' command *}
theory Quickcheck_Examples
-imports Complex_Main
+imports Complex_Main "~~/src/HOL/Library/Dlist"
begin
text {*
@@ -342,6 +342,17 @@
quickcheck[expect = counterexample]
oops
+subsection {* Examples with abstract types *}
+
+lemma
+ "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1"
+quickcheck[exhaustive]
+oops
+
+lemma
+ "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1"
+quickcheck[exhaustive]
+oops
subsection {* Examples with Records *}
--- a/src/HOL/ex/Sqrt.thy Sat Dec 17 15:53:58 2011 +0100
+++ b/src/HOL/ex/Sqrt.thy Tue Dec 20 18:46:05 2011 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/ex/Sqrt.thy
- Author: Markus Wenzel, TU Muenchen
+ Author: Markus Wenzel, Tobias Nipkow, TU Muenchen
*)
header {* Square roots of primes are irrational *}
@@ -47,7 +47,7 @@
with p show False by simp
qed
-corollary "sqrt (real (2::nat)) \<notin> \<rat>"
+corollary sqrt_real_2_not_rat: "sqrt (real (2::nat)) \<notin> \<rat>"
by (rule sqrt_prime_irrational) (rule two_is_prime_nat)
@@ -87,4 +87,22 @@
with p show False by simp
qed
+
+text{* Another old chestnut, which is a consequence of the irrationality of 2. *}
+
+lemma "\<exists>a b::real. a \<notin> \<rat> \<and> b \<notin> \<rat> \<and> a powr b \<in> \<rat>" (is "EX a b. ?P a b")
+proof cases
+ assume "sqrt 2 powr sqrt 2 \<in> \<rat>"
+ hence "?P (sqrt 2) (sqrt 2)" by(metis sqrt_real_2_not_rat[simplified])
+ thus ?thesis by blast
+next
+ assume 1: "sqrt 2 powr sqrt 2 \<notin> \<rat>"
+ have "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2"
+ using powr_realpow[of _ 2]
+ by (simp add: powr_powr power2_eq_square[symmetric])
+ hence "?P (sqrt 2 powr sqrt 2) (sqrt 2)"
+ by (metis 1 Rats_number_of sqrt_real_2_not_rat[simplified])
+ thus ?thesis by blast
+qed
+
end