Email Gateway (Aug 18 2022 at 12:07): Email Gateway (Aug 18 2022 at 12:07):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
given the following datatype
datatype test = A | B | C
how can I prove the following subgoal automatically with one (or a few)
apply statements. I want to avoid to make the proof explicit in Isar,
because of the writing overhead.
"[| !!t. x:(case t of A => s1 | B => s2 | C => s3) ==> P; x:s2 |] ==> P"
something like (auto split: test.splits) does not work, am I missing
some lemmas or is there a way to explicitly instantiating t ?
Thanks for any hints in advance,
Peter
Email Gateway (Aug 18 2022 at 12:07):From: Tobias Nipkow <nipkow@in.tum.de>
The problem are the deeply nested meta-logical symbols that the split
facility seems unable to cope with. If you reformulate it a bit, it works:
lemma [rule_format]:
"[| !t. x:(case t of A => s1 | B => s2 | C => s3) --> P; x:s2 |] ==> P"
by(auto split: test.splits)
Tobias
Peter Lammich wrote:
Email Gateway (Aug 18 2022 at 12:07):From: Brian Huffman <brianh@cs.pdx.edu>
By the way, you can use the "atomize" tactic to automatically
reformulate the current subgoal from meta-level to object-level
quantifiers.
lemma "[| !!t. x:(case t of A => s1 | B => s2 | C => s3) ==> P; x:s2 |] ==> P"
by (atomize, auto split: test.splits)
Another option is to manually instantiate the meta-universal
quantifier using the meta_spec rule:
lemma "[| !!t. x:(case t of A => s1 | B => s2 | C => s3) ==> P; x:s2 |] ==> P"
by (drule meta_spec [where x=B], simp)
Quoting Tobias Nipkow <nipkow@in.tum.de>:
Last updated: May 03 2024 at 12:27 UTC