Re: [isabelle] how to know which rules to apply before apply(auto)?
- To: Lars Noschinski <noschinl at in.tum.de>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] how to know which rules to apply before apply(auto)?
- From: M A <tesleft at hotmail.com>
- Date: Mon, 27 Oct 2014 07:15:41 +0800
- Importance: Normal
- In-reply-to: <BAY167-W4331B35B219FCE88C6BD80B6910@phx.gbl>
- References: <BAY167-W98CD8E5A34362D3F91DB23B6910@phx.gbl>,,, , <978D0158-8D33-4127-B19B-3823CC04B9FF@in.tum.de>, , , <BAY167-W2B9A063451056956EEF7DB6910@phx.gbl>, , <BAY167-W170987875672AC6B117169B6910@phx.gbl>, , <544D3E80.email@example.com>, <BAY167-W4331B35B219FCE88C6BD80B6910@phx.gbl>
Hi after find lack of lemma length_map, I use find_theorems can not find length_maphow to find lemma length_map ? theory ts
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