Theory NBA

section ‹Nondeterministic Büchi Automata›

theory NBA
imports "../Nondeterministic"
begin

  datatype ('label, 'state) nba = nba
    (alphabet: "'label set")
    (initial: "'state set")
    (transition: "'label ⇒ 'state ⇒ 'state set")
    (accepting: "'state pred")

  global_interpretation nba: automaton nba alphabet initial transition accepting
    defines path = nba.path and run = nba.run and reachable = nba.reachable and nodes = nba.nodes
    by unfold_locales auto
  global_interpretation nba: automaton_run nba alphabet initial transition accepting "λ P w r p. infs P (p ## r)"
    defines language = nba.language
    by standard

  abbreviation target where "target ≡ nba.target"
  abbreviation states where "states ≡ nba.states"
  abbreviation trace where "trace ≡ nba.trace"
  abbreviation successors where "successors ≡ nba.successors TYPE('label)"

  instantiation nba :: (type, type) order
  begin

    definition less_eq_nba :: "('a, 'b) nba ⇒ ('a, 'b) nba ⇒ bool" where
      "A ≤ B ≡ alphabet A ≤ alphabet B ∧ initial A ≤ initial B ∧
        transition A ≤ transition B ∧ accepting A ≤ accepting B"
    definition less_nba :: "('a, 'b) nba ⇒ ('a, 'b) nba ⇒ bool" where
      "less_nba A B ≡ A ≤ B ∧ A ≠ B"

    instance by (intro_classes) (auto simp: less_eq_nba_def less_nba_def nba.expand)

  end

  lemma nodes_mono: "mono nodes"
  proof
    fix A B :: "('label, 'state) nba"
    assume 1: "A ≤ B"
    have 2: "alphabet A ⊆ alphabet B" using 1 unfolding less_eq_nba_def by auto
    have 3: "initial A ⊆ initial B" using 1 unfolding less_eq_nba_def by auto
    have 4: "transition A a p ⊆ transition B a p" for a p using 1 unfolding less_eq_nba_def le_fun_def by auto
    have 5: "p ∈ nodes B" if "p ∈ nodes A" for p using that 2 3 4 by induct fastforce+
    show "nodes A ⊆ nodes B" using 5 by auto
  qed

  lemma language_mono: "mono language"
  proof
    fix A B :: "('label, 'state) nba"
    assume 1: "A ≤ B"
    have 2: "alphabet A ⊆ alphabet B" using 1 unfolding less_eq_nba_def by auto
    have 3: "initial A ⊆ initial B" using 1 unfolding less_eq_nba_def by auto
    have 4: "transition A a p ⊆ transition B a p" for a p using 1 unfolding less_eq_nba_def le_fun_def by auto
    have 5: "accepting A p ⟹ accepting B p" for p using 1 unfolding less_eq_nba_def by auto
    have 6: "run B wr p" if "run A wr p" for wr p using that 2 4 by coinduct auto
    have 7: "infs (accepting B) w" if "infs (accepting A) w" for w using infs_mono that 5 by metis
    show "language A ⊆ language B" using 3 6 7 by blast
  qed

  lemma simulation_language:
    assumes "alphabet A ⊆ alphabet B"
    assumes "⋀ p. p ∈ initial A ⟹ ∃ q ∈ initial B. (p, q) ∈ R"
    assumes "⋀ a p p' q. p' ∈ transition A a p ⟹ (p, q) ∈ R ⟹ ∃ q' ∈ transition B a q. (p', q') ∈ R"
    assumes "⋀ p q. (p, q) ∈ R ⟹ accepting A p ⟹ accepting B q"
    shows "language A ⊆ language B"
  proof
    fix w
    assume 1: "w ∈ language A"
    obtain r p where 2: "p ∈ initial A" "run A (w ||| r) p" "infs (accepting A) (p ## r)" using 1 by rule
    define P where "P n q ≡ (target (stake n (w ||| r)) p, q) ∈ R" for n q
    obtain q where 3: "q ∈ initial B" "(p, q) ∈ R" using assms(2) 2(1) by auto
    obtain ws where 4:
      "run B ws q" "⋀ i. P (0 + i) (target (stake i ws) q)" "⋀ i. fst (ws !! i) = w !! (0 + i)"
    proof (rule nba.invariant_run_index)
      have "stake k (w ||| r) @- (w !! k, target (stake (Suc k) (w ||| r)) p) ##
        sdrop (Suc k) (w ||| r) = w ||| r" for k
        by (metis id_stake_snth_sdrop snth_szip sscan_snth szip_smap_snd nba.trace_alt_def)
      also have "run A … p" using 2(2) by this
      finally show "∃ a. (fst a ∈ alphabet B ∧ snd a ∈ transition B (fst a) q) ∧
        P (Suc n) (snd a) ∧ fst a = w !! n" if "P n q" for n q
        using assms(1, 3) that unfolding P_def by fastforce
      show "P 0 q" unfolding P_def using 3(2) by auto
    qed rule
    obtain s where 5: "ws = w ||| s" using 4(3) by (metis add.left_neutral eqI_snth snth_smap szip_smap)
    show "w ∈ language B"
    proof
      show "q ∈ initial B" using 3(1) by this
      show "run B (w ||| s) q" using 4(1) unfolding 5 by this
      have 6: "(λ a b. (a, b) ∈ R) ≤ (λ a b. accepting A a ⟶ accepting B b)" using assms(4) by auto
      have 7: "stream_all2 (λ p q. (p, q) ∈ R) (trace (w ||| r) p) (trace (w ||| s) q)"
        using 4(2) unfolding P_def 5 by (simp add: stream_rel_snth del: stake.simps(2))
      have 8: "stream_all2 (λ a b. accepting A a ⟶ accepting B b) r s"
        using stream.rel_mono 6 7 unfolding nba.trace_alt_def by auto
      show "infs (accepting B) (q ## s)" using infs_mono_strong 8 2(3) by simp
    qed
  qed

end