Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
authorberghofe
Wed May 07 10:59:24 2008 +0200 (2008-05-07)
changeset 26814b3e8d5ec721d
parent 26813 6a4d5ca6d2e5
child 26815 0cb35f537c91
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
definitions of + and * on functions.
src/HOL/Library/BigO.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/MetisExamples/BigO.thy
     1.1 --- a/src/HOL/Library/BigO.thy	Wed May 07 10:59:23 2008 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Wed May 07 10:59:24 2008 +0200
     1.3 @@ -99,8 +99,8 @@
     1.4    done
     1.5  
     1.6  lemma bigo_plus_self_subset [intro]: 
     1.7 -  "O(f) + O(f) <= O(f)"
     1.8 -  apply (auto simp add: bigo_alt_def set_plus)
     1.9 +  "O(f) \<oplus> O(f) <= O(f)"
    1.10 +  apply (auto simp add: bigo_alt_def set_plus_def)
    1.11    apply (rule_tac x = "c + ca" in exI)
    1.12    apply auto
    1.13    apply (simp add: ring_distribs func_plus)
    1.14 @@ -111,16 +111,16 @@
    1.15    apply force
    1.16  done
    1.17  
    1.18 -lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
    1.19 +lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)"
    1.20    apply (rule equalityI)
    1.21    apply (rule bigo_plus_self_subset)
    1.22    apply (rule set_zero_plus2) 
    1.23    apply (rule bigo_zero)
    1.24    done
    1.25  
    1.26 -lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
    1.27 +lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)"
    1.28    apply (rule subsetI)
    1.29 -  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus)
    1.30 +  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
    1.31    apply (subst bigo_pos_const [symmetric])+
    1.32    apply (rule_tac x = 
    1.33      "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
    1.34 @@ -170,18 +170,18 @@
    1.35    apply (auto simp add: if_splits linorder_not_le)
    1.36    done
    1.37  
    1.38 -lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"
    1.39 -  apply (subgoal_tac "A + B <= O(f) + O(f)")
    1.40 +lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"
    1.41 +  apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)")
    1.42    apply (erule order_trans)
    1.43    apply simp
    1.44    apply (auto del: subsetI simp del: bigo_plus_idemp)
    1.45    done
    1.46  
    1.47  lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
    1.48 -    O(f + g) = O(f) + O(g)"
    1.49 +    O(f + g) = O(f) \<oplus> O(g)"
    1.50    apply (rule equalityI)
    1.51    apply (rule bigo_plus_subset)
    1.52 -  apply (simp add: bigo_alt_def set_plus func_plus)
    1.53 +  apply (simp add: bigo_alt_def set_plus_def func_plus)
    1.54    apply clarify
    1.55    apply (rule_tac x = "max c ca" in exI)
    1.56    apply (rule conjI)
    1.57 @@ -232,7 +232,7 @@
    1.58      f : lb +o O(g)"
    1.59    apply (rule set_minus_imp_plus)
    1.60    apply (rule bigo_bounded)
    1.61 -  apply (auto simp add: diff_minus func_minus func_plus)
    1.62 +  apply (auto simp add: diff_minus fun_Compl_def func_plus)
    1.63    apply (drule_tac x = x in spec)+
    1.64    apply force
    1.65    apply (drule_tac x = x in spec)+
    1.66 @@ -265,7 +265,7 @@
    1.67      (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
    1.68    apply (drule set_plus_imp_minus)
    1.69    apply (rule set_minus_imp_plus)
    1.70 -  apply (subst func_diff)
    1.71 +  apply (subst fun_diff_def)
    1.72  proof -
    1.73    assume a: "f - g : O(h)"
    1.74    have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
    1.75 @@ -279,7 +279,7 @@
    1.76      done
    1.77    also have "... <= O(f - g)"
    1.78      apply (rule bigo_elt_subset)
    1.79 -    apply (subst func_diff)
    1.80 +    apply (subst fun_diff_def)
    1.81      apply (rule bigo_abs)
    1.82      done
    1.83    also from a have "... <= O(h)"
    1.84 @@ -290,12 +290,12 @@
    1.85  lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" 
    1.86    by (unfold bigo_def, auto)
    1.87  
    1.88 -lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)"
    1.89 +lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)"
    1.90  proof -
    1.91    assume "f : g +o O(h)"
    1.92 -  also have "... <= O(g) + O(h)"
    1.93 +  also have "... <= O(g) \<oplus> O(h)"
    1.94      by (auto del: subsetI)
    1.95 -  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
    1.96 +  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
    1.97      apply (subst bigo_abs3 [symmetric])+
    1.98      apply (rule refl)
    1.99      done
   1.100 @@ -304,16 +304,16 @@
   1.101    finally have "f : ...".
   1.102    then have "O(f) <= ..."
   1.103      by (elim bigo_elt_subset)
   1.104 -  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
   1.105 +  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
   1.106      by (rule bigo_plus_eq, auto)
   1.107    finally show ?thesis
   1.108      by (simp add: bigo_abs3 [symmetric])
   1.109  qed
   1.110  
   1.111 -lemma bigo_mult [intro]: "O(f)*O(g) <= O(f * g)"
   1.112 +lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
   1.113    apply (rule subsetI)
   1.114    apply (subst bigo_def)
   1.115 -  apply (auto simp add: bigo_alt_def set_times func_times)
   1.116 +  apply (auto simp add: bigo_alt_def set_times_def func_times)
   1.117    apply (rule_tac x = "c * ca" in exI)
   1.118    apply(rule allI)
   1.119    apply(erule_tac x = x in allE)+
   1.120 @@ -389,7 +389,7 @@
   1.121    done
   1.122  
   1.123  lemma bigo_mult7: "ALL x. f x ~= 0 ==>
   1.124 -    O(f * g) <= O(f::'a => ('b::ordered_field)) * O(g)"
   1.125 +    O(f * g) <= O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
   1.126    apply (subst bigo_mult6)
   1.127    apply assumption
   1.128    apply (rule set_times_mono3)
   1.129 @@ -397,14 +397,14 @@
   1.130    done
   1.131  
   1.132  lemma bigo_mult8: "ALL x. f x ~= 0 ==>
   1.133 -    O(f * g) = O(f::'a => ('b::ordered_field)) * O(g)"
   1.134 +    O(f * g) = O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
   1.135    apply (rule equalityI)
   1.136    apply (erule bigo_mult7)
   1.137    apply (rule bigo_mult)
   1.138    done
   1.139  
   1.140  lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
   1.141 -  by (auto simp add: bigo_def func_minus)
   1.142 +  by (auto simp add: bigo_def fun_Compl_def)
   1.143  
   1.144  lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
   1.145    apply (rule set_minus_imp_plus)
   1.146 @@ -414,7 +414,7 @@
   1.147    done
   1.148  
   1.149  lemma bigo_minus3: "O(-f) = O(f)"
   1.150 -  by (auto simp add: bigo_def func_minus abs_minus_cancel)
   1.151 +  by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
   1.152  
   1.153  lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
   1.154  proof -
   1.155 @@ -422,9 +422,9 @@
   1.156    show "f +o O(g) <= O(g)"
   1.157    proof -
   1.158      have "f : O(f)" by auto
   1.159 -    then have "f +o O(g) <= O(f) + O(g)"
   1.160 +    then have "f +o O(g) <= O(f) \<oplus> O(g)"
   1.161        by (auto del: subsetI)
   1.162 -    also have "... <= O(g) + O(g)"
   1.163 +    also have "... <= O(g) \<oplus> O(g)"
   1.164      proof -
   1.165        from a have "O(f) <= O(g)" by (auto del: subsetI)
   1.166        thus ?thesis by (auto del: subsetI)
   1.167 @@ -566,7 +566,7 @@
   1.168  
   1.169  lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o 
   1.170      O(%x. h(k x))"
   1.171 -  apply (simp only: set_minus_plus [symmetric] diff_minus func_minus
   1.172 +  apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
   1.173        func_plus)
   1.174    apply (erule bigo_compose1)
   1.175  done
   1.176 @@ -635,11 +635,11 @@
   1.177        (%x. SUM y : A x. l x y * g(k x y)) +o
   1.178          O(%x. SUM y : A x. abs(l x y * h(k x y)))"
   1.179    apply (rule set_minus_imp_plus)
   1.180 -  apply (subst func_diff)
   1.181 +  apply (subst fun_diff_def)
   1.182    apply (subst setsum_subtractf [symmetric])
   1.183    apply (subst right_diff_distrib [symmetric])
   1.184    apply (rule bigo_setsum3)
   1.185 -  apply (subst func_diff [symmetric])
   1.186 +  apply (subst fun_diff_def [symmetric])
   1.187    apply (erule set_plus_imp_minus)
   1.188    done
   1.189  
   1.190 @@ -664,11 +664,11 @@
   1.191          (%x. SUM y : A x. (l x y) * g(k x y)) +o
   1.192            O(%x. SUM y : A x. (l x y) * h(k x y))" 
   1.193    apply (rule set_minus_imp_plus)
   1.194 -  apply (subst func_diff)
   1.195 +  apply (subst fun_diff_def)
   1.196    apply (subst setsum_subtractf [symmetric])
   1.197    apply (subst right_diff_distrib [symmetric])
   1.198    apply (rule bigo_setsum5)
   1.199 -  apply (subst func_diff [symmetric])
   1.200 +  apply (subst fun_diff_def [symmetric])
   1.201    apply (drule set_plus_imp_minus)
   1.202    apply auto
   1.203    done
   1.204 @@ -677,7 +677,7 @@
   1.205  subsection {* Misc useful stuff *}
   1.206  
   1.207  lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
   1.208 -  A + B <= O(f)"
   1.209 +  A \<oplus> B <= O(f)"
   1.210    apply (subst bigo_plus_idemp [symmetric])
   1.211    apply (rule set_plus_mono2)
   1.212    apply assumption+
   1.213 @@ -723,11 +723,11 @@
   1.214         f 0 = g 0 ==> f =o g +o O(h)"
   1.215    apply (rule set_minus_imp_plus)
   1.216    apply (rule bigo_fix)
   1.217 -  apply (subst func_diff)
   1.218 -  apply (subst func_diff [symmetric])
   1.219 +  apply (subst fun_diff_def)
   1.220 +  apply (subst fun_diff_def [symmetric])
   1.221    apply (rule set_plus_imp_minus)
   1.222    apply simp
   1.223 -  apply (simp add: func_diff)
   1.224 +  apply (simp add: fun_diff_def)
   1.225    done
   1.226  
   1.227  
   1.228 @@ -794,7 +794,7 @@
   1.229    apply (rule allI)
   1.230    apply (rule le_maxI2)
   1.231    apply (rule allI)
   1.232 -  apply (subst func_diff)
   1.233 +  apply (subst fun_diff_def)
   1.234    apply (case_tac "0 <= k x - g x")
   1.235    apply simp
   1.236    apply (subst abs_of_nonneg)
   1.237 @@ -818,7 +818,7 @@
   1.238    apply (rule allI)
   1.239    apply (rule le_maxI2)
   1.240    apply (rule allI)
   1.241 -  apply (subst func_diff)
   1.242 +  apply (subst fun_diff_def)
   1.243    apply (case_tac "0 <= f x - k x")
   1.244    apply simp
   1.245    apply (subst abs_of_nonneg)
   1.246 @@ -839,12 +839,12 @@
   1.247    apply (unfold lesso_def)
   1.248    apply (drule set_plus_imp_minus)
   1.249    apply (drule bigo_abs5) back
   1.250 -  apply (simp add: func_diff)
   1.251 +  apply (simp add: fun_diff_def)
   1.252    apply (drule bigo_useful_add)
   1.253    apply assumption
   1.254    apply (erule bigo_lesseq2) back
   1.255    apply (rule allI)
   1.256 -  apply (auto simp add: func_plus func_diff compare_rls 
   1.257 +  apply (auto simp add: func_plus fun_diff_def compare_rls 
   1.258      split: split_max abs_split)
   1.259    done
   1.260  
     2.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Wed May 07 10:59:23 2008 +0200
     2.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Wed May 07 10:59:24 2008 +0200
     2.3 @@ -17,15 +17,9 @@
     2.4  
     2.5  subsection {* Basic definitions *}
     2.6  
     2.7 -instantiation set :: (plus) plus
     2.8 -begin
     2.9 -
    2.10  definition
    2.11 -  set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}"
    2.12 -
    2.13 -instance ..
    2.14 -
    2.15 -end
    2.16 +  set_plus :: "('a::plus) set => 'a set => 'a set"  (infixl "\<oplus>" 65) where
    2.17 +  "A \<oplus> B == {c. EX a:A. EX b:B. c = a + b}"
    2.18  
    2.19  instantiation "fun" :: (type, plus) plus
    2.20  begin
    2.21 @@ -37,15 +31,9 @@
    2.22  
    2.23  end
    2.24  
    2.25 -instantiation set :: (times) times
    2.26 -begin
    2.27 -
    2.28  definition
    2.29 -  set_times:"A * B == {c. EX a:A. EX b:B. c = a * b}"
    2.30 -
    2.31 -instance ..
    2.32 -
    2.33 -end
    2.34 +  set_times :: "('a::times) set => 'a set => 'a set"  (infixl "\<otimes>" 70) where
    2.35 +  "A \<otimes> B == {c. EX a:A. EX b:B. c = a * b}"
    2.36  
    2.37  instantiation "fun" :: (type, times) times
    2.38  begin
    2.39 @@ -57,36 +45,6 @@
    2.40  
    2.41  end
    2.42  
    2.43 -instantiation "fun" :: (type, minus) minus
    2.44 -begin
    2.45 -
    2.46 -definition
    2.47 -  func_diff: "f - g == %x. f x - g x"
    2.48 -
    2.49 -instance ..
    2.50 -
    2.51 -end
    2.52 -
    2.53 -instantiation "fun" :: (type, uminus) uminus
    2.54 -begin
    2.55 -
    2.56 -definition
    2.57 -  func_minus: "- f == (%x. - f x)"
    2.58 -
    2.59 -instance ..
    2.60 -
    2.61 -end
    2.62 -
    2.63 -
    2.64 -instantiation set :: (zero) zero
    2.65 -begin
    2.66 -
    2.67 -definition
    2.68 -  set_zero: "0::('a::zero)set == {0}"
    2.69 -
    2.70 -instance ..
    2.71 -
    2.72 -end
    2.73  
    2.74  instantiation "fun" :: (type, zero) zero
    2.75  begin
    2.76 @@ -98,16 +56,6 @@
    2.77  
    2.78  end
    2.79  
    2.80 -instantiation set :: (one) one
    2.81 -begin
    2.82 -
    2.83 -definition
    2.84 -  set_one: "1::('a::one)set == {1}"
    2.85 -
    2.86 -instance ..
    2.87 -
    2.88 -end
    2.89 -
    2.90  instantiation "fun" :: (type, one) one
    2.91  begin
    2.92  
    2.93 @@ -138,8 +86,8 @@
    2.94  
    2.95  instance "fun" :: (type,ab_group_add)ab_group_add
    2.96    apply default
    2.97 -   apply (simp add: func_minus func_plus func_zero)
    2.98 -  apply (simp add: func_minus func_plus func_diff diff_minus)
    2.99 +   apply (simp add: fun_Compl_def func_plus func_zero)
   2.100 +  apply (simp add: fun_Compl_def func_plus fun_diff_def diff_minus)
   2.101    done
   2.102  
   2.103  instance "fun" :: (type,semigroup_mult)semigroup_mult
   2.104 @@ -154,52 +102,50 @@
   2.105  
   2.106  instance "fun" :: (type,comm_ring_1)comm_ring_1
   2.107    apply default
   2.108 -   apply (auto simp add: func_plus func_times func_minus func_diff ext
   2.109 +   apply (auto simp add: func_plus func_times fun_Compl_def fun_diff_def ext
   2.110       func_one func_zero ring_simps)
   2.111    apply (drule fun_cong)
   2.112    apply simp
   2.113    done
   2.114  
   2.115 -instance set :: (semigroup_add)semigroup_add
   2.116 +interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
   2.117    apply default
   2.118 -  apply (unfold set_plus)
   2.119 +  apply (unfold set_plus_def)
   2.120    apply (force simp add: add_assoc)
   2.121    done
   2.122  
   2.123 -instance set :: (semigroup_mult)semigroup_mult
   2.124 +interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
   2.125    apply default
   2.126 -  apply (unfold set_times)
   2.127 +  apply (unfold set_times_def)
   2.128    apply (force simp add: mult_assoc)
   2.129    done
   2.130  
   2.131 -instance set :: (comm_monoid_add)comm_monoid_add
   2.132 +interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
   2.133    apply default
   2.134 -   apply (unfold set_plus)
   2.135 +   apply (unfold set_plus_def)
   2.136     apply (force simp add: add_ac)
   2.137 -  apply (unfold set_zero)
   2.138    apply force
   2.139    done
   2.140  
   2.141 -instance set :: (comm_monoid_mult)comm_monoid_mult
   2.142 +interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
   2.143    apply default
   2.144 -   apply (unfold set_times)
   2.145 +   apply (unfold set_times_def)
   2.146     apply (force simp add: mult_ac)
   2.147 -  apply (unfold set_one)
   2.148    apply force
   2.149    done
   2.150  
   2.151  
   2.152  subsection {* Basic properties *}
   2.153  
   2.154 -lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
   2.155 -  by (auto simp add: set_plus)
   2.156 +lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
   2.157 +  by (auto simp add: set_plus_def)
   2.158  
   2.159  lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
   2.160    by (auto simp add: elt_set_plus_def)
   2.161  
   2.162 -lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) +
   2.163 -    (b +o D) = (a + b) +o (C + D)"
   2.164 -  apply (auto simp add: elt_set_plus_def set_plus add_ac)
   2.165 +lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
   2.166 +    (b +o D) = (a + b) +o (C \<oplus> D)"
   2.167 +  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
   2.168     apply (rule_tac x = "ba + bb" in exI)
   2.169    apply (auto simp add: add_ac)
   2.170    apply (rule_tac x = "aa + a" in exI)
   2.171 @@ -210,9 +156,9 @@
   2.172      (a + b) +o C"
   2.173    by (auto simp add: elt_set_plus_def add_assoc)
   2.174  
   2.175 -lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C =
   2.176 -    a +o (B + C)"
   2.177 -  apply (auto simp add: elt_set_plus_def set_plus)
   2.178 +lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
   2.179 +    a +o (B \<oplus> C)"
   2.180 +  apply (auto simp add: elt_set_plus_def set_plus_def)
   2.181     apply (blast intro: add_ac)
   2.182    apply (rule_tac x = "a + aa" in exI)
   2.183    apply (rule conjI)
   2.184 @@ -222,9 +168,9 @@
   2.185     apply (auto simp add: add_ac)
   2.186    done
   2.187  
   2.188 -theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) =
   2.189 -    a +o (C + D)"
   2.190 -  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus add_ac)
   2.191 +theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
   2.192 +    a +o (C \<oplus> D)"
   2.193 +  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
   2.194     apply (rule_tac x = "aa + ba" in exI)
   2.195     apply (auto simp add: add_ac)
   2.196    done
   2.197 @@ -236,17 +182,17 @@
   2.198    by (auto simp add: elt_set_plus_def)
   2.199  
   2.200  lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
   2.201 -    C + E <= D + F"
   2.202 -  by (auto simp add: set_plus)
   2.203 +    C \<oplus> E <= D \<oplus> F"
   2.204 +  by (auto simp add: set_plus_def)
   2.205  
   2.206 -lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C + D"
   2.207 -  by (auto simp add: elt_set_plus_def set_plus)
   2.208 +lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
   2.209 +  by (auto simp add: elt_set_plus_def set_plus_def)
   2.210  
   2.211  lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
   2.212 -    a +o D <= D + C"
   2.213 -  by (auto simp add: elt_set_plus_def set_plus add_ac)
   2.214 +    a +o D <= D \<oplus> C"
   2.215 +  by (auto simp add: elt_set_plus_def set_plus_def add_ac)
   2.216  
   2.217 -lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C + D"
   2.218 +lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
   2.219    apply (subgoal_tac "a +o B <= a +o D")
   2.220     apply (erule order_trans)
   2.221     apply (erule set_plus_mono3)
   2.222 @@ -259,21 +205,21 @@
   2.223    apply auto
   2.224    done
   2.225  
   2.226 -lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==>
   2.227 -    x : D + F"
   2.228 +lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
   2.229 +    x : D \<oplus> F"
   2.230    apply (frule set_plus_mono2)
   2.231     prefer 2
   2.232     apply force
   2.233    apply assumption
   2.234    done
   2.235  
   2.236 -lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C + D"
   2.237 +lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
   2.238    apply (frule set_plus_mono3)
   2.239    apply auto
   2.240    done
   2.241  
   2.242  lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
   2.243 -    x : a +o D ==> x : D + C"
   2.244 +    x : a +o D ==> x : D \<oplus> C"
   2.245    apply (frule set_plus_mono4)
   2.246    apply auto
   2.247    done
   2.248 @@ -281,8 +227,8 @@
   2.249  lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
   2.250    by (auto simp add: elt_set_plus_def)
   2.251  
   2.252 -lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A + B"
   2.253 -  apply (auto intro!: subsetI simp add: set_plus)
   2.254 +lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
   2.255 +  apply (auto intro!: subsetI simp add: set_plus_def)
   2.256    apply (rule_tac x = 0 in bexI)
   2.257     apply (rule_tac x = x in bexI)
   2.258      apply (auto simp add: add_ac)
   2.259 @@ -302,15 +248,15 @@
   2.260    by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
   2.261      assumption)
   2.262  
   2.263 -lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
   2.264 -  by (auto simp add: set_times)
   2.265 +lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
   2.266 +  by (auto simp add: set_times_def)
   2.267  
   2.268  lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
   2.269    by (auto simp add: elt_set_times_def)
   2.270  
   2.271 -lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) *
   2.272 -    (b *o D) = (a * b) *o (C * D)"
   2.273 -  apply (auto simp add: elt_set_times_def set_times)
   2.274 +lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
   2.275 +    (b *o D) = (a * b) *o (C \<otimes> D)"
   2.276 +  apply (auto simp add: elt_set_times_def set_times_def)
   2.277     apply (rule_tac x = "ba * bb" in exI)
   2.278     apply (auto simp add: mult_ac)
   2.279    apply (rule_tac x = "aa * a" in exI)
   2.280 @@ -321,9 +267,9 @@
   2.281      (a * b) *o C"
   2.282    by (auto simp add: elt_set_times_def mult_assoc)
   2.283  
   2.284 -lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C =
   2.285 -    a *o (B * C)"
   2.286 -  apply (auto simp add: elt_set_times_def set_times)
   2.287 +lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
   2.288 +    a *o (B \<otimes> C)"
   2.289 +  apply (auto simp add: elt_set_times_def set_times_def)
   2.290     apply (blast intro: mult_ac)
   2.291    apply (rule_tac x = "a * aa" in exI)
   2.292    apply (rule conjI)
   2.293 @@ -333,9 +279,9 @@
   2.294     apply (auto simp add: mult_ac)
   2.295    done
   2.296  
   2.297 -theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) =
   2.298 -    a *o (C * D)"
   2.299 -  apply (auto intro!: subsetI simp add: elt_set_times_def set_times
   2.300 +theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
   2.301 +    a *o (C \<otimes> D)"
   2.302 +  apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
   2.303      mult_ac)
   2.304     apply (rule_tac x = "aa * ba" in exI)
   2.305     apply (auto simp add: mult_ac)
   2.306 @@ -348,17 +294,17 @@
   2.307    by (auto simp add: elt_set_times_def)
   2.308  
   2.309  lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
   2.310 -    C * E <= D * F"
   2.311 -  by (auto simp add: set_times)
   2.312 +    C \<otimes> E <= D \<otimes> F"
   2.313 +  by (auto simp add: set_times_def)
   2.314  
   2.315 -lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C * D"
   2.316 -  by (auto simp add: elt_set_times_def set_times)
   2.317 +lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
   2.318 +  by (auto simp add: elt_set_times_def set_times_def)
   2.319  
   2.320  lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
   2.321 -    a *o D <= D * C"
   2.322 -  by (auto simp add: elt_set_times_def set_times mult_ac)
   2.323 +    a *o D <= D \<otimes> C"
   2.324 +  by (auto simp add: elt_set_times_def set_times_def mult_ac)
   2.325  
   2.326 -lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C * D"
   2.327 +lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
   2.328    apply (subgoal_tac "a *o B <= a *o D")
   2.329     apply (erule order_trans)
   2.330     apply (erule set_times_mono3)
   2.331 @@ -371,21 +317,21 @@
   2.332    apply auto
   2.333    done
   2.334  
   2.335 -lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==>
   2.336 -    x : D * F"
   2.337 +lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
   2.338 +    x : D \<otimes> F"
   2.339    apply (frule set_times_mono2)
   2.340     prefer 2
   2.341     apply force
   2.342    apply assumption
   2.343    done
   2.344  
   2.345 -lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C * D"
   2.346 +lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
   2.347    apply (frule set_times_mono3)
   2.348    apply auto
   2.349    done
   2.350  
   2.351  lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
   2.352 -    x : a *o D ==> x : D * C"
   2.353 +    x : a *o D ==> x : D \<otimes> C"
   2.354    apply (frule set_times_mono4)
   2.355    apply auto
   2.356    done
   2.357 @@ -397,19 +343,19 @@
   2.358      (a * b) +o (a *o C)"
   2.359    by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
   2.360  
   2.361 -lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
   2.362 -    (a *o B) + (a *o C)"
   2.363 -  apply (auto simp add: set_plus elt_set_times_def ring_distribs)
   2.364 +lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
   2.365 +    (a *o B) \<oplus> (a *o C)"
   2.366 +  apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
   2.367     apply blast
   2.368    apply (rule_tac x = "b + bb" in exI)
   2.369    apply (auto simp add: ring_distribs)
   2.370    done
   2.371  
   2.372 -lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
   2.373 -    a *o D + C * D"
   2.374 +lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
   2.375 +    a *o D \<oplus> C \<otimes> D"
   2.376    apply (auto intro!: subsetI simp add:
   2.377 -    elt_set_plus_def elt_set_times_def set_times
   2.378 -    set_plus ring_distribs)
   2.379 +    elt_set_plus_def elt_set_times_def set_times_def
   2.380 +    set_plus_def ring_distribs)
   2.381    apply auto
   2.382    done
   2.383  
     3.1 --- a/src/HOL/MetisExamples/BigO.thy	Wed May 07 10:59:23 2008 +0200
     3.2 +++ b/src/HOL/MetisExamples/BigO.thy	Wed May 07 10:59:24 2008 +0200
     3.3 @@ -266,24 +266,24 @@
     3.4  done
     3.5  
     3.6  lemma bigo_plus_self_subset [intro]: 
     3.7 -  "O(f) + O(f) <= O(f)"
     3.8 -  apply (auto simp add: bigo_alt_def set_plus)
     3.9 +  "O(f) \<oplus> O(f) <= O(f)"
    3.10 +  apply (auto simp add: bigo_alt_def set_plus_def)
    3.11    apply (rule_tac x = "c + ca" in exI)
    3.12    apply auto
    3.13    apply (simp add: ring_distribs func_plus)
    3.14    apply (blast intro:order_trans abs_triangle_ineq add_mono elim:) 
    3.15  done
    3.16  
    3.17 -lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
    3.18 +lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)"
    3.19    apply (rule equalityI)
    3.20    apply (rule bigo_plus_self_subset)
    3.21    apply (rule set_zero_plus2) 
    3.22    apply (rule bigo_zero)
    3.23  done
    3.24  
    3.25 -lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
    3.26 +lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)"
    3.27    apply (rule subsetI)
    3.28 -  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus)
    3.29 +  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
    3.30    apply (subst bigo_pos_const [symmetric])+
    3.31    apply (rule_tac x = 
    3.32      "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
    3.33 @@ -330,8 +330,8 @@
    3.34    apply (auto simp add: if_splits linorder_not_le)
    3.35  done
    3.36  
    3.37 -lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"
    3.38 -  apply (subgoal_tac "A + B <= O(f) + O(f)")
    3.39 +lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"
    3.40 +  apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)")
    3.41    apply (erule order_trans)
    3.42    apply simp
    3.43    apply (auto del: subsetI simp del: bigo_plus_idemp)
    3.44 @@ -339,10 +339,10 @@
    3.45  
    3.46  ML_command{*ResAtp.problem_name := "BigO__bigo_plus_eq"*}
    3.47  lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
    3.48 -  O(f + g) = O(f) + O(g)"
    3.49 +  O(f + g) = O(f) \<oplus> O(g)"
    3.50    apply (rule equalityI)
    3.51    apply (rule bigo_plus_subset)
    3.52 -  apply (simp add: bigo_alt_def set_plus func_plus)
    3.53 +  apply (simp add: bigo_alt_def set_plus_def func_plus)
    3.54    apply clarify 
    3.55  (*sledgehammer*); 
    3.56    apply (rule_tac x = "max c ca" in exI)
    3.57 @@ -478,7 +478,7 @@
    3.58      f : lb +o O(g)"
    3.59    apply (rule set_minus_imp_plus)
    3.60    apply (rule bigo_bounded)
    3.61 -  apply (auto simp add: diff_minus func_minus func_plus)
    3.62 +  apply (auto simp add: diff_minus fun_Compl_def func_plus)
    3.63    prefer 2
    3.64    apply (drule_tac x = x in spec)+ 
    3.65    apply arith (*not clear that it's provable otherwise*) 
    3.66 @@ -538,7 +538,7 @@
    3.67      (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
    3.68    apply (drule set_plus_imp_minus)
    3.69    apply (rule set_minus_imp_plus)
    3.70 -  apply (subst func_diff)
    3.71 +  apply (subst fun_diff_def)
    3.72  proof -
    3.73    assume a: "f - g : O(h)"
    3.74    have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
    3.75 @@ -552,7 +552,7 @@
    3.76      done
    3.77    also have "... <= O(f - g)"
    3.78      apply (rule bigo_elt_subset)
    3.79 -    apply (subst func_diff)
    3.80 +    apply (subst fun_diff_def)
    3.81      apply (rule bigo_abs)
    3.82      done
    3.83    also have "... <= O(h)"
    3.84 @@ -563,12 +563,12 @@
    3.85  lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" 
    3.86  by (unfold bigo_def, auto)
    3.87  
    3.88 -lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)"
    3.89 +lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)"
    3.90  proof -
    3.91    assume "f : g +o O(h)"
    3.92 -  also have "... <= O(g) + O(h)"
    3.93 +  also have "... <= O(g) \<oplus> O(h)"
    3.94      by (auto del: subsetI)
    3.95 -  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
    3.96 +  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
    3.97      apply (subst bigo_abs3 [symmetric])+
    3.98      apply (rule refl)
    3.99      done
   3.100 @@ -577,18 +577,18 @@
   3.101    finally have "f : ...".
   3.102    then have "O(f) <= ..."
   3.103      by (elim bigo_elt_subset)
   3.104 -  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
   3.105 +  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
   3.106      by (rule bigo_plus_eq, auto)
   3.107    finally show ?thesis
   3.108      by (simp add: bigo_abs3 [symmetric])
   3.109  qed
   3.110  
   3.111  ML_command{*ResAtp.problem_name := "BigO__bigo_mult"*}
   3.112 -lemma bigo_mult [intro]: "O(f)*O(g) <= O(f * g)"
   3.113 +lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
   3.114    apply (rule subsetI)
   3.115    apply (subst bigo_def)
   3.116    apply (auto simp del: abs_mult mult_ac
   3.117 -              simp add: bigo_alt_def set_times func_times)
   3.118 +              simp add: bigo_alt_def set_times_def func_times)
   3.119  (*sledgehammer*); 
   3.120    apply (rule_tac x = "c * ca" in exI)
   3.121    apply(rule allI)
   3.122 @@ -722,7 +722,7 @@
   3.123  ML_command{*ResAtp.problem_name := "BigO__bigo_mult7"*}
   3.124    declare bigo_mult6 [simp]
   3.125  lemma bigo_mult7: "ALL x. f x ~= 0 ==>
   3.126 -    O(f * g) <= O(f::'a => ('b::ordered_field)) * O(g)"
   3.127 +    O(f * g) <= O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
   3.128  (*sledgehammer*)
   3.129    apply (subst bigo_mult6)
   3.130    apply assumption
   3.131 @@ -734,11 +734,11 @@
   3.132  ML_command{*ResAtp.problem_name := "BigO__bigo_mult8"*}
   3.133    declare bigo_mult7[intro!]
   3.134  lemma bigo_mult8: "ALL x. f x ~= 0 ==>
   3.135 -    O(f * g) = O(f::'a => ('b::ordered_field)) * O(g)"
   3.136 +    O(f * g) = O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
   3.137  by (metis bigo_mult bigo_mult7 order_antisym_conv)
   3.138  
   3.139  lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
   3.140 -  by (auto simp add: bigo_def func_minus)
   3.141 +  by (auto simp add: bigo_def fun_Compl_def)
   3.142  
   3.143  lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
   3.144    apply (rule set_minus_imp_plus)
   3.145 @@ -748,7 +748,7 @@
   3.146  done
   3.147  
   3.148  lemma bigo_minus3: "O(-f) = O(f)"
   3.149 -  by (auto simp add: bigo_def func_minus abs_minus_cancel)
   3.150 +  by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
   3.151  
   3.152  lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
   3.153  proof -
   3.154 @@ -756,9 +756,9 @@
   3.155    show "f +o O(g) <= O(g)"
   3.156    proof -
   3.157      have "f : O(f)" by auto
   3.158 -    then have "f +o O(g) <= O(f) + O(g)"
   3.159 +    then have "f +o O(g) <= O(f) \<oplus> O(g)"
   3.160        by (auto del: subsetI)
   3.161 -    also have "... <= O(g) + O(g)"
   3.162 +    also have "... <= O(g) \<oplus> O(g)"
   3.163      proof -
   3.164        from a have "O(f) <= O(g)" by (auto del: subsetI)
   3.165        thus ?thesis by (auto del: subsetI)
   3.166 @@ -944,7 +944,7 @@
   3.167  
   3.168  lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o 
   3.169      O(%x. h(k x))"
   3.170 -  apply (simp only: set_minus_plus [symmetric] diff_minus func_minus
   3.171 +  apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
   3.172        func_plus)
   3.173    apply (erule bigo_compose1)
   3.174  done
   3.175 @@ -1007,11 +1007,11 @@
   3.176        (%x. SUM y : A x. l x y * g(k x y)) +o
   3.177          O(%x. SUM y : A x. abs(l x y * h(k x y)))"
   3.178    apply (rule set_minus_imp_plus)
   3.179 -  apply (subst func_diff)
   3.180 +  apply (subst fun_diff_def)
   3.181    apply (subst setsum_subtractf [symmetric])
   3.182    apply (subst right_diff_distrib [symmetric])
   3.183    apply (rule bigo_setsum3)
   3.184 -  apply (subst func_diff [symmetric])
   3.185 +  apply (subst fun_diff_def [symmetric])
   3.186    apply (erule set_plus_imp_minus)
   3.187  done
   3.188  
   3.189 @@ -1036,11 +1036,11 @@
   3.190          (%x. SUM y : A x. (l x y) * g(k x y)) +o
   3.191            O(%x. SUM y : A x. (l x y) * h(k x y))" 
   3.192    apply (rule set_minus_imp_plus)
   3.193 -  apply (subst func_diff)
   3.194 +  apply (subst fun_diff_def)
   3.195    apply (subst setsum_subtractf [symmetric])
   3.196    apply (subst right_diff_distrib [symmetric])
   3.197    apply (rule bigo_setsum5)
   3.198 -  apply (subst func_diff [symmetric])
   3.199 +  apply (subst fun_diff_def [symmetric])
   3.200    apply (drule set_plus_imp_minus)
   3.201    apply auto
   3.202  done
   3.203 @@ -1048,7 +1048,7 @@
   3.204  subsection {* Misc useful stuff *}
   3.205  
   3.206  lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
   3.207 -  A + B <= O(f)"
   3.208 +  A \<oplus> B <= O(f)"
   3.209    apply (subst bigo_plus_idemp [symmetric])
   3.210    apply (rule set_plus_mono2)
   3.211    apply assumption+
   3.212 @@ -1093,11 +1093,11 @@
   3.213         f 0 = g 0 ==> f =o g +o O(h)"
   3.214    apply (rule set_minus_imp_plus)
   3.215    apply (rule bigo_fix)
   3.216 -  apply (subst func_diff)
   3.217 -  apply (subst func_diff [symmetric])
   3.218 +  apply (subst fun_diff_def)
   3.219 +  apply (subst fun_diff_def [symmetric])
   3.220    apply (rule set_plus_imp_minus)
   3.221    apply simp
   3.222 -  apply (simp add: func_diff)
   3.223 +  apply (simp add: fun_diff_def)
   3.224  done
   3.225  
   3.226  subsection {* Less than or equal to *}
   3.227 @@ -1159,7 +1159,7 @@
   3.228    apply (rule allI)
   3.229    apply (rule le_maxI2)
   3.230    apply (rule allI)
   3.231 -  apply (subst func_diff)
   3.232 +  apply (subst fun_diff_def)
   3.233  apply (erule thin_rl)
   3.234  (*sledgehammer*);  
   3.235    apply (case_tac "0 <= k x - g x")
   3.236 @@ -1196,7 +1196,7 @@
   3.237    apply (rule allI)
   3.238    apply (rule le_maxI2)
   3.239    apply (rule allI)
   3.240 -  apply (subst func_diff)
   3.241 +  apply (subst fun_diff_def)
   3.242  apply (erule thin_rl) 
   3.243  (*sledgehammer*); 
   3.244    apply (case_tac "0 <= f x - k x")
   3.245 @@ -1214,12 +1214,12 @@
   3.246    apply (unfold lesso_def)
   3.247    apply (drule set_plus_imp_minus)
   3.248    apply (drule bigo_abs5) back
   3.249 -  apply (simp add: func_diff)
   3.250 +  apply (simp add: fun_diff_def)
   3.251    apply (drule bigo_useful_add)
   3.252    apply assumption
   3.253    apply (erule bigo_lesseq2) back
   3.254    apply (rule allI)
   3.255 -  apply (auto simp add: func_plus func_diff compare_rls 
   3.256 +  apply (auto simp add: func_plus fun_diff_def compare_rls 
   3.257      split: split_max abs_split)
   3.258  done
   3.259