Theory NGBA_Implement

section ‹Implementation of Nondeterministic Generalized Büchi Automata›

theory NGBA_Implement
imports
  "NGBA_Refine"
  "../../Basic/Implement"
begin

  consts i_ngba_scheme :: "interface ⇒ interface ⇒ interface"

  context
  begin

    interpretation autoref_syn by this

    lemma ngba_scheme_itype[autoref_itype]:
      "ngba ::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 i_list →i
        ⟨L, S⟩i i_ngba_scheme"
      "alphabet ::i ⟨L, S⟩i i_ngba_scheme →i ⟨L⟩i i_set"
      "initial ::i ⟨L, S⟩i i_ngba_scheme →i ⟨S⟩i i_set"
      "transition ::i ⟨L, S⟩i i_ngba_scheme →i L →i S →i ⟨S⟩i i_set"
      "accepting ::i ⟨L, S⟩i i_ngba_scheme →i ⟨⟨S⟩i i_set⟩i i_list"
      by auto

  end

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

  definition ngbai_rel :: "('label1 × 'label2) set ⇒ ('state1 × 'state2) set ⇒
    (('label1, 'state1) ngbai × ('label2, 'state2) ngbai) set" where
    [to_relAPP]: "ngbai_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⟩ list_rel}"

  lemma ngbai_param[param]:
    "(ngbai, ngbai) ∈ ⟨L⟩ list_rel → ⟨S⟩ list_rel → (L → S → ⟨S⟩ list_rel) →
      ⟨S → bool_rel⟩ list_rel → ⟨L, S⟩ ngbai_rel"
    "(alphabeti, alphabeti) ∈ ⟨L, S⟩ ngbai_rel → ⟨L⟩ list_rel"
    "(initiali, initiali) ∈ ⟨L, S⟩ ngbai_rel → ⟨S⟩ list_rel"
    "(transitioni, transitioni) ∈ ⟨L, S⟩ ngbai_rel → L → S → ⟨S⟩ list_rel"
    "(acceptingi, acceptingi) ∈ ⟨L, S⟩ ngbai_rel → ⟨S → bool_rel⟩ list_rel"
    unfolding ngbai_rel_def fun_rel_def by auto

  definition ngbai_ngba_rel :: "('label1 × 'label2) set ⇒ ('state1 × 'state2) set ⇒
    (('label1, 'state1) ngbai × ('label2, 'state2) ngba) set" where
    [to_relAPP]: "ngbai_ngba_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⟩ list_rel}"

  lemmas [autoref_rel_intf] = REL_INTFI[of ngbai_ngba_rel i_ngba_scheme]

  lemma ngbai_ngba_param[param, autoref_rules]:
    "(ngbai, ngba) ∈ ⟨L⟩ list_set_rel → ⟨S⟩ list_set_rel → (L → S → ⟨S⟩ list_set_rel) →
      ⟨S → bool_rel⟩ list_rel → ⟨L, S⟩ ngbai_ngba_rel"
    "(alphabeti, alphabet) ∈ ⟨L, S⟩ ngbai_ngba_rel → ⟨L⟩ list_set_rel"
    "(initiali, initial) ∈ ⟨L, S⟩ ngbai_ngba_rel → ⟨S⟩ list_set_rel"
    "(transitioni, transition) ∈ ⟨L, S⟩ ngbai_ngba_rel → L → S → ⟨S⟩ list_set_rel"
    "(acceptingi, accepting) ∈ ⟨L, S⟩ ngbai_ngba_rel → ⟨S → bool_rel⟩ list_rel"
    unfolding ngbai_ngba_rel_def fun_rel_def by auto

  definition ngbai_ngba :: "('label, 'state) ngbai ⇒ ('label, 'state) ngba" where
    "ngbai_ngba A ≡ ngba (set (alphabeti A)) (set (initiali A)) (λ a p. set (transitioni A a p)) (acceptingi A)"
  definition ngbai_invar :: "('label, 'state) ngbai ⇒ bool" where
    "ngbai_invar A ≡ distinct (alphabeti A) ∧ distinct (initiali A) ∧ (∀ a p. distinct (transitioni A a p))"

  lemma ngbai_ngba_id_param[param]: "(ngbai_ngba, id) ∈ ⟨L, S⟩ ngbai_ngba_rel → ⟨L, S⟩ ngba_rel"
  proof
    fix Ai A
    assume 1: "(Ai, A) ∈ ⟨L, S⟩ ngbai_ngba_rel"
    have 2: "ngbai_ngba Ai = ngba (set (alphabeti Ai)) (set (initiali Ai))
      (λ a p. set (transitioni Ai a p)) (acceptingi Ai)" unfolding ngbai_ngba_def by rule
    have 3: "id A = ngba (id (alphabet A)) (id (initial A))
      (λ a p. id (transition A a p)) (accepting A)" by simp
    show "(ngbai_ngba Ai, id A) ∈ ⟨L, S⟩ ngba_rel" unfolding 2 3 using 1 by parametricity
  qed

  lemma ngbai_ngba_br: "⟨Id, Id⟩ ngbai_ngba_rel = br ngbai_ngba ngbai_invar"
  proof safe
    show "(A, B) ∈ ⟨Id, Id⟩ ngbai_ngba_rel" if "(A, B) ∈ br ngbai_ngba ngbai_invar"
      for A and B :: "('a, 'b) ngba"
      using that unfolding ngbai_ngba_rel_def ngbai_ngba_def ngbai_invar_def
      by (auto simp: in_br_conv list_set_rel_def)
    show "(A, B) ∈ br ngbai_ngba ngbai_invar" if "(A, B) ∈ ⟨Id, Id⟩ ngbai_ngba_rel"
      for A and B :: "('a, 'b) ngba"
    proof -
      have 1: "(ngbai_ngba A, id B) ∈ ⟨Id, Id⟩ ngba_rel" using that by parametricity
      have 2: "ngbai_invar A"
        using ngbai_ngba_param(2 - 5)[param_fo, OF that]
        by (auto simp: in_br_conv list_set_rel_def ngbai_invar_def)
      show ?thesis using 1 2 unfolding in_br_conv by auto
    qed
  qed

end