*To*: Buday Gergely <gbuday at karolyrobert.hu>, Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] successful attempt vs failed to apply initial proof method*From*: Lars Hupel <hupel at in.tum.de>*Date*: Fri, 18 Mar 2016 10:14:23 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <C32D3449D568C445AB18C60817FABFE101AC727CE83F@ingrid.foiskola.krf>*References*: <C32D3449D568C445AB18C60817FABFE101AC727CE83E@ingrid.foiskola.krf> <alpine.LNX.2.00.1603171719550.2715@lxbroy10.informatik.tu-muenchen.de> <C32D3449D568C445AB18C60817FABFE101AC727CE83F@ingrid.foiskola.krf>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

> Is the above "exported rule" a fact, and, where does it come from? Can I use it to prove the goal, or it is a hypothetical fact that would prove the goal? Let's say you need to show a HOL implication "A --> B". lemma "A â B" proof (* The proof command applies a standard rule. As a result, the state panel shows an unstructured goal state A â B. *) assume A show B sorry qed Do you agree that this is a syntactically correct proof "template"? This is what the system tells you: > Successful attempt to solve goal by exported rule It could use the locally fixed variables, assumptions, and shown propositions to (partly) discharge a subgoal in the goal state. When you replace the "sorry" with a subproof which doesn't work, the outer proof is still syntactically correct. But the system also tells you that the subproof itself is incorrect ("Failed to apply ..."). It may help to think of Isar as a compiler with error recovery. Even if a part of a program (= proof) does not type check, the compiler "assumes" correctness and lets you go on with the rest. It'll only report the error where it actually occurred. Cheers Lars

**References**:**[isabelle] successful attempt vs failed to apply initial proof method***From:*Buday Gergely

**Re: [isabelle] successful attempt vs failed to apply initial proof method***From:*Makarius

**Re: [isabelle] successful attempt vs failed to apply initial proof method***From:*Buday Gergely

- Previous by Date: Re: [isabelle] finished proof contains coloured proof method
- Next by Date: [isabelle] Improper Integrals in Isabelle
- Previous by Thread: Re: [isabelle] successful attempt vs failed to apply initial proof method
- Next by Thread: Re: [isabelle] successful attempt vs failed to apply initial proof method
- Cl-isabelle-users March 2016 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