Session TESL_Language

Theory Introduction

chapter‹A Gentle Introduction to TESL›

(*<*)
theory Introduction
  imports Main
begin

(*>*)

section ‹Context›
text‹
The design of complex systems involves different formalisms for modeling their different parts or 
aspects. The global model of a system may therefore consist of a coordination of concurrent 
sub-models that use different paradigms such as differential equations, state machines, 
synchronous data-flow networks, 
discrete event models and so on, as illustrated in \autoref{fig:het-timed-system}. 
This raises the interest in architectural composition languages 
that allow for ``bolting the respective sub-models together'', along their various interfaces, and 
specifying the various ways of collaboration and coordination~@{cite "nguyenvan:hal-01583815"}.

We are interested in languages that allow for specifying the timed coordination of subsystems by 
addressing the following conceptual issues:
▪ events may occur in different sub-systems at unrelated times, leading to ∗‹polychronous› systems, 
  which do not necessarily have a common base clock,
▪ the behavior of the sub-systems is observed only at a series of discrete instants, and time 
  coordination has to take this ∗‹discretization› into account,
▪ the instants at which a system is observed may be arbitrary and should not change its behavior 
  (∗‹stuttering invariance›),
▪ coordination between subsystems involves causality, so the occurrence of an event may enforce 
  the occurrence of other events, possibly after a certain duration has elapsed or an event has 
  occurred a given number of times,
▪ the domain of time (discrete, rational, continuous. . . ) may be different in the subsystems, 
  leading to ∗‹polytimed› systems,
▪ the time frames of different sub-systems may be related (for instance, time in a GPS satellite 
  and in a GPS receiver on Earth are related although they are not the same).
›

text‹
\begin{figure}[htbp]
 \centering
 \includegraphics{glue.pdf}
 \caption{A Heterogeneous Timed System Model}
 \label{fig:het-timed-system}
\end{figure}›

(*<*)
― ‹Constants and notation to be able to write what we want as Isabelle terms, not as LaTeX maths›
consts dummyInfty    :: ‹'a ⇒ 'a›
consts dummyTESLSTAR :: ‹'a›
consts dummyFUN      :: ‹'a set ⇒ 'b set ⇒ 'c set›
consts dummyCLOCK    :: ‹'a set›
consts dummyBOOL     :: ‹bool set› 
consts dummyTIMES    :: ‹'a set› 
consts dummyLEQ      :: ‹'a ⇒ 'a ⇒ bool›

notation dummyInfty    (‹(_∞)› [1000] 999)
notation dummyTESLSTAR (‹TESL*›)
notation dummyFUN      (infixl ‹→› 100)
notation dummyCLOCK    (‹𝒦›) 
notation dummyBOOL     (‹𝔹›) 
notation dummyTIMES    (‹𝒯›) 
notation dummyLEQ      (infixl ‹≤𝒯› 100)
(*>*)

text‹
In order to tackle the heterogeneous nature of the subsystems, we abstract their behavior as clocks. 
Each clock models an event, i.e., something that can occur or not at a given time. This time is measured 
in a time frame associated with each clock, and the nature of time (integer, rational, real, or any 
type with a linear order) is specific to each clock. 
When the event associated with a clock occurs, the clock ticks. In order to support any kind of 
behavior for the subsystems, we are only interested in specifying what we can observe at a series 
of discrete instants. There are two constraints on observations: a clock may tick only at an 
observation instant, and the time on any clock cannot decrease from an instant to the next one. 
However, it is always possible to add arbitrary observation instants, which allows for stuttering 
and modular composition of systems. 
As a consequence, the key concept of our setting is the notion of a clock-indexed Kripke model: 
@{term ‹Σ∞ = ℕ → 𝒦 → (𝔹 × 𝒯)›}, where @{term ‹𝒦›} is an enumerable set of clocks, @{term ‹𝔹›} 
is the set of booleans – used to  indicate that a clock ticks at a given instant – and @{term ‹𝒯›} 
is a universal metric time space for which we only assume that it is large enough to contain all 
individual time spaces of clocks and that it is ordered by some linear ordering @{term ‹(≤𝒯)›}.
›

text‹
  The elements of @{term ‹Σ∞›} are called runs. A specification language is a set of 
  operators that constrains the set of possible monotonic runs. Specifications are composed by 
  intersecting the denoted run sets of constraint operators.
  Consequently, such specification languages do not limit the number of clocks used to model a 
  system (as long as it is finite) and it is always possible to add clocks to a specification. 
  Moreover, they are ∗‹compositional› by construction since the composition of specifications 
  consists of the conjunction of their constraints.
›

text‹
  This work provides the following contributions:
  ▪ defining the non-trivial language @{term ‹TESL*›} in terms of clock-indexed Kripke models, 
  ▪ proving that this denotational semantics is stuttering invariant,
  ▪ defining an adapted form of symbolic primitives and presenting the set of operational 
    semantic rules,
  ▪ presenting formal proofs for soundness, completeness, and progress of the latter.
›

section‹The TESL Language›
   
