Email Gateway (Aug 22 2022 at 12:55): Email Gateway (Aug 22 2022 at 12:55):From: Freek Wiedijk <freek@cs.ru.nl>
Dear all,
My apologies for a newbie question.
I am trying to understand the relationship between "dest"
and "elim". From
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-March/msg00077.html>
I got the impression that "elim" is a generalisation of
"dest". But in the Tutorial (reference from that message)
I read in 5.7 that "erule" unifies Q with the subgoal,
while "drule" does not. So that seems to imply that "erule"
might fail where "drule" does not?
In the example files for Concrete Semantics, I see lemmas
(for example "SkipE") that are proved with "[elim]", but
where I think that you do not only want to use them when
their conclusion unifies with the goal?
A pointer to a relevant book/manual is all I need. And if
this is too trivial, do not bother the list with this!
Freek
Email Gateway (Aug 22 2022 at 12:56):From: Peter Lammich <lammich@in.tum.de>
Hi,
chapter 5 of the tutorial (rules of the game) is exactly the right thing
to read (the whole chapter), in particluar 5.2..5.4 may answer your
questions.
Best,
Peter
Email Gateway (Aug 22 2022 at 12:56):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Freek,
for me, the difference is mostly in how a fact is stated. A basic
example from natural deduction is conjunction elimination.
In textbooks we often see two rules
conj1: A & B ==> A
conj2: A & B ==> B
in Isabelle parlance those are "dest" (as in destructive) rules, since
they loose information. If you apply such a rule (with drule) in an
apply-script you can turn a provable subgoal into an unprovable one
(since the fact that B holds disappeared).
The corresponding "elim" rule (which I would really consider to be more
general, as you suggested) is:
conjE: A & B ==> (A ==> B ==> thesis) ==> thesis
if you apply it with "erule" you just turn the single fact "A & B" into
two facts "A" and "B" without (really) using information (since you
could reconstruct "A & B" again with what you got).
Moreover, the conclusion of "conjE" is so general that it will unify
with the conclusion of any subgoal. So, whether "erule" succeeds or
fails purely depends on whether some formula of the shape "?A & ?B" is
among the premises of the subgoal.
hope this helps,
cheers
chris
Email Gateway (Aug 22 2022 at 12:56):From: Lawrence Paulson <lp15@cam.ac.uk>
The terminology comes from natural deduction.
But elimination rules in natural reduction come in two forms. The most general form (e.g. disjE or exE in Isabelle) allows any formula as the conclusion, and is analogous to a sequent calculus rule that operates only on the left side. But there is also a special form (e.g. conjunct1, mp) that doesn’t fit this pattern, but performs forward reasoning. I have called these destruction rules, but this nomenclature is totally non-standard.
Larry
Email Gateway (Aug 22 2022 at 12:56):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Freek,
"inductive_cases" generates a new fact from the given formula which you
can inspect e.g. using "thm".
"thm SkipE" reveales
(SKIP, ?s) ⇒ ?t ⟹ (?t = ?s ⟹ ?P) ⟹ ?P
which is in "elim-format" i.e., the conclusion is fully general and
unifies with any subgoal and we have a major premise that is eliminated.
Where did you actually see "(SKIP,s) \<Rightarrow> t \<Longrightarrow> t
= s" ?
cheers,
chris
Email Gateway (Aug 22 2022 at 12:56):From: Peter Lammich <lammich@in.tum.de>
In the example files for Concrete Semantics, I see lemmas
(for example "SkipE") that are proved with "[elim]", but
where I think that you do not only want to use them when
their conclusion unifies with the goal?
Do you mean?
inductive_cases SkipE[elim!]: "(SKIP,s) ⇒ t"
thm SkipE
⟦(SKIP, ?s) ⇒ ?t; ?t = ?s ⟹ ?P⟧ ⟹ ?P
This is a standard pattern for case distinction, that you see all over
Isabelle. It is also produced by "obtains".
For SKIP, there is only one case, namely t=s.
The intuition is as follows:
If the premise contains a (SKIP,s) => t, this rule will unify with any
conclusion P, and what remains to proof is "t=s ==> P" ... the SKIP is
gone.
Look, e.g., at
thm list.set_cases
to see examples for more than one case.
Also inductive predicates generate rules in this format, to be applied
with "rule inversion", e.g.
thm big_step.cases
Note that the "proof (cases)" method essentially applies the
corresponding cases rules, and then tries to automatically prove trivial
goals.
Email Gateway (Aug 22 2022 at 12:56):From: Freek Wiedijk <freek@cs.ru.nl>
Dear Peter,
thm SkipE
⟦(SKIP, ?s) ⇒ ?t; ?t = ?s ⟹ ?P⟧ ⟹ ?P
Oops! From the book (on page 81) I had got the impression
that the theorem would be "(SKIP, s) => t ==> t = s".
(I hadn't actually tried it.)
I feel embarrassed now. My apologies for the disturbance,
and thanks for all the help!
Freek
Email Gateway (Aug 22 2022 at 12:56):From: Tobias Nipkow <nipkow@in.tum.de>
The book is intentionally ambiguous at this point. The fact that the
inductive_cases command produces the rules in elimination format is merely a
logical diversion. Hence I suppressed that discussion.
Tobias
smime.p7s
Last updated: Apr 26 2024 at 04:17 UTC