# [isabelle] feature request: proof-local datatypes

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.*