text‹
  The TESL language @{cite "BouJacHarPro2014MEMOCODE"} was initially designed to coordinate the
  execution of heterogeneous components during the simulation of a system. We define here a minimal
  kernel of operators that will form the basis of a family of specification languages, including the
  original TESL language, which is described at \url{http://wdi.supelec.fr/software/TESL/}.
›  

subsection‹Instantaneous Causal Operators›
text‹
  TESL has operators to deal with instantaneous causality, i.e., to react to an event occurrence
  in the very same observation instant.
  ▪ ▩‹c1 implies c2› means that at any instant where ▩‹c1› ticks, ▩‹c2› has to tick too.
  ▪ ▩‹c1 implies not c2› means that at any instant where ▩‹c1› ticks, ▩‹c2› cannot tick.
  ▪ ▩‹c1 kills c2› means that at any instant where ▩‹c1› ticks, and at any future instant, 
    ▩‹c2› cannot tick.
›

subsection‹Temporal Operators›
text‹
  TESL also has chronometric temporal operators that deal with dates and chronometric delays.
  ▪ ▩‹c sporadic t› means that clock ▩‹c› must have a tick at time ▩‹t› on its own time scale.
  ▪ ▩‹c1 sporadic t on c2› means that clock ▩‹c1› must have a tick at an instant where the time 
    on ▩‹c2› is ▩‹t›.
  ▪ ▩‹c1 time delayed by d on m implies c2› means that every time clock ▩‹c1› ticks, ▩‹c2› must have 
    a tick at the first instant where the time on ▩‹m› is ▩‹d› later than it was when ▩‹c1› had ticked.
    This means that every tick on ▩‹c1› is followed by a tick on ▩‹c2› after a delay ▩‹d› measured
    on the time scale of clock ▩‹m›.
  ▪ ▩‹time relation (c1, c2) in R› means that at every instant, the current time on clocks ▩‹c1›
    and ▩‹c2› must be in relation ▩‹R›. By default, the time lines of different clocks are 
    independent. This operator allows us to link two time lines, for instance to model the fact
    that time in a GPS satellite and time in a GPS receiver on Earth are not the same but are 
    related. Time being polymorphic in TESL, this can also be used to model the fact that the
    angular position on the camshaft of an engine moves twice as fast as the angular position 
    on the crankshaft~⁋‹See \url{http://wdi.supelec.fr/software/TESL/GalleryEngine} for more details›. 
    We may consider only linear arithmetic relations to restrict the problem to a domain where 
    the resolution is decidable.›

subsection‹Asynchronous Operators›
text‹
  The last category of TESL operators allows the specification of asynchronous relations between
  event occurrences. They do not specify the precise instants at which ticks have to occur, 
  they only put bounds on the set of instants at which they should occur.
  ▪ ▩‹c1 weakly precedes c2› means that for each tick on ▩‹c2›, there must be at least one tick
    on ▩‹c1› at a previous or at the same instant. This can also be expressed by stating
    that at each instant, the number of ticks since the beginning of the run must be lower or 
    equal on ▩‹c2› than on ▩‹c1›.
  ▪ ▩‹c1 strictly precedes c2› means that for each tick on ▩‹c2›, there must be at least one tick
    on ▩‹c1› at a previous instant. This can also be expressed by saying that at each instant, 
    the number of ticks on ▩‹c2› from the beginning of the run to this instant, must be lower or 
    equal to the number of ticks on ▩‹c1› from the beginning of the run to the previous instant.
›


(*<*)
no_notation dummyInfty      (‹(_∞)› )
no_notation dummyTESLSTAR   (‹TESL*›)
no_notation dummyFUN        (infixl ‹→› 100)
no_notation dummyCLOCK      (‹𝒦›) 
no_notation dummyBOOL       (‹𝔹›) 
no_notation dummyTIMES      (‹𝒯›) 
no_notation dummyLEQ        (infixl ‹≤𝒯› 100)


end
(*>*)

Theory TESL

(*chapter‹The Core of the TESL Language: Syntax and Basics›*)
text‹\chapter[Core TESL: Syntax and Basics]{The Core of the TESL Language: Syntax and Basics}›

theory TESL
imports Main

begin

section‹Syntactic Representation›
text‹
  We define here the syntax of TESL specifications.
›

subsection‹Basic elements of a specification›
text‹
  The following items appear in specifications:
  ▪ Clocks, which are identified by a name.
  ▪ Tag constants are just constants of a type which denotes the metric time space.
›

datatype     clock         = Clk ‹string›
type_synonym instant_index = ‹nat›

datatype     'τ tag_const =  TConst   (the_tag_const : 'τ)         (‹τcst›)


subsection‹Operators for the TESL language›
text‹
  The type of atomic TESL constraints, which can be combined to form specifications.
›
datatype 'τ TESL_atomic =
    SporadicOn       ‹clock› ‹'τ tag_const›  ‹clock›  (‹_ sporadic _ on _› 55)
  | TagRelation      ‹clock› ‹clock› ‹('τ tag_const × 'τ tag_const) ⇒ bool› 
                                                      (‹time-relation ⌊_, _⌋ ∈ _› 55)
  | Implies          ‹clock› ‹clock›                  (infixr ‹implies› 55)
  | ImpliesNot       ‹clock› ‹clock›                  (infixr ‹implies not› 55)
  | TimeDelayedBy    ‹clock› ‹'τ tag_const› ‹clock› ‹clock› 
                                                      (‹_ time-delayed by _ on _ implies _› 55)
  | WeaklyPrecedes   ‹clock› ‹clock›                  (infixr ‹weakly precedes› 55)
  | StrictlyPrecedes ‹clock› ‹clock›                  (infixr ‹strictly precedes› 55)
  | Kills            ‹clock› ‹clock›                  (infixr ‹kills› 55)

text‹
  A TESL formula is just a list of atomic constraints, with implicit conjunction
  for the semantics.
›
type_synonym 'τ TESL_formula = ‹'τ TESL_atomic list›

text‹
  We call ∗‹positive atoms› the atomic constraints that create ticks from nothing.
  Only sporadic constraints are positive in the current version of TESL.
›
fun positive_atom :: ‹'τ TESL_atomic ⇒ bool› where
    ‹positive_atom (_ sporadic _ on _) = True›
  | ‹positive_atom _                   = False›

text‹
  The @{term ‹NoSporadic›} function removes sporadic constraints from a TESL formula.
›
abbreviation NoSporadic :: ‹'τ TESL_formula ⇒ 'τ TESL_formula›
where 
  ‹NoSporadic f ≡ (List.filter (λfatom. case fatom of
      _ sporadic _ on _ ⇒ False
    | _ ⇒ True) f)›

subsection‹Field Structure of the Metric Time Space›
text‹
  In order to handle tag relations and delays, tags must belong to a field.
  We show here that this is the case when the type parameter of @{typ ‹'τ tag_const›} 
  is itself a field.
›
instantiation tag_const ::(field)field
begin
  fun inverse_tag_const
  where ‹inverse (τcst t) = τcst (inverse t)›

  fun divide_tag_const 
    where ‹divide (τcst t1) (τcst t2) = τcst (divide t1 t2)›

  fun uminus_tag_const
    where ‹uminus (τcst t) = τcst (uminus t)›

fun minus_tag_const
  where ‹minus (τcst t1) (τcst t2) = τcst (minus t1 t2)›

definition ‹one_tag_const ≡ τcst 1›

fun times_tag_const
  where ‹times (τcst t1) (τcst t2) = τcst (times t1 t2)›

definition ‹zero_tag_const ≡ τcst 0›

fun plus_tag_const
  where ‹plus (τcst t1) (τcst t2) = τcst (plus t1 t2)›

instance proof
  text‹Multiplication is associative.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
                               and c::‹'τ::field tag_const›
  obtain u v w where ‹a = τcst u› and ‹b = τcst v› and ‹c = τcst w›
    using tag_const.exhaust by metis
  thus ‹a * b * c = a * (b * c)›
    by (simp add: TESL.times_tag_const.simps)
next
  text‹Multiplication is commutative.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
  obtain u v where ‹a = τcst u› and ‹b = τcst v› using tag_const.exhaust by metis
  thus ‹ a * b = b * a›
    by (simp add: TESL.times_tag_const.simps)
next
  text‹One is neutral for multiplication.›
  fix a::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  thus ‹1 * a = a›
    by (simp add: TESL.times_tag_const.simps one_tag_const_def)
next
  text‹Addition is associative.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
                               and c::‹'τ::field tag_const›
  obtain u v w where ‹a = τcst u› and ‹b = τcst v› and ‹c = τcst w›
    using tag_const.exhaust by metis
  thus ‹a + b + c = a + (b + c)›
    by (simp add: TESL.plus_tag_const.simps)
next
  text‹Addition is commutative.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
  obtain u v where ‹a = τcst u› and ‹b = τcst v› using tag_const.exhaust by metis
  thus ‹a + b = b + a›
    by (simp add: TESL.plus_tag_const.simps)
next
  text‹Zero is neutral for addition.›
  fix a::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  thus ‹0 + a = a›
    by (simp add: TESL.plus_tag_const.simps zero_tag_const_def)
next
  text‹The sum of an element and its opposite is zero.›
  fix a::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  thus ‹-a + a = 0›
    by (simp add: TESL.plus_tag_const.simps
                  TESL.uminus_tag_const.simps
                  zero_tag_const_def)
next
  text‹Subtraction is adding the opposite.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
  obtain u v where ‹a = τcst u› and ‹b = τcst v› using tag_const.exhaust by metis
  thus ‹a - b = a + -b›
    by (simp add: TESL.minus_tag_const.simps
                  TESL.plus_tag_const.simps
                  TESL.uminus_tag_const.simps)
next
  text‹Distributive property of multiplication over addition.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
                               and c::‹'τ::field tag_const›
  obtain u v w where ‹a = τcst u› and ‹b = τcst v› and ‹c = τcst w›
    using tag_const.exhaust by metis
  thus ‹(a + b) * c = a * c + b * c›
    by (simp add: TESL.plus_tag_const.simps
                  TESL.times_tag_const.simps
                  ring_class.ring_distribs(2))
next
  text‹The neutral elements are distinct.›
  show ‹(0::('τ::field tag_const)) ≠ 1›
    by (simp add: one_tag_const_def zero_tag_const_def)
next
  text‹The product of an element and its inverse is 1.›
  fix a::‹'τ::field tag_const› assume h:‹a ≠ 0›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  moreover with h have ‹u ≠ 0› by (simp add: zero_tag_const_def)
  ultimately show ‹inverse a * a = 1›
    by (simp add: TESL.inverse_tag_const.simps
                  TESL.times_tag_const.simps
                  one_tag_const_def)
next
  text‹Dividing is multiplying by the inverse.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
  obtain u v where ‹a = τcst u› and ‹b = τcst v› using tag_const.exhaust by metis
  thus ‹a div b = a * inverse b›
    by (simp add: TESL.divide_tag_const.simps
                  TESL.inverse_tag_const.simps
                  TESL.times_tag_const.simps
                  divide_inverse)
next
  text‹Zero is its own inverse.›
  show ‹inverse (0::('τ::field tag_const)) = 0›
    by (simp add: TESL.inverse_tag_const.simps zero_tag_const_def)
qed

end

text‹
  For comparing dates (which are represented by tags) on clocks, we need an order on tags.
›

instantiation tag_const :: (order)order
begin
  inductive less_eq_tag_const :: ‹'a tag_const ⇒ 'a tag_const ⇒ bool›
  where
    Int_less_eq[simp]:      ‹n ≤ m ⟹ (TConst n) ≤ (TConst m)›

  definition less_tag: ‹(x::'a tag_const) < y ⟷ (x ≤ y) ∧ (x ≠ y)›

  instance proof
    show ‹⋀x y :: 'a tag_const. (x < y) = (x ≤ y ∧ ¬ y ≤ x)›
      using less_eq_tag_const.simps less_tag by auto
  next
    fix x::‹'a tag_const›
    from tag_const.exhaust obtain x0::'a where ‹x = TConst x0› by blast
    with Int_less_eq show ‹x ≤ x› by simp
  next
    show ‹⋀x y z  :: 'a tag_const. x ≤ y ⟹ y ≤ z ⟹ x ≤ z›
      using less_eq_tag_const.simps by auto
  next
    show ‹⋀x y  :: 'a tag_const. x ≤ y ⟹ y ≤ x ⟹ x = y›
      using less_eq_tag_const.simps by auto
  qed

end

text‹
  For ensuring that time does never flow backwards, we need a total order on tags.
›
instantiation tag_const :: (linorder)linorder
begin
  instance proof
    fix x::‹'a tag_const› and y::‹'a tag_const›
    from tag_const.exhaust obtain x0::'a where ‹x = TConst x0› by blast
    moreover from tag_const.exhaust obtain y0::'a where ‹y = TConst y0› by blast
    ultimately show ‹x ≤ y ∨ y ≤ x› using less_eq_tag_const.simps by fastforce
  qed

end

end

Theory Run

section ‹ Defining Runs ›

theory Run
imports TESL
      
begin
text ‹
  Runs are sequences of instants, and each instant maps a clock to a pair 
  @{term ‹(h, t)›} where @{term ‹h›} indicates whether the clock ticks or not, 
  and @{term ‹t›} is the current time on this clock.
  The first element of the pair is called the ∗‹hamlet› of the clock (to tick or 
  not to tick), the second element is called the ∗‹time›.
›

abbreviation hamlet where ‹hamlet ≡ fst›
abbreviation time   where ‹time ≡ snd›

type_synonym 'τ instant = ‹clock ⇒ (bool × 'τ tag_const)›

text‹
  Runs have the additional constraint that time cannot go backwards on any clock
  in the sequence of instants.
  Therefore, for any clock, the time projection of a run is monotonous.
›
typedef (overloaded) 'τ::linordered_field run =
  ‹{ ρ::nat ⇒ 'τ instant. ∀c. mono (λn. time (ρ n c)) }›
proof
  show ‹(λ_ _. (True, τcst 0)) ∈ {ρ. ∀c. mono (λn. time (ρ n c))}› 
    unfolding mono_def by blast
qed

lemma Abs_run_inverse_rewrite:
  ‹∀c. mono (λn. time (ρ n c)) ⟹ Rep_run (Abs_run ρ) = ρ›
by (simp add: Abs_run_inverse)

text ‹
  A ∗‹dense› run is a run in which something happens (at least one clock ticks) 
  at every instant.
›
definition ‹dense_run ρ ≡ (∀n. ∃c. hamlet ((Rep_run ρ) n c))›

text‹
  @{term ‹run_tick_count ρ K n›} counts the number of ticks on clock @{term ‹K›} 
  in the interval ▩‹[0, n]› of run @{term ‹ρ›}.
›
fun run_tick_count :: ‹('τ::linordered_field) run ⇒ clock ⇒ nat ⇒ nat›
  (‹#≤ _ _ _›)
where
  ‹(#≤ ρ K 0)       = (if hamlet ((Rep_run ρ) 0 K)
                       then 1
                       else 0)›
| ‹(#≤ ρ K (Suc n)) = (if hamlet ((Rep_run ρ) (Suc n) K)
                       then 1 + (#≤ ρ K n)
                       else (#≤ ρ K n))›

text‹
  @{term ‹run_tick_count_strictly ρ K n›} counts the number of ticks on
  clock @{term ‹K›} in the interval ▩‹[0, n[› of run @{term ‹ρ›}.
›
fun run_tick_count_strictly :: ‹('τ::linordered_field) run ⇒ clock ⇒ nat ⇒ nat›
  (‹#< _ _ _›)
where
  ‹(#< ρ K 0)       = 0›
| ‹(#< ρ K (Suc n)) = #≤ ρ K n›

text‹
  @{term ‹first_time ρ K n τ›} tells whether instant @{term ‹n›} in run @{term‹ρ›}
  is the first one where the time on clock @{term ‹K›} reaches @{term ‹τ›}.
›
definition first_time :: ‹'a::linordered_field run ⇒ clock ⇒ nat ⇒ 'a tag_const
                          ⇒ bool›
where
  ‹first_time ρ K n τ ≡ (time ((Rep_run ρ) n K) = τ)
                      ∧ (∄n'. n' < n ∧ time ((Rep_run ρ) n' K) = τ)›

text‹
  The time on a clock is necessarily less than @{term ‹τ›} before the first instant
  at which it reaches @{term ‹τ›}.
›
lemma before_first_time:
  assumes ‹first_time ρ K n τ›
      and ‹m < n›
    shows ‹time ((Rep_run ρ) m K) < τ›
proof -
  have ‹mono (λn. time (Rep_run ρ n K))› using Rep_run by blast
  moreover from assms(2) have ‹m ≤ n› using less_imp_le by simp
  moreover have ‹mono (λn. time (Rep_run ρ n K))› using Rep_run by blast
  ultimately have  ‹time ((Rep_run ρ) m K) ≤ time ((Rep_run ρ) n K)›
    by (simp add:mono_def)
  moreover from assms(1) have ‹time ((Rep_run ρ) n K) = τ›
    using first_time_def by blast
  moreover from assms have ‹time ((Rep_run ρ) m K) ≠ τ›
    using first_time_def by blast
  ultimately show ?thesis by simp
qed

text‹
  This leads to an alternate definition of @{term ‹first_time›}:
›
lemma alt_first_time_def:
  assumes ‹∀m < n. time ((Rep_run ρ) m K) < τ›
      and ‹time ((Rep_run ρ) n K) = τ›
    shows ‹first_time ρ K n τ›
proof -
  from assms(1) have ‹∀m < n. time ((Rep_run ρ) m K) ≠ τ›
    by (simp add: less_le)
  with assms(2) show ?thesis by (simp add: first_time_def)
qed

end

Theory Denotational

chapter ‹Denotational Semantics›

theory Denotational
imports
    TESL
    Run

begin
text‹
  The denotational semantics maps TESL formulae to sets of satisfying runs.
  Firstly, we define the semantics of atomic formulae (basic constructs of the 
  TESL language), then we define the semantics of compound formulae as the
  intersection of the semantics of their components: a run must satisfy all
  the individual formulae of a compound formula.
›
section ‹Denotational interpretation for atomic TESL formulae›
(*<*)
consts dummyT0 ::‹'τ tag_const›
consts dummyDeltaT ::‹'τ tag_const›

notation dummyT0     (‹t0›)
notation dummyDeltaT (‹δt›)
(*>*)

fun TESL_interpretation_atomic
    :: ‹('τ::linordered_field) TESL_atomic ⇒ 'τ run set› (‹⟦ _ ⟧TESL›)
where
  ― ‹@{term ‹K1 sporadic τ on K2›} means that @{term ‹K1›} should tick at an 
      instant where the time on @{term ‹K2›} is @{term ‹τ›}.›
    ‹⟦ K1 sporadic τ on K2 ⟧TESL =
        {ρ. ∃n::nat. hamlet ((Rep_run ρ) n K1) ∧ time ((Rep_run ρ) n K2) = τ}›
  ― ‹@{term ‹time-relation ⌊K1, K2⌋ ∈ R›} means that at each instant, the time 
      on @{term ‹K1›} and the time on @{term ‹K2›} are in relation~@{term ‹R›}.›
  | ‹⟦ time-relation ⌊K1, K2⌋ ∈ R ⟧TESL =
        {ρ. ∀n::nat. R (time ((Rep_run ρ) n K1), time ((Rep_run ρ) n K2))}›
  ― ‹@{term ‹master implies slave›} means that at each instant at which 
      @{term ‹master›} ticks, @{term ‹slave›} also ticks.›
  | ‹⟦ master implies slave ⟧TESL =
        {ρ. ∀n::nat. hamlet ((Rep_run ρ) n master) ⟶ hamlet ((Rep_run ρ) n slave)}›
  ― ‹@{term ‹master implies not slave›} means that at each instant at which 
      @{term ‹master›} ticks, @{term ‹slave›} does not tick.›
  | ‹⟦ master implies not slave ⟧TESL =
        {ρ. ∀n::nat. hamlet ((Rep_run ρ) n master) ⟶ ¬hamlet ((Rep_run ρ) n slave)}›
  ― ‹@{term ‹master time-delayed by δτ on measuring implies slave›} means that 
      at each instant at which  @{term ‹master›} ticks, @{term ‹slave›} will
      tick after a delay @{term ‹δτ›} measured on the time scale 
      of @{term ‹measuring›}.›
  | ‹⟦ master time-delayed by δτ on measuring implies slave ⟧TESL =
    ― ‹
      When master ticks, let's call @{term ‹t0›} the current date on measuring. Then, 
      at the first instant when the date on measuring is @{term ‹t0+δt›}, 
      slave has to tick.
    ›
        {ρ. ∀n. hamlet ((Rep_run ρ) n master) ⟶
                 (let measured_time = time ((Rep_run ρ) n measuring) in
                  ∀m ≥ n.  first_time ρ measuring m (measured_time + δτ)
                            ⟶ hamlet ((Rep_run ρ) m slave)
                 )
        }›
  ― ‹@{term ‹K1 weakly precedes K2›} means that each tick on @{term ‹K2›}
        must be preceded by or coincide with at least one tick on @{term ‹K1›}.
        Therefore, at each instant @{term ‹n›}, the number of ticks on @{term ‹K2›} 
        must be less or equal to the number of ticks on @{term ‹K1›}.›
  | ‹⟦ K1 weakly precedes K2 ⟧TESL =
        {ρ. ∀n::nat. (run_tick_count ρ K2 n) ≤ (run_tick_count ρ K1 n)}›
  ― ‹@{term ‹K1 strictly precedes K2›} means that each tick on @{term ‹K2›}
        must be preceded by at least one tick on @{term ‹K1›} at a previous instant.
        Therefore, at each instant n, the number of ticks on @{term ‹K2›}
        must be less or equal to the number of ticks on @{term ‹K1›} 
        at instant n - 1.›
  | ‹⟦ K1 strictly precedes K2 ⟧TESL =
        {ρ. ∀n::nat. (run_tick_count ρ K2 n) ≤ (run_tick_count_strictly ρ K1 n)}›
  ― ‹@{term ‹K1 kills K2›} means that when @{term ‹K1›} ticks, @{term ‹K2›}
        cannot tick and is not allowed to tick at any further instant.›
  | ‹⟦ K1 kills K2 ⟧TESL =
        {ρ. ∀n::nat. hamlet ((Rep_run ρ) n K1)
                        ⟶ (∀m≥n. ¬ hamlet ((Rep_run ρ) m K2))}›

section ‹Denotational interpretation for TESL formulae›

text‹
  To satisfy a formula, a run has to satisfy the conjunction of its atomic 
  formulae. Therefore, the interpretation of a formula is the intersection
  of the interpretations of its components.
›
fun TESL_interpretation :: ‹('τ::linordered_field) TESL_formula ⇒ 'τ run set›
  (‹⟦⟦ _ ⟧⟧TESL›)
where
  ‹⟦⟦ [] ⟧⟧TESL = {_. True}›
| ‹⟦⟦ φ # Φ ⟧⟧TESL = ⟦ φ ⟧TESL ∩ ⟦⟦ Φ ⟧⟧TESL›

lemma TESL_interpretation_homo:
  ‹⟦ φ ⟧TESL ∩ ⟦⟦ Φ ⟧⟧TESL = ⟦⟦ φ # Φ ⟧⟧TESL›
by simp

subsection ‹Image interpretation lemma›

theorem TESL_interpretation_image:
  ‹⟦⟦ Φ ⟧⟧TESL = ⋂ ((λφ. ⟦ φ ⟧TESL) ` set Φ)›
by (induction Φ, simp+)

subsection ‹Expansion law›
text ‹Similar to the expansion laws of lattices.›

theorem TESL_interp_homo_append:
  ‹⟦⟦ Φ1 @ Φ2 ⟧⟧TESL = ⟦⟦ Φ1 ⟧⟧TESL ∩ ⟦⟦ Φ2 ⟧⟧TESL›
by (induction Φ1, simp, auto)

section ‹Equational laws for the denotation of TESL formulae›

lemma TESL_interp_assoc:
  ‹⟦⟦ (Φ1 @ Φ2) @ Φ3 ⟧⟧TESL = ⟦⟦ Φ1 @ (Φ2 @ Φ3) ⟧⟧TESL›
by auto

lemma TESL_interp_commute:
  shows ‹⟦⟦ Φ1 @ Φ2 ⟧⟧TESL = ⟦⟦ Φ2 @ Φ1 ⟧⟧TESL›
by (simp add: TESL_interp_homo_append inf_sup_aci(1))

lemma TESL_interp_left_commute:
  ‹⟦⟦ Φ1 @ (Φ2 @ Φ3) ⟧⟧TESL = ⟦⟦ Φ2 @ (Φ1 @ Φ3) ⟧⟧TESL›
unfolding TESL_interp_homo_append by auto

lemma TESL_interp_idem:
  ‹⟦⟦ Φ @ Φ ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL›
using TESL_interp_homo_append by auto

lemma TESL_interp_left_idem:
  ‹⟦⟦ Φ1 @ (Φ1 @ Φ2) ⟧⟧TESL = ⟦⟦ Φ1 @ Φ2 ⟧⟧TESL›
using TESL_interp_homo_append by auto

lemma TESL_interp_right_idem:
  ‹⟦⟦ (Φ1 @ Φ2) @ Φ2 ⟧⟧TESL = ⟦⟦ Φ1 @ Φ2 ⟧⟧TESL›
unfolding TESL_interp_homo_append by auto

lemmas TESL_interp_aci = TESL_interp_commute
                         TESL_interp_assoc
                         TESL_interp_left_commute
                         TESL_interp_left_idem

text ‹The empty formula is the identity element.›
lemma TESL_interp_neutral1:
  ‹⟦⟦ [] @ Φ ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL›
by simp

lemma TESL_interp_neutral2:
  ‹⟦⟦ Φ @ [] ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL›
by simp

section ‹Decreasing interpretation of TESL formulae›
text‹
  Adding constraints to a TESL formula reduces the number of satisfying runs.
›
lemma TESL_sem_decreases_head:
  ‹⟦⟦ Φ ⟧⟧TESL ⊇ ⟦⟦ φ # Φ ⟧⟧TESL›
by simp

lemma TESL_sem_decreases_tail:
  ‹⟦⟦ Φ ⟧⟧TESL ⊇ ⟦⟦ Φ @ [φ] ⟧⟧TESL›
by (simp add: TESL_interp_homo_append)

text ‹
  Repeating a formula in a specification does not change the specification.
›
lemma TESL_interp_formula_stuttering:
  assumes ‹φ ∈ set Φ›
    shows ‹⟦⟦ φ # Φ ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL›
proof -
  have ‹φ # Φ = [φ] @ Φ› by simp
  hence ‹⟦⟦ φ # Φ ⟧⟧TESL = ⟦⟦ [φ] ⟧⟧TESL ∩ ⟦⟦ Φ ⟧⟧TESL›
    using TESL_interp_homo_append by simp
  thus ?thesis using assms TESL_interpretation_image by fastforce
qed

text ‹
  Removing duplicate formulae in a specification does not change the specification.
›
lemma TESL_interp_remdups_absorb:
  ‹⟦⟦ Φ ⟧⟧TESL = ⟦⟦ remdups Φ ⟧⟧TESL›
proof (induction Φ)
  case Cons
    thus ?case using TESL_interp_formula_stuttering by auto
qed simp

text ‹
  Specifications that contain the same formulae have the same semantics.
›
lemma TESL_interp_set_lifting:
  assumes ‹set Φ = set Φ'›
    shows ‹⟦⟦ Φ ⟧⟧TESL = ⟦⟦ Φ' ⟧⟧TESL›
proof -     
  have ‹set (remdups Φ) = set (remdups Φ')›
    by (simp add: assms)
  moreover have fxpntΦ: ‹⋂ ((λφ. ⟦ φ ⟧TESL) ` set Φ) = ⟦⟦ Φ ⟧⟧TESL›
    by (simp add: TESL_interpretation_image)
  moreover have fxpntΦ': ‹⋂ ((λφ. ⟦ φ ⟧TESL) ` set Φ') = ⟦⟦ Φ' ⟧⟧TESL›
    by (simp add: TESL_interpretation_image)
  moreover have ‹⋂ ((λφ. ⟦ φ ⟧TESL) ` set Φ) = ⋂ ((λφ. ⟦ φ ⟧TESL) ` set Φ')›
    by (simp add: assms)
  ultimately show ?thesis using TESL_interp_remdups_absorb by auto
qed

text ‹
  The semantics of specifications is contravariant with respect to their inclusion.
›
theorem TESL_interp_decreases_setinc:
  assumes ‹set Φ ⊆ set Φ'›
    shows ‹⟦⟦ Φ ⟧⟧TESL ⊇ ⟦⟦ Φ' ⟧⟧TESL›
proof -
  obtain Φr where decompose: ‹set (Φ @ Φr) = set Φ'› using assms by auto
  hence ‹set (Φ @ Φr) = set Φ'› using assms by blast
  moreover have ‹(set Φ) ∪ (set Φr) = set Φ'›
    using assms decompose by auto
  moreover have ‹⟦⟦ Φ' ⟧⟧TESL = ⟦⟦ Φ @ Φr ⟧⟧TESL›
    using TESL_interp_set_lifting decompose by blast
  moreover have ‹⟦⟦ Φ @ Φr ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL ∩ ⟦⟦ Φr ⟧⟧TESL›
    by (simp add: TESL_interp_homo_append)
  moreover have ‹⟦⟦ Φ ⟧⟧TESL ⊇ ⟦⟦ Φ ⟧⟧TESL ∩ ⟦⟦ Φr ⟧⟧TESL› by simp
  ultimately show ?thesis by simp
qed

lemma TESL_interp_decreases_add_head:
  assumes ‹set Φ ⊆ set Φ'›
    shows ‹⟦⟦ φ # Φ ⟧⟧TESL ⊇ ⟦⟦ φ # Φ' ⟧⟧TESL›
using assms TESL_interp_decreases_setinc by auto

lemma TESL_interp_decreases_add_tail:
  assumes ‹set Φ ⊆ set Φ'›
    shows ‹⟦⟦ Φ @ [φ] ⟧⟧TESL ⊇ ⟦⟦ Φ' @ [φ] ⟧⟧TESL›
using TESL_interp_decreases_setinc[OF assms] 
  by (simp add: TESL_interpretation_image dual_order.trans)

lemma TESL_interp_absorb1:
  assumes ‹set Φ1 ⊆ set Φ2›
    shows ‹⟦⟦ Φ1 @ Φ2 ⟧⟧TESL = ⟦⟦ Φ2 ⟧⟧TESL›
by (simp add: Int_absorb1 TESL_interp_decreases_setinc
                          TESL_interp_homo_append assms)

lemma TESL_interp_absorb2:
  assumes ‹set Φ2 ⊆ set Φ1›
    shows ‹⟦⟦ Φ1 @ Φ2 ⟧⟧TESL = ⟦⟦ Φ1 ⟧⟧TESL›
using TESL_interp_absorb1 TESL_interp_commute assms by blast

section ‹Some special cases›

lemma NoSporadic_stable [simp]:
  ‹⟦⟦ Φ ⟧⟧TESL ⊆ ⟦⟦ NoSporadic Φ ⟧⟧TESL›
proof -
  from filter_is_subset have ‹set (NoSporadic Φ) ⊆ set Φ› .
  from TESL_interp_decreases_setinc[OF this] show ?thesis .
qed

lemma NoSporadic_idem [simp]:
  ‹⟦⟦ Φ ⟧⟧TESL ∩ ⟦⟦ NoSporadic Φ ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL›
using NoSporadic_stable by blast

lemma NoSporadic_setinc:
  ‹set (NoSporadic Φ) ⊆ set Φ›
by (rule filter_is_subset)

(*<*)
no_notation dummyT0    (‹t0›)
no_notation dummyDeltaT (‹δt›)
(*>*)

end

Theory SymbolicPrimitive

chapter ‹Symbolic Primitives for Building Runs›

theory SymbolicPrimitive
  imports Run

begin

text‹
  We define here the primitive constraints on runs, towards which we translate
  TESL specifications in the operational semantics.
  These constraints refer to a specific symbolic run and can therefore access
  properties of the run at particular instants (for instance, the fact that a clock
  ticks at instant @{term ‹n›} of the run, or the time on a given clock at 
  that instant).

  In the previous chapters, we had no reference to particular instants of a run 
  because the TESL language should be invariant by stuttering in order to allow 
  the composition of specifications: adding an instant where no clock ticks to 
  a run that satisfies a formula should yield another run that satisfies the 
  same formula. However, when constructing runs that satisfy a formula, we
  need to be able to refer to the time or hamlet of a clock at a given instant.
›

text‹
  Counter expressions are used to get the number of ticks of a clock up to 
  (strictly or not) a given instant index.
›
datatype cnt_expr =
  TickCountLess ‹clock› ‹instant_index› (‹#<›)
| TickCountLeq ‹clock› ‹instant_index›  (‹#≤›)

subsection‹ Symbolic Primitives for Runs ›

text‹
  Tag values are used to refer to the time on a clock at a given instant index.
›
datatype tag_val =
  TSchematic ‹clock * instant_index› (‹τvar›)

datatype 'τ constr =
― ‹@{term ‹c ⇓ n @ τ›} constrains clock @{term ‹c›} to have time @{term ‹τ›}
    at instant @{term ‹n›} of the run.›
  Timestamp     ‹clock›   ‹instant_index› ‹'τ tag_const›         (‹_ ⇓ _ @ _›)
― ‹@{term ‹m @ n ⊕ δt ⇒ s›} constrains clock @{term ‹s›} to tick at the
    first instant at which the time on @{term ‹m›} has increased by @{term ‹δt›}
    from the value it had at instant @{term ‹n›} of the run.›
| TimeDelay     ‹clock›   ‹instant_index› ‹'τ tag_const› ‹clock› (‹_ @ _ ⊕ _ ⇒ _›)
― ‹@{term ‹c ⇑ n›} constrains clock @{term ‹c›} to tick
    at instant @{term ‹n›} of the run.›
| Ticks         ‹clock›   ‹instant_index›                        (‹_ ⇑ _›)
― ‹@{term ‹c ¬⇑ n›} constrains clock @{term ‹c›} not to tick
    at instant @{term ‹n›} of the run.›
| NotTicks      ‹clock›   ‹instant_index›                        (‹_ ¬⇑ _›)
― ‹@{term ‹c ¬⇑ < n›} constrains clock @{term ‹c›} not to tick
    before instant @{term ‹n›} of the run.›
| NotTicksUntil ‹clock›   ‹instant_index›                        (‹_ ¬⇑ < _›)
― ‹@{term ‹c ¬⇑ ≥ n›} constrains clock @{term ‹c›} not to tick
    at and after instant @{term ‹n›} of the run.›
| NotTicksFrom  ‹clock›   ‹instant_index›                        (‹_ ¬⇑ ≥ _›)
― ‹@{term ‹⌊τ1, τ2⌋ ∈ R›} constrains tag variables @{term ‹τ1›} and  @{term ‹τ2›} 
    to be in relation @{term ‹R›}.›
| TagArith      ‹tag_val› ‹tag_val› ‹('τ tag_const × 'τ tag_const) ⇒ bool› (‹⌊_, _⌋ ∈ _›)
― ‹@{term ‹⌈k1, k2⌉ ∈ R›} constrains counter expressions @{term ‹k1›} and  @{term ‹k2›} 
    to be in relation @{term ‹R›}.›
| TickCntArith  ‹cnt_expr› ‹cnt_expr› ‹(nat × nat) ⇒ bool›      (‹⌈_, _⌉ ∈ _›)
― ‹@{term ‹k1 ≼ k2›} constrains counter expression @{term ‹k1›} to be less or equal 
    to counter expression @{term ‹k2›}.›
| TickCntLeq    ‹cnt_expr› ‹cnt_expr›                            (‹_ ≼ _›)

type_synonym 'τ system = ‹'τ constr list›


text ‹
  The abstract machine has configurations composed of:
  ▪ the past @{term‹Γ›}, which captures choices that have already be made as a 
    list of symbolic primitive constraints on the run;
  ▪ the current index @{term ‹n›}, which is the index of the present instant;
  ▪ the present @{term‹Ψ›}, which captures the formulae that must be satisfied
    in the current instant;
  ▪ the future @{term‹Φ›}, which captures the constraints on the future of the run.
›
type_synonym 'τ config =
                ‹'τ system * instant_index * 'τ TESL_formula * 'τ TESL_formula›


section ‹Semantics of Primitive Constraints ›

text‹
  The semantics of the primitive constraints is defined in a way similar to
  the semantics of TESL formulae.
›
fun counter_expr_eval :: ‹('τ::linordered_field) run ⇒ cnt_expr ⇒ nat›
  (‹⟦ _ ⊢ _ ⟧cntexpr›)
where
  ‹⟦ ρ ⊢ #< clk indx ⟧cntexpr = run_tick_count_strictly ρ clk indx›
| ‹⟦ ρ ⊢ #≤ clk indx ⟧cntexpr = run_tick_count ρ clk indx›


fun symbolic_run_interpretation_primitive
  ::‹('τ::linordered_field) constr ⇒ 'τ run set› (‹⟦ _ ⟧prim›)
where
  ‹⟦ K ⇑ n  ⟧prim     = {ρ. hamlet ((Rep_run ρ) n K) }›
| ‹⟦ K @ n0 ⊕ δt ⇒ K' ⟧prim =
                  {ρ. ∀n ≥ n0. first_time ρ K n (time ((Rep_run ρ) n0 K) + δt)
                               ⟶ hamlet ((Rep_run ρ) n K')}›
| ‹⟦ K ¬⇑ n ⟧prim     = {ρ. ¬hamlet ((Rep_run ρ) n K) }›
| ‹⟦ K ¬⇑ < n ⟧prim   = {ρ. ∀i < n. ¬ hamlet ((Rep_run ρ) i K)}›
| ‹⟦ K ¬⇑ ≥ n ⟧prim   = {ρ. ∀i ≥ n. ¬ hamlet ((Rep_run ρ) i K) }›
| ‹⟦ K ⇓ n @ τ ⟧prim = {ρ. time ((Rep_run ρ) n K) = τ }›
| ‹⟦ ⌊τvar(K1, n1), τvar(K2, n2)⌋ ∈ R ⟧prim =
    { ρ. R (time ((Rep_run ρ) n1 K1), time ((Rep_run ρ) n2 K2)) }›
| ‹⟦ ⌈e1, e2⌉ ∈ R ⟧prim = { ρ. R (⟦ ρ ⊢ e1 ⟧cntexpr, ⟦ ρ ⊢ e2 ⟧cntexpr) }›
| ‹⟦ cnt_e1 ≼ cnt_e2 ⟧prim = { ρ. ⟦ ρ ⊢ cnt_e1 ⟧cntexpr ≤ ⟦ ρ ⊢ cnt_e2 ⟧cntexpr }›

text‹
  The composition of primitive constraints is their conjunction, and we get the
  set of satisfying runs by intersection.
›
fun symbolic_run_interpretation
  ::‹('τ::linordered_field) constr list ⇒ ('τ::linordered_field) run set›
  (‹⟦⟦ _ ⟧⟧prim›)
where
  ‹⟦⟦ [] ⟧⟧prim = {ρ. True }›
| ‹⟦⟦ γ # Γ ⟧⟧prim = ⟦ γ ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim›

lemma symbolic_run_interp_cons_morph:
  ‹⟦ γ ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim = ⟦⟦ γ # Γ ⟧⟧prim›
by auto

definition consistent_context :: ‹('τ::linordered_field) constr list ⇒ bool›
where 
  ‹consistent_context Γ ≡ ( ⟦⟦ Γ ⟧⟧prim ≠ {}) ›

subsection ‹Defining a method for witness construction›

text‹
  In order to build a run, we can start from an initial run in which no clock 
  ticks and the time is always 0 on any clock.
›
abbreviation initial_run :: ‹('τ::linordered_field) run› (‹ρ⊙›) where
  ‹ρ⊙ ≡ Abs_run ((λ_ _. (False, τcst 0)) ::nat ⇒ clock ⇒ (bool × 'τ tag_const))›

text‹
  To help avoiding that time flows backward, setting the time on a clock at a given 
  instant sets it for the future instants too.
›
fun time_update
  :: ‹nat ⇒ clock ⇒ ('τ::linordered_field) tag_const ⇒ (nat ⇒ 'τ instant)
      ⇒ (nat ⇒ 'τ instant)›
where
  ‹time_update n K τ ρ = (λn' K'. if K = K' ∧ n ≤ n'
                                  then (hamlet (ρ n K), τ)
                                  else ρ n' K')›


section ‹Rules and properties of consistence›

lemma context_consistency_preservationI:
  ‹consistent_context ((γ::('τ::linordered_field) constr)#Γ) ⟹ consistent_context Γ›
unfolding consistent_context_def by auto

― ‹This is very restrictive›
inductive context_independency
  ::‹('τ::linordered_field) constr ⇒ 'τ constr list ⇒ bool› (‹_ ⨝ _›)
where
  NotTicks_independency:
  ‹(K ⇑ n) ∉ set Γ ⟹ (K ¬⇑ n) ⨝ Γ›
| Ticks_independency:
  ‹(K ¬⇑ n) ∉ set Γ ⟹ (K ⇑ n) ⨝ Γ›
| Timestamp_independency:
  ‹(∄τ'. τ' = τ ∧ (K ⇓ n @ τ) ∈ set Γ) ⟹ (K ⇓ n @ τ) ⨝ Γ›


section‹Major Theorems›
subsection ‹Interpretation of a context›

text‹
  The interpretation of a context is the intersection of the interpretation 
  of its components.
›
theorem symrun_interp_fixpoint:
  ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ) = ⟦⟦ Γ ⟧⟧prim›
by (induction Γ, simp+)

subsection ‹Expansion law›
text ‹Similar to the expansion laws of lattices›

theorem symrun_interp_expansion:
  ‹⟦⟦ Γ1 @ Γ2 ⟧⟧prim = ⟦⟦ Γ1 ⟧⟧prim ∩ ⟦⟦ Γ2 ⟧⟧prim›
by (induction Γ1, simp, auto)

section ‹Equations for the interpretation of symbolic primitives› 
subsection ‹General laws›

lemma symrun_interp_assoc:
  ‹⟦⟦ (Γ1 @ Γ2) @ Γ3 ⟧⟧prim = ⟦⟦ Γ1 @ (Γ2 @ Γ3) ⟧⟧prim›
by auto

lemma symrun_interp_commute:
  ‹⟦⟦ Γ1 @ Γ2 ⟧⟧prim = ⟦⟦ Γ2 @ Γ1 ⟧⟧prim›
by (simp add: symrun_interp_expansion inf_sup_aci(1))

lemma symrun_interp_left_commute:
  ‹⟦⟦ Γ1 @ (Γ2 @ Γ3) ⟧⟧prim = ⟦⟦ Γ2 @ (Γ1 @ Γ3) ⟧⟧prim›
unfolding symrun_interp_expansion by auto

lemma symrun_interp_idem:
  ‹⟦⟦ Γ @ Γ ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim›
using symrun_interp_expansion by auto

lemma symrun_interp_left_idem:
  ‹⟦⟦ Γ1 @ (Γ1 @ Γ2) ⟧⟧prim = ⟦⟦ Γ1 @ Γ2 ⟧⟧prim›
using symrun_interp_expansion by auto

lemma symrun_interp_right_idem:
  ‹⟦⟦ (Γ1 @ Γ2) @ Γ2 ⟧⟧prim = ⟦⟦ Γ1 @ Γ2 ⟧⟧prim›
unfolding symrun_interp_expansion by auto

lemmas symrun_interp_aci =  symrun_interp_commute
                            symrun_interp_assoc
                            symrun_interp_left_commute
                            symrun_interp_left_idem

― ‹Identity element›
lemma symrun_interp_neutral1:
  ‹⟦⟦ [] @ Γ ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim›
by simp

lemma symrun_interp_neutral2:
  ‹⟦⟦ Γ @ [] ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim›
by simp

subsection ‹Decreasing interpretation of symbolic primitives›

text‹
  Adding constraints to a context reduces the number of satisfying runs.
›
lemma TESL_sem_decreases_head:
  ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ γ # Γ ⟧⟧prim›
by simp

lemma TESL_sem_decreases_tail:
  ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ Γ @ [γ] ⟧⟧prim›
by (simp add: symrun_interp_expansion)

text‹
  Adding a constraint that is already in the context does not change the
  interpretation of the context.
›
lemma symrun_interp_formula_stuttering:
  assumes ‹γ ∈ set Γ›
    shows ‹⟦⟦ γ # Γ ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim›
proof -
  have ‹γ # Γ = [γ] @ Γ› by simp
  hence ‹⟦⟦ γ # Γ ⟧⟧prim = ⟦⟦ [γ] ⟧⟧prim ∩ ⟦⟦ Γ ⟧⟧prim›
    using symrun_interp_expansion by simp
  thus ?thesis using assms symrun_interp_fixpoint by fastforce
qed


text‹
  Removing duplicate constraints from a context does not change the
  interpretation of the context.
›
lemma symrun_interp_remdups_absorb:
  ‹⟦⟦ Γ ⟧⟧prim = ⟦⟦ remdups Γ ⟧⟧prim›
proof (induction Γ)
  case Cons
    thus ?case using symrun_interp_formula_stuttering by auto
qed simp

text‹
  Two identical sets of constraints have the same interpretation,
  the order in the context does not matter.
›
lemma symrun_interp_set_lifting:
  assumes ‹set Γ = set Γ'›
    shows ‹⟦⟦ Γ ⟧⟧prim = ⟦⟦ Γ' ⟧⟧prim›
proof -     
  have ‹set (remdups Γ) = set (remdups Γ')›
    by (simp add: assms)
  moreover have fxpntΓ: ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ) = ⟦⟦ Γ ⟧⟧prim›
    by (simp add: symrun_interp_fixpoint)
  moreover have fxpntΓ': ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ') = ⟦⟦ Γ' ⟧⟧prim›
    by (simp add: symrun_interp_fixpoint)
  moreover have ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ) = ⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ')›
    by (simp add: assms)
  ultimately show ?thesis using symrun_interp_remdups_absorb by auto
qed

text‹
  The interpretation of contexts is contravariant with regard to set inclusion.
›
theorem symrun_interp_decreases_setinc:
  assumes ‹set Γ ⊆ set Γ'›
    shows ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ Γ' ⟧⟧prim›
proof -
  obtain Γr where decompose: ‹set (Γ @ Γr) = set Γ'› using assms by auto
  hence ‹set (Γ @ Γr) = set Γ'› using assms by blast
  moreover have ‹(set Γ) ∪ (set Γr) = set Γ'› using assms decompose by auto
  moreover have ‹⟦⟦ Γ' ⟧⟧prim = ⟦⟦ Γ @ Γr ⟧⟧prim›
    using symrun_interp_set_lifting decompose by blast
  moreover have ‹⟦⟦ Γ @ Γr ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Γr ⟧⟧prim›
    by (simp add: symrun_interp_expansion)
  moreover have ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Γr ⟧⟧prim› by simp
  ultimately show ?thesis by simp
qed

lemma symrun_interp_decreases_add_head:
  assumes ‹set Γ ⊆ set Γ'›
    shows ‹⟦⟦ γ # Γ ⟧⟧prim ⊇ ⟦⟦ γ # Γ' ⟧⟧prim›
using symrun_interp_decreases_setinc assms by auto

lemma symrun_interp_decreases_add_tail:
  assumes ‹set Γ ⊆ set Γ'›
    shows ‹⟦⟦ Γ @ [γ] ⟧⟧prim ⊇ ⟦⟦ Γ' @ [γ] ⟧⟧prim›
proof -
  from symrun_interp_decreases_setinc[OF assms] have ‹⟦⟦ Γ' ⟧⟧prim ⊆ ⟦⟦ Γ ⟧⟧prim› .
  thus ?thesis by (simp add: symrun_interp_expansion dual_order.trans)
qed

lemma symrun_interp_absorb1:
  assumes ‹set Γ1 ⊆ set Γ2›
    shows ‹⟦⟦ Γ1 @ Γ2 ⟧⟧prim = ⟦⟦ Γ2 ⟧⟧prim›
by (simp add: Int_absorb1 symrun_interp_decreases_setinc
                          symrun_interp_expansion assms)

lemma symrun_interp_absorb2:
  assumes ‹set Γ2 ⊆ set Γ1›
    shows ‹⟦⟦ Γ1 @ Γ2 ⟧⟧prim = ⟦⟦ Γ1 ⟧⟧prim›
using symrun_interp_absorb1 symrun_interp_commute assms by blast

end

Theory Operational

chapter ‹Operational Semantics›
text‹\label{chap:operational_semantics}›

theory Operational
imports
  SymbolicPrimitive

begin

text‹
  The operational semantics defines rules to build symbolic runs from a TESL 
  specification (a set of TESL formulae).
  Symbolic runs are described using the symbolic primitives presented in the 
  previous chapter.
  Therefore, the operational semantics compiles a set of constraints on runs, 
  as defined by the denotational semantics, into a set of symbolic constraints 
  on the instants of the runs. Concrete runs can then be obtained by solving the 
  constraints at each instant.
›

section‹Operational steps›

text ‹
  We introduce a notation to describe configurations:
  ▪ @{term ‹Γ›} is the context, the set of symbolic constraints on past instants of the run;
  ▪ @{term ‹n›} is the index of the current instant, the present;
  ▪ @{term ‹Ψ›} is the TESL formula that must be satisfied at the current instant (present);
  ▪ @{term ‹Φ›} is the TESL formula that must be satisfied for the following instants (the future).
›
abbreviation uncurry_conf
  ::‹('τ::linordered_field) system ⇒ instant_index ⇒ 'τ TESL_formula ⇒ 'τ TESL_formula
      ⇒ 'τ config›                                                  (‹_, _ ⊢ _ ▹ _› 80)
where
  ‹Γ, n ⊢ Ψ ▹ Φ ≡ (Γ, n, Ψ, Φ)›

text ‹
  The only introduction rule allows us to progress to the next instant 
  when there are no more constraints to satisfy for the present instant.
›
inductive operational_semantics_intro
  ::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪i _› 70)
where
  instant_i:
  ‹(Γ, n ⊢ [] ▹ Φ) ↪i  (Γ, Suc n ⊢ Φ ▹ [])›

text ‹
  The elimination rules describe how TESL formulae for the present are transformed 
  into constraints on the past and on the future.
›
inductive operational_semantics_elim
  ::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪e _› 70)
where
  sporadic_on_e1:
― ‹A sporadic constraint can be ignored in the present and rejected into the future.›
  ‹(Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ)
     ↪e  (Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ))›
| sporadic_on_e2:
― ‹It can also be handled in the present by making the clock tick and have 
  the expected time. Once it has been handled, it is no longer a constraint 
  to satisfy, so it disappears from the future.›
  ‹(Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ)›
| tagrel_e:
― ‹A relation between time scales has to be obeyed at every instant.›
  ‹(Γ, n ⊢ ((time-relation ⌊K1, K2⌋ ∈ R) # Ψ) ▹ Φ)
     ↪e  (((⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R) # Γ), n
              ⊢ Ψ ▹ ((time-relation ⌊K1, K2⌋ ∈ R) # Φ))›
| implies_e1:
― ‹An implication can be handled in the present by forbidding a tick of the master
  clock. The implication is copied back into the future because it holds for 
  the whole run.›
  ‹(Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ))›
| implies_e2:
― ‹It can also be handled in the present by making both the master and the slave
    clocks tick.›
  ‹(Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ⇑ n) # (K2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ))›
| implies_not_e1:
― ‹A negative implication can be handled in the present by forbidding a tick of 
  the master clock. The implication is copied back into the future because 
  it holds for the whole run.›
  ‹(Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ))›
| implies_not_e2:
― ‹It can also be handled in the present by making the master clock ticks and 
    forbidding a tick on the slave clock.›
  ‹(Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ))›
| timedelayed_e1:
― ‹A timed delayed implication can be handled by forbidding a tick on 
    the master clock.›
  ‹(Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)
     ↪e  (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))›
| timedelayed_e2:
― ‹It can also be handled by making the master clock tick and adding a constraint 
    that makes the slave clock tick when the delay has elapsed on the measuring clock.›
  ‹(Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)
     ↪e  (((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
            ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))›
| weakly_precedes_e:
― ‹A weak precedence relation has to hold at every instant.›
  ‹(Γ, n ⊢ ((K1 weakly precedes K2) # Ψ) ▹ Φ)
     ↪e  (((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
            ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ))›
| strictly_precedes_e:
― ‹A strict precedence relation has to hold at every instant.›
  ‹(Γ, n ⊢ ((K1 strictly precedes K2) # Ψ) ▹ Φ)
     ↪e  (((⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
            ⊢ Ψ ▹ ((K1 strictly precedes K2) # Φ))›
| kills_e1:
― ‹A kill can be handled by forbidding a tick of the triggering clock.›
  ‹(Γ, n ⊢ ((K1 kills K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ))›
| kills_e2:
― ‹It can also be handled by making the triggering clock tick and by forbidding 
    any further tick of the killed clock.›
  ‹(Γ, n ⊢ ((K1 kills K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ⇑ n) # (K2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ))›

text ‹
  A step of the operational semantics is either the application of the introduction 
  rule or the application of an elimination rule.
›
inductive operational_semantics_step
  ::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪ _› 70)
where
  intro_part:
  ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1)  ↪i  (Γ2, n2 ⊢ Ψ2 ▹ Φ2)
    ⟹ (Γ1, n1 ⊢ Ψ1 ▹ Φ1)  ↪  (Γ2, n2 ⊢ Ψ2 ▹ Φ2)›
| elims_part:
  ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1)  ↪e  (Γ2, n2 ⊢ Ψ2 ▹ Φ2)
    ⟹ (Γ1, n1 ⊢ Ψ1 ▹ Φ1)  ↪  (Γ2, n2 ⊢ Ψ2 ▹ Φ2)›

text ‹
  We introduce notations for the reflexive transitive closure of the operational 
  semantic step, its transitive closure and its reflexive closure.
›
abbreviation operational_semantics_step_rtranclp
  ::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪** _› 70)
where
  ‹𝒞1 ↪** 𝒞2 ≡ operational_semantics_step** 𝒞1 𝒞2›

abbreviation operational_semantics_step_tranclp
  ::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪++ _› 70)
where
  ‹𝒞1 ↪++ 𝒞2 ≡ operational_semantics_step++ 𝒞1 𝒞2›

abbreviation operational_semantics_step_reflclp
  ::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪== _› 70)
where
  ‹𝒞1 ↪== 𝒞2 ≡ operational_semantics_step== 𝒞1 𝒞2›

abbreviation operational_semantics_step_relpowp
  ::‹('τ::linordered_field) config ⇒ nat ⇒ 'τ config ⇒ bool›       (‹_ ↪⇗_⇖ _› 70)
where
  ‹𝒞1 ↪n 𝒞2 ≡ (operational_semantics_step ^^ n) 𝒞1 𝒞2›

definition operational_semantics_elim_inv
  ::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪e← _› 70)
where
  ‹𝒞1 ↪e← 𝒞2 ≡ 𝒞2 ↪e 𝒞1›


section‹Basic Lemmas›

text ‹
  If a configuration can be reached in @{term ‹m›} steps from a configuration that 
  can be reached in @{term ‹n›} steps from an original configuration, then it can be 
  reached in @{term ‹n+m›} steps from the original configuration.
›
lemma operational_semantics_trans_generalized:
  assumes ‹𝒞1 ↪n 𝒞2›
  assumes ‹𝒞2 ↪m 𝒞3›
    shows ‹𝒞1 ↪n + m 𝒞3›
using relcompp.relcompI[of  ‹operational_semantics_step ^^ n› _ _ 
                            ‹operational_semantics_step ^^ m›, OF assms]
by (simp add: relpowp_add) 

text ‹
  We consider the set of configurations that can be reached in one operational
  step from a given configuration.
›
abbreviation Cnext_solve
  ::‹('τ::linordered_field) config ⇒ 'τ config set› (‹𝒞next _›)
where
  ‹𝒞next 𝒮 ≡ { 𝒮'. 𝒮 ↪ 𝒮' }›

text ‹
  Advancing to the next instant is possible when there are no more constraints 
  on the current instant.
›
lemma Cnext_solve_instant:
  ‹(𝒞next (Γ, n ⊢ [] ▹ Φ)) ⊇ { Γ, Suc n ⊢ Φ ▹ [] }›
by (simp add: operational_semantics_step.simps operational_semantics_intro.instant_i)

text ‹
  The following lemmas state that the configurations produced by the elimination 
  rules of the operational semantics belong to the configurations that can be 
  reached in one step.
›
lemma Cnext_solve_sporadicon:
  ‹(𝒞next (Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ))
    ⊇ { Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ),
        ((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.sporadic_on_e1
              operational_semantics_elim.sporadic_on_e2)

lemma Cnext_solve_tagrel:
  ‹(𝒞next (Γ, n ⊢ ((time-relation ⌊K1, K2⌋ ∈ R) # Ψ) ▹ Φ))
    ⊇ { ((⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R) # Γ),n
          ⊢ Ψ ▹ ((time-relation ⌊K1, K2⌋ ∈ R) # Φ) }›
by (simp add: operational_semantics_step.simps operational_semantics_elim.tagrel_e)

lemma Cnext_solve_implies:
  ‹(𝒞next (Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ))
    ⊇ { ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ),
         ((K1 ⇑ n) # (K2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ) }›
by (simp add: operational_semantics_step.simps operational_semantics_elim.implies_e1
              operational_semantics_elim.implies_e2)

lemma Cnext_solve_implies_not:
  ‹(𝒞next (Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ))
    ⊇ { ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ),
        ((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ) }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.implies_not_e1
              operational_semantics_elim.implies_not_e2)

lemma Cnext_solve_timedelayed:
  ‹(𝒞next (Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ))
    ⊇ { ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ),
        ((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
          ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.timedelayed_e1
              operational_semantics_elim.timedelayed_e2)

lemma Cnext_solve_weakly_precedes:
  ‹(𝒞next (Γ, n ⊢ ((K1 weakly precedes K2) # Ψ) ▹ Φ))
    ⊇ { ((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
          ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ) }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.weakly_precedes_e)

lemma Cnext_solve_strictly_precedes:
  ‹(𝒞next (Γ, n ⊢ ((K1 strictly precedes K2) # Ψ) ▹ Φ))
    ⊇ { ((⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
          ⊢ Ψ ▹ ((K1 strictly precedes K2) # Φ) }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.strictly_precedes_e)

lemma Cnext_solve_kills:
  ‹(𝒞next (Γ, n ⊢ ((K1 kills K2) # Ψ) ▹ Φ))
    ⊇ { ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ),
        ((K1 ⇑ n) # (K2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ) }›
by (simp add: operational_semantics_step.simps operational_semantics_elim.kills_e1
              operational_semantics_elim.kills_e2)

text ‹
  An empty specification can be reduced to an empty specification for 
  an arbitrary number of steps.
›
lemma empty_spec_reductions:
  ‹([], 0 ⊢ [] ▹ []) ↪k ([], k ⊢ [] ▹ [])›
proof (induct k)
  case 0 thus ?case by simp
next
  case Suc thus ?case
    using instant_i operational_semantics_step.simps by fastforce 
qed

end

Theory Corecursive_Prop

(*chapter‹Equivalence of Operational and Denotational Semantics›*)
text‹\chapter[Semantics Equivalence]{Equivalence of the Operational and Denotational Semantics}›

theory Corecursive_Prop
  imports
    SymbolicPrimitive
    Operational
    Denotational

begin

section ‹Stepwise denotational interpretation of TESL atoms›

text ‹
  In order to prove the equivalence of the denotational and operational semantics, 
  we need to be able to ignore the past (for which the constraints are encoded 
  in the context) and consider only the satisfaction of the constraints from
  a given instant index.
  For this purpose, we define an interpretation of TESL formulae for a suffix of a run.
  That interpretation is closely related to the denotational semantics as
  defined in the preceding chapters.
›
fun TESL_interpretation_atomic_stepwise
    :: ‹('τ::linordered_field) TESL_atomic ⇒ nat ⇒ 'τ run set› (‹⟦ _ ⟧TESL⇗≥ _⇖›)
where
  ‹⟦ K1 sporadic τ on K2 ⟧TESL≥ i =
      {ρ. ∃n≥i. hamlet ((Rep_run ρ) n K1) ∧ time ((Rep_run ρ) n K2) = τ}›
| ‹⟦ time-relation ⌊K1, K2⌋ ∈ R ⟧TESL≥ i =
      {ρ. ∀n≥i. R (time ((Rep_run ρ) n K1), time ((Rep_run ρ) n K2))}›
| ‹⟦ master implies slave ⟧TESL≥ i =
      {ρ. ∀n≥i. hamlet ((Rep_run ρ) n master) ⟶ hamlet ((Rep_run ρ) n slave)}›
| ‹⟦ master implies not slave ⟧TESL≥ i =
      {ρ. ∀n≥i. hamlet ((Rep_run ρ) n master) ⟶ ¬ hamlet ((Rep_run ρ) n slave)}›
| ‹⟦ master time-delayed by δτ on measuring implies slave ⟧TESL≥ i =
      {ρ. ∀n≥i. hamlet ((Rep_run ρ) n master) ⟶
               (let measured_time = time ((Rep_run ρ) n measuring) in
                ∀m ≥ n. first_time ρ measuring m (measured_time + δτ)
                         ⟶ hamlet ((Rep_run ρ) m slave)
               )
      }›
| ‹⟦ K1 weakly precedes K2 ⟧TESL≥ i =
      {ρ. ∀n≥i. (run_tick_count ρ K2 n) ≤ (run_tick_count ρ K1 n)}›
| ‹⟦ K1 strictly precedes K2 ⟧TESL≥ i =
      {ρ. ∀n≥i. (run_tick_count ρ K2 n) ≤ (run_tick_count_strictly ρ K1 n)}›
| ‹⟦ K1 kills K2 ⟧TESL≥ i =
      {ρ. ∀n≥i. hamlet ((Rep_run ρ) n K1) ⟶ (∀m≥n. ¬ hamlet ((Rep_run ρ) m K2))}›

text ‹
  The denotational interpretation of TESL formulae can be unfolded into the 
  stepwise interpretation.
›
lemma TESL_interp_unfold_stepwise_sporadicon:
  ‹⟦ K1 sporadic τ on K2 ⟧TESL = ⋃ {Y. ∃n::nat. Y = ⟦ K1 sporadic τ on K2 ⟧TESL≥ n}›
by auto

lemma TESL_interp_unfold_stepwise_tagrelgen:
  ‹⟦ time-relation ⌊K1, K2⌋ ∈ R ⟧TESL
    = ⋂ {Y. ∃n::nat. Y = ⟦ time-relation ⌊K1, K2⌋ ∈ R ⟧TESL≥ n}›
by auto

lemma TESL_interp_unfold_stepwise_implies:
  ‹⟦ master implies slave ⟧TESL
    = ⋂ {Y. ∃n::nat. Y = ⟦ master implies slave ⟧TESL≥ n}›
by auto

lemma TESL_interp_unfold_stepwise_implies_not:
  ‹⟦ master implies not slave ⟧TESL
    = ⋂ {Y. ∃n::nat. Y = ⟦ master implies not slave ⟧TESL≥ n}›
by auto

lemma TESL_interp_unfold_stepwise_timedelayed:
  ‹⟦ master time-delayed by δτ on measuring implies slave ⟧TESL
    = ⋂ {Y. ∃n::nat.
          Y = ⟦ master time-delayed by δτ on measuring implies slave ⟧TESL≥ n}›
by auto

lemma TESL_interp_unfold_stepwise_weakly_precedes:
  ‹⟦ K1 weakly precedes K2 ⟧TESL
    = ⋂ {Y. ∃n::nat. Y = ⟦ K1 weakly precedes K2 ⟧TESL≥ n}›
by auto

lemma TESL_interp_unfold_stepwise_strictly_precedes:
  ‹⟦ K1 strictly precedes K2 ⟧TESL
    = ⋂ {Y. ∃n::nat. Y = ⟦ K1 strictly precedes K2 ⟧TESL≥ n}›
by auto

lemma TESL_interp_unfold_stepwise_kills:
  ‹⟦ master kills slave ⟧TESL = ⋂ {Y. ∃n::nat. Y = ⟦ master kills slave ⟧TESL≥ n}›
by auto

text ‹
  Positive atomic formulae (the ones that create ticks from nothing) are unfolded
  as the union of the stepwise interpretations.
›
theorem TESL_interp_unfold_stepwise_positive_atoms:
  assumes ‹positive_atom φ›
    shows ‹⟦ φ::'τ::linordered_field TESL_atomic ⟧TESL
            = ⋃ {Y. ∃n::nat. Y = ⟦ φ ⟧TESL≥ n}›
proof -
  from positive_atom.elims(2)[OF assms]
    obtain u v w where ‹φ = (u sporadic v on w)› by blast
  with TESL_interp_unfold_stepwise_sporadicon show ?thesis by simp
qed

text ‹
  Negative atomic formulae are unfolded
  as the intersection of the stepwise interpretations.
›
theorem TESL_interp_unfold_stepwise_negative_atoms:
  assumes ‹¬ positive_atom φ›
    shows ‹⟦ φ ⟧TESL = ⋂ {Y. ∃n::nat. Y = ⟦ φ ⟧TESL≥ n}›
proof (cases φ)
  case SporadicOn thus ?thesis using assms by simp
next
  case TagRelation
    thus ?thesis using TESL_interp_unfold_stepwise_tagrelgen by simp
next
  case Implies
    thus ?thesis using TESL_interp_unfold_stepwise_implies by simp
next
  case ImpliesNot
    thus ?thesis using TESL_interp_unfold_stepwise_implies_not by simp
next
  case TimeDelayedBy
    thus ?thesis using TESL_interp_unfold_stepwise_timedelayed by simp
next
  case WeaklyPrecedes
    thus ?thesis
      using TESL_interp_unfold_stepwise_weakly_precedes by simp
next
  case StrictlyPrecedes
    thus ?thesis
      using TESL_interp_unfold_stepwise_strictly_precedes by simp
next
  case Kills
    thus ?thesis
      using TESL_interp_unfold_stepwise_kills by simp
qed

text ‹
  Some useful lemmas for reasoning on properties of sequences.
›
lemma forall_nat_expansion:
  ‹(∀n ≥ (n0::nat). P n) = (P n0 ∧ (∀n ≥ Suc n0. P n))›
proof -
  have ‹(∀n ≥ (n0::nat). P n) = (∀n. (n = n0 ∨ n > n0) ⟶ P n)›
    using le_less by blast
  also have ‹... = (P n0 ∧ (∀n > n0. P n))› by blast
  finally show ?thesis using Suc_le_eq by simp
qed

lemma exists_nat_expansion:
  ‹(∃n ≥ (n0::nat). P n) = (P n0 ∨ (∃n ≥ Suc n0. P n))›
proof -
  have ‹(∃n ≥ (n0::nat). P n) = (∃n. (n = n0 ∨ n > n0) ∧ P n)›
    using le_less by blast
  also have ‹... = (∃n. (P n0) ∨ (n > n0 ∧ P n))› by blast
  finally show ?thesis using Suc_le_eq by simp
qed

lemma forall_nat_set_suc:‹{x. ∀m ≥ n. P x m} = {x. P x n} ∩ {x. ∀m ≥ Suc n. P x m}›
proof
  { fix x assume h:‹x ∈ {x. ∀m ≥ n. P x m}›
    hence ‹P x n› by simp
    moreover from h have ‹x ∈ {x. ∀m ≥ Suc n. P x m}› by simp
    ultimately have ‹x ∈ {x. P x n} ∩ {x. ∀m ≥ Suc n. P x m}› by simp
  } thus ‹{x. ∀m ≥ n. P x m} ⊆ {x. P x n} ∩ {x. ∀m ≥ Suc n. P x m}› ..
next
  { fix x  assume h:‹x ∈ {x. P x n} ∩ {x. ∀m ≥ Suc n. P x m}›
    hence ‹P x n› by simp
    moreover from h have ‹∀m ≥ Suc n. P x m› by simp
    ultimately have ‹∀m ≥ n. P x m› using forall_nat_expansion by blast
    hence ‹x ∈ {x. ∀m ≥ n. P x m}› by simp
  } thus ‹{x. P x n} ∩ {x. ∀m ≥ Suc n. P x m} ⊆ {x. ∀m ≥ n. P x m}› ..
qed

lemma exists_nat_set_suc:‹{x. ∃m ≥ n. P x m} = {x. P x n} ∪ {x. ∃m ≥ Suc n. P x m}›
proof
  { fix x assume h:‹x ∈ {x. ∃m ≥ n. P x m}›
    hence ‹x ∈ {x. ∃m. (m = n ∨ m ≥ Suc n) ∧ P x m}›
      using Suc_le_eq antisym_conv2 by fastforce
    hence ‹x ∈ {x. P x n} ∪ {x. ∃m ≥ Suc n. P x m}› by blast
  } thus ‹{x. ∃m ≥ n. P x m} ⊆ {x. P x n} ∪ {x. ∃m ≥ Suc n. P x m}› ..
next
  { fix x  assume h:‹x ∈ {x. P x n} ∪ {x. ∃m ≥ Suc n. P x m}›
    hence ‹x ∈ {x. ∃m ≥ n. P x m}› using Suc_leD by blast
  } thus ‹{x. P x n} ∪ {x. ∃m ≥ Suc n. P x m} ⊆ {x. ∃m ≥ n. P x m}› ..
qed

section ‹Coinduction Unfolding Properties›

text ‹
  The following lemmas show how  to shorten a suffix, i.e. to unfold one instant 
  in the construction of a run. They correspond to the rules of the operational 
  semantics.
›
lemma TESL_interp_stepwise_sporadicon_coind_unfold:
  ‹⟦ K1 sporadic τ on K2 ⟧TESL≥ n =
    ⟦ K1 ⇑ n ⟧prim ∩ ⟦ K2 ⇓ n @ τ ⟧prim        ― ‹rule @{term sporadic_on_e2}›
    ∪ ⟦ K1 sporadic τ on K2 ⟧TESL≥ Suc n›   ― ‹rule @{term sporadic_on_e1}›
unfolding TESL_interpretation_atomic_stepwise.simps(1)
          symbolic_run_interpretation_primitive.simps(1,6)
using exists_nat_set_suc[of ‹n› ‹λρ n. hamlet (Rep_run ρ n K1)
                                     ∧ time (Rep_run ρ n K2) = τ›]
by (simp add: Collect_conj_eq)


lemma TESL_interp_stepwise_tagrel_coind_unfold:
  ‹⟦ time-relation ⌊K1, K2⌋ ∈ R ⟧TESL≥ n =        ― ‹rule @{term tagrel_e}›
     ⟦ ⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R ⟧prim
     ∩ ⟦ time-relation ⌊K1, K2⌋ ∈ R ⟧TESL≥ Suc n›
proof -
  have ‹{ρ. ∀m≥n. R (time ((Rep_run ρ) m K1), time ((Rep_run ρ) m K2))}
       = {ρ. R (time ((Rep_run ρ) n K1), time ((Rep_run ρ) n K2))}
       ∩ {ρ. ∀m≥Suc n. R (time ((Rep_run ρ) m K1), time ((Rep_run ρ) m K2))}›
    using forall_nat_set_suc[of ‹n› ‹λx y. R (time ((Rep_run x) y K1),
                                       time ((Rep_run x) y K2))›] by simp
  thus ?thesis by auto
qed

lemma TESL_interp_stepwise_implies_coind_unfold:
  ‹⟦ master implies slave ⟧TESL≥ n =
     (   ⟦ master ¬⇑ n ⟧prim                     ― ‹rule @{term implies_e1}›
       ∪ ⟦ master ⇑ n ⟧prim ∩ ⟦ slave ⇑ n ⟧prim)  ― ‹rule @{term implies_e2}›
     ∩ ⟦ master implies slave ⟧TESL≥ Suc n›
proof -
  have ‹{ρ. ∀m≥n. hamlet ((Rep_run ρ) m master) ⟶ hamlet ((Rep_run ρ) m slave)}
        = {ρ. hamlet ((Rep_run ρ) n master) ⟶ hamlet ((Rep_run ρ) n slave)}
        ∩ {ρ. ∀m≥Suc n. hamlet ((Rep_run ρ) m master)
                     ⟶ hamlet ((Rep_run ρ) m slave)}›
    using forall_nat_set_suc[of ‹n› ‹λx y. hamlet ((Rep_run x) y master)
                                ⟶ hamlet ((Rep_run x) y slave)›] by simp
  thus ?thesis by auto
qed

lemma TESL_interp_stepwise_implies_not_coind_unfold:
  ‹⟦ master implies not slave ⟧TESL≥ n =
     (    ⟦ master ¬⇑ n ⟧prim                       ― ‹rule @{term implies_not_e1}›
        ∪ ⟦ master ⇑ n ⟧prim ∩ ⟦ slave ¬⇑ n ⟧prim)  ― ‹rule @{term implies_not_e2}›
     ∩ ⟦ master implies not slave ⟧TESL≥ Suc n›
proof -
  have ‹{ρ. ∀m≥n. hamlet ((Rep_run ρ) m master) ⟶ ¬ hamlet ((Rep_run ρ) m slave)}
       = {ρ. hamlet ((Rep_run ρ) n master) ⟶ ¬ hamlet ((Rep_run ρ) n slave)}
          ∩ {ρ. ∀m≥Suc n. hamlet ((Rep_run ρ) m master)
                     ⟶ ¬ hamlet ((Rep_run ρ) m slave)}›
    using forall_nat_set_suc[of ‹n› ‹λx y. hamlet ((Rep_run x) y master)
                               ⟶ ¬hamlet ((Rep_run x) y slave)›] by simp
  thus ?thesis by auto
qed

lemma TESL_interp_stepwise_timedelayed_coind_unfold:
  ‹⟦ master time-delayed by δτ on measuring implies slave ⟧TESL≥ n =
     (     ⟦ master ¬⇑ n ⟧prim               ― ‹rule @{term timedelayed_e1}›
        ∪ (⟦ master ⇑ n ⟧prim ∩ ⟦ measuring @ n ⊕ δτ ⇒ slave ⟧prim))
                                             ― ‹rule @{term timedelayed_e2}›
     ∩ ⟦ master time-delayed by δτ on measuring implies slave ⟧TESL≥ Suc n›
proof -
  let ?prop = ‹λρ m. hamlet ((Rep_run ρ) m master) ⟶
                 (let measured_time = time ((Rep_run ρ) m measuring) in
                  ∀p ≥ m. first_time ρ measuring p (measured_time + δτ)
                           ⟶ hamlet ((Rep_run ρ) p slave))›
  have ‹{ρ. ∀m ≥ n. ?prop ρ m} = {ρ. ?prop ρ n} ∩ {ρ. ∀m ≥ Suc n. ?prop ρ m}›
    using forall_nat_set_suc[of ‹n› ?prop] by blast
  also have ‹... = {ρ. ?prop ρ n}
              ∩ ⟦ master time-delayed by δτ on measuring implies slave ⟧TESL≥ Suc n›
    by simp
  finally show ?thesis by auto
qed

lemma TESL_interp_stepwise_weakly_precedes_coind_unfold:
   ‹⟦ K1 weakly precedes K2 ⟧TESL≥ n =                 ― ‹rule @{term weakly_precedes_e}›
      ⟦ (⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x,y). x≤y)) ⟧prim 
      ∩ ⟦ K1 weakly precedes K2 ⟧TESL≥ Suc n›
proof -
  have ‹{ρ. ∀p≥n. (run_tick_count ρ K2 p) ≤ (run_tick_count ρ K1 p)}
         = {ρ. (run_tick_count ρ K2 n) ≤ (run_tick_count ρ K1 n)}
         ∩ {ρ. ∀p≥Suc n. (run_tick_count ρ K2 p) ≤ (run_tick_count ρ K1 p)}›
    using forall_nat_set_suc[of ‹n› ‹λρ n. (run_tick_count ρ K2 n)
                                  ≤ (run_tick_count ρ K1 n)›]
    by simp
  thus ?thesis by auto
qed

lemma TESL_interp_stepwise_strictly_precedes_coind_unfold:
   ‹⟦ K1 strictly precedes K2 ⟧TESL≥ n =               ― ‹rule @{term strictly_precedes_e}›
      ⟦ (⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x,y). x≤y)) ⟧prim
      ∩ ⟦ K1 strictly precedes K2 ⟧TESL≥ Suc n›
proof -
  have ‹{ρ. ∀p≥n. (run_tick_count ρ K2 p) ≤ (run_tick_count_strictly ρ K1 p)}
         = {ρ. (run_tick_count ρ K2 n) ≤ (run_tick_count_strictly ρ K1 n)}
         ∩ {ρ. ∀p≥Suc n. (run_tick_count ρ K2 p) ≤ (run_tick_count_strictly ρ K1 p)}›
    using forall_nat_set_suc[of ‹n› ‹λρ n. (run_tick_count ρ K2 n)
                                  ≤ (run_tick_count_strictly ρ K1 n)›]
    by simp
  thus ?thesis by auto
qed

lemma TESL_interp_stepwise_kills_coind_unfold:
   ‹⟦ K1 kills K2 ⟧TESL≥ n =
      (   ⟦ K1 ¬⇑ n ⟧prim                        ― ‹rule @{term kills_e1}›
        ∪ ⟦ K1 ⇑ n ⟧prim ∩ ⟦ K2 ¬⇑ ≥ n ⟧prim)    ― ‹rule @{term kills_e2}›
      ∩ ⟦ K1 kills K2 ⟧TESL≥ Suc n›
proof -
  let ?kills = ‹λn ρ. ∀p≥n. hamlet ((Rep_run ρ) p K1)
                             ⟶ (∀m≥p. ¬ hamlet ((Rep_run ρ) m K2))›
  let ?ticks = ‹λn ρ c. hamlet ((Rep_run ρ) n c)›
  let ?dead = ‹λn ρ c. ∀m ≥ n. ¬hamlet ((Rep_run ρ) m c)›
  have ‹⟦ K1 kills K2 ⟧TESL≥ n = {ρ. ?kills n ρ}› by simp
  also have ‹... = ({ρ. ¬ ?ticks n ρ K1}  ∩ {ρ. ?kills (Suc n) ρ})
                 ∪ ({ρ. ?ticks n ρ K1} ∩ {ρ. ?dead n ρ K2})›
  proof
    { fix ρ::‹'τ::linordered_field run›
      assume ‹ρ ∈ {ρ. ?kills n ρ}›
      hence ‹?kills n ρ› by simp
      hence ‹(?ticks n ρ K1 ∧ ?dead n ρ K2) ∨ (¬?ticks n ρ K1 ∧ ?kills (Suc n) ρ)›
        using Suc_leD by blast
      hence ‹ρ ∈ ({ρ. ?ticks n ρ K1} ∩ {ρ. ?dead n ρ K2})
               ∪ ({ρ. ¬ ?ticks n ρ K1} ∩ {ρ. ?kills (Suc n) ρ})›
        by blast
    } thus ‹{ρ. ?kills n ρ}
           ⊆ {ρ. ¬ ?ticks n ρ K1} ∩ {ρ. ?kills (Suc n) ρ} 
            ∪ {ρ. ?ticks n ρ K1} ∩ {ρ. ?dead n ρ K2}› by blast
  next
    { fix ρ::‹'τ::linordered_field run›
      assume ‹ρ ∈ ({ρ. ¬ ?ticks n ρ K1}  ∩ {ρ. ?kills (Suc n) ρ})
                 ∪ ({ρ. ?ticks n ρ K1} ∩ {ρ. ?dead n ρ K2})›
      hence ‹¬ ?ticks n ρ K1 ∧ ?kills (Suc n) ρ
             ∨ ?ticks n ρ K1 ∧ ?dead n ρ K2› by blast
      moreover have ‹((¬ ?ticks n ρ K1) ∧ (?kills (Suc n) ρ)) ⟶ ?kills n ρ›
        using dual_order.antisym not_less_eq_eq by blast
      ultimately have ‹?kills n ρ ∨ ?ticks n ρ K1 ∧ ?dead n ρ K2› by blast
      hence ‹?kills n ρ› using le_trans by blast
    } thus ‹({ρ. ¬ ?ticks n ρ K1}  ∩ {ρ. ?kills (Suc n) ρ})
                 ∪ ({ρ. ?ticks n ρ K1} ∩ {ρ. ?dead n ρ K2})
          ⊆ {ρ. ?kills n ρ}› by blast
  qed
  also have ‹... = {ρ. ¬ ?ticks n ρ K1} ∩ {ρ. ?kills (Suc n) ρ}
                 ∪ {ρ. ?ticks n ρ K1} ∩ {ρ. ?dead n ρ K2} ∩ {ρ. ?kills (Suc n) ρ}›
    using Collect_cong Collect_disj_eq by auto
  also have ‹... = ⟦ K1 ¬⇑ n ⟧prim ∩ ⟦ K1 kills K2 ⟧TESL≥ Suc n
                 ∪ ⟦ K1 ⇑ n ⟧prim ∩ ⟦ K2 ¬⇑ ≥ n ⟧prim
                 ∩ ⟦ K1 kills K2 ⟧TESL≥ Suc n› by simp
  finally show ?thesis by blast
qed

text ‹
  The stepwise interpretation of a TESL formula is the intersection of the
  interpretation of its atomic components.
›
fun TESL_interpretation_stepwise
  ::‹'τ::linordered_field TESL_formula ⇒ nat ⇒ 'τ run set›
  (‹⟦⟦ _ ⟧⟧TESL⇗≥ _⇖›)
where
  ‹⟦⟦ [] ⟧⟧TESL≥ n = {ρ. True}›
| ‹⟦⟦ φ # Φ ⟧⟧TESL≥ n = ⟦ φ ⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ n›

lemma TESL_interpretation_stepwise_fixpoint:
  ‹⟦⟦ Φ ⟧⟧TESL≥ n = ⋂ ((λφ. ⟦ φ ⟧TESL≥ n) ` set Φ)›
by (induction Φ, simp, auto)

text ‹
  The global interpretation of a TESL formula is its interpretation starting
  at the first instant.
›
lemma TESL_interpretation_stepwise_zero:
  ‹⟦ φ ⟧TESL = ⟦ φ ⟧TESL≥ 0›
by (induction φ, simp+)

lemma TESL_interpretation_stepwise_zero':
  ‹⟦⟦ Φ ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL≥ 0›
by (induction Φ, simp, simp add: TESL_interpretation_stepwise_zero)

lemma TESL_interpretation_stepwise_cons_morph:
  ‹⟦ φ ⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ n = ⟦⟦ φ # Φ ⟧⟧TESL≥ n›
by auto

theorem TESL_interp_stepwise_composition:
  shows ‹⟦⟦ Φ1 @ Φ2 ⟧⟧TESL≥ n = ⟦⟦ Φ1 ⟧⟧TESL≥ n ∩ ⟦⟦ Φ2 ⟧⟧TESL≥ n›
by (induction Φ1, simp, auto)

section ‹Interpretation of configurations›

text ‹
  The interpretation of a configuration of the operational semantics abstract 
  machine is the intersection of:
  ▪ the interpretation of its context (the past),
  ▪ the interpretation of its present from the current instant,
  ▪ the interpretation of its future from the next instant.
›
fun HeronConf_interpretation
  ::‹'τ::linordered_field config ⇒ 'τ run set›          (‹⟦ _ ⟧config› 71)
where
  ‹⟦ Γ, n ⊢ Ψ ▹ Φ ⟧config = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›

lemma HeronConf_interp_composition:
   ‹⟦ Γ1, n ⊢ Ψ1 ▹ Φ1 ⟧config ∩ ⟦ Γ2, n ⊢ Ψ2 ▹ Φ2 ⟧config
     = ⟦ (Γ1 @ Γ2), n ⊢ (Ψ1 @ Ψ2) ▹ (Φ1 @ Φ2) ⟧config›
  using TESL_interp_stepwise_composition symrun_interp_expansion
by (simp add: TESL_interp_stepwise_composition
              symrun_interp_expansion inf_assoc inf_left_commute)

text ‹
  When there are no remaining constraints on the present, the interpretation of
  a configuration is the same as the configuration at the next instant of its future.
  This corresponds to the introduction rule of the operational semantics.
›
lemma HeronConf_interp_stepwise_instant_cases:
   ‹⟦ Γ, n ⊢ [] ▹ Φ ⟧config = ⟦ Γ, Suc n ⊢ Φ ▹ [] ⟧config›
proof -
  have ‹⟦ Γ, n ⊢ [] ▹ Φ ⟧config = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ [] ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ Γ, Suc n ⊢ Φ ▹ [] ⟧config
                  = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n ∩ ⟦⟦ [] ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ [] ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n
                 = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n ∩ ⟦⟦ [] ⟧⟧TESL≥ Suc n›
    by simp
  ultimately show ?thesis by blast
qed

text ‹
  The following lemmas use the unfolding properties of the stepwise denotational 
  semantics to give rewriting rules for the interpretation of configurations that
  match the elimination rules of the operational semantics.
›
lemma HeronConf_interp_stepwise_sporadicon_cases:
   ‹⟦ Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ ⟧config
    = ⟦ Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ) ⟧config
    ∪ ⟦ ((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ ⟧config›
proof -
  have ‹⟦ Γ, n ⊢ (K1 sporadic τ on K2) # Ψ ▹ Φ ⟧config
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (K1 sporadic τ on K2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ) ⟧config
                 =  ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (K1 sporadic τ on K2) # Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ ((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ ⟧config
                 =  ⟦⟦ ((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ) ⟧⟧prim
                  ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
    by simp
  ultimately show ?thesis
  proof -
    have ‹(⟦ K1 ⇑ n ⟧prim ∩ ⟦ K2 ⇓ n @ τ ⟧prim ∪ ⟦ K1 sporadic τ on K2 ⟧TESL≥ Suc n)
            ∩ (⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n)
          = ⟦ K1 sporadic τ on K2 ⟧TESL≥ n ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Γ ⟧⟧prim)›
      using TESL_interp_stepwise_sporadicon_coind_unfold by blast
    hence ‹⟦⟦ ((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ) ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
            ∪ ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦ K1 sporadic τ on K2 ⟧TESL≥ Suc n
           = ⟦⟦ (K1 sporadic τ on K2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Γ ⟧⟧prim› by auto
    thus ?thesis by auto
  qed
qed

lemma HeronConf_interp_stepwise_tagrel_cases:
   ‹⟦ Γ, n ⊢ ((time-relation ⌊K1, K2⌋ ∈ R) # Ψ) ▹ Φ ⟧config
    = ⟦ ((⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R) # Γ), n
        ⊢ Ψ ▹ ((time-relation ⌊K1, K2⌋ ∈ R) # Φ) ⟧config›
proof -
  have ‹⟦ Γ, n ⊢ (time-relation ⌊K1, K2⌋ ∈ R) # Ψ ▹ Φ ⟧config
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (time-relation ⌊K1, K2⌋ ∈ R) # Ψ ⟧⟧TESL≥ n
        ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n› by simp
  moreover have ‹⟦ ((⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R) # Γ), n
                  ⊢ Ψ ▹ ((time-relation ⌊K1, K2⌋ ∈ R) # Φ) ⟧config
                 = ⟦⟦ (⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                 ∩ ⟦⟦ (time-relation ⌊K1, K2⌋ ∈ R) # Φ ⟧⟧TESL≥ Suc n›
    by simp
  ultimately show ?thesis
  proof -
    have ‹⟦ ⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R ⟧prim
          ∩ ⟦ time-relation ⌊K1, K2⌋ ∈ R ⟧TESL≥ Suc n
          ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n = ⟦⟦ (time-relation ⌊K1, K2⌋ ∈ R) # Ψ ⟧⟧TESL≥ n›
      using TESL_interp_stepwise_tagrel_coind_unfold
            TESL_interpretation_stepwise_cons_morph by blast
    thus ?thesis by auto
  qed
qed

lemma HeronConf_interp_stepwise_implies_cases:
   ‹⟦ Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ ⟧config
      = ⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ) ⟧config
      ∪ ⟦ ((K1 ⇑ n) # (K2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ) ⟧config›
proof -
  have ‹⟦ Γ, n ⊢ (K1 implies K2) # Ψ ▹ Φ ⟧config
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (K1 implies K2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ) ⟧config
                = ⟦⟦ (K1 ¬⇑ n) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                ∩ ⟦⟦ (K1 implies K2) # Φ ⟧⟧TESL≥ Suc n› by simp
  moreover have ‹⟦ ((K1 ⇑ n) # (K2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ) ⟧config
                =  ⟦⟦ ((K1 ⇑ n) # (K2 ⇑ n) # Γ) ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                 ∩ ⟦⟦ (K1 implies K2) # Φ ⟧⟧TESL≥ Suc n› by simp
  ultimately show ?thesis
  proof -
    have f1: ‹(⟦ K1 ¬⇑ n ⟧prim ∪ ⟦ K1 ⇑ n ⟧prim ∩ ⟦ K2 ⇑ n ⟧prim)
                ∩ ⟦ K1 implies K2 ⟧TESL≥ Suc n ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n
                ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n)
              = ⟦⟦ (K1 implies K2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
      using TESL_interp_stepwise_implies_coind_unfold
            TESL_interpretation_stepwise_cons_morph by blast
    have ‹⟦ K1 ¬⇑ n ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim ∪ ⟦ K1 ⇑ n ⟧prim ∩ ⟦⟦ (K2 ⇑ n) # Γ ⟧⟧prim
         = (⟦ K1 ¬⇑ n ⟧prim ∪ ⟦ K1 ⇑ n ⟧prim ∩ ⟦ K2 ⇑ n ⟧prim) ∩ ⟦⟦ Γ ⟧⟧prim›
      by force
    hence ‹⟦ Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ ⟧config
      = (⟦ K1 ¬⇑ n ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim ∪ ⟦ K1 ⇑ n ⟧prim ∩ ⟦⟦ (K2 ⇑ n) # Γ ⟧⟧prim)
        ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ (K1 implies K2) # Φ ⟧⟧TESL≥ Suc n)›
      using f1 by (simp add: inf_left_commute inf_assoc)
    thus ?thesis by (simp add: Int_Un_distrib2 inf_assoc)
  qed
qed

lemma HeronConf_interp_stepwise_implies_not_cases:
   ‹⟦ Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ ⟧config
      = ⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ) ⟧config
      ∪ ⟦ ((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ) ⟧config›
proof -
  have ‹⟦ Γ, n ⊢ (K1 implies not K2) # Ψ ▹ Φ ⟧config
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (K1 implies not K2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ) ⟧config
                  = ⟦⟦ (K1 ¬⇑ n) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (K1 implies not K2) # Φ ⟧⟧TESL≥ Suc n› by simp
  moreover have ‹⟦ ((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ) ⟧config
                  = ⟦⟦ ((K1 ⇑ n) # (K2 ¬⇑ n) # Γ) ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (K1 implies not K2) # Φ ⟧⟧TESL≥ Suc n› by simp
  ultimately show ?thesis
  proof -
    have f1: ‹(⟦ K1 ¬⇑ n ⟧prim ∪ ⟦ K1 ⇑ n ⟧prim ∩ ⟦ K2 ¬⇑ n ⟧prim)
              ∩ ⟦ K1 implies not K2 ⟧TESL≥ Suc n
              ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n)
              = ⟦⟦ (K1 implies not K2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
      using TESL_interp_stepwise_implies_not_coind_unfold
            TESL_interpretation_stepwise_cons_morph by blast
    have ‹⟦ K1 ¬⇑ n ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim ∪ ⟦ K1 ⇑ n ⟧prim ∩ ⟦⟦ (K2 ¬⇑ n) # Γ ⟧⟧prim
           = (⟦ K1 ¬⇑ n ⟧prim ∪ ⟦ K1 ⇑ n ⟧prim ∩ ⟦ K2 ¬⇑ n ⟧prim) ∩ ⟦⟦ Γ ⟧⟧prim›
      by force
    then have ‹⟦ Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ ⟧config
                 = (⟦ K1 ¬⇑ n ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim ∪ ⟦ K1 ⇑ n ⟧prim
                    ∩ ⟦⟦ (K2 ¬⇑ n) # Γ ⟧⟧prim) ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n
                    ∩ ⟦⟦ (K1 implies not K2) # Φ ⟧⟧TESL≥ Suc n)›
      using f1 by (simp add: inf_left_commute inf_assoc)
    thus ?thesis by (simp add: Int_Un_distrib2 inf_assoc)
  qed
qed

lemma HeronConf_interp_stepwise_timedelayed_cases:
  ‹⟦ Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ ⟧config
    = ⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) ⟧config
    ∪ ⟦ ((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
        ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) ⟧config›
proof -
  have 1:‹⟦ Γ, n ⊢ (K1 time-delayed by δτ on K2 implies K3) # Ψ ▹ Φ ⟧config
         = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (K1 time-delayed by δτ on K2 implies K3) # Ψ ⟧⟧TESL≥ n
          ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n› by simp
  moreover have ‹⟦ ((K1 ¬⇑ n) # Γ), n
                  ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) ⟧config
                 = ⟦⟦ (K1 ¬⇑ n) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (K1 time-delayed by δτ on K2 implies K3) # Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ ((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
                  ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) ⟧config
                 = ⟦⟦ (K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (K1 time-delayed by δτ on K2 implies K3) # Φ ⟧⟧TESL≥ Suc n›
    by simp
  ultimately show ?thesis
  proof -
    have ‹⟦ Γ, n ⊢ (K1 time-delayed by δτ on K2 implies K3) # Ψ ▹ Φ ⟧config
      = ⟦⟦ Γ ⟧⟧prim ∩ (⟦⟦ (K1 time-delayed by δτ on K2 implies K3) # Ψ ⟧⟧TESL≥ n
        ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n)›
      using 1 by blast
    hence ‹⟦ Γ, n ⊢ (K1 time-delayed by δτ on K2 implies K3) # Ψ ▹ Φ ⟧config
          = (⟦ K1 ¬⇑ n ⟧prim ∪ ⟦ K1 ⇑ n ⟧prim ∩ ⟦ K2 @ n ⊕ δτ ⇒ K3 ⟧prim)
            ∩ (⟦⟦ Γ ⟧⟧prim ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n
            ∩ ⟦⟦ (K1 time-delayed by δτ on K2 implies K3) # Φ ⟧⟧TESL≥ Suc n))›
      using TESL_interpretation_stepwise_cons_morph
            TESL_interp_stepwise_timedelayed_coind_unfold
    proof -
      have ‹⟦⟦ (K1 time-delayed by δτ on K2 implies K3) # Ψ ⟧⟧TESL≥ n
            = (⟦ K1 ¬⇑ n ⟧prim ∪ ⟦ K1 ⇑ n ⟧prim ∩ ⟦ K2 @ n ⊕ δτ ⇒ K3 ⟧prim)
            ∩ ⟦ K1 time-delayed by δτ on K2 implies K3 ⟧TESL≥ Suc n ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n›
        using TESL_interp_stepwise_timedelayed_coind_unfold
              TESL_interpretation_stepwise_cons_morph by blast
      then show ?thesis
        by (simp add: Int_assoc Int_left_commute)
    qed
    then show ?thesis by (simp add: inf_assoc inf_sup_distrib2)
  qed
qed

lemma HeronConf_interp_stepwise_weakly_precedes_cases:
   ‹⟦ Γ, n ⊢ ((K1 weakly precedes K2) # Ψ) ▹ Φ ⟧config
    = ⟦ ((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
      ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ) ⟧config›
proof -
  have ‹⟦ Γ, n ⊢ (K1 weakly precedes K2) # Ψ ▹ Φ ⟧config
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (K1 weakly precedes K2) # Ψ ⟧⟧TESL≥ n
          ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n› by simp
  moreover have ‹⟦ ((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
                  ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ) ⟧config
                = ⟦⟦ (⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ ⟧⟧prim
                ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ (K1 weakly precedes K2) # Φ ⟧⟧TESL≥ Suc n›
    by simp
  ultimately show ?thesis
  proof -
    have ‹⟦ ⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x,y). x≤y) ⟧prim
            ∩ ⟦ K1 weakly precedes K2 ⟧TESL≥ Suc n ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
          = ⟦⟦ (K1 weakly precedes K2) # Ψ ⟧⟧TESL≥ n›
      using TESL_interp_stepwise_weakly_precedes_coind_unfold
            TESL_interpretation_stepwise_cons_morph by blast
    thus ?thesis by auto
  qed
qed

lemma HeronConf_interp_stepwise_strictly_precedes_cases:
   ‹⟦ Γ, n ⊢ ((K1 strictly precedes K2) # Ψ) ▹ Φ ⟧config
    = ⟦ ((⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
      ⊢ Ψ ▹ ((K1 strictly precedes K2) # Φ) ⟧config›
proof -
  have ‹⟦ Γ, n ⊢ (K1 strictly precedes K2) # Ψ ▹ Φ ⟧config
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (K1 strictly precedes K2) # Ψ ⟧⟧TESL≥ n
          ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n› by simp
  moreover have ‹⟦ ((⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
                  ⊢ Ψ ▹ ((K1 strictly precedes K2) # Φ) ⟧config
                = ⟦⟦ (⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ ⟧⟧prim
                ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                ∩ ⟦⟦ (K1 strictly precedes K2) # Φ ⟧⟧TESL≥ Suc n› by simp
  ultimately show ?thesis
  proof -
    have ‹⟦ ⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x,y). x≤y) ⟧prim
            ∩ ⟦ K1 strictly precedes K2 ⟧TESL≥ Suc n ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
          = ⟦⟦ (K1 strictly precedes K2) # Ψ ⟧⟧TESL≥ n›
      using TESL_interp_stepwise_strictly_precedes_coind_unfold
            TESL_interpretation_stepwise_cons_morph by blast
    thus ?thesis by auto
  qed
qed

lemma HeronConf_interp_stepwise_kills_cases:
   ‹⟦ Γ, n ⊢ ((K1 kills K2) # Ψ) ▹ Φ ⟧config
    = ⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ) ⟧config
    ∪ ⟦ ((K1 ⇑ n) # (K2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ) ⟧config›
proof -
  have ‹⟦ Γ, n ⊢ ((K1 kills K2) # Ψ) ▹ Φ ⟧config
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (K1 kills K2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ) ⟧config
                = ⟦⟦ (K1 ¬⇑ n) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (K1 kills K2) # Φ ⟧⟧TESL≥ Suc n› by simp
  moreover have ‹⟦ ((K1 ⇑ n) # (K2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ) ⟧config
                = ⟦⟦ (K1 ⇑ n) # (K2 ¬⇑ ≥ n) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (K1 kills K2) # Φ ⟧⟧TESL≥ Suc n› by simp
  ultimately show ?thesis
    proof -
      have ‹⟦⟦ (K1 kills K2) # Ψ ⟧⟧TESL≥ n
            = (⟦ (K1 ¬⇑ n) ⟧prim ∪ ⟦ (K1 ⇑ n) ⟧prim ∩ ⟦ (K2 ¬⇑ ≥ n) ⟧prim)
              ∩ ⟦ (K1 kills K2) ⟧TESL≥ Suc n ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n›
        using TESL_interp_stepwise_kills_coind_unfold
              TESL_interpretation_stepwise_cons_morph by blast
      thus ?thesis by auto
    qed
qed

end

Theory Hygge_Theory

chapter‹Main Theorems›

theory Hygge_Theory
imports
  Corecursive_Prop

begin
text ‹
  Using the properties we have shown about the interpretation of configurations 
  and the stepwise unfolding of the denotational semantics, we can now prove 
  several important results about the construction of runs from a specification.
›
section ‹Initial configuration›

text ‹
  The denotational semantics of a specification @{term ‹Ψ›} is the interpretation 
  at the first instant of a configuration which has @{term ‹Ψ›} as its present.
  This means that we can start to build a run that satisfies a specification by 
  starting from this configuration.
›
theorem solve_start:
  shows ‹⟦⟦ Ψ ⟧⟧TESL = ⟦ [], 0 ⊢ Ψ ▹ [] ⟧config›
  proof -
    have ‹⟦⟦ Ψ ⟧⟧TESL = ⟦⟦ Ψ ⟧⟧TESL≥ 0›
    by (simp add: TESL_interpretation_stepwise_zero')
    moreover have ‹⟦ [], 0 ⊢ Ψ ▹ [] ⟧config =
                      ⟦⟦ [] ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ 0 ∩ ⟦⟦ [] ⟧⟧TESL≥ Suc 0›
    by simp
    ultimately show ?thesis by auto
  qed

section ‹Soundness›
text ‹
  The interpretation of a configuration @{term ‹𝒮2›} that is a refinement of a
  configuration @{term ‹𝒮1›} is contained in the interpretation of @{term ‹𝒮1›}.
  This means that by making successive choices in building the instants of a run,
  we preserve the soundness of the constructed run with regard to the original 
  specification.
›
lemma sound_reduction:
  assumes ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1)  ↪  (Γ2, n2 ⊢ Ψ2 ▹ Φ2)›
  shows ‹⟦⟦ Γ1 ⟧⟧prim ∩ ⟦⟦ Ψ1 ⟧⟧TESL≥ n1 ∩ ⟦⟦ Φ1 ⟧⟧TESL≥ Suc n1
          ⊇  ⟦⟦ Γ2 ⟧⟧prim ∩ ⟦⟦ Ψ2 ⟧⟧TESL≥ n2 ∩ ⟦⟦ Φ2 ⟧⟧TESL≥ Suc n2› (is ?P)
proof -
  from assms consider
    (a) ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1)  ↪i  (Γ2, n2 ⊢ Ψ2 ▹ Φ2)›
  | (b) ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1)  ↪e  (Γ2, n2 ⊢ Ψ2 ▹ Φ2)›
    using operational_semantics_step.simps by blast
  thus ?thesis
  proof (cases)
    case a
      thus ?thesis by (simp add: operational_semantics_intro.simps)
  next
    case b thus ?thesis
    proof (rule operational_semantics_elim.cases)
      fix  Γ n K1 τ K2 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) = (Γ, n ⊢ (K1 sporadic τ on K2) # Ψ ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) = (Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_sporadicon_cases
                    HeronConf_interpretation.simps by blast
    next
      fix  Γ n K1 τ K2 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) = (Γ, n ⊢ (K1 sporadic τ on K2) # Ψ ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) = (((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ)›
      thus ?P using HeronConf_interp_stepwise_sporadicon_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K1 K2 R Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) = (Γ, n ⊢ (time-relation ⌊K1, K2⌋ ∈ R) # Ψ ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) = (((⌊τvar (K1, n), τvar (K2, n)⌋ ∈ R) # Γ), n
                                      ⊢ Ψ ▹ ((time-relation ⌊K1, K2⌋ ∈ R) # Φ))›
      thus ?P using HeronConf_interp_stepwise_tagrel_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K1 K2 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) = (Γ, n ⊢ (K1 implies K2) # Ψ ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) = (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_implies_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K1 K2 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) = (Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) = (((K1 ⇑ n) # (K2 ⇑ n) # Γ), n
                                   ⊢ Ψ ▹ ((K1 implies K2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_implies_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K1 K2 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) = (Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) = (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_implies_not_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K1 K2 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) = (Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) = (((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n
                                   ⊢ Ψ ▹ ((K1 implies not K2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_implies_not_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K1 δτ K2 K3 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) =
                (Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) =
            (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))›
      thus ?P using HeronConf_interp_stepwise_timedelayed_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K1 δτ K2 K3 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) =
               (Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2)
            = (((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
                ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))›
      thus ?P using HeronConf_interp_stepwise_timedelayed_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K1 K2 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) = (Γ, n ⊢ ((K1 weakly precedes K2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) = (((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_weakly_precedes_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K1 K2 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) = (Γ, n ⊢ ((K1 strictly precedes K2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) = (((⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊢ Ψ ▹ ((K1 strictly precedes K2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_strictly_precedes_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K1 K2 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) = (Γ, n ⊢ ((K1 kills K2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) = (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_kills_cases
                    HeronConf_interpretation.simps by blast
    next
      fix Γ n K1 K2 Ψ Φ
      assume ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1) = (Γ, n ⊢ ((K1 kills K2) # Ψ) ▹ Φ)›
      and ‹(Γ2, n2 ⊢ Ψ2 ▹ Φ2) =
            (((K1 ⇑ n) # (K2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ))›
      thus ?P using HeronConf_interp_stepwise_kills_cases
                    HeronConf_interpretation.simps by blast
    qed
  qed
qed

inductive_cases step_elim:‹𝒮1 ↪ 𝒮2›

lemma sound_reduction':
  assumes ‹𝒮1 ↪ 𝒮2›
  shows ‹⟦ 𝒮1 ⟧config ⊇ ⟦ 𝒮2 ⟧config›
proof -
  have ‹∀s1 s2. (⟦ s2 ⟧config ⊆ ⟦ s1 ⟧config) ∨ ¬(s1 ↪ s2)›
    using sound_reduction by fastforce
  thus ?thesis using assms by blast
qed

lemma sound_reduction_generalized:
  assumes ‹𝒮1 ↪k 𝒮2›
    shows ‹⟦ 𝒮1 ⟧config ⊇ ⟦ 𝒮2 ⟧config›
proof -
  from assms show ?thesis
  proof (induction k arbitrary: 𝒮2)
    case 0
      hence *: ‹𝒮1 ↪0 𝒮2 ⟹ 𝒮1 = 𝒮2› by auto
      moreover have ‹𝒮1 = 𝒮2› using * "0.prems" by linarith
      ultimately show ?case by auto
  next
    case (Suc k)
      thus ?case
      proof -
        fix k :: nat
        assume ff: ‹𝒮1 ↪Suc k 𝒮2›
        assume hi: ‹⋀𝒮2. 𝒮1 ↪k 𝒮2 ⟹ ⟦ 𝒮2 ⟧config ⊆ ⟦ 𝒮1 ⟧config›
        obtain 𝒮n where red_decomp: ‹(𝒮1 ↪k 𝒮n) ∧ (𝒮n ↪ 𝒮2)› using ff by auto
        hence ‹⟦ 𝒮1 ⟧config ⊇ ⟦ 𝒮n ⟧config› using hi by simp
        also have ‹⟦ 𝒮n ⟧config ⊇ ⟦ 𝒮2 ⟧config› by (simp add: red_decomp sound_reduction')
        ultimately show ‹⟦ 𝒮1 ⟧config ⊇ ⟦ 𝒮2 ⟧config› by simp
      qed
  qed
qed

text ‹
  From the initial configuration, a configuration @{term ‹𝒮›} obtained after any 
  number @{term ‹k›} of reduction steps denotes runs from the 
  initial specification @{term ‹Ψ›}.
›
theorem soundness:
  assumes ‹([], 0 ⊢ Ψ ▹ []) ↪k 𝒮›
    shows ‹⟦⟦ Ψ ⟧⟧TESL ⊇ ⟦ 𝒮 ⟧config›
  using assms sound_reduction_generalized solve_start by blast

section ‹Completeness›

text ‹
  We will now show that any run that satisfies a specification can be derived
  from the initial configuration, at any number of steps.

  We start by proving that any run that is denoted by a configuration @{term ‹𝒮›}
  is necessarily denoted by at least one of the configurations that can be reached
  from @{term ‹𝒮›}.
›
lemma complete_direct_successors:
  shows ‹⟦ Γ, n ⊢ Ψ ▹ Φ ⟧config ⊆ (⋃X∈𝒞next (Γ, n ⊢ Ψ ▹ Φ). ⟦ X ⟧config)›
  proof (induct Ψ)
    case Nil
    show ?case
      using HeronConf_interp_stepwise_instant_cases operational_semantics_step.simps
            operational_semantics_intro.instant_i
      by fastforce
  next
    case (Cons ψ Ψ)  thus ?case
      proof (cases ψ)
        case (SporadicOn K1 τ K2) thus ?thesis 
          using HeronConf_interp_stepwise_sporadicon_cases
                                      [of ‹Γ› ‹n› ‹K1› ‹τ› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_sporadicon[of ‹Γ› ‹n› ‹Ψ› ‹K1› ‹τ› ‹K2› ‹Φ›] by blast
      next
        case (TagRelation K1 K2 R) thus ?thesis
          using HeronConf_interp_stepwise_tagrel_cases
                                  [of ‹Γ› ‹n› ‹K1› ‹K2› ‹R› ‹Ψ› ‹Φ›]
                Cnext_solve_tagrel[of ‹K1› ‹n› ‹K2› ‹R› ‹Γ› ‹Ψ› ‹Φ›] by blast
      next
        case (Implies K1 K2) thus ?thesis
          using HeronConf_interp_stepwise_implies_cases
                                   [of ‹Γ› ‹n› ‹K1› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_implies[of ‹K1› ‹n› ‹Γ› ‹Ψ› ‹K2› ‹Φ›] by blast
      next
        case (ImpliesNot K1 K2) thus ?thesis
          using HeronConf_interp_stepwise_implies_not_cases
                                       [of ‹Γ› ‹n› ‹K1› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_implies_not[of ‹K1› ‹n› ‹Γ› ‹Ψ› ‹K2› ‹Φ›] by blast
      next
        case (TimeDelayedBy Kmast τ Kmeas Kslave) thus ?thesis
          using HeronConf_interp_stepwise_timedelayed_cases
                          [of ‹Γ› ‹n› ‹Kmast› ‹τ› ‹Kmeas› ‹Kslave› ‹Ψ› ‹Φ›]
                Cnext_solve_timedelayed
                          [of ‹Kmast› ‹n› ‹Γ› ‹Ψ› ‹τ› ‹Kmeas› ‹Kslave› ‹Φ›] by blast
      next
        case (WeaklyPrecedes K1 K2) thus ?thesis
          using HeronConf_interp_stepwise_weakly_precedes_cases
                                           [of ‹Γ› ‹n› ‹K1› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_weakly_precedes[of ‹K2› ‹n› ‹K1› ‹Γ› ‹Ψ›  ‹Φ›]
          by blast
      next
        case (StrictlyPrecedes K1 K2)  thus ?thesis
          using HeronConf_interp_stepwise_strictly_precedes_cases
                                             [of ‹Γ› ‹n› ‹K1› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_strictly_precedes[of ‹K2› ‹n› ‹K1› ‹Γ› ‹Ψ›  ‹Φ›]
          by blast
      next
        case (Kills K1 K2) thus ?thesis
          using HeronConf_interp_stepwise_kills_cases[of ‹Γ› ‹n› ‹K1› ‹K2› ‹Ψ› ‹Φ›]
                Cnext_solve_kills[of ‹K1› ‹n› ‹Γ› ‹Ψ› ‹K2› ‹Φ›] by blast
      qed
  qed

lemma complete_direct_successors':
  shows ‹⟦ 𝒮 ⟧config ⊆ (⋃X∈𝒞next 𝒮. ⟦ X ⟧config)›
proof -
  from HeronConf_interpretation.cases obtain Γ n Ψ Φ
    where ‹𝒮 = (Γ, n ⊢ Ψ ▹ Φ)› by blast
  with complete_direct_successors[of ‹Γ› ‹n› ‹Ψ› ‹Φ›] show ?thesis by simp
qed

text ‹
  Therefore, if a run belongs to a configuration, it necessarily belongs to a
  configuration derived from it.
›
lemma branch_existence:
  assumes ‹ρ ∈ ⟦ 𝒮1 ⟧config›
  shows ‹∃𝒮2. (𝒮1 ↪ 𝒮2) ∧ (ρ ∈ ⟦ 𝒮2 ⟧config)›
proof -
  from assms complete_direct_successors' have ‹ρ ∈ (⋃X∈𝒞next 𝒮1. ⟦ X ⟧config)› by blast
  hence ‹∃s∈𝒞next 𝒮1. ρ ∈ ⟦ s ⟧config› by simp
  thus ?thesis by blast
qed

lemma branch_existence':
  assumes ‹ρ ∈ ⟦ 𝒮1 ⟧config›
  shows ‹∃𝒮2. (𝒮1 ↪k 𝒮2) ∧ (ρ ∈ ⟦ 𝒮2 ⟧config)›
proof (induct k)
  case 0
    thus ?case by (simp add: assms)
next
  case (Suc k)
    thus ?case
      using branch_existence relpowp_Suc_I[of ‹k› ‹operational_semantics_step›]
    by blast
qed

text‹
  Any run that belongs to the original specification @{term ‹Ψ›} has a corresponding 
  configuration @{term ‹𝒮›} at any number @{term ‹k›} of reduction steps
  from the initial configuration. Therefore, any run that satisfies a specification
  can be derived from the initial configuration at any level of reduction.
›
theorem completeness:
  assumes ‹ρ ∈ ⟦⟦ Ψ ⟧⟧TESL›
  shows ‹∃𝒮. (([], 0 ⊢ Ψ ▹ [])  ↪k  𝒮)
           ∧ ρ ∈ ⟦ 𝒮 ⟧config›
  using assms branch_existence' solve_start by blast

section ‹Progress›

text ‹
  Reduction steps do not guarantee that the construction of a run progresses in the
  sequence of instants. We need to show that it is always possible to reach the next 
  instant, and therefore any future instant, through a number of steps.
›
lemma instant_index_increase:
  assumes ‹ρ ∈ ⟦ Γ, n ⊢ Ψ ▹ Φ ⟧config›
  shows   ‹∃Γk Ψk Φk k. ((Γ, n ⊢ Ψ ▹ Φ)  ↪k  (Γk, Suc n ⊢ Ψk ▹ Φk))
                         ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
proof (insert assms, induct Ψ arbitrary: Γ Φ)
  case (Nil Γ Φ)
    then show ?case
    proof -
      have ‹(Γ, n ⊢ [] ▹ Φ) ↪1 (Γ, Suc n ⊢ Φ ▹ [])›
        using instant_i intro_part by fastforce
      moreover have ‹⟦ Γ, n ⊢ [] ▹ Φ ⟧config = ⟦ Γ, Suc n ⊢ Φ ▹ [] ⟧config›
        by auto
      moreover have ‹ρ ∈ ⟦ Γ, Suc n ⊢ Φ ▹ [] ⟧config›
        using assms Nil.prems calculation(2) by blast
      ultimately show ?thesis by blast
    qed
next
  case (Cons ψ Ψ)
    then show ?case
    proof (induct ψ)
      case (SporadicOn K1 τ K2)
        have branches: ‹⟦ Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ ⟧config
                      = ⟦ Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ) ⟧config
                      ∪ ⟦ ((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ ⟧config›
          using HeronConf_interp_stepwise_sporadicon_cases by simp
        have br1: ‹ρ ∈ ⟦ Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ) ⟧config
                    ⟹ ∃Γk Ψk Φk k.
                      ((Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ)
                          ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                      ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
        proof -
          assume h1: ‹ρ ∈ ⟦ Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ) ⟧config›
          hence ‹∃Γk Ψk Φk k. ((Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ))
                                      ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                                 ∧ (ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config)›
            using h1 SporadicOn.prems by simp
          from this obtain Γk Ψk Φk k where
              fp:‹((Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ))
                    ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config› by blast
          have
            ‹(Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ)
              ↪ (Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ))›
            by (simp add: elims_part sporadic_on_e1)
          with fp relpowp_Suc_I2 have
            ‹((Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ)
              ↪Suc k (Γk, Suc n ⊢ Ψk ▹ Φk))› by auto
          thus ?thesis using fp by blast
        qed
        have br2: ‹ρ ∈ ⟦ ((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ ⟧config
                  ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ)
                                        ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                            ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
        proof -
          assume h2: ‹ρ ∈ ⟦ ((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ ⟧config›
          hence ‹∃Γk Ψk Φk k. ((((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ)
                                    ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                             ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
            using h2 SporadicOn.prems by simp

            from this obtain Γk Ψk Φk k
            where fp:‹((((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ)
                            ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))›
              and rc:‹ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config› by blast
            have pc:‹(Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ)
              ↪ (((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ)›
            by (simp add: elims_part sporadic_on_e2)
            hence ‹(Γ, n ⊢ (K1 sporadic τ on K2) # Ψ ▹ Φ)
                    ↪Suc k (Γk, Suc n ⊢ Ψk ▹ Φk)›
                using fp relpowp_Suc_I2 by auto
            with rc show ?thesis by blast
        qed
        from branches SporadicOn.prems(2) have
          ‹ρ ∈ ⟦ Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ) ⟧config
             ∪ ⟦ ((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ ⟧config›
          by simp
        with br1 br2 show ?case by blast
  next
    case (TagRelation K1 K2 R)
      have branches: ‹⟦ Γ, n ⊢ ((time-relation ⌊K1, K2⌋ ∈ R) # Ψ) ▹ Φ ⟧config
          = ⟦ ((⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R) # Γ), n
              ⊢ Ψ ▹ ((time-relation ⌊K1, K2⌋ ∈ R) # Φ) ⟧config›
        using HeronConf_interp_stepwise_tagrel_cases by simp
      thus ?case
      proof -
        have ‹∃Γk Ψk Φk k.
            ((((⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R) # Γ), n
                ⊢ Ψ ▹ ((time-relation ⌊K1, K2⌋ ∈ R) # Φ))
              ↪k (Γk, Suc n ⊢ Ψk ▹ Φk)) ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
          using TagRelation.prems by simp

        from this obtain Γk Ψk Φk k
          where fp:‹((((⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R) # Γ), n
                        ⊢ Ψ ▹ ((time-relation ⌊K1, K2⌋ ∈ R) # Φ))
                    ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))›
            and rc:‹ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config› by blast
        have pc:‹(Γ, n ⊢ ((time-relation ⌊K1, K2⌋ ∈ R) # Ψ) ▹ Φ)
            ↪ (((⌊τvar (K1, n), τvar (K2, n)⌋ ∈ R) # Γ), n
                  ⊢ Ψ ▹ ((time-relation ⌊K1, K2⌋ ∈ R) # Φ))›
          by (simp add: elims_part tagrel_e)
        hence ‹(Γ, n ⊢ (time-relation ⌊K1, K2⌋ ∈ R) # Ψ ▹ Φ)
                ↪Suc k (Γk, Suc n ⊢ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
  next
    case (Implies K1 K2)
      have branches: ‹⟦ Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ ⟧config
          = ⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ) ⟧config
          ∪ ⟦ ((K1 ⇑ n) # (K2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ) ⟧config›
        using HeronConf_interp_stepwise_implies_cases by simp
      moreover have br1: ‹ρ ∈ ⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ) ⟧config
                ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ)
                                    ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                  ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
      proof -
        assume h1: ‹ρ ∈ ⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ) ⟧config›
        then have ‹∃Γk Ψk Φk k.
                    ((((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ))
                        ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                  ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
          using h1 Implies.prems by simp
        from this obtain Γk Ψk Φk k where
          fp:‹((((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ))
            ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))›
          and rc:‹ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config› by blast
        have pc:‹(Γ, n ⊢ (K1 implies K2) # Ψ ▹ Φ)
                  ↪ (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ))›
          by (simp add: elims_part implies_e1)
        hence ‹(Γ, n ⊢ (K1 implies K2) # Ψ ▹ Φ) ↪Suc k (Γk, Suc n ⊢ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2: ‹ρ ∈ ⟦ ((K1 ⇑ n) # (K2 ⇑ n) # Γ), n
                                ⊢ Ψ ▹ ((K1 implies K2) # Φ) ⟧config
                            ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ)
                                              ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                                  ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
      proof -
        assume h2: ‹ρ ∈ ⟦ ((K1 ⇑ n) # (K2 ⇑ n) # Γ), n
                          ⊢ Ψ ▹ ((K1 implies K2) # Φ) ⟧config›
        then have ‹∃Γk Ψk Φk k. (
                        (((K1 ⇑ n) # (K2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ))
                          ↪k (Γk, Suc n ⊢ Ψk ▹ Φk)
                    ) ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
          using h2 Implies.prems by simp
        from this obtain Γk Ψk Φk k where
            fp:‹(((K1 ⇑ n) # (K2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ))
                ↪k (Γk, Suc n ⊢ Ψk ▹ Φk)›
        and rc:‹ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config› by blast
        have ‹(Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ)
              ↪ (((K1 ⇑ n) # (K2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ))›
          by (simp add: elims_part implies_e2)
        hence ‹(Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ) ↪Suc k (Γk, Suc n ⊢ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      ultimately show ?case using Implies.prems(2) by blast
  next
    case (ImpliesNot K1 K2)
      have branches: ‹⟦ Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ ⟧config
          = ⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ) ⟧config
          ∪ ⟦ ((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ) ⟧config›
        using HeronConf_interp_stepwise_implies_not_cases by simp
      moreover have br1: ‹ρ ∈ ⟦ ((K1 ¬⇑ n) # Γ), n
                            ⊢ Ψ ▹ ((K1 implies not K2) # Φ) ⟧config
                ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ)
                                    ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                  ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
      proof -
        assume h1: ‹ρ ∈ ⟦ ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ) ⟧config›
        then have ‹∃Γk Ψk Φk k.
                    ((((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ))
                      ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                  ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
          using h1 ImpliesNot.prems by simp
        from this obtain Γk Ψk Φk k where
          fp:‹((((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ))
                ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))›
          and rc:‹ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config› by blast
        have pc:‹(Γ, n ⊢ (K1 implies not K2) # Ψ ▹ Φ)
                  ↪ (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ))›
          by (simp add: elims_part implies_not_e1)
        hence ‹(Γ, n ⊢ (K1 implies not K2) # Ψ ▹ Φ) ↪Suc k (Γk, Suc n ⊢ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2: ‹ρ ∈ ⟦ ((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n
                            ⊢ Ψ ▹ ((K1 implies not K2) # Φ) ⟧config
                            ⟹ ∃Γk Ψk Φk k. ((Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ)
                                              ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                                  ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
      proof -
        assume h2: ‹ρ ∈ ⟦ ((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n
                          ⊢ Ψ ▹ ((K1 implies not K2) # Φ) ⟧config›
        then have ‹∃Γk Ψk Φk k. (
                     (((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n
                       ⊢ Ψ ▹ ((K1 implies not K2) # Φ)) ↪k (Γk, Suc n ⊢ Ψk ▹ Φk)
                    ) ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
          using h2 ImpliesNot.prems by simp
        from this obtain Γk Ψk Φk k where
            fp:‹(((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ))
                ↪k (Γk, Suc n ⊢ Ψk ▹ Φk)›
        and rc:‹ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config› by blast
        have ‹(Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ)
              ↪ (((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ))›
          by (simp add: elims_part implies_not_e2)
        hence ‹(Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ)
                ↪Suc k (Γk, Suc n ⊢ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      ultimately show ?case  using ImpliesNot.prems(2) by blast
  next
    case (TimeDelayedBy K1 δτ K2 K3)
      have branches:
        ‹⟦ Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ ⟧config
          = ⟦ ((K1 ¬⇑ n) # Γ), n
              ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) ⟧config
          ∪ ⟦ ((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
              ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) ⟧config›
        using HeronConf_interp_stepwise_timedelayed_cases by simp
      moreover have br1:
        ‹ρ ∈ ⟦ ((K1 ¬⇑ n) # Γ), n
              ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) ⟧config
          ⟹ ∃Γk Ψk Φk k.
            ((Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)
                ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
            ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
      proof -
        assume h1: ‹ρ ∈ ⟦ ((K1 ¬⇑ n) # Γ), n
                         ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) ⟧config›
        then have ‹∃Γk Ψk Φk k.
          ((((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))
            ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
          ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
          using h1 TimeDelayedBy.prems by simp
        from this obtain Γk Ψk Φk k
          where fp:‹(((K1 ¬⇑ n) # Γ), n
                      ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))
                    ↪k (Γk, Suc n ⊢ Ψk ▹ Φk)›
            and rc:‹ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config› by blast
        have ‹(Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)
              ↪ (((K1 ¬⇑ n) # Γ), n
                    ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))›
          by (simp add: elims_part timedelayed_e1)
        hence ‹(Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)
                ↪Suc k (Γk, Suc n ⊢ Ψk ▹ Φk)›
          using fp relpowp_Suc_I2 by auto
        with rc show ?thesis by blast
      qed
      moreover have br2:
        ‹ρ ∈ ⟦ ((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
              ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) ⟧config
          ⟹ ∃Γk Ψk Φk k.
              ((Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)
                ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
              ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
      proof -
        assume h2: ‹ρ ∈ ⟦ ((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
                    ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) ⟧config›
        then have ‹∃Γk Ψk Φk k. ((((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
                                 ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))
                                 ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                                ∧ ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config›
          using h2 TimeDelayedBy.prems by simp
        from this obtain Γk Ψk Φk k
          where fp:‹(((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
                         ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))
                       ↪k (Γk, Suc n ⊢ Ψk ▹ Φk)›
            and rc:‹ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config› by blast
        have ‹(Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)
              ↪ (((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
                  ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))›
          by (simp add: elims_part timedelayed_e2)
        with fp relpowp_Suc_I2 have
          ‹(Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)
            ↪Suc k (Γk, Suc n ⊢ Ψk ▹ Φk)›
          by auto
        with rc show ?thesis by blast
      qed
      ultimately show ?case using TimeDelayedBy.prems(2) by blast
  next
    case (WeaklyPrecedes K1 K2)
      have ‹⟦ Γ, n ⊢ ((K1 weakly precedes K2) # Ψ) ▹ Φ ⟧config =
        ⟦ ((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
            ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ) ⟧config›
        using HeronConf_interp_stepwise_weakly_precedes_cases by simp
      moreover have ‹ρ ∈ ⟦ ((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                            ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ) ⟧config
            ⟹ (∃Γk Ψk Φk k. ((Γ, n ⊢ ((K1 weakly precedes K2) # Ψ) ▹ Φ)
                                  ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                ∧ (ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config))›
      proof -
        assume ‹ρ ∈ ⟦ ((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                        ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ) ⟧config›
        hence ‹∃Γk Ψk Φk k. ((((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ))
                             ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                          ∧ (ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config)›
          using  WeaklyPrecedes.prems by simp
        from this obtain Γk Ψk Φk k
          where fp:‹(((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                                  ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ))
                             ↪k (Γk, Suc n ⊢ Ψk ▹ Φk)›
            and rc:‹ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config› by blast
        have ‹(Γ, n ⊢ ((K1 weakly precedes K2) # Ψ) ▹ Φ)
                ↪ (((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
              ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ))›
          by (simp add: elims_part weakly_precedes_e)
        with fp relpowp_Suc_I2 have ‹(Γ, n ⊢ ((K1 weakly precedes K2) # Ψ) ▹ Φ)
                                      ↪Suc k (Γk, Suc n ⊢ Ψk ▹ Φk)›
          by auto
        with rc show ?thesis by blast
      qed
      ultimately show ?case using WeaklyPrecedes.prems(2) by blast
  next
    case (StrictlyPrecedes K1 K2)
      have ‹⟦ Γ, n ⊢ ((K1 strictly precedes K2) # Ψ) ▹ Φ ⟧config =
        ⟦ ((⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
          ⊢ Ψ ▹ ((K1 strictly precedes K2) # Φ) ⟧config›
        using HeronConf_interp_stepwise_strictly_precedes_cases by simp
      moreover have ‹ρ ∈ ⟦ ((⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                            ⊢ Ψ ▹ ((K1 strictly precedes K2) # Φ) ⟧config
            ⟹ (∃Γk Ψk Φk k. ((Γ, n ⊢ ((K1 strictly precedes K2) # Ψ) ▹ Φ)
                                  ↪k (Γk, Suc n ⊢ Ψk ▹ Φk))
                ∧ (ρ ∈ ⟦ Γk, Suc n ⊢ Ψk ▹ Φk ⟧config))›
      proof -
        assume ‹ρ ∈ ⟦ ((⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ), n
                        ⊢ Ψ ▹ ((K1 strictly precedes K2) # Φ) ⟧config›
        hence ‹∃Γk Ψk Φk k. ((((⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x, y). x ≤ y)) # Γ