Theory NBA_Implement

section ‹Implementation of Nondeterministic Büchi Automata›

theory NBA_Implement
imports
  "NBA_Refine"
  "../../Basic/Implement"
begin

  consts i_nba_scheme :: "interface ⇒ interface ⇒ interface"

  context
  begin

    interpretation autoref_syn by this

    lemma nba_scheme_itype[autoref_itype]:
      "nba ::i ⟨L⟩i i_set →i ⟨S⟩i i_set →i (L →i S →i ⟨S⟩i i_set) →i ⟨S⟩i i_set →i
        ⟨L, S⟩i i_nba_scheme"
      "alphabet ::i ⟨L, S⟩i i_nba_scheme →i ⟨L⟩i i_set"
      "initial ::i ⟨L, S⟩i i_nba_scheme →i ⟨S⟩i i_set"
      "transition ::i ⟨L, S⟩i i_nba_scheme →i L →i S →i ⟨S⟩i i_set"
      "accepting ::i ⟨L, S⟩i i_nba_scheme →i ⟨S⟩i i_set"
      by auto

  end

  datatype ('label, 'state) nbai = nbai
    (alphabeti: "'label list")
    (initiali: "'state list")
    (transitioni: "'label ⇒ 'state ⇒ 'state list")
    (acceptingi: "'state ⇒ bool")

  definition nbai_rel :: "('label1 × 'label2) set ⇒ ('state1 × 'state2) set ⇒
    (('label1, 'state1) nbai × ('label2, 'state2) nbai) set" where
    [to_relAPP]: "nbai_rel L S ≡ {(A1, A2).
      (alphabeti A1, alphabeti A2) ∈ ⟨L⟩ list_rel ∧
      (initiali A1, initiali A2) ∈ ⟨S⟩ list_rel ∧
      (transitioni A1, transitioni A2) ∈ L → S → ⟨S⟩ list_rel ∧
      (acceptingi A1, acceptingi A2) ∈ S → bool_rel}"

  lemma nbai_param[param, autoref_rules]:
    "(nbai, nbai) ∈ ⟨L⟩ list_rel → ⟨S⟩ list_rel → (L → S → ⟨S⟩ list_rel) →
      (S → bool_rel) → ⟨L, S⟩ nbai_rel"
    "(alphabeti, alphabeti) ∈ ⟨L, S⟩ nbai_rel → ⟨L⟩ list_rel"
    "(initiali, initiali) ∈ ⟨L, S⟩ nbai_rel → ⟨S⟩ list_rel"
    "(transitioni, transitioni) ∈ ⟨L, S⟩ nbai_rel → L → S → ⟨S⟩ list_rel"
    "(acceptingi, acceptingi) ∈ ⟨L, S⟩ nbai_rel → (S → bool_rel)"
    unfolding nbai_rel_def fun_rel_def by auto

  definition nbai_nba_rel :: "('label1 × 'label2) set ⇒ ('state1 × 'state2) set ⇒
    (('label1, 'state1) nbai × ('label2, 'state2) nba) set" where
    [to_relAPP]: "nbai_nba_rel L S ≡ {(A1, A2).
      (alphabeti A1, alphabet A2) ∈ ⟨L⟩ list_set_rel ∧
      (initiali A1, initial A2) ∈ ⟨S⟩ list_set_rel ∧
      (transitioni A1, transition A2) ∈ L → S → ⟨S⟩ list_set_rel ∧
      (acceptingi A1, accepting A2) ∈ S → bool_rel}"

  lemmas [autoref_rel_intf] = REL_INTFI[of nbai_nba_rel i_nba_scheme]

  (* TODO: why is there a warning? *)
  lemma nbai_nba_param[param, autoref_rules]:
    "(nbai, nba) ∈ ⟨L⟩ list_set_rel → ⟨S⟩ list_set_rel → (L → S → ⟨S⟩ list_set_rel) →
      (S → bool_rel) → ⟨L, S⟩ nbai_nba_rel"
    "(alphabeti, alphabet) ∈ ⟨L, S⟩ nbai_nba_rel → ⟨L⟩ list_set_rel"
    "(initiali, initial) ∈ ⟨L, S⟩ nbai_nba_rel → ⟨S⟩ list_set_rel"
    "(transitioni, transition) ∈ ⟨L, S⟩ nbai_nba_rel → L → S → ⟨S⟩ list_set_rel"
    "(acceptingi, accepting) ∈ ⟨L, S⟩ nbai_nba_rel → S → bool_rel"
    unfolding nbai_nba_rel_def fun_rel_def by auto

  definition nbai_nba :: "('label, 'state) nbai ⇒ ('label, 'state) nba" where
    "nbai_nba A ≡ nba (set (alphabeti A)) (set (initiali A)) (λ a p. set (transitioni A a p)) (acceptingi A)"
  definition nbai_invar :: "('label, 'state) nbai ⇒ bool" where
    "nbai_invar A ≡ distinct (alphabeti A) ∧ distinct (initiali A) ∧ (∀ a p. distinct (transitioni A a p))"

  lemma nbai_nba_id_param[param]: "(nbai_nba, id) ∈ ⟨L, S⟩ nbai_nba_rel → ⟨L, S⟩ nba_rel"
  proof
    fix Ai A
    assume 1: "(Ai, A) ∈ ⟨L, S⟩ nbai_nba_rel"
    have 2: "nbai_nba Ai = nba (set (alphabeti Ai)) (set (initiali Ai))
      (λ a p. set (transitioni Ai a p)) (acceptingi Ai)" unfolding nbai_nba_def by rule
    have 3: "id A = nba (id (alphabet A)) (id (initial A))
      (λ a p. id (transition A a p)) (accepting A)" by simp
    show "(nbai_nba Ai, id A) ∈ ⟨L, S⟩ nba_rel" unfolding 2 3 using 1 by parametricity
  qed

  lemma nbai_nba_br: "⟨Id, Id⟩ nbai_nba_rel = br nbai_nba nbai_invar"
  proof safe
    show "(A, B) ∈ ⟨Id, Id⟩ nbai_nba_rel" if "(A, B) ∈ br nbai_nba nbai_invar"
      for A and B :: "('a, 'b) nba"
      using that unfolding nbai_nba_rel_def nbai_nba_def nbai_invar_def
      by (auto simp: in_br_conv list_set_rel_def)
    show "(A, B) ∈ br nbai_nba nbai_invar" if "(A, B) ∈ ⟨Id, Id⟩ nbai_nba_rel"
      for A and B :: "('a, 'b) nba"
    proof -
      have 1: "(nbai_nba A, id B) ∈ ⟨Id, Id⟩ nba_rel" using that by parametricity
      have 2: "nbai_invar A"
        using nbai_nba_param(2 - 5)[param_fo, OF that]
        by (auto simp: in_br_conv list_set_rel_def nbai_invar_def)
      show ?thesis using 1 2 unfolding in_br_conv by auto
    qed
  qed

end