# HG changeset patch
# User berghofe
# Date 1210150764 -7200
# Node ID b3e8d5ec721dfc8eb7e8e7c1ffe0f842491daf96
# Parent  6a4d5ca6d2e5ccc4247d5ad4e271d00e43ab861a
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
definitions of + and * on functions.

diff -r 6a4d5ca6d2e5 -r b3e8d5ec721d src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Wed May 07 10:59:23 2008 +0200
+++ b/src/HOL/Library/BigO.thy	Wed May 07 10:59:24 2008 +0200
@@ -99,8 +99,8 @@
   done
 
 lemma bigo_plus_self_subset [intro]: 
-  "O(f) + O(f) <= O(f)"
-  apply (auto simp add: bigo_alt_def set_plus)
+  "O(f) \<oplus> O(f) <= O(f)"
+  apply (auto simp add: bigo_alt_def set_plus_def)
   apply (rule_tac x = "c + ca" in exI)
   apply auto
   apply (simp add: ring_distribs func_plus)
@@ -111,16 +111,16 @@
   apply force
 done
 
-lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
+lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)"
   apply (rule equalityI)
   apply (rule bigo_plus_self_subset)
   apply (rule set_zero_plus2) 
   apply (rule bigo_zero)
   done
 
-lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
+lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)"
   apply (rule subsetI)
-  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus)
+  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
   apply (subst bigo_pos_const [symmetric])+
   apply (rule_tac x = 
     "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
@@ -170,18 +170,18 @@
   apply (auto simp add: if_splits linorder_not_le)
   done
 
-lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"
-  apply (subgoal_tac "A + B <= O(f) + O(f)")
+lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"
+  apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)")
   apply (erule order_trans)
   apply simp
   apply (auto del: subsetI simp del: bigo_plus_idemp)
   done
 
 lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
-    O(f + g) = O(f) + O(g)"
+    O(f + g) = O(f) \<oplus> O(g)"
   apply (rule equalityI)
   apply (rule bigo_plus_subset)
-  apply (simp add: bigo_alt_def set_plus func_plus)
+  apply (simp add: bigo_alt_def set_plus_def func_plus)
   apply clarify
   apply (rule_tac x = "max c ca" in exI)
   apply (rule conjI)
@@ -232,7 +232,7 @@
     f : lb +o O(g)"
   apply (rule set_minus_imp_plus)
   apply (rule bigo_bounded)
-  apply (auto simp add: diff_minus func_minus func_plus)
+  apply (auto simp add: diff_minus fun_Compl_def func_plus)
   apply (drule_tac x = x in spec)+
   apply force
   apply (drule_tac x = x in spec)+
@@ -265,7 +265,7 @@
     (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
   apply (drule set_plus_imp_minus)
   apply (rule set_minus_imp_plus)
-  apply (subst func_diff)
+  apply (subst fun_diff_def)
 proof -
   assume a: "f - g : O(h)"
   have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
@@ -279,7 +279,7 @@
     done
   also have "... <= O(f - g)"
     apply (rule bigo_elt_subset)
-    apply (subst func_diff)
+    apply (subst fun_diff_def)
     apply (rule bigo_abs)
     done
   also from a have "... <= O(h)"
@@ -290,12 +290,12 @@
 lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" 
   by (unfold bigo_def, auto)
 
-lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)"
+lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)"
 proof -
   assume "f : g +o O(h)"
-  also have "... <= O(g) + O(h)"
+  also have "... <= O(g) \<oplus> O(h)"
     by (auto del: subsetI)
-  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
+  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
     apply (subst bigo_abs3 [symmetric])+
     apply (rule refl)
     done
@@ -304,16 +304,16 @@
   finally have "f : ...".
   then have "O(f) <= ..."
     by (elim bigo_elt_subset)
-  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
+  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
     by (rule bigo_plus_eq, auto)
   finally show ?thesis
     by (simp add: bigo_abs3 [symmetric])
 qed
 
-lemma bigo_mult [intro]: "O(f)*O(g) <= O(f * g)"
+lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
   apply (rule subsetI)
   apply (subst bigo_def)
-  apply (auto simp add: bigo_alt_def set_times func_times)
+  apply (auto simp add: bigo_alt_def set_times_def func_times)
   apply (rule_tac x = "c * ca" in exI)
   apply(rule allI)
   apply(erule_tac x = x in allE)+
