[isabelle] The method "insert"



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.