# Re: [isabelle] dest_Trueprop question

On Fri, 16 Jun 2006, Dimitrios Vytiniotis wrote:
> I have a datatype which has only one constructor that takes a pair.
> Values of this datatype are paired with naturals and contained in a
> list. I have very often found out that when I do induction on the list
> to prove a theorem, in the inductive case I often have to do a "by(cases
> "x", cases "snd x", blast)"
This is how to provide your own cases rule for that specific type scheme:
datatype ('a, 'b) foo = Foo "'a * 'b"
lemma nat_foo_cases [cases type]:
"(!!(n::nat) a b. x = (n, Foo (a, b)) ==> C) ==> C"
by (cases x, cases "snd x") auto
lemma
fixes foos :: "(nat * ('a, 'b) foo) list"
shows "P foos"
proof (induct foos)
case Nil
show ?case sorry
next
case (Cons x xs)
show ?case
apply (cases x)
sorry
qed
> How do I do this elegantly (e.g with a single tactic like
> (cases_deep_break "x", auto) or similar)
As a rule of thumb, it is better to derive rules of the Pure framework (as
above) rather than do ML hacking with methods/tactics.
Makarius

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