Email Gateway (Aug 18 2022 at 10:56): Email Gateway (Aug 18 2022 at 10:56):From: Andreas Lochbihler <lochbihl@infosun.fim.uni-passau.de>
Hello all,
I'm currently converting my old theories to the new syntax of the latest
Isabelle development snapshot.
In doing so, I stumbled over the new inductive package which subsumes
the set definition and the syntax translation in one step.
However, in some cases, I have problems converting constants which
formerly were function to sets.
For example, if the old syntax read like this. In the syntax
translation, the order of the parameters is changed:
(*
consts p :: "'a => 'b => nat => bool"
consts
w :: "'a => 'b => (nat * nat) set"
syntax
w_syntax :: "'a => nat => 'b => nat => bool" -- define here some nice
syntax
translations
"w_syntax a c b d" == "(c, d) : w a b"
inductive "w a b"
intros
"p a b c ==> w_syntax a c b 0"
"w_syntax a (Suc c) b n ==> w_syntax a c b (Suc n)"
*)
I then tried to convert this to the new syntax, but then Isabelle
responds with an error message
consts p :: "'a => 'b => nat => bool"
inductive w :: "'a => nat => 'b => nat => bool"
for a :: 'a and b :: 'b where
"p a b c => w a c b 0"
| "w a (Suc c) b n => w a c b (Suc n)"
*** Ill-formed introduction rule ""
*** p a b c ==> w a c b 0
*** Inductive predicate must be applied to parameter(s) a, b
*** At command "inductive".
My workaround was to define the set w with type 'a => 'b => nat => nat
=> bool (thereby rewriting every introduction rule to get rid of the
syntax translation which is no longer available) and then to provide an
abbreviation which gives the original syntax back.
Is there any way I can use the order of parameters as given by the old
syntax translation in the introduction rules for w?
Regards,
Andreas Lochbihler
Email Gateway (Aug 18 2022 at 10:56):From: Makarius <makarius@sketis.net>
There is a special add-on feature of the inductive package that allows to
mix the specification with abbreviations. E.g. see
HOL/Bali/DeclConcepts.thy for the definition/abbreviation of
accessible_fromR etc.
Makarius
Email Gateway (Aug 18 2022 at 10:56):From: Stefan Berghofer <berghofe@in.tum.de>
Andreas Lochbihler wrote:
The new inductive command allows introduction rules to be specified
simultaneously with abbreviations. All rules of the form "... == ..."
occurring after the "where" keyword are treated as abbreviations.
The abbreviations are expanded automatically, so you can already
write the introduction rules using the desired syntax. In your
example, this would look as follows:
inductive
w_syntax :: "'a => nat => 'b => nat => bool"
and w :: "'a => 'b => nat => nat => bool"
for a :: 'a and b :: 'b
where
"w_syntax a c b d == w a b c d"
| "p a b c ==> w_syntax a c b 0"
| "w_syntax a (Suc c) b n ==> w_syntax a c b (Suc n)"
Greetings,
Stefan
Last updated: May 03 2024 at 08:18 UTC