Theory Well_Sorted_Terms
section ‹Binding Signatures and well-sorted terms›
theory Well_Sorted_Terms
imports Terms
begin
text ‹This section introduces binding signatures
and well-sorted terms for them. All the properties we proved for good terms are then
lifted to well-sorted terms.
›
subsection ‹Binding signatures›
text‹A {\em (binding) signature} consists of:
\\- an indication of which sorts of variables can be injected in
which sorts of terms;
\\- for any operation symbol, dwelling in a type ``opSym",
an indication of its result sort, its (nonbinding) arity, and its binding arity.
In addition, we have a predicate, ``wlsOpSym", that specifies which operations symbols
are well-sorted (or well-structured)
\footnote
{
We shall use ``wls" in many contexts as a prefix indicating well-sortedness or
well-structuredness.
}
-- only these operation symbols will be considered in
forming terms. In other words, the relevant collection of operation symbols is given not by the
whole type ``opSym", but by the predicate ``wlsOpSym". This bit of extra flexibility
will be useful when (pre)instantiating the signature to concrete syntaxes.
(Note that the ``wlsOpSym" condition will be required for well-sorted terms as part of the notion of
well-sorted (free and bound) input, ``wlsInp" and ``wlsBinp".)
›
record ('index,'bindex,'varSort,'sort,'opSym)signature =
varSortAsSort :: "'varSort ⇒ 'sort"
wlsOpSym :: "'opSym ⇒ bool"
sortOf :: "'opSym ⇒ 'sort"
arityOf :: "'opSym ⇒ ('index, 'sort)input"
barityOf :: "'opSym ⇒ ('bindex, 'varSort * 'sort)input"
subsection ‹The Binding Syntax locale›
text ‹For our signatures, we shall make some assumptions:
\\- For each sort of term, there is at most one sort of variables injectable
in terms of that sort (i.e., ``varSortAsSort" is injective");
\\- The domains of arities (sets of indexes) are smaller than the set of variables
of each sort;
\\- The type of sorts is smaller than the set of variables
of each sort.
These are satisfiable assumptions, and in particular they are trivially satisfied by any finitary syntax
with bindings.
›
definition varSortAsSort_inj where
"varSortAsSort_inj Delta ==
inj (varSortAsSort Delta)"
definition arityOf_lt_var where
"arityOf_lt_var (_ :: 'var) Delta ==
∀ delta.
wlsOpSym Delta delta ⟶ |{i. arityOf Delta delta i ≠ None}| <o |UNIV :: 'var set|"
definition barityOf_lt_var where
"barityOf_lt_var (_ :: 'var) Delta ==
∀ delta.
wlsOpSym Delta delta ⟶ |{i. barityOf Delta delta i ≠ None}| <o |UNIV :: 'var set|"
definition sort_lt_var where
"sort_lt_var (_ :: 'sort) (_ :: 'var) ==
|UNIV :: 'sort set| <o |UNIV :: 'var set|"
locale FixSyn =
fixes dummyV :: 'var
and Delta :: "('index,'bindex,'varSort,'sort,'opSym)signature"
assumes
FixSyn_var_infinite: "var_infinite (undefined :: 'var)"
and FixSyn_var_regular: "var_regular (undefined :: 'var)"
and varSortAsSort_inj: "varSortAsSort_inj Delta"
and arityOf_lt_var: "arityOf_lt_var (undefined :: 'var) Delta"
and barityOf_lt_var: "barityOf_lt_var (undefined :: 'var) Delta"
and sort_lt_var: "sort_lt_var (undefined :: 'sort) (undefined :: 'var)"
context FixSyn
begin
lemmas FixSyn_assms =
FixSyn_var_infinite FixSyn_var_regular
varSortAsSort_inj arityOf_lt_var barityOf_lt_var
sort_lt_var
end
subsection ‹Definitions and basic properties of well-sortedness›
subsubsection ‹Notations and definitions›