Theory Non_Confluence

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2014)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2014, 2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Non_Confluence
imports 
  Usable_Rules_NJ
  "../Termination_and_Complexity/Semantic_Labeling"
  "../Orderings/Argument_Filter"
  "Check-NT.Name"
begin

lemma modularity_of_non_confluence: fixes R :: "('f,'v)trs" 
  assumes nCR: "¬ CR (rstep R)"
  and wfR: "⋀ l r. (l,r) ∈ R ⟹ vars_term r ⊆ vars_term l"
  and wfS: "⋀ l r. (l,r) ∈ S ⟹ is_Fun l"
  and disj: "funas_trs R ∩ funas_trs S = {}"
  and fin: "finite (funas_trs R ∪ funas_trs S)"
  and inf: "infinite (UNIV :: 'f set)"
  shows "¬ CR (rstep (R ∪ S))"
proof -
  def F ≡ "funas_trs R"
  def G ≡ "funas_trs S"
  from F_def have R: "funas_trs R ⊆ F" by auto
  from G_def have S: "funas_trs S ⊆ G" by auto
  from nCR obtain s t u where stR: "(s,t) ∈ (rstep R)^*" and suR: "(s,u) ∈ (rstep R)^*"
    and tu: "(t,u) ∉ join (rstep R)" unfolding CR_on_def by blast
  def H ≡ "funas_term s - F"
  have "finite (fst ` (F ∪ G ∪ H))" unfolding H_def F_def G_def using finite_funas_term[of s] fin by auto
  from finite_fresh_names_infinite_univ[OF this inf] obtain f g where fg: "⋀ x. x ∈ fst ` (F ∪ G ∪ H) ⟹
    f x ∉ fst ` (F ∪ G ∪ H) ∧ g (f x) = x" by blast
  def ren ≡ "λ (h,n). if (h,n) ∈ F then h else f h"
  def H' ≡ "((λ(h, y). (f h, y)) ` H)"
  let ?m = "map_funs_term_wa ren"
  have id: "⋀ g n. (g,n) ∈ F ⟹ ren (g,n) = g"
    unfolding ren_def by force
  have mR: "map_funs_trs_wa ren R = R"
    by (rule map_funs_trs_wa_funas_trs_id[OF R id])
  from map_funs_trs_wa_rsteps[OF stR, of ren] map_funs_trs_wa_rsteps[OF suR, of ren]
  have st: "(?m s, ?m t) ∈ (rstep R)^*" and su: "(?m s, ?m u) ∈ (rstep R)^*" unfolding mR .
  have sFH: "funas_term s ⊆ F ∪ H" unfolding H_def by blast
  hence "funas_term (?m s) ⊆ (λ(f, y). (ren (f,y), y)) ` (F ∪ H)" unfolding funas_term_map_funs_term_wa by blast
  also have "… = F ∪ ((λ(f, y). (ren (f,y), y)) ` H)" using id by force
  also have "… ⊆ F ∪ H'" unfolding H'_def ren_def by force
  finally have fs: "funas_term (?m s) ⊆ F ∪ H'" by auto
  from R have RH: "funas_trs R ⊆ F ∪ H'" by auto
  from rsteps_preserve_funas_terms_var_cond[OF RH fs st wfR] have ft: "funas_term (?m t) ⊆ F ∪ H'" .
  from rsteps_preserve_funas_terms_var_cond[OF RH fs su wfR] have fu: "funas_term (?m u) ⊆ F ∪ H'" .
  from su have su: "(?m s, ?m u) ∈ (rstep (R ∪ S))^*" unfolding rstep_union by regexp
  from st have st: "(?m s, ?m t) ∈ (rstep (R ∪ S))^*" unfolding rstep_union by regexp
  {
    fix v
    assume tv: "(?m t, v) ∈ (rstep (R ∪ S))^*" and uv: "(?m u, v) ∈ (rstep (R ∪ S))^*"
    {
      fix t
      have "(t,v) ∈ (rstep (R ∪ S))^* ⟹ funas_term t ⊆ F ∪ H' ⟹ (t,v) ∈ (rstep R)^*"
      proof (induct rule: rtrancl_induct)
        case (step u v)
        from rsteps_preserve_funas_terms_var_cond[OF RH step(4) step(3)[OF step(4)] wfR]
        have fu: "funas_term u ⊆ F ∪ H'" by auto
        from step(2)[unfolded rstep_union] have "(u,v) ∈ rstep R"
        proof
          assume "(u,v) ∈ (rstep S)"
          then obtain C l r σ where lr: "(l,r) ∈ S" and u: "u = C ⟨ l ⋅ σ ⟩" by auto
          from wfS[OF lr] obtain h ls where l: "l = Fun h ls" by (cases l, auto)
          let ?h = "(h,length ls)"
          from l lr S have hG: "?h ∈ G" unfolding funas_trs_def by (force simp: funas_rule_def)
          from fu[unfolded u l] have "?h ∈ F ∪ H'" by auto
          with disj hG have "?h ∈ H'" unfolding F_def G_def by auto
          from this[unfolded H'_def] obtain h' where h': "(h',length ls) ∈ H" and h: "h = f h'" by auto
          hence hfst: "h' ∈ fst ` (F ∪ G ∪ H)" by force
          from fg[OF hfst, folded h] hG have False by force
          thus ?thesis ..
        qed
        with step(3)[OF step(4)] show ?case by auto
      qed simp
    } note disjoint = this
    from disjoint[OF tv ft] have tv: "(?m t, v) ∈ (rstep R)^*" .
    from disjoint[OF uv fu] have uv: "(?m u, v) ∈ (rstep R)^*" .
    def ren' ≡ "λ (h,n). if (h,n) ∈ F then h else g h"
    let ?m' = "map_funs_term_wa ren'"
    have id: "⋀ g n. (g,n) ∈ F ⟹ ren' (g,n) = g"
      unfolding ren'_def by force
    have mR: "map_funs_trs_wa ren' R = R"
      by (rule map_funs_trs_wa_funas_trs_id[OF R id])
    have RH: "funas_trs R ⊆ F ∪ H" using R by auto
    {
      fix t
      assume t: "funas_term t ⊆ F ∪ H"
      have "?m' (?m t) = t"
        unfolding map_funs_term_wa_compose
      proof (rule map_funs_term_wa_funas_term_id[OF subset_refl], unfold split)
        fix h n
        assume "(h,n) ∈ funas_term t"
        hence "(h,n) ∈ F ∪ (H - F)" using t by auto
        thus "ren' (ren (h, n), n) = h"
        proof
          assume "(h,n) ∈ F"
          thus ?thesis unfolding ren_def ren'_def by auto
        next
          assume h: "(h,n) ∈ H - F"
          hence ren: "ren (h,n) = f h" unfolding ren_def by auto
          from h have "h ∈ fst ` (F ∪ G ∪ H)" by force
          from fg[OF this] have "(f h,n) ∉ F" "g (f h) = h" by force+
          thus ?thesis unfolding ren ren'_def by auto
        qed
      qed
    }
    note map_map = this[OF rsteps_preserve_funas_terms_var_cond[OF RH sFH _ wfR]]
    from map_funs_trs_wa_rsteps[OF tv, of ren'] map_funs_trs_wa_rsteps[OF uv, of ren']
    have tv: "(t, ?m' v) ∈ (rstep R)^*" and uv: "(u, ?m' v) ∈ (rstep R)^*" unfolding mR 
      using map_map[OF stR] map_map[OF suR] by auto
    from tv uv tu have False by auto
  }
  hence "(?m t, ?m u) ∉ join (rstep (R ∪ S))" by auto
  with st su show ?thesis by auto
