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



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 at hotmail.com
> To: noschinl at in.tum.de; isabelle-users at cl.cam.ac.uk
> Date: Mon, 27 Oct 2014 06:21:01 +0800
> Subject: Re: [isabelle] how to know which rules to apply before apply(auto)?
> 
> 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
> > From: noschinl at in.tum.de
> > To: tesleft at hotmail.com; isabelle-users at cl.cam.ac.uk
> > Subject: Re: [isabelle] how to know which rules to apply before apply(auto)?
> > 
> > On 26.10.2014 19:37, M A wrote:
> > > After find
> > > https://www.mail-archive.com/isabelle-dev at 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.
> > >  
> > > 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.