Email Gateway (Aug 19 2022 at 09:22): Email Gateway (Aug 19 2022 at 09:22):From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
Dear all,
This one should be simple. I'm looking for the name of the rule that
will do the job of RRR below:
lemma "\<forall> (a,b) \<in> S. P"
proof (rule RRR)
fix a b
assume "(a,b) \<in> S"
show "P" sorry
qed
Thanks in advance!
Stephan
Email Gateway (Aug 19 2022 at 09:22):From: Stephan Merz <Stephan.Merz@loria.fr>
There is not a single rule that would introduce two quantifiers. You can either use rule allI twice (see the Isar combinator "+") or use the clarify method.
Stephan
Email Gateway (Aug 19 2022 at 09:23):From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
Using allI twice (or with +) does not work for me, but clarify does the
job perfectly. Thanks a lot!
Stephan
Email Gateway (Aug 19 2022 at 09:23):From: Tjark Weber <webertj@in.tum.de>
Hi Stephan,
clarify may do more than you want if S or P are compound terms. Here is
another solution:
lemma RRR:
assumes "⋀a b. (a,b) ∈ S ⟹ P"
shows "∀ (a,b) ∈ S. P"
by (metis assms splitI2)
Best regards,
Tjark
Email Gateway (Aug 19 2022 at 09:23):From: Makarius <makarius@sketis.net>
Putting automated tools like "clarify" or "auto" in the initial "proof"
position is actually an anti-pattern of structured proofs. Sometimes it
cannot be avoided, but it should not be done by default.
Instead, the usual way is to make a bottom-up proof with automated
re-composition like this:
notepad
begin
have "∀(a, b) ∈ S. P"
proof -
{
fix a b
assume "(a, b) ∈ S"
have P sorry
}
then show ?thesis
by auto -- "terminal auto, instead of initial clarify etc."
qed
end
This can also cause surprises sometimes, especially with too general
types for the body within { ... }, but it usually works in a reasonably
robust way, and does not depend on the details of what automation does.
Makarius
Email Gateway (Aug 19 2022 at 09:23):From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
Your solution works for me and is quite readable. Thanks for helping!
Stephan
Last updated: Apr 23 2024 at 16:19 UTC