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 K2TESL⇗≥ i=
      {ρ. ni. hamlet ((Rep_run ρ) n K1)  time ((Rep_run ρ) n K2) = τ}
|  time-relation K1, K2  RTESL⇗≥ i=
      {ρ. ni. R (time ((Rep_run ρ) n K1), time ((Rep_run ρ) n K2))}
|  master implies slaveTESL⇗≥ i=
      {ρ. ni. hamlet ((Rep_run ρ) n master)  hamlet ((Rep_run ρ) n slave)}
|  master implies not slaveTESL⇗≥ i=
      {ρ. ni. hamlet ((Rep_run ρ) n master)  ¬ hamlet ((Rep_run ρ) n slave)}
|  master time-delayed by δτ on measuring implies slaveTESL⇗≥ i=
      {ρ. ni. 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 K2TESL⇗≥ i=
      {ρ. ni. (run_tick_count ρ K2 n)  (run_tick_count ρ K1 n)}
|  K1 strictly precedes K2TESL⇗≥ i=
      {ρ. ni. (run_tick_count ρ K2 n)  (run_tick_count_strictly ρ K1 n)}
|  K1 kills K2TESL⇗≥ i=
      {ρ. ni. hamlet ((Rep_run ρ) n K1)  (mn. ¬ 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 K2TESL⇗≥ n}
by auto

lemma TESL_interp_unfold_stepwise_tagrelgen:
   time-relation K1, K2  R TESL
    =  {Y. n::nat. Y =  time-relation K1, K2  RTESL⇗≥ n}
by auto

lemma TESL_interp_unfold_stepwise_implies:
   master implies slave TESL
    =  {Y. n::nat. Y =  master implies slaveTESL⇗≥ n}
by auto

lemma TESL_interp_unfold_stepwise_implies_not:
   master implies not slave TESL
    =  {Y. n::nat. Y =  master implies not slaveTESL⇗≥ 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 slaveTESL⇗≥ n}
by auto

lemma TESL_interp_unfold_stepwise_weakly_precedes:
   K1 weakly precedes K2 TESL
    =  {Y. n::nat. Y =  K1 weakly precedes K2TESL⇗≥ n}
by auto

lemma TESL_interp_unfold_stepwise_strictly_precedes:
   K1 strictly precedes K2 TESL
    =  {Y. n::nat. Y =  K1 strictly precedes K2TESL⇗≥ n}
by auto

lemma TESL_interp_unfold_stepwise_kills:
   master kills slave TESL =  {Y. n::nat. Y =  master kills slaveTESL⇗≥ 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 K2TESL⇗≥ n=
     K1  n prim   K2  n @ τ prim        ― ‹rule @{term sporadic_on_e2}
      K1 sporadic τ on K2TESL⇗≥ 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  RTESL⇗≥ n=        ― ‹rule @{term tagrel_e}
      τvar(K1, n), τvar(K2, n)  R prim
       time-relation K1, K2  RTESL⇗≥ Suc n⇖›
proof -
  have {ρ. mn. R (time ((Rep_run ρ) m K1), time ((Rep_run ρ) m K2))}
       = {ρ. R (time ((Rep_run ρ) n K1), time ((Rep_run ρ) n K2))}
        {ρ. mSuc 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 slaveTESL⇗≥ n=
     (    master ¬⇑ n prim                     ― ‹rule @{term implies_e1}
         master  n prim   slave  n prim)  ― ‹rule @{term implies_e2}
       master implies slaveTESL⇗≥ Suc n⇖›
proof -
  have {ρ. mn. hamlet ((Rep_run ρ) m master)  hamlet ((Rep_run ρ) m slave)}
        = {ρ. hamlet ((Rep_run ρ) n master)  hamlet ((Rep_run ρ) n slave)}
         {ρ. mSuc 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 slaveTESL⇗≥ n=
     (     master ¬⇑ n prim                       ― ‹rule @{term implies_not_e1}
          master  n prim   slave ¬⇑ n prim)  ― ‹rule @{term implies_not_e2}
       master implies not slaveTESL⇗≥ Suc n⇖›
proof -
  have {ρ. mn. hamlet ((Rep_run ρ) m master)  ¬ hamlet ((Rep_run ρ) m slave)}
       = {ρ. hamlet ((Rep_run ρ) n master)  ¬ hamlet ((Rep_run ρ) n slave)}
           {ρ. mSuc 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 slaveTESL⇗≥ 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 slaveTESL⇗≥ 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 slaveTESL⇗≥ Suc n⇖›
    by simp
  finally show ?thesis by auto
qed

lemma TESL_interp_stepwise_weakly_precedes_coind_unfold:
    K1 weakly precedes K2TESL⇗≥ n=                 ― ‹rule @{term weakly_precedes_e}
       (# K2 n, # K1 n  (λ(x,y). xy)) prim 
        K1 weakly precedes K2TESL⇗≥ Suc n⇖›
proof -
  have {ρ. pn. (run_tick_count ρ K2 p)  (run_tick_count ρ K1 p)}
         = {ρ. (run_tick_count ρ K2 n)  (run_tick_count ρ K1 n)}
          {ρ. pSuc 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 K2TESL⇗≥ n=               ― ‹rule @{term strictly_precedes_e}
       (# K2 n, #< K1 n  (λ(x,y). xy)) prim
        K1 strictly precedes K2TESL⇗≥ Suc n⇖›
proof -
  have {ρ. pn. (run_tick_count ρ K2 p)  (run_tick_count_strictly ρ K1 p)}
         = {ρ. (run_tick_count ρ K2 n)  (run_tick_count_strictly ρ K1 n)}
          {ρ. pSuc 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 K2TESL⇗≥ n=
      (    K1 ¬⇑ n prim                        ― ‹rule @{term kills_e1}
          K1  n prim   K2 ¬⇑  n prim)    ― ‹rule @{term kills_e2}
        K1 kills K2TESL⇗≥ Suc n⇖›
proof -
  let ?kills = λn ρ. pn. hamlet ((Rep_run ρ) p K1)
                              (mp. ¬ 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 K2TESL⇗≥ 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 K2TESL⇗≥ Suc n  K1  n prim   K2 ¬⇑  n prim
                   K1 kills K2TESL⇗≥ 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 K2TESL⇗≥ Suc n)
             (⟦⟦ Γ ⟧⟧prim  ⟦⟦ Ψ ⟧⟧TESL⇗≥ n)
          =  K1 sporadic τ on K2TESL⇗≥ 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 K2TESL⇗≥ 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  RTESL⇗≥ 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 K2TESL⇗≥ 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 K2TESL⇗≥ 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 K3TESL⇗≥ 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). xy)) # Γ), 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). xy)) # Γ), n
                   Ψ  ((K1 weakly precedes K2) # Φ) config
                = ⟦⟦ (# K2 n, # K1 n  (λ(x,y). xy)) # Γ ⟧⟧prim
                 ⟦⟦ Ψ ⟧⟧TESL⇗≥ n ⟦⟦ (K1 weakly precedes K2) # Φ ⟧⟧TESL⇗≥ Suc n⇖›
    by simp
  ultimately show ?thesis
  proof -
    have  # K2 n, # K1 n  (λ(x,y). xy) prim
              K1 weakly precedes K2TESL⇗≥ 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). xy)) # Γ), 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). xy)) # Γ), n
                   Ψ  ((K1 strictly precedes K2) # Φ) config
                = ⟦⟦ (# K2 n, #< K1 n  (λ(x,y). xy)) # Γ ⟧⟧prim
                 ⟦⟦ Ψ ⟧⟧TESL⇗≥ n ⟦⟦ (K1 strictly precedes K2) # Φ ⟧⟧TESL⇗≥ Suc n⇖› by simp
  ultimately show ?thesis
  proof -
    have  # K2 n, #< K1 n  (λ(x,y). xy) prim
              K1 strictly precedes K2TESL⇗≥ 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