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