qed
      

text ‹Formalization of some techniques Aoto's FroCoS'13 paper›

fun eval :: "('f,'c)inter ⇒ ('v,'c)assign ⇒ ('f,'v)term ⇒ 'c" where 
  "eval I α (Var x) = (α x)"
| "eval I α (Fun f ts) = I f (map (eval I α) ts)"

lemma eval_lab_eval[simp]: "fst (Semantic_Labeling.eval_lab I L LC α t) = eval I α t"
proof (induct t)
  case (Fun f ss)
  hence [simp]: "map (fst ∘ eval_lab I L LC α) ss = map (eval I α) ss" by auto
  show ?case by (simp add: Let_def)
qed simp

lemma wf_eval: assumes I: "wf_inter I C" and ass: "wf_assign C α"
  shows "eval I α t ∈ C"
proof (induct t)
  case (Var x)
  with ass show ?case unfolding wf_assign_def by auto
next
  case (Fun f ts)
  note I = I[unfolded wf_inter_def, rule_format]
  show ?case unfolding eval.simps
    by (rule I, insert Fun, auto)
qed

abbreviation qmodel_rule where "qmodel_rule I C cge l r ≡ ∀ α. wf_assign C α ⟶ cge (eval I α l) (eval I α r)"
definition qmodel where "qmodel I C cge R ≡ ∀ (l,r) ∈ R. qmodel_rule I C cge l r"

