Re: [isabelle] feature request: proof-local datatypes



Hello John,

not quite what you want, but with the new localized datatype package you can structure your proofs and datatypes definition with locales (with or) without assumptions.

theory Scratch
imports "~~/src/HOL/BNF/BNF"
begin

locale A
begin

data 'a list = ...

theorem x: "..."
using list.map ..

end

thm A.x

end

Of course, these "local" datatypes may not depend variables fixed by the locale, since this is already forbidden for typedefs. One could imagine a proof-local version of the data command with the same restriction.

Best,
Dmitriy

On 28.02.2013 12:17, John Wickerson wrote:
Dear Isabelle,

I have a theorem.

theorem t: "......"

To *state* my theorem is quite straightforward, but to *prove* it I require a whole bunch of other lemmas, definitions and datatypes. My theory file, therefore, looks like this:

definition x1: "......"

datatype x2 = ......

definition x3: "......"

lemma x4: "......"

datatype x5 = ......

lemma x6: "......"

theorem t: "......."
proof ......
Something about this strikes me as sub-optimal. The lemmas, definitions and datatypes x1...x6 are only required *within* this one particular proof. It seems like a violation of modularity for them to be globally-available outside of this proof. So I would prefer my theory file to look like this:

theorem t: "......."
proof

   definition x1: "......"

   datatype x2 = ......

   definition x3: "......"

   lemma x4: "......"

   datatype x5 = ......

   lemma x6: "......"

   ......

qed
I know I can already kind-of define lemmas within a proof (by writing "have x4: ...") and I know I can already kind-of make definitions within a proof (by writing "let ..." or "def ..."). But what would be quite nice would be to have the *full* expressivity that is available at the "top-level", also available within a proof, so that I can make proof-local datatypes, typedefs, and so on.

cheers,
john






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