Theory Trs_Impl

theory Trs_Impl
imports Term_Impl Matching Abstract_Rewriting_Impl Option_Util Map_Choice RBT_Map_Set_Extension Renaming_Interpretations
(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2011-2016)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2011-2015)
Author:  Thomas Sternagel <thomas.sternagel@uibk.ac.at> (2012)
License: LGPL (see file COPYING.LESSER)
*)
theory Trs_Impl
  imports
    Trs
    Term_Impl
    First_Order_Terms.Matching
    Abstract_Rewriting_Impl
    Auxx.Option_Util
    Auxx.Map_Choice
    "Transitive-Closure.RBT_Map_Set_Extension"
    Renaming_Interpretations
begin

type_synonym ('f, 'v) rules = "('f, 'v) rule list"

fun rewrite :: "('f, 'v) rules ⇒ ('f, 'v) term ⇒ ('f, 'v) term list"
where
  "rewrite R s = concat (map (λ (l, r) . concat (map (λ p.
    (case match (s |_ p) l of
      None ⇒ []
    | Some σ ⇒ [replace_at s p (r ⋅ σ)])) (poss_list s))) R)"

lemma rewrite_complete_main:
  fixes l r :: "('f, 'v) term"
  assumes "(s, t) ∈ rstep_r_p_s (set R) (l, r) p σ" 
  shows "∃u ∈ set (rewrite R s). vars_term l ⊇ vars_term r ⟶ u = t"
proof -
  let ?C = "ctxt_of_pos_term p s"
  from assms have lr: "(l,r) ∈ set R" 
    and p: "p ∈ poss s" 
    and s: "?C⟨l ⋅ σ⟩ = s"
    and t: "?C⟨r ⋅ σ⟩ = t"
    unfolding rstep_r_p_s_def by (auto simp: Let_def)
  from s p have "?C⟨l ⋅ σ⟩ = ?C⟨s|_p⟩" by (simp add: ctxt_supt_id)
  then have "l ⋅ σ = s|_p" by auto
  from this match_complete' obtain δ where 
    match: "match (s|_p) l = Some δ" and 
      vars: "∀ x ∈ vars_term l. σ x = δ x" by blast
  have l: "l ⋅ σ = l ⋅ δ"
    by (rule term_subst_eq, insert vars, auto)
  obtain u where u: "u = ?C⟨r ⋅ δ⟩" by auto
  {
    assume sub: "vars_term r ⊆ vars_term l"
    have "r ⋅ σ = r ⋅ δ"
      by (rule term_subst_eq, insert sub vars, auto)
    with t have "u = t" unfolding u by simp
  } note ut = this
  have nearlyDone: "(l,r) ∈ set R ∧ p ∈ poss s ∧ u ∈ set (case match (s|_p) l of None ⇒ [] | Some σ ⇒ [ ?C⟨r⋅σ⟩])" using lr p match unfolding u by auto 
  then have "u ∈ set ((λ(l, r). concat  (map 
     (λp. case match (s|_p) l  of None ⇒ [] | Some σ ⇒ [(ctxt_of_pos_term p s)⟨r ⋅ σ⟩])
                          (poss_list s)))  (l,r))" (is "_ ∈ (?P (l,r))")
    by auto
  with lr have "∃ lr ∈ set R. u ∈ (?P lr)" by blast
  then have "u ∈ set (rewrite R s)" by auto
  then show ?thesis using ut by (auto simp del:rewrite.simps)
qed

lemma rewrite_complete:
  fixes l r::"('f,'v)term"
  assumes "(s,t) ∈ rstep_r_p_s (set R) (l,r) p σ" 
  and "vars_term l ⊇ vars_term r"
  shows "t ∈ set (rewrite R s)"
  using rewrite_complete_main[OF assms(1)] using assms(2) by auto

lemma rewrite_sound:
  assumes "t ∈ set (rewrite R s)"
  shows "(s, t) ∈ rstep (set R)"
proof -
  from assms 
  have "∃ l r p.  (l,r) ∈ set R ∧ p ∈ poss s ∧ t ∈ set (case match (s|_p) l of None ⇒ [] | Some σ ⇒ [ (ctxt_of_pos_term p s)⟨r⋅σ⟩])" 
    by auto
  from this obtain l r p where one:
    "(l,r) ∈ set R ∧ p ∈ poss s ∧ t ∈ set (case match (s|_p) l of None ⇒ [] | Some σ ⇒ [ (ctxt_of_pos_term p s)⟨r⋅σ⟩])"
    by auto
  from this obtain σ where two: "match (s|_p) l = Some σ ∧ t ∈ {(ctxt_of_pos_term p s)⟨r⋅σ⟩}"
    by (cases "match (s|_p) l", auto)
  then have match: "l ⋅ σ = s|_p" using match_sound by auto 
  with one match one two have "(s,t) ∈ rstep_r_p_s (set R) (l,r) p σ" unfolding rstep_r_p_s_def by (simp add: Let_def ctxt_supt_id)
  then show "(s,t) ∈ rstep (set R)" unfolding rstep_iff_rstep_r_p_s by blast
qed

declare rewrite.simps[simp del]

lemma rewrite_iff_rstep:
  assumes "⋀ l r. (l,r) ∈ set R ⟹ vars_term l ⊇ vars_term r"
  shows "set (rewrite R s) = {t. (s,t) ∈ rstep (set R)}" (is "?l = ?r")
proof -
  {
    fix t
    assume "t ∈ ?l"
    from rewrite_sound[OF this] have "t ∈ ?r" by auto
  }
  moreover
  {
    fix t
    assume "t ∈ ?r"
    then have "(s,t) ∈ rstep (set R)" by auto
    from this[unfolded rstep_iff_rstep_r_p_s] obtain l r p σ where 
      st: "(s,t) ∈ rstep_r_p_s (set R) (l,r) p σ" by auto
    then have "(l,r) ∈ set R" unfolding rstep_r_p_s_def Let_def by auto
    from rewrite_complete[OF st assms[OF this]] have "t ∈ ?l" .
  }
  ultimately show ?thesis by auto
qed

definition first_rewrite :: "('f,'v)rules ⇒ ('f,'v)term ⇒ ('f,'v)term option"
  where "first_rewrite R s ≡ case rewrite R s of Nil ⇒ None | Cons t _ ⇒ Some t"

definition in_rstep_impl where 
  "in_rstep_impl s t R ≡ ∃ p ∈ set (poss_list s). p ∈ poss t ∧ ctxt_of_pos_term p s = ctxt_of_pos_term p t ∧ 
     (let sp = s |_ p; tp = t |_ p in ∃ lr ∈ R. match_list Var [(fst lr,sp), (snd lr,tp)] ≠ None)"

