[isabelle] Concrete syntax and default structure



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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.