Theory TRS_GTT

theory TRS_GTT
  imports GTT Tree_Automata_Utils
begin

definition TRS_fst :: "('f, 'v) trs ⇒ ('f, 'v) term set" where
  "TRS_fst Ts ≡ {fst R|R. R ∈ Ts} "

definition TRS_snd :: "('f, 'v) trs ⇒ ('f, 'v) term set" where
  "TRS_snd Ts ≡ {snd R|R. R ∈ Ts}"

definition TRS_terms :: "('f, 'v) trs ⇒ ('f, 'v) term set" where
  "TRS_terms Ts ≡ (TRS_fst Ts) ∪ (TRS_snd Ts)"


definition TRS_sides :: "('f, 'v) trs ⇒ ('f, 'v) term set" where
  "TRS_sides T ≡ {fst R|R. R ∈ T} ∪ {snd R|R. R ∈ T}"

definition cmn_ta_rules_G :: "('f, 'v) term set ⇒(('f, 'v) term + ('f, 'v) term, 'f) ta_rule set" where
  "cmn_ta_rules_G T ≡ {(f (map Inl ts) → Inl (Fun f ts))|f ts t. Fun f ts ⊴ t ∧ t ∈ T}"

definition cmn_ta_rules_D :: "('f, 'v) term set ⇒(('f, 'v) term + ('f, 'v) term, 'f) ta_rule set" where
  "cmn_ta_rules_D T ≡ {(f (map Inr ts) → Inr (Fun f ts))|f ts t. Fun f ts ⊴ t ∧ t ∈ T}"

(*In the following, we use G and D to denote the two automaton, as consistent with the notation 
in the Dauchet-Tison paper*)

definition trs_to_ta_A :: "('f, 'v) trs ⇒ (('f, 'v) term + ('f, 'v) term, 'f) ta" where
  "trs_to_ta_A Ts ≡ ta.make {}
    (cmn_ta_rules_G (TRS_terms Ts))
    {(Inl l, Inr r)| l r. (l,r) ∈ Ts}"

definition trs_to_ta_B :: "('f, 'v) trs ⇒ (('f, 'v) term + ('f, 'v) term, 'f) ta" where
  "trs_to_ta_B Ts ≡ ta.make {}
    (cmn_ta_rules_D (TRS_terms Ts))
    {(Inr r, Inl l)| l r. (l,r) ∈ Ts}"


definition is_Inl :: "('a + 'b) ⇒ bool" where
  "is_Inl x ≡ (∃v. x = Inl v)"

definition is_Inr :: "('a + 'b) ⇒ bool" where
  "is_Inr x ≡ (∃v. x = Inr v)"

(*The following two ancillary lemmas are needed for the rstep_to_gtt proof. Note to self- Try to see if a 
common proof can be extracted *)

lemma ground_recur:
  assumes "ground (Fun f ts)" "i < length ts" shows "ground (ts!i)"
  using assms by simp

lemma adpvars_A: 
  assumes "ground s" "ground_trs R" "Inl q ∈ ta_res (trs_to_ta_A R) (adapt_vars s)"
  shows "q = s"
  using assms(3,2,1) 
