--- 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
--- 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}
--- 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 *}
--- 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 -
--- 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