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:

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.