@@ -389,7 +389,7 @@
   done
 
 lemma bigo_mult7: "ALL x. f x ~= 0 ==>
-    O(f * g) <= O(f::'a => ('b::ordered_field)) * O(g)"
+    O(f * g) <= O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
   apply (subst bigo_mult6)
   apply assumption
   apply (rule set_times_mono3)
@@ -397,14 +397,14 @@
   done
 
 lemma bigo_mult8: "ALL x. f x ~= 0 ==>
-    O(f * g) = O(f::'a => ('b::ordered_field)) * O(g)"
+    O(f * g) = O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
   apply (rule equalityI)
   apply (erule bigo_mult7)
   apply (rule bigo_mult)
   done
 
 lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
-  by (auto simp add: bigo_def func_minus)
+  by (auto simp add: bigo_def fun_Compl_def)
 
 lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
   apply (rule set_minus_imp_plus)
@@ -414,7 +414,7 @@
   done
 
 lemma bigo_minus3: "O(-f) = O(f)"
-  by (auto simp add: bigo_def func_minus abs_minus_cancel)
+  by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
 
 lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
 proof -
@@ -422,9 +422,9 @@
   show "f +o O(g) <= O(g)"
   proof -
     have "f : O(f)" by auto
-    then have "f +o O(g) <= O(f) + O(g)"
+    then have "f +o O(g) <= O(f) \<oplus> O(g)"
       by (auto del: subsetI)
-    also have "... <= O(g) + O(g)"
+    also have "... <= O(g) \<oplus> O(g)"
     proof -
       from a have "O(f) <= O(g)" by (auto del: subsetI)
       thus ?thesis by (auto del: subsetI)
@@ -566,7 +566,7 @@
 
 lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o 
     O(%x. h(k x))"
-  apply (simp only: set_minus_plus [symmetric] diff_minus func_minus
+  apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
       func_plus)
   apply (erule bigo_compose1)
 done
@@ -635,11 +635,11 @@
       (%x. SUM y : A x. l x y * g(k x y)) +o
         O(%x. SUM y : A x. abs(l x y * h(k x y)))"
   apply (rule set_minus_imp_plus)
-  apply (subst func_diff)
+  apply (subst fun_diff_def)
   apply (subst setsum_subtractf [symmetric])
   apply (subst right_diff_distrib [symmetric])
   apply (rule bigo_setsum3)
-  apply (subst func_diff [symmetric])
+  apply (subst fun_diff_def [symmetric])
   apply (erule set_plus_imp_minus)
   done
 
@@ -664,11 +664,11 @@
         (%x. SUM y : A x. (l x y) * g(k x y)) +o
           O(%x. SUM y : A x. (l x y) * h(k x y))" 
   apply (rule set_minus_imp_plus)
-  apply (subst func_diff)
+  apply (subst fun_diff_def)
   apply (subst setsum_subtractf [symmetric])
   apply (subst right_diff_distrib [symmetric])
   apply (rule bigo_setsum5)
-  apply (subst func_diff [symmetric])
+  apply (subst fun_diff_def [symmetric])
   apply (drule set_plus_imp_minus)
   apply auto
   done
@@ -677,7 +677,7 @@
 subsection {* Misc useful stuff *}
 
 lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
-  A + B <= O(f)"
+  A \<oplus> B <= O(f)"
   apply (subst bigo_plus_idemp [symmetric])
   apply (rule set_plus_mono2)
   apply assumption+
@@ -723,11 +723,11 @@
        f 0 = g 0 ==> f =o g +o O(h)"
   apply (rule set_minus_imp_plus)
   apply (rule bigo_fix)
-  apply (subst func_diff)
-  apply (subst func_diff [symmetric])
+  apply (subst fun_diff_def)
+  apply (subst fun_diff_def [symmetric])
   apply (rule set_plus_imp_minus)
   apply simp
-  apply (simp add: func_diff)
+  apply (simp add: fun_diff_def)
   done
 
 
@@ -794,7 +794,7 @@
   apply (rule allI)
   apply (rule le_maxI2)
   apply (rule allI)
-  apply (subst func_diff)
+  apply (subst fun_diff_def)
   apply (case_tac "0 <= k x - g x")
   apply simp
   apply (subst abs_of_nonneg)
