Theory Tree_Automata_Utils

section ‹Stuff about tree automata›
theory Tree_Automata_Utils
  imports TA.Tree_Automata
begin

subsection ‹Trivialities›

lemma ta_lang_imp_ground [simp]:
  "t ∈ ta_lang A ⟹ ground t"
  by (elim ta_langE2)

lemma ta_res_adapt_vars_ground [simp]:
  "ground t ⟹ ta_res A (adapt_vars t) = ta_res A t"
  by (induct t) auto

text ‹Properties of @{term adapt_vars}›

lemma adapt_vars_inj [simp]:
  assumes "adapt_vars x = adapt_vars y" "ground x" "ground y"
  shows "x = y"
  using adapt_vars_adapt_vars assms by metis

lemma funs_term_adapt_vars [simp]:
  "funs_term (adapt_vars t) = funs_term t"
  by (induct t) (auto simp: adapt_vars_def)

lemma adapt_vars_idemp:
  "ground t ⟹ adapt_vars (adapt_vars t) = adapt_vars t"
  by (induct t) auto

lemma adapt_vars_id:
  "ground t ⟹ adapt_vars t = t"
  by (induct t) (auto intro!: nth_equalityI)

lemma adapt_vars_in_ta_lang_conv [simp]:
  "adapt_vars t ∈ ta_lang A ⟷ t ∈ ta_lang A"
  unfolding ta_lang_def
  using adapt_vars_idemp adapt_vars_reverse ground_adapt_vars by blast

hide_const (open) make (* use ta.make instead *)

lemma ta_make_simps [simp]:
  "ta_rules (ta.make Q⇩f Δ ℰ) = Δ"
  "ta_eps (ta.make Q⇩f Δ ℰ) = ℰ"
  "ta_final (ta.make Q⇩f Δ ℰ) = Q⇩f"
  "ta.make Q⇩f Δ ℰ = ta.make Q⇩f' Δ' ℰ' ⟷ Q⇩f = Q⇩f' ∧ Δ = Δ' ∧ ℰ = ℰ'"
  by (simp_all add: ta.make_def)


subsection ‹Renaming automata symbols›

definition fmap_funs_ta :: "('f ⇒ 'g) ⇒ ('a, 'f) ta ⇒ ('a, 'g) ta" where
  "fmap_funs_ta h A = ta.make (ta_final A) {(h f) qs → q |f qs q. f qs → q ∈ ta_rules A} (ta_eps A)"

definition funs_ta :: "('q, 'f) ta ⇒ 'f set" where
  "funs_ta A = {f |f qs q. f qs → q ∈ ta_rules A}"

lemma fmap_funs_ta_cong [cong]:
  "(⋀x. x ∈ funs_ta A ⟹ h x = k x) ⟹ A = B ⟹ fmap_funs_ta h A = fmap_funs_ta k B"
  by (force simp: fmap_funs_ta_def funs_ta_def)

lemma fmap_funs_ta_id [simp]:
  "fmap_funs_ta id A = A"
proof -
  have [simp]: "{f qs → q |f qs q. f qs → q ∈ X} = X" for X by (intro set_eqI; case_tac x) auto
  show ?thesis by (simp add: fmap_funs_ta_def)
qed

(* maybe TODO: change definition of fmap_states_ta to this? *)
lemma fmap_states_ta_def':
  "fmap_states_ta f A = ta.make (f ` ta_final A) (map_ta_rule f id ` ta_rules A) (map_prod f f ` ta_eps A)"
proof -
  have [simp]: "map_ta_rule f id = case_ta_rule (λg qs q. g (map f qs) → f q)"
    by (auto split: ta_rule.splits)
  show ?thesis
    by (auto simp: fmap_states_ta_def ta.make_def[symmetric])
qed

lemma fmap_states_ta_id [simp]:
  "fmap_states_ta id A = A"
  by (cases A) (auto simp: fmap_states_ta_def split: ta_rule.splits)

lemmas fmap_funs_ta_id' [simp] = fmap_funs_ta_id[unfolded id_def]

lemma fmap_funs_ta_comp:
  "fmap_funs_ta h (fmap_funs_ta k A) = fmap_funs_ta (h ∘ k) A"
  by (auto simp: fmap_funs_ta_def)

