# HG changeset patch
# User haftmann
# Date 1605168404 -3600
# Node ID de581f98a3a1efa54f561b1343887b4493853356
# Parent  531a0c44ea3f397eb65c525dfdcfb10e41922d13
bundled syntax for state monad combinators

diff -r 531a0c44ea3f -r de581f98a3a1 NEWS
--- 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 ***
 
diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Library/DAList.thy
--- 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
 
diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Library/FSet.thy
--- 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
diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Library/Multiset.thy
--- 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
diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Library/Open_State_Syntax.thy
--- 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>
 
diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Probability/PMF_Impl.thy
--- 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
diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Product_Type.thy
--- 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 "#->"
 
diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Quickcheck_Random.thy
--- 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
diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Random.thy
--- 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
diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Rat.thy
--- 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
diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Real.thy
--- 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