# HG changeset patch
# User haftmann
# Date 1264597388 -3600
# Node ID cc1d4c3ca9db4df7a38e390bfc4af4e4e9cec612
# Parent  4b068e52ab3f1152abeca6159aea05fd87bb7303# Parent  5c290f56ebf7bb5b0e1261d4d71f0131c48bc5da
merged

diff -r 4b068e52ab3f -r cc1d4c3ca9db src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Wed Jan 27 11:47:17 2010 +0100
+++ b/src/HOL/Quickcheck.thy	Wed Jan 27 14:03:08 2010 +0100
@@ -126,9 +126,24 @@
   shows "random_aux k = rhs k"
   using assms by (rule code_numeral.induct)
 
-setup {* Quickcheck.setup *}
+use "Tools/quickcheck_generators.ML"
+setup Quickcheck_Generators.setup
+
+
+subsection {* Code setup *}
 
-subsection {* the Random-Predicate Monad *} 
+code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun")
+  -- {* With enough criminal energy this can be abused to derive @{prop False};
+  for this reason we use a distinguished target @{text Quickcheck}
+  not spoiling the regular trusted code generation *}
+
+code_reserved Quickcheck Quickcheck_Generators
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
+
+subsection {* The Random-Predicate Monad *} 
 
 types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
 
@@ -167,24 +182,9 @@
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
   where "map f P = bind P (single o f)"
 
-subsection {* Code setup *}
-
-use "Tools/quickcheck_generators.ML"
-setup {* Quickcheck_Generators.setup *}
-
-code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun")
-  -- {* With enough criminal energy this can be abused to derive @{prop False};
-  for this reason we use a distinguished target @{text Quickcheck}
-  not spoiling the regular trusted code generation *}
-
-code_reserved Quickcheck Quickcheck_Generators
-
 hide (open) fact empty_def single_def bind_def union_def if_randompred_def not_randompred_def Random_def map_def
 hide (open) type randompred
 hide (open) const random collapse beyond random_fun_aux random_fun_lift
   empty single bind union if_randompred not_randompred Random map
 
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
-
 end
diff -r 4b068e52ab3f -r cc1d4c3ca9db src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Wed Jan 27 11:47:17 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Jan 27 14:03:08 2010 +0100
@@ -65,14 +65,14 @@
 
 fun mk_random_typecopy tyco vs constr T' thy =
   let
+    val mk_const = curry (Sign.mk_const thy);
     val Ts = map TFree vs;  
     val T = Type (tyco, Ts);
     val Tm = termifyT T;
     val Tm' = termifyT T';
-    fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
     val v = "x";
     val t_v = Free (v, Tm');
-    val t_constr = mk_const constr Ts;
+    val t_constr = Const (constr, T' --> 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}
diff -r 4b068e52ab3f -r cc1d4c3ca9db src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Jan 27 11:47:17 2010 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Jan 27 14:03:08 2010 +0100
@@ -309,6 +309,25 @@
 apply (blast intro:rtrancl_trans)
 done
 
+lemma Image_closed_trancl:
+  assumes "r `` X \<subseteq> X" shows "r\<^sup>* `` X = X"
+proof -
+  from assms have **: "{y. \<exists>x\<in>X. (x, y) \<in> r} \<subseteq> X" by auto
+  have "\<And>x y. (y, x) \<in> r\<^sup>* \<Longrightarrow> y \<in> X \<Longrightarrow> x \<in> X"
+  proof -
+    fix x y
+    assume *: "y \<in> X"
+    assume "(y, x) \<in> r\<^sup>*"
+    then show "x \<in> X"
+    proof induct
+      case base show ?case by (fact *)
+    next
+      case step with ** show ?case by auto
+    qed
+  qed
+  then show ?thesis by auto
+qed
+
 
 subsection {* Transitive closure *}
 
diff -r 4b068e52ab3f -r cc1d4c3ca9db src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Wed Jan 27 11:47:17 2010 +0100
+++ b/src/HOL/ex/Records.thy	Wed Jan 27 14:03:08 2010 +0100
@@ -334,6 +334,16 @@
   done
 
 
+subsection {* A more complex record expression *}
+
+record ('a, 'b, 'c) bar = bar1 :: 'a
+  bar2 :: 'b
+  bar3 :: 'c
+  bar21 :: "'b \<times> 'a"
+  bar32 :: "'c \<times> 'b"
+  bar31 :: "'c \<times> 'a"
+
+
 subsection {* Some code generation *}
 
 export_code foo1 foo3 foo5 foo10 foo11 in SML file -
diff -r 4b068e52ab3f -r cc1d4c3ca9db src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Wed Jan 27 11:47:17 2010 +0100
+++ b/src/Tools/Code_Generator.thy	Wed Jan 27 14:03:08 2010 +0100
@@ -29,6 +29,7 @@
   #> Code_Haskell.setup
   #> Code_Scala.setup
   #> Nbe.setup
+  #> Quickcheck.setup
 *}
 
 end