Theory DRA_Translate

section ‹Explore and Enumerate Nodes of Deterministic Rabin Automata›

theory DRA_Translate
imports DRA_Explicit
begin

  subsection ‹Syntax›

  (* TODO: this syntax has unnecessarily high inner binding strength, requiring extra parentheses
    the regular let syntax correctly uses inner binding strength 0: ("(2_ =/ _)" 10) *)
  no_syntax "_do_let" :: "[pttrn, 'a] ⇒ do_bind" (‹(‹indent=2 notation=‹infix do let››let _ =/ _)› [1000, 13] 13)
  syntax "_do_let" :: "[pttrn, 'a] ⇒ do_bind" (‹(‹indent=2 notation=‹infix do let››let _ =/ _)› 13)

  section ‹Image on Explicit Automata›

  definition drae_image where "drae_image f A ≡ drae (alphabete A) (f (initiale A))
    ((λ (p, a, q). (f p, a, f q)) ` transitione A) (map (map_prod (image f) (image f)) (conditione A))"

  lemma drae_image_param[param]: "(drae_image, drae_image) ∈ (S → T) → ⟨L, S⟩ drae_rel → ⟨L, T⟩ drae_rel"
    unfolding drae_image_def by parametricity

  lemma drae_image_id[simp]: "drae_image id = id" unfolding drae_image_def by auto
  lemma drae_image_dra_drae: "drae_image f (dra_drae A) = drae
    (alphabet A) (f (initial A))
    (⋃ p ∈ nodes A. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p})
    (map (λ (P, Q). (f ` {p ∈ nodes A. P p}, f ` {p ∈ nodes A. Q p})) (condition A))"
    unfolding dra_drae_def drae_image_def drae.simps Set.filter_def by force

  section ‹Exploration and Translation›

  definition trans_spec where
    "trans_spec A f ≡ ⋃ p ∈ nodes A. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p}"

  definition trans_algo where
    "trans_algo N L S f ≡
      FOREACH N (λ p T. do {
        ASSERT (p ∈ N);
        FOREACH L (λ a T. do {
          ASSERT (a ∈ L);
          let q = S a p;
          ASSERT ((f p, a, f q) ∉ T);
          RETURN (insert (f p, a, f q) T) }
        ) T }
      ) {}"

  lemma trans_algo_refine:
    assumes "finite (nodes A)" "finite (alphabet A)" "inj_on f (nodes A)"
    assumes "N = nodes A" "L = alphabet A" "S = transition A"
    shows "(trans_algo N L S f, SPEC (HOL.eq (trans_spec A f))) ∈ ⟨Id⟩ nres_rel"
  unfolding trans_algo_def trans_spec_def assms(4-6)
  proof (refine_vcg FOREACH_rule_insert_eq)
    show "finite (nodes A)" using assms(1) by this
    show "(⋃ p ∈ nodes A. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p}) =
      (⋃ p ∈ nodes A. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p})" by rule
    show "(⋃ p ∈ {}. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p}) = {}" by simp
    fix T x
    assume 1: "T ⊆ nodes A" "x ∈ nodes A" "x ∉ T"
    show "finite (alphabet A)" using assms(2) by this
    show "(⋃ a ∈ {}. f ` {x} × {a} × f ` {transition A a x}) ∪
      (⋃ p ∈ T. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p}) =
      (⋃ p ∈ T. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p})"
      "(⋃ a ∈ alphabet A. f ` {x} × {a} × f ` {transition A a x}) ∪
      (⋃ p ∈ T. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p}) =
      (⋃ p ∈ insert x T. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p})" by auto
    fix Ta xa
    assume 2: "Ta ⊆ alphabet A" "xa ∈ alphabet A" "xa ∉ Ta"
    show "(f x, xa, f (transition A xa x)) ∉ (⋃ a ∈ Ta. f ` {x} × {a} × f ` {transition A a x}) ∪
      (⋃ p ∈ T. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p})"
      using 1 2(3) assms(3) by (auto dest: inj_onD)
    show "(⋃ a ∈ insert xa Ta. f ` {x} × {a} × f ` {transition A a x}) ∪
      (⋃ p ∈ T. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p}) =
      insert (f x, xa, f (transition A xa x)) ((⋃ a ∈ Ta. f ` {x} × {a} × f ` {transition A a x}) ∪
      (⋃ p ∈ T. ⋃ a ∈ alphabet A. f ` {p} × {a} × f ` {transition A a p}))"
      by simp
  qed

  definition to_draei :: "('state, 'label) dra ⇒ ('state, 'label) dra"
    where "to_draei ≡ id"

  (* TODO: make separate implementations for "dra_drae" and "op_set_enumerate ⤜ drae_image" *)
  schematic_goal to_draei_impl:
    fixes S :: "('statei × 'state) set"
    assumes [simp]: "finite (nodes A)"
    assumes [autoref_ga_rules]: "is_bounded_hashcode S seq bhc"
    assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('statei) hms"
    assumes [autoref_rules]: "(seq, HOL.eq) ∈ S → S → bool_rel"
    assumes [autoref_rules]: "(Ai, A) ∈ ⟨L, S⟩ drai_dra_rel"
    shows "(?f :: ?'a, do {
        let N = nodes A;
        f ← op_set_enumerate N;
        ASSERT (dom f = N);
        ASSERT (f (initial A) ≠ None);
        ASSERT (∀ a ∈ alphabet A. ∀ p ∈ dom f. f (transition A a p) ≠ None);
        T ← trans_algo N (alphabet A) (transition A) (λ x. the (f x));
        RETURN (drae (alphabet A) ((λ x. the (f x)) (initial A)) T
          (map (λ (P, Q). ((λ x. the (f x)) ` {p ∈ N. P p}, (λ x. the (f x)) ` {p ∈ N. Q p})) (condition A)))
      }) ∈ ?R"
    unfolding trans_algo_def by (autoref_monadic (plain))
  concrete_definition to_draei_impl uses to_draei_impl
  lemma to_draei_impl_refine'':
    fixes S :: "('statei × 'state) set"
    assumes "finite (nodes A)"
    assumes "is_bounded_hashcode S seq bhc"
    assumes "is_valid_def_hm_size TYPE('statei) hms"
    assumes "(seq, HOL.eq) ∈ S → S → bool_rel"
    assumes "(Ai, A) ∈ ⟨L, S⟩ drai_dra_rel"
    shows "(RETURN (to_draei_impl seq bhc hms Ai), do {
        f ← op_set_enumerate (nodes A);
        RETURN (drae_image (the ∘ f) (dra_drae A))
      }) ∈ ⟨⟨L, nat_rel⟩ draei_drae_rel⟩ nres_rel"
  proof -
    have 1: "finite (alphabet A)"
      using drai_dra_param(2)[param_fo, OF assms(5)] list_set_rel_finite
      unfolding finite_set_rel_def by auto
    note to_draei_impl.refine[OF assms]
    also have "(do {
        let N = nodes A;
        f ← op_set_enumerate N;
        ASSERT (dom f = N);
        ASSERT (f (initial A) ≠ None);
        ASSERT (∀ a ∈ alphabet A. ∀ p ∈ dom f. f (transition A a p) ≠ None);
        T ← trans_algo N (alphabet A) (transition A) (λ x. the (f x));
        RETURN (drae (alphabet A) ((λ x. the (f x)) (initial A)) T
          (map (λ (P, Q). ((λ x. the (f x)) ` {p ∈ N. P p}, (λ x. the (f x)) ` {p ∈ N. Q p})) (condition A)))
      }, do {
        f ← op_set_enumerate (nodes A);
        T ← SPEC (HOL.eq (trans_spec A (λ x. the (f x))));
        RETURN (drae (alphabet A) ((λ x. the (f x)) (initial A)) T
          (map (λ (P, Q). ((λ x. the (f x)) ` {p ∈ nodes A. P p}, (λ x. the (f x)) ` {p ∈ nodes A. Q p})) (condition A)))
      }) ∈ ⟨Id⟩ nres_rel"
      unfolding Let_def comp_apply op_set_enumerate_def using assms(1) 1
      by (refine_vcg vcg0[OF trans_algo_refine]) (auto intro!: inj_on_map_the[unfolded comp_apply])
    also have "(do {
        f ← op_set_enumerate (nodes A);
        T ← SPEC (HOL.eq (trans_spec A (λ x. the (f x))));
        RETURN (drae (alphabet A) ((λ x. the (f x)) (initial A)) T
          (map (λ (P, Q). ((λ x. the (f x)) ` {p ∈ nodes A. P p}, (λ x. the (f x)) ` {p ∈ nodes A. Q p})) (condition A)))
      },  do {
        f ← op_set_enumerate (nodes A);
        RETURN (drae_image (the ∘ f) (dra_drae A))
      }) ∈ ⟨Id⟩ nres_rel"
      unfolding trans_spec_def drae_image_dra_drae by refine_vcg force
    finally show ?thesis unfolding nres_rel_comp by simp
  qed

  (* TODO: generalize L *)
  context
    fixes Ai A
    fixes seq bhc hms
    fixes S :: "('statei × 'state) set"
    assumes a: "finite (nodes A)"
    assumes b: "is_bounded_hashcode S seq bhc"
    assumes c: "is_valid_def_hm_size TYPE('statei) hms"
    assumes d: "(seq, HOL.eq) ∈ S → S → bool_rel"
    assumes e: "(Ai, A) ∈ ⟨Id, S⟩ drai_dra_rel"
  begin

    definition f' where "f' ≡ SOME f'.
      (to_draei_impl seq bhc hms Ai, drae_image (the ∘ f') (dra_drae A)) ∈ ⟨Id, nat_rel⟩ draei_drae_rel ∧
      dom f' = nodes A ∧ inj_on f' (nodes A)"

    lemma 1: "∃ f'. (to_draei_impl seq bhc hms Ai, drae_image (the ∘ f') (dra_drae A)) ∈
      ⟨Id, nat_rel⟩ draei_drae_rel ∧ dom f' = nodes A ∧ inj_on f' (nodes A)"
      using to_draei_impl_refine''[
        OF a b c d e,
        unfolded op_set_enumerate_def bind_RES_RETURN_eq,
        THEN nres_relD,
        THEN RETURN_ref_SPECD]
      by force

    lemma f'_refine: "(to_draei_impl seq bhc hms Ai, drae_image (the ∘ f') (dra_drae A)) ∈
      ⟨Id, nat_rel⟩ draei_drae_rel" using someI_ex[OF 1, folded f'_def] by auto
    lemma f'_dom: "dom f' = nodes A" using someI_ex[OF 1, folded f'_def] by auto
    lemma f'_inj: "inj_on f' (nodes A)" using someI_ex[OF 1, folded f'_def] by auto

    definition f where "f ≡ the ∘ f'"
    definition g where "g = inv_into (nodes A) f"
    lemma inj_f[intro!, simp]: "inj_on f (nodes A)"
      using f'_inj f'_dom unfolding f_def by (simp add: inj_on_map_the)
    lemma inj_g[intro!, simp]: "inj_on g (f ` nodes A)"
      unfolding g_def by (simp add: inj_on_inv_into)

    definition rel where "rel ≡ {(f p, p) |p. p ∈ nodes A}"
    lemma rel_alt_def: "rel = (br f (λ p. p ∈ nodes A))¯"
      unfolding rel_def by (auto simp: in_br_conv)
    lemma rel_inv_def: "rel = br g (λ k. k ∈ f ` nodes A)"
      unfolding rel_alt_def g_def by (auto simp: in_br_conv)
    lemma rel_domain[simp]: "Domain rel = f ` nodes A" unfolding rel_def by force
    lemma rel_range[simp]: "Range rel = nodes A" unfolding rel_def by auto
    lemma [intro!, simp]: "bijective rel" unfolding rel_inv_def by (simp add: bijective_alt)
    lemma [simp]: "Id_on (f ` nodes A) O rel = rel" unfolding rel_def by auto
    lemma [simp]: "rel O Id_on (nodes A) = rel" unfolding rel_def by auto

    lemma [param]: "(f, f) ∈ Id_on (Range rel) → Id_on (Domain rel)" unfolding rel_alt_def by auto
    lemma [param]: "(g, g) ∈ Id_on (Domain rel) → Id_on (Range rel)" unfolding rel_inv_def by auto
    lemma [param]: "(id, f) ∈ rel → Id_on (Domain rel)" unfolding rel_alt_def by (auto simp: in_br_conv)
    lemma [param]: "(f, id) ∈ Id_on (Range rel) → rel" unfolding rel_alt_def by (auto simp: in_br_conv)
    lemma [param]: "(id, g) ∈ Id_on (Domain rel) → rel" unfolding rel_inv_def by (auto simp: in_br_conv)
    lemma [param]: "(g, id) ∈ rel → Id_on (Range rel)" unfolding rel_inv_def by (auto simp: in_br_conv)

    lemma to_draei_impl_refine':
      "(to_draei_impl seq bhc hms Ai, to_draei A) ∈ ⟨Id_on (alphabet A), rel⟩ draei_dra_rel"
    proof -
      have 1: "(draei_drae (to_draei_impl seq bhc hms Ai), id (drae_image f (dra_drae A))) ∈
        ⟨Id, nat_rel⟩ drae_rel" using f'_refine[folded f_def] by parametricity
      have 2: "(draei_drae (to_draei_impl seq bhc hms Ai), id (drae_image f (dra_drae A))) ∈
        ⟨Id_on (alphabet A), Id_on (f ` nodes A)⟩ drae_rel"
        using 1 unfolding drae_rel_def dra_drae_def drae_image_def by auto

      have 3: "wft (alphabet A) (nodes A) (transitione (dra_drae A))"
        using wft_transitions unfolding dra_drae_def drae.sel by this
      have 4: "(wft (alphabet A) (f ` nodes A) (transitione (drae_image f (dra_drae A))),
        wft (alphabet A) (id ` nodes A) (transitione (drae_image id (dra_drae A)))) ∈ bool_rel"
        using dra_rel_eq by parametricity auto
      have 5: "wft (alphabet A) (f ` nodes A) (transitione (drae_image f (dra_drae A)))" using 3 4 by simp

      have "(drae_dra (draei_drae (to_draei_impl seq bhc hms Ai)), drae_dra (id (drae_image f (dra_drae A)))) ∈
        ⟨Id_on (alphabet A), Id_on (f ` nodes A)⟩ dra_rel" using 2 5 by parametricity auto
      also have "(drae_dra (id (drae_image f (dra_drae A))), drae_dra (id (drae_image id (dra_drae A)))) ∈
        ⟨Id_on (alphabet A), rel⟩ dra_rel" using dra_rel_eq 3 by parametricity auto
      also have "drae_dra (id (drae_image id (dra_drae A))) = (drae_dra ∘ dra_drae) A" by simp
      also have "(…, id A) ∈ ⟨Id_on (alphabet A), Id_on (nodes A)⟩ dra_rel" by parametricity
      also have "id A = to_draei A" unfolding to_draei_def by simp
      finally show ?thesis unfolding draei_dra_rel_def by simp
    qed

  end

  context
  begin

    interpretation autoref_syn by this

    lemma to_draei_impl_refine[autoref_rules]:
      fixes S :: "('statei × 'state) set"
      assumes "SIDE_PRECOND (finite (nodes A))"
      assumes "SIDE_GEN_ALGO (is_bounded_hashcode S seq bhc)"
      assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('statei) hms)"
      assumes "GEN_OP seq HOL.eq (S → S → bool_rel)"
      assumes "(Ai, A) ∈ ⟨Id, S⟩ drai_dra_rel"
      shows "(to_draei_impl seq bhc hms Ai,
        (OP to_draei ::: ⟨Id, S⟩ drai_dra_rel →
        ⟨Id_on (alphabet A), rel Ai A seq bhc hms⟩ draei_dra_rel) $ A) ∈
        ⟨Id_on (alphabet A), rel Ai A seq bhc hms⟩ draei_dra_rel"
      using to_draei_impl_refine' assms unfolding autoref_tag_defs by this

  end

end