Theory DRA_Implement

section ‹Implementation of Deterministic Rabin Automata›

theory DRA_Implement

  datatype ('label, 'state) drai = drai
    (alphabeti: "'label list")
    (initiali: "'state")
    (transitioni: "'label  'state  'state")
    (conditioni: "'state rabin gen")

  definition drai_rel :: "('label1 × 'label2) set  ('state1 × 'state2) set 
    (('label1, 'state1) drai × ('label2, 'state2) drai) set" where
    [to_relAPP]: "drai_rel L S  {(A1, A2).
      (alphabeti A1, alphabeti A2)  L list_rel 
      (initiali A1, initiali A2)  S 
      (transitioni A1, transitioni A2)  L  S  S 
      (conditioni A1, conditioni A2)  rabin_rel S list_rel}"

  lemma drai_param[param]:
    "(drai, drai)  L list_rel  S  (L  S  S) 
      rabin_rel S list_rel  L, S drai_rel"
    "(alphabeti, alphabeti)  L, S drai_rel  L list_rel"
    "(initiali, initiali)  L, S drai_rel  S"
    "(transitioni, transitioni)  L, S drai_rel  L  S  S"
    "(conditioni, conditioni)  L, S drai_rel  rabin_rel S list_rel"
    unfolding drai_rel_def fun_rel_def by auto

  definition drai_dra_rel :: "('label1 × 'label2) set  ('state1 × 'state2) set 
    (('label1, 'state1) drai × ('label2, 'state2) dra) set" where
    [to_relAPP]: "drai_dra_rel L S  {(A1, A2).
      (alphabeti A1, alphabet A2)  L list_set_rel 
      (initiali A1, initial A2)  S 
      (transitioni A1, transition A2)  L  S  S 
      (conditioni A1, condition A2)  rabin_rel S list_rel}"

  lemma drai_dra_param[param, autoref_rules]:
    "(drai, dra)  L list_set_rel  S  (L  S  S) 
      rabin_rel S list_rel  L, S drai_dra_rel"
    "(alphabeti, alphabet)  L, S drai_dra_rel  L list_set_rel"
    "(initiali, initial)  L, S drai_dra_rel  S"
    "(transitioni, transition)  L, S drai_dra_rel  L  S  S"
    "(conditioni, condition)  L, S drai_dra_rel  rabin_rel S list_rel"
    unfolding drai_dra_rel_def fun_rel_def by auto

  definition drai_dra :: "('label, 'state) drai  ('label, 'state) dra" where
    "drai_dra A  dra (set (alphabeti A)) (initiali A) (transitioni A) (conditioni A)"
  definition drai_invar :: "('label, 'state) drai  bool" where
    "drai_invar A  distinct (alphabeti A)"

  lemma drai_dra_id_param[param]: "(drai_dra, id)  L, S drai_dra_rel  L, S dra_rel"
    fix Ai A
    assume 1: "(Ai, A)  L, S drai_dra_rel"
    have 2: "drai_dra Ai = dra (set (alphabeti Ai)) (initiali Ai) (transitioni Ai) (conditioni Ai)"
      unfolding drai_dra_def by rule
    have 3: "id A = dra (id (alphabet A)) (initial A) (transition A) (condition A)" by simp
    show "(drai_dra Ai, id A)  L, S dra_rel" unfolding 2 3 using 1 by parametricity

  lemma drai_dra_br: "Id, Id drai_dra_rel = br drai_dra drai_invar"
  proof safe
    show "(A, B)  Id, Id drai_dra_rel" if "(A, B)  br drai_dra drai_invar"
      for A and B :: "('a, 'b) dra"
      using that unfolding drai_dra_rel_def drai_dra_def drai_invar_def
      by (auto simp: in_br_conv list_set_rel_def)
    show "(A, B)  br drai_dra drai_invar" if "(A, B)  Id, Id drai_dra_rel"
      for A and B :: "('a, 'b) dra"
    proof -
      have 1: "(drai_dra A, id B)  Id, Id dra_rel" using that by parametricity
      have 2: "drai_invar A"
        using drai_dra_param(2 - 5)[param_fo, OF that]
        by (auto simp: in_br_conv list_set_rel_def drai_invar_def)
      show ?thesis using 1 2 unfolding in_br_conv by auto