proof (induction s arbitrary: q rule:ta_res.induct)
   case (2 TA f ts)
  define TA where "TA = (trs_to_ta_A R)"
  with 2 obtain q' qs where qs:
    "(f qs → q') ∈ ta_rules TA"
    "(q',Inl q) ∈ ((ta_eps TA)^*)" 
    "length qs = length ts " 
    "∀ i < length ts. qs ! i ∈ (ta_res TA (adapt_vars (ts! i)))" 
    by auto
  have q:"q' = Inl q" 
  proof -
    obtain ss :: "((('a, 'b) Term.term + ('a, 'b) Term.term) × (('a, 'b) Term.term + ('a, 'b) Term.term)) set ⇒ ('a, 'b) Term.term + ('a, 'b) Term.term ⇒ ('a, 'b) Term.term + ('a, 'b) Term.term ⇒ ('a, 'b) Term.term + ('a, 'b) Term.term" where
      f1: "∀x0 x1 x2. (∃v3. (x2, v3) ∈ x0⇧* ∧ (v3, x1) ∈ x0) = ((x2, ss x0 x1 x2) ∈ x0⇧* ∧ (ss x0 x1 x2, x1) ∈ x0)"
      by moura
    have "(q', ss (ta_eps TA) (Inl q) q') ∉ (ta_eps TA)⇧* ∨ (ss (ta_eps TA) (Inl q) q', Inl q) ∉ ta_eps TA"
      by (simp add: TA_def TRS_GTT.trs_to_ta_A_def)
    then show ?thesis
      using f1 by (meson ‹(q', Inl q) ∈ (ta_eps TA)⇧*› rtranclE)
  qed
  moreover obtain qs' where qs':"qs = map Inl qs'" using qs(1) unfolding TA_def trs_to_ta_A_def cmn_ta_rules_G_def
    by fastforce
  hence "q' = Inl (Fun f qs')" using qs(1)  unfolding TA_def trs_to_ta_A_def cmn_ta_rules_G_def
    by force
  hence step1:"q = Fun f qs'"  using q by blast
  {fix i
    assume i:"i < length ts"
    hence "Inl (qs'!i) ∈ (ta_res TA (adapt_vars (ts! i)))" 
      using qs(3,4) qs' by fastforce
    moreover have "ground (ts!i)" using ground_recur[OF 2(4) i].
    ultimately have "(ts!i) = (qs'!i)" using 2(1) 
      by (metis TA_def assms(2) i nth_mem)}
  then have "ts = qs'" using qs(3) qs'
    by (simp add: ‹⋀i. i < length ts ⟹ ts ! i = qs' ! i› nth_equalityI) 
  with step1 show ?case by argo
qed (fastforce)

lemma ta_eps_Inl:
  assumes "(Inl q⇩1, Inl q⇩2) ∈ (ta_eps (trs_to_ta_A R))⇧*"
  shows "q⇩1 = q⇩2"
  using assms 
proof (induction rule: rtranclE)
  case (step y)
  hence "(y, Inl q⇩2) ∉ ta_eps (trs_to_ta_A R)" unfolding trs_to_ta_A_def by auto
  with step show ?case by auto
qed (blast)

lemma adpvars_A':
  assumes "ground s" "ground_trs R" "Inr q ∈ ta_res (trs_to_ta_A R) (adapt_vars s)"
  shows "(s, q) ∈ R"
  using assms(3,2,1) 
proof (induction s arbitrary: q rule:ta_res.induct)
  case (2 TA f ts)
  define TA where "TA = (trs_to_ta_A R)"
  with 2 obtain q' qs where qs:
    "(f qs → q') ∈ ta_rules TA"
    "(q',Inr q) ∈ ((ta_eps TA)^*)" 
    "length qs = length ts " 
    "∀ i < length ts. qs ! i ∈ (ta_res TA (adapt_vars (ts! i)))" 
    by auto
  moreover obtain qs' where qs':"qs = map Inl qs'" using qs(1) unfolding TA_def trs_to_ta_A_def cmn_ta_rules_G_def
    by fastforce
  hence q':"q' = Inl (Fun f qs')" using qs(1)  unfolding TA_def trs_to_ta_A_def cmn_ta_rules_G_def
    by force
  hence step1:"(Fun f qs', q) ∈ R" using qs(2) unfolding TA_def
    by (smt Inr_inject TA_def TRS_GTT.trs_to_ta_A_def mem_Collect_eq prod.sel(1) prod.sel(2) qs(2) rtranclE sum.simps(4) ta_eps_Inl ta_make_simps(2))
  moreover have "q' ∈ ta_res TA (adapt_vars (Fun f ts))"
    using qs(1) 
  proof -
    have "(f qs → q') ∈ ta_rules TA"
    "(q',q') ∈ ((ta_eps TA)^*)" 
      "∀ i < length ts. qs ! i ∈ (ta_res TA (adapt_vars (ts! i)))" 
      using qs qs(1) by blast+
    then show ?thesis using qs(3) by auto
  qed
      hence "Fun f ts = Fun f qs'" using q' adpvars_A[OF assms(1,2)]
    using "2.prems"(3) TA_def adpvars_A assms(2) by blast 
  then show ?case using step1 par_rstep_def 
    using par_rstep_id by blast
qed (fastforce)


lemma conv_adpvars_G:
  assumes "ground s" "s ⊴ t ∧ t ∈ TRS_terms R"
  shows "Inl s ∈ ta_res (trs_to_ta_A R) (adapt_vars s)"
  using assms
proof (induction s)
  case (Fun f  ss)
  have 0:"∀i < length ss. (map (ta_res (trs_to_ta_A R)) (map adapt_vars ss))!i 
                                = (ta_res (trs_to_ta_A R) (adapt_vars (ss!i)))"
    by simp
    hence 1:"adapt_vars (Fun f ss) = Fun f (map adapt_vars ss)" by force
  {fix i
    assume i: "i < length ss"
    hence "ground (ss!i)" using Fun(2) by simp
    moreover have "(ss!i) ⊴ t ∧ t ∈ TRS_terms R" using Fun(3)
      by (meson ‹i < length ss› nth_mem supteq.refl supteq.subt supteq_trans) 
    moreover have "adapt_vars (ss!i) = (ss!i)" 
      by (simp add: adapt_vars_id calculation(1))
    ultimately have "Inl (ss!i) ∈ ta_res (trs_to_ta_A R) (adapt_vars (ss!i))"
      using Fun(1) i by fastforce} note ref = this
  have "f (map Inl ss) →  Inl (Fun f ss) ∈ ta_rules (trs_to_ta_A R)"
    unfolding trs_to_ta_A_def cmn_ta_rules_G_def  TRS_terms_def
    by (metis (mono_tags, lifting) CollectI Fun.prems(2) TRS_terms_def ta_make_simps(1)) 
  thus ?case
  proof -
    have "(∀ i < length ss. (map Inl ss) ! i ∈ (map (ta_res (trs_to_ta_A R)) (map adapt_vars ss))!i)"
      using ref by simp
    moreover have "f (map Inl ss) →  Inl (Fun f ss) ∈ ta_rules (trs_to_ta_A R)"
      by (simp add: ‹f map Inl ss → Inl (Fun f ss) ∈ ta_rules (trs_to_ta_A R)›)
    ultimately show ?thesis using 1 by force
  qed
qed (fastforce)

(*OF B*)

lemma adpvars_B: 
  assumes "ground s" "ground_trs R" "Inr q ∈ ta_res (trs_to_ta_B R) (adapt_vars s)"
  shows "q = s"
  using assms(3,2,1) 
proof (induction s arbitrary: q rule:ta_res.induct)
   case (2 TA f ts)
  define TA where "TA = (trs_to_ta_B R)"
  with 2 obtain q' qs where qs:
    "(f qs → q') ∈ ta_rules TA"
    "(q',Inr q) ∈ ((ta_eps TA)^*)" 
    "length qs = length ts " 
    "∀ i < length ts. qs ! i ∈ (ta_res TA (adapt_vars (ts! i)))" 
    by auto
  have q:"q' = Inr q"
  proof -
    obtain ss :: "((('a, 'b) Term.term + ('a, 'b) Term.term) × (('a, 'b) Term.term + ('a, 'b) Term.term)) set ⇒ ('a, 'b) Term.term + ('a, 'b) Term.term ⇒ ('a, 'b) Term.term + ('a, 'b) Term.term ⇒ ('a, 'b) Term.term + ('a, 'b) Term.term" where
      f1: "∀x0 x1 x2. (∃v3. (x2, v3) ∈ x0⇧* ∧ (v3, x1) ∈ x0) = ((x2, ss x0 x1 x2) ∈ x0⇧* ∧ (ss x0 x1 x2, x1) ∈ x0)"
      by moura
    have "(q', ss (ta_eps TA) (Inr q) q') ∉ (ta_eps TA)⇧* ∨ (ss (ta_eps TA) (Inr q) q', Inr q) ∉ ta_eps TA"
      by (simp add: TA_def TRS_GTT.trs_to_ta_B_def)
    then show ?thesis
      using f1 by (meson qs(2) rtranclD tranclD2)
  qed
  moreover obtain qs' where qs':"qs = map Inr qs'" using qs(1) unfolding TA_def trs_to_ta_B_def cmn_ta_rules_D_def
    by fastforce
  hence "q' = Inr (Fun f qs')" using qs(1)  unfolding TA_def trs_to_ta_B_def cmn_ta_rules_D_def
    by force
  hence step1:"q = Fun f qs'"  using q by blast
  {fix i
    assume i:"i < length ts"
    hence "Inr (qs'!i) ∈ (ta_res TA (adapt_vars (ts! i)))" 
      using qs(3,4) qs' by fastforce
    moreover have "ground (ts!i)" using ground_recur[OF 2(4) i].
    ultimately have "(ts!i) = (qs'!i)" using 2(1) 
      by (metis TA_def assms(2) i nth_mem)}
  then have "ts = qs'" using qs(3) qs'
    by (simp add: ‹⋀i. i < length ts ⟹ ts ! i = qs' ! i› nth_equalityI) 
  with step1 show ?case by argo
qed (fastforce)

lemma adpvars_B': 
  assumes "ground s" "ground_trs R" "Inl q ∈ ta_res (trs_to_ta_B R) (adapt_vars s)"
  shows "(q, s) ∈ R"
  using assms(3,2,1) 
proof (induction s arbitrary: q rule:ta_res.induct)
  case (2 TA f ts)
  define TA where "TA = (trs_to_ta_B R)"
  with 2 obtain q' qs where qs:
    "(f qs → q') ∈ ta_rules TA"
    "(q',Inl q) ∈ ((ta_eps TA)^*)" 
    "length qs = length ts " 
    "∀ i < length ts. qs ! i ∈ (ta_res TA (adapt_vars (ts! i)))" 
    by auto
  moreover obtain qs' where qs':"qs = map Inr qs'" using qs(1) unfolding TA_def trs_to_ta_B_def cmn_ta_rules_D_def
    by fastforce
  hence q':"q' = Inr (Fun f qs')" using qs(1)  unfolding TA_def trs_to_ta_B_def cmn_ta_rules_D_def
    by force
  hence step1:"( q, Fun f qs') ∈ R" using qs(2) unfolding   TA_def trs_to_ta_B_def
    by (smt Inl_Inr_False Inl_inject Inr_inject mem_Collect_eq prod.sel(1) prod.sel(2) rtranclE ta_make_simps(2))

  moreover have "q' ∈ ta_res TA (adapt_vars (Fun f ts))"
    using qs(1) 
  proof -
    have "(f qs → q') ∈ ta_rules TA"
    "(q',q') ∈ ((ta_eps TA)^*)" 
      "∀ i < length ts. qs ! i ∈ (ta_res TA (adapt_vars (ts! i)))" 
      using qs qs(1) by blast+
    then show ?thesis using qs(3) by auto
  qed
  hence "Fun f ts = Fun f qs'" using q' adpvars_A[OF assms(1,2)]
    using "2.prems"(3) TA_def adpvars_B assms(2) by blast 
  then show ?case using step1 par_rstep_def 
    using par_rstep_id by blast
qed (fastforce)

lemma conv_adpvars_D:
  assumes "ground s" "s ⊴ t ∧ t ∈ TRS_terms R"
  shows "Inr s ∈ ta_res (trs_to_ta_B R) (adapt_vars s)"
  using assms 
proof (induction s)
  case (Fun f  ss)
  have 0:"∀i < length ss. (map (ta_res (trs_to_ta_B R)) (map adapt_vars ss))!i 
                                = (ta_res (trs_to_ta_B R) (adapt_vars (ss!i)))"
    by simp
    hence 1:"adapt_vars (Fun f ss) = Fun f (map adapt_vars ss)" by force
  {fix i
    assume i: "i < length ss"
    hence "ground (ss!i)" using Fun(2) by simp
    moreover have "(ss!i) ⊴ t ∧ t ∈ TRS_terms R" using Fun(3)
      by (meson ‹i < length ss› nth_mem supteq.refl supteq.subt supteq_trans) 
    moreover have "adapt_vars (ss!i) = (ss!i)" 
      by (simp add: adapt_vars_id calculation(1))
    ultimately have "Inr (ss!i) ∈ ta_res (trs_to_ta_B R) (adapt_vars (ss!i))"
      using Fun(1) i by fastforce} note ref = this
  have "f (map Inr ss) →  Inr (Fun f ss) ∈ ta_rules (trs_to_ta_B R)"
    unfolding trs_to_ta_A_def TRS_terms_def
    by (metis (mono_tags, lifting) CollectI Fun.prems(2) cmn_ta_rules_D_def  ta_make_simps(1) trs_to_ta_B_def)
    thus ?case
  proof -
    have "(∀ i < length ss. (map Inr ss) ! i ∈ (map (ta_res (trs_to_ta_B R)) (map adapt_vars ss))!i)"
      using ref by simp
    moreover have "f (map Inr ss) →  Inr (Fun f ss) ∈ ta_rules (trs_to_ta_B R)"
      
      by (simp add: ‹f map Inr ss → Inr (Fun f ss) ∈ ta_rules (trs_to_ta_B R)›)
    ultimately show ?thesis using 1 by force
  qed
qed (fastforce)

(*Now model above using TRS_GTT*)

lemma rstep_to_gtt_accept:
  assumes "ground_trs R" "ground u" "ground v" "(u, v) ∈ (rstep R)"
  shows "gtt_accept (trs_to_ta_A R, trs_to_ta_B R) (adapt_vars u) (adapt_vars v)"
  using assms(4,3,2,1)
proof (induction rule: rstepE)
   case (rstep s' t' C σ s t)
   let ?𝒢 = "(trs_to_ta_A R, trs_to_ta_B R)"
   let ?C = "adapt_vars_ctxt C"
   let ?s = "adapt_vars s"
   let ?t = "adapt_vars t"
   have grnd_s_t:"ground s" "ground t" using rstep(3,8) unfolding ground_trs_def by fastforce+
   hence 1:"Inr t ∈ ta_res (trs_to_ta_A R) (adapt_vars s)"
   proof -
     from rstep have "(Inl s, Inr t) ∈ ta_eps (trs_to_ta_A R)" unfolding trs_to_ta_A_def cmn_ta_rules_G_def
       by (metis (mono_tags, lifting) mem_Collect_eq ta_make_simps(2))  
     hence s_res:"(Inr t) ∈ ta_res (trs_to_ta_A R) (Var (Inl s))" by auto
     have "Inl s ∈ ta_res (trs_to_ta_A R) (adapt_vars s)"
       using grnd_s_t(1) rstep(3) conv_adpvars_G[of s s R] 
       unfolding TRS_terms_def TRS_fst_def by auto
     hence loc:"Var (Inl s) ∈ ta_res' (trs_to_ta_A R) (adapt_vars s)"
       using ta_res_res'_inclusion[of "Inl s" "(trs_to_ta_A R)" "adapt_vars s"] by blast
     thus ?thesis using ta_res'_ta_res[OF "loc" "s_res"] by argo
   qed   
   hence 2:"(Inr t) ∈ ta_res (trs_to_ta_B R) (adapt_vars t)"
   proof -
     have t_res:"(Inr t) ∈ ta_res (trs_to_ta_B R) (Var (Inr t))"
       unfolding trs_to_ta_B_def trs_to_ta_B_def using rule by simp  
     have "Inr t ∈ ta_res (trs_to_ta_B R) (adapt_vars t)"
       using grnd_s_t(2) rstep(3) conv_adpvars_D[of t t R] 
       unfolding TRS_terms_def TRS_snd_def by auto
     hence loc:"Var (Inr t) ∈ ta_res' (trs_to_ta_B R) (adapt_vars t)"
       using ta_res_res'_inclusion[of "Inr t" "(trs_to_ta_B R)" "adapt_vars t"] by blast
     thus ?thesis using ta_res'_ta_res[OF "loc" "t_res"]  by argo
   qed
  with 1 have IH:"gtt_accept (trs_to_ta_A R, trs_to_ta_B R) (adapt_vars s) (adapt_vars t)"
     by force
   moreover have u_v:"u = C⟨s⟩" "v = C⟨t⟩"  using grnd_s_t ground_subst_apply rstep(1,2,4,5) by metis+
   ultimately have "gtt_accept' ?𝒢 (adapt_vars u) (adapt_vars v)"
      proof -
     have loc:"(?C)⟨?s⟩  = adapt_vars u"
          "(?C)⟨?t⟩  = adapt_vars v"
       using u_v by simp+
     moreover have "fill_holes (mctxt_of_ctxt ?C) [?s] = ?C⟨?s⟩"
                   "fill_holes (mctxt_of_ctxt ?C) [?t] = ?C⟨?t⟩"
                          using fill_holes_mctxt_of_ctxt by blast+
     ultimately show ?thesis 
       using accept'_closed_ctxt[of "[adapt_vars s]" "[adapt_vars t]" "?𝒢" 
            "mctxt_of_ctxt (adapt_vars_ctxt C)"] 
             IH
       by (simp add:loc gtt_accept_equiv) 
   qed
   thus ?thesis using gtt_accept_equiv by blast
 qed

lemma par_rstep_to_gtt_accept:
  assumes "ground_trs R" "ground u" "ground v" "(u, v) ∈ (par_rstep R)"
  shows "gtt_accept (trs_to_ta_A R, trs_to_ta_B R) (adapt_vars u) (adapt_vars v)"
  using assms(4,3,2,1)
proof (induction rule:par_rstep.induct)
  case (root_step s t σ)
  hence "s⋅ σ = s" "t⋅ σ = t" unfolding ground_trs_def
    by (metis case_prodD ground_subst_apply)+  
  then show ?case using rstep_to_gtt_accept[of R s t] 
    by (metis root_step.hyps root_step.prems(1) root_step.prems(2) root_step.prems(3) rstep_rule)
next
  case (par_step_fun ts ss f)
  {fix i
   assume i: "i < length ts"
   hence "ground (ts!i)" "ground (ss!i)" using par_step_fun(2,4,5) 
     by auto 
   with i have "gtt_accept (trs_to_ta_A R, trs_to_ta_B R) (adapt_vars (ss!i)) (adapt_vars (ts!i))"
     using par_step_fun(3,6) by blast}
  then have "gtt_accept (trs_to_ta_A R, trs_to_ta_B R) 
            (Fun f (map adapt_vars ss)) (Fun f (map adapt_vars ts))"
     using par_step_fun(2) by auto 
   then show ?case by simp
qed (blast)

lemma gtt_accept_to_rstep:
  assumes "ground_trs R" "ground s" "ground t" "gtt_accept (trs_to_ta_A R, trs_to_ta_B R) s t"
  shows  "(adapt_vars s, adapt_vars t) ∈ (par_rstep R)"
  using assms(4,3,2,1)
proof (induction rule:gtt_accept.induct)
  case (refl t)
  then show ?case
    using adapt_vars_inj by blast
next
  case (join q s t)
  have "is_Inl q ∨ is_Inr q" unfolding is_Inl_def is_Inr_def
    by (meson sum.exhaust_sel) 
  then show ?case  
   proof (rule disjE, goal_cases Inl Inr)
     case Inl
     then obtain q' where q':"q = Inl q'" unfolding is_Inl_def by presburger
     then have "q' = adapt_vars s" using adpvars_A
       by (metis adapt_vars_adapt_vars fstI ground_adapt_vars join.hyps(1) join.prems(2) join.prems(3))
     moreover have "(q',adapt_vars t) ∈ R" using adpvars_B'
       by (metis adapt_vars_adapt_vars ground_adapt_vars join.hyps(2) join.prems(1) join.prems(3) q' sndI)        
     ultimately show ?case  using par_rstep_id by blast
   next
     case Inr
   then obtain q' where q':"q = Inr q'" unfolding is_Inr_def by presburger
   then have "q' = adapt_vars t" using adpvars_B
     by (metis adapt_vars_adapt_vars ground_adapt_vars join.hyps(2) join.prems(1) join.prems(3) prod.sel(2))
   moreover have "(adapt_vars s, q') ∈ R" using adpvars_A'
     by (metis adapt_vars_adapt_vars fstI ground_adapt_vars join.hyps(1) join.prems(2) join.prems(3) q')
     ultimately show ?case  using par_rstep_id by blast
   qed
next
  case (ctxt ss ts f)
  {fix i
    assume i:"i < length ss"
    hence "ground (ss!i)" "ground (ts!i)" using ctxt(1,3,4) by simp+
    hence "(adapt_vars (ss!i), adapt_vars (ts!i)) ∈ par_rstep R"
      using ctxt(2,5) using i by blast}
  hence "(Fun f (map adapt_vars ss), Fun f (map adapt_vars ts)) ∈ par_rstep R"
    using ctxt(1) by auto
  then show ?case by force
qed

end