# HG changeset patch # User wenzelm # Date 1245094407 -7200 # Node ID 76d8c30a92c5a96ca0534757a1a3a9564c965472 # Parent f4723b1ae5a14da57ef9dd8c5d25ef4c72a210cb# Parent ef30cd0e41e5f9f2c240c1f8fdfdc8a416c6b915 merged diff -r ef30cd0e41e5 -r 76d8c30a92c5 NEWS --- a/NEWS Mon Jun 15 21:17:34 2009 +0200 +++ b/NEWS Mon Jun 15 21:33:27 2009 +0200 @@ -40,6 +40,9 @@ * Implementation of quickcheck using generic code generator; default generators are provided for all suitable HOL types, records and datatypes. +* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions +Set.Pow_def and Set.image_def. INCOMPATIBILITY. + *** ML *** diff -r ef30cd0e41e5 -r 76d8c30a92c5 src/HOL/Library/Fin_Fun.thy --- a/src/HOL/Library/Fin_Fun.thy Mon Jun 15 21:17:34 2009 +0200 +++ b/src/HOL/Library/Fin_Fun.thy Mon Jun 15 21:33:27 2009 +0200 @@ -323,13 +323,13 @@ primrec random_finfun_aux :: "code_numeral \ code_numeral \ Random.seed \ ('a \\<^isub>f 'b \ (unit \ Code_Eval.term)) \ Random.seed" where "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight - [(1, random j o\ (\y. Pair (valtermify_finfun_const y)))])" + [(1, Quickcheck.random j o\ (\y. Pair (valtermify_finfun_const y)))])" | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight - [(Suc_code_numeral i, random j o\ (\x. random j o\ (\y. random_finfun_aux i j o\ (\f. Pair (valtermify_finfun_update_code x y f))))), - (1, random j o\ (\y. Pair (valtermify_finfun_const y)))])" + [(Suc_code_numeral i, Quickcheck.random j o\ (\x. Quickcheck.random j o\ (\y. random_finfun_aux i j o\ (\f. Pair (valtermify_finfun_update_code x y f))))), + (1, Quickcheck.random j o\ (\y. Pair (valtermify_finfun_const y)))])" definition - "random i = random_finfun_aux i i" + "Quickcheck.random i = random_finfun_aux i i" instance .. @@ -337,8 +337,8 @@ lemma random_finfun_aux_code [code]: "random_finfun_aux i j = Quickcheck.collapse (Random.select_weight - [(i, random j o\ (\x. random j o\ (\y. random_finfun_aux (i - 1) j o\ (\f. Pair (valtermify_finfun_update_code x y f))))), - (1, random j o\ (\y. Pair (valtermify_finfun_const y)))])" + [(i, Quickcheck.random j o\ (\x. Quickcheck.random j o\ (\y. random_finfun_aux (i - 1) j o\ (\f. Pair (valtermify_finfun_update_code x y f))))), + (1, Quickcheck.random j o\ (\y. Pair (valtermify_finfun_const y)))])" apply (cases i rule: code_numeral.exhaust) apply (simp_all only: random_finfun_aux.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one) apply (subst select_weight_cons_zero) apply (simp only:) diff -r ef30cd0e41e5 -r 76d8c30a92c5 src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Mon Jun 15 21:17:34 2009 +0200 +++ b/src/HOL/Quickcheck.thy Mon Jun 15 21:33:27 2009 +0200 @@ -137,7 +137,7 @@ code_reserved Quickcheck Quickcheck_Generators -hide (open) const collapse beyond random_fun_aux random_fun_lift +hide (open) const random collapse beyond random_fun_aux random_fun_lift no_notation fcomp (infixl "o>" 60) no_notation scomp (infixl "o\" 60) diff -r ef30cd0e41e5 -r 76d8c30a92c5 src/HOL/Rational.thy --- a/src/HOL/Rational.thy Mon Jun 15 21:17:34 2009 +0200 +++ b/src/HOL/Rational.thy Mon Jun 15 21:33:27 2009 +0200 @@ -1012,7 +1012,7 @@ begin definition - "random i = random i o\ (\num. Random.range i o\ (\denom. Pair ( + "Quickcheck.random i = Quickcheck.random i o\ (\num. Random.range i o\ (\denom. Pair ( let j = Code_Numeral.int_of (denom + 1) in valterm_fract num (j, \u. Code_Eval.term_of j))))" diff -r ef30cd0e41e5 -r 76d8c30a92c5 src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Mon Jun 15 21:17:34 2009 +0200 +++ b/src/HOL/RealDef.thy Mon Jun 15 21:33:27 2009 +0200 @@ -1137,7 +1137,7 @@ begin definition - "random i = random i o\ (\r. Pair (valterm_ratreal r))" + "Quickcheck.random i = Quickcheck.random i o\ (\r. Pair (valterm_ratreal r))" instance .. diff -r ef30cd0e41e5 -r 76d8c30a92c5 src/HOL/Set.thy --- a/src/HOL/Set.thy Mon Jun 15 21:17:34 2009 +0200 +++ b/src/HOL/Set.thy Mon Jun 15 21:33:27 2009 +0200 @@ -23,8 +23,6 @@ Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers" Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers" Bex1 :: "'a set => ('a => bool) => bool" -- "bounded unique existential quantifiers" - Pow :: "'a set => 'a set set" -- "powerset" - image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) local @@ -215,9 +213,6 @@ supset_eq ("op \") and supset_eq ("(_/ \ _)" [50, 51] 50) -abbreviation - range :: "('a => 'b) => 'b set" where -- "of function" - "range f == f ` UNIV" subsubsection "Bounded quantifiers" @@ -408,9 +403,15 @@ end -defs - Pow_def: "Pow A == {B. B <= A}" - image_def: "f`A == {y. EX x:A. y = f(x)}" +definition Pow :: "'a set => 'a set set" where + Pow_def: "Pow A = {B. B \ A}" + +definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where + image_def: "f ` A = {y. EX x:A. y = f(x)}" + +abbreviation + range :: "('a => 'b) => 'b set" where -- "of function" + "range f == f ` UNIV" subsection {* Lemmas and proof tool setup *} diff -r ef30cd0e41e5 -r 76d8c30a92c5 src/HOL/Tools/datatype_package/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Mon Jun 15 21:17:34 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Mon Jun 15 21:33:27 2009 +0200 @@ -458,9 +458,9 @@ let val isoT = T --> Univ_elT in HOLogic.imp $ (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $ - (if i < length newTs then Const ("True", HOLogic.boolT) + (if i < length newTs then HOLogic.true_const else HOLogic.mk_mem (mk_Free "x" Univ_elT i, - Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $ + Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $ Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T))) end; diff -r ef30cd0e41e5 -r 76d8c30a92c5 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Mon Jun 15 21:17:34 2009 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Mon Jun 15 21:33:27 2009 +0200 @@ -49,7 +49,7 @@ mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit => term"}, t'))); fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty - (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i); + (Sign.mk_const thy (@{const_name Quickcheck.random}, [ty]) $ Bound i); in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end; fun compile_generator_expr thy t = @@ -98,7 +98,7 @@ val Ttm = mk_termifyT T; val typtm = mk_termifyT typ; fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts)); - fun mk_random T = mk_const @{const_name random} [T]; + fun mk_random T = mk_const @{const_name Quickcheck.random} [T]; val size = @{term "j::code_numeral"}; val v = "x"; val t_v = Free (v, typtm); diff -r ef30cd0e41e5 -r 76d8c30a92c5 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon Jun 15 21:17:34 2009 +0200 +++ b/src/Pure/Isar/code.ML Mon Jun 15 21:33:27 2009 +0200 @@ -30,6 +30,7 @@ (*code equations*) val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool + val mk_eqn_warning: theory -> (string -> bool) -> thm -> (thm * bool) option val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option val assert_eqn: theory -> thm * bool -> thm * bool val assert_eqns_const: theory -> string @@ -72,6 +73,7 @@ val get_datatype_of_constr: theory -> string -> string option val default_typscheme: theory -> string -> (string * sort) list * typ val these_eqns: theory -> string -> (thm * bool) list + val all_eqns: theory -> (thm * bool) list val get_case_scheme: theory -> string -> (int * (int * string list)) option val is_undefined: theory -> string -> bool val print_codesetup: theory -> unit @@ -363,6 +365,7 @@ exception BAD_THM of string; fun bad_thm msg = raise BAD_THM msg; fun error_thm f thm = f thm handle BAD_THM msg => error msg; +fun warning_thm f thm = SOME (f thm) handle BAD_THM msg => (warning msg; NONE) fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE; fun is_linear thm = @@ -445,6 +448,10 @@ fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy)); +fun mk_eqn_warning thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) + o warning_thm (gen_assert_eqn thy is_constr_head (K true)) + o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); + fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) o try_thm (gen_assert_eqn thy is_constr_head (K true)) o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); @@ -861,6 +868,11 @@ fun add_eqn thm thy = gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, true)) thy; +fun add_warning_eqn thm thy = + case mk_eqn_warning thy (is_constr thy) thm + of SOME eqn => gen_add_eqn false eqn thy + | NONE => thy; + fun add_default_eqn thm thy = case mk_eqn_liberal thy (is_constr thy) thm of SOME eqn => gen_add_eqn true eqn thy @@ -938,7 +950,7 @@ || Scan.succeed (mk_attribute add)) in TypeInterpretation.init - #> add_del_attribute ("", (add_eqn, del_eqn)) + #> add_del_attribute ("", (add_warning_eqn, del_eqn)) #> add_simple_attribute ("nbe", add_nbe_eqn) end)); @@ -947,6 +959,10 @@ |> (map o apfst) (Thm.transfer thy) |> burrow_fst (common_typ_eqns thy); +fun all_eqns thy = + Symtab.dest ((the_eqns o the_exec) thy) + |> maps (Lazy.force o snd o snd o fst o snd); + fun default_typscheme thy c = let fun the_const_typscheme c = (curry (typscheme thy) c o snd o dest_Const