Theory Transition_System

section ‹Transition Systems›

theory Transition_System
imports "../Basic/Sequence"
begin

  subsection ‹Universal Transition Systems›

  locale transition_system_universal =
    fixes execute :: "'transition ⇒ 'state ⇒ 'state"
  begin

    abbreviation "target ≡ fold execute"
    abbreviation "states ≡ scan execute"
    abbreviation "trace ≡ sscan execute"

    lemma target_alt_def: "target r p = last (p # states r p)" using scan_last by rule

  end

  subsection ‹Transition Systems›

  locale transition_system =
    transition_system_universal execute
    for execute :: "'transition ⇒ 'state ⇒ 'state"
    +
    fixes enabled :: "'transition ⇒ 'state ⇒ bool"
  begin

    abbreviation "successors p ≡ {execute a p |a. enabled a p}"

    inductive path :: "'transition list ⇒ 'state ⇒ bool" where
      nil[intro!]: "path [] p" |
      cons[intro!]: "enabled a p ⟹ path r (execute a p) ⟹ path (a # r) p"

    inductive_cases path_cons_elim[elim!]: "path (a # r) p"

    lemma path_append[intro!]:
      assumes "path r p" "path s (target r p)"
      shows "path (r @ s) p"
      using assms by (induct r arbitrary: p) (auto)
    lemma path_append_elim[elim!]:
      assumes "path (r @ s) p"
      obtains "path r p" "path s (target r p)"
      using assms by (induct r arbitrary: p) (auto)

    coinductive run :: "'transition stream ⇒ 'state ⇒ bool" where
      scons[intro!]: "enabled a p ⟹ run r (execute a p) ⟹ run (a ## r) p"

    inductive_cases run_scons_elim[elim!]: "run (a ## r) p"

    lemma run_shift[intro!]:
      assumes "path r p" "run s (target r p)"
      shows "run (r @- s) p"
      using assms by (induct r arbitrary: p) (auto)
    lemma run_shift_elim[elim!]:
      assumes "run (r @- s) p"
      obtains "path r p" "run s (target r p)"
      using assms by (induct r arbitrary: p) (auto)

    lemma run_coinduct[case_names run, coinduct pred: run]:
      assumes "R r p"
      assumes "⋀ a r p. R (a ## r) p ⟹ enabled a p ∧ R r (execute a p)"
      shows "run r p"
      using stream.collapse run.coinduct assms by metis
    lemma run_coinduct_shift[case_names run, consumes 1]:
      assumes "R r p"
      assumes "⋀ r p. R r p ⟹ ∃ s t. r = s @- t ∧ s ≠ [] ∧ path s p ∧ R t (target s p)"
      shows "run r p"
    proof -
      have "∃ s t. r = s @- t ∧ path s p ∧ R t (target s p)" using assms(1) by force
      then show ?thesis using assms(2) by (coinduct) (force elim: path.cases)
    qed
    lemma run_flat_coinduct[case_names run, consumes 1]:
      assumes "R rs p"
      assumes "⋀ r rs p. R (r ## rs) p ⟹ r ≠ [] ∧ path r p ∧ R rs (target r p)"
      shows "run (flat rs) p"
    using assms(1)
    proof (coinduction arbitrary: rs p rule: run_coinduct_shift)
      case (run rs p)
      then show ?case using assms(2) by (metis stream.exhaust flat_Stream)
    qed

    inductive_set reachable :: "'state ⇒ 'state set" for p where
      reflexive[intro!]: "p ∈ reachable p" |
      execute[intro!]: "q ∈ reachable p ⟹ enabled a q ⟹ execute a q ∈ reachable p"

    inductive_cases reachable_elim[elim]: "q ∈ reachable p"

    lemma reachable_execute'[intro]:
      assumes "enabled a p" "q ∈ reachable (execute a p)"
      shows "q ∈ reachable p"
      using assms(2, 1) by induct auto
    lemma reachable_elim'[elim]:
      assumes "q ∈ reachable p"
      obtains "q = p" | a where "enabled a p" "q ∈ reachable (execute a p)"
      using assms by induct auto

    lemma reachable_target[intro]:
      assumes "q ∈ reachable p" "path r q"
      shows "target r q ∈ reachable p"
      using assms by (induct r arbitrary: q) (auto)
    lemma reachable_target_elim[elim]:
      assumes "q ∈ reachable p"
      obtains r
      where "path r p" "q = target r p"
      using assms by induct force+

    lemma reachable_alt_def: "reachable p = {target r p |r. path r p}" by auto

    lemma reachable_trans[trans]: "q ∈ reachable p ⟹ s ∈ reachable q ⟹ s ∈ reachable p" by auto

    lemma reachable_successors[intro!]: "successors p ⊆ reachable p" by auto

    lemma reachable_step: "reachable p = insert p (⋃ (reachable ` successors p))" by auto

  end

  subsection ‹Transition Systems with Initial States›

  locale transition_system_initial =
    transition_system execute enabled
    for execute :: "'transition ⇒ 'state ⇒ 'state"
    and enabled :: "'transition ⇒ 'state ⇒ bool"
    +
    fixes initial :: "'state ⇒ bool"
  begin

    inductive_set nodes :: "'state set" where
      initial[intro]: "initial p ⟹ p ∈ nodes" |
      execute[intro!]: "p ∈ nodes ⟹ enabled a p ⟹ execute a p ∈ nodes"

    lemma nodes_target[intro]:
      assumes "p ∈ nodes" "path r p"
      shows "target r p ∈ nodes"
      using assms by (induct r arbitrary: p) (auto)
    lemma nodes_target_elim[elim]:
      assumes "q ∈ nodes"
      obtains r p
      where "initial p" "path r p" "q = target r p"
      using assms by induct force+

    lemma nodes_alt_def: "nodes = ⋃ (reachable ` Collect initial)" by auto

    lemma nodes_trans[trans]: "p ∈ nodes ⟹ q ∈ reachable p ⟹ q ∈ nodes" by auto

  end

end