Re: [isabelle] Splitting case-expressions automatically



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)

- Brian

Quoting Tobias Nipkow <nipkow at 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:
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










This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.