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.