Theory Transition_System_Construction

section ‹Constructing Paths and Runs in Transition Systems›

theory Transition_System_Construction
imports
  "../Basic/Sequence_LTL"
  "Transition_System"
begin

  context transition_system
  begin

    lemma invariant_run:
      assumes "P p" "⋀ p. P p ⟹ ∃ a. enabled a p ∧ P (execute a p) ∧ Q p a"
      obtains r
      where "run r p" "pred_stream P (p ## trace r p)" "stream_all2 Q (p ## trace r p) r"
    proof -
      obtain f where 1: "enabled (f p) p" "P (execute (f p) p)" "Q p (f p)" if "P p" for p using assms(2) by metis
      let ?g = "λ p. execute (f p) p"
      let ?r = "λ p. smap f (siterate ?g p)"
      show ?thesis
      proof
        show "run (?r p) p" using assms(1) 1 by (coinduction arbitrary: p) (auto)
        show "pred_stream P (p ## trace (?r p) p)" using assms(1) 1 by (coinduction arbitrary: p) (auto)
        show "stream_all2 Q (p ## trace (?r p) p) (?r p)" using assms(1) 1 by (coinduction arbitrary: p) (auto)
      qed
    qed
    lemma recurring_condition:
      assumes "P p" "⋀ p. P p ⟹ ∃ r. r ≠ [] ∧ path r p ∧ P (target r p)"
      obtains r
      where "run r p" "infs P (p ## trace r p)"
    proof -
      obtain f where 1: "f p ≠ []" "path (f p) p" "P (target (f p) p)" if "P p" for p using assms(2) by metis
      let ?g = "λ p. target (f p) p"
      let ?r = "λ p. flat (smap f (siterate ?g p))"
      have 2: "?r p = f p @- ?r (?g p)" if "P p" for p using that 1(1) by (simp add: flat_unfold)
      show ?thesis
      proof
        show "run (?r p) p" using assms(1) 1 2 by (coinduction arbitrary: p rule: run_coinduct_shift) (blast)
        show "infs P (p ## trace (?r p) p)" using assms(1) 1 2 by (coinduction arbitrary: p rule: infs_sscan_coinduct) (blast)
      qed
    qed

    lemma invariant_run_index:
      assumes "P n p" "⋀ n p. P n p ⟹ ∃ a. enabled a p ∧ P (Suc n) (execute a p) ∧ Q n p a"
      obtains r
      where
        "run r p"
        "⋀ i. P (n + i) (target (stake i r) p)"
        "⋀ i. Q (n + i) (target (stake i r) p) (r !! i)"
    proof -
      define s where "s ≡ (n, p)"
      have 1: "case_prod P s" using assms(1) unfolding s_def by auto
      obtain f where 2:
        "⋀ n p. P n p ⟹ enabled (f n p) p"
        "⋀ n p. P n p ⟹ P (Suc n) (execute (f n p) p)"
        "⋀ n p. P n p ⟹ Q n p (f n p)"
        using assms(2) by metis
      define g where "g ≡ λ (n, p). (Suc n, execute (f n p) p)"

      let ?r = "smap (case_prod f) (siterate g s)"

      have 3: "run ?r (snd s)" using 1 2(1, 2) unfolding g_def by (coinduction arbitrary: s) (auto)
      have 4: "case_prod P (compow k g s)" for k using 1 2(2) unfolding g_def by (induct k) (auto)
      have 5: "case_prod Q (compow k g s) (?r !! k)" for k using 2(3) 4 by (simp add: case_prod_beta)

      have 6: "compow k g (n, p) = (n + k, target (stake k ?r) p)" for k
        unfolding s_def g_def by (induct k) (auto simp add: stake_Suc simp del: stake.simps(2))

      show ?thesis using that 3 4 5 unfolding s_def 6 by simp
    qed

    lemma koenig:
      assumes "infinite (reachable p)"
      assumes "⋀ q. q ∈ reachable p ⟹ finite (successors q)"
      obtains r
      where "run r p"
    proof (rule invariant_run[where ?P = "λ q. q ∈ reachable p ∧ infinite (reachable q)"])
      show "p ∈ reachable p ∧ infinite (reachable p)" using assms(1) by auto
    next
      fix q
      assume 1: "q ∈ reachable p ∧ infinite (reachable q)"
      have 2: "finite (successors q)" using assms(2) 1 by auto
      have 3: "infinite (insert q (⋃(reachable ` (successors q))))" using reachable_step 1 by metis
      obtain s where 4: "s ∈ successors q" "infinite (reachable s)" using 2 3 by auto
      show "∃ a. enabled a q ∧ (execute a q ∈ reachable p ∧ infinite (reachable (execute a q))) ∧ True"
        using 1 4 by auto
    qed

  end

end