removed syntax from monad combinators; renamed mbind to scomp
authorhaftmann
Wed Apr 09 08:10:11 2008 +0200 (2008-04-09)
changeset 26588d83271bfaba5
parent 26587 58fb6e033c00
child 26589 43cb72871897
removed syntax from monad combinators; renamed mbind to scomp
src/HOL/Fun.thy
src/HOL/Library/State_Monad.thy
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Fun.thy	Wed Apr 09 08:10:09 2008 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Apr 09 08:10:11 2008 +0200
     1.3 @@ -82,19 +82,13 @@
     1.4  by (unfold comp_def, blast)
     1.5  
     1.6  
     1.7 -subsection {* The Forward Composition Operator @{text "f \<circ>> g"} *}
     1.8 +subsection {* The Forward Composition Operator @{text fcomp} *}
     1.9  
    1.10  definition
    1.11    fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o>" 60)
    1.12  where
    1.13    "f o> g = (\<lambda>x. g (f x))"
    1.14  
    1.15 -notation (xsymbols)
    1.16 -  fcomp  (infixl "\<circ>>" 60)
    1.17 -
    1.18 -notation (HTML output)
    1.19 -  fcomp  (infixl "\<circ>>" 60)
    1.20 -
    1.21  lemma fcomp_apply:  "(f o> g) x = g (f x)"
    1.22    by (simp add: fcomp_def)
    1.23  
    1.24 @@ -107,6 +101,8 @@
    1.25  lemma fcomp_id [simp]: "f o> id = f"
    1.26    by (simp add: fcomp_def)
    1.27  
    1.28 +no_notation fcomp (infixl "o>" 60)
    1.29 +
    1.30  
    1.31  subsection {* Injectivity and Surjectivity *}
    1.32  
     2.1 --- a/src/HOL/Library/State_Monad.thy	Wed Apr 09 08:10:09 2008 +0200
     2.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Apr 09 08:10:11 2008 +0200
     2.3 @@ -56,29 +56,18 @@
     2.4    we use a set of monad combinators:
     2.5  *}
     2.6  
     2.7 -definition
     2.8 -  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
     2.9 -    (infixl ">>=" 60) where
    2.10 -  "f >>= g = split g \<circ> f"
    2.11 +notation fcomp (infixl ">>" 60)
    2.12 +notation (xsymbols) fcomp (infixl "\<guillemotright>" 60)
    2.13 +notation scomp (infixl ">>=" 60)
    2.14 +notation (xsymbols) scomp (infixl "\<guillemotright>=" 60)
    2.15  
    2.16 -definition
    2.17 -  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    2.18 -    (infixl ">>" 60) where
    2.19 -  "f >> g = g \<circ> f"
    2.20 +abbreviation (input)
    2.21 +  "return \<equiv> Pair"
    2.22  
    2.23  definition
    2.24    run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    2.25    "run f = f"
    2.26  
    2.27 -syntax (xsymbols)
    2.28 -  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    2.29 -    (infixl "\<guillemotright>=" 60)
    2.30 -  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    2.31 -    (infixl "\<guillemotright>" 60)
    2.32 -
    2.33 -abbreviation (input)
    2.34 -  "return \<equiv> Pair"
    2.35 -
    2.36  print_ast_translation {*
    2.37    [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]
    2.38  *}
    2.39 @@ -142,12 +131,12 @@
    2.40  *}
    2.41  
    2.42  lemma
    2.43 -  return_mbind [simp]: "return x \<guillemotright>= f = f x"
    2.44 -  unfolding mbind_def by (simp add: expand_fun_eq)
    2.45 +  return_scomp [simp]: "return x \<guillemotright>= f = f x"
    2.46 +  unfolding scomp_def by (simp add: expand_fun_eq)
    2.47  
    2.48  lemma
    2.49 -  mbind_return [simp]: "x \<guillemotright>= return = x"
    2.50 -  unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
    2.51 +  scomp_return [simp]: "x \<guillemotright>= return = x"
    2.52 +  unfolding scomp_def by (simp add: expand_fun_eq split_Pair)
    2.53  
    2.54  lemma
    2.55    id_fcomp [simp]: "id \<guillemotright> f = f"
    2.56 @@ -158,30 +147,30 @@
    2.57    unfolding fcomp_def by simp
    2.58  
    2.59  lemma
    2.60 -  mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
    2.61 -  unfolding mbind_def by (simp add: split_def expand_fun_eq)
    2.62 +  scomp_scomp [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
    2.63 +  unfolding scomp_def by (simp add: split_def expand_fun_eq)
    2.64  
    2.65  lemma
    2.66 -  mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
    2.67 -  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
    2.68 +  scomp_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
    2.69 +  unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
    2.70  
    2.71  lemma
    2.72 -  fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
    2.73 -  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
    2.74 +  fcomp_scomp [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
    2.75 +  unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
    2.76  
    2.77  lemma
    2.78    fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
    2.79    unfolding fcomp_def o_assoc ..
    2.80  
    2.81 -lemmas monad_simp = run_simp return_mbind mbind_return id_fcomp fcomp_id
    2.82 -  mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
    2.83 +lemmas monad_simp = run_simp return_scomp scomp_return id_fcomp fcomp_id
    2.84 +  scomp_scomp scomp_fcomp fcomp_scomp fcomp_fcomp
    2.85  
    2.86  text {*
    2.87    Evaluation of monadic expressions by force:
    2.88  *}
    2.89  
    2.90  lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
    2.91 -  mbind_def fcomp_def run_def
    2.92 +  scomp_def fcomp_def run_def
    2.93  
    2.94  subsection {* ML abstract operations *}
    2.95  
    2.96 @@ -194,7 +183,7 @@
    2.97  
    2.98  fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
    2.99  
   2.100 -fun mbind T1 T2 sT f g = Const (@{const_name mbind},
   2.101 +fun scomp T1 T2 sT f g = Const (@{const_name scomp},
   2.102    liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   2.103  
   2.104  fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) $ f;
   2.105 @@ -216,7 +205,7 @@
   2.106  syntax
   2.107    "_do" :: "do_expr \<Rightarrow> 'a"
   2.108      ("do _ done" [12] 12)
   2.109 -  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   2.110 +  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   2.111      ("_ <- _;// _" [1000, 13, 12] 12)
   2.112    "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   2.113      ("_;// _" [13, 12] 12)
   2.114 @@ -226,12 +215,12 @@
   2.115      ("_" [12] 12)
   2.116  
   2.117  syntax (xsymbols)
   2.118 -  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   2.119 +  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   2.120      ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
   2.121  
   2.122  translations
   2.123    "_do f" => "CONST run f"
   2.124 -  "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   2.125 +  "_scomp x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   2.126    "_fcomp f g" => "f \<guillemotright> g"
   2.127    "_let x t f" => "CONST Let t (\<lambda>x. f)"
   2.128    "_nil f" => "f"
   2.129 @@ -246,10 +235,10 @@
   2.130          let
   2.131            val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
   2.132          in ((v, dummyT), t) end
   2.133 -  fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) =
   2.134 +  fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
   2.135          let
   2.136            val ((v, ty), g') = dest_abs_eta g;
   2.137 -        in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   2.138 +        in Const ("_scomp", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   2.139      | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
   2.140          Const ("_fcomp", dummyT) $ f $ unfold_monad g
   2.141      | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
     3.1 --- a/src/HOL/Product_Type.thy	Wed Apr 09 08:10:09 2008 +0200
     3.2 +++ b/src/HOL/Product_Type.thy	Wed Apr 09 08:10:11 2008 +0200
     3.3 @@ -699,34 +699,33 @@
     3.4    The composition-uncurry combinator.
     3.5  *}
     3.6  
     3.7 -definition
     3.8 -  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o->" 60)
     3.9 -where
    3.10 -  "f o-> g = (\<lambda>x. split g (f x))"
    3.11 +notation fcomp (infixl "o>" 60)
    3.12  
    3.13 -notation (xsymbols)
    3.14 -  mbind  (infixl "\<circ>\<rightarrow>" 60)
    3.15 +definition
    3.16 +  scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60)
    3.17 +where
    3.18 +  "f o\<rightarrow> g = (\<lambda>x. split g (f x))"
    3.19  
    3.20 -notation (HTML output)
    3.21 -  mbind  (infixl "\<circ>\<rightarrow>" 60)
    3.22 +lemma scomp_apply:  "(f o\<rightarrow> g) x = split g (f x)"
    3.23 +  by (simp add: scomp_def)
    3.24  
    3.25 -lemma mbind_apply:  "(f \<circ>\<rightarrow> g) x = split g (f x)"
    3.26 -  by (simp add: mbind_def)
    3.27 +lemma Pair_scomp: "Pair x o\<rightarrow> f = f x"
    3.28 +  by (simp add: expand_fun_eq scomp_apply)
    3.29  
    3.30 -lemma Pair_mbind: "Pair x \<circ>\<rightarrow> f = f x"
    3.31 -  by (simp add: expand_fun_eq mbind_apply)
    3.32 +lemma scomp_Pair: "x o\<rightarrow> Pair = x"
    3.33 +  by (simp add: expand_fun_eq scomp_apply)
    3.34  
    3.35 -lemma mbind_Pair: "x \<circ>\<rightarrow> Pair = x"
    3.36 -  by (simp add: expand_fun_eq mbind_apply)
    3.37 +lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)"
    3.38 +  by (simp add: expand_fun_eq split_twice scomp_def)
    3.39  
    3.40 -lemma mbind_mbind: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
    3.41 -  by (simp add: expand_fun_eq split_twice mbind_def)
    3.42 +lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)"
    3.43 +  by (simp add: expand_fun_eq scomp_apply fcomp_def split_def)
    3.44  
    3.45 -lemma mbind_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)"
    3.46 -  by (simp add: expand_fun_eq mbind_apply fcomp_def split_def)
    3.47 +lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
    3.48 +  by (simp add: expand_fun_eq scomp_apply fcomp_apply)
    3.49  
    3.50 -lemma fcomp_mbind: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
    3.51 -  by (simp add: expand_fun_eq mbind_apply fcomp_apply)
    3.52 +no_notation fcomp (infixl "o>" 60)
    3.53 +no_notation scomp (infixl "o\<rightarrow>" 60)
    3.54  
    3.55  
    3.56  text {*