Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] local datatypes?


view this post on Zulip Email Gateway (Aug 18 2022 at 18:36):

From: John Wickerson <jpw48@cam.ac.uk>
Hello,

Is it possible to introduce a new datatype that scoped only for the duration of a single proof? My datatype doesn't technically depend on local definitions inside the proof -- I just want to make it clear to the reader that these datatype only needs to be understood in the context of this proof.

That is, I want to write something like this:

theorem soundness:
"\<forall> a :: A. prov a --> sem a"
proof

datatype myNewType = Foo int | Bar nat

fun f :: "A => myNewType => bool"
where (* ... *)

lemma soundness_first_step:
"\<forall> a. prov a --> (\<exists> m. f a m)"
proof (* ... *) qed

lemma soundness_second_step:
"\<forall> a. (\<exists> m. f a m) --> sem a"
proof (* ... *) qed

show ?thesis
using soundness_first_step
and soundness_second_step by auto

qed

Thanks very much,
john

view this post on Zulip Email Gateway (Aug 18 2022 at 18:36):

From: Makarius <makarius@sketis.net>
On Fri, 28 Oct 2011, John Wickerson wrote:

Is it possible to introduce a new datatype that scoped only for the
duration of a single proof? My datatype doesn't technically depend on
local definitions inside the proof -- I just want to make it clear to
the reader that these datatype only needs to be understood in the
context of this proof.

There are technical reasons why such extreme for of locality is not
supported, and practical ones.

If you take locales for example, the "local" specifications are always
accessible from outside via qualified names. Picking lemmas from other
peoples private developments is common practice, and seems to cause little
problems in reality. (Less than in regular programming.)

That is, I want to write something like this:

theorem soundness:
"\<forall> a :: A. prov a --> sem a"
proof

datatype myNewType = Foo int | Bar nat

fun f :: "A => myNewType => bool"
where (* ... *)

lemma soundness_first_step:
"\<forall> a. prov a --> (\<exists> m. f a m)"
proof (* ... *) qed

The standard way to do it is to put the 'theorem' last, without any
special nesting. Its classification as "theorem" already indicates it
being a main result. There is also 'corollary'.

BTW, type names in HOL are almost always plain identifiers like foo_bar,
without caps or camels.

BTW2, closed statements with HOL \<forall> --> are rare. You normally
state open inference rules, using !! ==> or better fixes/assumes/shows in
Isar notation. E.g. like this:

lemma soundness_first_step:
fixes a
assumes "prov a"
shows "\<exists> m. f a m"

You can also split up the \<exists> via Isar 'obtains', if you are
more ambitious.

Makarius


Last updated: Mar 29 2024 at 04:18 UTC