Email Gateway (Aug 19 2022 at 16:09): Email Gateway (Aug 19 2022 at 16:09):From: Lars Noschinski <noschinl@in.tum.de>
On 26.10.2014 18:44, M A wrote:
is it fact_filter to give hints about what lemma to be used? what is
the correct command to return hints about which lemmas to be used?
Usually you just start sledgehammer (e.g., from the the sledgehammer
panel). Options like fact_filter are either for very advanced or just
internal usage.
after tried, it seems same as giving hints about rules, however not
lemmas.
Rules are lemmas. Or did you expect sledgehammer to suggest you a
proposition which you should prove to prove the theorem?
Sometimes it do not have immediate response, I do not know whether it
start or running or not start.
If you use the sledgehammer panel, there is a small rotating circle
indicating whether sledgehammer is running. If you write the
"sledgehammer" command in your theory file, it has a different
background as long as it is running.
"remote_vampire": Cannot connect to remote server.
You probably had no network connection, so the vampire server could not
be reached.
"spass": Try this: by (metis list.inject) (0 ms).
Spass found a proof involving the "list.inject" lemma.
(No structured proof available -- proof too simple.)
The proof is so simple, that sledgehammer cannot split it into more
simple steps.
-- Lars
Email Gateway (Aug 19 2022 at 16:09):From: Lars Noschinski <noschinl@in.tum.de>
On 26.10.2014 19:37, M A wrote:
After find
https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03468.html
This is about improving how Sledgehammer is working -- note that it was
posted on the development mailing list. This is nothing you need to care
about as a beginner.
I click apply that can see it is running, it seems need to know at
least one lemma.
Sledgehammer tries to discharge the current proof goal, yes.
1. How about if we do not know any lemma so that no starting lemma for
it to run the command?
Then what should sledgehammer try to prove?
Be careful with the notation: A lemma (or theorem, fact, rule) is a
proven statement which can be used in further proofs.
The "lemma" command in Isabelle allows you to state a proposition. It
then sets up (one or more) goals you need to prove (using the commands
proof, apply, ...). After finishing the prove, a lemma with the
proposition you stated is added to your theory.
- do not know from example of the link about Facts in "e" proof (of
1000): zip_rev@1, length_map@5 <mailto:length_map@5>
the information is not like a lemma, how to know what is zip_rev@1
<mailto:zip_rev@1> and length_map@5 <mailto:length_map@5> ?
This is some internal sledgehammer stuff.- using example below, how to find two lemma below ?
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
I am not sure what you are trying to do here. You don't need them
explicitly in your proof?
-- Lars
Email Gateway (Aug 19 2022 at 16:09):From: M A <tesleft@hotmail.com>
Hi I use toylist example in http://isabelle.in.tum.de/doc/tutorial.pdf To practise how it find other lemma from one lemma with Sledgehammer when I left click it , it runs a very long time without a listbox pop up. lemma app_Nil2 [simp]: "xs @ [] = xs"sledgehammer learn_isar are essential lemmas must include associative lemma and distributive lemma? Regards, Martin > Date: Sun, 26 Oct 2014 19:33:36 +0100
Email Gateway (Aug 19 2022 at 16:09):From: M A <tesleft@hotmail.com>
Hi after find lack of lemma length_map, I use find_theorems can not find length_maphow to find lemma length_map ? theory ts
imports Main
begin
lemma "map f xs = ys ==> rev (zip xs ys) = zip (rev xs) (rev ys)"
sledgehammer [prover = e, fact_filter = mesh, verbose]
find_theorems "length_map ?" Regards, Martin > From: tesleft@hotmail.com
Email Gateway (Aug 19 2022 at 16:22):From: M A <tesleft@hotmail.com>
Hi
Regards,
Martin
Email Gateway (Aug 19 2022 at 16:23):From: Lawrence Paulson <lp15@cam.ac.uk>
Becoming an expert at Isabelle takes time and cannot be rushed. It sounds like you simply need to work through the tutorials, doing small examples to begin with. Before attempting to prove a theorem, you need to have an intuitive grasp of the key steps of the proof. Don’t expect “auto” to work miracles.
Larry Paulson
Email Gateway (Aug 19 2022 at 16:23):From: M A <tesleft@hotmail.com>
Hi ,
I just think to apply all the rules at one time and then apply(auto) to see which rules it use in debug rather than guess by observation and trial and error.It seems think out essential number of lemmas in order before theorem already a miracle. apply(a,b,c,d,e,f,g.......etc)apply(auto)
Regards,
Martin
Email Gateway (Aug 19 2022 at 16:23):From: Lars Noschinski <noschinl@in.tum.de>
When proving something in Isabelle, you should have an idea how you would prove it on paper first: This should give you an idea which properties you need for the proof.
Isabelle offers you a few tools to discover useful lemmas: Sledgehammer can search for a proof and gives you a list of lemmas it needed for a proof. Inspecting this list often helps to give the right lemmas to auto (and similar tools), so they can find a proof.
Very helpful is also the "find theorems" tool which is found in the query panel: You can search for lemmas containing certain constants or having a specific shape. In particular, you can also search for lemmas which are applicable by rule (using the intro, elim, dest keywords).
It is important to keep in mind that lemmas are often formulated a bit differently than in maths, to make them work better with the various proof tools.
There is no manual of all rules. Rather, the lemmas available can be either discovered by browsing the theories or (more directly) by the use of find theorems.
In many cases, "apply(a,b)" and "apply a apply b" are equivalent, but there are some differences: Some proof methods (e.g. rule) don't return a single proof step but potentially a sequence of multiple proof steps (try applying the "back" command). In the (a,b) case, when the second proof method fails, Isabelle backtracks and tries the next proof step produced by a. Also, if there are chained facts (from using then, from, using or similar) then these facts are available to both proof methods. This is usually not what you want.
Best regards, Lars
Email Gateway (Aug 19 2022 at 16:24):From: M A <tesleft@hotmail.com>
Hi is it fact_filter to give hints about what lemma to be used? what is the correct command to return hints about which lemmas to be used? after tried, it seems same as giving hints about rules, however not lemmas. Sometimes it do not have immediate response, I do not know whether it start or running or not start. "remote_vampire": Cannot connect to remote server.
"spass": Try this: by (metis list.inject) (0 ms).
(No structured proof available -- proof too simple.)
"e": Try this: by (metis the_elem_set) (0 ms).
(No structured proof available -- proof too simple.) theory ts
imports Main
begin
lemma "[a] = [b] ==> a = b"
sledgehammer fact_filter = <"[a] = [b] ==> a = b"> {smart} Regards, Martin > From: noschinl@in.tum.de
Email Gateway (Aug 19 2022 at 16:24):From: M A <tesleft@hotmail.com>
Hi After find https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03468.html I click apply that can see it is running, it seems need to know at least one lemma. 1. How about if we do not know any lemma so that no starting lemma for it to run the command? 2. do not know from example of the link about Facts in "e" proof (of 1000): zip_rev@1, length_map@5the information is not like a lemma, how to know what is zip_rev@1 and length_map@5 ? 3. using example below, how to find two lemma below ?lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
sledgehammer_params [fact_filter = mesh]
theory Scratch
imports Datatype
begin
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
(* This is the append function: *)
primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65)
where
"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"
primrec rev :: "'a list => 'a list" where
"rev [] = []" |
"rev (x # xs) = (rev xs) @ (x # [])"primrec itrev :: "'a list => 'a list => 'a list" where
"itrev [] ys = ys" |
"itrev (x#xs) ys = itrev xs (x#ys)"
value "rev (True # False # [])"
lemma app_Nil2 [simp]: "xs @ [] = xs"
sledgehammer learn_isar
apply(induct_tac xs)
apply(auto)
doneend Regards, Martin > From: tesleft@hotmail.com
Last updated: Apr 18 2024 at 20:16 UTC