Theory Partial_Order_Reduction.Stuttering

section ‹Stuttering›

theory Stuttering
imports
  Stuttering_Equivalence.StutterEquivalence
  LList_Prefixes
begin

  function nth_least_ext :: "nat set ⇒ nat ⇒ nat"
    where
      "enat k < esize A ⟹ nth_least_ext A k = nth_least A k" |
      "enat k ≥ esize A ⟹ nth_least_ext A k = Suc (Max A + (k - card A))"
    by force+ termination by lexicographic_order

  lemma nth_least_ext_strict_mono:
    assumes "k < l"
    shows "nth_least_ext s k < nth_least_ext s l"
  proof (cases "enat l < esize s")
    case True
    have 1: "enat k < esize s" using assms True by (metis enat_ord_simps(2) less_trans)
    show ?thesis using nth_least_strict_mono assms True 1 by simp
  next
    case False
    have 1: "finite s" using False esize_infinite_enat by auto
    have 2: "enat l ≥ esize s" using False by simp
    have 3: "l ≥ card s" using 1 2 by simp
    show ?thesis
    proof (cases "enat k < esize s")
      case True
      have 4: "s ≠ {}" using True by auto
      have "nth_least_ext s k = nth_least s k" using True by simp
      also have "… ≤ Max s" using nth_least_le_Max 1 4 True by this
      also have "… < Suc (Max s)" by auto
      also have "… ≤ Suc (Max s + (l - card s))" by auto
      also have "Suc (Max s + (l - card s)) = nth_least_ext s l" using 2 by simp
      finally show ?thesis by this
    next
      case False
      have 4: "enat k ≥ esize s" using False by simp
      have 5: "k ≥ card s" using 1 4 by simp
      have "nth_least_ext s k = Suc (Max s + (k - card s))" using 4 by simp
      also have "… < Suc (Max s + (l - card s))" using assms 5 by simp
      also have "… = nth_least_ext s l" using 2 by simp
      finally show ?thesis by this
    qed
  qed

  definition stutter_selection :: "nat set ⇒ 'a llist ⇒ bool"
    where "stutter_selection s w ≡ 0 ∈ s ∧
      (∀ k i. enat i < llength w ⟶ enat (Suc k) < esize s ⟶
      nth_least s k < i ⟶ i < nth_least s (Suc k) ⟶ w ?! i = w ?! nth_least s k) ∧
      (∀ i. enat i < llength w ⟶ finite s ⟶ Max s < i ⟶ w ?! i = w ?! Max s)"

  lemma stutter_selectionI[intro]:
    assumes "0 ∈ s"
    assumes "⋀ k i. enat i < llength w ⟹ enat (Suc k) < esize s ⟹
      nth_least s k < i ⟹ i < nth_least s (Suc k) ⟹ w ?! i = w ?! nth_least s k"
    assumes "⋀ i. enat i < llength w ⟹ finite s ⟹ Max s < i ⟹ w ?! i = w ?! Max s"
    shows "stutter_selection s w"
    using assms unfolding stutter_selection_def by auto
  lemma stutter_selectionD_0[dest]:
    assumes "stutter_selection s w"
    shows "0 ∈ s"
    using assms unfolding stutter_selection_def by auto
  lemma stutter_selectionD_inside[dest]:
    assumes "stutter_selection s w"
    assumes "enat i < llength w" "enat (Suc k) < esize s"
    assumes "nth_least s k < i" "i < nth_least s (Suc k)"
    shows "w ?! i = w ?! nth_least s k"
    using assms unfolding stutter_selection_def by auto
  lemma stutter_selectionD_infinite[dest]:
    assumes "stutter_selection s w"
    assumes "enat i < llength w" "finite s" "Max s < i"
    shows "w ?! i = w ?! Max s"
    using assms unfolding stutter_selection_def by auto

  lemma stutter_selection_stutter_sampler[intro]:
    assumes "linfinite w" "stutter_selection s w"
    shows "stutter_sampler (nth_least_ext s) (lnth w)"
  unfolding stutter_sampler_def
  proof safe
    show "nth_least_ext s 0 = 0" using assms(2) by (cases "enat 0 < esize s", auto)
    show "strict_mono (nth_least_ext s)" using strict_monoI nth_least_ext_strict_mono by blast
  next
    fix k i
    assume 1: "nth_least_ext s k < i" "i < nth_least_ext s (Suc k)"
    show "w ?! i = w ?! nth_least_ext s k"
    proof (cases "enat (Suc k)" "esize s" rule: linorder_cases)
      case less
      have "w ?! i = w ?! nth_least s k"
      proof (rule stutter_selectionD_inside)
        show "stutter_selection s w" using assms(2) by this
        show "enat i < llength w" using assms(1) by auto
        show "enat (Suc k) < esize s" using less by this
        show "nth_least s k < i" using 1(1) less by auto
        show "i < nth_least s (Suc k)" using 1(2) less by simp
      qed
      also have "w ?! nth_least s k = w ?! nth_least_ext s k" using less by auto
      finally show ?thesis by this
    next
      case equal
      have 2: "enat k < esize s" using equal by (metis enat_ord_simps(2) lessI)
      have 3: "finite s" using equal by (metis esize_infinite_enat less_irrefl)
      have 4: "⋀ i. i > Max s ⟹ w ?! i = w ?! Max s" using assms 3 by auto
      have 5: "k = card s - 1" using equal 3 by (metis diff_Suc_1 enat.inject esize_set.simps(1))
      have "Max s = nth_least s (card s - 1)" using nth_least_Max 3 assms(2) by force
      also have "… = nth_least s k" unfolding 5 by rule
      also have "… = nth_least_ext s k" using 2 by simp 
      finally have 6: "Max s = nth_least_ext s k" by this
      have "w ?! i = w ?! Max s" using 1(1) 4 6 by auto
      also have "… = w ?! nth_least_ext s k" unfolding 6 by rule
      finally show ?thesis by this
    next
      case greater
      have 2: "enat k ≥ esize s" using greater by (metis Suc_ile_eq not_le)
      have 3: "finite s" using greater by (metis esize_infinite_enat less_asym)
      have 4: "⋀ i. i > Max s ⟹ w ?! i = w ?! Max s" using assms 3 by auto
      have "w ?! i = w ?! Max s" using 1(1) 2 4 by auto 
      also have "… = w ?! Suc (Max s + (k - card s))" using 4 by simp
      also have "… = w ?! nth_least_ext s k" using 2 by simp
      finally show ?thesis by this
    qed
  qed

  lemma stutter_equivI_selection[intro]:
    assumes "linfinite u" "linfinite v"
    assumes "stutter_selection s u" "stutter_selection t v"
    assumes "lselect s u = lselect t v"
    shows "lnth u ≈ lnth v"
  proof (rule stutter_equivI)
    have 1: "llength (lselect s u) = llength (lselect t v)" unfolding assms(5) by rule
    have 2: "esize s = esize t" using 1 assms(1, 2) unfolding lselect_llength by simp
    show "stutter_sampler (nth_least_ext s) (lnth u)" using assms(1, 3) by rule
    show "stutter_sampler (nth_least_ext t) (lnth v)" using assms(2, 4) by rule
    show "lnth u ∘ nth_least_ext s = lnth v ∘ nth_least_ext t"
    proof (rule ext, unfold comp_apply)
      fix i
      show "u ?! nth_least_ext s i = v ?! nth_least_ext t i" 
      proof (cases "enat i < esize s")
        case True
        have 3: "enat i < llength (lselect s u)" "enat i < llength (lselect t v)"
          using assms(1, 2) 2 True unfolding lselect_llength by auto
        have "u ?! nth_least_ext s i = u ?! nth_least s i" using True by simp
        also have "… = lselect s u ?! i" using 3(1) by simp
        also have "… = lselect t v ?! i" unfolding assms(5) by rule
        also have "… = v ?! nth_least t i" using 3(2) by simp
        also have "… = v ?! nth_least_ext t i" using True unfolding 2 by simp
        finally show "u ?! nth_least_ext s i = v ?! nth_least_ext t i" by this
      next
        case False
        have 3: "s ≠ {}" "t ≠ {}" using assms(3, 4) by auto
        have 4: "finite s" "finite t" using esize_infinite_enat 2 False by metis+
        have 5: "⋀ i. i > Max s ⟹ u ?! i = u ?! Max s" using assms(1, 3) 4(1) by auto
        have 6: "⋀ i. i > Max t ⟹ v ?! i = v ?! Max t" using assms(2, 4) 4(2) by auto
        have 7: "esize s = enat (card s)" "esize t = enat (card t)" using 4 by auto
        have 8: "card s ≠ 0" "card t ≠ 0" using 3 4 by auto
        have 9: "enat (card s - 1) < llength (lselect s u)"
          using assms(1) 7(1) 8(1) unfolding lselect_llength by simp
        have 10: "enat (card t - 1) < llength (lselect t v)"
          using assms(2) 7(2) 8(2) unfolding lselect_llength by simp
        have "u ?! nth_least_ext s i = u ?! Suc (Max s + (i - card s))" using False by simp
        also have "… = u ?! Max s" using 5 by simp
        also have "… = u ?! nth_least s (card s - 1)" using nth_least_Max 4(1) 3(1) by force
        also have "… = lselect s u ?! (card s - 1)" using lselect_lnth 9 by simp
        also have "… = lselect s u ?! (card t - 1)" using 2 4 by simp
        also have "… = lselect t v ?! (card t - 1)" unfolding assms(5) by rule
        also have "… = v ?! nth_least t (card t - 1)" using lselect_lnth 10 by simp
        also have "… = v ?! Max t" using nth_least_Max 4(2) 3(2) by force
        also have "… = v ?! Suc (Max t + (i - card t))" using 6 by simp
        also have "… = v ?! nth_least_ext t i" using 2 False by simp
        finally show ?thesis by this
      qed
    qed
  qed

  definition stuttering_invariant :: "'a word set ⇒ bool"
    where "stuttering_invariant A ≡ ∀ u v. u ≈ v ⟶ u ∈ A ⟷ v ∈ A"

  lemma stuttering_invariant_complement[intro!]:
    assumes "stuttering_invariant A"
    shows "stuttering_invariant (- A)"
    using assms unfolding stuttering_invariant_def by simp

  lemma stutter_equiv_forw_subst[trans]: "w⇩1 = w⇩2 ⟹ w⇩2 ≈ w⇩3 ⟹ w⇩1 ≈ w⇩3" by auto

  lemma stutter_sampler_build:
    assumes "stutter_sampler f w"
    shows "stutter_sampler (0 ## (Suc ∘ f)) (a ## w)"
  unfolding stutter_sampler_def
  proof safe
    have 0: "f 0 = 0" using assms unfolding stutter_sampler_def by auto
    have 1: "f x < f y" if "x < y" for x y
      using assms that unfolding stutter_sampler_def strict_mono_def by auto
    have 2: "(0 ## (Suc ∘ f)) x < (0 ## (Suc ∘ f)) y" if "x < y" for x y
      using 1 that by (cases x; cases y) (auto)
    have 3: "w n = w (f k)" if "f k < n" "n < f (Suc k)" for k n
      using assms that unfolding stutter_sampler_def by auto
    show "(0 ## (Suc ∘ f)) 0 = 0" by simp
    show "strict_mono (0 ## (Suc ∘ f))" using 2 by rule
    show "(a ## w) n = (a ## w) ((0 ## (Suc ∘ f)) k)"
      if "(0 ## (Suc ∘ f)) k < n" "n < (0 ## (Suc ∘ f)) (Suc k)" for k n
      using 0 3 that by (cases k; cases n) (force)+
  qed
  lemma stutter_extend_build:
    assumes "u ≈ v"
    shows "a ## u ≈ a ## v"
  proof -
    obtain f g where 1: "stutter_sampler f u" "stutter_sampler g v" "u ∘ f = v ∘ g"
      using stutter_equivE assms by this
    show ?thesis
    proof (intro stutter_equivI ext)
      show "stutter_sampler (0 ## (Suc ∘ f)) (a ## u)" using stutter_sampler_build 1(1) by this
      show "stutter_sampler (0 ## (Suc ∘ g)) (a ## v)" using stutter_sampler_build 1(2) by this
      show "(a ## u ∘ 0 ## (Suc ∘ f)) i = (a ## v ∘ 0 ## (Suc ∘ g)) i" for i
        using fun_cong[OF 1(3)] by (cases i) (auto)
    qed
  qed
  lemma stutter_extend_concat:
    assumes "u ≈ v"
    shows "w ⌢ u ≈ w ⌢ v"
    using stutter_extend_build assms by (induct w, force+)
  lemma build_stutter: "w 0 ## w ≈ w"
  proof (rule stutter_equivI)
    show "stutter_sampler (Suc (0 := 0)) (w 0 ## w)"
    unfolding stutter_sampler_def
    proof safe
      show "(Suc (0 := 0)) 0 = 0" by simp
      show "strict_mono (Suc (0 := 0))" by (rule strict_monoI, simp)
    next
      fix k n
      assume 1: "(Suc (0 := 0)) k < n" "n < (Suc (0 := 0)) (Suc k)"
      show "(w 0 ## w) n = (w 0 ## w) ((Suc (0 := 0)) k)" using 1 by (cases n, auto)
    qed
    show "stutter_sampler id w" by rule
    show "w 0 ## w ∘ (Suc (0 := 0)) = w ∘ id" by auto
  qed
  lemma replicate_stutter: "replicate n (v 0) ⌢ v ≈ v"
  proof (induct n)
    case 0
    show ?case using stutter_equiv_refl by simp
  next
    case (Suc n)
    have "replicate (Suc n) (v 0) ⌢ v = v 0 ## replicate n (v 0) ⌢ v" by simp
    also have "… = (replicate n (v 0) ⌢ v) 0 ## replicate n (v 0) ⌢ v" by (cases n, auto)
    also have "… ≈ replicate n (v 0) ⌢ v" using build_stutter by this
    also have "… ≈ v" using Suc by this
    finally show ?case by this
  qed

  lemma replicate_stutter': "u ⌢ replicate n (v 0) ⌢ v ≈ u ⌢ v"
    using stutter_extend_concat replicate_stutter by this

end