--- a/NEWS Wed Nov 11 23:06:27 2020 +0100
+++ b/NEWS Thu Nov 12 09:06:44 2020 +0100
@@ -171,6 +171,9 @@
- Use veriT in proof preplay.
- Take adventage of more cores in proof preplay.
+* Syntax for state monad combinators fcomp and scomp is organized in
+bundle state_combinator_syntax. Minor INCOMPATIBILITY.
+
*** FOL ***
--- a/src/HOL/Library/DAList.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Library/DAList.thy Thu Nov 12 09:06:44 2020 +0100
@@ -128,9 +128,6 @@
subsection \<open>Quickcheck generators\<close>
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
definition (in term_syntax)
valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
where "valterm_empty = Code_Evaluation.valtermify empty"
@@ -142,7 +139,11 @@
('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
-fun (in term_syntax) random_aux_alist
+context
+ includes state_combinator_syntax
+begin
+
+fun random_aux_alist
where
"random_aux_alist i j =
(if i = 0 then Pair valterm_empty
@@ -152,6 +153,8 @@
(\<lambda>v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (\<lambda>a. Pair (valterm_update k v a))))),
(1, Pair valterm_empty)]))"
+end
+
instantiation alist :: (random, random) random
begin
@@ -163,9 +166,6 @@
end
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
instantiation alist :: (exhaustive, exhaustive) exhaustive
begin
--- a/src/HOL/Library/FSet.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Library/FSet.thy Thu Nov 12 09:06:44 2020 +0100
@@ -1342,9 +1342,11 @@
no_notation Quickcheck_Exhaustive.orelse (infixr "orelse" 55)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
+instantiation fset :: (random) random
+begin
-instantiation fset :: (random) random
+context
+ includes state_combinator_syntax
begin
fun random_aux_fset :: "natural \<Rightarrow> natural \<Rightarrow> natural \<times> natural \<Rightarrow> ('a fset \<times> (unit \<Rightarrow> term)) \<times> natural \<times> natural" where
@@ -1373,6 +1375,6 @@
end
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+end
end
--- a/src/HOL/Library/Multiset.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Nov 12 09:06:44 2020 +0100
@@ -3539,12 +3539,13 @@
\<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "msetify xs = Code_Evaluation.valtermify mset {\<cdot>} xs"
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
instantiation multiset :: (random) random
begin
+context
+ includes state_combinator_syntax
+begin
+
definition
"Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (msetify xs))"
@@ -3552,8 +3553,7 @@
end
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+end
instantiation multiset :: (full_exhaustive) full_exhaustive
begin
--- a/src/HOL/Library/Open_State_Syntax.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Library/Open_State_Syntax.thy Thu Nov 12 09:06:44 2020 +0100
@@ -8,6 +8,10 @@
imports Main
begin
+context
+ includes state_combinator_syntax
+begin
+
subsection \<open>Motivation\<close>
text \<open>
@@ -55,9 +59,6 @@
again. To achieve this, we use a set of monad combinators:
\<close>
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
text \<open>
Given two transformations \<^term>\<open>f\<close> and \<^term>\<open>g\<close>, they may be
directly composed using the \<^term>\<open>(\<circ>>)\<close> combinator, forming a
@@ -111,6 +112,8 @@
lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
+end
+
subsection \<open>Do-syntax\<close>
--- a/src/HOL/Probability/PMF_Impl.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Probability/PMF_Impl.thy Thu Nov 12 09:06:44 2020 +0100
@@ -539,11 +539,11 @@
(Code_Evaluation.valtermify (+) {\<cdot>} A {\<cdot>}
(Code_Evaluation.valtermify single {\<cdot>} x))"
+instantiation pmf :: (random) random
+begin
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-instantiation pmf :: (random) random
+context
+ includes state_combinator_syntax
begin
definition
@@ -555,8 +555,7 @@
end
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+end
instantiation pmf :: (full_exhaustive) full_exhaustive
begin
--- a/src/HOL/Product_Type.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Product_Type.thy Thu Nov 12 09:06:44 2020 +0100
@@ -771,12 +771,24 @@
text \<open>The composition-uncurry combinator.\<close>
-notation fcomp (infixl "\<circ>>" 60)
-
definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60)
where "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))"
-lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+bundle state_combinator_syntax
+begin
+
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+end
+
+context
+ includes state_combinator_syntax
+begin
+
+lemma scomp_unfold: "(\<circ>\<rightarrow>) = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
by (simp add: fun_eq_iff scomp_def case_prod_unfold)
lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = case_prod g (f x)"
@@ -797,6 +809,8 @@
lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
by (simp add: fun_eq_iff scomp_unfold)
+end
+
code_printing
constant scomp \<rightharpoonup> (Eval) infixl 3 "#->"
--- 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
--- a/src/HOL/Random.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Random.thy Thu Nov 12 09:06:44 2020 +0100
@@ -6,10 +6,6 @@
imports List Groups_List
begin
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-
subsection \<open>Auxiliary functions\<close>
fun log :: "natural \<Rightarrow> natural \<Rightarrow> natural" where
@@ -46,6 +42,10 @@
subsection \<open>Base selectors\<close>
+context
+ includes state_combinator_syntax
+begin
+
fun iterate :: "natural \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
"iterate k f x = (if k = 0 then Pair x else f x \<circ>\<rightarrow> iterate (k - 1) f)"
@@ -134,6 +134,8 @@
fun_eq_iff pick_same [symmetric] less_natural_def)
qed
+end
+
subsection \<open>\<open>ML\<close> interface\<close>
@@ -183,7 +185,4 @@
iterate range select pick select_weight
hide_fact (open) range_def
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
end
--- a/src/HOL/Rat.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Rat.thy Thu Nov 12 09:06:44 2020 +0100
@@ -1004,10 +1004,11 @@
rat \<times> (unit \<Rightarrow> Code_Evaluation.term)"
where [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
+instantiation rat :: random
+begin
-instantiation rat :: random
+context
+ includes state_combinator_syntax
begin
definition
@@ -1020,8 +1021,7 @@
end
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+end
instantiation rat :: exhaustive
begin
--- a/src/HOL/Real.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Real.thy Thu Nov 12 09:06:44 2020 +0100
@@ -1638,10 +1638,11 @@
valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)"
where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
+instantiation real :: random
+begin
-instantiation real :: random
+context
+ includes state_combinator_syntax
begin
definition
@@ -1651,8 +1652,7 @@
end
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+end
instantiation real :: exhaustive
begin