Theory Stuttering

theory Stuttering
imports StutteringLemmas
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'⟧TESL
    shows ‹r ∈ ⟦c sporadic τ on c'⟧TESL
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)
           ∧ ticks ((Rep_run sub) n c) = ticks ((Rep_run r) (f n) c)› by (simp add: dilating_def)
  moreover from assms(2) have
    ‹sub ∈ {r. ∃ n. ticks ((Rep_run r) n c) ∧ time ((Rep_run r) n c') = τ}› by simp
  from this obtain k where ‹time ((Rep_run sub) k c') = τ ∧ ticks ((Rep_run sub) k c)› by auto
  ultimately have ‹time ((Rep_run r) (f k) c') = τ ∧ ticks ((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 ∈ ⟦c1 implies c2TESL
    shows ‹r ∈ ⟦c1 implies c2TESL
proof -
  from assms(1) is_subrun_def obtain f where ‹dilating f sub r› by blast
  moreover from assms(2) have
    ‹sub ∈ {r. ∀n. ticks ((Rep_run r) n c1) ⟶ ticks ((Rep_run r) n c2)}› by simp
  hence ‹∀n. ticks ((Rep_run sub) n c1) ⟶ ticks ((Rep_run sub) n c2)› by simp
  ultimately have ‹∀n. ticks ((Rep_run r) n c1) ⟶ ticks ((Rep_run r) n c2)›
    using ticks_imp_ticks_subk ticks_sub by blast
  thus ?thesis by simp
qed

theorem implies_not_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦c1 implies not c2TESL
    shows ‹r ∈ ⟦c1 implies not c2TESL
proof -
  from assms(1) is_subrun_def obtain f where ‹dilating f sub r› by blast
  moreover from assms(2) have
    ‹sub ∈ {r. ∀n. ticks ((Rep_run r) n c1) ⟶ ¬ ticks ((Rep_run r) n c2)}› by simp
  hence ‹∀n. ticks ((Rep_run sub) n c1) ⟶ ¬ ticks ((Rep_run sub) n c2)› by simp
  ultimately have ‹∀n. ticks ((Rep_run r) n c1) ⟶ ¬ ticks ((Rep_run r) n c2)›
    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 ∈ ⟦c1 weakly precedes c2TESL
    shows ‹r ∈ ⟦c1 weakly precedes c2TESL
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 c2 n) ≤ (run_tick_count r c1 n)}› by simp
  hence ‹∀n. (run_tick_count sub c2 n) ≤ (run_tick_count sub c1 n)› by simp
  from dil_tick_count[OF assms(1) this]
    have ‹∀n. (run_tick_count r c2 n) ≤ (run_tick_count r c1 n)› by simp
  thus ?thesis by simp
qed

theorem strictly_precedes_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦c1 strictly precedes c2TESL
    shows ‹r ∈ ⟦c1 strictly precedes c2TESL
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 ρ c2 n) ≤ (run_tick_count_strictly ρ c1 n) }›
  by simp
  with strictly_precedes_alt_def2[of ‹c2 ‹c1]  have
    ‹sub ∈ { ρ. (¬ticks ((Rep_run ρ) 0 c2))
  ∧ (∀n::nat. (run_tick_count ρ c2 (Suc n)) ≤ (run_tick_count ρ c1 n)) }›
  by blast
  hence ‹(¬ticks ((Rep_run sub) 0 c2))
       ∧ (∀n::nat. (run_tick_count sub c2 (Suc n)) ≤ (run_tick_count sub c1 n))›
    by simp
  hence
    1:‹(¬ticks ((Rep_run sub) 0 c2))
     ∧ (∀n::nat. (tick_count sub c2 (Suc n)) ≤ (tick_count sub c1 n))›
  by (simp add: tick_count_is_fun)
  have ‹∀n::nat. (tick_count r c2 (Suc n)) ≤ (tick_count r c1 n)›
  proof -
    { fix n::nat
      have ‹tick_count r c2 (Suc n) ≤ tick_count r c1 n›
      proof (cases ‹∃n0. f n0 = n›)
        case True ― ‹n is in the image of f›
          from this obtain n0 where fn:‹f n0 = n› by blast
          show ?thesis
          proof (cases ‹∃sn0. f sn0 = Suc n›)
            case True ― ‹Suc n is in the image of f›
              from this obtain sn0 where fsn:‹f sn0 = Suc n› by blast
              with fn strict_mono_suc * have ‹sn0 = Suc n0
                using  dilating_def dilating_fun_def by blast
              with 1 have ‹tick_count sub c2 sn0 ≤ tick_count sub c1 n0 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 ‹¬ticks ((Rep_run r) (Suc n) c2)›
                using * by (simp add: dilating_def dilating_fun_def)
              hence ‹tick_count r c2 (Suc n) = tick_count r c2 n›
                by (simp add: tick_count_suc)
              also have ‹... = tick_count sub c2 n0
                using fn tick_count_sub[OF *] by simp
              finally have ‹tick_count r c2 (Suc n) = tick_count sub c2 n0 .
              moreover have ‹tick_count sub c2 n0 ≤ tick_count sub c2 (Suc n0)›
                by (simp add: tick_count_suc)
              ultimately have
                ‹tick_count r c2 (Suc n) ≤ tick_count sub c2 (Suc n0)› by simp
              moreover have
                ‹tick_count sub c2 (Suc n0) ≤ tick_count sub c1 n0 using 1 by simp
              ultimately have ‹tick_count r c2 (Suc n) ≤ tick_count sub c1 n0 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 np  where
            np_prop:‹f np < n ∧ (∀k. f np < k ∧ k ≤ n ⟶ (∄k0. f k0 = k))› by blast
          from tick_count_latest[OF * this] have
            ‹tick_count r c1 n = tick_count r c1 (f np)› . 
          hence a:‹tick_count r c1 n = tick_count sub c1 np
            using tick_count_sub[OF *] by simp
          have b: ‹tick_count sub c2 (Suc np) ≤ tick_count sub c1 np using 1 by simp
          show ?thesis
          proof (cases ‹∃sn0. f sn0 = Suc n›)
            case True ― ‹Suc n is in the image of f›
              from this obtain sn0 where fsn:‹f sn0 = Suc n› by blast
              from next_non_stuttering[OF * np_prop this]  have sn_prop:‹sn0 = Suc np .
              with b have ‹tick_count sub c2 sn0 ≤ tick_count sub c1 np 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 ‹¬ticks ((Rep_run r) (Suc n) c2)›
                using * by (simp add: dilating_def dilating_fun_def)
              hence ‹tick_count r c2 (Suc n) = tick_count r c2 n›
                by (simp add: tick_count_suc)
              also have ‹... = tick_count sub c2 np using np_prop tick_count_sub[OF *]
                by (simp add: tick_count_latest[OF * np_prop])
              finally have ‹tick_count r c2 (Suc n) = tick_count sub c2 np .
              moreover have ‹tick_count sub c2 np ≤ tick_count sub c2 (Suc np)›
                by (simp add: tick_count_suc)
              ultimately have
                ‹tick_count r c2 (Suc n) ≤ tick_count sub c2 (Suc np)› by simp
              moreover have
                ‹tick_count sub c2 (Suc np) ≤ tick_count sub c1 np using 1 by simp
              ultimately have ‹tick_count r c2 (Suc n) ≤ tick_count sub c1 np by simp
              thus ?thesis using np_prop mono_tick_count  using a by linarith
          qed
      qed
    } thus ?thesis ..
  qed
  moreover from 1 have ‹¬ticks ((Rep_run r) 0 c2)›
    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 ⟧TESL
    shows ‹r ∈ ⟦ a time-delayed by δτ on ms implies b ⟧TESL