lemma in_rstep_code[code_unfold]: "(st ∈ rstep R) = (in_rstep_impl (fst st) (snd st) R)"
proof (cases st)
  case (Pair s t)
  show ?thesis unfolding Pair in_rstep_impl_def Let_def fst_conv snd_conv poss_list_sound
  proof -
    show "((s,t) ∈ rstep R) = 
      (∃p∈poss s. p ∈ poss t ∧ ctxt_of_pos_term p s = ctxt_of_pos_term p t ∧ (∃lr∈R. match_list Var [(fst lr, s |_ p), (snd lr, t |_ p)] ≠ None))"
      (is "?l = ?r")
    proof
      assume ?l
      from this[unfolded rstep_iff_rstep_r_p_s] obtain l r p σ
      where "(s, t) ∈ rstep_r_p_s R (l, r) p σ" by auto
      from this[unfolded rstep_r_p_s_def Let_def fst_conv snd_conv]
      have ps: "p ∈ poss s" and lr: "(l, r) ∈ R" and s: "(ctxt_of_pos_term p s)⟨l ⋅ σ⟩ = s" and t: "(ctxt_of_pos_term p s)⟨r ⋅ σ⟩ = t" by auto
      have pt: "p ∈ poss t" using ps s t 
        by (metis hole_pos_ctxt_of_pos_term hole_pos_poss)
      from ps pt have id: "ctxt_of_pos_term p s = ctxt_of_pos_term p t" unfolding t[symmetric]
        by (metis hole_pos_ctxt_of_pos_term hole_pos_id_ctxt)
      from s ps have sp: "s |_ p = l ⋅ σ" by (rule subt_at_ctxt_of_pos_term)
      from t ps have tp: "t |_ p = r ⋅ σ" by (metis hole_pos_ctxt_of_pos_term subt_at_hole_pos)
      let ?P = "[(l, s |_ p), (r, t |_ p)]"
      have "⋀ sa ta. (sa, ta) ∈ set ?P ⟹ sa ⋅ σ = ta" unfolding sp tp by auto
      from match_list_complete'[of ?P σ Var, OF this] have match: "match_list Var ?P ≠ None" by auto
      show ?r
        by (intro bexI conjI, rule pt, insert lr id match ps, auto)
    next
      assume ?r
      then obtain p lr where 
        ps: "p ∈ poss s" and
        pt: "p ∈ poss t" and
        id: "ctxt_of_pos_term p s = ctxt_of_pos_term p t" (is "?Cs = ?Ct") and
        lr: "lr∈R" and
        match: "match_list Var [(fst lr, s |_ p), (snd lr, t |_ p)] ≠ None" 
        by blast
      obtain l r where l_r: "lr = (l,r)" by force
      from lr l_r have lr: "(l,r) ∈ R" by simp
      from match l_r obtain σ where "match_list Var [(l, s|_p), (r, t|_p)] = Some σ" by force
      from match_list_sound[OF this, unfolded matchers_def] have sp: "l ⋅ σ = s |_ p" and tp: "r ⋅ σ = t |_ p" by auto
      from ps have s: "s = ?Cs ⟨ l ⋅ σ ⟩" unfolding sp by (metis ctxt_supt_id)
      from pt have t: "t = ?Cs ⟨ r ⋅ σ ⟩" unfolding tp id by (metis ctxt_supt_id)
      show ?l by (rule rstepI[OF lr s t])
    qed
  qed
qed

definition compute_rstep_NF :: "('f,'v)rules ⇒ ('f,'v)term ⇒ ('f,'v)term option"
  where "compute_rstep_NF R s ≡ compute_NF (first_rewrite R) s"

lemma compute_rstep_NF_sound:
  assumes res: "compute_rstep_NF R s = Some t"
  shows "(s, t) ∈ (rstep (set R))^*" using res[unfolded compute_rstep_NF_def]
proof (rule compute_NF_sound)
  fix s t
  assume "first_rewrite R s = Some t"
  from this[unfolded first_rewrite_def] obtain ts where "rewrite R s = t # ts"
    by (cases "rewrite R s", auto)
  then have t: "t ∈ set (rewrite R s)" by simp
  from rewrite_sound[OF this] show "(s,t) ∈ rstep (set R)" .
qed

lemma compute_rstep_NF_complete: assumes res: "compute_rstep_NF R s = Some t"
  shows "t ∈ NF (rstep (set R))" using res[unfolded compute_rstep_NF_def]
proof (rule compute_NF_complete)
  fix s
  assume "first_rewrite R s = None"
  from this[unfolded first_rewrite_def] have empty: "rewrite R s = []" 
    by (cases "rewrite R s", auto)
  show "s ∈ NF (rstep (set R))"
  proof(rule, rule)
    fix t
    assume "(s,t) ∈ rstep (set R)"
    from this[unfolded rstep_iff_rstep_r_p_s]
    obtain l r p σ where step: "(s,t) ∈ rstep_r_p_s (set R) (l,r) p σ" by auto
    from rewrite_complete_main[OF step] arg_cong[OF empty, of set] show False 
      by auto
  qed
qed

lemma compute_rstep_NF_SN: assumes SN: "SN (rstep (set R))"
  shows "∃ t. compute_rstep_NF R s = Some t"
proof -
  have "∃ t. compute_NF (first_rewrite R) s = Some t"
  proof (rule compute_NF_SN[OF SN])
    fix s t
    assume "first_rewrite R s = Some t"
    from this[unfolded first_rewrite_def] have
      rewrite: "t ∈ set (rewrite R s)" by (auto split: list.splits)
    from rewrite_sound[OF this]
    show "(s,t) ∈ rstep (set R)" .
  qed  
  then show ?thesis unfolding compute_rstep_NF_def .
qed

definition
  check_join_NF ::
    "('f :: showl, 'v :: showl) rules ⇒ 
     ('f, 'v) term ⇒ ('f, 'v) term ⇒ showsl check"
where
  "check_join_NF R s t ≡ case (compute_rstep_NF R s, compute_rstep_NF R t) of
      (Some s', Some t') ⇒ 
     check (s' = t') (
    showsl (STR ''the normal form '') ∘ showsl s' ∘ showsl (STR '' of '') ∘ showsl s 
      ∘ showsl (STR '' differs from⏎the normal form '') ∘ showsl t' ∘ showsl (STR '' of '') ∘ showsl t)
       |  _ ⇒ error (showsl (STR ''strange error in normal form computation''))"

lemma check_join_NF_sound:
  assumes ok: "isOK (check_join_NF R s t)"
  shows "(s, t) ∈ join (rstep (set R))"
proof -
  note ok = ok[unfolded check_join_NF_def]
  from ok obtain s' where s: "compute_rstep_NF R s = Some s'" by force
  note ok = ok[unfolded s]
  from ok obtain t' where t: "compute_rstep_NF R t = Some t'" by force
  from ok[unfolded t] have id: "s' = t'" by simp
  note seq = compute_rstep_NF_sound
  from seq[OF s] seq[OF t]
  show ?thesis unfolding id by auto
qed

fun reachable_terms :: 
  "('f, 'v) rules ⇒ ('f, 'v) term ⇒ nat ⇒ ('f, 'v) term list"
where 
  "reachable_terms R s 0 = [s]"
| "reachable_terms R s (Suc n) = (
  let ts = (reachable_terms R s n) in
    remdups (ts@(concat (map (λ t. rewrite R t) ts)))
  )"

lemma reachable_terms_nat:
assumes "t ∈ set (reachable_terms R s i)"
shows "∃ j. j ≤ i ∧ (s,t) ∈ (rstep (set R))^^j"
using assms
proof (induct i arbitrary: t)
  case 0 
  then show ?case by auto
next
  case (Suc i) 
  let ?R = "λ j. (rstep (set R))^^j"
  from Suc(2)
  have "t ∈ set (reachable_terms R s i)
    ∨ (∃ u ∈ set (reachable_terms R s i). t ∈ set (rewrite R u))" by (simp add: Let_def)
  then show ?case
  proof
    assume "t ∈ set (reachable_terms R s i)"
    from Suc(1)[OF this] obtain j where "j ≤ i" and "(s,t) ∈ ?R j" by auto 
    then show ?thesis by (intro exI[of _ j], auto)
  next
    assume "∃ u ∈ set (reachable_terms R s i). t ∈ set (rewrite R u)"
    then obtain u where u: "u ∈ set (reachable_terms R s i)"
      and 1: "t ∈ set (rewrite R u)" by auto
    from rewrite_sound[OF 1] have ut: "(u,t) ∈ rstep (set R)" by auto
    from Suc(1)[OF u] obtain j where j: "j ≤ i" and su: "(s,u) ∈ ?R j" by auto
    from su ut have "(s,t) ∈ ?R (Suc j)" by auto
    with j show ?thesis by (intro exI[of _ "Suc j"], auto)
  qed
qed

lemma reachable_terms:
assumes "t ∈ set (reachable_terms R s i)"
shows "(s,t) ∈ (rstep (set R))^*"
  using reachable_terms_nat[OF assms] by (metis relpow_imp_rtrancl)