@@ -818,7 +818,7 @@
   apply (rule allI)
   apply (rule le_maxI2)
   apply (rule allI)
-  apply (subst func_diff)
+  apply (subst fun_diff_def)
   apply (case_tac "0 <= f x - k x")
   apply simp
   apply (subst abs_of_nonneg)
@@ -839,12 +839,12 @@
   apply (unfold lesso_def)
   apply (drule set_plus_imp_minus)
   apply (drule bigo_abs5) back
-  apply (simp add: func_diff)
+  apply (simp add: fun_diff_def)
   apply (drule bigo_useful_add)
   apply assumption
   apply (erule bigo_lesseq2) back
   apply (rule allI)
-  apply (auto simp add: func_plus func_diff compare_rls 
+  apply (auto simp add: func_plus fun_diff_def compare_rls 
     split: split_max abs_split)
   done
 
diff -r 6a4d5ca6d2e5 -r b3e8d5ec721d src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Wed May 07 10:59:23 2008 +0200
+++ b/src/HOL/Library/SetsAndFunctions.thy	Wed May 07 10:59:24 2008 +0200
@@ -17,15 +17,9 @@
 
 subsection {* Basic definitions *}
 
-instantiation set :: (plus) plus
-begin
-
 definition
-  set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}"
-
-instance ..
-
-end
+  set_plus :: "('a::plus) set => 'a set => 'a set"  (infixl "\<oplus>" 65) where
+  "A \<oplus> B == {c. EX a:A. EX b:B. c = a + b}"
 
 instantiation "fun" :: (type, plus) plus
 begin
@@ -37,15 +31,9 @@
 
 end
 
-instantiation set :: (times) times
-begin
-
 definition
-  set_times:"A * B == {c. EX a:A. EX b:B. c = a * b}"
-
-instance ..
-
-end
+  set_times :: "('a::times) set => 'a set => 'a set"  (infixl "\<otimes>" 70) where
+  "A \<otimes> B == {c. EX a:A. EX b:B. c = a * b}"
 
 instantiation "fun" :: (type, times) times
 begin
@@ -57,36 +45,6 @@
 
 end
 
-instantiation "fun" :: (type, minus) minus
-begin
-
-definition
-  func_diff: "f - g == %x. f x - g x"
-
-instance ..
-
-end
-
-instantiation "fun" :: (type, uminus) uminus
-begin
-
-definition
-  func_minus: "- f == (%x. - f x)"
-
-instance ..
-
-end
-
-
-instantiation set :: (zero) zero
-begin
-
-definition
-  set_zero: "0::('a::zero)set == {0}"
-
-instance ..
-
-end
 
 instantiation "fun" :: (type, zero) zero
 begin
@@ -98,16 +56,6 @@
 
 end
 
-instantiation set :: (one) one
-begin
-
-definition
-  set_one: "1::('a::one)set == {1}"
-
-instance ..
-
-end
-
 instantiation "fun" :: (type, one) one
 begin
 
@@ -138,8 +86,8 @@
 
 instance "fun" :: (type,ab_group_add)ab_group_add
   apply default
-   apply (simp add: func_minus func_plus func_zero)
-  apply (simp add: func_minus func_plus func_diff diff_minus)
+   apply (simp add: fun_Compl_def func_plus func_zero)
+  apply (simp add: fun_Compl_def func_plus fun_diff_def diff_minus)
   done
 
 instance "fun" :: (type,semigroup_mult)semigroup_mult
@@ -154,52 +102,50 @@
 
 instance "fun" :: (type,comm_ring_1)comm_ring_1
   apply default
