Re: [isabelle] how to know which rules to apply before apply(auto)?

On 26.10.2014 19:37, M A wrote:
> After find
> at
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.
> 2.  do not know from example of the link about Facts in "e" proof (of
> 1000): zip_rev at 1, length_map at 5 <mailto:length_map at 5>
> the information is not like a lemma, how to know what is zip_rev at 1
> <mailto:zip_rev at 1> and length_map at 5 <mailto:length_map at 5> ?
This is some internal sledgehammer stuff.
>  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)"
I am not sure what you are trying to do here. You don't need them
explicitly in your proof?

  -- Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.