Theory NBA_Explicit

section ‹Explicit Nondeterministic Büchi Automata›

theory NBA_Explicit
imports NBA_Algorithms
begin

  datatype ('label, 'state) nbae = nbae
    (alphabete: "'label set")
    (initiale: "'state set")
    (transitione: "('state × 'label × 'state) set")
    (acceptinge: "'state set")

  definition nbae_rel where
    [to_relAPP]: "nbae_rel L S ≡ {(A1, A2).
      (alphabete A1, alphabete A2) ∈ ⟨L⟩ set_rel ∧
      (initiale A1, initiale A2) ∈ ⟨S⟩ set_rel ∧
      (transitione A1, transitione A2) ∈ ⟨S ×r L ×r S⟩ set_rel ∧
      (acceptinge A1, acceptinge A2) ∈ ⟨S⟩ set_rel}"

  lemma nbae_param[param, autoref_rules]:
    "(nbae, nbae) ∈ ⟨L⟩ set_rel → ⟨S⟩ set_rel → ⟨S ×r L ×r S⟩ set_rel →
      ⟨S⟩ set_rel → ⟨L, S⟩ nbae_rel"
    "(alphabete, alphabete) ∈ ⟨L, S⟩ nbae_rel → ⟨L⟩ set_rel"
    "(initiale, initiale) ∈ ⟨L, S⟩ nbae_rel → ⟨S⟩ set_rel"
    "(transitione, transitione) ∈ ⟨L, S⟩ nbae_rel → ⟨S ×r L ×r S⟩ set_rel"
    "(acceptinge, acceptinge) ∈ ⟨L, S⟩ nbae_rel → ⟨S⟩ set_rel"
    unfolding nbae_rel_def by auto

  lemma nbae_rel_id[simp]: "⟨Id, Id⟩ nbae_rel = Id" unfolding nbae_rel_def using nbae.expand by auto
  lemma nbae_rel_comp[simp]: "⟨L1 O L2, S1 O S2⟩ nbae_rel = ⟨L1, S1⟩ nbae_rel O ⟨L2, S2⟩ nbae_rel"
  proof safe
    fix A B
    assume 1: "(A, B) ∈ ⟨L1 O L2, S1 O S2⟩ nbae_rel"
    obtain a b c d where 2:
      "(alphabete A, a) ∈ ⟨L1⟩ set_rel" "(a, alphabete B) ∈ ⟨L2⟩ set_rel"
      "(initiale A, b) ∈ ⟨S1⟩ set_rel" "(b, initiale B) ∈ ⟨S2⟩ set_rel"
      "(transitione A, c) ∈ ⟨S1 ×r L1 ×r S1⟩ set_rel" "(c, transitione B) ∈ ⟨S2 ×r L2 ×r S2⟩ set_rel"
      "(acceptinge A, d) ∈ ⟨S1⟩ set_rel" "(d, acceptinge B) ∈ ⟨S2⟩ set_rel"
      using 1 unfolding nbae_rel_def prod_rel_compp set_rel_compp by auto
    show "(A, B) ∈ ⟨L1, S1⟩ nbae_rel O ⟨L2, S2⟩ nbae_rel"
    proof
      show "(A, nbae a b c d) ∈ ⟨L1, S1⟩ nbae_rel" using 2 unfolding nbae_rel_def by auto
      show "(nbae a b c d, B) ∈ ⟨L2, S2⟩ nbae_rel" using 2 unfolding nbae_rel_def by auto
    qed
  next
    show "(A, C) ∈ ⟨L1 O L2, S1 O S2⟩ nbae_rel"
      if "(A, B) ∈ ⟨L1, S1⟩ nbae_rel" "(B, C) ∈ ⟨L2, S2⟩ nbae_rel" for A B C
      using that unfolding nbae_rel_def prod_rel_compp set_rel_compp by auto
  qed

  (* TODO: why do we need all this setup? can't i_of_rel do the trick? *)
  consts i_nbae_scheme :: "interface ⇒ interface ⇒ interface"

  context
  begin

    interpretation autoref_syn by this

    lemma nbae_scheme_itype[autoref_itype]:
      "nbae ::i ⟨L⟩i i_set →i ⟨S⟩i i_set →i ⟨⟨S, ⟨L, S⟩i i_prod⟩i i_prod⟩i i_set →i ⟨S⟩i i_set →i
        ⟨L, S⟩i i_nbae_scheme"
      "alphabete ::i ⟨L, S⟩i i_nbae_scheme →i ⟨L⟩i i_set"
      "initiale ::i ⟨L, S⟩i i_nbae_scheme →i ⟨S⟩i i_set"
      "transitione ::i ⟨L, S⟩i i_nbae_scheme →i ⟨⟨S, ⟨L, S⟩i i_prod⟩i i_prod⟩i i_set"
      "acceptinge ::i ⟨L, S⟩i i_nbae_scheme →i ⟨S⟩i i_set"
      by auto

  end

  datatype ('label, 'state) nbaei = nbaei
    (alphabetei: "'label list")
    (initialei: "'state list")
    (transitionei: "('state × 'label × 'state) list")
    (acceptingei: "'state list")

  definition nbaei_rel where
    [to_relAPP]: "nbaei_rel L S ≡ {(A1, A2).
      (alphabetei A1, alphabetei A2) ∈ ⟨L⟩ list_rel ∧
      (initialei A1, initialei A2) ∈ ⟨S⟩ list_rel ∧
      (transitionei A1, transitionei A2) ∈ ⟨S ×r L ×r S⟩ list_rel ∧
      (acceptingei A1, acceptingei A2) ∈ ⟨S⟩ list_rel}"

  lemma nbaei_param[param, autoref_rules]:
    "(nbaei, nbaei) ∈ ⟨L⟩ list_rel → ⟨S⟩ list_rel → ⟨S ×r L ×r S⟩ list_rel →
      ⟨S⟩ list_rel → ⟨L, S⟩ nbaei_rel"
    "(alphabetei, alphabetei) ∈ ⟨L, S⟩ nbaei_rel → ⟨L⟩ list_rel"
    "(initialei, initialei) ∈ ⟨L, S⟩ nbaei_rel → ⟨S⟩ list_rel"
    "(transitionei, transitionei) ∈ ⟨L, S⟩ nbaei_rel → ⟨S ×r L ×r S⟩ list_rel"
    "(acceptingei, acceptingei) ∈ ⟨L, S⟩ nbaei_rel → ⟨S⟩ list_rel"
    unfolding nbaei_rel_def by auto

  definition nbaei_nbae_rel where
    [to_relAPP]: "nbaei_nbae_rel L S ≡ {(A1, A2).
      (alphabetei A1, alphabete A2) ∈ ⟨L⟩ list_set_rel ∧
      (initialei A1, initiale A2) ∈ ⟨S⟩ list_set_rel ∧
      (transitionei A1, transitione A2) ∈ ⟨S ×r L ×r S⟩ list_set_rel ∧
      (acceptingei A1, acceptinge A2) ∈ ⟨S⟩ list_set_rel}"

  lemmas [autoref_rel_intf] = REL_INTFI[of nbaei_nbae_rel i_nbae_scheme]

  lemma nbaei_nbae_param[param, autoref_rules]:
    "(nbaei, nbae) ∈ ⟨L⟩ list_set_rel → ⟨S⟩ list_set_rel → ⟨S ×r L ×r S⟩ list_set_rel →
      ⟨S⟩ list_set_rel → ⟨L, S⟩ nbaei_nbae_rel"
    "(alphabetei, alphabete) ∈ ⟨L, S⟩ nbaei_nbae_rel → ⟨L⟩ list_set_rel"
    "(initialei, initiale) ∈ ⟨L, S⟩ nbaei_nbae_rel → ⟨S⟩ list_set_rel"
    "(transitionei, transitione) ∈ ⟨L, S⟩ nbaei_nbae_rel → ⟨S ×r L ×r S⟩ list_set_rel"
    "(acceptingei, acceptinge) ∈ ⟨L, S⟩ nbaei_nbae_rel → ⟨S⟩ list_set_rel"
    unfolding nbaei_nbae_rel_def by auto

  definition nbaei_nbae where
    "nbaei_nbae A ≡ nbae (set (alphabetei A)) (set (initialei A))
      (set (transitionei A)) (set (acceptingei A))"

  lemma nbaei_nbae_id_param[param]: "(nbaei_nbae, id) ∈ ⟨L, S⟩ nbaei_nbae_rel → ⟨L, S⟩ nbae_rel"
  proof
    fix Ai A
    assume 1: "(Ai, A) ∈ ⟨L, S⟩ nbaei_nbae_rel"
    have 2: "nbaei_nbae Ai = nbae (set (alphabetei Ai)) (set (initialei Ai))
      (set (transitionei Ai)) (set (acceptingei Ai))" unfolding nbaei_nbae_def by rule
    have 3: "id A = nbae (id (alphabete A)) (id (initiale A))
      (id (transitione A)) (id (acceptinge A))" by simp
    show "(nbaei_nbae Ai, id A) ∈ ⟨L, S⟩ nbae_rel" unfolding 2 3 using 1 by parametricity
  qed

  abbreviation "transitions L S s ≡ ⋃ a ∈ L. ⋃ p ∈ S. {p} × {a} × s a p"
  abbreviation "succs T a p ≡ (T `` {p}) `` {a}"

  definition nba_nbae where "nba_nbae A ≡ nbae (alphabet A) (initial A)
    (transitions (alphabet A) (nodes A) (transition A)) (Set.filter (accepting A) (nodes A))"
  definition nbae_nba where "nbae_nba A ≡ nba (alphabete A) (initiale A)
    (succs (transitione A)) (λ p. p ∈ acceptinge A)"

  lemma nba_nbae_param[param]: "(nba_nbae, nba_nbae) ∈ ⟨L, S⟩ nba_rel → ⟨L, S⟩ nbae_rel"
    unfolding nba_nbae_def by parametricity
  lemma nbae_nba_param[param]:
    assumes "bijective L" "bijective S"
    shows "(nbae_nba, nbae_nba) ∈ ⟨L, S⟩ nbae_rel → ⟨L, S⟩ nba_rel"
    using assms assms(2)[unfolded bijective_alt] unfolding nbae_nba_def by parametricity auto

  lemma nbae_nba_nba_nbae_param[param]:
    "((nbae_nba ∘ nba_nbae) A, id A) ∈ ⟨Id_on (alphabet A), Id_on (nodes A)⟩ nba_rel"
  proof -
    have "(nbae_nba ∘ nba_nbae) A = nba (alphabet A) (initial A)
      (succs (transitions (alphabet A) (nodes A) (transition A))) (λ p. p ∈ Set.filter (accepting A) (nodes A))"
      unfolding nbae_nba_def nba_nbae_def by simp
    also have "(…, nba (alphabet A) (initial A) (transition A) (accepting A)) ∈
      ⟨Id_on (alphabet A), Id_on (nodes A)⟩ nba_rel"
      using nba_rel_eq by parametricity auto
    also have  "nba (alphabet A) (initial A) (transition A) (accepting A) = id A" by simp
    finally show ?thesis by this
  qed

  definition nbaei_nba_rel where
    [to_relAPP]: "nbaei_nba_rel L S ≡ {(Ae, A). (nbae_nba (nbaei_nbae Ae), A) ∈ ⟨L, S⟩ nba_rel}"
  lemma nbaei_nba_id[param]: "(nbae_nba ∘ nbaei_nbae, id) ∈ ⟨L, S⟩ nbaei_nba_rel → ⟨L, S⟩ nba_rel"
    unfolding nbaei_nba_rel_def by auto

  schematic_goal nbae_nba_impl:
    assumes [autoref_rules]: "(leq, HOL.eq) ∈ L → L → bool_rel"
    assumes [autoref_rules]: "(seq, HOL.eq) ∈ S → S → bool_rel"
    shows "(?f, nbae_nba) ∈ ⟨L, S⟩ nbaei_nbae_rel → ⟨L, S⟩ nbai_nba_rel"
    unfolding nbae_nba_def by autoref
  concrete_definition nbae_nba_impl uses nbae_nba_impl
  lemma nbae_nba_impl_refine[autoref_rules]:
    assumes "GEN_OP leq HOL.eq (L → L → bool_rel)"
    assumes "GEN_OP seq HOL.eq (S → S → bool_rel)"
    shows "(nbae_nba_impl leq seq, nbae_nba) ∈ ⟨L, S⟩ nbaei_nbae_rel → ⟨L, S⟩ nbai_nba_rel"
    using nbae_nba_impl.refine assms unfolding autoref_tag_defs by this

end