lemma reachable_terms_one:
  assumes "t ∈ set (reachable_terms R s (Suc 0))"
  shows "(s,t) ∈ (rstep (set R))^="
proof -
  from reachable_terms_nat[OF assms] obtain j where "j ≤ 1"
  and "(s,t) ∈ (rstep (set R))^^j" by auto
  then show ?thesis by (cases j, auto)
qed


function iterative_join_search_main ::
  "('f,'v) rules ⇒ ('f,'v) term ⇒ ('f,'v) term ⇒ nat ⇒ nat ⇒ bool"
where
  "iterative_join_search_main R s t i n = (if i ≤ n then
  (((list_inter (reachable_terms R s i) (reachable_terms R t i)) ≠ []) ∨ (iterative_join_search_main R s t (Suc i) n)) else False)"
by pat_completeness auto

termination by (relation "measure ( λ (R,s,t,i,n). Suc n - i)") auto

lemma iterative_join_search_main: 
  "iterative_join_search_main R s t i n ⟹ (s,t) ∈ join (rstep (set R))"
proof (induction rule: iterative_join_search_main.induct)
  case (1 R s t i n)
  from 1(2) have i_n: "i ≤ n" by (simp split: if_splits)
  note IH = 1(1)[OF i_n]
  let ?I = "list_inter (reachable_terms R s i) (reachable_terms R t i)"
  from 1(2) i_n have "?I ≠ [] ∨ iterative_join_search_main R s t (Suc i) n" by auto
  then show ?case
  proof
    assume a: "?I ≠ []"
    then obtain u us where u: "?I = u # us" by (cases ?I, auto)
    then have d: "u ∈ set ?I" by auto
    from this[simplified] reachable_terms[of u _ _ i] have c: "(s, u) ∈ (rstep (set R))*" by auto
    from d[simplified] reachable_terms[of u _ _ i] have e: "(t,u) ∈ (rstep (set R))^*" by auto
    from c e show ?thesis by auto
  next
    assume b: "iterative_join_search_main R s t (Suc i) n"
    from  IH[OF this] show ?thesis .
  qed
qed

definition iterative_join_search where 
  "iterative_join_search R s t n ≡ iterative_join_search_main R s t 0 n"

lemma iterative_join_search: "iterative_join_search R s t n ⟹ (s,t) ∈ join (rstep (set R))"
  by (rule iterative_join_search_main, unfold iterative_join_search_def)

definition
  check_join_BFS_limit ::
    "nat ⇒ ('f :: showl, 'v :: showl) rules ⇒ 
     ('f, 'v) term ⇒ ('f, 'v) term ⇒ showsl check"
where
  "check_join_BFS_limit n R s t ≡ check (iterative_join_search R s t n) 
    (showsl (STR ''could not find a joining sequence of length at most '') ∘ 
     showsl n ∘ showsl (STR '' for the terms '') ∘ showsl s ∘ 
     showsl (STR '' and '') ∘ showsl t ∘ showsl_nl)"

lemma check_join_BFS_limit_sound:
  assumes ok: "isOK (check_join_BFS_limit n R s t)"
  shows "(s, t) ∈ join (rstep (set R))"
  by (rule iterative_join_search, insert ok[unfolded check_join_BFS_limit_def], simp)

definition map_funs_rules :: "('f ⇒ 'g) ⇒ ('f, 'v) rules ⇒ ('g, 'v) rules" where
  "map_funs_rules fg R = map (map_funs_rule fg) R"

lemma map_funs_rules_sound[simp]:
  "set (map_funs_rules fg R) = map_funs_trs fg (set R)"
  unfolding map_funs_rules_def map_funs_trs.simps by simp


subsection ‹Output›