proof -
  from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast
  from assms(2) have ‹∀n. ticks ((Rep_run sub) n a)
                          ⟶ (∀m ≥ n. first_time sub ms m (time ((Rep_run sub) n ms) + δτ)
                                       ⟶ ticks ((Rep_run sub) m b))›
    using TESL_interpretation_atomic.simps(5)[of ‹a› ‹δτ› ‹ms› ‹b›] by simp
  hence **:‹∀n0. ticks ((Rep_run r) (f n0) a)
                  ⟶ (∀m0 ≥ n0. first_time r ms (f m0) (time ((Rep_run r) (f n0) ms) + δτ)
                                  ⟶ ticks ((Rep_run r) (f m0) b))  ›
    using first_time_image[OF *] dilating_def * by fastforce
  hence ‹∀n. ticks ((Rep_run r) n a)
                  ⟶ (∀m ≥ n. first_time r ms m (time ((Rep_run r) n ms) + δτ)
                                ⟶ ticks ((Rep_run r) m b))›
  proof -
    { fix n assume assm:‹ticks ((Rep_run r) n a)›
      from ticks_image_sub[OF * assm] obtain n0 where nfn0:‹n = f n0 by blast
      with ** assm have ft0:
        ‹(∀m0 ≥ n0. first_time r ms (f m0) (time ((Rep_run r) (f n0) ms) + δτ)
                    ⟶ ticks ((Rep_run r) (f m0) b))› by blast
      have ‹(∀m ≥ n. first_time r ms m (time ((Rep_run r) n ms) + δτ) 
                       ⟶ ticks ((Rep_run r) m b)) ›
      proof -
      { fix m assume hyp:‹m ≥ n›
        have ‹first_time r ms m (time (Rep_run r n ms) + δτ) ⟶ ticks (Rep_run r m b)›
        proof (cases ‹∃m0. f m0 = m›)
          case True
          from this obtain m0 where ‹m = f m0 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 ‹∄pm0. f pm0 = Suc pm› using ‹∄m0. f m0 = 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 ‹
  Relaxed time delayed relations are preserved in a dilated run.
›
theorem relaxed_time_delayed_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦ a time-delayed⨝ by δτ on ms implies b ⟧TESL
    shows ‹r ∈ ⟦ a time-delayed⨝ by δτ on ms implies b ⟧TESL
proof -
  from assms(1) is_subrun_def obtain f where dilf:‹dilating f sub r› by blast
  from assms(2) have ‹∀n. ticks ((Rep_run sub) n a)
                          ⟶ (∃m ≥ n. ticks ((Rep_run sub) m b)
                                     ∧ time ((Rep_run sub) m ms) = time ((Rep_run sub) n ms) + δτ)›
    using TESL_interpretation_atomic.simps(6)[of ‹a› ‹δτ› ‹ms› ‹b›] by simp
  hence **:‹∀n0. ticks ((Rep_run r) (f n0) a)
                  ⟶ (∃m0 ≥ n0. ticks ((Rep_run r) (f m0) b)
                               ∧ time ((Rep_run r) (f m0) ms) = time ((Rep_run r) (f n0) ms) + δτ)›
    using first_time_image[OF dilf] dilating_def dilf by fastforce
  hence ‹∀n. ticks ((Rep_run r) n a)
                  ⟶ (∃m ≥ n. ticks ((Rep_run r) m b)
                             ∧  time ((Rep_run r) m ms) = time ((Rep_run r) n ms) + δτ)›
  proof -
    { fix n assume assm:‹ticks ((Rep_run r) n a)›
      from ticks_image_sub[OF dilf assm] obtain n0 where nfn0:‹n = f n0 by blast
      with ** assm have ft0:
        ‹(∃m0 ≥ n0. ticks ((Rep_run r) (f m0) b)
                  ∧ time ((Rep_run r) (f m0) ms) = time ((Rep_run r) (f n0) ms) + δτ)› by blast
      from this obtain m0 where
        ‹m0 ≥ n0 ∧ ticks ((Rep_run r) (f m0) b)
      ∧ (time ((Rep_run r) (f m0) ms) = time ((Rep_run r) n ms) + δτ)› using nfn0 by blast
      hence ‹f m0 ≥ n›
        and ‹ticks ((Rep_run r) (f m0) b)
          ∧ (time ((Rep_run r) (f m0) ms) = time ((Rep_run r) n ms) + δτ)›
        using dilf nfn0
        by (simp add: dilating_def dilating_fun_def strict_mono_less_eq, simp)
      hence ‹(∃m ≥ n. ticks ((Rep_run r) m b)
                  ∧ time ((Rep_run r) m ms) = time ((Rep_run r) n ms) + δτ)› by blast
    } 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 ⌊c1,c2⌋ ∈ R ⟧TESL
    shows ‹R (time ((Rep_run r) n c1), time ((Rep_run r) n c2))›
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 c1), time ((Rep_run r) n c2))}› by blast
  hence 1:‹∀n. R (time ((Rep_run sub) n c1), time ((Rep_run sub) n c2))› by simp
  show ?thesis
  proof (induction n)
    case 0
      from 1 have ‹R (time ((Rep_run sub) 0 c1), time ((Rep_run sub) 0 c2))› 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 ‹∄n0. f n0 = 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 n0 where n0prop:‹f n0 = Suc n› by blast
      from 1 have ‹R (time ((Rep_run sub) n0 c1), time ((Rep_run sub) n0 c2))› by simp
      moreover from n0prop * have ‹time ((Rep_run sub) n0 c1) = time ((Rep_run r) (Suc n) c1)›
        by (simp add: dilating_def)
      moreover from n0prop * have ‹time ((Rep_run sub) n0 c2) = time ((Rep_run r) (Suc n) c2)›
        by (simp add: dilating_def)
      ultimately show ?thesis by simp
    qed
  qed
