--- 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 *}
--- 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 *}
--- 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
--- 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"
--- 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
--- 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 *}
--- 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
--- 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 *}
--- 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 *}
--- 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 *}