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.17 +\cite{Avigad-Donnelly}.
    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.76    apply (simp add: compare_rls)
    1.77    apply (subst diff_minus)+
    1.78    apply (rule add_right_mono)
    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.85    apply (simp add: compare_rls)
    1.86    apply (subst diff_minus)+
    1.87    apply (rule add_left_mono)
    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.94    apply (simp add: func_diff)
    1.95    apply (drule bigo_useful_add)
    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