Email Gateway (Aug 18 2022 at 11:55): Email Gateway (Aug 18 2022 at 11:55):From: Peter Chapman <pc@cs.st-and.ac.uk>
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?
Thanks
Peter
Email Gateway (Aug 18 2022 at 11:55):From: Peter Lammich <peter.lammich@uni-muenster.de>
Peter Chapman wrote:
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):
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.
Email Gateway (Aug 18 2022 at 11:55):From: Makarius <makarius@sketis.net>
For Isabelle2007 see the isar-ref manual section 4.3.5 "Proof by cases and
induction", especially page 100, which gives an overview how the
cases/induct methods select the rules being used in a proof.
For eliminating inductive set membership "x:A", the basic idiom is like
this:
from x:A have "P x"
proof induct
case (blah a b c)
...
Assuming the usual declarations produced by the Isabelle/HOL packages,
this will use the A.cases rule as expected (A.exhaust is an obsolete name
for that). These rules rarely need to be referenced explicitly by name
anyway.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC