4.3 ITL library for Isabelle/HOL
Isabelle/HOL is a generic proof assistant. It allows mathematical formulas to be expressed in a formal
language and provides tools for proving those formulas in a logical calculus.
We have given a deep embedding of propositional ITL and a shallow embedding of ﬁrst order ITL in
Isabelle/HOL. A shallow embedding represents ITL using Isabelle/HOL predicates, while a deep embedding
would represent ITL formulas as mutually inductive datatypes. See, e.g., [103] for a discussion about deep
vs. shallow embeddings in Isabelle/HOL. The shallow embedding of ﬁrst order ITL uses techniques
developed by Stefan Merz [186, 23] for the shallow embedding of Temporal Logic of Actions (TLA) in
Isabelle/HOL.
4.3.1 Shallow embedding
Finite and Inﬁnite ITL
 Intervals are denoted by nonempty coinductive lists. These are a subtype of coinductive lists
formalised by Andreas Lochbihler [25].
 First Order ﬁnite ITL, both quantiﬁcation over state variables, temporal variables (current,
next, ﬁnal, penultimate), syntax, semantics, and axioms and proof rules. The encoding is similar
to that of Stephan Merz [186, 23] used for TLA in Isabelle/HOL.
 The lemmas from Imperative Reasoning in Interval Temporal Logic by Ben Moszkowski.
 The until operator for ﬁnite and inﬁnite ITL and extensive list of lemmas from [183].
 The Pi operator [80, 3] for ﬁnite and inﬁnite ITL.
 Finite and Inﬁnite Interval Temporal Algebra. This work is based on Interval Temporal Algebra
(Section 4.4) but now reencoded in Isabelle/HOL. So the work on ITL and Prover9 and PVS
has now been superseded by the Isabelle/HOL library. ITA is related to Kleene and Omega
Algebras [12].
Download:

Version 3.3 (13/09/2023) gzipped tar ﬁle
Changes:
 Fixes for Isabelle 2023.
 Ported ﬁrst and monitor operator deﬁnitions and lemmas from the ITL v2.x series.

Version 3.2 (26/10/2022) gzipped tar ﬁle
Changes:
 Ported the ﬁnite projection operator deﬁnitions and lemmas from ITLv2.x series (ﬁnite
ITL) to inﬁnite ITL. Added inﬁnite projection operator deﬁnition and lemmas.
 Added remaining lemmas for chopstar and Pi from [3]. Added lemma for omega and Pi.
 Added womega (Omega operation from Omega Algebra) deﬁnition and lemmas, these are
ported from [12]. Added corresponding lemmas for omega (omega from ITL) deﬁnition.
Added aomega (semantic version) deﬁnition and lemma stating the equivalence with the
omega deﬁnition.
 Added wpowerstar (Kleene star operation from Kleene Algebra) deﬁnition and lemmas,
these are ported from [12]. Added corresponding lemmas for schopstar (strong schopstar
from ITL) deﬁnition. Added achopstar (semantic version) deﬁnition and lemma stating
the equivalence with the schopstar deﬁnition. Added inductive deﬁnition istar and various
lemmas related them to schopstar and wpowerstar.
 Moved all chopstar related deﬁnitions and lemmas into a separate theory ﬁle.
 Moved all omega related deﬁnitions and lemmas into a separate theory ﬁle.

Version 3.1 (14/12/2021) gzipped tar ﬁle
Changes:
 Incorporate changes for Isabelle20211.
 Version 3.0 (09/04/2021, ﬁrst public release) gzipped tar ﬁle
Finite ITL
 First Order ﬁnite ITL, both quantiﬁcation over state variables, temporal variables (current,
next, ﬁnal, penultimate), syntax, semantics, and axioms and proof rules. The encoding is similar
to that of Stephan Merz [186, 23] used for TLA in Isabelle/HOL.
 The lemmas from Imperative Reasoning in Interval Temporal Logic by Ben Moszkowski.
 Time Reversal operator and an extensive list of lemmas included. Time reversal operator is
