# HG changeset patch
# User haftmann
# Date 1242917460 -7200
# Node ID 6f4fb815439abbe297e17e4372d8cc1525596dac
# Parent  0a3a9bd5ca835d2fbecc6fe583f702949cbac022# Parent  87bde6b5f79349491dd89d68fb37438b24dbe0c0
merged

diff -r 0a3a9bd5ca83 -r 6f4fb815439a src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu May 21 15:25:44 2009 +0100
+++ b/src/HOL/Predicate.thy	Thu May 21 16:51:00 2009 +0200
@@ -637,6 +637,7 @@
   and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
   val yield: 'a pred -> ('a * 'a pred) option
   val yieldn: int -> 'a pred -> 'a list * 'a pred
+  val map: ('a -> 'b) -> 'a pred -> 'b pred
 end;
 
 structure Predicate : PREDICATE =
@@ -661,6 +662,8 @@
 
 fun yieldn P = anamorph yield P;
 
+fun map f = @{code map} f;
+
 end;
 *}
 
diff -r 0a3a9bd5ca83 -r 6f4fb815439a src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Thu May 21 15:25:44 2009 +0100
+++ b/src/HOL/Quickcheck.thy	Thu May 21 16:51:00 2009 +0200
@@ -175,6 +175,60 @@
 
 end
 
+subsection {* Type copies *}
+
+setup {*
+let
+
+fun mk_random_typecopy tyco vs constr typ thy =
+  let
+    val Ts = map TFree vs;  
+    val T = Type (tyco, Ts);
+    fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"})
+    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];
+    val size = @{term "k\<Colon>code_numeral"};
+    val v = "x";
+    val t_v = Free (v, typtm);
+    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]
+        $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
+      @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
+    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+  in   
+    thy
+    |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
+    |> `(fn lthy => Syntax.check_term lthy eq)
+    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
+    |> snd
+    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+  end;
+
+fun ensure_random_typecopy tyco thy =
+  let
+    val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
+      TypecopyPackage.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 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;
+
+in
+
+TypecopyPackage.interpretation ensure_random_typecopy
+
+end
+*}
+
 
 no_notation fcomp (infixl "o>" 60)
 no_notation scomp (infixl "o\<rightarrow>" 60)