Re: [isabelle] local datatypes?
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:
"\<forall> a :: A. prov a --> sem a"
datatype myNewType = Foo int | Bar nat
fun f :: "A => myNewType => bool"
where (* ... *)
"\<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:
assumes "prov a"
shows "\<exists> m. f a m"
You can also split up the \<exists> via Isar 'obtains', if you are
This archive was generated by a fusion of
Pipermail (Mailman edition) and