# [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
• 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.