Theory Regular_Tree_Relations.GTT

theory GTT
  imports Tree_Automata Ground_Closure
begin

section β€ΉGround Tree Transducers (GTT)β€Ί

(* A GTT 𝒒 consists of a set of interface states and
   a set of rules for automaton π’œ and one for ℬ. *)
type_synonym ('q, 'f) gtt = "('q, 'f) ta Γ— ('q, 'f) ta"

abbreviation gtt_rules where
  "gtt_rules 𝒒 ≑ rules (fst 𝒒) |βˆͺ| rules (snd 𝒒)"
abbreviation gtt_eps where
  "gtt_eps 𝒒 ≑ eps (fst 𝒒) |βˆͺ| eps (snd 𝒒)"
definition gtt_states where
  "gtt_states 𝒒 = 𝒬 (fst 𝒒) |βˆͺ| 𝒬 (snd 𝒒)"
abbreviation gtt_syms where
  "gtt_syms 𝒒 ≑ ta_sig (fst 𝒒) |βˆͺ| ta_sig (snd 𝒒)"
definition gtt_interface where
  "gtt_interface 𝒒 = 𝒬 (fst 𝒒) |∩| 𝒬 (snd 𝒒)"
definition gtt_eps_free where
  "gtt_eps_free 𝒒 = (eps_free (fst 𝒒), eps_free (snd 𝒒))"

definition is_gtt_eps_free :: "('q, 'f) ta Γ— ('p, 'g) ta β‡’ bool" where
  "is_gtt_eps_free 𝒒 ⟷ eps (fst 𝒒) = {||} ∧ eps (snd 𝒒) = {||}"

text β€Ή*anchored* language accepted by a GTTβ€Ί

definition agtt_lang :: "('q, 'f) gtt β‡’ 'f gterm rel" where
  "agtt_lang 𝒒 = {(t, u) |t u q. q |∈| gta_der (fst 𝒒) t ∧ q |∈| gta_der (snd 𝒒) u}"

lemma agtt_langI:
  "q |∈| gta_der (fst 𝒒) s ⟹ q |∈| gta_der (snd 𝒒) t ⟹ (s, t) ∈ agtt_lang 𝒒"
  by (auto simp: agtt_lang_def)

lemma agtt_langE:
  assumes "(s, t) ∈ agtt_lang 𝒒"
  obtains q where "q |∈| gta_der (fst 𝒒) s" "q |∈| gta_der (snd 𝒒) t"
  using assms by (auto simp: agtt_lang_def)

lemma converse_agtt_lang:
  "(agtt_lang 𝒒)Β― = agtt_lang (prod.swap 𝒒)"
  by (auto simp: agtt_lang_def)

lemma agtt_lang_swap:
  "agtt_lang (prod.swap 𝒒) = prod.swap ` agtt_lang 𝒒"
  by (auto simp: agtt_lang_def)

text β€Ήlanguage accepted by a GTTβ€Ί

abbreviation gtt_lang :: "('q, 'f) gtt β‡’ 'f gterm rel" where
  "gtt_lang 𝒒 ≑ gmctxt_cl UNIV (agtt_lang 𝒒)"  

lemma gtt_lang_join:
  "q |∈| gta_der (fst 𝒒) s ⟹ q |∈| gta_der (snd 𝒒) t ⟹ (s, t) ∈ gmctxt_cl UNIV (agtt_lang 𝒒)"
  by (auto simp: agtt_lang_def)

definition gtt_accept where
  "gtt_accept 𝒒 s t ≑ (s, t) ∈ gmctxt_cl UNIV (agtt_lang 𝒒)"

lemma gtt_accept_intros:
  "(s, t) ∈ agtt_lang 𝒒 ⟹ gtt_accept 𝒒 s t"
  "length ss = length ts ⟹ βˆ€ i < length ts. gtt_accept 𝒒 (ss ! i) (ts ! i) ⟹
    (f, length ss) ∈ β„± ⟹ gtt_accept 𝒒 (GFun f ss) (GFun f ts)"
  by (auto simp: gtt_accept_def)

