Theory Transition_System_Traces

section ‹Transition Systems and Trace Theory›

theory Transition_System_Traces
imports
  Transition_System_Extensions
  Traces
begin

  lemma (in transition_system) words_infI_construct[rule_format, intro?]:
    assumes "∀ v. v ≤⇩F⇩I w ⟶ path v p"
    shows "run w p"
    using assms by coinduct auto

  lemma (in transition_system) words_infI_construct':
    assumes "⋀ k. ∃ v. v ≤⇩F⇩I w ∧ k < length v ∧ path v p"
    shows "run w p"
  proof
    fix u
    assume 1: "u ≤⇩F⇩I w"
    obtain v where 2: "v ≤⇩F⇩I w" "length u < length v" "path v p" using assms(1) by auto
    have 3: "length u ≤ length v" using 2(2) by simp
    have 4: "u ≤ v" using prefix_fininf_length 1 2(1) 3 by this
    show "path u p" using 4 2(3) by auto
  qed

  lemma (in transition_system) words_infI_construct_chain[intro]:
    assumes "chain w" "⋀ k. path (w k) p"
    shows "run (limit w) p"
  proof (rule words_infI_construct')
    fix k
    obtain l where 1: "k < length (w l)" using assms(1) by rule
    show "∃ v. v ≤⇩F⇩I limit w ∧ k < length v ∧ path v p"
    proof (intro exI conjI)
      show "w l ≤⇩F⇩I limit w" using chain_prefix_limit assms(1) by this
      show "k < length (w l)" using 1 by this
      show "path (w l) p" using assms(2) by this
    qed
  qed

  lemma (in transition_system) words_fin_blocked:
    assumes "⋀ w. path w p ⟹ A ∩ set w = {} ⟹ A ∩ {a. enabled a (target w p)} ⊆ A ∩ {a. enabled a p}"
    assumes "path w p" "A ∩ {a. enabled a p} ∩ set w = {}"
    shows "A ∩ set w = {}"
    using assms by (induct w rule: rev_induct, auto)

  locale transition_system_traces =
    transition_system ex en +
    traces ind
    for ex :: "'action ⇒ 'state ⇒ 'state"
    and en :: "'action ⇒ 'state ⇒ bool"
    and ind :: "'action ⇒ 'action ⇒ bool"
    +
    assumes en: "ind a b ⟹ en a p ⟹ en b p ⟷ en b (ex a p)"
    assumes ex: "ind a b ⟹ en a p ⟹ en b p ⟹ ex b (ex a p) = ex a (ex b p)"
  begin

    lemma diamond_bottom:
      assumes "ind a b"
      assumes "en a p" "en b p"
      shows "en a (ex b p)" "en b (ex a p)" "ex b (ex a p) = ex a (ex b p)"
      using assms independence_symmetric en ex by metis+
    lemma diamond_right:
      assumes "ind a b"
      assumes "en a p" "en b (ex a p)"
      shows "en a (ex b p)" "en b p" "ex b (ex a p) = ex a (ex b p)"
      using assms independence_symmetric en ex by metis+
    lemma diamond_left:
      assumes "ind a b"
      assumes "en a (ex b p)" "en b p"
      shows "en a p" "en b (ex a p)" "ex b (ex a p) = ex a (ex b p)"
      using assms independence_symmetric en ex by metis+

    lemma eq_swap_word:
      assumes "w⇩1 =⇩S w⇩2" "path w⇩1 p"
      shows "path w⇩2 p"
      using assms diamond_right by (induct, auto)
    lemma eq_fin_word:
      assumes "w⇩1 =⇩F w⇩2" "path w⇩1 p"
      shows "path w⇩2 p"
      using assms eq_swap_word by (induct, auto)
    lemma le_fin_word:
      assumes "w⇩1 ≼⇩F w⇩2" "path w⇩2 p"
      shows "path w⇩1 p"
      using assms eq_fin_word by blast
    lemma le_fininf_word:
      assumes "w⇩1 ≼⇩F⇩I w⇩2" "run w⇩2 p"
      shows "path w⇩1 p"
      using assms le_fin_word by blast
    lemma le_inf_word:
      assumes "w⇩2 ≼⇩I w⇩1" "run w⇩1 p"
      shows "run w⇩2 p"
      using assms le_fininf_word by (blast intro: words_infI_construct)
    lemma eq_inf_word:
      assumes "w⇩1 =⇩I w⇩2" "run w⇩1 p"
      shows "run w⇩2 p"
      using assms le_inf_word by auto

    lemma eq_swap_execute:
      assumes "path w⇩1 p" "w⇩1 =⇩S w⇩2"
      shows "fold ex w⇩1 p = fold ex w⇩2 p"
      using assms(2, 1) diamond_right by (induct, auto)
    lemma eq_fin_execute:
      assumes "path w⇩1 p" "w⇩1 =⇩F w⇩2"
      shows "fold ex w⇩1 p = fold ex w⇩2 p"
      using assms(2, 1) eq_fin_word eq_swap_execute by (induct, auto)

    lemma diamond_fin_word_step:
      assumes "Ind {a} (set v)" "en a p" "path v p"
      shows "path v (ex a p)"
      using diamond_bottom assms by (induct v arbitrary: p, auto, metis)
    lemma diamond_inf_word_step:
      assumes "Ind {a} (sset w)" "en a p" "run w p"
      shows "run w (ex a p)"
      using diamond_fin_word_step assms by (fast intro: words_infI_construct)
    lemma diamond_fin_word_inf_word:
      assumes "Ind (set v) (sset w)" "path v p" "run w p"
      shows "run w (fold ex v p)"
      using diamond_inf_word_step assms by (induct v arbitrary: p, auto)
    lemma diamond_fin_word_inf_word':
      assumes "Ind (set v) (sset w)" "path (u @ v) p" "run (u @- w) p"
      shows "run (u @- v @- w) p"
      using assms diamond_fin_word_inf_word by auto

  end

end