--- a/src/HOL/Quickcheck_Random.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Quickcheck_Random.thy Thu Nov 12 09:06:44 2020 +0100
@@ -8,9 +8,6 @@
imports Random Code_Evaluation Enum
begin
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
setup \<open>Code_Target.add_derived_target ("Quickcheck", [(Code_Runtime.target, I)])\<close>
subsection \<open>Catching Match exceptions\<close>
@@ -33,6 +30,10 @@
instantiation bool :: random
begin
+context
+ includes state_combinator_syntax
+begin
+
definition
"random i = Random.range 2 \<circ>\<rightarrow>
(\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
@@ -41,6 +42,8 @@
end
+end
+
instantiation itself :: (typerep) random
begin
@@ -55,6 +58,10 @@
instantiation char :: random
begin
+context
+ includes state_combinator_syntax
+begin
+
definition
"random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
@@ -62,6 +69,8 @@
end
+end
+
instantiation String.literal :: random
begin
@@ -75,6 +84,10 @@
instantiation nat :: random
begin
+context
+ includes state_combinator_syntax
+begin
+
definition random_nat :: "natural \<Rightarrow> Random.seed
\<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
where
@@ -86,9 +99,15 @@
end
+end
+
instantiation int :: random
begin
+context
+ includes state_combinator_syntax
+begin
+
definition
"random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
let j = (if k \<ge> i then int (nat_of_natural (k - i)) else - (int (nat_of_natural (i - k))))
@@ -98,9 +117,15 @@
end
+end
+
instantiation natural :: random
begin
+context
+ includes state_combinator_syntax
+begin
+
definition random_natural :: "natural \<Rightarrow> Random.seed
\<Rightarrow> (natural \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
where
@@ -110,9 +135,15 @@
end
+end
+
instantiation integer :: random
begin
+context
+ includes state_combinator_syntax
+begin
+
definition random_integer :: "natural \<Rightarrow> Random.seed
\<Rightarrow> (integer \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
where
@@ -124,6 +155,8 @@
end
+end
+
subsection \<open>Complex generators\<close>
@@ -153,9 +186,15 @@
text \<open>Towards type copies and datatypes\<close>
+context
+ includes state_combinator_syntax
+begin
+
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
where "collapse f = (f \<circ>\<rightarrow> id)"
+end
+
definition beyond :: "natural \<Rightarrow> natural \<Rightarrow> natural"
where "beyond k l = (if l > k then l else 0)"
@@ -172,6 +211,10 @@
instantiation set :: (random) random
begin
+context
+ includes state_combinator_syntax
+begin
+
fun random_aux_set
where
"random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
@@ -200,6 +243,8 @@
end
+end
+
lemma random_aux_rec:
fixes random_aux :: "natural \<Rightarrow> 'a"
assumes "random_aux 0 = rhs 0"
@@ -223,9 +268,6 @@
code_reserved Quickcheck Random_Generators
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
hide_fact (open) collapse_def beyond_def random_fun_lift_def