Email Gateway (Aug 18 2022 at 09:51): Email Gateway (Aug 18 2022 at 09:51):From: Fulya <fulyahorozal@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
Email Gateway (Aug 18 2022 at 09:54):From: Tjark Weber <tjark.weber@gmx.de>
Fulya,
"oops" aborts a proof attempt, so quite naturally example333alem1 isn't
available afterwards. Try to "insert" a lemma that you have actually
proved.
Best,
Tjark
Email Gateway (Aug 18 2022 at 09:56):From: John Ridgway <jridgway@wesleyan.edu>
You could try using "sorry" instead of "oops", as "sorry" does not
abort the proof attempt.
Peace
Last updated: May 03 2024 at 04:19 UTC