Email Gateway (Aug 19 2022 at 17:16): Email Gateway (Aug 19 2022 at 17:16):From: "Elsa L. Gunter" <egunter@illinois.edu>
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
Email Gateway (Aug 19 2022 at 17:16):From: Alfio Martini <alfio.martini@acm.org>
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!
Email Gateway (Aug 19 2022 at 17:16):From: "Elsa L. Gunter" <egunter@illinois.edu>
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
Email Gateway (Aug 19 2022 at 17:16):From: Alfio Martini <alfio.martini@acm.org>
Dear Elsa,
I did not have to separately derive B and supply it explicitly as the
Email Gateway (Aug 19 2022 at 17:17):From: Dmitriy Traytel <traytel@in.tum.de>
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
Last updated: Apr 27 2024 at 01:05 UTC