Email Gateway (Aug 18 2022 at 18:36): 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
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"
proofdatatype 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: Nov 21 2024 at 12:39 UTC