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



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


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