Email Gateway (Aug 18 2022 at 11:10): Email Gateway (Aug 18 2022 at 11:10):From: George Karabotsos <g_karab@cs.concordia.ca>
Hello,
I am wondering how I can change the following inductive set definition
(along with its associated syntax) using Isabelle 2007. I am able to
use the inductive_set syntax for its definition, however, I am unable to
use the -e-> syntax.
consts
eval :: "(B * bool)set"
syntax
"_eval" :: "B => bool => bool" (infixl "-e->" 50)
translations
"b -e-> b'" == "(b,b') : eval"
inductive eval
intros
TrueB: "TrueB -e-> True"
FalseB: "FalseB -e-> False"
TIA,
George
Email Gateway (Aug 18 2022 at 11:10):From: Makarius <makarius@sketis.net>
This works by using abbreviations simultaneously within the
'inductive_set' definition, e.g. like this:
inductive_set eval and eval_syn (infixl "-e->" 50)
where
"b -e-> b' == (b, b') : eval"
| TrueB: "TrueB -e-> True"
| FalseB: "FalseB -e-> False"
Also note that 'inductive' for inductive predicates is usually more
convient than the historical detour via sets; it does not need separate
syntax at all:
inductive eval_rel (infixl "-e->" 50)
where
TrueB: "TrueB -e-> True"
| FalseB: "FalseB -e-> False"
Makarius
Last updated: May 03 2024 at 12:27 UTC