Theory Transition_System_Extensions

section ‹Transition Systems›

theory Transition_System_Extensions
imports
  "Basics/Word_Prefixes"
  "Extensions/Set_Extensions"
  "Extensions/Relation_Extensions"
  Transition_Systems_and_Automata.Transition_System
  Transition_Systems_and_Automata.Transition_System_Extra
  Transition_Systems_and_Automata.Transition_System_Construction
begin

  context transition_system_initial
  begin

    definition cycles :: "'state ⇒ 'transition list set"
      where "cycles p ≡ {w. path w p ∧ target w p = p}"

    lemma cyclesI[intro!]:
      assumes "path w p" "target w p = p"
      shows "w ∈ cycles p"
      using assms unfolding cycles_def by auto
    lemma cyclesE[elim!]:
      assumes "w ∈ cycles p"
      obtains "path w p" "target w p = p"
      using assms unfolding cycles_def by auto

    inductive_set executable :: "'transition set"
      where executable: "p ∈ nodes ⟹ enabled a p ⟹ a ∈ executable"

    lemma executableI_step[intro!]:
      assumes "p ∈ nodes" "enabled a p"
      shows "a ∈ executable"
      using executable assms by this
    lemma executableI_words_fin[intro!]:
      assumes "p ∈ nodes" "path w p"
      shows "set w ⊆ executable"
      using assms by (induct w arbitrary: p, auto del: subsetI)
    lemma executableE[elim?]:
      assumes "a ∈ executable"
      obtains p
      where "p ∈ nodes" "enabled a p"
      using assms by induct auto

  end

  locale transition_system_interpreted =
    transition_system ex en
    for ex :: "'action ⇒ 'state ⇒ 'state"
    and en :: "'action ⇒ 'state ⇒ bool"
    and int :: "'state ⇒ 'interpretation"
  begin

    definition visible :: "'action set"
      where "visible ≡ {a. ∃ q. en a q ∧ int q ≠ int (ex a q)}"

    lemma visibleI[intro]:
      assumes "en a q" "int q ≠ int (ex a q)"
      shows "a ∈ visible"
      using assms unfolding visible_def by auto
    lemma visibleE[elim]:
      assumes "a ∈ visible"
      obtains q
      where "en a q" "int q ≠ int (ex a q)"
      using assms unfolding visible_def by auto

    abbreviation "invisible ≡ - visible"

    lemma execute_fin_word_invisible:
      assumes "path w p" "set w ⊆ invisible"
      shows "int (target w p) = int p"
      using assms by (induct w arbitrary: p rule: list.induct, auto)
    lemma execute_inf_word_invisible:
      assumes "run w p" "k ≤ l" "⋀ i. k ≤ i ⟹ i < l ⟹ w !! i ∉ visible"
      shows "int ((p ## trace w p) !! k) = int ((p ## trace w p) !! l)"
    proof -
      have "(p ## trace w p) !! l = target (stake l w) p" by simp
      also have "stake l w = stake k w @ stake (l - k) (sdrop k w)" using assms(2) by simp
      also have "target … p = target (stake (l - k) (sdrop k w)) (target (stake k w) p)"
        unfolding fold_append comp_apply by rule
      also have "int … = int (target (stake k w) p)"
      proof (rule execute_fin_word_invisible)
        have "w = stake l w @- sdrop l w" by simp
        also have "stake l w = stake k w @ stake (l - k) (sdrop k w)" using assms(2) by simp
        finally have 1: "run (stake k w @- stake (l - k) (sdrop k w) @- sdrop l w) p"
          unfolding shift_append using assms(1) by simp
        show "path (stake (l - k) (sdrop k w)) (target (stake k w) p)" using 1 by auto
        show "set (stake (l - k) (sdrop k w)) ⊆ invisible" using assms(3) by (auto simp: set_stake_snth)
      qed
      also have "… = int ((p ## trace w p) !! k)" by simp
      finally show ?thesis by rule
    qed

  end

  locale transition_system_complete =
    transition_system_initial ex en init +
    transition_system_interpreted ex en int
    for ex :: "'action ⇒ 'state ⇒ 'state"
    and en :: "'action ⇒ 'state ⇒ bool"
    and init :: "'state ⇒ bool"
    and int :: "'state ⇒ 'interpretation"
  begin

    definition language :: "'interpretation stream set"
      where "language ≡ {smap int (p ## trace w p) |p w. init p ∧ run w p}"

    lemma languageI[intro!]:
      assumes "w = smap int (p ## trace v p)" "init p" "run v p"
      shows "w ∈ language"
      using assms unfolding language_def by auto
    lemma languageE[elim!]:
      assumes "w ∈ language"
      obtains p v
      where "w = smap int (p ## trace v p)" "init p" "run v p"
      using assms unfolding language_def by auto

  end

  locale transition_system_finite_nodes =
    transition_system_initial ex en init
    for ex :: "'action ⇒ 'state ⇒ 'state"
    and en :: "'action ⇒ 'state ⇒ bool"
    and init :: "'state ⇒ bool"
    +
    assumes reachable_finite: "finite nodes"

  locale transition_system_cut =
    transition_system_finite_nodes ex en init
    for ex :: "'action ⇒ 'state ⇒ 'state"
    and en :: "'action ⇒ 'state ⇒ bool"
    and init :: "'state ⇒ bool"
    +
    fixes cuts :: "'action set"
    assumes cycles_cut: "p ∈ nodes ⟹ w ∈ cycles p ⟹ w ≠ [] ⟹ set w ∩ cuts ≠ {}"
  begin

    inductive scut :: "'state ⇒ 'state ⇒ bool"
      where scut: "p ∈ nodes ⟹ en a p ⟹ a ∉ cuts ⟹ scut p (ex a p)"

    declare scut.intros[intro!]
    declare scut.cases[elim!]

    lemma scut_reachable:
      assumes "scut p q"
      shows "p ∈ nodes" "q ∈ nodes"
      using assms by auto
    lemma scut_trancl:
      assumes "scut⇧+⇧+ p q"
      obtains w
      where "path w p" "target w p = q" "set w ∩ cuts = {}" "w ≠ []"
    using assms
    proof (induct arbitrary: thesis)
      case (base q)
      show ?case using base by force
    next
      case (step q r)
      obtain w where 1: "path w p" "target w p = q" "set w ∩ cuts = {}" "w ≠ []"
        using step(3) by this
      obtain a where 2: "en a q" "a ∉ cuts" "ex a q = r" using step(2) by auto
      show ?case
      proof (rule step(4))
        show "path (w @ [a]) p" using 1 2 by auto
        show "target (w @ [a]) p = r" using 1 2 by auto
        show "set (w @ [a]) ∩ cuts = {}" using 1 2 by auto
        show "w @ [a] ≠ []" by auto
      qed
    qed

    sublocale wellfounded_relation "scut¯¯"
    proof (unfold_locales, intro finite_acyclic_wf_converse[to_pred] acyclicI[to_pred], safe)
      have 1: "{(p, q). scut p q} ⊆ nodes × nodes" using scut_reachable by blast
      have 2: "finite (nodes × nodes)"
        using finite_cartesian_product reachable_finite by blast
      show "finite {(p, q). scut p q}" using 1 2 by blast
    next
      fix p
      assume 1: "scut⇧+⇧+ p p"
      have 2: "p ∈ nodes" using 1 tranclE[to_pred] scut_reachable by metis
      obtain w where 3: "path w p" "target w p = p" "set w ∩ cuts = {}" "w ≠ []"
        using scut_trancl 1 by this
      have 4: "w ∈ cycles p" using 3(1, 2) by auto
      have 5: "set w ∩ cuts ≠ {}" using cycles_cut 2 4 3(4) by this
      show "False" using 3(3) 5 by simp
    qed

    lemma no_cut_scut:
      assumes "p ∈ nodes" "en a p" "a ∉ cuts"
      shows "scut¯¯ (ex a p) p"
      using assms by auto

  end

  locale transition_system_sticky =
    transition_system_complete ex en init int +
    transition_system_cut ex en init sticky
    for ex :: "'action ⇒ 'state ⇒ 'state"
    and en :: "'action ⇒ 'state ⇒ bool"
    and init :: "'state ⇒ bool"
    and int :: "'state ⇒ 'interpretation"
    and sticky :: "'action set"
    +
    assumes executable_visible_sticky: "executable ∩ visible ⊆ sticky"

end