lemma qmodel_model[simp]: "Semantic_Labeling.qmodel I L LC C cge R = qmodel I C cge R"
  unfolding Semantic_Labeling.qmodel_def qmodel_def by auto

lemma sl_interpr: "c ∈ C ⟹ wf_inter I C ⟹ cge_wm I C cge ⟹ 
  sl_interpr C c I cge (λ _ _. op =) (λ _ _. ()) (λ x y z. (x,z)) id (λ _ _ _. True)"
  by (unfold_locales, auto simp: lge_wm lge_to_lgr_rel_def lge_to_lgr_def Let_def wf_label_def)

lemma sem_rewrites: fixes R' :: "('f,'v)trs"
  assumes steps: "(s,t) ∈ (rstep U)^*"
  and U: "U ⊆ R'"
  and wf_ass: "wf_assign C (α :: ('v,'c)assign)"
  and c: "c ∈ C"
  and wf_I: "wf_inter I C" 
  and wm: "cge_wm I C cge"
  and model: "qmodel I C cge R'"
  and refl: "⋀ c. c ∈ C ⟹ cge c c"
  and trans: "⋀ c d e. c ∈ C ⟹ d ∈ C ⟹ e ∈ C ⟹ cge c d ⟹ cge d e ⟹ cge c e"
  shows "cge (eval I α s) (eval I α t)"
proof -
  interpret sl_interpr C c I cge "λ _ _. op =" "λ _ _. ()" "(λ x y z. (x,z))" id "λ _ _ _. True"
    by (rule sl_interpr[OF c wf_I wm])
  have "Semantic_Labeling.qmodel I (λ_ _. ()) (λx y. Pair x) C cge R'" using model by simp
  from quasi_sem_rewrite[OF _ this wf_ass, unfolded eval_lab_eval, of _ _ False "{}"] rstep_mono[OF U]
  have eval: "⋀ s t. (s,t) ∈ rstep U ⟹ cge (eval I α s) (eval I α t)" by auto
  note wf = wf_eval[OF wf_I wf_ass]
  from steps
  show ?thesis
  proof (induct)
    case (step t u)
    show ?case 
      by (rule trans[OF wf wf wf step(3) eval[OF step(2)]])
  next
    case base
    show ?case by (rule refl[OF wf])
  qed
qed

abbreviation cgt where "cgt cge a b ≡ cge a b ∧ ¬ cge b a"

lemma aoto_theorem_2: (* we weakened > to not ≤ *)
  assumes model: "qmodel I C cge (Rs^-1 ∪ Rt)"
  and c: "c ∈ C"
  and wf_I: "wf_inter I C" 
  and wm: "cge_wm I C cge"
  and refl: "⋀ c. c ∈ C ⟹ cge c c"
  and trans: "⋀ c d e. c ∈ C ⟹ d ∈ C ⟹ e ∈ C ⟹ cge c d ⟹ cge d e ⟹ cge c e"
  and not_ge: "¬ cge (eval I (λ _ . c) t) (eval I (λ _ . c) s)" (is "¬ cge (eval _ ?ass _) _")
  (* before not_ge was [t] > [s] where > was defined as ≥ \ ≤ *)
  shows "¬ (∃ u. (s,u) ∈ (rstep Rs)^* ∧ (t,u) ∈ (rstep Rt)^*)"
