*To*: John Wickerson <jpw48 at cam.ac.uk>*Subject*: Re: [isabelle] local datatypes?*From*: Makarius <makarius at sketis.net>*Date*: Fri, 28 Oct 2011 21:53:59 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <B54E0D2E-A180-4B43-B29D-055460C7EA6F@cam.ac.uk>*References*: <B54E0D2E-A180-4B43-B29D-055460C7EA6F@cam.ac.uk>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Fri, 28 Oct 2011, John Wickerson wrote:

Is it possible to introduce a new datatype that scoped only for theduration of a single proof? My datatype doesn't technically *depend* onlocal definitions inside the proof -- I just want to make it clear tothe reader that these datatype only needs to be understood in thecontext 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_first_step: fixes a assumes "prov a" shows "\<exists> m. f a m"

Makarius

**References**:**[isabelle] local datatypes?***From:*John Wickerson

- Previous by Date: Re: [isabelle] "usedir -b" on Probability: I have to add a relative path in Borel_Space.thy
- Next by Date: [isabelle] CMCS 2012: second call for papers
- Previous by Thread: [isabelle] local datatypes?
- Next by Thread: [isabelle] CMCS 2012: second call for papers
- Cl-isabelle-users October 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list