[isabelle] parametric typedef?



Consider the following (very simplified) example:

  datatype myDatatype = A | B

  locale fix_n = fixes n :: nat
  begin

  inductive myProperty :: "myDatatype => bool"
    where
    mPA : "myProperty A"
  | mPB : "even n \<Longrightarrow> myProperty B"

Now I want to define a new type

  typedef myType = "{X::myDatatype . myProperty X}"

This is not accepted:

  *** Illegal application of command "typedef" (...) in local theory mode

Is there a way to do such a thing, or a reason why it cannot be done?

Notice that leaving locale fix_n, the following is accepted:

  end (** fix_n **)

  consts N :: nat

  interpretation FN:fix_n "N :: nat"
  done

  typedef myType = "{X::myDatatype . FN.myProperty X}"
    by (rule exI[of _ "A"], simp add: FN.mPA)

So Isabelle accepts that parametric definition and reasoning about
myType is sound.  But with this approach I will never be able to
instantiate the constant N.

Randy




-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






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