Re: [isabelle] Formal semantics for Isar structured proof language



Dear Alfio,
This concurs with what I have learned form experimentation and experience. But you might note the the second proof, using impE is willing to fill in the proof of B ==> B; I did not have to separately derive B and supply it explicitly as the third hypothesis, even though impE has three hypotheses/subgoals required. So sometime proof is willing to look among the available hypotheses to see if a generated subgoal is among them (perhaps it will only do so for assumptions it just generated?), but other times (perhaps when they are given through from?) it will not. Apparently, the order of the from clauses matter by why is quite unclear to me. Anyway, it is my feeling and hope that such matters can be resolved by reference to a formal semantics and not by experimenting with a given implementation.
---Elsa


On 2/18/15 8:28 PM, Alfio Martini wrote:
Dear Elsa,

I have just a working knowledge of Isar and Isabelle. But by experience tells me that when you use the method "by (rule R)" in a forward way, the premises of the goal have to match exactly the premises of the rule. In this case, the rule mp is coded in Isabelle like this:

 ?P-->?Q ==> ?P ==>?Q

So, the first premise in you third proof is only "A" and thus does not match
the implication of the rule. In such cases, using "simp" will suffice.

Anyway, I am sure a more technical and precise answer will follow this message.

Best!

On Wed, Feb 18, 2015 at 7:49 PM, Elsa L. Gunter <egunter at illinois.edu <mailto:egunter at illinois.edu>> wrote:

    Dear Isabelle Community,
      Does there exist / where can I find a formal semantics for the
    Isar structured proof scripting language?  The syntax of the Isar
    proof scripting language is defined fairly formally in Section 6
    of The Isabelle / Isar Reference Manual and it is accompanied by
    an informal and high level English explanation of each construct
    or group of construct, but I have not yet found a formal
    description of the language, via, say, something like modular
    structural operational semantics.  I'm not looking for any one
    particular style of semantics, but I would like something rigorous
    enough that it could be expressed in Isabelle, and rigorous enough
    so that it would explain why


    lemma fixes A and B shows "A â (A â B) â B"
    proof (rule impI)
     assume A: "A"
     show "(A â B) â B"
     proof (rule impI)
      assume AB: "A â B"
      from AB and A
      show "B"
      by (rule mp)
     qed
    qed

    and

    lemma fixes A and B shows "A â (A â B) â B"
    proof (rule impI)
     assume A: "A"
     show "(A â B) â B"
     proof (rule impI)
      assume AB: "A â B"
      from AB and A
      show "B"
      by (rule impE)
     qed
    qed

    both succeed, but

    lemma fixes A and B shows "A â (A â B) â B"
    proof (rule impI)
     assume A: "A"
     show "(A â B) â B"
     proof (rule impI)
      assume AB: "A â B"
      from A and AB
      show "B"
      by (rule mp)
     qed
    qed

    fails at by (rule mp).

    ---Elsa

    Elsa L Gunter
    Department of Computer Science
    University of Illinois at Urbana - Champaign




--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio <http://www.inf.pucrs.br/alfio>
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.