[isabelle] local datatypes?



Hello,

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.

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_second_step:
    "\<forall> a. (\<exists> m. f a m) --> sem a"
  proof (* ... *) qed

  show ?thesis 
    using soundness_first_step
      and soundness_second_step by auto

qed

Thanks very much,
john




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