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 Li i_set i Si i_set i (L i S i Si i_set) i Si i_set i
        L, Si i_nba_scheme"
      "alphabet ::i L, Si i_nba_scheme i Li i_set"
      "initial ::i L, Si i_nba_scheme i Si i_set"
      "transition ::i L, Si i_nba_scheme i L i S i Si i_set"
      "accepting ::i L, Si i_nba_scheme i Si 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