Theory Coinductive_Prop

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

theory Coinductive_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
  ‹⟦ C1 sporadic τ on C2 ⟧TESL≥ i =
      {ρ. ∃n≥i. ticks ((Rep_run ρ) n C1) ∧ time ((Rep_run ρ) n C2) = τ}›
| ‹⟦ C1 sporadic♯ ⦇τvar(Cpast, npast) ⊕ δτ⦈ on C2 ⟧TESL≥ i =
      {ρ. ∃n≥i. ticks ((Rep_run ρ) n C1)
                         ∧ time ((Rep_run ρ) n C2) = time ((Rep_run ρ) npast Cpast) + δτ }›
| ‹⟦ time-relation ⌊C1, C2⌋ ∈ R ⟧TESL≥ i =
      {ρ. ∀n≥i. R (time ((Rep_run ρ) n C1), time ((Rep_run ρ) n C2))}›
| ‹⟦ master implies slave ⟧TESL≥ i =
      {ρ. ∀n≥i. ticks ((Rep_run ρ) n master) ⟶ ticks ((Rep_run ρ) n slave)}›
| ‹⟦ master implies not slave ⟧TESL≥ i =
      {ρ. ∀n≥i. ticks ((Rep_run ρ) n master) ⟶ ¬ ticks ((Rep_run ρ) n slave)}›
| ‹⟦ master time-delayed by δτ on measuring implies slave ⟧TESL≥ i =
      {ρ. ∀n≥i. ticks ((Rep_run ρ) n master) ⟶
               (let measured_time = time ((Rep_run ρ) n measuring) in
                ∀m ≥ n. first_time ρ measuring m (measured_time + δτ)
                         ⟶ ticks ((Rep_run ρ) m slave)
               )
      }›
| ‹⟦ master time-delayed⨝ by δτ on measuring implies slave ⟧TESL≥ i =
      {ρ. ∀n≥i. ticks ((Rep_run ρ) n master) ⟶
               (let measured_time = time ((Rep_run ρ) n measuring) in
                ∃m ≥ n. ticks ((Rep_run ρ) m slave)
                          ∧ time ((Rep_run ρ) m measuring) = measured_time + δτ
               )
      }›
| ‹⟦ C1 weakly precedes C2 ⟧TESL≥ i =
      {ρ. ∀n≥i. (run_tick_count ρ C2 n) ≤ (run_tick_count ρ C1 n)}›
| ‹⟦ C1 strictly precedes C2 ⟧TESL≥ i =
      {ρ. ∀n≥i. (run_tick_count ρ C2 n) ≤ (run_tick_count_strictly ρ C1 n)}›
| ‹⟦ C1 kills C2 ⟧TESL≥ i =
      {ρ. ∀n≥i. ticks ((Rep_run ρ) n C1) ⟶ (∀m≥n. ¬ ticks ((Rep_run ρ) m C2))}›

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

lemma TESL_interp_unfold_stepwise_sporadicon_tvar:
  ‹⟦ C1 sporadic♯ τexpr on C2 ⟧TESL = ⋃ {Y. ∃n::nat. Y = ⟦ C1 sporadic♯ τexpr on C2 ⟧TESL≥ n}›
