# HG changeset patch
# User haftmann
# Date 1246946184 -7200
# Node ID 9787769764bb3a128543f676239c974419f21cd5
# Parent  ea8c8bf47ce33e160825e555b6266266fcc98b26# Parent  7300186d745af4479422ba48b79885b74d887d39
merged

diff -r ea8c8bf47ce3 -r 9787769764bb src/HOL/Fun.thy
--- 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
diff -r ea8c8bf47ce3 -r 9787769764bb src/HOL/Inductive.thy
--- 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 =
diff -r ea8c8bf47ce3 -r 9787769764bb src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- 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;
diff -r ea8c8bf47ce3 -r 9787769764bb src/HOL/Tools/quickcheck_generators.ML
--- 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;