Email Gateway (Aug 18 2022 at 12:12): Email Gateway (Aug 18 2022 at 12:12):From: Robert Rothenberg <robrwo@gmail.com>
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
Email Gateway (Aug 18 2022 at 12:13):From: Robert Rothenberg <robrwo@gmail.com>
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
Email Gateway (Aug 18 2022 at 12:14):From: Stefan Berghofer <berghofe@in.tum.de>
Robert Rothenberg wrote:
nominal_datatype labelled_formula =
"\<guillemotleft>simple_label\<guillemotright> * formula"
Hi Rob,
note that this command does not quite do what you want. The type expression
"\<guillemotleft>simple_label\<guillemotright> * formula" is not even well-formed,
since the type of a binder must have the form "\<guillemotleft>T\<guillemotright>U".
The reason why Isabelle does not complain about the ill-formed type is that it does
not define a datatype with a constructor having one argument of type
"\<guillemotleft>simple_label\<guillemotright> * formula". Instead, it defines a
datatype with a zero-argument constructor which is named
"\<guillemotleft>simple_label\<guillemotright> * formula".
Greetings,
Stefan
Last updated: May 03 2024 at 01:09 UTC