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 rs⇩1 rs⇩2 = do {
ts ← zip_option (terms_of_rules rs⇩2) (terms_of_rules rs⇩1);
match_list Var ts
}"
abbreviation "term_of_rules rs ≡ Fun (SOME f. True) (terms_of_rules rs)"
lemma match_rules_alt_def:
"match_rules rs⇩1 rs⇩2 = match (term_of_rules rs⇩1) (term_of_rules rs⇩2)"
by (cases "zip_option (terms_of_rules rs⇩1) (terms_of_rules rs⇩2)")
(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 rs⇩1 = term_of_rules rs⇩2 ⟷ π ∙ rs⇩1 = rs⇩2"
by (auto simp: eqvt rules_enc_aux)
lemma match_rules_imp_variants:
fixes rs⇩1 rs⇩2 :: "('f, 'v :: infinite) rules"
assumes "match_rules rs⇩2 rs⇩1 = Some σ⇩1" and "match_rules rs⇩1 rs⇩2 = Some σ⇩2"
shows "∃π::'v perm. π ∙ rs⇩1 = rs⇩2"
proof -
have "term_of_rules rs⇩2 ⋅ σ⇩2 = term_of_rules rs⇩1"
and "term_of_rules rs⇩1 ⋅ σ⇩1 = term_of_rules rs⇩2"
using assms by (auto simp: match_rules_alt_def dest: match_sound)
then obtain π :: "'v perm" where "π ∙ rs⇩2 = rs⇩1"
using term_variants_iff [of "term_of_rules rs⇩2" "term_of_rules rs⇩1"]
unfolding perm_term_of_rules_eq_conv by auto
then have "-π ∙ rs⇩1 = rs⇩2" 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