-   apply (auto simp add: func_plus func_times func_minus func_diff ext
+   apply (auto simp add: func_plus func_times fun_Compl_def fun_diff_def ext
      func_one func_zero ring_simps)
   apply (drule fun_cong)
   apply simp
   done
 
-instance set :: (semigroup_add)semigroup_add
+interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
   apply default
-  apply (unfold set_plus)
+  apply (unfold set_plus_def)
   apply (force simp add: add_assoc)
   done
 
-instance set :: (semigroup_mult)semigroup_mult
+interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
   apply default
-  apply (unfold set_times)
+  apply (unfold set_times_def)
   apply (force simp add: mult_assoc)
   done
 
-instance set :: (comm_monoid_add)comm_monoid_add
+interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
   apply default
-   apply (unfold set_plus)
+   apply (unfold set_plus_def)
    apply (force simp add: add_ac)
-  apply (unfold set_zero)
   apply force
   done
 
-instance set :: (comm_monoid_mult)comm_monoid_mult
+interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
   apply default
-   apply (unfold set_times)
+   apply (unfold set_times_def)
    apply (force simp add: mult_ac)
-  apply (unfold set_one)
   apply force
   done
 
 
 subsection {* Basic properties *}
 
-lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
-  by (auto simp add: set_plus)
+lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
+  by (auto simp add: set_plus_def)
 
 lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
   by (auto simp add: elt_set_plus_def)
 
-lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) +
-    (b +o D) = (a + b) +o (C + D)"
-  apply (auto simp add: elt_set_plus_def set_plus add_ac)
+lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
+    (b +o D) = (a + b) +o (C \<oplus> D)"
+  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
    apply (rule_tac x = "ba + bb" in exI)
   apply (auto simp add: add_ac)
   apply (rule_tac x = "aa + a" in exI)
@@ -210,9 +156,9 @@
     (a + b) +o C"
   by (auto simp add: elt_set_plus_def add_assoc)
 
-lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C =
-    a +o (B + C)"
-  apply (auto simp add: elt_set_plus_def set_plus)
+lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
+    a +o (B \<oplus> C)"
+  apply (auto simp add: elt_set_plus_def set_plus_def)
    apply (blast intro: add_ac)
   apply (rule_tac x = "a + aa" in exI)
   apply (rule conjI)
@@ -222,9 +168,9 @@
    apply (auto simp add: add_ac)
   done
 
-theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) =
-    a +o (C + D)"
-  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus add_ac)
+theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
+    a +o (C \<oplus> D)"
+  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
    apply (rule_tac x = "aa + ba" in exI)
    apply (auto simp add: add_ac)
   done
@@ -236,17 +182,17 @@
   by (auto simp add: elt_set_plus_def)
 
 lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
-    C + E <= D + F"
-  by (auto simp add: set_plus)
+    C \<oplus> E <= D \<oplus> F"
+  by (auto simp add: set_plus_def)
 
-lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C + D"
-  by (auto simp add: elt_set_plus_def set_plus)
+lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
+  by (auto simp add: elt_set_plus_def set_plus_def)
 
 lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
-    a +o D <= D + C"
-  by (auto simp add: elt_set_plus_def set_plus add_ac)
+    a +o D <= D \<oplus> C"
+  by (auto simp add: elt_set_plus_def set_plus_def add_ac)
 
-lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C + D"
+lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
   apply (subgoal_tac "a +o B <= a +o D")
    apply (erule order_trans)
    apply (erule set_plus_mono3)
@@ -259,21 +205,21 @@
   apply auto
   done
 
-lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==>
-    x : D + F"
+lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
+    x : D \<oplus> F"
   apply (frule set_plus_mono2)
    prefer 2
    apply force
   apply assumption
   done
 
-lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C + D"
+lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
   apply (frule set_plus_mono3)
   apply auto
   done
 
 lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
-    x : a +o D ==> x : D + C"
+    x : a +o D ==> x : D \<oplus> C"
   apply (frule set_plus_mono4)
   apply auto
   done
@@ -281,8 +227,8 @@
 lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
   by (auto simp add: elt_set_plus_def)
 
-lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A + B"
-  apply (auto intro!: subsetI simp add: set_plus)
+lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
+  apply (auto intro!: subsetI simp add: set_plus_def)
   apply (rule_tac x = 0 in bexI)
    apply (rule_tac x = x in bexI)
     apply (auto simp add: add_ac)
@@ -302,15 +248,15 @@
   by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
     assumption)
 
-lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
-  by (auto simp add: set_times)
+lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
+  by (auto simp add: set_times_def)
 
 lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
   by (auto simp add: elt_set_times_def)
 
-lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) *
-    (b *o D) = (a * b) *o (C * D)"
-  apply (auto simp add: elt_set_times_def set_times)
+lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
+    (b *o D) = (a * b) *o (C \<otimes> D)"
+  apply (auto simp add: elt_set_times_def set_times_def)
    apply (rule_tac x = "ba * bb" in exI)
    apply (auto simp add: mult_ac)
   apply (rule_tac x = "aa * a" in exI)
