# HG changeset patch
# User haftmann
# Date 1278655870 -7200
# Node ID 89e16802b6cc187b24339fafaa0c282a190cb223
# Parent  82e0fe8b07ebea37fa43fdd290046a02b5824f40
nicer xsymbol syntax for fcomp and scomp

diff -r 82e0fe8b07eb -r 89e16802b6cc src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Jul 08 17:23:05 2010 +0200
+++ b/src/HOL/Fun.thy	Fri Jul 09 08:11:10 2010 +0200
@@ -95,26 +95,26 @@
 subsection {* The Forward Composition Operator @{text fcomp} *}
 
 definition
-  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o>" 60)
+  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
 where
-  "f o> g = (\<lambda>x. g (f x))"
+  "f \<circ>> g = (\<lambda>x. g (f x))"
 
-lemma fcomp_apply:  "(f o> g) x = g (f x)"
+lemma fcomp_apply [simp]:  "(f \<circ>> g) x = g (f x)"
   by (simp add: fcomp_def)
 
-lemma fcomp_assoc: "(f o> g) o> h = f o> (g o> h)"
+lemma fcomp_assoc: "(f \<circ>> g) \<circ>> h = f \<circ>> (g \<circ>> h)"
   by (simp add: fcomp_def)
 
-lemma id_fcomp [simp]: "id o> g = g"
+lemma id_fcomp [simp]: "id \<circ>> g = g"
   by (simp add: fcomp_def)
 
-lemma fcomp_id [simp]: "f o> id = f"
+lemma fcomp_id [simp]: "f \<circ>> id = f"
   by (simp add: fcomp_def)
 
 code_const fcomp
   (Eval infixl 1 "#>")
 
-no_notation fcomp (infixl "o>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
 
 
 subsection {* Injectivity and Surjectivity *}
diff -r 82e0fe8b07eb -r 89e16802b6cc src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Thu Jul 08 17:23:05 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Fri Jul 09 08:11:10 2010 +0200
@@ -69,21 +69,21 @@
     \<Rightarrow> 'a fset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   [code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\<cdot>} xs"
 
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 instantiation fset :: (random) random
 begin
 
 definition
-  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (setify xs))"
+  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
 
 instance ..
 
 end
 
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 
 subsection {* Lattice instantiation *}
diff -r 82e0fe8b07eb -r 89e16802b6cc src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Jul 08 17:23:05 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Jul 09 08:11:10 2010 +0200
@@ -954,21 +954,21 @@
     \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   [code_unfold]: "bagify xs = Code_Evaluation.valtermify Bag {\<cdot>} xs"
 
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 instantiation multiset :: (random) random
 begin
 
 definition
-  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
+  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
 
 instance ..
 
 end
 
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 hide_const (open) bagify
 
diff -r 82e0fe8b07eb -r 89e16802b6cc src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Thu Jul 08 17:23:05 2010 +0200
+++ b/src/HOL/Library/State_Monad.thy	Fri Jul 09 08:11:10 2010 +0200
@@ -55,23 +55,23 @@
   we use a set of monad combinators:
 *}
 
-notation fcomp (infixl "o>" 60)
-notation (xsymbols) fcomp (infixl "o>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation (xsymbols) fcomp (infixl "\<circ>>" 60)
 notation scomp (infixl "o->" 60)
-notation (xsymbols) scomp (infixl "o\<rightarrow>" 60)
+notation (xsymbols) scomp (infixl "\<circ>\<rightarrow>" 60)
 
 abbreviation (input)
   "return \<equiv> Pair"
 
 text {*
   Given two transformations @{term f} and @{term g}, they
-  may be directly composed using the @{term "op o>"} combinator,
-  forming a forward composition: @{prop "(f o> g) s = f (g s)"}.
+  may be directly composed using the @{term "op \<circ>>"} combinator,
+  forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
 
   After any yielding transformation, we bind the side result
   immediately using a lambda abstraction.  This 
-  is the purpose of the @{term "op o\<rightarrow>"} combinator:
-  @{prop "(f o\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
+  is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator:
+  @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
 
   For queries, the existing @{term "Let"} is appropriate.
 
@@ -141,8 +141,8 @@
 
 translations
   "_do f" => "f"
-  "_scomp x f g" => "f o\<rightarrow> (\<lambda>x. g)"
-  "_fcomp f g" => "f o> g"
+  "_scomp x f g" => "f \<circ>\<rightarrow> (\<lambda>x. g)"
+  "_fcomp f g" => "f \<circ>> g"
   "_let x t f" => "CONST Let t (\<lambda>x. f)"
   "_done f" => "f"
 
diff -r 82e0fe8b07eb -r 89e16802b6cc src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Jul 08 17:23:05 2010 +0200
+++ b/src/HOL/Product_Type.thy	Fri Jul 09 08:11:10 2010 +0200
@@ -791,37 +791,37 @@
   The composition-uncurry combinator.
 *}
 
-notation fcomp (infixl "o>" 60)
+notation fcomp (infixl "\<circ>>" 60)
 
-definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) where
-  "f o\<rightarrow> g = (\<lambda>x. split g (f x))"
+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. prod_case g (f x))"
 
 lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
-  by (simp add: expand_fun_eq scomp_def split_def)
+  by (simp add: expand_fun_eq scomp_def prod_case_unfold)
 
-lemma scomp_apply:  "(f o\<rightarrow> g) x = split g (f x)"
-  by (simp add: scomp_unfold split_def)
+lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = prod_case g (f x)"
+  by (simp add: scomp_unfold prod_case_unfold)
 
-lemma Pair_scomp: "Pair x o\<rightarrow> f = f x"
+lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
   by (simp add: expand_fun_eq scomp_apply)
 