proof
  let ?eval = "λ t. eval I ?ass t"
  assume "(∃ u. (s,u) ∈ (rstep Rs)^* ∧ (t,u) ∈ (rstep Rt)^*)"
  then obtain u where su: "(s,u) ∈ (rstep Rs)^*" and tu: "(t,u) ∈ (rstep Rt)^*" by auto
  have wf: "wf_assign C ?ass" unfolding wf_assign_def using c by auto
  from su have us: "(u,s) ∈ (rstep (Rs^-1))^*"
    unfolding reverseTrs[symmetric] rtrancl_converse by auto
  note sem = sem_rewrites[OF _ _ wf c wf_I wm model refl trans]
  note wf = wf_eval[OF wf_I wf]
  from sem[OF us] have us: "cge (?eval u) (?eval s)" by auto
  from sem[OF tu] have tu: "cge (?eval t) (?eval u)" by auto
  from trans[OF wf wf wf tu us] have ts: "cge (?eval t) (?eval s)" .
  with not_ge show False by auto
qed

lemma aoto_theorem_10: (* we weakened > to not ≤ *)
  assumes model: "qmodel I C cge ((usable_rules_reach R s)^-1 ∪ usable_rules_reach R t)"
  and c: "c ∈ C"
  and wf_I: "wf_inter I C" 
  and wm: "cge_wm I C cge"
  and refl: "⋀ c. c ∈ C ⟹ cge c c"
  and trans: "⋀ c d e. c ∈ C ⟹ d ∈ C ⟹ e ∈ C ⟹ cge c d ⟹ cge d e ⟹ cge c e"
  and not_ge: "¬ cge (eval I (λ _ . c) t) (eval I (λ _ . c) s)" (is "¬ cge (eval _ ?ass _) _")
  (* before not_ge was [t] > [s] where > was defined as ≥ \ ≤ *)
  shows "(s,t) ∉ join (rstep R)"
  using usable_rules_reach_nj[OF aoto_theorem_2[OF model c wf_I wm refl trans not_ge]]
  by auto

