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

Hi  I use toylist example in 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
> From: noschinl at
> To: tesleft at; isabelle-users at
> Subject: 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.