lemma fmap_states_ta_comp:
  "fmap_states_ta h (fmap_states_ta k A) = fmap_states_ta (h ∘ k) A"
  by (auto simp: fmap_states_ta_def' ta_rule.map_comp image_comp comp_def id_def prod.map_comp)

lemma funs_ta_fmap_funs_ta [simp]:
  "funs_ta (fmap_funs_ta f A) = f ` funs_ta A"
  by (auto simp: funs_ta_def fmap_funs_ta_def)

lemma ta_states_fmap_states_ta [simp]:
  "ta_states (fmap_states_ta f A) = f ` ta_states A"
  by (cases A) (simp add: fmap_states_ta_def ta_states_def image_Un case_prod_eta prod.case_distrib
    image_UN r_states_def ta_rule.case_distrib r_rhs_def r_lhs_states_def cong: ta_rule.case_cong)

lemma ta_res_funs_ta:
  "q ∈ ta_res A t ⟹ funs_term t ⊆ funs_ta A"
proof (induct t arbitrary: q)
  case (Fun f ts)
  then have "f ∈ funs_ta A" by (auto simp: funs_ta_def)
  then show ?case using Fun(1)[OF nth_mem, THEN subsetD] Fun(2) by (auto dest!: in_set_idx)
qed auto

lemma ta_lang_funs_ta:
  "t ∈ ta_lang A ⟹ funs_term t ⊆ funs_ta A"
  by (elim ta_langE) (simp add: ta_res_funs_ta)

lemma ta_res_fmap_funs_ta:
  "q ∈ ta_res A t ⟹ q ∈ ta_res (fmap_funs_ta f A) (map_funs_term f t)"
  by (induct t arbitrary: q) (auto 0 4 simp: fmap_funs_ta_def)

lemma ta_res_fmap_states_ta:
  assumes "q ∈ ta_res A t"
  shows "h q ∈ ta_res (fmap_states_ta h A) (map_vars_term h t)"
proof -
  have [intro]: "(q, q') ∈ (ta_eps A)⇧* ⟹ (h q, h q') ∈ (ta_eps (fmap_states_ta h A))⇧*" for q q'
    by (force intro!: rtrancl_map[of "ta_eps A"] simp: fmap_states_ta_def)
  show ?thesis using assms
  proof (induct t arbitrary: q)
    case (Fun f ts)
    obtain q' qs where *: "f qs → q' ∈ ta_rules A" "(q', q) ∈ (ta_eps A)⇧*" "length qs = length ts"
      "⋀i. i < length ts ⟹ qs ! i ∈ ta_res A (ts ! i)" using Fun(2) by auto
    have "f (map h qs) → h q' ∈ ta_rules (fmap_states_ta h A)"
      using *(1) by (force simp: fmap_states_ta_def)
    then show ?case using Fun(1)[OF nth_mem *(4)] *(2,3) by (auto 0 4)
  qed auto
qed

lemma fmap_funs_ta_res':
  "q ∈ ta_res (fmap_funs_ta h A) t ⟹ ∃t'. q ∈ ta_res A t' ∧ map_funs_term h t' = t"
proof (induct t arbitrary: q)
  case (Var x) then show ?case by (auto simp: fmap_funs_ta_def intro!: exI[of _ "Var x"])
next
  case (Fun f ts)
  obtain f' qs q' where f': "f = h f'" "f' qs → q' ∈ ta_rules A" "(q', q) ∈ (ta_eps A)⇧*"
    "length qs = length ts" "⋀i. i < length ts ⟹ qs ! i ∈ ta_res (fmap_funs_ta h A) (ts ! i)"
    using Fun(2) by (auto simp: fmap_funs_ta_def)
  obtain ts' where "⋀i. i < length ts ⟹ qs ! i ∈ ta_res A (ts' i) ∧ map_funs_term h (ts' i) = ts ! i"
    using Fun(1)[OF nth_mem f'(5)] by metis
  note [simp] = conjunct1[OF this] conjunct2[OF this, unfolded id_def]
  show ?case by (auto simp: comp_def f'(1,2,3,4)
    intro!: exI[of _ "Fun f' (map ts' [0..<length ts])"] exI[of _ qs] exI[of _ q'] nth_equalityI)
qed

lemma fmap_funs_ta_lang:
  "ta_lang (fmap_funs_ta h A) = map_funs_term h ` ta_lang A"
proof ((intro set_eqI iffI; elim imageE ta_langE2), goal_cases lr rl)
  case (lr t q)
  obtain t' where t': "q ∈ ta_res A t'" "adapt_vars t = map_funs_term h t'"
    using lr(3) by (auto dest!: fmap_funs_ta_res')
  have [simp]: "adapt_vars (map_funs_term h t') = map_funs_term h (adapt_vars t')"
    by (simp add: adapt_vars_def term.map_comp comp_def)
  have "t' ∈ ta_lang A" using t'(1) lr(1,2)
    arg_cong[OF t'(2), of ground, unfolded id_def, symmetric]
    by (auto simp: fmap_funs_ta_def adapt_vars_id intro!: ta_langI[where q = q])
  then show ?case using lr(1) arg_cong[OF t'(2), of "adapt_vars :: _ ⇒ ('a, 'b) term"]
    by (auto intro!: rev_image_eqI[of "adapt_vars t'"])
next
  case (rl t t' q)
  have "q ∈ ta_res (fmap_funs_ta h A) (adapt_vars (map_funs_term h t'))"
    using ta_res_fmap_funs_ta[OF rl(4), of h] by (simp add: adapt_vars_def term.map_comp comp_def)
  then show ?case using rl(2,3) unfolding rl(1)
    by (intro ta_langI2[of "map_funs_term h t'" q]) (auto simp: id_def fmap_funs_ta_def)
qed

lemma ta_states_fmap_funs_ta [simp]:
  "ta_states (fmap_funs_ta f A) = ta_states A"
  by (auto 0 4 simp: fmap_funs_ta_def ta_states_def r_states_def r_rhs_def r_lhs_states_def split: ta_rule.splits)

lemma ta_reachable_fmap_funs_ta [simp]:
  "ta_reachable (fmap_funs_ta f A) = ta_reachable A"
  unfolding ta_reachable_def
  by (metis (mono_tags, lifting) fmap_funs_ta_res' ta_res_fmap_funs_ta ground_map_funs_term)

subsection ‹epsilon-closure of tree automata›
(* Do you want to shift the following theorems to another file, so that we can make it
a result on tree automata?*)

definition eps_closure :: "('q, 'f) ta ⇒ 'q ⇒ 'q set" where
   "eps_closure 𝒜 q = { q'. (q,q') ∈ (ta_eps 𝒜)^* }"

definition eps_elim :: "('q, 'f) ta ⇒ ('q, 'f) ta" where
   "eps_elim 𝒜 = (ta.make (ta_final 𝒜)
                  (ta_rules 𝒜 ∪ { rule . (∃fs qs q' q. rule = fs qs → q' ∧
                   fs qs → q ∈ ta_rules 𝒜 ∧ q' ∈ eps_closure 𝒜 q) }) {})"

text ‹The following theorem shows that epsilon-elimination of a
      tree automaton preserves its language.›
lemma ta_lang_eps_elim:
  fixes 𝒜 :: "('q, 'f) ta"
  shows "ta_lang (eps_elim 𝒜) = ta_lang 𝒜"
proof -
  { fix q t
    assume asm: "q ∈ ta_res (eps_elim 𝒜) t" "ground t"
    hence "q ∈ ta_res 𝒜 t"
    proof (induction t arbitrary: q)
      case (Fun f ts)
      then obtain q' qs where seq_props: "(f qs → q') ∈ ta_rules (eps_elim 𝒜)"
        "(q',q) ∈ ((ta_eps (eps_elim 𝒜))^*)" "length qs = length ts"
        "∀ i < length ts. qs ! i ∈ (map (ta_res (eps_elim 𝒜)) ts) ! i"
        using asm by auto
      have "ta_eps (eps_elim 𝒜) = {}" unfolding eps_elim_def make_def by auto
      then have "q = q'" using seq_props(2) by simp
      then obtain p where rule': "(f qs → p) ∈ ta_rules  𝒜" "(p,q) ∈ ((ta_eps 𝒜)^*)"
        using seq_props(1) unfolding eps_elim_def make_def eps_closure_def
        by fastforce
      { fix i
        assume "i < length ts"
        hence "qs ! i ∈ (map (ta_res 𝒜) ts) ! i"
          using Fun(1)[of "ts ! i" "qs ! i"] Fun(2-) seq_props(3,4)
          by force
      }
      thus ?case using eps_elim_def rule' seq_props(3) Fun by auto
    qed simp
  }
  moreover { fix q t
    assume asm: "q ∈ ta_res 𝒜 t" "ground t"
    hence "q ∈ ta_res (eps_elim 𝒜) t"
    proof (induction t arbitrary: q)
      case (Fun f ts)
      then obtain q' qs where seq_props: "(f qs → q') ∈ ta_rules 𝒜"
        "(q',q) ∈ ((ta_eps 𝒜)^*)" "length qs = length ts"
        "∀ i < length ts. qs ! i ∈ (map (ta_res 𝒜) ts) ! i"
        using asm by auto
      then have rule': "(f qs → q) ∈ ta_rules (eps_elim 𝒜)"
        unfolding eps_elim_def make_def eps_closure_def by auto
      { fix i
        assume "i < length ts"
        hence "qs ! i ∈ (map (ta_res (eps_elim 𝒜)) ts) ! i"
          using Fun(1)[of "ts ! i" "qs ! i"] Fun(2-) seq_props(3,4)
          by force
      }
      thus ?case using eps_elim_def rule' seq_props(3) Fun by auto
    qed simp
  }
  ultimately have res_eq: "ground t ⟶ ta_res 𝒜 t = ta_res (eps_elim 𝒜) t"
      for t
    by blast
  have final_eq: "ta_final (eps_elim 𝒜) = ta_final 𝒜"
    unfolding eps_elim_def make_def by auto
  {
    fix tv :: "('f, 'v) term"
    assume asm: "tv ∈ ta_lang 𝒜"
    obtain t  where t: "tv = adapt_vars (t::('f,'q) term)"
      using asm adapt_vars_adapt_vars ta_langE2
      by metis
    hence ground_t: "ground t" using asm ta_langE3 by blast
    hence "ta_final 𝒜 ∩ ta_res 𝒜 t ≠ {}" using t asm unfolding ta_lang_def
      using adapt_vars_inj by blast
    hence "ta_final (eps_elim 𝒜) ∩ ta_res (eps_elim 𝒜) t ≠ {}"
      using  ground_t res_eq[of t] final_eq by auto
    hence "tv ∈ ta_lang (eps_elim 𝒜)"
      using t asm ground_t unfolding ta_lang_def by blast
  }
  hence lang_incl: "ta_lang 𝒜 ⊆ ta_lang (eps_elim 𝒜)"
    using subsetI by auto
  { fix tv :: "('f, 'v) term"
    assume asm: "tv ∈ ta_lang (eps_elim 𝒜)"
    obtain t  where t: "tv = adapt_vars (t::('f,'q) term)"
      using asm adapt_vars_adapt_vars ta_langE2
      by metis
    hence ground_t:"ground t" using asm ta_langE3 by blast
    hence "ta_final (eps_elim 𝒜) ∩ ta_res (eps_elim 𝒜) t ≠ {}"
      using t asm adapt_vars_inj unfolding ta_lang_def by blast
    hence "ta_final 𝒜 ∩ ta_res 𝒜 t ≠ {}"
      using ground_t res_eq[of t] final_eq by auto
    hence "tv ∈ ta_lang 𝒜"
      using t asm ground_t unfolding ta_lang_def by blast
  }
  hence "ta_lang (eps_elim 𝒜) ⊆ ta_lang 𝒜"
    using subsetI by auto
  thus ?thesis using lang_incl by blast
qed

(* The reachable mixed terms of some term. *)
fun ta_res' :: "('q,'f)ta ⇒ ('f,'q)term ⇒ ('f,'q)term set" where
  "ta_res' TA (Var q) = {p. ∃q'. p = Var q' ∧ (q, q') ∈ (ta_eps TA)^*}"
| "ta_res' TA (Fun f ts) = {q. ∃q'. q = Var q' ∧ q' ∈ ta_res TA (Fun f ts)} ∪
                           {t. ∃ss. t = Fun f ss ∧ length ss = length ts ∧
                               (∀i < length ts. ss ! i ∈ ta_res' TA (ts ! i))}"

lemma ta_res'_ta_res:
  assumes "t ∈ ta_res' TA s" "p ∈ ta_res TA t"
  shows "p ∈ ta_res TA s"
  using assms
proof (induction arbitrary: p t rule: ta_res'.induct)
  case (2 TA f ts) show ?case using 2(2-)
  proof (induction t)
    case (Var q)
    show ?thesis using ta_res_ctxt[of q TA "Fun f ts" p □] Var by simp
  next
    case (Fun g ss)
    have ss_props: "g = f" "length ss = length ts" "∀i < length ts. ss ! i ∈ ta_res' TA (ts ! i)"
      using Fun(2) by (auto elim!: ta_res'.cases)
    obtain qs p' where qs_props: "(g qs → p') ∈ ta_rules TA ∧
          (p',p) ∈ (ta_eps TA)⇧* ∧ length qs = length ss ∧
          (∀i < length ss. qs ! i ∈ (map (ta_res TA) ss) ! i)"
      using Fun(3) by auto
    { fix i
      assume asm: "i < length ts"
      hence ss_i_ts_i: "ss ! i ∈ ta_res' TA (ts ! i)" using ss_props by blast
      have "qs ! i ∈ ta_res TA (ts ! i)"
        using Fun(3) 2(1)[OF asm ss_i_ts_i, of "qs ! i"] asm ss_props(2) qs_props by force
    }
    hence "∀i<length ts. qs ! i ∈ ta_res TA (ts ! i)"
      using ss_props(1,2) by blast
    thus ?thesis using qs_props unfolding ss_props by auto
  qed
qed force

lemma ta_res'_refl[simp]: "t ∈ ta_res' TA t"
by (induction t) fastforce+

lemma ta_eps_states: "ta_eps 𝒜 ⊆ ta_states 𝒜 × ta_states 𝒜"
  unfolding ta_states_def by auto

lemma finite_ta_statesI:
  assumes "finite (ta_final TA)" and "finite (ta_rules TA)" and "finite (ta_eps TA)"
  shows "finite (ta_states TA)"
  using assms unfolding ta_states_def r_states_def insert_def by auto

end