# [isabelle] The method "insert"

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] The method "insert"
*From*: Fulya <fulyahorozal at gmail.com>
*Date*: Tue, 31 Oct 2006 17:03:03 +0100
*In-reply-to*: <68d9dc2d0610310612n4b52f7f2v5acdbe00036c31df@mail.gmail.com>
*References*: <68d9dc2d0610310612n4b52f7f2v5acdbe00036c31df@mail.gmail.com>

Dear Isabelle users,
I am trying to construct a proof for an example in Isabelle regarding
sequences.
I am having a problem to apply the method "insert" in the proof.
Here is the formalized example:
--
constdefs
real_lower_bound_of :: "real set => real => bool"
"real_lower_bound_of S u == \<forall>s \<in> S. u \<le> s"
inf :: "real set => real"
"inf S == THE x. (is_infimum_of S x)"
underlying_set_of_sequence :: "(nat => real) => real set"
" underlying_set_of_sequence X == {x. \<exists>(n::nat). (X n)=x}"
...
lemma example333alem1:
"real_lower_bound_of (underlying_set_of_sequence (%(n::nat). (1 / (sqrt
(real n))))) 0"
oops
...
lemma example333a:
"lim (%(n::nat). (1 / (sqrt (real n)))) = 0"
apply (insert example333alem1)
--
The error given in the proof of the lemma "example333a" is as follows:
Error in method "Pure.insert":
*** Unknown theorem(s) "example333alem1"
*** At command "apply".
Could anyone give a solution to that error?
Thanks a lot!
Best,
Fulya Horozal
--
Saarland University
Saarbruecken, Germany

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*