Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Accessing split-theorems on ML-level

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

From: Moa Johansson <s0199173@sms.ed.ac.uk>
Hi,
I need to get hold of theorems for splitting case-statements, given a
datatype, on the ML level (eg. theorems like "list.split", "nat.split"
etc). Where can I find these?

Thanks,
Moa

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

From: Amine Chaieb <chaieb@in.tum.de>
In ML you can access facts in the theorem databaase using thm or thms,
when the result is a theorem list.

In you case , e.g.

ML> thm "list.split";
val it =
"?P (list_case ?f1.0 ?f2.0 ?x) =
((?x = [] --> ?P ?f1.0) &
(ALL a list. ?x = a # list --> ?P (?f2.0 a list)))" : Thm.thm

Amine.

Moa Johansson wrote:

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

From: Moa Johansson <s0199173@sms.ed.ac.uk>
Yes, this is not quite what I had in mind though. In my program, I have
a type (from some variable in a term) and I would like to get the split
theorem directly from the type, without having to create a string
representation of the name of that type.

Moa

Amine Chaieb wrote:

Last updated: May 03 2024 at 08:18 UTC