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" ("(2let _ =/ _)" [1000, 13] 13)
  syntax "_do_let" :: "[pttrn, 'a]  do_bind" ("(2let _ =/ _)" 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