theory Usable_Rules_NJ_Unif
imports
"Check-NT.Tcap"
"Check-NT.Ground_Context_Impl"
begin
text ‹Def. 4.4, containment ordering›
definition contains :: "('f,'v)trs ⇒ ('f,'v)trs ⇒ bool" where
"contains U V ≡ V ⊆ rstep U"
lemma containsI[intro]: assumes "⋀ l r. (l,r) ∈ V ⟹ (l,r) ∈ rstep U"
shows "contains U V" unfolding contains_def using assms by force
lemma contains_rstep: assumes "(s,t) ∈ rstep V" and "contains U V"
shows "(s,t) ∈ rstep U"
using assms unfolding contains_def using rstep_rstep[of U] by force
context
fixes R U :: "('f,string)trs"
begin
inductive_set U0 :: "('f,string)term ⇒ ('f,string)trs" for s :: "('f,string)term" where
match_non_var: "(l,r) ∈ R ⟹ s ⊵ Fun f ts ⟹ gc_matcher (tcap_below U f ts) l = Some σ ⟹ (l ⋅ σ, r ⋅ σ) ∈ U0 s"
definition usable_instantiation :: "('f,string)term ⇒ bool" where
"usable_instantiation s ≡ contains U (U0 s)
∧ (∀ r ∈ rhss U. contains U (U0 r))"
definition "no_lhs_var ≡ ∀ l r. (l,r) ∈ R ⟶ is_Fun l"
lemma U0_contains: assumes ground: "ground s ∨ no_lhs_var"
shows "contains (U0 s) { (s,t) | t. (s,t) ∈ rstep R }" (is "contains ?L ?R")
proof
fix s' t
assume "(s',t) ∈ ?R" hence s': "s' = s" and st: "(s,t) ∈ rstep R" by auto
from st obtain Θ C l r where lr: "(l,r) ∈ R" and s: "s = C ⟨ l ⋅ Θ ⟩" and t: "t = C ⟨ r ⋅ Θ ⟩" by auto
from ground[unfolded s no_lhs_var_def] lr obtain f ls where lt: "l ⋅ Θ = Fun f ls" by (cases l, auto, cases "l ⋅ Θ", auto)
from s have "s ⊵ Fun f ls" unfolding lt by auto
note match = match_non_var[OF lr this]
have "l ⋅ Θ ∈ equiv_class (tcap_below U f ls)" unfolding lt by (auto simp: tcap_refl)
from gc_matcher_complete[OF this] obtain σ δ
where mgu: "gc_matcher (tcap_below U f ls) l = Some σ" and theta: "Θ = σ ∘⇩s δ" by auto
let ?lr = "(l ⋅ σ, r ⋅ σ)"
from match[OF mgu] have "?lr ∈ ?L" .
from rstepI[OF this, of s C δ t] theta s t
show "(s',t) ∈ rstep ?L" unfolding s' by auto
qed
context
assumes wfU: "⋀ l r. (l,r) ∈ U ⟹ vars_term r ⊆ vars_term l"
begin
lemma usable_instantiation_rstep: assumes step: "(s,t) ∈ rstep R"
and ground: "ground s ∨ no_lhs_var"
and U: "usable_instantiation s"
shows "usable_instantiation t"
proof -
note d = usable_instantiation_def
note U0 = match_non_var
from U have cs: "contains U (U0 s)"
and crec: "⋀ r. r ∈ rhss U ⟹ contains U (U0 r)"
unfolding d by auto
have "contains U (U0 t)"
proof
fix ls rs
assume "(ls,rs) ∈ U0 t"
thus "(ls,rs) ∈ rstep U"
proof (cases)
case (match_non_var l' r' f us σ)
note lr' = match_non_var(3)
note subt = match_non_var(4)
note mgu = match_non_var(5)
note ls_rs = match_non_var(1-2)
let ?u = "Fun f us"
from U0_contains[OF ground, unfolded contains_def] step have "(s,t) ∈ rstep (U0 s)" by auto
from contains_rstep[OF this cs] obtain C l r Θ where
lr: "(l,r) ∈ U" and s: "s = C ⟨ l ⋅ Θ ⟩" and t: "t = C ⟨ r ⋅ Θ ⟩" by auto
{
assume sub: "C ⟨ l ⋅ Θ ⟩ ⊵ ?u"
have "(ls,rs) ∈ U0 s" unfolding ls_rs
by (rule U0[OF lr' _ mgu], insert sub, auto simp: s)
with cs have ?thesis unfolding contains_def by auto
} note subt_goal = this
from lr have r: "r ∈ rhss U" by force
note trans = subterm.dual_order.trans
from subt[unfolded t]
show ?thesis
proof (cases rule: supteq_ctxt_cases)
case in_ctxt
show ?thesis by (rule subt_goal[OF supt_imp_supteq[OF suptc_imp_supt[OF in_ctxt]]])
next
case in_term
thus ?thesis
proof (cases rule: supteq_subst_cases)
case (in_subst x)
from wfU[OF lr] in_subst have "x ∈ vars_term l" by auto
hence "l ⊵ Var x" by auto
from trans[OF supteq_subst[OF this, of Θ], of ?u] in_subst have subt: "l ⋅ Θ ⊵ ?u" by simp
show ?thesis by (rule subt_goal[OF trans[OF _ subt]], auto)
next
case (in_term v)
from in_term obtain vs where v: "v = Fun f vs" by (cases v, auto)
let ?vs = "map (λ v. v ⋅ Θ) vs"
from in_term(3) have us: "us = ?vs" unfolding v by simp
note U0 = U0[OF lr' in_term(1)[unfolded v]]
from gc_matcher_sound[OF mgu[unfolded us]]
have mem: "⋀ σ'. l' ⋅ σ ⋅ σ' ∈ equiv_class (tcap_below U f ?vs)" .
have "equiv_class (tcap_below U f ?vs) ⊆ equiv_class (tcap_below U f vs)"
by (rule equiv_class_GCFun_subset, insert tcap_instance_subset, auto)
hence mem: "⋀ σ'. l' ⋅ σ ⋅ σ' ∈ equiv_class (tcap_below U f vs)" using mem by blast
from mem[of Var] have "l' ⋅ σ ∈ equiv_class (tcap_below U f vs)" by simp
from gc_matcher_complete[OF this] obtain μ δ where
match: "gc_matcher (tcap_below U f vs) l' = Some μ" and σ: "σ = μ ∘⇩s δ" by blast
from U0[OF match] have mem: "(l' ⋅ μ, r' ⋅ μ) ∈ U0 r" by auto
show ?thesis unfolding ls_rs σ
by (rule contains_rstep[OF _ crec[OF r]], insert mem, auto)
qed
next
case (sub_ctxt D C')
then obtain bef D' aft where C': "C' = More f bef D' aft" by (cases C', auto)
from sub_ctxt(2)[unfolded C'] have us: "us = bef @ D'⟨r ⋅ Θ⟩ # aft" by simp
from gc_matcher_sound[OF mgu[unfolded us]]
have mgu: "⋀ σ'. l' ⋅ σ ⋅ σ' ∈ equiv_class (tcap_below U f (bef @ D'⟨r ⋅ Θ⟩ # aft))" .
from tcap_rewrite[OF rstepI[OF lr]]
have "equiv_class (tcap U D'⟨r ⋅ Θ⟩) ⊆ equiv_class (tcap U D'⟨l ⋅ Θ⟩)" by auto
from mgu[of Var] equiv_class_mono[OF this, of f "map (tcap U) bef" "map (tcap U) aft"]
have "l' ⋅ σ ∈ equiv_class (tcap_below U f (bef @ D'⟨l ⋅ Θ⟩ # aft))" by auto
from gc_matcher_complete[OF this] obtain μ δ where
mgu: "gc_matcher (tcap_below U f (bef @ D'⟨l ⋅ Θ⟩ # aft)) l' = Some μ" and σ: "σ = μ ∘⇩s δ" by auto
have step: "(l' ⋅ μ, r' ⋅ μ) ∈ U0 s" unfolding s C' sub_ctxt
by (rule U0[OF lr' _ mgu], auto)
show ?thesis unfolding ls_rs σ
using contains_rstep[OF rstepI[OF step, of _ Hole] cs] by auto
qed
qed
qed
with crec show ?thesis unfolding d by auto
qed
text ‹lemma 4.9›
lemma usable_instantiation_rsteps_main: assumes sU: "usable_instantiation s"
and st: "(s,t) ∈ (rstep R)^*" and gs: "ground s ∨ no_lhs_var"
shows "(s,t) ∈ (rstep U)^* ∧ usable_instantiation t ∧ (ground t ∨ no_lhs_var)"
using st
proof (induct)
case (step t u)
hence gt: "ground t ∨ no_lhs_var" by simp
from usable_instantiation_rstep[OF step(2)] step(3) have
uu: "usable_instantiation u" and ut: "usable_instantiation t" by blast+
from ut[unfolded usable_instantiation_def] have "contains U (U0 t)" ..
from step(2) U0_contains[OF gt] contains_rstep[OF _ this, of t u] have tu: "(t,u) ∈ rstep U"
unfolding contains_def by auto
from tu gt wfU have "ground u ∨ no_lhs_var" by fastforce
with tu uu step(3) show ?case by auto
qed (insert sU gs, auto)
end
end
end