fun showsl_rule' :: "('f ⇒ showsl) ⇒ ('v ⇒ showsl) ⇒ String.literal ⇒ ('f, 'v) rule ⇒ showsl"
where
  "showsl_rule' fun var arr (l, r) =
    showsl_term' fun var l ∘ showsl arr ∘ showsl_term' fun var r"

definition "showsl_rule ≡ showsl_rule' showsl showsl (STR '' -> '')"
definition "showsl_weak_rule ≡ showsl_rule' showsl showsl (STR '' ->= '')"

definition
  showsl_rules' :: "('f ⇒ showsl) ⇒ ('v ⇒ showsl) ⇒ String.literal ⇒ ('f, 'v) rules ⇒ showsl"
where
  "showsl_rules' fun var arr trs =
    showsl_list_gen (showsl_rule' fun var arr) (STR '''') (STR '''') (STR ''⏎'') (STR '''') trs ∘ showsl_nl"

definition "showsl_rules ≡ showsl_rules' showsl showsl (STR '' -> '')"
definition "showsl_weak_rules ≡ showsl_rules' showsl showsl (STR '' ->= '')"

definition
  showsl_trs' :: "('f ⇒ showsl) ⇒ ('v ⇒ showsl) ⇒ String.literal ⇒ String.literal ⇒ ('f, 'v) rules ⇒ showsl"
where
  "showsl_trs' fun var name arr R = showsl name ∘ showsl (STR ''⏎⏎'') ∘ showsl_rules' fun var arr R"

definition "showsl_trs ≡ showsl_trs' showsl showsl (STR ''rewrite system:'') (STR '' -> '')"

definition add_vars_rule :: "('f, 'v) rule ⇒ 'v list ⇒ 'v list"
where
  "add_vars_rule r xs = add_vars_term (fst r) (add_vars_term (snd r) xs)"

definition add_funs_rule :: "('f, 'v) rule ⇒ 'f list ⇒ 'f list"
where
  "add_funs_rule r fs = add_funs_term (fst r) (add_funs_term (snd r) fs)"

definition add_funas_rule :: "('f, 'v) rule ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
  "add_funas_rule r fs = add_funas_term (fst r) (add_funas_term (snd r) fs)"

definition add_roots_rule :: "('f, 'v) rule ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
  "add_roots_rule r fs = root_list (fst r) @ root_list (snd r) @ fs"

definition add_funas_args_rule :: "('f, 'v) rule ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
  "add_funas_args_rule r fs = add_funas_args_term (fst r) (add_funas_args_term (snd r) fs)"

lemma add_vars_rule_vars_rule_list_conv [simp]:
  "add_vars_rule r xs = vars_rule_list r @ xs"
  by (simp add: add_vars_rule_def vars_rule_list_def)

lemma add_funs_rule_funs_rule_list_conv [simp]:
  "add_funs_rule r fs = funs_rule_list r @ fs"
  by (simp add: add_funs_rule_def funs_rule_list_def)

lemma add_funas_rule_funas_rule_list_conv [simp]:
  "add_funas_rule r fs = funas_rule_list r @ fs"
  by (simp add: add_funas_rule_def funas_rule_list_def)

lemma add_roots_rule_roots_rule_list_conv [simp]:
  "add_roots_rule r fs = roots_rule_list r @ fs"
  by (simp add: add_roots_rule_def roots_rule_list_def)

lemma add_funas_args_rule_funas_args_rule_list_conv [simp]:
  "add_funas_args_rule r fs = funas_args_rule_list r @ fs"
  by (simp add: add_funas_args_rule_def funas_args_rule_list_def)

definition insert_vars_rule :: "('f, 'v) rule ⇒ 'v list ⇒ 'v list"
where
  "insert_vars_rule r xs = insert_vars_term (fst r) (insert_vars_term (snd r) xs)"

definition insert_funs_rule :: "('f, 'v) rule ⇒ 'f list ⇒ 'f list"
where
  "insert_funs_rule r fs = insert_funs_term (fst r) (insert_funs_term (snd r) fs)"

definition insert_funas_rule :: "('f, 'v) rule ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
  "insert_funas_rule r fs = insert_funas_term (fst r) (insert_funas_term (snd r) fs)"

definition insert_roots_rule :: "('f, 'v) rule ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
  "insert_roots_rule r fs =
    foldr List.insert (option_to_list (root (fst r)) @ option_to_list (root (snd r))) fs"

definition insert_funas_args_rule :: "('f, 'v) rule ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
  "insert_funas_args_rule r fs = insert_funas_args_term (fst r) (insert_funas_args_term (snd r) fs)"

lemma set_insert_vars_rule [simp]:
  "set (insert_vars_rule r xs) = vars_term (fst r) ∪ vars_term (snd r) ∪ set xs"
  by (simp add: insert_vars_rule_def ac_simps)

lemma set_insert_funs_rule [simp]:
  "set (insert_funs_rule r xs) = funs_term (fst r) ∪ funs_term (snd r) ∪ set xs"
  by (simp add: insert_funs_rule_def ac_simps)

lemma set_insert_funas_rule [simp]:
  "set (insert_funas_rule r xs) = funas_term (fst r) ∪ funas_term (snd r) ∪ set xs"
  by (simp add: insert_funas_rule_def ac_simps)

lemma set_insert_roots_rule [simp]:
  "set (insert_roots_rule r xs) = root_set (fst r) ∪ root_set (snd r) ∪ set xs"
  by (cases "fst r" "snd r" rule: term.exhaust [case_product term.exhaust])
     (auto simp: insert_roots_rule_def ac_simps)

lemma set_insert_funas_args_rule [simp]:
  "set (insert_funas_args_rule r xs) = funas_args_term (fst r) ∪ funas_args_term (snd r) ∪ set xs"
  by (simp add: insert_funas_args_rule_def ac_simps funas_args_term_def)

abbreviation "vars_rule_impl r ≡ insert_vars_rule r []"
abbreviation "funs_rule_impl r ≡ insert_funs_rule r []"
abbreviation "funas_rule_impl r ≡ insert_funas_rule r []"
abbreviation "roots_rule_impl r ≡ insert_roots_rule r []"
abbreviation "funas_args_rule_impl r ≡ insert_funas_args_rule r []"

lemma set_vars_rule_impl:
  "set (vars_rule_impl r) = vars_rule r"
  by (simp add: vars_rule_def)

lemma [code]:
  "vars_rule_list r = add_vars_rule r []"
  "funs_rule_list r = add_funs_rule r []"
  "funas_rule_list r = add_funas_rule r []"
  "roots_rule_list r = add_roots_rule r []"
  "funas_args_rule_list r = add_funas_args_rule r []"
  by (simp_all add: vars_rule_list_def funs_rule_list_def funas_rule_list_def
                    roots_rule_list_def funas_args_rule_list_def)

lemma [code]:
  "vars_trs_list trs = foldr add_vars_rule trs []"
  "funs_trs_list trs = foldr add_funs_rule trs []"
  "funas_trs_list trs = foldr add_funas_rule trs []"
  "funas_args_trs_list trs = foldr add_funas_args_rule trs []"
  by (induct_tac [!] trs)
     (simp_all add: vars_trs_list_def funs_trs_list_def funas_trs_list_def
                    roots_trs_list_def funas_args_trs_list_def)

definition insert_vars_trs :: "('f, 'v) rule list ⇒ 'v list ⇒ 'v list"
where
  "insert_vars_trs trs = foldr insert_vars_rule trs"

definition insert_funs_trs :: "('f, 'v) rule list ⇒ 'f list ⇒ 'f list"
where
  "insert_funs_trs trs = foldr insert_funs_rule trs"

definition insert_funas_trs :: "('f, 'v) rule list ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
  "insert_funas_trs trs = foldr insert_funas_rule trs"

definition insert_roots_trs :: "('f, 'v) rule list ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
  "insert_roots_trs trs = foldr insert_roots_rule trs"

definition insert_funas_args_trs :: "('f, 'v) rule list ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
  "insert_funas_args_trs trs = foldr insert_funas_args_rule trs"

lemma set_insert_vars_trs [simp]:
  "set (insert_vars_trs trs xs) = (⋃r ∈ set trs. vars_rule r) ∪ set xs"
  by (induct trs arbitrary: xs) (simp_all add: insert_vars_trs_def ac_simps vars_rule_def)

lemma set_insert_funs_trs [simp]:
  "set (insert_funs_trs trs fs) = (⋃r ∈ set trs. funs_rule r) ∪ set fs"
  by (induct trs arbitrary: fs) (simp_all add: insert_funs_trs_def ac_simps funs_rule_def)

lemma set_insert_funas_trs [simp]:
  "set (insert_funas_trs trs fs) = (⋃r ∈ set trs. funas_rule r) ∪ set fs"
  by (induct trs arbitrary: fs) (simp_all add: insert_funas_trs_def ac_simps funas_rule_def)

lemma set_insert_roots_trs [simp]:
  "set (insert_roots_trs trs fs) = (⋃r ∈ set trs. roots_rule r) ∪ set fs"
  by (induct trs arbitrary: fs) (simp_all add: insert_roots_trs_def ac_simps roots_rule_def)

lemma set_insert_funas_args_trs [simp]:
  "set (insert_funas_args_trs trs fs) = (⋃r ∈ set trs. funas_args_rule r) ∪ set fs"
  by (induct trs arbitrary: fs)
     (simp_all add: insert_funas_args_trs_def ac_simps funas_args_rule_def)

abbreviation "vars_trs_impl trs ≡ insert_vars_trs trs []"
abbreviation "funs_trs_impl trs ≡ insert_funs_trs trs []"
abbreviation "funas_trs_impl trs ≡ insert_funas_trs trs []"
abbreviation "roots_trs_impl trs ≡ insert_roots_trs trs []"
abbreviation "funas_args_trs_impl trs ≡ insert_funas_args_trs trs []"

definition defined_list :: "('f, 'v) rule list ⇒ ('f × nat) list"
where
  "defined_list R = [the (root l). (l, r) ← R, is_Fun l]"

lemma set_defined_list [simp]:
  "set (defined_list R) = {fn. defined (set R) fn}"
by (force simp: defined_list_def defined_def elim!: root_Some)

definition check_left_linear_trs :: "('f :: showl, 'v :: showl) rules ⇒ showsl check"
where
  "check_left_linear_trs trs =
     check_all (λr. linear_term (fst r)) trs
       <+? (λ _. showsl_trs trs ∘ showsl (STR ''⏎is not left-linear⏎''))"

lemma check_left_linear_trs [simp]:
  "isOK (check_left_linear_trs R) = left_linear_trs (set R)"
  unfolding check_left_linear_trs_def left_linear_trs_def
  by auto

definition check_varcond_subset :: "(_,_) rules ⇒ showsl check"
where
  "check_varcond_subset R =
    check_allm (λrule. 
      check_subseteq (vars_term_impl (snd rule)) (vars_term_impl (fst rule))
      <+? (λx. showsl (STR ''free variable '') ∘ showsl x
        ∘ showsl (STR '' in right-hand side of rule '') ∘ showsl_rule rule ∘ showsl_nl)
    ) R"

lemma check_varcond_subset [simp]:
  "isOK (check_varcond_subset R) = (∀ (l, r) ∈ set R. vars_term r ⊆ vars_term l)"
  unfolding check_varcond_subset_def by force+

definition "check_varcond_no_Var_lhs =
  check_allm (λrule.
    check (is_Fun (fst rule))
      (showsl (STR ''variable left-hand side in rule '') ∘ showsl_rule rule ∘ showsl_nl))"

lemma check_varcond_no_Var_lhs [simp]:
  "isOK (check_varcond_no_Var_lhs R) ⟷ (∀(l, r) ∈ set R. is_Fun l)"
by (auto simp: check_varcond_no_Var_lhs_def)

definition check_wf_trs :: "(_,_) rules ⇒ showsl check"
where
  "check_wf_trs R = do {
    check_varcond_no_Var_lhs R;
    check_varcond_subset R
  } <+? (λe. showsl (STR ''the TRS is not well-formed⏎'') ∘ e)"

lemma check_wf_trs_conf [simp]:
  "isOK (check_wf_trs R) = wf_trs (set R)"
by (force simp: check_wf_trs_def wf_trs_def)

definition check_not_wf_trs :: "(_,_) rules ⇒ showsl check" where
  "check_not_wf_trs R = check (¬ isOK (check_wf_trs R)) (showsl (STR ''The TRS is well formed⏎''))"

lemma check_not_wf_trs:
  assumes "isOK(check_not_wf_trs R)"
  shows "¬ SN (rstep (set R))"
proof -
  from assms have "¬ wf_trs (set R)" unfolding check_not_wf_trs_def by auto
  with SN_rstep_imp_wf_trs show ?thesis by auto
qed

lemma [code]:
  "instance_rule lr st ⟷ match_list (λ _. fst lr) [(fst st, fst lr), (snd st, snd lr)] ≠ None"
  (is "?l = (match_list ?d ?list ≠ None)")
proof
  assume ?l
  then obtain σ where "fst lr = fst st ⋅ σ"
    and "snd lr = snd st ⋅ σ" by (auto simp: instance_rule_def)
  then have "⋀l t. (l, t) ∈ set ?list ⟹ l ⋅ σ = t" by (auto)
  then have "matchers (set ?list) ≠ {}" by (auto simp: matchers_def)
  with match_list_complete
    show "match_list ?d ?list ≠ None" by blast
next
  assume "match_list ?d ?list ≠ None"
  then obtain τ where "match_list ?d ?list = Some τ" by auto
  from match_list_sound [OF this]
    have "fst lr = fst st ⋅ τ" and "snd lr = snd st ⋅ τ" by auto
  then show ?l by (auto simp: instance_rule_def)
qed

definition
  check_CS_subseteq :: "('f, 'v) rules ⇒ ('f, 'v) rules ⇒ ('f, 'v) rule check"
where
  "check_CS_subseteq R S ≡ check_allm (λ (l,r). check (Bex (set S) (instance_rule (l,r))) (l,r)) R"

lemma check_CS_subseteq [simp]:
  "isOK (check_CS_subseteq R S) ⟷ subst.closure (set R) ⊆ subst.closure (set S)" (is "?l = ?r")
proof
  assume ?l
  show ?r
  proof
    fix x y
    assume "(x,y) ∈ subst.closure (set R)"    
    then show "(x,y) ∈ subst.closure (set S)"
    proof (induct)
      case (subst s t σ)
      with ‹?l›[unfolded check_CS_subseteq_def]
      obtain l r δ where lr: "(l,r) ∈ set S" and s: "s = l ⋅ δ" and t: "t = r ⋅ δ"
        by (auto simp add: instance_rule_def)
      show ?case unfolding s t
        using subst.closure.intros[OF lr, of "δ ∘s σ"]
        by auto
    qed
  qed
next
  assume ?r
  show ?l
    unfolding check_CS_subseteq_def
  proof (simp, intro ballI)
    fix lr
    assume mem: "lr ∈ set R"
    obtain l r where lr: "lr = (l,r)" by (cases lr, auto)
    with mem have "(l,r) ∈ subst.closure (set R)" using subst.subset_closure by auto
    with ‹?r› have "(l,r) ∈ subst.closure (set S)" by auto
    then show "Bex (set S) (instance_rule lr)" unfolding lr
    proof (induct)
      case (subst s t σ)
      then show ?case unfolding instance_rule_def by force
    qed
  qed
qed


type_synonym ('f,'v)rule_map = "(('f × nat) ⇒ ('f,'v)rules)option"


fun computeRuleMapH :: "('f,'v)rules ⇒ (('f × nat) × ('f,'v)rules)list option"
where "computeRuleMapH [] = Some []"
    | "computeRuleMapH ((Fun f ts,r) # rules) = (let n = length ts in case computeRuleMapH rules of None ⇒ None | Some rm ⇒ 
            (case List.extract (λ (fa,rls). fa = (f,n)) rm of 
                None ⇒ Some (((f,n), [(Fun f ts,r)]) # rm)
              | Some (bef,(fa,rls),aft) ⇒  Some  ((fa,(Fun f ts,r) # rls) # bef @ aft)))"
    | "computeRuleMapH ((Var _, _) # rules) = None"

definition computeRuleMap :: "('f, 'v) rules ⇒ ('f, 'v) rule_map" where
  "computeRuleMap rls ≡
    (case computeRuleMapH rls of
      None ⇒ None
    | Some rm ⇒ Some (λf.
      (case map_of rm f of
        None ⇒ []
      | Some rls ⇒ rls)))"

lemma computeRuleMapHSound2: "(computeRuleMapH R = None) = (∃ (l, r) ∈ set R. root l = None)"
proof (induct R, simp)
  case (Cons rule rules)
  show ?case 
  proof (cases rule)
    case (Pair l r)
    show ?thesis 
    proof (cases l, simp add: Pair Cons)
      case (Fun f ts)
      show ?thesis
        using Pair Cons
      proof (cases "computeRuleMapH rules", simp add: Pair Fun Let_def)
        case (Some rm) note oSome = this
        let ?e = "List.extract (λ (fa,rls). fa = (f,length ts)) rm"
        from Some Fun Pair Cons show ?thesis 
        proof (cases ?e, simp)
          case (Some res)
          then obtain bef aft g rls where "?e = Some (bef, (g,rls), aft)" by (cases res, force) 
          with extract_SomeE[OF this] have rm: "rm = bef @ ((f, length ts),rls) # aft" and e: "?e = Some (bef, ((f,length ts),rls), aft)"
            by auto
          show ?thesis using Cons
            by (simp add: Pair Fun Let_def oSome e)
        qed
      qed
    qed
  qed
qed

lemma computeRuleMapSound2: "(computeRuleMap R = None) = (∃ (l, r) ∈ set R. root l = None)"
unfolding computeRuleMap_def
by (simp only: computeRuleMapHSound2[symmetric], cases "computeRuleMapH R", auto)


lemma computeRuleMapHSound: assumes "computeRuleMapH R = Some rm"
  shows "(λ (f,rls). (f,set rls)) ` set rm = {((f,n),{(l,r) | l r. (l,r) ∈ set R ∧ root l = Some (f, n)}) | f n. {(l,r) | l r. (l,r) ∈ set R ∧ root l = Some (f, n)} ≠ {}} ∧ distinct_eq (λ (f,rls) (g,rls'). f = g) rm"
using assms
proof (induct R arbitrary: rm, force)
  case (Cons rule rules)
  let ?setl = "λ rm. (λ (f,rls). (f,set rls)) ` set rm"
  let ?setr = "λ R. {((f,n),{(l,r) | l r. (l,r) ∈ set R ∧ root l = Some (f, n)}) | f n. {(l,r) | l r. (l,r) ∈ set R ∧ root l = Some (f, n)} ≠ {}}"
  show ?case
  proof (cases rule)
    case (Pair l r)
    show ?thesis
    proof (cases l)
      case (Var v)
      with Cons Pair show ?thesis by simp
    next
      case (Fun f ts)
      with Cons Pair show ?thesis 
      proof (cases "computeRuleMapH rules", simp)
        case (Some rrm) note oSome = this
        let ?dis = "distinct_eq (λ (f,rls) (g,rls'). f = g)"
        from Cons(1)[OF Some] have drrm: "?dis rrm" and srrm: "?setl rrm = ?setr rules" by auto
        show ?thesis
        proof (cases "List.extract (λ (fa,rls). fa = (f,length ts)) rrm")
          case None
          let ?e = "((f,length ts), [(Fun f ts,r)])"
          let ?e' = "((f,length ts), {(Fun f ts,r)})"
          from None Cons(2) have rm: "rm = ?e # rrm" by (simp add: Fun Pair Some None)
          from None[unfolded extract_None_iff] have rrm: "⋀ g n rl. ((g,n),rl) ∈ set rrm ⟹ (f,length ts) ≠ (g,n)" by auto
          then have rrm': "⋀ g n rl. ((g,n),rl) ∈ ?setr rules ⟹ (f,length ts) ≠ (g,n)" by (simp only: srrm[symmetric], auto)
          then have  id: " {(Fun f ts, r)} = {(l, ra). (l = Fun f ts ∧ ra = r ∨ (l, ra) ∈ set rules) ∧ root l = Some (f, length ts)}"  by force
          from rrm have dis: "?dis rm" 
            by (simp add: rm drrm, auto)
          have "?setl rm = insert ?e' (?setl rrm)" by (simp add: rm)
          also have "… = insert ?e' (?setr rules)" by (simp add: srrm)
          also have "… = ?setr ( (Fun f ts,r) # rules)" 
          proof (rule set_eqI, clarify)
            fix g n rls
            show "(((g,n),rls) ∈ insert ?e' (?setr rules)) = (((g,n),rls) ∈ ?setr ((Fun f ts,r) # rules))"
            proof (cases "(g,n) = (f,length ts)")
              case False
              then have "(((g,n),rls) ∈ insert ?e' (?setr rules)) = (((g,n),rls) ∈ ?setr rules)" by auto
              also have "… = (((g,n),rls) ∈ ?setr ((Fun f ts,r) # rules))" using False by auto
              finally show ?thesis .
            next
              case True note oTrue = this
              show ?thesis 
              proof (cases "rls = {(Fun f ts, r)}")
                case True
                with oTrue show ?thesis by (simp add: id, force)
              next
                case False
                show ?thesis using rrm'[of g n rls] True False by (simp add: False True id, auto)
              qed
            qed
          qed
          finally show ?thesis
            by (simp only: dis drrm, simp add: Pair Fun)
        next
          case (Some res)
          obtain bef fg rls aft where "res = (bef,(fg,rls),aft)" by (cases res, force)
          from extract_SomeE[OF Some[simplified this]] Some[simplified this] have rrm: "rrm = bef @ ((f,length ts), rls) # aft" 
            and e: "List.extract (λ (fa, rls). fa = (f,length ts)) rrm = Some (bef, ((f,length ts),rls),aft)" by auto
          let ?e = "((f,length ts), (Fun f ts,r) # rls)"
          let ?e' = "((f,length ts), insert (Fun f ts,r) (set rls))"
          have "((f,length ts),set rls) ∈ ?setl rrm" unfolding rrm by auto
          then have rls: "set rls = {(l, r) |l r. (l, r) ∈ set rules ∧ root l = Some (f, length ts)}" using Cons(1)[OF oSome] by auto
          obtain ba where ba: "ba = bef @ aft" by auto
          from Cons(2) e ba have rm: "rm = ?e # ba" by (simp add: Fun Pair oSome e)
          from drrm[simplified rrm] have dis: "?dis ba"  unfolding distinct_eq_append ba by auto
          from drrm[simplified rrm] have dis: "?dis rm" unfolding rm distinct_eq_append ba by (auto simp: dis[simplified ba])
          from drrm[simplified rrm distinct_eq_append] 
          have diff: "(∀x∈set ba. ¬ (λ(g, rls). (f,length ts) = g) x)" by (auto simp: ba)
          have "?setl [((f, length ts),rls)] ∪ ?setl ba = ?setl rrm" using rrm ba by auto
          also have "… = ?setr rules" by (rule srrm)
          finally have id: "?setl [((f, length ts),rls)] ∪ ?setl ba = ?setr rules" .          
          have "?setl rm = insert ?e' (?setl ba)" by (simp add: rm)
          also have "… = ?setr ((Fun f ts,r) # rules)" 
          proof (rule set_eqI, clarify)
            fix g n rl 
            show "(((g,n),rl) ∈ insert ?e' (?setl ba)) = (((g,n),rl) ∈ ?setr ((Fun f ts,r) # rules))"
            proof (cases "(g,n) = (f,length ts)")
              case False 
              then have "(((g,n),rl) ∈ insert ?e' (?setl ba)) = (((g,n),rl) ∈ ?setl ba)" by auto
              also have "… = (((g,n),rl) ∈ ?setr rules)" using False by (simp only: id[symmetric], auto)
              also have "… = (((g,n),rl) ∈ ?setr ((Fun f ts,r) # rules))" using False by auto
              finally show ?thesis .
            next
              case True note oTrue = this
              show ?thesis 
              proof (cases "rl = insert (Fun f ts, r) (set rls)")
                case True
                then have "(((g,n),rl) ∈ insert ?e' (?setl ba)) = True" using oTrue by auto
                also have "… = (((g,n),rl) ∈ ?setr ((Fun f ts,r) # rules))" unfolding True rls using oTrue by force
                finally show ?thesis .
              next
                case False
                then have "(((g,n),rl) ∈ insert ?e' (?setl ba)) = False" using diff by (simp add: True, auto)
                also have "… = (((g,n),rl) ∈ ?setr ((Fun f ts,r) # rules))" 
                proof (rule ccontr)
                  assume "¬ ?thesis"
                  with True have "((f,length ts),rl) ∈ ?setr ((Fun f ts,r) # rules)" by simp
                  then have "rl = {(l, ra) |l ra. (l, ra) ∈ set ((Fun f ts, r) # rules) ∧ root l = Some (f, length ts)}" by simp
                  with False rls show False by auto
                qed                              
                finally show ?thesis .
              qed
            qed
          qed
          also have "… = ?setr (rule # rules)" by (simp add: Pair Fun)
          finally show ?thesis by (simp add: dis)
        qed
      qed
    qed
  qed
qed

lemma computeRuleMapSound:
  assumes "computeRuleMap R = Some rm" 
  shows "(set (rm (f,n))) = {(l,r) | l r. (l,r) ∈ set R ∧ root l = Some (f, n)}"
proof (cases "computeRuleMapH R")
  case None
  then show ?thesis using assms unfolding computeRuleMap_def by auto
next
  case (Some rrm)
  note rrm = computeRuleMapHSound[OF this] 
  note rm = assms[unfolded computeRuleMap_def, simplified Some, simplified, symmetric]
  show ?thesis
  proof (cases "map_of rrm (f, n)")
    case (Some rls)
    from map_of_SomeD[OF this] have "((f,n),set rls) ∈ (λ (f,rls). (f, set rls)) ` set rrm"
      by auto
    then have "set rls = {(l,r) | l r. (l,r) ∈ set R ∧ root l = Some (f, n)}"
      by (simp only: rrm, simp) 
    then show ?thesis by (simp add: rm Some)
  next
    case None
    have id: "{(l, r) |l r. (l, r) ∈ set R ∧ root l = Some (f, n)} = {}" (is "?set = {}")
    proof (rule ccontr)
      assume "¬ ?thesis"
      then obtain l r where "(l, r) ∈ set R ∧ root l = Some (f, n)" by auto
      with rrm have "(((f,n), ?set)) ∈ (λ (f,rls). (f, set rls)) ` set rrm" by auto
      with None[unfolded map_of_eq_None_iff] show False by force
    qed
    then show ?thesis by (simp only: rm None id, auto)
  qed
qed
    
    
  
lemma computeRuleMap_left_vars:
  shows "(computeRuleMap R ≠ None) = (∀ lr ∈ set R. ∀ x. fst lr ≠ Var x)"
proof (cases "computeRuleMap R")
  case None
  from None computeRuleMapSound2 have "∃ (l,r) ∈ set R. root l = None" by auto
  from this obtain l r where "(l,r) ∈ set R ∧ root l = None" by auto
  from this have "(l,r) ∈ set R ∧ ¬ (∀ x. fst (l,r) ≠ Var x)" by (cases l, auto)
  with None show ?thesis by blast
next
  case (Some rm)
  then have left: "computeRuleMap R ≠ None" by auto
  from Some computeRuleMapSound2 have "∀ (l,r) ∈ set R. root l ≠ None" by force
  then have "∀ lr ∈ set R. ∀ x. fst lr ≠ Var x" by auto
  with left show ?thesis by blast
qed

lemma computeRuleMap_defined: fixes R :: "('f,'v)rules"
  assumes "computeRuleMap R = Some rm"
  shows "(rm (f,n) = []) = (¬ defined (set R) (f,n))"
proof -
  from assms computeRuleMapSound have rm: "⋀(f::'f) n. set (rm (f,n)) = {(l,r) | l r. (l, r) ∈ set R ∧ root l = Some (f, n)}" by force
  show ?thesis
  proof (cases "rm (f,n)")
    case Nil
    with rm have "¬ defined (set R) (f,n)" unfolding defined_def by force
    with Nil show ?thesis by blast
  next
    case (Cons lr RR)
    then have left: "rm (f,n) ≠ []" by auto
    from Cons rm[where f = f and n = n] have "defined (set R) (f,n)" unfolding defined_def by (cases lr, force)
    with left show ?thesis by blast
  qed
qed



lemma computeRuleMap_None_not_SN:
  assumes "computeRuleMap R = None"
  shows "¬ SN_on (rstep (set R)) {t}"
proof -
  from assms computeRuleMap_left_vars[of R] obtain x r where "(Var x,r) ∈ set R" by auto
  from left_var_imp_not_SN[OF this] show ?thesis .
qed


definition reverse_rules :: "('f, 'v) rules ⇒ ('f, 'v) rules" where
  "reverse_rules rs ≡ map prod.swap rs"

lemma reverse_rules[simp]: "set (reverse_rules R) = (set R)^-1" unfolding reverse_rules_def by force

definition
  map_funs_rules_wa :: "('f × nat ⇒ 'g) ⇒ ('f, 'v) rules ⇒ ('g, 'v) rules"
where
  "map_funs_rules_wa fg R = map (λ(l, r). (map_funs_term_wa fg l, map_funs_term_wa fg r)) R"

lemma map_funs_rules_wa: "set (map_funs_rules_wa fg R) = map_funs_trs_wa fg (set R)"
  unfolding map_funs_rules_wa_def map_funs_trs_wa_def by auto

lemma wf_rule [code]:
  "wf_rule r ⟷
    is_Fun (fst r) ∧ (∀ x ∈ set (vars_term_impl (snd r)). x ∈ set (vars_term_impl (fst r)))"
  unfolding wf_rule_def by auto

definition wf_rules_impl :: "('f, 'v) rules ⇒ ('f, 'v) rules"
where
  "wf_rules_impl R = filter wf_rule R"

lemma wf_rules_impl [simp]:
  "set (wf_rules_impl R) = wf_rules (set R)"
  unfolding wf_rules_impl_def wf_rules_def by auto

fun check_wf_reltrs :: "(_,_) rules × (_,_) rules ⇒ showsl check" where
  "check_wf_reltrs (R, S) = (do {
     check_wf_trs R;
     if R = [] then succeed
     else check_varcond_subset S
   })"

lemma check_wf_reltrs[simp]:
  "isOK (check_wf_reltrs (R, S)) = wf_reltrs (set R) (set S)"
  by (cases R) auto

declare check_wf_reltrs.simps[simp del]

definition check_linear_trs :: "(_,_) rules ⇒ showsl check" where
  "check_linear_trs R ≡
     check_all (λ (l,r). (linear_term l) ∧ (linear_term r)) R
       <+? (λ _. showsl_trs R ∘ showsl (STR ''⏎is not linear⏎''))"

lemma check_linear_trs [simp]:
  "isOK (check_linear_trs R) ⟷ linear_trs (set R)"
  unfolding check_linear_trs_def linear_trs_def by auto

definition "non_collapsing_impl R = list_all (is_Fun o snd) R"

lemma [simp]: "non_collapsing_impl R = non_collapsing (set R)"
  unfolding non_collapsing_impl_def non_collapsing_def list_all_iff by auto


type_synonym ('f, 'v) term_map = "'f × nat ⇒ ('f, 'v) term list"

definition term_map :: "('f::compare_order, 'v) term list ⇒ ('f, 'v) term_map" where
  "term_map ts = fun_of_map (rm.α (elem_list_to_rm (the ∘ root) ts)) []"

definition
  is_NF_main :: "bool ⇒ bool ⇒ ('f::compare_order, 'v) term_map ⇒ ('f, 'v) term ⇒ bool"
where
  "is_NF_main var_cond R_empty m = (if var_cond then (λ_. False) 
     else if R_empty then (λ_. True)
     else (λt. ∀u∈set (supteq_list t).
       if is_Fun u then
         ∀l∈set (m (the (root u))). ¬ matches u l
       else True))"

lemma neq_root_no_match:
  assumes "is_Fun l" and "the (root l) ≠ the (root t)"
  shows "¬ matches t l"
  using assms by (cases t) (force iff: matches_iff)+

lemma all_not_conv: "(∀x ∈ A. ¬ P x) = (¬ (∃x ∈ A. P x))" by auto

lemma efficient_supteq_list_do_not_match:
  assumes "∀l∈set ls. ∀u∈set (supteq_list t). the (root l) ≠ the (root u) ⟶ ¬ matches u l"
  shows
    "(∀l∈set ls. ∀u∈set (supteq_list t). ¬ matches u l) ⟷
     (∀u∈set (supteq_list t). ∀l∈set (term_map ls (the (root u))).
       ¬ matches u l)"
    (is "?lhs ⟷ ?rhs" is "_ ⟷ (∀u∈set ?subs. ∀l∈set (?ls u). ¬ matches u l)")
proof (intro iffI ballI)
  fix u l assume "∀l∈set ls. ∀u∈set ?subs. ¬ matches u l" and "u ∈ set ?subs"
    and "l ∈ set (?ls u)"
  then show "¬ matches u l"
    using elem_list_to_rm.rm_set_lookup[of "the ∘ root" ls "the (root u)"]
    by (auto simp: o_def term_map_def rm_set_lookup_def)
next
  fix l u assume 1: "∀u∈set ?subs. ∀l∈set (?ls u). ¬ matches u l"
    and "l ∈ set ls" and "u ∈ set ?subs"
  with assms have "the (root l) ≠ the (root u) ⟶ ¬ matches u l"
    and "∀l∈set (?ls u). ¬ matches u l " by simp+
  with elem_list_to_rm.rm_set_lookup[of "the ∘ root" ls "the (root u)"]
    and ‹l ∈ set ls›
    show "¬ matches u l" by (auto simp: o_def term_map_def rm_set_lookup_def)
qed

lemma supteq_list_ex:
  "(∃u∈set (supteq_list l). ∃σ. t ⋅ σ = u) ⟷ (∃σ. l ⊵ t ⋅ σ)"
  unfolding supteq_list by auto

definition "is_NF_trs R = is_NF_main (∃r∈set R. is_Var (fst r)) (R = []) (term_map (map fst R))"
definition "is_NF_terms Q = is_NF_main (∃q∈set Q. is_Var q) (Q = []) (term_map Q)"

lemma is_NF_main_NF_trs_conv:
  "is_NF_main (∃r∈set R. is_Var (fst r)) (R = []) (term_map (map fst R)) t ⟷
    t ∈ NF_trs (set R)"
  (is "is_NF_main ?var ?R ?map t ⟷ _")
proof (intro iffI allI)
  assume is_NF_main: "is_NF_main ?var ?R ?map t"
  show "t ∈ NF_trs (set R)"
  proof (cases "∃r∈set R. is_Var (fst r)")
    case True with is_NF_main[unfolded is_NF_main_def] show ?thesis by simp
  next
    case False
    let ?ts = "map fst R"
    from False have allfun: "∀s∈set ?ts. is_Fun s" by simp
    with neq_root_no_match
    have no_match: "∀s∈set ?ts. ∀u∈set (supteq_list t). the (root s) ≠ the (root u)
        ⟶ ¬ matches u s" by blast
    note is_NF_main = is_NF_main[unfolded is_NF_main_def if_not_P[OF False]]
    show ?thesis
    proof (cases "R = []")
      case False
      then have False: "(R = []) = False" by simp
      have "∀u∈set (supteq_list t). ∀l∈set (term_map ?ts (the (root u))). ¬ matches u l"
      proof
        fix u
        assume mem: "u ∈ set (supteq_list t)"
        show "∀l∈set (term_map ?ts (the (root u))). ¬ matches u l"
        proof (cases u)
          case (Var x)
          show ?thesis
          proof
            fix l
            assume "l ∈ set (term_map ?ts (the (root u))) "
            with elem_list_to_rm.rm_set_lookup[of "the ∘ root" ?ts "the (root u)"]
            have "l ∈ set ?ts" by (auto simp: o_def term_map_def rm_set_lookup_def)
            then have "is_Fun l" using allfun by auto
            then have "(∀σ. l ⋅ σ ≠ u)" using Var by auto
            then show "¬ matches u l" using matches_iff by blast
          qed
        next
          case (Fun f us)
          with mem is_NF_main[unfolded False] show ?thesis by auto
        qed
      qed
      then show ?thesis
        unfolding efficient_supteq_list_do_not_match[OF no_match, symmetric]
        unfolding all_not_conv matches_iff
        unfolding supteq_list_ex by auto
    qed auto
  qed
next
  assume NF_trs: "t ∈ NF_trs (set R)"
  show "is_NF_main (∃r∈set R. is_Var (fst r)) (R = []) (term_map (map fst R)) t"
  proof (cases "∃r∈set R. is_Var (fst r)")
    case True
    then obtain l where "l ∈ lhss (set R)" and "is_Var l" by auto
    from lhs_var_not_NF[OF this] and NF_trs show ?thesis by simp
  next
    case False note oFalse = this
    let ?ts = "map fst R"
    from False have "∀s∈set ?ts. is_Fun s" by auto
    with neq_root_no_match
    have
      no_match: "∀s∈set ?ts. ∀u∈set (supteq_list t). the (root s) ≠ the (root u)
      ⟶ ¬ matches u s" by blast
    show ?thesis
    proof (cases "R = []")
      case True then show ?thesis unfolding is_NF_main_def by auto
    next
      case False
      then have False: "(R = []) = False" by simp
      from NF_trs
      show ?thesis
        unfolding is_NF_main_def False if_False if_not_P[OF oFalse]
        using efficient_supteq_list_do_not_match[OF no_match, symmetric]
        unfolding all_not_conv matches_iff
        unfolding supteq_list_ex set_map by fastforce
    qed
  qed
qed

lemma is_NF_trs [simp]:
  "is_NF_trs R = (λ t. t ∈ NF_trs (set R))"
  by (rule ext, unfold is_NF_trs_def is_NF_main_NF_trs_conv, simp)

lemma is_NF_terms [simp]:
  "is_NF_terms Q = (λ t. t ∈ NF_terms (set Q))"
proof (rule ext)
  fix t
  let ?Q = "map (λt. (t, t)) Q"
  have 1: "(∃t∈set Q. is_Var t) = (∃t∈set ?Q. is_Var (fst t))"
    by (induct Q) (auto simp: o_def)
  have 2: "map fst ?Q = Q" by (induct Q) simp_all
  have 3: "term_map Q = term_map (map fst ?Q)" unfolding 2 ..
  have 4: "set ?Q = Id_on (set Q)" by (induct Q) (auto simp: o_def)
  from is_NF_main_NF_trs_conv[of "?Q" t]
  show "is_NF_terms Q t = (t ∈ NF_terms (set Q))"
    unfolding is_NF_terms_def 1 3 4 unfolding 2 by auto
qed

abbreviation "terms_of_rules rs ≡ map fst rs @ map snd rs"
  
definition "match_rules rs1 rs2 = do {
  ts ← zip_option (terms_of_rules rs2) (terms_of_rules rs1);
  match_list Var ts
}"

abbreviation "term_of_rules rs ≡ Fun (SOME f. True) (terms_of_rules rs)"

lemma match_rules_alt_def:
  "match_rules rs1 rs2 = match (term_of_rules rs1) (term_of_rules rs2)"
  by (cases "zip_option (terms_of_rules rs1) (terms_of_rules rs2)")
    (auto simp: match_rules_def match_def match_list_def decompose_def
          split: option.splits Option.bind_splits)

lemma rules_enc_aux:
  fixes xs ys :: "('f, 'v :: infinite) rules"
  assumes "map ((∙) π ∘ fst) xs @ map ((∙) π ∘ snd) xs = map fst ys @ map snd ys"
  shows "map ((∙) π) xs = ys"
proof -
  have "length xs = length ys"
  proof (rule ccontr)
    assume "length xs ≠ length ys"
    moreover
    have "length (map ((∙) π ∘ fst) xs @ map ((∙) π ∘ snd) xs) = length (map fst ys @ map snd ys)"
      using assms by simp
    ultimately show False by simp
  qed
  then show ?thesis
    using assms by (induct xs ys rule: list_induct2; auto simp: eqvt)
qed

lemma perm_term_of_rules_eq_conv:
  "π ∙ term_of_rules rs1 = term_of_rules rs2 ⟷ π ∙ rs1 = rs2"
  by (auto simp: eqvt rules_enc_aux)

lemma match_rules_imp_variants:
  fixes rs1 rs2 :: "('f, 'v :: infinite) rules"
  assumes "match_rules rs2 rs1 = Some σ1" and "match_rules rs1 rs2 = Some σ2"
  shows "∃π::'v perm. π ∙ rs1 = rs2"
proof -
  have "term_of_rules rs2 ⋅ σ2 = term_of_rules rs1"
    and "term_of_rules rs1 ⋅ σ1 = term_of_rules rs2"
    using assms by (auto simp: match_rules_alt_def dest: match_sound)
  then obtain π :: "'v perm" where "π ∙ rs2 = rs1"
    using term_variants_iff [of "term_of_rules rs2" "term_of_rules rs1"]
    unfolding perm_term_of_rules_eq_conv by auto
  then have "-π ∙ rs1 = rs2" by (auto simp del: rules_pt.permute_list_def)
  then show ?thesis ..
qed

definition
  "check_variants_rule r r' = do {
    check (match_rules [r] [r'] ≠ None ∧ match_rules [r'] [r] ≠ None)
      (showsl_rule r ∘ showsl (STR '' and '') ∘ showsl_rule r' ∘ showsl (STR '' are not variants of each other⏎''))
  }"

lemma check_variants_rule [elim!]:
  assumes "isOK (check_variants_rule r r')"
  obtains p where "p ∙ r = r'"
  using assms
  by (cases r; cases r') (auto simp: check_variants_rule_def eqvt dest: match_rules_imp_variants)

definition
  "check_variant_in_trs R r =
    check_exm (check_variants_rule r) R (showsl_sep id id)
    <+? (λ_. showsl_rule r ∘ showsl (STR '' is not a variant of any rule in '') ∘ showsl_trs R)"

lemma check_variant_in_trs [elim!]:
  assumes "isOK (check_variant_in_trs R r)"
  obtains p where "p ∙ r ∈ set R"
  using assms by (cases r) (force simp: check_variant_in_trs_def eqvt)

definition "check_variants_trs R R' = check_allm (check_variant_in_trs R') R"

lemma check_variants_trs [dest!]:
  assumes "isOK (check_variants_trs R R')"
  shows "∀r ∈ set R. ∃p. p ∙ r ∈ set R'"
  using assms by (auto simp: check_variants_trs_def)

end