@@ -321,9 +267,9 @@
     (a * b) *o C"
   by (auto simp add: elt_set_times_def mult_assoc)
 
-lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C =
-    a *o (B * C)"
-  apply (auto simp add: elt_set_times_def set_times)
+lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
+    a *o (B \<otimes> C)"
+  apply (auto simp add: elt_set_times_def set_times_def)
    apply (blast intro: mult_ac)
   apply (rule_tac x = "a * aa" in exI)
   apply (rule conjI)
@@ -333,9 +279,9 @@
    apply (auto simp add: mult_ac)
   done
 
-theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) =
-    a *o (C * D)"
-  apply (auto intro!: subsetI simp add: elt_set_times_def set_times
+theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
+    a *o (C \<otimes> D)"
+  apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
     mult_ac)
    apply (rule_tac x = "aa * ba" in exI)
    apply (auto simp add: mult_ac)
@@ -348,17 +294,17 @@
   by (auto simp add: elt_set_times_def)
 
 lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
-    C * E <= D * F"
-  by (auto simp add: set_times)
+    C \<otimes> E <= D \<otimes> F"
+  by (auto simp add: set_times_def)
 
-lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C * D"
-  by (auto simp add: elt_set_times_def set_times)
+lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
+  by (auto simp add: elt_set_times_def set_times_def)
 
 lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
-    a *o D <= D * C"
-  by (auto simp add: elt_set_times_def set_times mult_ac)
+    a *o D <= D \<otimes> C"
+  by (auto simp add: elt_set_times_def set_times_def mult_ac)
 
-lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C * D"
+lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
   apply (subgoal_tac "a *o B <= a *o D")
    apply (erule order_trans)
    apply (erule set_times_mono3)
@@ -371,21 +317,21 @@
   apply auto
   done
 
-lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==>
-    x : D * F"
+lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
+    x : D \<otimes> F"
   apply (frule set_times_mono2)
    prefer 2
    apply force
   apply assumption
   done
 
-lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C * D"
+lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
   apply (frule set_times_mono3)
   apply auto
   done
 
 lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
-    x : a *o D ==> x : D * C"
+    x : a *o D ==> x : D \<otimes> C"
   apply (frule set_times_mono4)
   apply auto
   done
@@ -397,19 +343,19 @@
     (a * b) +o (a *o C)"
   by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
 
-lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
-    (a *o B) + (a *o C)"
-  apply (auto simp add: set_plus elt_set_times_def ring_distribs)
+lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
+    (a *o B) \<oplus> (a *o C)"
+  apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
    apply blast
   apply (rule_tac x = "b + bb" in exI)
   apply (auto simp add: ring_distribs)
   done
 
-lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
-    a *o D + C * D"
+lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
+    a *o D \<oplus> C \<otimes> D"
   apply (auto intro!: subsetI simp add:
-    elt_set_plus_def elt_set_times_def set_times
-    set_plus ring_distribs)
+    elt_set_plus_def elt_set_times_def set_times_def
+    set_plus_def ring_distribs)
   apply auto
   done
 
diff -r 6a4d5ca6d2e5 -r b3e8d5ec721d src/HOL/MetisExamples/BigO.thy
--- a/src/HOL/MetisExamples/BigO.thy	Wed May 07 10:59:23 2008 +0200
+++ b/src/HOL/MetisExamples/BigO.thy	Wed May 07 10:59:24 2008 +0200
@@ -266,24 +266,24 @@
 done
 
 lemma bigo_plus_self_subset [intro]: 
-  "O(f) + O(f) <= O(f)"
-  apply (auto simp add: bigo_alt_def set_plus)
+  "O(f) \<oplus> O(f) <= O(f)"
+  apply (auto simp add: bigo_alt_def set_plus_def)
   apply (rule_tac x = "c + ca" in exI)
   apply auto
   apply (simp add: ring_distribs func_plus)
   apply (blast intro:order_trans abs_triangle_ineq add_mono elim:) 
 done
 
-lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
+lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)"
   apply (rule equalityI)
   apply (rule bigo_plus_self_subset)
   apply (rule set_zero_plus2) 
   apply (rule bigo_zero)
 done
 
-lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
+lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)"
   apply (rule subsetI)
