--- a/src/HOL/Fun.thy Tue Jul 07 00:29:34 2009 +0200
+++ b/src/HOL/Fun.thy Tue Jul 07 07:56:24 2009 +0200
@@ -496,6 +496,40 @@
hide (open) const swap
+
+subsection {* Inversion of injective functions *}
+
+definition inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
+ "inv f y = (THE x. f x = y)"
+
+lemma inv_f_f:
+ assumes "inj f"
+ shows "inv f (f x) = x"
+proof -
+ from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)"
+ by (simp only: inj_eq)
+ also have "... = x" by (rule the_eq_trivial)
+ finally show ?thesis by (unfold inv_def)
+qed
+
+lemma f_inv_f:
+ assumes "inj f"
+ and "y \<in> range f"
+ shows "f (inv f y) = y"
+proof (unfold inv_def)
+ from `y \<in> range f` obtain x where "y = f x" ..
+ then have "f x = y" ..
+ then show "f (THE x. f x = y) = y"
+ proof (rule theI)
+ fix x' assume "f x' = y"
+ with `f x = y` have "f x' = f x" by simp
+ with `inj f` show "x' = x" by (rule injD)
+ qed
+qed
+
+hide (open) const inv
+
+
subsection {* Proof tool setup *}
text {* simplifies terms of the form
--- a/src/HOL/Inductive.thy Tue Jul 07 00:29:34 2009 +0200
+++ b/src/HOL/Inductive.thy Tue Jul 07 07:56:24 2009 +0200
@@ -258,38 +258,6 @@
subsection {* Inductive predicates and sets *}
-text {* Inversion of injective functions. *}
-
-constdefs
- myinv :: "('a => 'b) => ('b => 'a)"
- "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
-
-lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
-proof -
- assume "inj f"
- hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
- by (simp only: inj_eq)
- also have "... = x" by (rule the_eq_trivial)
- finally show ?thesis by (unfold myinv_def)
-qed
-
-lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
-proof (unfold myinv_def)
- assume inj: "inj f"
- assume "y \<in> range f"
- then obtain x where "y = f x" ..
- hence x: "f x = y" ..
- thus "f (THE x. f x = y) = y"
- proof (rule theI)
- fix x' assume "f x' = y"
- with x have "f x' = f x" by simp
- with inj show "x' = x" by (rule injD)
- qed
-qed
-
-hide const myinv
-
-
text {* Package setup. *}
theorems basic_monos =
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Jul 07 00:29:34 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Jul 07 07:56:24 2009 +0200
@@ -37,10 +37,6 @@
(** theory context references **)
-val f_myinv_f = thm "f_myinv_f";
-val myinv_f_f = thm "myinv_f_f";
-
-
fun exh_thm_of (dt_info : info Symtab.table) tname =
#exhaustion (the (Symtab.lookup dt_info tname));
@@ -162,7 +158,7 @@
app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
in (j + 1, list_all (map (pair "x") Ts,
HOLogic.mk_Trueprop
- (Free (List.nth (rep_set_names', k), UnivT') $ free_t)) :: prems,
+ (Free (nth rep_set_names' k, UnivT') $ free_t)) :: prems,
mk_lim free_t Ts :: ts)
end
| _ =>
@@ -225,7 +221,7 @@
val free_t = mk_Free "x" T j
in (case (strip_dtyp dt, strip_type T) of
((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
- (Const (List.nth (all_rep_names, m), U --> Univ_elT) $
+ (Const (nth all_rep_names m, U --> Univ_elT) $
app_bnds free_t (length Us)) Us :: r_args)
| _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
end;
@@ -295,8 +291,8 @@
fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) =
let
val argTs = map (typ_of_dtyp descr' sorts) cargs;
- val T = List.nth (recTs, k);
- val rep_name = List.nth (all_rep_names, k);
+ val T = nth recTs k;
+ val rep_name = nth all_rep_names k;
val rep_const = Const (rep_name, T --> Univ_elT);
val constr = Const (cname, argTs ---> T);
@@ -311,7 +307,7 @@
Ts @ [Us ---> Univ_elT])
else
(i2 + 1, i2', ts @ [mk_lim
- (Const (List.nth (all_rep_names, j), U --> Univ_elT) $
+ (Const (nth all_rep_names j, U --> Univ_elT) $
app_bnds (mk_Free "x" T' i2) (length Us)) Us], Ts)
| _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
end;
@@ -339,7 +335,7 @@
let
val (fs', eqns', _) = Library.foldl (make_iso_def k ks (length constrs))
((fs, eqns, 1), constrs);
- val iso = (List.nth (recTs, k), List.nth (all_rep_names, k))
+ val iso = (nth recTs k, nth all_rep_names k)
in (fs', eqns', isos @ [iso]) end;
val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
@@ -397,9 +393,9 @@
fun mk_ind_concl (i, _) =
let
- val T = List.nth (recTs, i);
- val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT);
- val rep_set_name = List.nth (rep_set_names, i)
+ val T = nth recTs i;
+ val Rep_t = Const (nth all_rep_names i, T --> Univ_elT);
+ val rep_set_name = nth rep_set_names i
in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $
HOLogic.mk_eq (mk_Free "x" T i, Bound 0)),
@@ -490,7 +486,7 @@
val Abs_inverse_thms' =
map #1 newT_iso_axms @
- map2 (fn r_inj => fn r => f_myinv_f OF [r_inj, r RS mp])
+ map2 (fn r_inj => fn r => @{thm f_inv_f} OF [r_inj, r RS mp])
iso_inj_thms_unfolded iso_thms;
val Abs_inverse_thms = maps (mk_funs_inv thy5) Abs_inverse_thms';
@@ -578,22 +574,22 @@
val _ = message config "Proving induction rule for datatypes ...";
val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
- (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded);
- val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded;
+ (map (fn r => r RS @{thm inv_f_f} RS subst) iso_inj_thms_unfolded);
+ val Rep_inverse_thms' = map (fn r => r RS @{thm inv_f_f}) iso_inj_thms_unfolded;
fun mk_indrule_lemma ((prems, concls), ((i, _), T)) =
let
- val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT) $
+ val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $
mk_Free "x" T i;
val Abs_t = if i < length newTs then
Const (Sign.intern_const thy6
- ("Abs_" ^ (List.nth (new_type_names, i))), Univ_elT --> T)
- else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $
- Const (List.nth (all_rep_names, i), T --> Univ_elT)
+ ("Abs_" ^ (nth new_type_names i)), Univ_elT --> T)
+ else Const (@{const_name Fun.inv}, [T --> Univ_elT, Univ_elT] ---> T) $
+ Const (nth all_rep_names i, T --> Univ_elT)
in (prems @ [HOLogic.imp $
- (Const (List.nth (rep_set_names, i), UnivT') $ Rep_t) $
+ (Const (nth rep_set_names i, UnivT') $ Rep_t) $
(mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
end;
--- a/src/HOL/Tools/quickcheck_generators.ML Tue Jul 07 00:29:34 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Jul 07 07:56:24 2009 +0200
@@ -5,7 +5,6 @@
signature QUICKCHECK_GENERATORS =
sig
- val compile_generator_expr: theory -> term -> int -> term list option
type seed = Random_Engine.seed
val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
-> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
@@ -16,6 +15,7 @@
-> string list -> string list * string list -> typ list * typ list
-> term list * (term * term) list
val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
+ val compile_generator_expr: theory -> term -> int -> term list option
val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
val setup: theory -> theory
end;
@@ -23,42 +23,13 @@
structure Quickcheck_Generators : QUICKCHECK_GENERATORS =
struct
-(** building and compiling generator expressions **)
-
-val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
-
-val target = "Quickcheck";
+(** abstract syntax **)
-fun mk_generator_expr thy prop tys =
- let
- val bound_max = length tys - 1;
- val bounds = map_index (fn (i, ty) =>
- (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
- val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
- val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
- val check = @{term "If :: bool => term list option => term list option => term list option"}
- $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option "} $ terms);
- val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"};
- fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
- fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit => term"});
- fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
- liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
- fun mk_split ty = Sign.mk_const thy
- (@{const_name split}, [ty, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
- fun mk_scomp_split ty t t' =
- 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 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 =
- let
- val tys = (map snd o fst o strip_abs) t;
- val t' = mk_generator_expr thy t tys;
- val f = Code_ML.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
- (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
- in f #> Random_Engine.run end;
+fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
+val size = @{term "i::code_numeral"};
+val size1 = @{term "(i::code_numeral) - 1"};
+val size' = @{term "j::code_numeral"};
+val seed = @{term "s::Random.seed"};
(** typ "'a => 'b" **)
@@ -91,25 +62,22 @@
(** type copies **)
-fun mk_random_typecopy tyco vs constr typ thy =
+fun mk_random_typecopy tyco vs constr T' thy =
let
val Ts = map TFree vs;
val T = Type (tyco, Ts);
- fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
- val Ttm = mk_termifyT T;
- val typtm = mk_termifyT typ;
+ val Tm = termifyT T;
+ val Tm' = termifyT T';
fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
- 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);
+ val t_v = Free (v, Tm');
val t_constr = mk_const constr Ts;
- val lhs = mk_random T $ size;
- val rhs = HOLogic.mk_ST [(((mk_random typ) $ size, @{typ Random.seed}), SOME (v, typtm))]
- (HOLogic.mk_return Ttm @{typ Random.seed}
- (mk_const "Code_Eval.valapp" [typ, T]
+ val lhs = HOLogic.mk_random T size;
+ val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))]
+ (HOLogic.mk_return Tm @{typ Random.seed}
+ (mk_const "Code_Eval.valapp" [T', T]
$ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
- @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
+ @{typ Random.seed} (SOME Tm, @{typ Random.seed});
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in
thy
@@ -122,16 +90,16 @@
fun ensure_random_typecopy tyco thy =
let
- val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
+ val SOME { vs = raw_vs, constr, typ = raw_T, ... } =
Typecopy.get_info thy tyco;
val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
- val typ = map_atyps (fn TFree (v, sort) =>
- TFree (v, constrain sort @{sort random})) raw_typ;
- val vs' = Term.add_tfreesT typ [];
+ val T = map_atyps (fn TFree (v, sort) =>
+ TFree (v, constrain sort @{sort random})) raw_T;
+ val vs' = Term.add_tfreesT T [];
val vs = map (fn (v, sort) =>
(v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
- val do_inst = Sign.of_sort thy (typ, @{sort random});
- in if do_inst then mk_random_typecopy tyco vs constr typ thy else thy end;
+ val can_inst = Sign.of_sort thy (T, @{sort random});
+ in if can_inst then mk_random_typecopy tyco vs constr T thy else thy end;
(** datatypes **)
@@ -258,12 +226,7 @@
fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
let
val mk_const = curry (Sign.mk_const thy);
- val i = @{term "i\<Colon>code_numeral"};
- val i1 = @{term "(i\<Colon>code_numeral) - 1"};
- val j = @{term "j\<Colon>code_numeral"};
- val seed = @{term "s\<Colon>Random.seed"};
val random_auxsN = map (prefix (random_auxN ^ "_")) (names @ auxnames);
- fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"});
val rTs = Ts @ Us;
fun random_resultT T = @{typ Random.seed}
--> HOLogic.mk_prodT (termifyT T,@{typ Random.seed});
@@ -272,7 +235,7 @@
val random_auxT = sizeT o random_resultT;
val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT))
random_auxsN rTs;
- fun mk_random_call T = (NONE, (HOLogic.mk_random T j, T));
+ fun mk_random_call T = (NONE, (HOLogic.mk_random T size', T));
fun mk_random_aux_call fTs (k, _) (tyco, Ts) =
let
val T = Type (tyco, Ts);
@@ -280,7 +243,7 @@
| mk_random_fun_lift (fT :: fTs) t =
mk_const @{const_name random_fun_lift} [fTs ---> T, fT] $
mk_random_fun_lift fTs t;
- val t = mk_random_fun_lift fTs (nth random_auxs k $ i1 $ j);
+ val t = mk_random_fun_lift fTs (nth random_auxs k $ size1 $ size');
val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k)
|> the_default 0;
in (SOME size, (t, fTs ---> T)) end;
@@ -300,9 +263,9 @@
val t = HOLogic.mk_ST (map (fn (t, _) => (t, @{typ Random.seed})) tTs ~~ map SOME vs')
tc @{typ Random.seed} (SOME T, @{typ Random.seed});
val tk = if is_rec
- then if k = 0 then i
+ then if k = 0 then size
else @{term "Quickcheck.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
- $ HOLogic.mk_number @{typ code_numeral} k $ i
+ $ HOLogic.mk_number @{typ code_numeral} k $ size
else @{term "1::code_numeral"}
in (is_rec, HOLogic.mk_prod (tk, t)) end;
fun sort_rec xs =
@@ -316,24 +279,23 @@
$ (mk_const @{const_name Random.select_weight} [random_resultT rT]
$ HOLogic.mk_list (HOLogic.mk_prodT (@{typ code_numeral}, random_resultT rT)) xs)
$ seed;
- val auxs_lhss = map (fn t => t $ i $ j $ seed) random_auxs;
+ val auxs_lhss = map (fn t => t $ size $ size' $ seed) random_auxs;
val auxs_rhss = map mk_select gen_exprss;
in (random_auxs, auxs_lhss ~~ auxs_rhss) end;
fun mk_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
val _ = DatatypeAux.message config "Creating quickcheck generators ...";
- val i = @{term "i\<Colon>code_numeral"};
val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k
- of SOME (_, l) => if l = 0 then i
+ of SOME (_, l) => if l = 0 then size
else @{term "max :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
- $ HOLogic.mk_number @{typ code_numeral} l $ i
- | NONE => i;
+ $ HOLogic.mk_number @{typ code_numeral} l $ size
+ | NONE => size;
val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq
(mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us));
val random_defs = map_index (fn (k, T) => mk_prop_eq
- (HOLogic.mk_random T i, nth random_auxs k $ mk_size_arg k $ i)) Ts;
+ (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
in
thy
|> TheoryTarget.instantiation (tycos, vs, @{sort random})
@@ -381,11 +343,49 @@
end;
+(** building and compiling generator expressions **)
+
+val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
+
+val target = "Quickcheck";
+
+fun mk_generator_expr thy prop Ts =
+ let
+ val bound_max = length Ts - 1;
+ val bounds = map_index (fn (i, ty) =>
+ (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
+ val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
+ val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
+ val check = @{term "If :: bool => term list option => term list option => term list option"}
+ $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option "} $ terms);
+ val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"};
+ fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+ fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
+ fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
+ liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
+ fun mk_split T = Sign.mk_const thy
+ (@{const_name split}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
+ fun mk_scomp_split T t t' =
+ mk_scomp (mk_termtyp T) @{typ "term list option"} @{typ Random.seed} t
+ (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
+ fun mk_bindclause (_, _, i, T) = mk_scomp_split T
+ (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
+ in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
+
+fun compile_generator_expr thy t =
+ let
+ val Ts = (map snd o fst o strip_abs) t;
+ val t' = mk_generator_expr thy t Ts;
+ val compile = Code_ML.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
+ (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+ in compile #> Random_Engine.run end;
+
+
(** setup **)
-val setup = Code_Target.extend_target (target, (Code_ML.target_Eval, K I))
- #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of)
- #> Typecopy.interpretation ensure_random_typecopy
- #> Datatype.interpretation ensure_random_datatype;
+val setup = Typecopy.interpretation ensure_random_typecopy
+ #> Datatype.interpretation ensure_random_datatype
+ #> Code_Target.extend_target (target, (Code_ML.target_Eval, K I))
+ #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of);
end;