Email Gateway (Jan 10 2024 at 18:12): Email Gateway (Jan 10 2024 at 18:12):From: Gunnar Teege <gunnar.teege@unibw.de>
Hello all,
I observed an unexpected behavior when using the cases method with an
elimination rule attributed by [consumes 1], such as the trivial example
lemma elim1[consumes 1]: "⟦Q; Q ⟹ P⟧ ⟹ P" by blast
When applied in the form
lemma "X ⟹ Y" proof (cases rule: elim1)
the resulting goal state is
1. X ⟹ ?Q
2. ⟦X; ?Q⟧ ⟹ Y
which means that the major premise Q has not been consumed.
The induct method works as expected:
lemma "X ⟹ Y" proof (induct rule: elim1)
results in the goal state
1. X ⟹ Y
It works for the cases method if X is passed as input:
lemma assumes "X" shows "Y" using assms proof (cases rule: elim1)
results in the goal state
1. X ⟹ Y
Is that behavior intended?
Background: I was just curious whether elimination rule application can
be combined with creating named contexts for the cases.
Best regards
Gunnar Teege
Email Gateway (Jan 12 2024 at 16:21):From: Makarius <makarius@sketis.net>
On 10/01/2024 19:10, Gunnar Teege wrote:
Hello all,
I observed an unexpected behavior when using the cases method with an
elimination rule attributed by [consumes 1], such as the trivial examplelemma elim1[consumes 1]: "⟦Q; Q ⟹ P⟧ ⟹ P" by blast
When applied in the form
lemma "X ⟹ Y" proof (cases rule: elim1)
the resulting goal state is
1. X ⟹ ?Q
2. ⟦X; ?Q⟧ ⟹ Y
which means that the major premise Q has not been consumed.
This is correct in the sense of the Pure rule calculus, introduced by Paulson
1989 and turned into Isar proof text and proof methods by Wenzel 1999.
It is intendend, and the proper approach is indeed:
It works for the cases method if X is passed as input:
lemma assumes "X" shows "Y" using assms proof (cases rule: elim1)
results in the goal state
1. X ⟹ YIs that behavior intended?
The induct method works as expected:
lemma "X ⟹ Y" proof (induct rule: elim1)
results in the goal state
1. X ⟹ Y
The various proof methods for induction and coinduction actually violate a few
principles of Pure rule composition. The idea is to pass the goal context
properly through the induction principle (and a few other tricks). That is
practically important, but makes the whole setup a bit dense and hard to
explain / understand.
Background: I was just curious whether elimination rule application can be
combined with creating named contexts for the cases.
Maybe you want to check the isar-ref manual concerning the command 'subgoal'
or proof method "goal_cases". Both are outside proper Isar, though: the
puristic approach is to write statements such you have the context-particles
in your hand already, e.g. via 'obtains' / 'obtain' / 'consider'.
Makarius
Email Gateway (Jan 12 2024 at 17:39):From: Makarius <makarius@sketis.net>
More possibilities:
have A if B
using that by method
have A if B
using that
proof method
The postfix 'if' corresponds to prefix 'assumes' in toplevel statements. It is
a "recent" addition to Isar (from 2015).
Makarius
Last updated: Apr 29 2024 at 04:18 UTC