-  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus)
+  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
   apply (subst bigo_pos_const [symmetric])+
   apply (rule_tac x = 
     "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
@@ -330,8 +330,8 @@
   apply (auto simp add: if_splits linorder_not_le)
 done
 
-lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"
-  apply (subgoal_tac "A + B <= O(f) + O(f)")
+lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"
+  apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)")
   apply (erule order_trans)
   apply simp
   apply (auto del: subsetI simp del: bigo_plus_idemp)
@@ -339,10 +339,10 @@
 
 ML_command{*ResAtp.problem_name := "BigO__bigo_plus_eq"*}
 lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
-  O(f + g) = O(f) + O(g)"
+  O(f + g) = O(f) \<oplus> O(g)"
   apply (rule equalityI)
   apply (rule bigo_plus_subset)
-  apply (simp add: bigo_alt_def set_plus func_plus)
+  apply (simp add: bigo_alt_def set_plus_def func_plus)
   apply clarify 
 (*sledgehammer*); 
   apply (rule_tac x = "max c ca" in exI)
@@ -478,7 +478,7 @@
     f : lb +o O(g)"
   apply (rule set_minus_imp_plus)
   apply (rule bigo_bounded)
-  apply (auto simp add: diff_minus func_minus func_plus)
+  apply (auto simp add: diff_minus fun_Compl_def func_plus)
   prefer 2
   apply (drule_tac x = x in spec)+ 
   apply arith (*not clear that it's provable otherwise*) 
@@ -538,7 +538,7 @@
     (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
   apply (drule set_plus_imp_minus)
   apply (rule set_minus_imp_plus)
-  apply (subst func_diff)
+  apply (subst fun_diff_def)
 proof -
   assume a: "f - g : O(h)"
   have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
@@ -552,7 +552,7 @@
     done
   also have "... <= O(f - g)"
     apply (rule bigo_elt_subset)
-    apply (subst func_diff)
+    apply (subst fun_diff_def)
     apply (rule bigo_abs)
     done
   also have "... <= O(h)"
@@ -563,12 +563,12 @@
 lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" 
 by (unfold bigo_def, auto)
 
-lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)"
+lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)"
 proof -
   assume "f : g +o O(h)"
-  also have "... <= O(g) + O(h)"
+  also have "... <= O(g) \<oplus> O(h)"
     by (auto del: subsetI)
-  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
+  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
     apply (subst bigo_abs3 [symmetric])+
     apply (rule refl)
     done
@@ -577,18 +577,18 @@
   finally have "f : ...".
   then have "O(f) <= ..."
     by (elim bigo_elt_subset)
-  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
+  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
     by (rule bigo_plus_eq, auto)
   finally show ?thesis
     by (simp add: bigo_abs3 [symmetric])
 qed
 
 ML_command{*ResAtp.problem_name := "BigO__bigo_mult"*}
-lemma bigo_mult [intro]: "O(f)*O(g) <= O(f * g)"
+lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
   apply (rule subsetI)
   apply (subst bigo_def)
   apply (auto simp del: abs_mult mult_ac
-              simp add: bigo_alt_def set_times func_times)
+              simp add: bigo_alt_def set_times_def func_times)
 (*sledgehammer*); 
   apply (rule_tac x = "c * ca" in exI)
   apply(rule allI)
@@ -722,7 +722,7 @@
 ML_command{*ResAtp.problem_name := "BigO__bigo_mult7"*}
   declare bigo_mult6 [simp]
 lemma bigo_mult7: "ALL x. f x ~= 0 ==>
-    O(f * g) <= O(f::'a => ('b::ordered_field)) * O(g)"
+    O(f * g) <= O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
 (*sledgehammer*)
   apply (subst bigo_mult6)
   apply assumption
@@ -734,11 +734,11 @@
 ML_command{*ResAtp.problem_name := "BigO__bigo_mult8"*}
   declare bigo_mult7[intro!]
 lemma bigo_mult8: "ALL x. f x ~= 0 ==>
-    O(f * g) = O(f::'a => ('b::ordered_field)) * O(g)"
+    O(f * g) = O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
 by (metis bigo_mult bigo_mult7 order_antisym_conv)
 
 lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
-  by (auto simp add: bigo_def func_minus)
+  by (auto simp add: bigo_def fun_Compl_def)
 
 lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
   apply (rule set_minus_imp_plus)
