src/HOL/Library/BigO.thy
 changeset 17199 59c1bfc81d91 parent 16961 9c5871b16553 child 19279 48b527d0331b
     1.1 --- a/src/HOL/Library/BigO.thy	Wed Aug 31 15:46:35 2005 +0200
1.2 +++ b/src/HOL/Library/BigO.thy	Wed Aug 31 15:46:36 2005 +0200
1.3 @@ -11,31 +11,29 @@
1.4
1.5  text {*
1.6  This library is designed to support asymptotic big O'' calculations,
1.7 -i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g + O(h)$.
1.8 -An earlier version of this library is described in detail in
1.9 -\begin{quote}
1.10 -Avigad, Jeremy, and Kevin Donnelly, \emph{Formalizing O notation in
1.11 -Isabelle/HOL}, in David Basin and Micha\"el Rusiowitch, editors,
1.12 -\emph{Automated Reasoning: second international conference, IJCAR 2004},
1.13 -Springer, 357--371, 2004.
1.14 -\end{quote}
1.15 +i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g + 1.16 +O(h)$.  An earlier version of this library is described in detail in
1.18 +
1.19  The main changes in this version are as follows:
1.20  \begin{itemize}
1.21 -\item We have eliminated the $O$ operator on sets. (Most uses of this seem
1.22 +\item We have eliminated the @{text O} operator on sets. (Most uses of this seem
1.23    to be inessential.)
1.24 -\item We no longer use $+$ as output syntax for $+o$.
1.25 -\item Lemmas involving sumr'' have been replaced by more general lemmas
1.26 -  involving setsum''.
1.27 +\item We no longer use @{text "+"} as output syntax for @{text "+o"}
1.28 +\item Lemmas involving @{text "sumr"} have been replaced by more general lemmas
1.29 +  involving @{text "setsum"}.
1.30  \item The library has been expanded, with e.g.~support for expressions of
1.31 -  the form $f < g + O(h)$.
1.32 +  the form @{text "f < g + O(h)"}.
1.33  \end{itemize}
1.34 -Note that two lemmas at the end of this file are commented out, as they
1.35 -require the HOL-Complex library.
1.36 +
1.37 +See \verb,Complex/ex/BigO_Complex.thy, for additional lemmas that
1.38 +require the \verb,HOL-Complex, logic image.
1.39
1.40 -Note also since the Big O library includes rules that demonstrate set
1.41 -inclusion, to use the automated reasoners effectively with the library one
1.42 -should redeclare the theorem subsetI'' as an intro rule, rather than as
1.43 -an intro! rule, for example, using declare subsetI [del, intro]''.
1.44 +Note also since the Big O library includes rules that demonstrate set
1.45 +inclusion, to use the automated reasoners effectively with the library
1.46 +one should redeclare the theorem @{text "subsetI"} as an intro rule,
1.47 +rather than as an @{text "intro!"} rule, for example, using
1.48 +\isa{\isakeyword{declare}}~@{text "subsetI [del, intro]"}.
1.49  *}
1.50
1.51  subsection {* Definitions *}
1.52 @@ -581,7 +579,7 @@
1.53        (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
1.54    apply (auto simp add: bigo_def)
1.55    apply (rule_tac x = "abs c" in exI)
1.56 -  apply (subst abs_of_nonneg);back;back
1.57 +  apply (subst abs_of_nonneg) back back
1.58    apply (rule setsum_nonneg)
1.59    apply force
1.60    apply (subst setsum_mult)
1.61 @@ -718,7 +716,7 @@
1.62    apply force
1.63    apply force
1.64    apply (subgoal_tac "x = Suc (x - 1)")
1.65 -  apply (erule ssubst)back
1.66 +  apply (erule ssubst) back
1.67    apply (erule spec)
1.68    apply simp
1.69  done
1.70 @@ -802,7 +800,7 @@
1.71    apply (case_tac "0 <= k x - g x")
1.72    apply simp
1.73    apply (subst abs_of_nonneg)
1.74 -  apply (drule_tac x = x in spec)back
1.75 +  apply (drule_tac x = x in spec) back
1.77    apply (subst diff_minus)+
1.79 @@ -826,7 +824,7 @@
1.80    apply (case_tac "0 <= f x - k x")
1.81    apply simp
1.82    apply (subst abs_of_nonneg)
1.83 -  apply (drule_tac x = x in spec)back
1.84 +  apply (drule_tac x = x in spec) back
1.86    apply (subst diff_minus)+
1.88 @@ -842,11 +840,11 @@
1.89      g =o h +o O(k) ==> f <o h =o O(k)"
1.90    apply (unfold lesso_def)
1.91    apply (drule set_plus_imp_minus)
1.92 -  apply (drule bigo_abs5)back
1.93 +  apply (drule bigo_abs5) back
1.96    apply assumption
1.97 -  apply (erule bigo_lesseq2)back
1.98 +  apply (erule bigo_lesseq2) back
1.99    apply (rule allI)
1.100    apply (auto simp add: func_plus func_diff compare_rls
1.101      split: split_max abs_split)
1.102 @@ -875,43 +873,4 @@
1.103    apply (auto split: split_max simp add: func_plus)
1.104  done
1.105
1.106 -(*
1.107 -These last two lemmas require the HOL-Complex library.
1.108 -
1.109 -lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> 0"
1.110 -  apply (simp add: LIMSEQ_def bigo_alt_def)
1.111 -  apply clarify
1.112 -  apply (drule_tac x = "r / c" in spec)
1.113 -  apply (drule mp)
1.114 -  apply (erule divide_pos_pos)
1.115 -  apply assumption
1.116 -  apply clarify
1.117 -  apply (rule_tac x = no in exI)
1.118 -  apply (rule allI)
1.119 -  apply (drule_tac x = n in spec)+
1.120 -  apply (rule impI)
1.121 -  apply (drule mp)
1.122 -  apply assumption
1.123 -  apply (rule order_le_less_trans)
1.124 -  apply assumption
1.125 -  apply (rule order_less_le_trans)
1.126 -  apply (subgoal_tac "c * abs(g n) < c * (r / c)")
1.127 -  apply assumption
1.128 -  apply (erule mult_strict_left_mono)
1.129 -  apply assumption
1.130 -  apply simp
1.131 -done
1.132 -
1.133 -lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a
1.134 -    ==> g ----> a"
1.135 -  apply (drule set_plus_imp_minus)
1.136 -  apply (drule bigo_LIMSEQ1)
1.137 -  apply assumption
1.138 -  apply (simp only: func_diff)
1.139 -  apply (erule LIMSEQ_diff_approach_zero2)
1.140 -  apply assumption
1.141 -done
1.142 -
1.143 -*)
1.144 -
1.145  end
`