--- 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 ***
--- 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 \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
"random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight
- [(1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
+ [(1, Quickcheck.random j o\<rightarrow> (\<lambda>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\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun_aux i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
- (1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
+ [(Suc_code_numeral i, Quickcheck.random j o\<rightarrow> (\<lambda>x. Quickcheck.random j o\<rightarrow> (\<lambda>y. random_finfun_aux i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
+ (1, Quickcheck.random j o\<rightarrow> (\<lambda>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\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun_aux (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
- (1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
+ [(i, Quickcheck.random j o\<rightarrow> (\<lambda>x. Quickcheck.random j o\<rightarrow> (\<lambda>y. random_finfun_aux (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
+ (1, Quickcheck.random j o\<rightarrow> (\<lambda>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:)
--- 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\<rightarrow>" 60)
--- 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\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
+ "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
let j = Code_Numeral.int_of (denom + 1)
in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
--- 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\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
+ "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
instance ..
--- 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 \<supseteq>") and
supset_eq ("(_/ \<supseteq> _)" [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 \<le> 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 *}
--- 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;
--- 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);
--- 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