lemma aoto_theorem_10_af: (* not present in Aoto, but simple consequence *)
  assumes model: "qmodel I C cge ((usable_rules_reach (af_rule π ` (usable_rules_reach R s)) (af_term π s))^-1 ∪ 
    usable_rules_reach (af_rule π ` (usable_rules_reach R t)) (af_term π t))"
  and c: "c ∈ C"
  and wf_I: "wf_inter I C" 
  and wm: "cge_wm I C cge"
  and refl: "⋀ c. c ∈ C ⟹ cge c c"
  and trans: "⋀ c d e. c ∈ C ⟹ d ∈ C ⟹ e ∈ C ⟹ cge c d ⟹ cge d e ⟹ cge c e"
  and not_ge: "¬ cge (eval I (λ _ . c) (af_term π t)) (eval I (λ _ . c) (af_term π s))" (is "¬ cge (eval _ ?ass _) _")
  (* before not_ge was [t] > [s] where > was defined as ≥ \ ≤ *)
  shows "(s,t) ∉ join (rstep R)"
  using usable_rules_reach_nj[OF argument_filter_nj[OF usable_rules_reach_nj[OF aoto_theorem_2[OF model c wf_I wm refl trans not_ge]]]] by auto
  
lemma aoto_corollary_6: (* we show that this is an instance of theorem 10 *)
  assumes model: "qmodel I C (op =) (usable_rules_reach R s ∪ usable_rules_reach R t)"
  and c: "c ∈ C"
  and wf_I: "wf_inter I C" 
  and neg: "eval I (λ _ . c) s ≠ eval I (λ _ . c) t" (is "eval _ ?ass _ ≠ _")
  shows "(s,t) ∉ join (rstep R)"
proof -
  interpret usable_rules_reachability R .
  {
    fix l r
    note model = model[unfolded qmodel_def, rule_format]
    assume "(l,r) ∈ (Ur s)^-1 ∪ Ur t"
    hence "(l,r) ∈ Ur s ∪ Ur t ∨ (r,l) ∈ Ur s ∪ Ur t" by auto
    with model[of "(l,r)"] model[of "(r,l)"]
    have "qmodel_rule I C (op =) l r" by auto
  }
  hence model: "qmodel I C (op =) ((Ur s)^-1 ∪ Ur t)"
    unfolding qmodel_def by auto
  show ?thesis by (rule aoto_theorem_10[OF model c wf_I], insert neg, auto simp: cge_wm)
qed


locale discrimination_pair = compat S NS (* we only require one side compatibility: ≥ o > ⊆ ≥ *)
  for S NS :: "('f,'v)trs" +
  assumes wm_NS: "ctxt.closed NS"
  and subst_NS: "subst.closed NS"
  and irrefl_S: "(t,t) ∉ S"
begin
lemma rstep_imp_NS: "R ⊆ NS ⟹ rstep R ⊆ NS"
  by (rule rstep_subset[OF wm_NS subst_NS])
end

lemma aoto_pre_theorem_12:
  assumes "discrimination_pair S NS"
  and s: "Rs^-1 ⊆ NS"
  and t: "Rt ⊆ NS"
  and st: "(s,t) ∈ S"
  shows "¬ (∃ u. (s,u) ∈ (rstep Rs)^* ∧ (t,u) ∈ (rstep Rt)^*)"
proof
  assume "(∃ u. (s,u) ∈ (rstep Rs)^* ∧ (t,u) ∈ (rstep Rt)^*)"
  then obtain u where su: "(s,u) ∈ (rstep Rs)^*" and tu: "(t,u) ∈ (rstep Rt)^*" by auto
  from su have us: "(u,s) ∈ (rstep (Rs^-1))^*" unfolding rtrancl_converse reverseTrs[symmetric] by simp
  interpret discrimination_pair S NS by fact
  from rtrancl_mono[OF rstep_imp_NS[OF s]] us have us: "(u,s) ∈ NS^*" by auto
  from rtrancl_mono[OF rstep_imp_NS[OF t]] tu have tu: "(t,u) ∈ NS^*" by auto
  from tu us have "(t,s) ∈ NS^*" by auto
  with st have "(t,t) ∈ NS^* O S" by auto
  with trCompat have "(t,t) ∈ S" by auto
  with irrefl_S show False by blast
qed
  
lemma aoto_theorem_12: 
  assumes pair: "discrimination_pair S NS"
  and s: "(usable_rules_reach R s)^-1 ⊆ NS"
  and t: "usable_rules_reach R t ⊆ NS"
  and st: "(s,t) ∈ S"
  shows "(s,t) ∉ join (rstep R)"
  using usable_rules_reach_nj[OF aoto_pre_theorem_12[OF pair s t st]] by auto

lemma aoto_theorem_14: 
  assumes pair: "discrimination_pair S NS"
  and s: "(usable_rules_reach (af_rule π ` (usable_rules_reach R s)) (af_term π s))^-1 ⊆ NS" 
  and t: "usable_rules_reach (af_rule π ` (usable_rules_reach R t)) (af_term π t) ⊆ NS"
  and st: "(af_term π s,af_term π t) ∈ S"
  shows "(s,t) ∉ join (rstep R)"
  using usable_rules_reach_nj[OF argument_filter_nj[OF usable_rules_reach_nj[OF aoto_pre_theorem_12[OF pair s t st]]]]
  by auto

lemma (in redtriple) discrimination_pair: "discrimination_pair S NS"
  by (unfold_locales, rule wm_NS, rule subst_NS, insert SN, fast)


end