Theory Transition_Systems_and_Automata.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