-lemma scomp_Pair: "x o\<rightarrow> Pair = x"
+lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x"
   by (simp add: expand_fun_eq scomp_apply)
 
-lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)"
+lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
   by (simp add: expand_fun_eq scomp_unfold)
 
-lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)"
+lemma scomp_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)"
   by (simp add: expand_fun_eq scomp_unfold fcomp_def)
 
-lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
+lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
   by (simp add: expand_fun_eq scomp_unfold fcomp_apply)
 
 code_const scomp
   (Eval infixl 3 "#->")
 
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 text {*
   @{term prod_fun} --- action of the product functor upon
diff -r 82e0fe8b07eb -r 89e16802b6cc src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Thu Jul 08 17:23:05 2010 +0200
+++ b/src/HOL/Quickcheck.thy	Fri Jul 09 08:11:10 2010 +0200
@@ -7,8 +7,8 @@
 uses ("Tools/quickcheck_generators.ML")
 begin
 
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 
 subsection {* The @{text random} class *}
@@ -23,7 +23,7 @@
 begin
 
 definition
-  "random i = Random.range 2 o\<rightarrow>
+  "random i = Random.range 2 \<circ>\<rightarrow>
     (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
 
 instance ..
@@ -44,7 +44,7 @@
 begin
 
 definition
-  "random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
+  "random _ = Random.select chars \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
 
 instance ..
 
@@ -64,7 +64,7 @@
 begin
 
 definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
-  "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
+  "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
      let n = Code_Numeral.nat_of k
      in (n, \<lambda>_. Code_Evaluation.term_of n)))"
 
@@ -76,7 +76,7 @@
 begin
 
 definition
-  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
+  "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
      let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
      in (j, \<lambda>_. Code_Evaluation.term_of j)))"
 
@@ -110,7 +110,7 @@
 text {* Towards type copies and datatypes *}
 
 definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
-  "collapse f = (f o\<rightarrow> id)"
+  "collapse f = (f \<circ>\<rightarrow> id)"
 
 definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   "beyond k l = (if l > k then l else 0)"
@@ -139,8 +139,8 @@
 
 code_reserved Quickcheck Quickcheck_Generators
 
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 
 subsection {* The Random-Predicate Monad *} 
diff -r 82e0fe8b07eb -r 89e16802b6cc src/HOL/Random.thy
--- a/src/HOL/Random.thy	Thu Jul 08 17:23:05 2010 +0200
+++ b/src/HOL/Random.thy	Fri Jul 09 08:11:10 2010 +0200
@@ -7,8 +7,8 @@
 imports Code_Numeral List
 begin
 
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 
 subsection {* Auxiliary functions *}
@@ -48,12 +48,12 @@
 subsection {* Base selectors *}
 
 fun iterate :: "code_numeral \<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 o\<rightarrow> iterate (k - 1) f)"
+  "iterate k f x = (if k = 0 then Pair x else f x \<circ>\<rightarrow> iterate (k - 1) f)"
 
 definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where
   "range k = iterate (log 2147483561 k)
-      (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
-    o\<rightarrow> (\<lambda>v. Pair (v mod k))"
+      (\<lambda>l. next \<circ>\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
+    \<circ>\<rightarrow> (\<lambda>v. Pair (v mod k))"
 
 lemma range:
   "k > 0 \<Longrightarrow> fst (range k s) < k"
@@ -61,7 +61,7 @@
 
 definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   "select xs = range (Code_Numeral.of_nat (length xs))
-    o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
+    \<circ>\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
      
 lemma select:
   assumes "xs \<noteq> []"
@@ -97,7 +97,7 @@
 
 definition select_weight :: "(code_numeral \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   "select_weight xs = range (listsum (map fst xs))
-   o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
+   \<circ>\<rightarrow> (\<lambda>k. Pair (pick xs k))"
 
 lemma select_weight_member:
   assumes "0 < listsum (map fst xs)"
@@ -184,8 +184,8 @@
   iterate range select pick select_weight
 hide_fact (open) range_def
 
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 end
 
diff -r 82e0fe8b07eb -r 89e16802b6cc src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Thu Jul 08 17:23:05 2010 +0200
+++ b/src/HOL/Rat.thy	Fri Jul 09 08:11:10 2010 +0200
@@ -1114,14 +1114,14 @@
   valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> 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 "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 instantiation rat :: random
 begin
 
 definition
-  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
+  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair (
      let j = Code_Numeral.int_of (denom + 1)
      in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
 
@@ -1129,8 +1129,8 @@
 
 end
 
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 text {* Setup for SML code generator *}
 
diff -r 82e0fe8b07eb -r 89e16802b6cc src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Thu Jul 08 17:23:05 2010 +0200
+++ b/src/HOL/RealDef.thy	Fri Jul 09 08:11:10 2010 +0200
@@ -1743,21 +1743,21 @@
   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 "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 instantiation real :: random
 begin
 
 definition
-  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
+  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
 
 instance ..
 
 end
 
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 text {* Setup for SML code generator *}
 
diff -r 82e0fe8b07eb -r 89e16802b6cc src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Jul 08 17:23:05 2010 +0200
+++ b/src/HOL/Word/Word.thy	Fri Jul 09 08:11:10 2010 +0200
@@ -26,14 +26,14 @@
 
 code_datatype word_of_int
 
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 instantiation word :: ("{len0, typerep}") random
 begin
 
 definition
-  "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) o\<rightarrow> (\<lambda>k. Pair (
+  "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) \<circ>\<rightarrow> (\<lambda>k. Pair (
      let j = word_of_int (Code_Numeral.int_of k) :: 'a word
      in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
 
@@ -41,8 +41,8 @@
 
 end
 
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 
 subsection {* Type conversions and casting *}