@@ -748,7 +748,7 @@
 done
 
 lemma bigo_minus3: "O(-f) = O(f)"
-  by (auto simp add: bigo_def func_minus abs_minus_cancel)
+  by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
 
 lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
 proof -
@@ -756,9 +756,9 @@
   show "f +o O(g) <= O(g)"
   proof -
     have "f : O(f)" by auto
-    then have "f +o O(g) <= O(f) + O(g)"
+    then have "f +o O(g) <= O(f) \<oplus> O(g)"
       by (auto del: subsetI)
-    also have "... <= O(g) + O(g)"
+    also have "... <= O(g) \<oplus> O(g)"
     proof -
       from a have "O(f) <= O(g)" by (auto del: subsetI)
       thus ?thesis by (auto del: subsetI)
@@ -944,7 +944,7 @@
 
 lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o 
     O(%x. h(k x))"
-  apply (simp only: set_minus_plus [symmetric] diff_minus func_minus
+  apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
       func_plus)
   apply (erule bigo_compose1)
 done
@@ -1007,11 +1007,11 @@
       (%x. SUM y : A x. l x y * g(k x y)) +o
         O(%x. SUM y : A x. abs(l x y * h(k x y)))"
   apply (rule set_minus_imp_plus)
-  apply (subst func_diff)
+  apply (subst fun_diff_def)
   apply (subst setsum_subtractf [symmetric])
   apply (subst right_diff_distrib [symmetric])
   apply (rule bigo_setsum3)
-  apply (subst func_diff [symmetric])
+  apply (subst fun_diff_def [symmetric])
   apply (erule set_plus_imp_minus)
 done
 
@@ -1036,11 +1036,11 @@
         (%x. SUM y : A x. (l x y) * g(k x y)) +o
           O(%x. SUM y : A x. (l x y) * h(k x y))" 
   apply (rule set_minus_imp_plus)
-  apply (subst func_diff)
+  apply (subst fun_diff_def)
   apply (subst setsum_subtractf [symmetric])
   apply (subst right_diff_distrib [symmetric])
   apply (rule bigo_setsum5)
-  apply (subst func_diff [symmetric])
+  apply (subst fun_diff_def [symmetric])
   apply (drule set_plus_imp_minus)
   apply auto
 done
@@ -1048,7 +1048,7 @@
 subsection {* Misc useful stuff *}
 
 lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
-  A + B <= O(f)"
+  A \<oplus> B <= O(f)"
   apply (subst bigo_plus_idemp [symmetric])
   apply (rule set_plus_mono2)
   apply assumption+
@@ -1093,11 +1093,11 @@
        f 0 = g 0 ==> f =o g +o O(h)"
   apply (rule set_minus_imp_plus)
   apply (rule bigo_fix)
-  apply (subst func_diff)
-  apply (subst func_diff [symmetric])
+  apply (subst fun_diff_def)
+  apply (subst fun_diff_def [symmetric])
   apply (rule set_plus_imp_minus)
   apply simp
-  apply (simp add: func_diff)
+  apply (simp add: fun_diff_def)
 done
 
 subsection {* Less than or equal to *}
@@ -1159,7 +1159,7 @@
   apply (rule allI)
   apply (rule le_maxI2)
   apply (rule allI)
-  apply (subst func_diff)
+  apply (subst fun_diff_def)
 apply (erule thin_rl)
 (*sledgehammer*);  
   apply (case_tac "0 <= k x - g x")
@@ -1196,7 +1196,7 @@
   apply (rule allI)
   apply (rule le_maxI2)
   apply (rule allI)
-  apply (subst func_diff)
+  apply (subst fun_diff_def)
 apply (erule thin_rl) 
 (*sledgehammer*); 
   apply (case_tac "0 <= f x - k x")
@@ -1214,12 +1214,12 @@
   apply (unfold lesso_def)
   apply (drule set_plus_imp_minus)
   apply (drule bigo_abs5) back
-  apply (simp add: func_diff)
+  apply (simp add: fun_diff_def)
   apply (drule bigo_useful_add)
   apply assumption
   apply (erule bigo_lesseq2) back
   apply (rule allI)
-  apply (auto simp add: func_plus func_diff compare_rls 
+  apply (auto simp add: func_plus fun_diff_def compare_rls 
     split: split_max abs_split)
 done