Email Gateway (Aug 19 2022 at 16:10): Email Gateway (Aug 19 2022 at 16:10):From: M A <tesleft@hotmail.com>
Hi
http://fa.isabelle.narkive.com/LVdvCYnK/isabelle-stuck-on-proof
above link mention in proof general, the "Isabelle/Show me .../Facts" menu
I can not find in plugin or other menu, where can show facts
show "list.inject" this command can not show facts content.
lemma "P ∧ Q ==> P"
sledgehammer learn_isar
sledgehammer [prover = e, fact_filter = mesh, verbose]
"mesh": Including 1000 relevant facts: list.inject ...
Regards,
Martin
Email Gateway (Aug 19 2022 at 16:10):From: Makarius <makarius@sketis.net>
The proper spelling is "Proof General" with capitals. It was once the
main user interface for Isabelle, and is still used in some other proof
assistants like Coq.
In Isabelle2014 Proof General is no longer included, but it happens to
work as "optional component" as explained in the NEWS. In the next
release it will be no longer there -- its deletion is scheduled for the
end of this week!
As a new user of Isabelle, there is no need to know what Proof General is
or was. I do recommend, though, to study the Isabelle/jEdit manual, which
is available in the "Documentation" panel via the label "jedit". For
example, it explains how to input mathematical symbols (there is more
than one way to do it).
Makarius
http://stop-ttip.org 742,965 people so far
Email Gateway (Aug 19 2022 at 16:10):From: Lars Noschinski <noschinl@in.tum.de>
On 27.10.2014 17:53, M A wrote:
I can not find in plugin or other menu, where can show facts
show "list.inject" this command can not show facts content.
You should really read the documentation.
You can print lemmas with the "print_statement" or "thm" commands or by
using the find theorems tab of the query panel.
lemma "P ∧ Q ==> P"
sledgehammer learn_isar
sledgehammer [prover = e, fact_filter = mesh, verbose]"mesh": Including 1000 relevant facts: list.inject ...
Do not use fact_filter, verbose and learn_isar. At this point in your
Isabelle career, they won't help you.
Email Gateway (Aug 19 2022 at 16:10):From: M A <tesleft@hotmail.com>
Hi
as it return the fact name, I would like to know the fact body
I have search search fact in help but can not find relevant information. How to show the fact body?
for example rotate, body is (length xs) (xs++ys) == ys++xs
rotate (length xs) (xs++ys) == ys++xs
$ hipspec Rotate.hs --auto --cg --verbosity=30
Depth 1: 11 terms, 5 tests, 29 evaluations, 11 classes, 0 raw equations.
Depth 2: 63 terms, 100 tests, 2151 evaluations, 48 classes, 15 raw equations.
Depth 3: 1688 terms, 100 tests, 63851 evaluations, 1303 classes, 385 raw equations.
Proved xs++[] == xs by induction on xs using Z3
Proved (xs++ys)++zs == xs++(ys++zs) by induction on xs using Z3
Proved length (xs++ys) == length (ys++xs) by induction on ys,xs using Z3
Proved rotate m [] == [] without induction using Z3
Proved rotate m (rotate n xs) == rotate n (rotate m xs) by induction on n,m using Z3
Proved rotate (S m) (rotate n xs) == rotate (S n) (rotate m xs) by induction on xs using Z3
Proved rotate m (x:[]) == x:[] by induction on m using Z3
Proved rotate m xs++rotate m xs == rotate m (xs++xs) by induction on m using Z3
Proved length (rotate m xs) == length xs by induction on m using Z3
Proved rotate (length xs) (xs++ys) == ys++xs by induction on xs using Z3
Proved prop_rotate {- rotate (length xs) xs == xs -} without induction using Z3
Proved:
xs++[] == xs
(xs++ys)++zs == xs++(ys++zs)
length (xs++ys) == length (ys++xs)
rotate m (rotate n xs) == rotate n (rotate m xs)
rotate (S m) (rotate n xs) == rotate (S n) (rotate m xs)
rotate m (x:[]) == x:[]
rotate m xs++rotate m xs == rotate m (xs++xs)
length (rotate m xs) == length xs
rotate (length xs) (xs++ys) == ys++xs
prop_rotate {- rotate (length xs) xs == xs -}
Regards,
Martin
Last updated: Apr 16 2024 at 20:15 UTC