[isabelle] Nominal Isabelle and pair types



I am experimenting with using Nominal Isabelle for labelled deductive systems. For starters, I am trying to create a pair type of labels and formulae.

The following definition seems to work:

  atom_decl simple_label prop_var

  datatype formula = Atom "prop_var"
                   | Impl "formula" "formula"
                   | Conj "formula" "formula"
                   | Disj "formula" "formula"
                   | Bottom

  nominal_datatype labelled_formula =
    "\<guillemotleft>simple_label\<guillemotright> * formula"

but them I am unable to use fst (and snd?) on the pair. I get type unification errors from the following:

  constdefs
   get_label :: "labelled_formula \<Rightarrow> simple_label"
   "get_label lf \<equiv> (fst lf)"
   get_formula :: "labelled_formula \<Rightarrow> formula"
   "get_formula lf \<equiv> (snd lf)"

Please advise.

Thanks,
Rob





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