Email Gateway (Aug 18 2022 at 12:12): Email Gateway (Aug 18 2022 at 12:12):From: Christian Urban <urbanc@in.tum.de>
Hi Rob,
I am slightly unsure what exactly you are trying to do. If you
want to have pairs built up by simple_labels and formulae,
then the following works
atom_decl simple_label prop_var
datatype formula =
Atom "prop_var"
| Impl "formula" "formula"
| Conj "formula" "formula"
| Disj "formula" "formula"
| Bottom
types labelled_formula = "simple_label * formula"
constdefs
get_label :: "labelled_formula => simple_label"
"get_label lf == (fst lf)"
get_formula :: "labelled_formula => formula"
"get_formula lf == (snd lf)"
Note that the construction \<guillemotleft>simple_label\<guillemotright>
is for a binder of type simple_label. Your formulae, however, do not
contain any simple_labels, so the binding would always be vacuous. This
is nearly always not what is intended.
I am experimenting with using Nominal Isabelle for labelled
deductive systems.
Feel free to subscribe to the dedicated Nominal Isabelle mailing list.
See
http://isabelle.in.tum.de/nominal/
Hope this helps,
Christian
Last updated: May 03 2024 at 04:19 UTC