[isabelle] apply (cases a b c)



Is there a built-in way to generate subgoals for all cases of a set of
variables?

For instance, suppose I have the definitions:

  datatype dt = Num int | Infinity
  
  fun plus :: "dt ⇒ dt ⇒ dt"
  where
    "plus Infinity _ = Infinity"
  | "plus _ Infinity = Infinity"
  | "plus (Num a) (Num b) = Num (a + b)"

And now that I want to show:

  lemma "plus a b = plus b a"

I would like to be able to type:
    by (cases a b) simp_all

But this is not supported.

I know that I can type:
  by (tactic "(List.foldl (op THEN_ALL_NEW) (fn i => all_tac)
                (List.map (Induct_Tacs.case_tac @{context}) ["a", "b"]) 1)")
     simp_all

But somehow this is not very pleasing!

So, is there a good way to do this?

Would it be worth extending the cases method?

Tim.

Attachment: signature.asc
Description: Digital signature



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