add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
authorhoelzl
Wed Mar 06 16:56:21 2013 +0100 (2013-03-06)
changeset 51360c4367ed99b5e
parent 51359 00b45c7e831f
child 51361 21e5b6efb317
add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Limits.thy	Wed Mar 06 16:10:56 2013 +0100
     1.2 +++ b/src/HOL/Limits.thy	Wed Mar 06 16:56:21 2013 +0100
     1.3 @@ -775,15 +775,24 @@
     1.4    tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
     1.5    "(f ---> l) F \<equiv> filterlim f (nhds l) F"
     1.6  
     1.7 +lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
     1.8 +  by simp
     1.9 +
    1.10  ML {*
    1.11 +
    1.12  structure Tendsto_Intros = Named_Thms
    1.13  (
    1.14    val name = @{binding tendsto_intros}
    1.15    val description = "introduction rules for tendsto"
    1.16  )
    1.17 +
    1.18  *}
    1.19  
    1.20 -setup Tendsto_Intros.setup
    1.21 +setup {*
    1.22 +  Tendsto_Intros.setup #>
    1.23 +  Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
    1.24 +    map (fn thm => @{thm tendsto_eq_rhs} OF [thm]) o Tendsto_Intros.get o Context.proof_of);
    1.25 +*}
    1.26  
    1.27  lemma tendsto_def: "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
    1.28    unfolding filterlim_def