theory Monadic_Confluence
imports Ground_Confluence Ord.Signature_Extension LV_to_GTT LLRG_Confluence
begin
locale monadic_signature =
fixes ℱ :: "'f sig"
assumes monadic_sig: "snd ` ℱ ⊆ {0,1}"
and ex_constant:"∃c ∈ ℱ. snd c = 0"
begin
definition monadic :: "('f, 'v) term ⇒ bool" where
"monadic s ≡ (funas_term s ⊆ ℱ) "
lemma monadic_subterm:
assumes "monadic s" "t ⊴ s"
shows "monadic t" unfolding monadic_def
by (meson assms(1) assms(2) dual_order.trans monadic_def supteq_imp_funas_term_subset)
lemma monadic_vars:
assumes "monadic s"
shows "card (vars_term s) ≤ 1"
using assms
proof (induction s)
case (Fun f ss)
hence 1:"snd ` (funas_term (Fun f ss)) ⊆ {0,1}" unfolding monadic_def using monadic_sig
by (meson order.trans subset_image_iff)
hence 2:"length ss = 0 ∨ length ss = 1" by auto
then show ?case
proof (cases "length ss = 0")
case False
with 2 have "length ss = 1" by simp
then obtain s where s:"ss = [s]"
by (metis One_nat_def add.right_neutral add_Suc_right le_add_same_cancel2
le_imp_less_Suc length_0_conv less_not_refl list.size(4) remdups_adj.cases zero_le)
hence "vars_term (Fun f ss) = vars_term s" by simp
moreover have "monadic s" using monadic_subterm[of "Fun f ss" "s"]
using Fun.prems s by auto
ultimately show ?thesis using Fun(1)
by (simp add: ‹vars_term (Fun f ss) = vars_term s› s)
qed (auto)
qed (auto)
lemma grnd_ctxt_vars_ctxt:
"ground_ctxt C ⟷ vars_ctxt C = {}"
proof (rule iffI, goal_cases)
case 1 then show ?case
proof (induction C)
case (More f ss C ts)
have eq:"vars_ctxt (More f ss C ts) = ((⋃s∈set ss. vars_term s) ∪ vars_ctxt C ∪ (⋃t∈set ts. vars_term t))"
by auto
have "∀s ∈ set ss. vars_term s ={}" "∀t ∈ set ts. vars_term t ={}"
using More(2)
by (simp add: ground_vars_term_empty)+
then show ?case using More eq by force
qed (simp)
next
case 2 then show ?case
proof (induction C)
case (More f ss C ts)
hence "∀s ∈ set ss. vars_term s = {}" "∀t ∈ set ts. vars_term t = {}" by force+
hence "∀s ∈ set ss. ground s" "∀t ∈ set ts. ground t"
by (simp add: ground_vars_term_empty)+
then show ?case using More by auto
qed (auto)
qed
lemma ground_ctxt_monadic:
assumes "monadic C⟨s⟩" "monadic s"
shows "ground_ctxt C"
using assms
proof (induction C)
case (More f ss C ts)
hence 1:"snd ` (funas_term (Fun f (ss@C⟨s⟩#ts))) ⊆ {0,1}" unfolding monadic_def using monadic_sig
by (metis ctxt_apply_term.simps(2) doubleton_eq_iff order.trans subset_image_iff)
hence 2:"(length (ss@C⟨s⟩#ts) = 0) ∨ (length (ss@C⟨s⟩#ts) = 1)" by force
moreover have C:"ground_ctxt C" using More monadic_subterm by force
show ?case
proof (cases "(length (ss@C⟨s⟩#ts) = 0)")
case False
hence "(ss@C⟨s⟩#ts) = [C⟨s⟩]" using 2
by simp
hence "More f ss C ts = More f [] C []" using False
by (metis Cons_eq_append_conv Nil_is_append_conv list.discI list.inject)
with C show ?thesis by force
qed (fast)
qed (simp)
lemma ground_monadic_eq:
assumes "ground s" "funas_term s ⊆ ℱ"
shows "monadic s"
using assms unfolding monadic_def by simp
lemma ground_ctxt_apply:
assumes "ground_ctxt C" "ground s"
shows "ground C⟨s⟩" using assms
by (simp add: grnd_ctxt_vars_ctxt ground_vars_term_empty vars_term_ctxt_apply)
lemma monadic_subst:
fixes g :: "'f"
defines "σ ≡ λ t. Fun g []"
assumes "(g,0) ∈ ℱ" "monadic s"
shows "funas_term (s ⋅ σ) ⊆ ℱ"
using assms
proof (induction s)
case (Fun f ss)
have 1:"Fun f ss ⋅ σ = Fun f (map (λ t. (t ⋅ σ)) ss)" by auto
{fix i
assume i:"i < length ss"
hence "monadic (ss!i)" using Fun(4) monadic_subterm by fastforce
hence "funas_term ((ss!i)⋅ σ) ⊆ ℱ" using Fun(1,2,3) i
using monadic_def
by auto} note ind = this
hence int:"⋃(set (map funas_term (map (λ t. (t ⋅ σ)) ss))) ⊆ ℱ"
by (smt Union_least in_set_idx length_map map_nth_eq_conv)
have "(f, length ss) ∈ ℱ" using monadic_def Fun(4) by force
hence "(f, length (map (λ t. t ⋅ σ) ss)) ∈ ℱ" by auto
thus ?case using int 1 by simp
qed (simp)
lemma property_1:
fixes g :: 'f
defines "σ' ≡ λ_. Fun g []"
assumes "(s,t) ∈ sig_step ℱ (rstep R)" "monadic s" "monadic t" "llrg R" "(g,0) ∈ ℱ"
shows "(s ⋅ σ', t) ∈ sig_step ℱ (rstep R) ∧ (ground t)"
using assms
proof -
have asm1:"(s,t) ∈ rstep R" "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" using assms(2)
by blast+
thus ?thesis using assms(3-6,1)
proof (induction rule:rstepE)
case (rstep s t C σ l r)
hence "r ⋅ σ = r" unfolding llrg_def using ground_subst_apply[of r σ]
by (metis ground_subst_apply snd_conv)
hence t:"t = C⟨r⟩" using rstep(5) by argo
hence "monadic r" using rstep(2,9) monadic_subterm[of t r] by blast
with t have "ground_ctxt C" using rstep(2,9,10) ground_ctxt_monadic by blast
moreover have "ground r" using rstep(3,10) unfolding llrg_def by auto
ultimately have grnd:"ground t" using t ground_ctxt_apply by blast
hence "(s ⋅ σ', t ⋅ σ') ∈ (rstep R)" using rstep asm1 by blast
hence step:"(s ⋅ σ', t) ∈ (rstep R)" using ground_subst_apply[OF grnd] by metis
moreover have "funas_term (s ⋅ σ') ⊆ ℱ" using monadic_subst rstep by blast
hence "(s ⋅ σ', t) ∈ sig_step ℱ (rstep R)" using rstep(2,7) step by blast
then show ?case using grnd rstep(1,2) by fast
qed
qed
lemma property_1_trancl:
fixes g :: 'f
defines "σ' ≡ λ t. Fun g []"
assumes "(s,t) ∈ (sig_step ℱ (rstep R))^+" "monadic s" "monadic t" "llrg R" "(g,0) ∈ ℱ"
shows "(s ⋅ σ', t) ∈ (sig_step ℱ (rstep R))^+ ∧ ground t"
using assms(2,1,3-6)
proof (induction rule:trancl_induct)
case (base y)
then show ?case using property_1 by blast
next
case (step u v)
from step(2) have u:"monadic u" unfolding monadic_def by fast
with step(3,4,5,7,8) have "(s ⋅ σ', u) ∈ (sig_step ℱ (rstep R))⇧+" by blast
hence "(s ⋅ σ', v) ∈ (sig_step ℱ (rstep R))⇧+" using step(2) by simp
moreover have "ground v" using property_1[OF step(2) u step(6,7,8)] by force
ultimately show ?case by satx
qed
lemma CR_implies_GCR:
fixes R::"('f,'v) trs"
assumes
"CR (sig_step ℱ (rstep R))"
"llrg R" "funas_trs R ⊆ ℱ"
shows "CR_on (sig_step ℱ (rstep R)) {s. ground s}"
using assms
proof -
{fix s u v
assume "ground s"
"(s,u) ∈ (sig_step ℱ (rstep R))^*"
"(s,v) ∈ (sig_step ℱ (rstep R))^*"
hence "(u,v) ∈ join (sig_step ℱ (rstep R))"
using assms(1) by auto}
then show ?thesis by auto
qed
lemma GCR_implies_CR:
fixes R :: "('f,'v) trs"
assumes
"CR_on (sig_step ℱ (rstep R)) {s. ground s}"
"llrg R" "funas_trs R ⊆ ℱ"
shows "CR (sig_step ℱ (rstep R))"
proof -
obtain c where c:"(c,0) ∈ ℱ" using ex_constant by force
define σ where σ:"σ ≡ λ (t::'v). Fun c ([]::('f,'v) term list)"
{fix s u v
assume asm:"(s, u) ∈ (sig_step ℱ (rstep R))⇧*" "(s, v) ∈ (sig_step ℱ (rstep R))⇧*"
hence "(u,v) ∈ join (sig_step ℱ (rstep R))"
proof (cases "s = u ∨ s = v")
case True
then show ?thesis
using asm(1) asm(2) by blast
next
case False
hence tr:"(s, u) ∈ (sig_step ℱ (rstep R))⇧+" "(s, v) ∈ (sig_step ℱ (rstep R))⇧+"
by (meson asm rtranclD)+
hence mon:"monadic s" "monadic u" "monadic v" unfolding monadic_def
apply (meson sig_stepE tranclD)
apply (meson sig_stepE tr(1) tranclD2)
by (meson sig_stepE tr(2) tranclD2)
have grnd:"ground (s⋅ σ)" using σ by (induction s) (simp , force)
have r1:"((s ⋅ σ, u) ∈ (sig_step ℱ (rstep R))^+)" "(ground u)"
using property_1_trancl[OF tr(1) mon(1,2) assms(2) c] σ by blast+
have r2:"((s ⋅ σ, v) ∈ (sig_step ℱ (rstep R))^+)" "(ground v)"
using property_1_trancl[OF tr(2) mon(1,3) assms(2) c] σ by blast+
thus ?thesis using assms(1) r1 grnd unfolding CR_on_def
by (metis mem_Collect_eq trancl_into_rtrancl)
qed}
thus ?thesis by auto
qed
lemma CR_GCR_eq:
fixes R :: "('f,'v) trs"
assumes "llrg R" "funas_trs R ⊆ ℱ"
shows "CR (sig_step ℱ (rstep R)) = CR_on (sig_step ℱ (rstep R)) {s. ground s}"
using GCR_implies_CR CR_implies_GCR assms by metis
end
end