*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 02:37:54 +0800*Importance*: Normal*In-reply-to*: <BAY167-W2B9A063451056956EEF7DB6910@phx.gbl>*References*: <BAY167-W98CD8E5A34362D3F91DB23B6910@phx.gbl>, , <978D0158-8D33-4127-B19B-3823CC04B9FF@in.tum.de>, <BAY167-W2B9A063451056956EEF7DB6910@phx.gbl>

Hi After find https://www.mail-archive.com/isabelle-dev at 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 at 1, length_map at 5the information is not like a lemma, how to know what is zip_rev at 1 and length_map at 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 at hotmail.com > To: noschinl at in.tum.de; isabelle-users at cl.cam.ac.uk > Date: Mon, 27 Oct 2014 01:44:25 +0800 > Subject: Re: [isabelle] how to know which rules to apply before apply(auto)? > > 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 at in.tum.de > > Date: Sun, 26 Oct 2014 11:12:12 +0100 > > 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)? > > > > 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 > > > > Am 26. Oktober 2014 10:11:41 MEZ, schrieb M A <tesleft at hotmail.com>: > > >Hi > > >1. how to know which rules to apply before apply(auto)?2. any manual to > > >show all the rules that can be applied for each library when import > > >them?3. is there any difference to apply rules in one statement or > > >apply one by one? > > >a. apply(a)apply(b)done > > >b.apply(a,b)done > > > > > >Regards, > > >Martin >

**Follow-Ups**:**Re: [isabelle] how to know which rules to apply before apply(auto)?***From:*Lars Noschinski

**References**:

- Previous by Date: Re: [isabelle] how to know which rules to apply before apply(auto)?
- Next by Date: Re: [isabelle] how to know which rules to apply before apply(auto)?
- Previous by Thread: Re: [isabelle] how to know which rules to apply before apply(auto)?
- Next by Thread: Re: [isabelle] how to know which rules to apply before apply(auto)?
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list