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.