Theory Stuttering

subsection‹Main Theorems›

theory Stuttering
imports StutteringLemmas

begin

text ‹
  Using the lemmas of the previous section about the invariance by stuttering
  of various properties of TESL specifications, we can now prove that the atomic 
  formulae that compose TESL specifications are invariant by stuttering.
›

text ‹Sporadic specifications are preserved in a dilated run.›
lemma sporadic_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦c sporadic τ on c'⟧⇩T⇩E⇩S⇩L›
    shows ‹r ∈ ⟦c sporadic τ on c'⟧⇩T⇩E⇩S⇩L›
proof -
  from assms(1) is_subrun_def obtain f
    where ‹dilating f sub r› by blast
  hence ‹∀n c. time ((Rep_run sub) n c) = time ((Rep_run r) (f n) c)
           ∧ hamlet ((Rep_run sub) n c) = hamlet ((Rep_run r) (f n) c)› by (simp add: dilating_def)
  moreover from assms(2) have
    ‹sub ∈ {r. ∃ n. hamlet ((Rep_run r) n c) ∧ time ((Rep_run r) n c') = τ}› by simp
  from this obtain k where ‹time ((Rep_run sub) k c') = τ ∧ hamlet ((Rep_run sub) k c)› by auto
  ultimately have ‹time ((Rep_run r) (f k) c') = τ ∧ hamlet ((Rep_run r) (f k) c)› by simp
  thus ?thesis by auto
qed

text ‹Implications are preserved in a dilated run.›
theorem implies_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦c⇩1 implies c⇩2⟧⇩T⇩E⇩S⇩L›
    shows ‹r ∈ ⟦c⇩1 implies c⇩2⟧⇩T⇩E⇩S⇩L›
proof -
  from assms(1) is_subrun_def obtain f where ‹dilating f sub r› by blast
  moreover from assms(2) have
    ‹sub ∈ {r. ∀n. hamlet ((Rep_run r) n c⇩1) ⟶ hamlet ((Rep_run r) n c⇩2)}› by simp
  hence ‹∀n. hamlet ((Rep_run sub) n c⇩1) ⟶ hamlet ((Rep_run sub) n c⇩2)› by simp
  ultimately have ‹∀n. hamlet ((Rep_run r) n c⇩1) ⟶ hamlet ((Rep_run r) n c⇩2)›
    using ticks_imp_ticks_subk ticks_sub by blast
  thus ?thesis by simp
qed

theorem implies_not_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦c⇩1 implies not c⇩2⟧⇩T⇩E⇩S⇩L›
    shows ‹r ∈ ⟦c⇩1 implies not c⇩2⟧⇩T⇩E⇩S⇩L›
proof -
  from assms(1) is_subrun_def obtain f where ‹dilating f sub r› by blast
  moreover from assms(2) have
    ‹sub ∈ {r. ∀n. hamlet ((Rep_run r) n c⇩1) ⟶ ¬ hamlet ((Rep_run r) n c⇩2)}› by simp
  hence ‹∀n. hamlet ((Rep_run sub) n c⇩1) ⟶ ¬ hamlet ((Rep_run sub) n c⇩2)› by simp
  ultimately have ‹∀n. hamlet ((Rep_run r) n c⇩1) ⟶ ¬ hamlet ((Rep_run r) n c⇩2)›
    using ticks_imp_ticks_subk ticks_sub by blast
  thus ?thesis by simp
qed

text ‹Precedence relations are preserved in a dilated run.›
theorem weakly_precedes_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦c⇩1 weakly precedes c⇩2⟧⇩T⇩E⇩S⇩L›
    shows ‹r ∈ ⟦c⇩1 weakly precedes c⇩2⟧⇩T⇩E⇩S⇩L›
proof -
  from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast
  from assms(2) have
    ‹sub ∈ {r. ∀n. (run_tick_count r c⇩2 n) ≤ (run_tick_count r c⇩1 n)}› by simp
  hence ‹∀n. (run_tick_count sub c⇩2 n) ≤ (run_tick_count sub c⇩1 n)› by simp
  from dil_tick_count[OF assms(1) this]
    have ‹∀n. (run_tick_count r c⇩2 n) ≤ (run_tick_count r c⇩1 n)› by simp
  thus ?thesis by simp
qed

theorem strictly_precedes_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦c⇩1 strictly precedes c⇩2⟧⇩T⇩E⇩S⇩L›
    shows ‹r ∈ ⟦c⇩1 strictly precedes c⇩2⟧⇩T⇩E⇩S⇩L›
proof -
  from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast
  from assms(2) have
    ‹sub ∈ { ρ. ∀n::nat. (run_tick_count ρ c⇩2 n) ≤ (run_tick_count_strictly ρ c⇩1 n) }›
  by simp
  with strictly_precedes_alt_def2[of ‹c⇩2› ‹c⇩1›]  have
    ‹sub ∈ { ρ. (¬hamlet ((Rep_run ρ) 0 c⇩2))
  ∧ (∀n::nat. (run_tick_count ρ c⇩2 (Suc n)) ≤ (run_tick_count ρ c⇩1 n)) }›
  by blast
  hence ‹(¬hamlet ((Rep_run sub) 0 c⇩2))
       ∧ (∀n::nat. (run_tick_count sub c⇩2 (Suc n)) ≤ (run_tick_count sub c⇩1 n))›
    by simp
  hence
    1:‹(¬hamlet ((Rep_run sub) 0 c⇩2))
     ∧ (∀n::nat. (tick_count sub c⇩2 (Suc n)) ≤ (tick_count sub c⇩1 n))›
  by (simp add: tick_count_is_fun)
  have ‹∀n::nat. (tick_count r c⇩2 (Suc n)) ≤ (tick_count r c⇩1 n)›
  proof -
    { fix n::nat
      have ‹tick_count r c⇩2 (Suc n) ≤ tick_count r c⇩1 n›
      proof (cases ‹∃n⇩0. f n⇩0 = n›)
        case True ― ‹n is in the image of f›
          from this obtain n⇩0 where fn:‹f n⇩0 = n› by blast
          show ?thesis
          proof (cases ‹∃sn⇩0. f sn⇩0 = Suc n›)
            case True ― ‹Suc n is in the image of f›
              from this obtain sn⇩0 where fsn:‹f sn⇩0 = Suc n› by blast
              with fn strict_mono_suc * have ‹sn⇩0 = Suc n⇩0›
                using  dilating_def dilating_fun_def by blast
              with 1 have ‹tick_count sub c⇩2 sn⇩0 ≤ tick_count sub c⇩1 n⇩0› by simp
              thus ?thesis using fn fsn tick_count_sub[OF *] by simp
          next
            case False ― ‹Suc n is not in the image of f›
              hence ‹¬hamlet ((Rep_run r) (Suc n) c⇩2)›
                using * by (simp add: dilating_def dilating_fun_def)
              hence ‹tick_count r c⇩2 (Suc n) = tick_count r c⇩2 n›
                by (simp add: tick_count_suc)
              also have ‹... = tick_count sub c⇩2 n⇩0›
                using fn tick_count_sub[OF *] by simp
              finally have ‹tick_count r c⇩2 (Suc n) = tick_count sub c⇩2 n⇩0› .
              moreover have ‹tick_count sub c⇩2 n⇩0 ≤ tick_count sub c⇩2 (Suc n⇩0)›
                by (simp add: tick_count_suc)
              ultimately have
                ‹tick_count r c⇩2 (Suc n) ≤ tick_count sub c⇩2 (Suc n⇩0)› by simp
              moreover have
                ‹tick_count sub c⇩2 (Suc n⇩0) ≤ tick_count sub c⇩1 n⇩0› using 1 by simp
              ultimately have ‹tick_count r c⇩2 (Suc n) ≤ tick_count sub c⇩1 n⇩0› by simp
              thus ?thesis using tick_count_sub[OF *] fn by simp
          qed
      next
        case False ― ‹n is not in the image of f›
          from greatest_prev_image[OF * this] obtain n⇩p  where
            np_prop:‹f n⇩p < n ∧ (∀k. f n⇩p < k ∧ k ≤ n ⟶ (∄k⇩0. f k⇩0 = k))› by blast
          from tick_count_latest[OF * this] have
            ‹tick_count r c⇩1 n = tick_count r c⇩1 (f n⇩p)› . 
          hence a:‹tick_count r c⇩1 n = tick_count sub c⇩1 n⇩p›
            using tick_count_sub[OF *] by simp
          have b: ‹tick_count sub c⇩2 (Suc n⇩p) ≤ tick_count sub c⇩1 n⇩p› using 1 by simp
          show ?thesis
          proof (cases ‹∃sn⇩0. f sn⇩0 = Suc n›)
            case True ― ‹Suc n is in the image of f›
              from this obtain sn⇩0 where fsn:‹f sn⇩0 = Suc n› by blast
              from next_non_stuttering[OF * np_prop this]  have sn_prop:‹sn⇩0 = Suc n⇩p› .
              with b have ‹tick_count sub c⇩2 sn⇩0 ≤ tick_count sub c⇩1 n⇩p› by simp
              thus ?thesis using tick_count_sub[OF *] fsn a by auto
          next
            case False ― ‹Suc n is not in the image of f›
              hence ‹¬hamlet ((Rep_run r) (Suc n) c⇩2)›
                using * by (simp add: dilating_def dilating_fun_def)
              hence ‹tick_count r c⇩2 (Suc n) = tick_count r c⇩2 n›
                by (simp add: tick_count_suc)
              also have ‹... = tick_count sub c⇩2 n⇩p› using np_prop tick_count_sub[OF *]
                by (simp add: tick_count_latest[OF * np_prop])
              finally have ‹tick_count r c⇩2 (Suc n) = tick_count sub c⇩2 n⇩p› .
              moreover have ‹tick_count sub c⇩2 n⇩p ≤ tick_count sub c⇩2 (Suc n⇩p)›
                by (simp add: tick_count_suc)
              ultimately have
                ‹tick_count r c⇩2 (Suc n) ≤ tick_count sub c⇩2 (Suc n⇩p)› by simp
              moreover have
                ‹tick_count sub c⇩2 (Suc n⇩p) ≤ tick_count sub c⇩1 n⇩p› using 1 by simp
              ultimately have ‹tick_count r c⇩2 (Suc n) ≤ tick_count sub c⇩1 n⇩p› by simp
              thus ?thesis using np_prop mono_tick_count  using a by linarith
          qed
      qed
    } thus ?thesis ..
  qed
  moreover from 1 have ‹¬hamlet ((Rep_run r) 0 c⇩2)›
    using * empty_dilated_prefix ticks_sub by fastforce
  ultimately show ?thesis by (simp add: tick_count_is_fun strictly_precedes_alt_def2) 
qed

text ‹
  Time delayed relations are preserved in a dilated run.
›
theorem time_delayed_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦ a time-delayed by δτ on ms implies b ⟧⇩T⇩E⇩S⇩L›
    shows ‹r ∈ ⟦ a time-delayed by δτ on ms implies b ⟧⇩T⇩E⇩S⇩L›
proof -
  from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast
  from assms(2) have ‹∀n. hamlet ((Rep_run sub) n a)
                          ⟶ (∀m ≥ n. first_time sub ms m (time ((Rep_run sub) n ms) + δτ)
                                       ⟶ hamlet ((Rep_run sub) m b))›
    using TESL_interpretation_atomic.simps(5)[of ‹a› ‹δτ› ‹ms› ‹b›] by simp
  hence **:‹∀n⇩0. hamlet ((Rep_run r) (f n⇩0) a)
                  ⟶ (∀m⇩0 ≥ n⇩0. first_time r ms (f m⇩0) (time ((Rep_run r) (f n⇩0) ms) + δτ)
                                  ⟶ hamlet ((Rep_run r) (f m⇩0) b))  ›
    using first_time_image[OF *] dilating_def * by fastforce
  hence ‹∀n. hamlet ((Rep_run r) n a)
                  ⟶ (∀m ≥ n. first_time r ms m (time ((Rep_run r) n ms) + δτ)
                                ⟶ hamlet ((Rep_run r) m b))›
  proof -
    { fix n assume assm:‹hamlet ((Rep_run r) n a)›
      from ticks_image_sub[OF * assm] obtain n⇩0 where nfn0:‹n = f n⇩0› by blast
      with ** assm have ft0:
        ‹(∀m⇩0 ≥ n⇩0. first_time r ms (f m⇩0) (time ((Rep_run r) (f n⇩0) ms) + δτ)
                    ⟶ hamlet ((Rep_run r) (f m⇩0) b))› by blast
      have ‹(∀m ≥ n. first_time r ms m (time ((Rep_run r) n ms) + δτ) 
                       ⟶ hamlet ((Rep_run r) m b)) ›
      proof -
      { fix m assume hyp:‹m ≥ n›
        have ‹first_time r ms m (time (Rep_run r n ms) + δτ) ⟶ hamlet (Rep_run r m b)›
        proof (cases ‹∃m⇩0. f m⇩0 = m›)
          case True
          from this obtain m⇩0 where ‹m = f m⇩0› by blast
          moreover have ‹strict_mono f› using * by (simp add: dilating_def dilating_fun_def)
          ultimately show ?thesis using ft0 hyp nfn0 by (simp add: strict_mono_less_eq)
        next
          case False thus ?thesis
          proof (cases ‹m = 0›)
            case True
              hence ‹m = f 0› using * by (simp add: dilating_def dilating_fun_def)
              then show ?thesis using False by blast
          next
            case False
            hence ‹∃pm. m = Suc pm› by (simp add: not0_implies_Suc)
            from this obtain pm where mpm:‹m = Suc pm› by blast
            hence ‹∄pm⇩0. f pm⇩0 = Suc pm› using ‹∄m⇩0. f m⇩0 = m› by simp 
            with *  have ‹time (Rep_run r (Suc pm) ms) = time (Rep_run r pm ms)›
              using dilating_def dilating_fun_def by blast
            hence ‹time (Rep_run r pm ms) = time (Rep_run r m ms)› using mpm by simp
            moreover from mpm have ‹pm < m› by simp
            ultimately have ‹∃m' < m. time (Rep_run r m' ms) = time (Rep_run r m ms)› by blast
            hence ‹¬(first_time r ms m (time (Rep_run r n ms) + δτ))›
              by (auto simp add: first_time_def)
            thus ?thesis by simp
          qed
        qed
      } thus ?thesis by simp
      qed
    } thus ?thesis by simp
  qed
  thus ?thesis by simp
qed

text ‹Time relations are preserved through dilation of a run.›
lemma tagrel_sub':
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦ time-relation ⌊c⇩1,c⇩2⌋ ∈ R ⟧⇩T⇩E⇩S⇩L›
    shows ‹R (time ((Rep_run r) n c⇩1), time ((Rep_run r) n c⇩2))›
proof -
  from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast
  moreover from assms(2) TESL_interpretation_atomic.simps(2) have
    ‹sub ∈ {r. ∀n. R (time ((Rep_run r) n c⇩1), time ((Rep_run r) n c⇩2))}› by blast
  hence 1:‹∀n. R (time ((Rep_run sub) n c⇩1), time ((Rep_run sub) n c⇩2))› by simp
  show ?thesis
  proof (induction n)
    case 0
      from 1 have ‹R (time ((Rep_run sub) 0 c⇩1), time ((Rep_run sub) 0 c⇩2))› by simp
      moreover from * have ‹f 0 = 0› by (simp add: dilating_def dilating_fun_def)
      moreover from * have ‹∀c. time ((Rep_run sub) 0 c) = time ((Rep_run r) (f 0) c)›
        by (simp add: dilating_def)
      ultimately show ?case by simp
  next
    case (Suc n)
    then show ?case
    proof (cases ‹∄n⇩0. f n⇩0 = Suc n›)
      case True
      with * have ‹∀c. time (Rep_run r (Suc n) c) = time (Rep_run r n c)›
        by (simp add: dilating_def dilating_fun_def) 
      thus ?thesis using Suc.IH by simp
    next
      case False
      from this obtain n⇩0 where n⇩0prop:‹f n⇩0 = Suc n› by blast
      from 1 have ‹R (time ((Rep_run sub) n⇩0 c⇩1), time ((Rep_run sub) n⇩0 c⇩2))› by simp
      moreover from n⇩0prop * have ‹time ((Rep_run sub) n⇩0 c⇩1) = time ((Rep_run r) (Suc n) c⇩1)›
        by (simp add: dilating_def)
      moreover from n⇩0prop * have ‹time ((Rep_run sub) n⇩0 c⇩2) = time ((Rep_run r) (Suc n) c⇩2)›
        by (simp add: dilating_def)
      ultimately show ?thesis by simp
    qed
  qed
qed

corollary tagrel_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦ time-relation ⌊c⇩1,c⇩2⌋ ∈ R ⟧⇩T⇩E⇩S⇩L›
    shows ‹r ∈ ⟦ time-relation ⌊c⇩1,c⇩2⌋ ∈ R ⟧⇩T⇩E⇩S⇩L›
using tagrel_sub'[OF assms] unfolding TESL_interpretation_atomic.simps(3) by simp

text ‹Time relations are also preserved by contraction›
lemma tagrel_sub_inv:
  assumes ‹sub ≪ r›
      and ‹r ∈ ⟦ time-relation ⌊c⇩1, c⇩2⌋ ∈ R ⟧⇩T⇩E⇩S⇩L›
    shows ‹sub ∈ ⟦ time-relation ⌊c⇩1, c⇩2⌋ ∈ R ⟧⇩T⇩E⇩S⇩L›
proof -
  from assms(1) is_subrun_def obtain f where df:‹dilating f sub r› by blast
  moreover from assms(2) TESL_interpretation_atomic.simps(2) have
    ‹r ∈ {ρ. ∀n. R (time ((Rep_run ρ) n c⇩1), time ((Rep_run ρ) n c⇩2))}› by blast
  hence ‹∀n. R (time ((Rep_run r) n c⇩1), time ((Rep_run r) n c⇩2))› by simp
  hence ‹∀n. (∃n⇩0. f n⇩0 = n) ⟶ R (time ((Rep_run r) n c⇩1), time ((Rep_run r) n c⇩2))› by simp
  hence ‹∀n⇩0. R (time ((Rep_run r) (f n⇩0) c⇩1), time ((Rep_run r) (f n⇩0) c⇩2))› by blast
  moreover from dilating_def df have
    ‹∀n c. time ((Rep_run sub) n c) = time ((Rep_run r) (f n) c)› by blast
  ultimately have ‹∀n⇩0. R (time ((Rep_run sub) n⇩0 c⇩1), time ((Rep_run sub) n⇩0 c⇩2))› by auto
  thus ?thesis by simp
qed

text ‹
  Kill relations are preserved in a dilated run.
›
theorem kill_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦ c⇩1 kills c⇩2 ⟧⇩T⇩E⇩S⇩L›
    shows ‹r ∈ ⟦ c⇩1 kills c⇩2 ⟧⇩T⇩E⇩S⇩L›
proof -
  from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast
  from assms(2) TESL_interpretation_atomic.simps(8) have
    ‹∀n. hamlet (Rep_run sub n c⇩1) ⟶ (∀m≥n. ¬ hamlet (Rep_run sub m c⇩2))› by simp
  hence 1:‹∀n. hamlet (Rep_run r (f n) c⇩1) ⟶ (∀m≥n. ¬ hamlet (Rep_run r (f m) c⇩2))›
    using ticks_sub[OF *] by simp
  hence ‹∀n. hamlet (Rep_run r (f n) c⇩1) ⟶ (∀m≥ (f n). ¬ hamlet (Rep_run r m c⇩2))›
  proof -
    { fix n assume ‹hamlet (Rep_run r (f n) c⇩1)›
      with 1 have 2:‹∀ m ≥ n. ¬ hamlet (Rep_run r (f m) c⇩2)› by simp
      have ‹∀ m≥ (f n). ¬ hamlet (Rep_run r m c⇩2)›
      proof -
        { fix m assume h:‹m ≥ f n›
          have ‹¬ hamlet (Rep_run r m c⇩2)›
          proof (cases ‹∃m⇩0. f m⇩0 = m›)
            case True
              from this obtain m⇩0 where fm0:‹f m⇩0 = m› by blast
              hence ‹m⇩0 ≥ n›
                using * dilating_def dilating_fun_def h strict_mono_less_eq by fastforce
              with 2 show ?thesis using fm0 by blast
          next
            case False
              thus ?thesis  using ticks_image_sub'[OF *] by blast
          qed
        } thus ?thesis by simp
      qed
    } thus ?thesis by simp
  qed
  hence ‹∀n. hamlet (Rep_run r n c⇩1) ⟶ (∀m ≥ n. ¬ hamlet (Rep_run r m c⇩2))›
    using ticks_imp_ticks_subk[OF *] by blast
  thus ?thesis using TESL_interpretation_atomic.simps(8) by blast
qed

lemmas atomic_sub_lemmas = sporadic_sub tagrel_sub implies_sub implies_not_sub
                           time_delayed_sub weakly_precedes_sub
                           strictly_precedes_sub kill_sub

text ‹
  We can now prove that all atomic specification formulae are preserved
  by the dilation of runs.
›
lemma atomic_sub: 
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦ φ ⟧⇩T⇩E⇩S⇩L›
    shows ‹r ∈ ⟦ φ ⟧⇩T⇩E⇩S⇩L›
using assms(2) atomic_sub_lemmas[OF assms(1)] by (cases φ, simp_all)

text ‹
  Finally, any TESL specification is invariant by stuttering.
›
theorem TESL_stuttering_invariant:
  assumes ‹sub ≪ r›
    shows ‹sub ∈ ⟦⟦ S ⟧⟧⇩T⇩E⇩S⇩L ⟹ r ∈ ⟦⟦ S ⟧⟧⇩T⇩E⇩S⇩L›
proof (induction S)
  case Nil
    thus ?case by simp
next
  case (Cons a s)
    from Cons.prems have sa:‹sub ∈ ⟦ a ⟧⇩T⇩E⇩S⇩L› and sb:‹sub ∈ ⟦⟦ s ⟧⟧⇩T⇩E⇩S⇩L›
      using TESL_interpretation_image by simp+
    from Cons.IH[OF sb] have ‹r ∈ ⟦⟦ s ⟧⟧⇩T⇩E⇩S⇩L› .
    moreover from atomic_sub[OF assms(1) sa] have ‹r ∈ ⟦ a ⟧⇩T⇩E⇩S⇩L› .
    ultimately show ?case using  TESL_interpretation_image by simp
qed

end