David,
On 31/10/2019 19:14, David Topham wrote:
Thank you Roger, that is very helpful. I found I had to add this line
to make it work:
(open_theory "cs113" handle _ => (open_theory "hol"; new_theory "cs113"));
But then my next problem is to work on geometric progressions which
require real numbers
When I use R->R
I get error message
"type constructor or abbreviation for R not in scope."
I wonder if hol is enough for using R? Or will I need to change or add
to the ancestor theory I am inheriting from?
You could try the theory "ℝ", which is not an ancestor of HOL.
You are making quite a big leap in complexity, going from arithmetic to
analysis, so things will get harder.
You can have geometric progressions over the natural numbers, so if the
result you are looking for actually works in that context, you might be
best to try it there first.
If not you might benefit from working in one of the theories in
maths_egs, depending on how much analysis you need.
You would need to look at what is available (you can see the listings at
lemma-one.com if you want to check before installing maths_egs) and
decide what is the best context for your work.
see: http://www.lemma-one.com/ProofPower/examples/examples.html
Even if you stick to the natural numbers, maths_egs has something for
you, the theory "numbers" in wrk074.
Roger
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