also deﬁned for temporal variables and quantiﬁcation.
 First operator and Monitors. All key theorems/lemmas/semantics in David Smallwood PhD
thesis “ITL Monitor: Compositional Runtime Analysis with Interval Temporal Logic” [161]
have been veriﬁed.
 The projection operator [134] for ﬁnite ITL.
 Finite Interval Temporal Algebra. This work is based on Interval Temporal Algebra (Section
4.4) but now reencoded in Isabelle/HOL. So the work on ITL and Prover9 and PVS has now
been superseded by the Isabelle/HOL library. ITA is related to Kleene Algebras [12].
 The until and since operator for ﬁnite ITL and extensive list of lemmas from [183].
 The Pi operator [80, 3] for ﬁnite ITL.
 Forward and backward executability of ITL formula.
Download:

Version 2.8 (14/12/2021) gzipped tar ﬁle
Changes:
 Incorporate changes for Isabelle20211.

Version 2.7 (28/02/2021) gzipped tar ﬁle
Changes:
 Added theory on executability of ITL formulae.
 Naming of deﬁnitions and lemmas is more consistent, all operations on intervals are
starting with i.
 Removed inﬁnite ITL, i.e., this version only deals with ﬁnite ITL. Inﬁnite and ﬁnite ITL
are now in the upcoming version 3.X which uses a uniform representation for ﬁnite and
inﬁnite intervals using coinductive lists.

Version 2.6 (16/04/2020) gzipped tar ﬁle
Changes:
 Added projection operator (for ﬁnite ITL), axioms and proof rules.
 Added ﬁlter operator on ﬁnite intervals and extensive list of lemmas.
 Added until and since operator (for ﬁnite ITL) and extensive list of lemmas.
 Added Pi operator (for ﬁnite ITL), axiom and proof rules.
 Added Interval Temporal Algebra (for ﬁnite ITL) from version 1.

Version 2.5 (21/07/2019, more polished version), axioms gzipped tar ﬁle.
Changes:
 Added Inﬁnite intervals, semantics, axioms and proof rules, and extensive list of lemmas.

Version 2.4 (11/06/2019, still work in progress), gzipped tar ﬁle.
Changes:
 Replaced notation deprecated in Isabelle/HOL 2019.

Version 2.3 (16/03/2019, still work in progress), gzipped tar ﬁle.
Changes:
 Use Intensional.thy from Isabelle/HOL distribution.
 Restructure First and Monitor Theories.
 Added equivalence relation on monitors.
 Restructure Example Theory.
 See ChangeLog for detailed changes.
 Version 2.2 (08/12/2018, warning this is work in progress), gzipped tar ﬁle.
4.3.2 Deep embedding
 Propositional ITL, syntax, semantics (ﬁnite intervals), and axioms and proof rules.
 The lemmas from Imperative Reasoning in Interval Temporal Logic by Ben Moszkowski.
 Time Reversal operator and an extensive list of lemmas.
 First operator and Monitors. All key theorems/lemmas/semantics in David Smallwood PhD
thesis “ITL Monitor: Compositional Runtime Analysis with Interval Temporal Logic” [161]
have been veriﬁed.
 Interval Temporal Algebra for ﬁnite interval. This work is based on Interval Temporal Algebra
(Section 4.4) but now reencoded in Isabelle/HOL. So the work on ITL and Prover9 and PVS
has now been superseded by the Isabelle/HOL library. ITA is related to Kleene Algebras [12].
Download:

Version 1.10 (11/06/2019), gzipped tar ﬁle.
Changes:
 Replaced notation deprecated in Isabelle/HOL 2019.

Version 1.9 (16/03/2019), gzipped tar ﬁle.
Changes:
 Restructure First and Monitor Theories.
 Added equivalence relation on monitors.
 See ChangeLog for detailed changes.
 Version 1.8 (08/12/2018, ﬁrst public release), gzipped tar ﬁle.