# Re: [isabelle] Case split for inductive definitions in Isar

Peter Chapman wrote:
> Hi
>
> I have a proof in which I wish to perform a case split as the proof
> method. Normally, I would just say
>
> proof (cases A)
>
> for something which was defined by primrec, or if I wanted to do a
> case split on its truth value. However, what I want to do a case
> split on was defined as an inductive datatype. I don't want to do
> induction, just a case split. I can do this "by hand", by proving a
> lemma which says "if the conclusion holds, then it must come from one
> of the clauses", and then use "moreover" blocks but this is
> cumbersome. Is there a way to call this proof method in Isar?
>
The cases method should also work for inductive datatypes, i.e. consider
consts P::"'a list \<Rightarrow> bool"
lemma "P l" proof (cases l)
which yields
goal (2 subgoals):
1. l = [] \<Longrightarrow> P l
2. \<And>a list. l = a # list \<Longrightarrow> P l
The lemma, that sais when the conclusion holds, it must come from one of
the clauses, is called <name>.exhaust for an inductive datatype <name>, i.e.
lemma list.exhaust:
\<lbrakk>?y = [] \<Longrightarrow> ?P; \<And>a list. ?y = a # list
\<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
and generated automatically upon defining an inductive datatype.
--
Peter Lammich, Institut für Informatik
Raum 715, Einsteinstrasse 62, 48149 Münster
Mail: peter.lammich at uni-muenster.de
Tel: 0251-83-32749
Mobil: 0163-5310380

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