Email Gateway (Aug 18 2022 at 09:31): Email Gateway (Aug 18 2022 at 09:31):From: Peter Lammich <peter.lammich@uni-muenster.de>
I have two records, defining some unrelated concepts, e.g. Labeled
transition systems and partial orders.
Each of this record defines some concrete syntax, e.g. "a -l-> b" for
transitions and a\<sqsubseteq>b for the order relation.
theory Scratch
imports Main "$ISABELLE_HOME/src/HOL/Algebra/Lattice"
begin
record ('s,'l) LTS =
S :: "'s"
T :: "'s \<Rightarrow> 'l \<Rightarrow> 's \<Rightarrow> bool" ("_
-_\<rightarrow>\<index> _")
Now I have some structure that relates this two concepts, for example a
partial order on the transition labels.
One possibility to write this down might be:
locale Combined = struct lts + complete_lattice L +
constrains lts :: "('a,'l) LTS"
constrains L :: "'l order"
assumes ...
But now the problem is, that the default structural parameter is only
applied to the concrete syntax of one of the both concepts. For the
other, I have to explicitely specify the structural index parameter,
which is annoying because of its writing overhead and because it makes
proof texts more difficult to read. In my case, the concrete syntax
"-_->" for LTS and \<sqsubseteq> for partial order is completely
disjunct so that it is always clear what structural parameter to apply
where.
lemma (in Combined) shows "\<lbrakk>a -l\<rightarrow> b; b
-l'\<rightarrow>c\<rbrakk>\<Longrightarrow> l \<sqsubseteq> l'"
this does not work, because it tries to index \<sqsubseteq> with lts
as structural parameter.
Is there any possibility to work around this problem and get a setting
where one can omit the indices to concrete syntax of both concepts.
A dirty hack would obviously be to define
record ('s,'l) LTS = 'l order +
S :: "'s"
T :: "'s \<Rightarrow> 'l \<Rightarrow> 's \<Rightarrow> bool" ("_
-_\<rightarrow>\<index> _")
but this would merge the two unrelated concepts of LTS and partial_order.
Is there any 'cleaner' solution. (Perhaps I'm misusing the concepts of
records/locales here, but how should it be done then ?)
Greetings and thanks in advance for any suggestions
Peter Lammich
Email Gateway (Aug 18 2022 at 09:32):From: Clemens Ballarin <ballarin@in.tum.de>
Dear Peter,
records are not flexible enough to achieve what you want since they
don't provide multiple inheritance on structures. Your "dirty hack" is
a way of simulating this. (My formalisation of additive groups in
HOL-Algebra uses an extension of the record for multiplicative groups
and ignores the unnecessary fields, so that's quite similar.)
An alternative would be not to use structural parameters and records,
but make each of the operations (that is, record entries) a separate
parameter. Renaming and syntax annotations in locale expressions then
give you full control over the syntax.
Clemens
Last updated: May 03 2024 at 04:19 UTC