proof (induction τexpr)
  case (AddDelay x1a τ)
  then show ?case 
  proof (induction x1a)
    case (TSchematic xa)
    then show ?case
    proof (induction xa)
      case (Pair K n')
      then show ?case by auto
    qed
  qed
qed

lemma TESL_interp_unfold_stepwise_tagrelgen:
  ‹⟦ time-relation ⌊C1, C2⌋ ∈ R ⟧TESL
    = ⋂ {Y. ∃n::nat. Y = ⟦ time-relation ⌊C1, C2⌋ ∈ 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_timedelayed_tvar:
  ‹⟦ 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:
  ‹⟦ C1 weakly precedes C2 ⟧TESL
    = ⋂ {Y. ∃n::nat. Y = ⟦ C1 weakly precedes C2 ⟧TESL≥ n}›
by auto

lemma TESL_interp_unfold_stepwise_strictly_precedes:
  ‹⟦ C1 strictly precedes C2 ⟧TESL
    = ⋂ {Y. ∃n::nat. Y = ⟦ C1 strictly precedes C2 ⟧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 (cases φ)
  case SporadicOn thus ?thesis using TESL_interp_unfold_stepwise_sporadicon by simp
next
  case SporadicOnTvar thus ?thesis using TESL_interp_unfold_stepwise_sporadicon_tvar by simp
next
  case TagRelation thus ?thesis using assms by simp
next
  case Implies thus ?thesis using assms by simp
next
  case ImpliesNot thus ?thesis using assms by simp
next
  case TimeDelayedBy thus ?thesis using assms by simp
next
  case RelaxedTimeDelayed thus ?thesis using assms by simp
next
  case WeaklyPrecedes thus ?thesis using assms by simp
next
  case StrictlyPrecedes thus ?thesis using assms by simp
next
  case Kills thus ?thesis using assms by simp
  qed
(*
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 SporadicOnTvar 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 RelaxedTimeDelayed
    thus ?thesis using TESL_interp_unfold_stepwise_timedelayed_tvar 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:
  ‹⟦ C1 sporadic τ on C2 ⟧TESL≥ n =
    ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 ⇓ n @ τ ⟧prim        ― ‹rule @{term sporadic_on_e2}›
    ∪ ⟦ C1 sporadic τ on C2 ⟧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. ticks (Rep_run ρ n C1)
                                     ∧ time (Rep_run ρ n C2) = τ›]
by (simp add: Collect_conj_eq)

lemma TESL_interp_stepwise_sporadicon_tvar_coind_unfold:
  ‹⟦ C1 sporadic♯ ⦇τvar(K, n') ⊕ τ⦈ on C2 ⟧TESL≥ n =
    ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 ⇓ n @♯ ⦇τvar(K, n') ⊕ τ⦈ ⟧prim
    ∪ ⟦ C1 sporadic♯ ⦇τvar(K, n') ⊕ τ⦈ on C2 ⟧TESL≥ Suc n›
proof -
  have ‹{ ρ. ∃m≥n. ticks ((Rep_run ρ) m C1) = True ∧ time ((Rep_run ρ) m C2) = time ((Rep_run ρ) n' K) + τ }
      = { ρ. ticks ((Rep_run ρ) n C1) = True ∧ time ((Rep_run ρ) n C2) = time ((Rep_run ρ) n' K) + τ
             ∨ (∃m≥Suc n. ticks ((Rep_run ρ) m C1) = True ∧ time ((Rep_run ρ) m C2) = time ((Rep_run ρ) n' K) + τ) }›
    using Suc_leD not_less_eq_eq by fastforce
  then show ?thesis by auto
qed

lemma TESL_interp_stepwise_sporadicon_tvar_coind_unfold2:
  ‹⟦ C1 sporadic♯ τexpr on C2 ⟧TESL≥ n =
    ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 ⇓ n @♯ τexpr ⟧prim        ― ‹rule @{term sporadic_on_tvar_e2}›
    ∪ ⟦ C1 sporadic♯ τexpr on C2 ⟧TESL≥ Suc n›   ― ‹rule @{term sporadic_on_tvar_e1}›
proof -
  from tag_expr.exhaust obtain v τ where ‹ τexpr=⦇ v ⊕ τ ⦈› by blast
  moreover from tag_var.exhaust obtain K n where ‹v=τvar(K, n)› by auto
  ultimately have ‹τexpr=⦇ τvar(K, n) ⊕ τ ⦈› by simp
  thus ?thesis using TESL_interp_stepwise_sporadicon_tvar_coind_unfold by blast
qed

lemma TESL_interp_stepwise_tagrel_coind_unfold:
  ‹⟦ time-relation ⌊C1, C2⌋ ∈ R ⟧TESL≥ n =        ― ‹rule @{term tagrel_e}›
     ⟦ ⌊τvar(C1, n), τvar(C2, n)⌋ ∈ R ⟧prim
     ∩ ⟦ time-relation ⌊C1, C2⌋ ∈ R ⟧TESL≥ Suc n›
proof -
  have ‹{ρ. ∀m≥n. R (time ((Rep_run ρ) m C1), time ((Rep_run ρ) m C2))}
       = {ρ. R (time ((Rep_run ρ) n C1), time ((Rep_run ρ) n C2))}
       ∩ {ρ. ∀m≥Suc n. R (time ((Rep_run ρ) m C1), time ((Rep_run ρ) m C2))}›
    using forall_nat_set_suc[of ‹n› ‹λx y. R (time ((Rep_run x) y C1),
                                       time ((Rep_run x) y C2))›] 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. ticks ((Rep_run ρ) m master) ⟶ ticks ((Rep_run ρ) m slave)}
        = {ρ. ticks ((Rep_run ρ) n master) ⟶ ticks ((Rep_run ρ) n slave)}
        ∩ {ρ. ∀m≥Suc n. ticks ((Rep_run ρ) m master)
                     ⟶ ticks ((Rep_run ρ) m slave)}›
    using forall_nat_set_suc[of ‹n› ‹λx y. ticks ((Rep_run x) y master)
                                ⟶ ticks ((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. ticks ((Rep_run ρ) m master) ⟶ ¬ ticks ((Rep_run ρ) m slave)}
       = {ρ. ticks ((Rep_run ρ) n master) ⟶ ¬ ticks ((Rep_run ρ) n slave)}
          ∩ {ρ. ∀m≥Suc n. ticks ((Rep_run ρ) m master)
                     ⟶ ¬ ticks ((Rep_run ρ) m slave)}›
    using forall_nat_set_suc[of ‹n› ‹λx y. ticks ((Rep_run x) y master)
                               ⟶ ¬ticks ((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. ticks ((Rep_run ρ) m master) ⟶
                 (let measured_time = time ((Rep_run ρ) m measuring) in
                  ∀p ≥ m. first_time ρ measuring p (measured_time + δτ)
                           ⟶ ticks ((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 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 TESL_interp_stepwise_timedelayed_tvar_coind_unfold:
  ‹⟦ master time-delayed⨝ by δτ on measuring implies slave ⟧TESL≥ n =
     (     ⟦ master ¬⇑ n ⟧prim               ― ‹rule @{term timedelayed_tvar_e1}›
        ∪ (⟦ master ⇑ n ⟧prim ∩ ⟦ slave sporadic♯ ⦇τvar(measuring, n) ⊕ δτ⦈ on measuring ⟧TESL≥ n))
                                             ― ‹rule @{term timedelayed_tvar_e2}›
     ∩ ⟦ master time-delayed⨝ by δτ on measuring implies slave ⟧TESL≥ Suc n›
proof -
  have ‹{ ρ. ∀m≥n. ticks ((Rep_run ρ) m master) ⟶
               (let measured_time = time ((Rep_run ρ) m measuring) in
                ∃p ≥ m. ticks ((Rep_run ρ) p slave)
                      ∧ time ((Rep_run ρ) p measuring) = measured_time + δτ)}
       = { ρ. ticks ((Rep_run ρ) n master) ⟶
               (let measured_time = time ((Rep_run ρ) n measuring) in
                ∃p ≥ n. ticks ((Rep_run ρ) p slave)
                      ∧ time ((Rep_run ρ) p measuring) = measured_time + δτ)}
         ∩ { ρ. ∀m≥Suc n. ticks ((Rep_run ρ) m master) ⟶
               (let measured_time = time ((Rep_run ρ) m measuring) in
                ∃p ≥ m. ticks ((Rep_run ρ) p slave)
                      ∧ time ((Rep_run ρ) p measuring) = measured_time + δτ)}›
  using nat_set_suc[of ‹n› ‹λx y. ticks ((Rep_run x) y master) ⟶
               (let measured_time = time ((Rep_run x) y measuring) in
                ∃p ≥ y. ticks ((Rep_run x) p slave)
                      ∧ time ((Rep_run x) p measuring) = measured_time + δτ)›] by simp
  then show ?thesis by auto
qed

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

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

lemma TESL_interp_stepwise_kills_coind_unfold:
   ‹⟦ C1 kills C2 ⟧TESL≥ n =
      (   ⟦ C1 ¬⇑ n ⟧prim                        ― ‹rule @{term kills_e1}›
        ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 ¬⇑ ≥ n ⟧prim)    ― ‹rule @{term kills_e2}›
      ∩ ⟦ C1 kills C2 ⟧TESL≥ Suc n›
proof -
  let ?kills = ‹λn ρ. ∀p≥n. ticks ((Rep_run ρ) p C1)
                             ⟶ (∀m≥p. ¬ ticks ((Rep_run ρ) m C2))›
  let ?ticks = ‹λn ρ c. ticks ((Rep_run ρ) n c)›
  let ?dead = ‹λn ρ c. ∀m ≥ n. ¬ticks ((Rep_run ρ) m c)›
  have ‹⟦ C1 kills C2 ⟧TESL≥ n = {ρ. ?kills n ρ}› by simp
  also have ‹... = ({ρ. ¬ ?ticks n ρ C1}  ∩ {ρ. ?kills (Suc n) ρ})
                 ∪ ({ρ. ?ticks n ρ C1} ∩ {ρ. ?dead n ρ C2})›
  proof
    { fix ρ::‹'τ::linordered_field run›
      assume ‹ρ ∈ {ρ. ?kills n ρ}›
      hence ‹?kills n ρ› by simp
      hence ‹(?ticks n ρ C1 ∧ ?dead n ρ C2) ∨ (¬?ticks n ρ C1 ∧ ?kills (Suc n) ρ)›
        using Suc_leD by blast
      hence ‹ρ ∈ ({ρ. ?ticks n ρ C1} ∩ {ρ. ?dead n ρ C2})
               ∪ ({ρ. ¬ ?ticks n ρ C1} ∩ {ρ. ?kills (Suc n) ρ})›
        by blast
    } thus ‹{ρ. ?kills n ρ}
           ⊆ {ρ. ¬ ?ticks n ρ C1} ∩ {ρ. ?kills (Suc n) ρ} 
            ∪ {ρ. ?ticks n ρ C1} ∩ {ρ. ?dead n ρ C2}› by blast
  next
    { fix ρ::‹'τ::linordered_field run›
      assume ‹ρ ∈ ({ρ. ¬ ?ticks n ρ C1}  ∩ {ρ. ?kills (Suc n) ρ})
                 ∪ ({ρ. ?ticks n ρ C1} ∩ {ρ. ?dead n ρ C2})›
      hence ‹¬ ?ticks n ρ C1 ∧ ?kills (Suc n) ρ
             ∨ ?ticks n ρ C1 ∧ ?dead n ρ C2› by blast
      moreover have ‹((¬ ?ticks n ρ C1) ∧ (?kills (Suc n) ρ)) ⟶ ?kills n ρ›
        using dual_order.antisym not_less_eq_eq by blast
      ultimately have ‹?kills n ρ ∨ ?ticks n ρ C1 ∧ ?dead n ρ C2› by blast
      hence ‹?kills n ρ› using le_trans by blast
    } thus ‹({ρ. ¬ ?ticks n ρ C1}  ∩ {ρ. ?kills (Suc n) ρ})
                 ∪ ({ρ. ?ticks n ρ C1} ∩ {ρ. ?dead n ρ C2})
          ⊆ {ρ. ?kills n ρ}› by blast
  qed
  also have ‹... = {ρ. ¬ ?ticks n ρ C1} ∩ {ρ. ?kills (Suc n) ρ}
                 ∪ {ρ. ?ticks n ρ C1} ∩ {ρ. ?dead n ρ C2} ∩ {ρ. ?kills (Suc n) ρ}›
    using Collect_cong Collect_disj_eq by auto
  also have ‹... = ⟦ C1 ¬⇑ n ⟧prim ∩ ⟦ C1 kills C2 ⟧TESL≥ Suc n
                 ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 ¬⇑ ≥ n ⟧prim
                 ∩ ⟦ C1 kills C2 ⟧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›
proof (induction φ)
case (SporadicOn x1 x2 x3)
  then show ?case by simp
next
  case (SporadicOnTvar C1 τexpr C2)
  then show ?case 
  proof (induction τexpr)
    case (AddDelay τvar0 δτ)
    then show ?case
    proof (induction τvar0)
      case (TSchematic tuple)
      then show ?case
      proof (induction tuple)
        case (Pair Cpast npast)
        then show ?case by simp
      qed
    qed
  qed
next
case (TagRelation x1 x2 x3)
  then show ?case by simp 
next
  case (Implies x1 x2)
then show ?case by simp 
next
  case (ImpliesNot x1 x2)
  then show ?case by simp
next
  case (TimeDelayedBy x1 x2 x3 x4)
then show ?case by simp
next
  case (RelaxedTimeDelayed x1 x2 x3 x4)
  then show ?case by simp
next
  case (WeaklyPrecedes x1 x2)
  then show ?case by simp
next
  case (StrictlyPrecedes x1 x2)
  then show ?case by simp
next
  case (Kills x1 x2)
then show ?case by simp
qed

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 configuration_interpretation
  ::‹'τ::linordered_field config ⇒ 'τ run set›          (‹⟦ _ ⟧config› 71)
where
  ‹⟦ Γ, n ⊨ Ψ ▹ Φ ⟧config = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›

lemma configuration_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 configuration_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 configuration_interp_stepwise_sporadicon_cases:
   ‹⟦ Γ, n ⊨ ((C1 sporadic τ on C2) # Ψ) ▹ Φ ⟧config
    = ⟦ Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ) ⟧config
    ∪ ⟦ ((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ ⟧config›
proof -
  have ‹⟦ Γ, n ⊨ (C1 sporadic τ on C2) # Ψ ▹ Φ ⟧config
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (C1 sporadic τ on C2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ) ⟧config
                 =  ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (C1 sporadic τ on C2) # Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ ((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ ⟧config
                 =  ⟦⟦ ((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ) ⟧⟧prim
                  ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
    by simp
  ultimately show ?thesis
  proof -
    have ‹(⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 ⇓ n @ τ ⟧prim ∪ ⟦ C1 sporadic τ on C2 ⟧TESL≥ Suc n)
            ∩ (⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n)
          = ⟦ C1 sporadic τ on C2 ⟧TESL≥ n ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Γ ⟧⟧prim)›
      using TESL_interp_stepwise_sporadicon_coind_unfold by blast
    hence ‹⟦⟦ ((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ) ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
            ∪ ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦ C1 sporadic τ on C2 ⟧TESL≥ Suc n
           = ⟦⟦ (C1 sporadic τ on C2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Γ ⟧⟧prim› by auto
    thus ?thesis by auto
  qed
qed

lemma configuration_interp_stepwise_sporadicon_tvar_cases:
   ‹⟦ Γ, n ⊨ ((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ ⟧config
    = ⟦ Γ, n ⊨ Ψ ▹ ((C1 sporadic♯ τexpr on C2) # Φ) ⟧config
    ∪ ⟦ ((C1 ⇑ n) # (C2 ⇓ n @♯ τexpr) # Γ), n ⊨ Ψ ▹ Φ ⟧config›
proof -
  from tag_expr.exhaust obtain v δτ where ‹ τexpr=⦇ v ⊕ δτ ⦈› by blast
  moreover from tag_var.exhaust obtain Cpast npast where ‹v=τvar(Cpast, npast)› by auto
  ultimately have *:‹τexpr=⦇ τvar(Cpast, npast) ⊕ δτ ⦈› by simp
  show ?thesis
  proof -
    have ‹(⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 ⇓ n @♯ ⦇ τvar (Cpast, npast) ⊕ δτ ⦈ ⟧prim
         ∪ ⟦ C1 sporadic♯ ⦇ τvar (Cpast, npast) ⊕ δτ ⦈ on C2 ⟧TESL≥ Suc n)
        ∩ (⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n)
      = ⟦ C1 sporadic♯ ⦇ τvar (Cpast, npast) ⊕ δτ ⦈ on C2 ⟧TESL≥ n ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Γ ⟧⟧prim)›
      using TESL_interp_stepwise_sporadicon_tvar_coind_unfold[of ‹C1› ‹Cpast› ‹npast› ‹δτ› ‹C2› ‹n›]
            Int_commute by blast
    then have ‹⟦⟦ (C1 ⇑ n) # (C2 ⇓ n @♯ ⦇ τvar (Cpast, npast) ⊕ δτ ⦈) # Γ ⟧⟧prim
            ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n ∪ ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
            ∩ ⟦ C1 sporadic♯ ⦇ τvar (Cpast, npast) ⊕ δτ ⦈ on C2 ⟧TESL≥ Suc n
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (C1 sporadic♯ ⦇ τvar (Cpast, npast) ⊕ δτ ⦈ on C2) # Ψ ⟧⟧TESL≥ n›
      by auto
    then have ‹⟦ Γ, n ⊨ ((C1 sporadic♯ ⦇ τvar (Cpast, npast) ⊕ δτ ⦈ on C2) # Ψ) ▹ Φ ⟧config
        = ⟦ ((C1 ⇑ n) # (C2 ⇓ n @♯ ⦇ τvar (Cpast, npast) ⊕ δτ ⦈) # Γ), n ⊨ Ψ ▹ Φ ⟧config
          ∪ ⟦ Γ, n ⊨ Ψ ▹ ((C1 sporadic♯ ⦇ τvar (Cpast, npast) ⊕ δτ ⦈ on C2) # Φ) ⟧config›
      by auto
    then show ?thesis using *
      by blast
  qed
qed

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

lemma configuration_interp_stepwise_implies_cases:
   ‹⟦ Γ, n ⊨ ((C1 implies C2) # Ψ) ▹ Φ ⟧config
      = ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ) ⟧config
      ∪ ⟦ ((C1 ⇑ n) # (C2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ) ⟧config›
proof -
  have ‹⟦ Γ, n ⊨ (C1 implies C2) # Ψ ▹ Φ ⟧config
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (C1 implies C2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ) ⟧config
                = ⟦⟦ (C1 ¬⇑ n) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                ∩ ⟦⟦ (C1 implies C2) # Φ ⟧⟧TESL≥ Suc n› by simp
  moreover have ‹⟦ ((C1 ⇑ n) # (C2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ) ⟧config
                =  ⟦⟦ ((C1 ⇑ n) # (C2 ⇑ n) # Γ) ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                 ∩ ⟦⟦ (C1 implies C2) # Φ ⟧⟧TESL≥ Suc n› by simp
  ultimately show ?thesis
  proof -
    have f1: ‹(⟦ C1 ¬⇑ n ⟧prim ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 ⇑ n ⟧prim)
                ∩ ⟦ C1 implies C2 ⟧TESL≥ Suc n ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n
                ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n)
              = ⟦⟦ (C1 implies C2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
      using TESL_interp_stepwise_implies_coind_unfold
            TESL_interpretation_stepwise_cons_morph by blast
    have ‹⟦ C1 ¬⇑ n ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦⟦ (C2 ⇑ n) # Γ ⟧⟧prim
         = (⟦ C1 ¬⇑ n ⟧prim ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 ⇑ n ⟧prim) ∩ ⟦⟦ Γ ⟧⟧prim›
      by force
    hence ‹⟦ Γ, n ⊨ ((C1 implies C2) # Ψ) ▹ Φ ⟧config
      = (⟦ C1 ¬⇑ n ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦⟦ (C2 ⇑ n) # Γ ⟧⟧prim)
        ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ (C1 implies C2) # Φ ⟧⟧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 configuration_interp_stepwise_implies_not_cases:
   ‹⟦ Γ, n ⊨ ((C1 implies not C2) # Ψ) ▹ Φ ⟧config
      = ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ) ⟧config
      ∪ ⟦ ((C1 ⇑ n) # (C2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ) ⟧config›
proof -
  have ‹⟦ Γ, n ⊨ (C1 implies not C2) # Ψ ▹ Φ ⟧config
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (C1 implies not C2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ) ⟧config
                  = ⟦⟦ (C1 ¬⇑ n) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (C1 implies not C2) # Φ ⟧⟧TESL≥ Suc n› by simp
  moreover have ‹⟦ ((C1 ⇑ n) # (C2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ) ⟧config
                  = ⟦⟦ ((C1 ⇑ n) # (C2 ¬⇑ n) # Γ) ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (C1 implies not C2) # Φ ⟧⟧TESL≥ Suc n› by simp
  ultimately show ?thesis
  proof -
    have f1: ‹(⟦ C1 ¬⇑ n ⟧prim ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 ¬⇑ n ⟧prim)
              ∩ ⟦ C1 implies not C2 ⟧TESL≥ Suc n
              ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n)
              = ⟦⟦ (C1 implies not C2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
      using TESL_interp_stepwise_implies_not_coind_unfold
            TESL_interpretation_stepwise_cons_morph by blast
    have ‹⟦ C1 ¬⇑ n ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦⟦ (C2 ¬⇑ n) # Γ ⟧⟧prim
           = (⟦ C1 ¬⇑ n ⟧prim ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 ¬⇑ n ⟧prim) ∩ ⟦⟦ Γ ⟧⟧prim›
      by force
    then have ‹⟦ Γ, n ⊨ ((C1 implies not C2) # Ψ) ▹ Φ ⟧config
                 = (⟦ C1 ¬⇑ n ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim ∪ ⟦ C1 ⇑ n ⟧prim
                    ∩ ⟦⟦ (C2 ¬⇑ n) # Γ ⟧⟧prim) ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n
                    ∩ ⟦⟦ (C1 implies not C2) # Φ ⟧⟧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 configuration_interp_stepwise_timedelayed_cases:
  ‹⟦ Γ, n ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ ⟧config
    = ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ) ⟧config
    ∪ ⟦ ((C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ), n
        ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ) ⟧config›
proof -
  have 1:‹⟦ Γ, n ⊨ (C1 time-delayed by δτ on C2 implies C3) # Ψ ▹ Φ ⟧config
         = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (C1 time-delayed by δτ on C2 implies C3) # Ψ ⟧⟧TESL≥ n
          ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n› by simp
  moreover have ‹⟦ ((C1 ¬⇑ n) # Γ), n
                  ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ) ⟧config
                 = ⟦⟦ (C1 ¬⇑ n) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (C1 time-delayed by δτ on C2 implies C3) # Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ ((C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ), n
                  ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ) ⟧config
                 = ⟦⟦ (C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (C1 time-delayed by δτ on C2 implies C3) # Φ ⟧⟧TESL≥ Suc n›
    by simp
  ultimately show ?thesis
  proof -
    have ‹⟦ Γ, n ⊨ (C1 time-delayed by δτ on C2 implies C3) # Ψ ▹ Φ ⟧config
      = ⟦⟦ Γ ⟧⟧prim ∩ (⟦⟦ (C1 time-delayed by δτ on C2 implies C3) # Ψ ⟧⟧TESL≥ n
        ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n)›
      using 1 by blast
    hence ‹⟦ Γ, n ⊨ (C1 time-delayed by δτ on C2 implies C3) # Ψ ▹ Φ ⟧config
          = (⟦ C1 ¬⇑ n ⟧prim ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 @ n ⊕ δτ ⇒ C3 ⟧prim)
            ∩ (⟦⟦ Γ ⟧⟧prim ∩ (⟦⟦ Ψ ⟧⟧TESL≥ n
            ∩ ⟦⟦ (C1 time-delayed by δτ on C2 implies C3) # Φ ⟧⟧TESL≥ Suc n))›
      using TESL_interpretation_stepwise_cons_morph
            TESL_interp_stepwise_timedelayed_coind_unfold
    proof -
      have ‹⟦⟦ (C1 time-delayed by δτ on C2 implies C3) # Ψ ⟧⟧TESL≥ n
            = (⟦ C1 ¬⇑ n ⟧prim ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C2 @ n ⊕ δτ ⇒ C3 ⟧prim)
            ∩ ⟦ C1 time-delayed by δτ on C2 implies C3 ⟧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 configuration_interp_stepwise_timedelayed_tvar_cases:
  ‹⟦ Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ ⟧config
    = ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config
    ∪ ⟦ ((C1 ⇑ n) # Γ), n
        ⊨ (C3 sporadic♯ ⦇τvar(C2, n) ⊕ δτ⦈ on C2) # Ψ
        ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) ⟧config›
proof -
  have ‹⟦⟦ Ψ ⟧⟧TESL≥ n
       ∩ (⟦ C1 ¬⇑ n ⟧prim ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C3 sporadic♯ ⦇ τvar (C2, n) ⊕ δτ ⦈ on C2 ⟧TESL≥ n)
       ∩ ⟦ C1 time-delayed⨝ by δτ on C2 implies C3 ⟧TESL≥ Suc n
      = ⟦⟦ Ψ ⟧⟧TESL≥ n ∩ ⟦ C1 time-delayed⨝ by δτ on C2 implies C3 ⟧TESL≥ n›
    using TESL_interp_stepwise_timedelayed_tvar_coind_unfold[of ‹C1› ‹δτ› ‹C2› ‹C3› ‹n›]
          Int_assoc by blast
  then have ‹⟦ Γ, n ⊨ (C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ ▹ Φ ⟧config
          = ⟦⟦ Ψ ⟧⟧TESL≥ n
          ∩ (⟦ C1 ¬⇑ n ⟧prim ∪ ⟦ C1 ⇑ n ⟧prim ∩ ⟦ C3 sporadic♯ ⦇ τvar (C2, n) ⊕ δτ ⦈ on C2 ⟧TESL≥ n)
          ∩ ⟦ C1 time-delayed⨝ by δτ on C2 implies C3 ⟧TESL≥ Suc n
          ∩ (⟦⟦ Φ ⟧⟧TESL≥ Suc n ∩ ⟦⟦ Γ ⟧⟧prim)›
    by force
  then show ?thesis
    by auto
qed

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

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

lemma configuration_interp_stepwise_kills_cases:
   ‹⟦ Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ ⟧config
    = ⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ) ⟧config
    ∪ ⟦ ((C1 ⇑ n) # (C2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ) ⟧config›
proof -
  have ‹⟦ Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ ⟧config
        = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ (C1 kills C2) # Ψ ⟧⟧TESL≥ n ∩ ⟦⟦ Φ ⟧⟧TESL≥ Suc n›
    by simp
  moreover have ‹⟦ ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ) ⟧config
                = ⟦⟦ (C1 ¬⇑ n) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (C1 kills C2) # Φ ⟧⟧TESL≥ Suc n› by simp
  moreover have ‹⟦ ((C1 ⇑ n) # (C2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ) ⟧config
                = ⟦⟦ (C1 ⇑ n) # (C2 ¬⇑ ≥ n) # Γ ⟧⟧prim ∩ ⟦⟦ Ψ ⟧⟧TESL≥ n
                  ∩ ⟦⟦ (C1 kills C2) # Φ ⟧⟧TESL≥ Suc n› by simp
  ultimately show ?thesis
    proof -
      have ‹⟦⟦ (C1 kills C2) # Ψ ⟧⟧TESL≥ n
            = (⟦ (C1 ¬⇑ n) ⟧prim ∪ ⟦ (C1 ⇑ n) ⟧prim ∩ ⟦ (C2 ¬⇑ ≥ n) ⟧prim)
              ∩ ⟦ (C1 kills C2) ⟧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