Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
definitions of + and * on functions.
--- 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
--- 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
--- 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