abbreviation gtt_lang_terms :: "('q, 'f) gtt β‡’ ('f, 'q) term rel" where
  "gtt_lang_terms 𝒒 ≑ (Ξ» s. map_both term_of_gterm s) ` (gmctxt_cl UNIV (agtt_lang 𝒒))"

lemma term_of_gterm_gtt_lang_gtt_lang_terms_conv:
  "map_both term_of_gterm ` gtt_lang 𝒒 = gtt_lang_terms 𝒒"
  by auto

lemma gtt_accept_swap [simp]:
  "gtt_accept (prod.swap 𝒒) s t ⟷ gtt_accept 𝒒 t s"
  by (auto simp: gmctxt_cl_swap agtt_lang_swap gtt_accept_def)

lemma gtt_lang_swap:
  "(gtt_lang (A, B))Β― = gtt_lang (B, A)"
  using gtt_accept_swap[of "(A, B)"]
  by (auto simp: gtt_accept_def)

(* The following Lemmas are about ta_res' *)

lemma gtt_accept_exI:
  assumes "gtt_accept 𝒒 s t"
  shows "βˆƒ u. u |∈| ta_der' (fst 𝒒) (term_of_gterm s) ∧ u |∈| ta_der' (snd 𝒒) (term_of_gterm t)"
  using assms unfolding gtt_accept_def
proof (induction)
  case (base s t)
  then show ?case unfolding agtt_lang_def
    by (auto simp: gta_der_def ta_der_to_ta_der')
next
  case (step ss ts f)
  then have inner: "βˆƒ us. length us = length ss ∧
    (βˆ€i < length ss. (us ! i) |∈| ta_der' (fst 𝒒) (term_of_gterm (ss ! i)) ∧
    (us ! i) |∈| ta_der' (snd 𝒒) (term_of_gterm (ts ! i)))"
    using Ex_list_of_length_P[of "length ss" "Ξ» u i. u |∈| ta_der' (fst 𝒒) (term_of_gterm (ss ! i)) ∧
      u |∈| ta_der' (snd 𝒒) (term_of_gterm (ts ! i))"]
    by auto
  then obtain us where "length us = length ss ∧ (βˆ€i < length ss.
            (us ! i) |∈| ta_der' (fst 𝒒) (term_of_gterm (ss ! i)) ∧ (us ! i) |∈| ta_der' (snd 𝒒) (term_of_gterm (ts ! i)))"
    by blast
  then have "Fun f us |∈| ta_der' (fst 𝒒) (Fun f (map term_of_gterm ss)) ∧
         Fun f us |∈| ta_der' (snd 𝒒) (Fun f (map term_of_gterm ts))" using step(1) by fastforce
  then show ?case by (metis term_of_gterm.simps) 
qed


lemma agtt_lang_mono:
  assumes "rules (fst 𝒒) |βŠ†| rules (fst 𝒒')" "eps (fst 𝒒) |βŠ†| eps (fst 𝒒')"
    "rules (snd 𝒒) |βŠ†| rules (snd 𝒒')" "eps (snd 𝒒) |βŠ†| eps (snd 𝒒')"
  shows "agtt_lang 𝒒 βŠ† agtt_lang 𝒒'"
  using fsubsetD[OF ta_der_mono[OF assms(1, 2)]] ta_der_mono[OF assms(3, 4)]
  by (auto simp: agtt_lang_def gta_der_def dest!: fsubsetD[OF ta_der_mono[OF assms(1, 2)]] fsubsetD[OF ta_der_mono[OF assms(3, 4)]])

lemma gtt_lang_mono:
  assumes "rules (fst 𝒒) |βŠ†| rules (fst 𝒒')" "eps (fst 𝒒) |βŠ†| eps (fst 𝒒')" 
    "rules (snd 𝒒) |βŠ†| rules (snd 𝒒')" "eps (snd 𝒒) |βŠ†| eps (snd 𝒒')"
  shows "gtt_lang 𝒒 βŠ† gtt_lang 𝒒'"
  using agtt_lang_mono[OF assms]
  by (intro gmctxt_cl_mono_rel) auto

definition fmap_states_gtt where
  "fmap_states_gtt f ≑ map_both (fmap_states_ta f)"

lemma ground_map_vars_term_simp:
  "ground t ⟹ map_term f g t = map_term f (λ_. undefined) t"
  by (induct t) auto

lemma states_fmap_states_gtt [simp]:
  "gtt_states (fmap_states_gtt f 𝒒) = f |`| gtt_states 𝒒"
  by (simp add: fimage_funion gtt_states_def fmap_states_gtt_def)

lemma agtt_lang_fmap_states_gtt:
  assumes "finj_on f (gtt_states 𝒒)"
  shows "agtt_lang (fmap_states_gtt f 𝒒) = agtt_lang 𝒒" (is "?Ls = ?Rs")
proof -
  from assms have inj: "finj_on f (𝒬 (fst 𝒒) |βˆͺ| 𝒬 (snd 𝒒))" "finj_on f (𝒬 (fst 𝒒))" "finj_on f (𝒬 (snd 𝒒))"
    by (auto simp: gtt_states_def finj_on_fUn)
  then have "?Ls βŠ† ?Rs" using ta_der_fmap_states_inv_superset[OF _ inj(1)]
    by (auto simp: agtt_lang_def gta_der_def fmap_states_gtt_def)
  moreover have "?Rs βŠ† ?Ls"
    by (auto simp: agtt_lang_def gta_der_def fmap_states_gtt_def elim!: ta_der_to_fmap_states_der)
  ultimately show ?thesis by blast
qed

lemma agtt_lang_Inl_Inr_states_agtt:
  "agtt_lang (fmap_states_gtt Inl 𝒒) = agtt_lang 𝒒"
  "agtt_lang (fmap_states_gtt Inr 𝒒) = agtt_lang 𝒒"
  by (auto simp: finj_Inl_Inr intro!: agtt_lang_fmap_states_gtt)

lemma gtt_lang_fmap_states_gtt:
  assumes "finj_on f (gtt_states 𝒒)"
  shows "gtt_lang (fmap_states_gtt f 𝒒) = gtt_lang 𝒒" (is "?Ls = ?Rs")
  unfolding fmap_states_gtt_def
  using agtt_lang_fmap_states_gtt[OF assms]
  by (simp add: fmap_states_gtt_def)

definition gtt_only_reach where
  "gtt_only_reach = map_both ta_only_reach"

subsection β€Ή(A)GTT reachable statesβ€Ί

lemma agtt_only_reach_lang:
  "agtt_lang (gtt_only_reach 𝒒) = agtt_lang 𝒒"
  unfolding agtt_lang_def gtt_only_reach_def
  by (auto simp: gta_der_def simp flip: ta_der_gterm_only_reach)

lemma gtt_only_reach_lang:
  "gtt_lang (gtt_only_reach 𝒒) = gtt_lang 𝒒"
  by (auto simp: agtt_only_reach_lang)

lemma gtt_only_reach_syms:
  "gtt_syms (gtt_only_reach 𝒒) |βŠ†| gtt_syms 𝒒"
  by (auto simp: gtt_only_reach_def ta_restrict_def ta_sig_def)

subsection β€Ή(A)GTT productive statesβ€Ί

definition gtt_only_prod where
  "gtt_only_prod 𝒒 = (let iface = gtt_interface 𝒒 in
     map_both (ta_only_prod iface) 𝒒)"

lemma agtt_only_prod_lang:
  "agtt_lang (gtt_only_prod 𝒒) = agtt_lang 𝒒" (is "?Ls = ?Rs")
proof -
  let ?A = "fst 𝒒" let ?B = "snd 𝒒"
  have "?Ls βŠ† ?Rs" unfolding agtt_lang_def gtt_only_prod_def
    by (auto simp: Let_def gta_der_def dest: ta_der_ta_only_prod_ta_der)
  moreover
  {fix s t assume "(s, t) ∈ ?Rs"
    then obtain q where r: "q |∈| ta_der (fst 𝒒) (term_of_gterm s)" "q |∈| ta_der (snd 𝒒) (term_of_gterm t)"
      by (auto simp: agtt_lang_def gta_der_def)
    then have " q |∈| gtt_interface 𝒒" by (auto simp: gtt_interface_def)
    then have "(s, t) ∈ ?Ls" using r
      by (auto simp: agtt_lang_def gta_der_def gtt_only_prod_def Let_def intro!: exI[of _ q] ta_der_only_prod ta_productive_setI)}
  ultimately show ?thesis by auto
qed
                   
lemma gtt_only_prod_lang:
  "gtt_lang (gtt_only_prod 𝒒) = gtt_lang 𝒒"
  by (auto simp: agtt_only_prod_lang)

lemma gtt_only_prod_syms:
  "gtt_syms (gtt_only_prod 𝒒) |βŠ†| gtt_syms 𝒒"
  by (auto simp: gtt_only_prod_def ta_restrict_def ta_sig_def Let_def)

subsection β€Ή(A)GTT trimmingβ€Ί

definition trim_gtt where
  "trim_gtt = gtt_only_prod ∘ gtt_only_reach"

lemma trim_agtt_lang:
  "agtt_lang (trim_gtt G) = agtt_lang G"
  unfolding trim_gtt_def comp_def agtt_only_prod_lang agtt_only_reach_lang ..

lemma trim_gtt_lang:
  "gtt_lang (trim_gtt G) = gtt_lang G"
  unfolding trim_gtt_def comp_def gtt_only_prod_lang gtt_only_reach_lang ..

lemma trim_gtt_prod_syms:
  "gtt_syms (trim_gtt G) |βŠ†| gtt_syms G"
  unfolding trim_gtt_def using fsubset_trans[OF gtt_only_prod_syms gtt_only_reach_syms] by simp

subsection β€Ήroot-cleanlinessβ€Ί

text β€ΉA GTT is root-clean if none of its interface states can occur in a non-root positions
  in the accepting derivations corresponding to its anchored GTT relation.β€Ί

definition ta_nr_states :: "('q, 'f) ta β‡’ 'q fset" where
  "ta_nr_states A = |⋃| ((fset_of_list ∘ r_lhs_states) |`| (rules A))"

definition gtt_nr_states where
  "gtt_nr_states G = ta_nr_states (fst G) |βˆͺ| ta_nr_states (snd G)"

definition gtt_root_clean where
  "gtt_root_clean G ⟷ gtt_nr_states G |∩| gtt_interface G = {||}"


subsection β€ΉRelabelingβ€Ί

definition relabel_gtt :: "('q :: linorder, 'f) gtt β‡’ (nat, 'f) gtt" where
  "relabel_gtt G = fmap_states_gtt (map_fset_to_nat (gtt_states G)) G"

lemma relabel_agtt_lang [simp]:
  "agtt_lang (relabel_gtt G) = agtt_lang G"
  by (simp add: agtt_lang_fmap_states_gtt map_fset_to_nat_inj relabel_gtt_def)

lemma agtt_lang_sig:
  "fset (gtt_syms G) βŠ† β„± ⟹ agtt_lang G βŠ† 𝒯G β„± Γ— 𝒯G β„±"
  by (auto simp: agtt_lang_def gta_der_def 𝒯G_equivalent_def)
     (metis ffunas_gterm.rep_eq less_eq_fset.rep_eq subset_iff ta_der_gterm_sig)+

subsection β€Ήepsilon free GTTsβ€Ί


lemma agtt_lang_gtt_eps_free [simp]:
  "agtt_lang (gtt_eps_free 𝒒) = agtt_lang 𝒒"
  by (auto simp: agtt_lang_def gta_der_def gtt_eps_free_def ta_res_eps_free)

lemma gtt_lang_gtt_eps_free [simp]:
  "gtt_lang (gtt_eps_free 𝒒) = gtt_lang 𝒒"
  by auto

end