isabelle: src/HOL/ex/BigO_Complex.thy@d41182a8135c (annotated)

17211 ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	1	(* Title: HOL/Complex/ex/BigO_Complex.thy
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	2	ID: $Id$
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	3	Authors: Jeremy Avigad and Kevin Donnelly
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	4	*)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	5
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	6	header {* Big O notation -- continued *}
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	7
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	8	theory BigO_Complex
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	9	imports BigO Complex
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	10	begin
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	11
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	12	text {*
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	13	Additional lemmas that require the \texttt{HOL-Complex} logic image.
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	14	*}
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	15
20550 5a925ad63f4d add required type annotation huffman parents: 17211 diff changeset	16	lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"
17211 ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	17	apply (simp add: LIMSEQ_def bigo_alt_def)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	18	apply clarify
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	19	apply (drule_tac x = "r / c" in spec)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	20	apply (drule mp)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	21	apply (erule divide_pos_pos)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	22	apply assumption
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	23	apply clarify
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	24	apply (rule_tac x = no in exI)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	25	apply (rule allI)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	26	apply (drule_tac x = n in spec)+
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	27	apply (rule impI)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	28	apply (drule mp)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	29	apply assumption
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	30	apply (rule order_le_less_trans)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	31	apply assumption
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	32	apply (rule order_less_le_trans)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	33	apply (subgoal_tac "c * abs(g n) < c * (r / c)")
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	34	apply assumption
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	35	apply (erule mult_strict_left_mono)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	36	apply assumption
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	37	apply simp
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	38	done
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	39
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	40	lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a
20550 5a925ad63f4d add required type annotation huffman parents: 17211 diff changeset	41	==> g ----> (a::real)"
17211 ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	42	apply (drule set_plus_imp_minus)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	43	apply (drule bigo_LIMSEQ1)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	44	apply assumption
26806 40b411ec05aa Adapted to encoding of sets as predicates berghofe parents: 20550 diff changeset	45	apply (simp only: fun_diff_def)
17211 ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	46	apply (erule LIMSEQ_diff_approach_zero2)
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	47	apply assumption
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	48	done
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	49
ebd268806589 Additional BigO lemmas that require the HOL-Complex logic image; wenzelm parents: diff changeset	50	end

author	krauss
	Tue, 16 Dec 2008 08:46:07 +0100
changeset 29125	d41182a8135c
parent 28952	15a4b2cf8c34
permissions	-rw-r--r--