Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] easy going with trivial cases in inductive proofs

Email Gateway (Aug 18 2022 at 10:19):

From: Carsten Varming <varming@cmu.edu>
Hi,

I am trying to use the Isar proof language to write nice inductive
proofs. Some of my proofs have two or three interesting cases and a ton
of trivial cases dealt with by a line for each case, eg:

case Lookup thus ?case by auto next
case Seq thus ?case by auto next
case Update thus ?case by auto next
case UpdateA thus ?case by auto next

Is there some way to tell Isabelle using Isar that for the yet to be
proved cases do:

case * thus ?case by auto next

It just not fun having to write a line for each trivial case.

Carsten

Email Gateway (Aug 18 2022 at 10:19):

From: Amine Chaieb <chaieb@in.tum.de>
You can attach a final method for qed. Hence in Isar you can concentrate
on the important cases and finish your proof e.g. by

qed auto

or the appropriate method instead of auto.

Amine.

Carsten Varming wrote:

Email Gateway (Aug 18 2022 at 10:19):

From: Julien Narboux <Julien.Narboux@inria.fr>
Carsten Varming a écrit :
Hi,

Yes there is, you can just put your automatic tactic between () at the
end of the manual cases at the qed.

case Foo thus ?case by ....

qed (auto) (* Lookup Seq Update UpdateA are solved by auto *)

Best wishes,

Julien

Last updated: May 03 2024 at 08:18 UTC