Unifying heterogeneous state-spaces with lenses

This is the web page supporting our ICTAC 2016 submission. All definition, theorems, and proofs can be located in our repository on GitHub. This page gives details of the theorem locations in those files relative to the repository.

Syntactic conventions

• Lens composition. Paper: ⨾. Isabelle: ;_L
• Unit lens. Paper: 0. Isabelle: 0_L
• Identity lens. Paper: 1. Isabelle: 1_L or Σ (the latter is used when referring to the alphabet)
• Sublens. Paper: ≼. Isabelle: ⊆_L
• Summation. Paper: ⊕. Isabelle: +_L

Theorem locations

Lenses

The lens theorems are all located in utils/Lenses.thy

3.1 Lens laws

• Weak lenses
• Well-behaved lenses
• Mainly well-behaved lenses
• Very well-behaved lenses
• Ineffectual lenses
• Bijective lenses

3.2 Concrete lenses

• Theorem 1 (Function lens is very well-behaved)
• Theorem 2 (Map lens is mainly well-behaved)

3.3 Lens algebraic operators

• Definition 2 (Lens composition)
• Definition 3 (Unit and identity lenses)
• "Lens composition and identity form a monoid"
• Definition 4 (Lens independence)
• ".. independence of function lenses corresponds to inequality of the inputs ..."
• "Lens independence is clearly a symmetric relation..."
• Definition 5 (Sublens relation)
• "... 0 is the least element ..."
• "... 1 is the greatest element ..."
• Theorem 4 (Sublens preserves independence)
• Theorem 5 (Bijective and ineffectual lenses equality)
• Definition 6 (Lens sum)
• Definition 7 (First and second lenses)
• Theorem 6 (Lens sum laws)
  • Commutativity
  • Associativity
  • Right unit
  • Distributivity
  • Upper bound
  • First + Second = 1
  • Sum preserves independence

Unifying state-space abstractions

UTP definitions and theorems are located under utp/.

4.1 Alphabetised predicate calculus

• Definition 9 (UTP expression constructs)
• Theorem 7 (Boolean Algebra)
• Theorem 8 (Complete Lattice)
• Definition 10 (Existential and universal quantifiers)
• Theorem 9 (Cylindric Algebra)
• Theorem 10 (Existential quantifier laws)

4.2 Meta-logical operators

• Definition 11 (Unrestriction)
• Theorem 11 (Unrestriction laws)
  • Expression laws
  • Predicate laws
• Definition 12 (Substitution functions)
• Theorem 12 (Substitution query laws)
• • Expression laws
  • Predicate laws
• Theorem 14 (One-point)

4.3 Relational laws of programming

• Definition 13 (Relational variables)
• Definition 14 (Relational operators)
  • Sequential composition
  • Skip
  • Conditional
  • Assignment
• Theorem 15 (Unital quantale)
• Theorem 16 (Assignment laws)
  • ASN1
  • ASN2
  • ASN3
  • ASN4

4.4 Parallel-by-merge

• Definition 15 (Separated and prior variables)
• Definition 16 (Separating simulations)
• Definition 17 (Parallel-by-merge)
• Theorem 17 (Commutativity of parallel-by-merge)