Theory TA_moves

theory TA_moves
imports "$ISAFOR/Tree_Automata/Tree_Automata" Tree_Automata_Utils Basic_Utils
begin

inductive move :: " ('q,'f) ta ⇒ ('f,'q) term ⇒ ('f,'q) term ⇒ bool" for TA where
  eps [intro]: "(q, q') ∈ ta_eps TA ⟹ move TA (Var q) (Var q')"
| rule [intro]: "∀q'∈set qs. is_Var q' ⟹ f (map the_Var qs) → q ∈ ta_rules TA ⟹
                 move TA (Fun f qs) (Var q)"
| ctxt [intro]: "f = g ⟹ length ts = length ss ⟹ (*`length ts = length ss` not needed anymore?*)
    (∃i < length ts. ss = take i ts @ ss ! i # drop (Suc i) ts ∧ move TA (ts ! i) (ss ! i)) ⟹
    move TA (Fun f ts) (Fun g ss)"

"move' TA ≡ {(s,t). move TA s t}"">abbreviation "move' TA ≡ {(s,t). move TA s t}"

lemma move_Var_Fun_neg:
  "¬ move TA (Var q) (Fun f ts)"
  using  move.cases by fast

lemma move_ctxt_closed:
  "move TA s t ⟹ move TA C⟨s⟩ C⟨t⟩"
proof (induction C)
  case (More f ss1 C ss2)
  let ?ts = "ss1 @ C⟨s⟩ # ss2" and ?ss = "ss1 @ C⟨t⟩ # ss2" and ?i = "length ss1"
  have "length ?ts = length ?ss" by simp
  moreover have "?i < length ?ts ∧ ?ss = take ?i ?ts @ ?ss ! ?i # drop (Suc ?i) ?ts ∧
        move TA (?ts ! length ss1) (?ss ! length ss1)"
    using More by force
  ultimately show ?case unfolding ctxt_apply_term.simps by (intro move.intros) blast+
qed simp

lemma move_star_ctxt_closed:
  assumes "(s, t) ∈ (move' TA)⇧*"
  shows "(C⟨s⟩, C⟨t⟩) ∈ (move' TA)⇧*"
  using assms
proof (induction rule: rtrancl_induct)
  case (step y z)
  thus ?case using move_ctxt_closed[of TA y z C]
    by (auto intro: rtrancl_into_rtrancl)
qed simp

lemma ta_res'_vars:
  "t ∈ ta_res' TA (Var q) ⟹ is_Var t"
  by (auto elim!: ta_res'.elims)

lemma move'_vars:
  "(Var q, t) ∈ move' TA ⟹ is_Var t"
  by (auto elim!: move.cases)

lemma move'_vars_star:
  assumes "(Var q, t) ∈ (move' TA)⇧*"
  shows "is_Var t"
  using assms
proof (induction arbitrary: q rule: rtrancl_induct)
  case (step y z)
  thus ?case using move'_vars by fast
qed simp

lemma move'_ta_states1:
  assumes "(Var q, t) ∈ move' TA"
  shows "q ∈ ta_states TA"
proof -
  obtain q' where "t = Var q'" using move'_vars[OF assms] by fast
  thus ?thesis using assms ta_eps_states by (auto elim: move.cases)
qed

lemma move'_ta_states2:
  assumes "(t, Var q) ∈ move' TA"
  shows "q ∈ ta_states TA"
proof (cases t)
  case (Var x)
  hence "(x, q) ∈ ta_eps TA" using assms by (auto elim: move.cases)
  then show ?thesis using ta_eps_states by blast
next
  case (Fun f ts)
  show ?thesis using assms r_rhs_states[of f "map the_Var ts" q TA]
    unfolding Fun by (auto elim: move.cases)
qed

lemma move'_ta_states3:
  assumes "(t, Var q) ∈ (move' TA)⇧*"
 and "t ≠ Var q"
shows "q ∈ ta_states TA"
proof -
  obtain s where "(t, s) ∈ (move' TA)⇧*" "(s, Var q) ∈ (move' TA)"
    using rtranclE assms by metis
  then show ?thesis using move'_ta_states2[of s q TA] by argo
qed

lemma is_Var_map:
  "∀i < length qs. is_Var ((map Var qs) ! i)"
  by auto

lemma transition_chain:
  assumes "∀i < length zs. zs ! i ∈ R⇧*"
          "∀i < length zs - 1. snd (zs ! i) = fst (zs ! (Suc i))"
  shows "zs ≠ [] ⟶ (fst (zs ! 0), snd (zs ! (length zs - 1))) ∈ R⇧*"
  using assms
proof (induction zs)
  case (Cons a zs)
  have "∀i<length zs. zs ! i ∈ R⇧*" using Cons(2) by force
  moreover have "∀i. Suc i < length zs ⟶ snd (zs ! i) = fst (zs ! Suc i)" using Cons(3) by force
  ultimately have "zs ≠ [] ⟶ (fst (zs ! 0), snd (zs ! (length zs - 1))) ∈ R⇧*"
    using Cons(1) by (cases zs) auto
  moreover have "a ∈ R⇧*" using Cons(2) by force
  moreover have "zs ≠ [] ⟶ snd a = fst (zs ! 0)" using Cons(3) by force
  ultimately show ?case
    by simp (metis One_nat_def length_0_conv nth_Cons' prod.collapse rtrancl_trans)
qed simp

fun create_list :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a list" where
  "create_list f 0 = []"
| "create_list f (Suc n) = f n # create_list f n"

lemma create_list_length [simp]:
  "length (create_list f n) = n"
  by (induction n) auto

lemma create_list_ith:
  "i < n ⟶ (rev (create_list f n)) ! i = f i"
  by (induction n) (simp, metis create_list.simps(2) create_list_length diff_Suc_Suc length_Cons
      length_upt less_SucE list.size(3) nth_Cons_0 nth_Cons_Suc rev_nth upt_rec)

lemma transition_chain':
  assumes "∀i < length xs. (f xs ys i, g xs ys i) ∈ R⇧*"
          "∀i < length xs - 1. g xs ys i = f xs ys (Suc i)"
          "length xs = length ys" "xs ≠ []"
  shows "(f xs ys 0, g xs ys (length xs - 1)) ∈ R⇧*"
proof -
  define ith zs where "ith = (λi. (f xs ys i, g xs ys i))" and
                      "zs = rev (create_list ith (length xs))"
  have zs_i: "∀i<length zs. zs ! i ∈ R⇧*" using assms(1,3) create_list_ith[of _ "length xs" ith]
    unfolding zs_def ith_def length_rev create_list_length by presburger
  have chain: "∀i<length zs - 1. snd (zs ! i) = fst (zs ! Suc i)"
    using assms(2-4) create_list_ith[of _ "length xs" ith]
    unfolding zs_def ith_def length_rev create_list_length by fastforce
  show ?thesis using transition_chain[of zs R, OF zs_i chain] assms(3,4)
    unfolding zs_def ith_def
    by (smt Suc_diff_Suc create_list_ith create_list_length diff_Suc_eq_diff_pred fst_conv
        length_greater_0_conv length_rev lessI minus_nat.diff_0 snd_conv)
qed

lemma move_ta_res:
  assumes "move TA s q" "is_Var q"
  shows "the_Var q ∈ ta_res TA s"
  using assms
proof (induction s q rule: move.induct)
  case (rule qs f q)
  hence "f (map the_Var qs) → q ∈ ta_rules TA ∧ (q, q) ∈ (ta_eps TA)⇧* ∧
       length (map the_Var qs) = length qs"
    by auto
  moreover { fix i
    assume asm: "i < length qs"
    hence "is_Var (qs ! i)" using rule(1) by simp
    hence "(map the_Var qs) ! i ∈ ta_res TA (qs ! i)" using asm by force
  }
  ultimately show ?case by force
qed simp+

lemma move_ta_res':
  assumes "move TA s q"
  shows "q ∈ ta_res' TA s"
  using assms
proof (induction s q rule: move.induct)
  case (rule qs f q)
  hence "f (map the_Var qs) → q ∈ ta_rules TA ∧ (q, q) ∈ (ta_eps TA)⇧* ∧
       length (map the_Var qs) = length qs"
    by auto
  moreover { fix i
    assume asm: "i < length qs"
    hence "is_Var (qs ! i)" using rule(1) by simp
    hence "(map the_Var qs) ! i ∈ ta_res TA (qs ! i)" using asm by force
  }
  ultimately show ?case by force
next
  case (ctxt f g ts ss)
  then obtain i where "i < length ts" "ss = take i ts @ ss ! i # drop (Suc i) ts"
                      "ss ! i ∈ ta_res' TA (ts ! i)"
    by blast
  hence "j < length ts ⟶ ss ! j ∈ ta_res' TA (ts ! j)" for j
    using ta_res'_refl[of "ts ! _" TA]
    by (metis less_imp_le_nat nth_append_take_drop_is_nth_conv)
  thus ?case using ctxt(1,2) by fastforce
qed force

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
    } note inner = this
    hence "∀i<length ts. qs ! i ∈ ta_res TA (ts ! i)"
      using ss_props(1,2) construct_exI'[of "length ts" "λx i. x ∈ ta_res TA (ts ! i)"] by blast
    thus ?thesis using qs_props unfolding ss_props by auto
  qed
qed force

lemma move_preserves_ta_res:
  assumes "move TA s t" "q ∈ ta_res TA t" shows "q ∈ ta_res TA s"
  using assms
  by (meson move_ta_res' ta_res'_ta_res)

lemma move_ta_res_star:
  assumes "(s, q) ∈ (move' TA)⇧*" "is_Var q"
  shows "the_Var q ∈ ta_res TA s"
  using assms
proof (induction rule: converse_rtrancl_induct)
  case (step y z)
  hence "the_Var q ∈ ta_res TA z" by argo
  moreover have "z ∈ ta_res' TA y" using step(1) move_ta_res'[of TA y z] by auto
  ultimately show ?case using ta_res'_ta_res by fast
qed auto

lemma ta_res_move_star:
  assumes "q ∈ ta_res TA s"
  shows "(s, Var q) ∈ (move' TA)⇧*"
  using assms
proof (induction TA s arbitrary: q rule: ta_res.induct)
  case (1 TA p)
  hence "(p, q) ∈ (ta_eps TA)⇧*"
    using ta_res'_vars by (auto elim!: ta_res'.elims)
  thus ?case by (induction rule: rtrancl_induct)
    (simp, metis case_prodI mem_Collect_eq move.intros(1) rtrancl.simps)
next
  case (2 TA f ts)
  then obtain q' qs where seq:
    "(f qs → q') ∈ ta_rules TA" "(q',q) ∈ ((ta_eps TA)^*)" "length qs = length ts"
     "∀i < length ts. qs ! i ∈ (map (ta_res TA) ts) ! i" by auto
  let ?f = "λts qs i. Fun f ((map Var (take i qs)) @ ts ! i # drop (Suc i) ts)" and
      ?g = "λts qs i. Fun f ((map Var (take i qs)) @ Var (qs ! i) # drop (Suc i) ts)"
  have "∀i < length ts. (ts ! i, Var (qs ! i)) ∈ (move' TA)⇧*"
    using 2(1)[of _ "ts ! _"] 2(2) seq by (auto elim!: ta_res.cases)
  hence move_in_ctxt: "i < length ts ⟶ (Fun f ((map Var (take i qs)) @ ts ! i # drop (Suc i) ts),
                            Fun f ((map Var (take i qs)) @ Var (qs ! i) # drop (Suc i) ts))
                            ∈ (move' TA)⇧*" for i
    using move_star_ctxt_closed[of _ _ TA "More f _ □ _"] by simp
  moreover { fix i
    assume asm: "i < length ts - 1"
    hence "map Var (take i qs) @ [Var (qs ! i)] = map Var (take (Suc i) qs)" using seq(3)
      by (simp add: take_Suc_conv_app_nth)
    moreover have "drop (Suc i) ts = ts ! Suc i # drop (Suc (Suc i)) ts" using asm
      by (metis Cons_nth_drop_Suc Suc_eq_plus1 less_diff_conv)
    ultimately have "?g ts qs i = ?f ts qs (Suc i)" using seq(3) by auto
  }
  ultimately have first_part: "(Fun f ts, Fun f (map Var qs)) ∈ (move' TA)⇧*"
    using transition_chain'[of ts "?f" qs ?g "move' TA"] seq(3)
    by (cases ts) (fastforce, simp, metis (no_types, lifting) Cons_nth_drop_Suc
          append_take_drop_id diff_self_eq_0 length_0_conv length_drop lessI
          list.map_disc_iff list.simps(9) map_append)
  have qs_simp: "map (the_Var ∘ Var) qs = qs" using map_nth_eq_conv[of qs qs "the_Var ∘ Var"] by simp
  have "move TA (Fun f (map Var qs)) (Var q')"
    using seq(1) by (intro move.intros(2)) (auto elim!: move.cases simp: qs_simp)
  moreover have "(Var q', Var q) ∈ (move' TA)⇧*"
    using seq(2) by (induction rule: rtrancl_induct)
      (simp, metis (no_types) case_prodI mem_Collect_eq move.intros(1) rtrancl.simps)
  ultimately show ?case using first_part
    by (metis case_prodI mem_Collect_eq rtrancl.rtrancl_into_rtrancl rtrancl_trans)
qed

lemma ta_res'_move_star:
  assumes "t ∈ ta_res' TA s"
  shows "(s, t) ∈ (move' TA)⇧*"
  using assms
proof (induction TA s arbitrary: t rule: ta_res'.induct)
  case (1 TA q)
  then obtain q' where "(q, q') ∈ (ta_eps TA)⇧*" "t = Var q'"
    using ta_res'_vars by (auto elim!: ta_res'.elims)
  thus ?case
  proof (induction arbitrary: t rule: rtrancl_induct)
    case (step y z)
    show ?case using step(1-3) unfolding step(4)
      by (simp, metis (no_types) case_prodI mem_Collect_eq move.intros(1) rtrancl.simps)
  qed blast
next
  case (2 TA f ts)
  consider (Var) "t ∈ {q. ∃q'. q = Var q' ∧ q' ∈ ta_res TA (Fun f ts)}" |
           (Fun) "t ∈ {t. ∃ss. t = Fun f ss ∧ length ss = length ts ∧
                 (∀ i < length ts. ss ! i ∈ ta_res' TA (ts ! i))}"
    using 2(2) by (metis (mono_tags, lifting) Un_iff ta_res'.simps(2))
  thus ?case
  proof cases
    case Var
    then obtain q where t_props: "t = Var q" "q ∈ ta_res TA (Fun f ts)" by blast
    show ?thesis using ta_res_move_star[OF t_props(2)] unfolding t_props(1) term.sel .
  next
    case Fun
    let ?f = "λts ss i. Fun f (take i ss @ ts ! i # drop (Suc i) ts)" and
      ?g = "λts ss i. Fun f (take i ss @ ss ! i # drop (Suc i) ts)"
    obtain ss where t_props: "t = Fun f ss" "length ss = length ts"
        "∀ i < length ts. ss ! i ∈ ta_res' TA (ts ! i)"
      using 2(2) Fun by blast
    hence "i < length ts ⟶ (ts ! i, ss ! i) ∈ (move' TA)⇧*" for i
      using 2(1)[of i "ss ! i"] 2(2) unfolding Fun by blast

    hence move_in_ctxt: "i < length ts ⟶ (Fun f (take i ss @ ts ! i # drop (Suc i) ts),
                            Fun f (take i ss @ ss ! i # drop (Suc i) ts)) ∈ (move' TA)⇧*" for i
      using move_star_ctxt_closed[of _ _ TA "More f _ □ _"] by simp
    moreover { fix i
      assume asm: "i < length ts - 1"
      hence "take i ss @ [ss ! i] = take (Suc i) ss" using t_props(2)
        by (simp add: take_Suc_conv_app_nth)
      moreover have "drop (Suc i) ts = ts ! Suc i # drop (Suc (Suc i)) ts" using asm
        by (metis Cons_nth_drop_Suc Suc_eq_plus1 less_diff_conv)
      ultimately have "?g ts ss i = ?f ts ss (Suc i)" using t_props(2) by auto
    }
    ultimately show ?thesis
      using transition_chain'[of ts "?f" ss ?g "move' TA"] t_props(2) unfolding t_props(1)
        by (cases ts) (force, simp, metis Cons_nth_drop_Suc lessI less_or_eq_imp_le
            list.sel(1) take_all take_hd_drop)
  qed
qed

lemma move_Fun_single:
  assumes "(s,t) ∈ (move' TA)⇧*"
  shows "(Fun f (ss@(s#ts)), Fun f (ss@(t#ts))) ∈ (move' TA)⇧*"
  using assms
  by (simp add: ctxt.closedI ctxt_closed_one move_star_ctxt_closed)

lemma move_Fun:
  assumes "∀i < length ts. (ts!i, ss!i) ∈ (move' TA)⇧*"
  and "length ts = length ss"
  and "ts ≠ []"
  shows "(Fun f ts, Fun f ss) ∈ (move' TA)⇧*"
proof -
  let ?h = "λ ts ss i. (Fun f ((take i ss)@(ts!i)#(drop (Suc i) ts)))"
  let ?g = "λ ts ss i. (Fun f ((take i ss)@(ss!i)#(drop (Suc i) ts)))"
  have "∀i< length ts - 1. ?g ts ss i = ?h ts ss (Suc i)"
    by (simp add: Cons_nth_drop_Suc assms(2) list.size(3) take_Suc_conv_app_nth)
  moreover have "∀i < length ts. (?h ts ss i, ?g ts ss i) ∈ (move' TA)⇧*"
    using assms by (simp add: move_Fun_single)
  moreover have "?h ts ss  0 = Fun f ts" "?g ts ss  (length ts - 1) = Fun f ss"
   using assms(2,3) nth_drop_0
   by (auto)[1](metis Cons_nth_drop_Suc One_nat_def Suc_diff_Suc
                append_take_drop_id assms(2) assms(3) diff_less diff_zero drop_eq_Nil
                length_greater_0_conv order_refl zero_less_Suc)
  ultimately show ?thesis using transition_chain'[of "ts" "?h" "ss" "?g" "(move' TA)"]
    assms(2,3) by argo
qed


lemma move_ctxt_closure:
  assumes "length ss = length ts" "num_holes C = length ss"
    "∀i < length ts. (ss!i, ts!i) ∈ (move' TA)⇧*"
  shows "(fill_holes C ss, fill_holes C ts) ∈ (move' TA)⇧*" using assms
proof (induction C arbitrary: ss ts)
  case (MVar x)
  then show ?case  by simp
next
  case MHole
  hence "∃q q'. ss = [q] ∧ ts = [q']" using MHole
    by (metis eq_fill.intros eqf_MHoleE)
  thus ?case using assms MHole.prems(3) by force
next
  case (MFun f Cs)
  let ?sss = "(partition_holes ss Cs)"
  let ?tss = "(partition_holes ts Cs)"
  obtain Css Cts  where  Css_Cts:"fill_holes (MFun f Cs) ss = Fun f Css"
                        "fill_holes (MFun f Cs) ts = Fun f Cts"
    by simp
  {fix i
   assume loc_asm:"i < length Cs"
   hence "length (?sss!i) = length (?tss!i)" using assms(1) MFun by simp
   moreover have "num_holes (Cs!i) = length (?sss!i)" using assms(2) loc_asm MFun by force
   moreover have "∀j < length (?tss!i). ((?sss ! i)!j , (?tss ! i)!j)∈ (move' TA)⇧*"
      using loc_asm MFun assms(3) by (metis calculation(1) calculation(2) length_map nth_map
                  num_holes.simps(3) partition_by_nth_nth(1) partition_by_nth_nth(2))
   ultimately have "(fill_holes (Cs!i) (?sss!i), fill_holes (Cs!i) (?tss!i)) ∈ (move' TA)⇧*"
     using MFun(1) loc_asm by force}
  hence "∀i < length Cs. (fill_holes (Cs!i) (?sss!i), fill_holes (Cs!i) (?tss!i)) ∈ (move' TA)⇧*"
    by blast
  hence "∀i < length Cts. (Css!i, Cts!i) ∈ (move' TA)⇧*" using MFun Css_Cts by force
  moreover have "length Css = length Cts" using Css_Cts by force
  ultimately show ?case using MFun move_Fun Css_Cts
    by (metis list.simps(8) list.size(3) map_nth rtrancl.rtrancl_refl upt_0)
qed

end