Email Gateway (Aug 18 2022 at 17:31): Email Gateway (Aug 18 2022 at 17:31):From: Alex Katovsky <apk32@cam.ac.uk>
Hi,
This is probably a very basic question, so I apologize if I'm not
reading the tutorial carefully enough. I have this lemma
lemma "(∀ x . A ⟶ B) ∧ (∀ y . C ⟶ D) ∧ (∀ x . E ⟶ F)"
and from this I want to generate the three subgoals
The only way I know how to do this at the moment is
apply(rule conjI, rule_tac [2] conjI)
apply(rule_tac [1] allI, rule_tac [2] allI, rule_tac [3] allI)
apply(rule_tac [1] impI, rule_tac [2] impI, rule_tac [3] impI)
What I would like to do is repeatedly apply "(rule conjI)|(rule
allI)|(rule impI)" to all subgoals until no further progress can be made.
Many thanks,
Alex.
Email Gateway (Aug 18 2022 at 17:31):From: Lawrence Paulson <lp15@cam.ac.uk>
Probably you should try
apply safe
This performs all so-called safe inferences: those that cannot lead to information loss.
Larry Paulson
Email Gateway (Aug 18 2022 at 17:32):From: Alex Katovsky <apk32@cam.ac.uk>
This works very well in the example I gave, but it appears that
sometimes "apply safe" can do more goal splitting than I want it to.
For example, if "F" below is "x = y" where x and y are sets then "apply
safe" will use set_eqI to generate these goals
and in some instances it would be preferable to keep equality as the
goal. Is there some way that I can limit "apply safe", for example
something like "apply (safe only: conjI allI impI)"?
Email Gateway (Aug 18 2022 at 17:32):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
untested, but I recall that I used "apply (intro conjI allI impI)" in
such cases.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 17:32):From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
You could use "intro":
apply (intro conjI allI impI)
which apply all introduction rules you give to it until no more is applicable.
Mathieu Giorgino
Email Gateway (Aug 18 2022 at 17:32):From: Lars Noschinski <noschinl@in.tum.de>
If you want to prove this lemma by proving the three goals mentioned
above, the idiomatic way to would probably be something like the following:
lemma "(∀ x . A ⟶ B) ∧ (∀ y . C ⟶ D) ∧ (∀ x . E ⟶ F)"
proof -
{ have "ALL x. A -> B" <some proof> }
moreover
{ have "ALL y. C -> D" <some proof> }
moreover
{ have "ALL x. E -> F" <some proof> }
ultimately
show ?thesis by auto
qed
Regards,
Lars
Email Gateway (Aug 18 2022 at 17:35):From: Alexander Katovsky <apk32@cam.ac.uk>
How about
lemma "\<forall> z . ((A (n :: nat) z) \<and> (B n z))
\<longrightarrow> C z"
proof(induct n, intro allI conjI impI)
It seems intro is not attacking the second induction goal. safe
works here, but in other cases (with particular forms for A B and C) it
does more than I want it to.
Email Gateway (Aug 18 2022 at 17:35):From: Makarius <makarius@sketis.net>
The proof methods "intro" and "elim" stem from a very ancient phase of
Isar (around 1998/1999) when certain key points about structured proofs
where not yet undestood.
Instead of iterative decomposition of standard connectives, proofs can be
done more directly by stating propositions in the intended way. The
"induct" method can work with such rule structure directly. For example:
notepad
begin
fix z :: 'a and n :: nat
have "A n z ==> B n z ==> C z"
proof (induct n)
...
No "intro" boilerplate is needed here.
Makarius
Email Gateway (Aug 18 2022 at 17:35):From: Makarius <makarius@sketis.net>
Here I meant to say (induct n arbitrary: z)
Makarius
Last updated: Apr 23 2024 at 20:15 UTC