Theory DRA_Explicit

section ‹Explicit Deterministic Rabin Automata›

theory DRA_Explicit
imports DRA_Nodes
begin

  datatype ('label, 'state) drae = drae
    (alphabete: "'label set")
    (initiale: "'state")
    (transitione: "('state × 'label × 'state) set")
    (conditione: "('state set × 'state set) list")

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

  lemma drae_param[param, autoref_rules]:
    "(drae, drae) ∈ ⟨L⟩ set_rel → S → ⟨S ×r L ×r S⟩ set_rel →
      ⟨⟨S⟩ set_rel ×r ⟨S⟩ set_rel⟩ list_rel → ⟨L, S⟩ drae_rel"
    "(alphabete, alphabete) ∈ ⟨L, S⟩ drae_rel → ⟨L⟩ set_rel"
    "(initiale, initiale) ∈ ⟨L, S⟩ drae_rel → S"
    "(transitione, transitione) ∈ ⟨L, S⟩ drae_rel → ⟨S ×r L ×r S⟩ set_rel"
    "(conditione, conditione) ∈ ⟨L, S⟩ drae_rel → ⟨⟨S⟩ set_rel ×r ⟨S⟩ set_rel⟩ list_rel"
    unfolding drae_rel_def by auto

  lemma drae_rel_id[simp]: "⟨Id, Id⟩ drae_rel = Id" unfolding drae_rel_def using drae.expand by auto
  lemma drae_rel_comp[simp]: "⟨L1 O L2, S1 O S2⟩ drae_rel = ⟨L1, S1⟩ drae_rel O ⟨L2, S2⟩ drae_rel"
  proof safe
    fix A B
    assume 1: "(A, B) ∈ ⟨L1 O L2, S1 O S2⟩ drae_rel"
    obtain a b c d where 2:
      "(alphabete A, a) ∈ ⟨L1⟩ set_rel" "(a, alphabete B) ∈ ⟨L2⟩ set_rel"
      "(initiale A, b) ∈ S1" "(b, initiale B) ∈ S2"
      "(transitione A, c) ∈ ⟨S1 ×r L1 ×r S1⟩ set_rel" "(c, transitione B) ∈ ⟨S2 ×r L2 ×r S2⟩ set_rel"
      "(conditione A, d) ∈ ⟨⟨S1⟩ set_rel ×r ⟨S1⟩ set_rel⟩ list_rel"
      "(d, conditione B) ∈ ⟨⟨S2⟩ set_rel ×r ⟨S2⟩ set_rel⟩ list_rel"
      using 1 unfolding drae_rel_def prod_rel_compp set_rel_compp by auto
    show "(A, B) ∈ ⟨L1, S1⟩ drae_rel O ⟨L2, S2⟩ drae_rel"
    proof
      show "(A, drae a b c d) ∈ ⟨L1, S1⟩ drae_rel" using 2 unfolding drae_rel_def by auto
      show "(drae a b c d, B) ∈ ⟨L2, S2⟩ drae_rel" using 2 unfolding drae_rel_def by auto
    qed
  next
    show "(A, C) ∈ ⟨L1 O L2, S1 O S2⟩ drae_rel"
      if "(A, B) ∈ ⟨L1, S1⟩ drae_rel" "(B, C) ∈ ⟨L2, S2⟩ drae_rel" for A B C
      using that unfolding drae_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_drae_scheme :: "interface ⇒ interface ⇒ interface"

  context
  begin

    interpretation autoref_syn by this

    lemma drae_scheme_itype[autoref_itype]:
      "drae ::i ⟨L⟩i i_set →i S →i ⟨⟨S, ⟨L, S⟩i i_prod⟩i i_prod⟩i i_set →i
        ⟨⟨⟨S⟩i i_set, ⟨S⟩i i_set⟩i i_prod⟩i i_list →i ⟨L, S⟩i i_drae_scheme"
      "alphabete ::i ⟨L, S⟩i i_drae_scheme →i ⟨L⟩i i_set"
      "initiale ::i ⟨L, S⟩i i_drae_scheme →i S"
      "transitione ::i ⟨L, S⟩i i_drae_scheme →i ⟨⟨S, ⟨L, S⟩i i_prod⟩i i_prod⟩i i_set"
      "conditione ::i ⟨L, S⟩i i_drae_scheme →i ⟨⟨⟨S⟩i i_set, ⟨S⟩i i_set⟩i i_prod⟩i i_list"
      by auto

  end

  datatype ('label, 'state) draei = draei
    (alphabetei: "'label list")
    (initialei: "'state")
    (transitionei: "('state × 'label × 'state) list")
    (conditionei: "('state list × 'state list) list")

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

  lemma draei_param[param, autoref_rules]:
    "(draei, draei) ∈ ⟨L⟩ list_rel → S → ⟨S ×r L ×r S⟩ list_rel →
      ⟨⟨S⟩ list_rel ×r ⟨S⟩ list_rel⟩ list_rel → ⟨L, S⟩ draei_rel"
    "(alphabetei, alphabetei) ∈ ⟨L, S⟩ draei_rel → ⟨L⟩ list_rel"
    "(initialei, initialei) ∈ ⟨L, S⟩ draei_rel → S"
    "(transitionei, transitionei) ∈ ⟨L, S⟩ draei_rel → ⟨S ×r L ×r S⟩ list_rel"
    "(conditionei, conditionei) ∈ ⟨L, S⟩ draei_rel → ⟨⟨S⟩ list_rel ×r ⟨S⟩ list_rel⟩ list_rel"
    unfolding draei_rel_def by auto

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

  lemmas [autoref_rel_intf] = REL_INTFI[of draei_drae_rel i_drae_scheme]

  lemma draei_drae_param[param, autoref_rules]:
    "(draei, drae) ∈ ⟨L⟩ list_set_rel → S → ⟨S ×r L ×r S⟩ list_set_rel →
      ⟨⟨S⟩ list_set_rel ×r ⟨S⟩ list_set_rel⟩ list_rel → ⟨L, S⟩ draei_drae_rel"
    "(alphabetei, alphabete) ∈ ⟨L, S⟩ draei_drae_rel → ⟨L⟩ list_set_rel"
    "(initialei, initiale) ∈ ⟨L, S⟩ draei_drae_rel → S"
    "(transitionei, transitione) ∈ ⟨L, S⟩ draei_drae_rel → ⟨S ×r L ×r S⟩ list_set_rel"
    "(conditionei, conditione) ∈ ⟨L, S⟩ draei_drae_rel → ⟨⟨S⟩ list_set_rel ×r ⟨S⟩ list_set_rel⟩ list_rel"
    unfolding draei_drae_rel_def by auto

  definition draei_drae where
    "draei_drae A ≡ drae (set (alphabetei A)) (initialei A)
      (set (transitionei A)) (map (map_prod set set) (conditionei A))"

  lemma draei_drae_id_param[param]: "(draei_drae, id) ∈ ⟨L, S⟩ draei_drae_rel → ⟨L, S⟩ drae_rel"
  proof
    fix Ai A
    assume 1: "(Ai, A) ∈ ⟨L, S⟩ draei_drae_rel"
    have 2: "draei_drae Ai = drae (set (alphabetei Ai)) (initialei Ai)
      (set (transitionei Ai)) (map (map_prod set set) (conditionei Ai))" unfolding draei_drae_def by rule
    have 3: "id A = drae (id (alphabete A)) (initiale A)
      (id (transitione A)) (map (map_prod id id) (conditione A))" by simp
    show "(draei_drae Ai, id A) ∈ ⟨L, S⟩ drae_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 ≡ the_elem ((T `` {p}) `` {a})"

  definition wft :: "'label set ⇒ 'state set ⇒ ('state × 'label × 'state) set ⇒ bool" where
    "wft L S T ≡ ∀ a ∈ L. ∀ p ∈ S. is_singleton ((T `` {p}) `` {a})"

  lemma wft_param[param]:
    assumes "bijective S" "bijective L"
    shows "(wft, wft) ∈ ⟨L⟩ set_rel → ⟨S⟩ set_rel → ⟨S ×r L ×r S⟩ set_rel → bool_rel"
    using assms unfolding wft_def by parametricity

  lemma wft_transitions: "wft L S (transitions L S s)" unfolding wft_def is_singleton_def by auto

  definition dra_drae where "dra_drae A ≡ drae (alphabet A) (initial A) 
    (transitions (alphabet A) (nodes A) (transition A))
    (map (λ (P, Q). (Set.filter P (nodes A), Set.filter Q (nodes A))) (condition A))"
  definition drae_dra where "drae_dra A ≡ dra (alphabete A) (initiale A)
    (succs (transitione A)) (map (λ (I, F). (λ p. p ∈ I, λ p. p ∈ F)) (conditione A))"

  lemma set_rel_Domain_Range[intro!, simp]: "(Domain A, Range A) ∈ ⟨A⟩ set_rel" unfolding set_rel_def by auto

  lemma dra_drae_param[param]: "(dra_drae, dra_drae) ∈ ⟨L, S⟩ dra_rel → ⟨L, S⟩ drae_rel"
    unfolding dra_drae_def by parametricity
  lemma drae_dra_param[param]:
    assumes "bijective L" "bijective S"
    assumes "wft (Range L) (Range S) (transitione B)"
    assumes [param]: "(A, B) ∈ ⟨L, S⟩ drae_rel"
    shows "(drae_dra A, drae_dra B) ∈ ⟨L, S⟩ dra_rel"
  proof -
    have 1: "(wft (Domain L) (Domain S) (transitione A), wft (Range L) (Range S) (transitione B)) ∈ bool_rel"
      using assms(1, 2) by parametricity auto
    have 2: "wft (Domain L) (Domain S) (transitione A)" using assms(3) 1 by simp
    show ?thesis
      using assms(1 - 3) 2 assms(2)[unfolded bijective_alt]
      unfolding drae_dra_def wft_def
      by parametricity force+
  qed

  lemma succs_transitions_param[param]:
    "(succs ∘ transitions L S, id) ∈ (Id_on L → Id_on S → Id_on S) → (Id_on L → Id_on S → Id_on S)"
  proof
    fix f g
    assume 1[param]: "(f, g) ∈ Id_on L → Id_on S → Id_on S"
    show "((succs ∘ transitions L S) f, id g) ∈ Id_on L → Id_on S → Id_on S"
    proof safe
      fix a p
      assume 2: "a ∈ L" "p ∈ S"
      have "(succs ∘ transitions L S) f a p = succs (transitions L S f) a p" by simp
      also have "(transitions L S f `` {p}) `` {a} = {f a p}" using 2 by auto
      also have "the_elem … = f a p" by simp
      also have "(…, g a p) ∈ Id_on S" using 2 by parametricity auto
      finally show "(succs ∘ transitions L S) f a p = id g a p" by simp
      show "id g a p ∈ S" using 1[param_fo] 2 by simp
    qed
  qed
  lemma drae_dra_dra_drae_param[param]:
    "((drae_dra ∘ dra_drae) A, id A) ∈ ⟨Id_on (alphabet A), Id_on (nodes A)⟩ dra_rel"
  proof -
    have [param]: "(λ (P, Q). (λ p. p ∈ Set.filter P (nodes A), λ p. p ∈ Set.filter Q (nodes A)), id) ∈
      pred_rel (Id_on (nodes A)) ×r pred_rel (Id_on (nodes A)) → rabin_rel (Id_on (nodes A))"
      unfolding fun_rel_def Id_on_def by auto
    have "(drae_dra ∘ dra_drae) A = dra (alphabet A) (initial A)
      ((succs ∘ transitions (alphabet A) (nodes A)) (transition A))
      (map (λ (P, Q). (λ p. p ∈ Set.filter P (nodes A), λ p. p ∈ Set.filter Q (nodes A))) (condition A))"
      unfolding drae_dra_def dra_drae_def by auto
    also have "(…, dra (alphabet A) (initial A) (id (transition A)) (map id (condition A))) ∈
      ⟨Id_on (alphabet A), Id_on (nodes A)⟩ dra_rel" using dra_rel_eq by parametricity auto
    also have "dra (alphabet A) (initial A) (id (transition A)) (map id (condition A)) = id A" by simp
    finally show ?thesis by this
  qed

  definition draei_dra_rel where
    [to_relAPP]: "draei_dra_rel L S ≡ {(Ae, A). (drae_dra (draei_drae Ae), A) ∈ ⟨L, S⟩ dra_rel}"
  lemma draei_dra_id[param]: "(drae_dra ∘ draei_drae, id) ∈ ⟨L, S⟩ draei_dra_rel → ⟨L, S⟩ dra_rel"
    unfolding draei_dra_rel_def by auto

(*
  schematic_goal drae_dra_impl: "(?f, drae_dra) ∈ ⟨Id, Id⟩ draei_drae_rel → ⟨Id, Id⟩ drai_dra_rel"
    unfolding drae_dra_def by (autoref (trace))
  concrete_definition drae_dra_impl uses drae_dra_impl
*)

end