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



Dear Elsa,

the formal semantics of Isar is documented in Chapter 3 of Makarius' PhD thesis [1]. There an equivalent formulation of "by" is given (on p. 62) as

by m1 m2 = apply m1 apply m2 apply (assumption+)? done

where in your case m1 is "rule impE" and m2 is "-". The semantics of the "rule"-method (requiring to match the chained facts in the order they are given) is described on p. 60.

Best wishes,
Dmitriy

[1] https://mediatum.ub.tum.de/doc/601724/601724.pdf

On 19.02.2015 04:45, Alfio Martini wrote:
Dear Elsa,

  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.

In this case, the third premise using "rule impE" seems to be "B==>B" which
holds by "rule assumption"
So I would expect this to go through. It is written somewhere in the
reference manual that "by" applies the assumption rule under the hood, or
at least I thought of reading so.

Best!

On Thu, Feb 19, 2015 at 12:39 AM, Elsa L. Gunter <egunter at illinois.edu>
wrote:

  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>
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
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.