qed

corollary tagrel_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦ time-relation ⌊c1,c2⌋ ∈ R ⟧TESL
    shows ‹r ∈ ⟦ time-relation ⌊c1,c2⌋ ∈ R ⟧TESL
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 ⌊c1, c2⌋ ∈ R ⟧TESL
    shows ‹sub ∈ ⟦ time-relation ⌊c1, c2⌋ ∈ R ⟧TESL
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 c1), time ((Rep_run ρ) n c2))}› by blast
  hence ‹∀n. R (time ((Rep_run r) n c1), time ((Rep_run r) n c2))› by simp
  hence ‹∀n. (∃n0. f n0 = n) ⟶ R (time ((Rep_run r) n c1), time ((Rep_run r) n c2))› by simp
  hence ‹∀n0. R (time ((Rep_run r) (f n0) c1), time ((Rep_run r) (f n0) c2))› 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 ‹∀n0. R (time ((Rep_run sub) n0 c1), time ((Rep_run sub) n0 c2))› by auto
  thus ?thesis by simp
qed

text ‹
  Kill relations are preserved in a dilated run.
›
theorem kill_sub:
  assumes ‹sub ≪ r›
      and ‹sub ∈ ⟦ c1 kills c2TESL
    shows ‹r ∈ ⟦ c1 kills c2TESL
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. ticks (Rep_run sub n c1) ⟶ (∀m≥n. ¬ ticks (Rep_run sub m c2))› by simp
  hence 1:‹∀n. ticks (Rep_run r (f n) c1) ⟶ (∀m≥n. ¬ ticks (Rep_run r (f m) c2))›
    using ticks_sub[OF *] by simp
  hence ‹∀n. ticks (Rep_run r (f n) c1) ⟶ (∀m≥ (f n). ¬ ticks (Rep_run r m c2))›
  proof -
    { fix n assume ‹ticks (Rep_run r (f n) c1)›
      with 1 have 2:‹∀ m ≥ n. ¬ ticks (Rep_run r (f m) c2)› by simp
      have ‹∀ m≥ (f n). ¬ ticks (Rep_run r m c2)›
      proof -
        { fix m assume h:‹m ≥ f n›
          have ‹¬ ticks (Rep_run r m c2)›
          proof (cases ‹∃m0. f m0 = m›)
            case True
              from this obtain m0 where fm0:‹f m0 = m› by blast
              hence ‹m0 ≥ 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. ticks (Rep_run r n c1) ⟶ (∀m ≥ n. ¬ ticks (Rep_run r m c2))›
    using ticks_imp_ticks_subk[OF *] by blast
  thus ?thesis using TESL_interpretation_atomic.simps(9) 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 relaxed_time_delayed_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 ‹is_public_atom φ›
      and ‹sub ∈ ⟦ φ ⟧TESL
    shows ‹r ∈ ⟦ φ ⟧TESL
using assms(2,3) 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 ‹⟦is_public_spec S; sub ∈ ⟦⟦ S ⟧⟧TESL⟧ ⟹ r ∈ ⟦⟦ S ⟧⟧TESL
proof (induction S)
  case Nil
    thus ?case by simp
next
  case (Cons a s) print_facts
    from Cons.prems(1) have puba:‹is_public_atom a› and pubs:‹is_public_spec s› by simp+
    from Cons.prems(2) have sa:‹sub ∈ ⟦ a ⟧TESL and sb:‹sub ∈ ⟦⟦ s ⟧⟧TESL
      using TESL_interpretation_image by simp+
    from Cons.IH[OF pubs sb] have ‹r ∈ ⟦⟦ s ⟧⟧TESL .
    moreover from atomic_sub[OF assms(1) puba sa] have ‹r ∈ ⟦ a ⟧TESL .
    ultimately show ?case using  TESL_interpretation_image by simp
qed

end