# HG changeset patch # User noschinl # Date 1324403165 -3600 # Node ID 0724e56b5dea19b70fc5343753d166f2618e5746 # Parent 32f769f94ea4442a52dc7fdd5d84053b85244e10# Parent d7d6c8cfb6f677402b349f709d70b3d07b6d53b6 merged diff -r 32f769f94ea4 -r 0724e56b5dea etc/isar-keywords.el --- 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" diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/IMP/Collecting.thy --- 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 \ '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 \ '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 \ 'a acom" where -"sub2(c1;c2) = c2" | -"sub2(IF b THEN c1 ELSE c2 {S}) = c2" +fun sub\<^isub>2 :: "'a acom \ 'a acom" where +"sub\<^isub>2(c1;c2) = c2" | +"sub\<^isub>2(IF b THEN c1 ELSE c2 {S}) = c2" fun invar :: "'a acom \ 'a" where "invar({I} WHILE b DO c {P}) = I" -fun lift :: "('a set set \ 'a set) \ com \ 'a set acom set \ 'a set acom" +fun lift :: "('a set \ 'a) \ com \ 'a acom set \ '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" diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Library/Dlist.thy --- 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 diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Library/Permutations.thy --- 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 (\p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs") proof- let ?S = "{p . p permutes S}" diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Library/Polynomial.thy --- 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 diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Library/RBT.thy --- 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 diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Quickcheck_Exhaustive.thy --- 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) diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Tools/ATP/atp_translate.ML --- 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 diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Tools/Quickcheck/abstract_generators.ML --- /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 diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- 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 diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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; diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Tools/Quickcheck/quickcheck_common.ML --- 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 **) diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Tools/Quickcheck/random_generators.ML --- 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; diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/Tools/Quotient/quotient_def.ML --- 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' diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/ex/Quickcheck_Examples.thy --- 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 *} diff -r 32f769f94ea4 -r 0724e56b5dea src/HOL/ex/Sqrt.thy --- 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)) \ \" +corollary sqrt_real_2_not_rat: "sqrt (real (2::nat)) \ \" 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 "\a b::real. a \ \ \ b \ \ \ a powr b \ \" (is "EX a b. ?P a b") +proof cases + assume "sqrt 2 powr sqrt 2 \ \" + 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 \ \" + 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