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