# HG changeset patch
# User wenzelm
# Date 1125496061 -7200
# Node ID ebd268806589ffac85238e756bd7cc3aabf569bc
# Parent  e80fd664a119d61c27653bb36ad0827d96d742b6
Additional BigO lemmas that require the HOL-Complex logic image;

diff -r e80fd664a119 -r ebd268806589 src/HOL/Complex/ex/BigO_Complex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Complex/ex/BigO_Complex.thy	Wed Aug 31 15:47:41 2005 +0200
@@ -0,0 +1,50 @@
+(*  Title:      HOL/Complex/ex/BigO_Complex.thy
+    ID:		$Id$
+    Authors:    Jeremy Avigad and Kevin Donnelly
+*)
+
+header {* Big O notation -- continued *}
+
+theory BigO_Complex
+imports BigO Complex
+begin
+
+text {*
+  Additional lemmas that require the \texttt{HOL-Complex} logic image.
+*}
+
+lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> 0"
+  apply (simp add: LIMSEQ_def bigo_alt_def)
+  apply clarify
+  apply (drule_tac x = "r / c" in spec)
+  apply (drule mp)
+  apply (erule divide_pos_pos)
+  apply assumption
+  apply clarify
+  apply (rule_tac x = no in exI)
+  apply (rule allI)
+  apply (drule_tac x = n in spec)+
+  apply (rule impI)
+  apply (drule mp)
+  apply assumption
+  apply (rule order_le_less_trans)
+  apply assumption
+  apply (rule order_less_le_trans)
+  apply (subgoal_tac "c * abs(g n) < c * (r / c)")
+  apply assumption
+  apply (erule mult_strict_left_mono)
+  apply assumption
+  apply simp
+done
+
+lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a 
+    ==> g ----> a"
+  apply (drule set_plus_imp_minus)
+  apply (drule bigo_LIMSEQ1)
+  apply assumption
+  apply (simp only: func_diff)
+  apply (erule LIMSEQ_diff_approach_zero2)
+  apply assumption
+done
+
+end