theory Usable_Rules_NJ
imports
"Check-NT.Tcap"
begin
text ‹Usable rules for reachability, formalization of Aoto's FroCoS'13 paper›
locale usable_rules_reachability =
fixes R :: "('f,'v)trs"
begin
inductive U0 :: "('f,'v)rule ⇒ ('f,'v)term ⇒ bool" where
lvar: "(l,r) ∈ R ⟹ is_Var l ⟹ U0 (l,r) t"
| rec: "U0 (l,r) t ⟹ U0 lr r ⟹ U0 lr t"
| match: "(l,r) ∈ R ⟹ match_tcap_below l R (Fun f ts) ⟹ s ⊵ Fun f ts ⟹ U0 (l,r) s"
lemma U0_R: "U0 lr t ⟹ lr ∈ R"
by (induct rule: U0.induct, auto)
definition "varcond ≡ λ (l,r). vars_term r ⊆ vars_term l"
definition "Ur t = (let U0t = {lr. U0 lr t} in if (∀ lr ∈ U0t. varcond lr) then U0t else R)"
lemma Ur_R: "Ur t ⊆ R" unfolding Ur_def Let_def using U0_R by auto
lemma Ur_1: assumes s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" and lr: "(l,r) ∈ R"
shows "U0 (l,r) s"
proof (cases l)
case (Var x)
hence "is_Var l" by auto
from lvar[OF lr this]
show ?thesis .
next
case (Fun f ls)
let ?ls = "Fun f (map (λ l. l ⋅ σ) ls)"
from Fun have "l ⋅ σ = ?ls" by simp
hence subt: "s ⊵ ?ls" unfolding s by auto
show ?thesis
by (rule match[OF lr _ subt], unfold match_tcap_below.simps Ground_Context.match_def, rule exI[of _ σ],
simp add: Fun tcap_refl)
qed
lemma Ur_2: assumes step: "(s,t) ∈ rstep R"
shows "Ur t ⊆ Ur s"
proof -
{
fix lr'
assume "U0 lr' t" and "⋀ lr. U0 lr s ⟹ varcond lr"
hence "U0 lr' s" using step
proof (induct arbitrary: s rule: U0.induct)
case lvar
from U0.lvar[OF this(1-2)] lvar show ?case by auto
next
case (rec l r t lr')
show ?case
by (rule U0.rec[OF rec(2)[OF rec(5) rec(6)] rec(3)])
next
case (match l' r' f ts t)
def u ≡ "Fun f ts"
note U = U0.match[OF match(1-2), folded u_def]
from rstepE[OF match(5)] obtain C σ l r where lr: "(l,r) ∈ R" and s: "s = C ⟨ l ⋅ σ⟩" and t: "t = C ⟨r ⋅ σ⟩" .
from match(3)[folded u_def] have subt: "t ⊵ u" .
note trans = subterm.dual_order.trans
{
assume u: "C⟨l ⋅ σ⟩ ⊵ u"
from U[OF this] have ?case unfolding s .
} note subt_goal = this
from subt[unfolded t]
show ?case
proof (cases rule: supteq_ctxt_cases)
case (sub_ctxt D C')
then obtain g bef D' aft where C': "C' = More g bef D' aft" by (cases C', auto)
from match(2)[folded u_def, unfolded sub_ctxt C']
have "match_tcap_below l' R (Fun g (bef @ D'⟨r ⋅ σ⟩ # aft))" by simp
hence "match_tcap_below l' R (Fun g (bef @ D'⟨l ⋅ σ⟩ # aft))" unfolding match_tcap_below.simps map_append list.map
by (rule match_below[OF _ tcap_rewrite[OF rstepI[OF lr]]], auto)
from U0.match[OF match(1) this, of s] show ?thesis
unfolding s sub_ctxt C' by auto
next
case in_ctxt
from subt_goal[OF supt_imp_supteq[OF suptc_imp_supt[OF this]]]
show ?thesis .
next
case in_term
thus ?thesis
proof (cases rule: supteq_subst_cases)
case (in_subst x)
from Ur_1[OF s t lr] have U0lr: "U0 (l,r) s" .
from match(4)[OF this, unfolded varcond_def] in_subst lr 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 u_def obtain vs where v: "v = Fun f vs" by auto
let ?vs = "map (λ v. v ⋅ σ) vs"
from match(2)[folded u_def, unfolded in_term v] have "match_tcap_below l' R (Fun f ?vs)" by simp
hence "match_tcap_below l' R (Fun f vs)" unfolding match_tcap_below.simps map_map o_def Ground_Context.match_def
using tcap_instance_subset[of R _ σ] by force
from U0.match[OF match(1) this in_term(1)[unfolded v]] have "U0 (l',r') r" .
from U0.rec[OF Ur_1(1)[OF s refl lr] this] show ?thesis .
qed
qed
qed
} note main = this
show ?thesis
by (cases "∀ lr ∈ {lr. U0 lr s}. varcond lr", insert main Ur_R,
auto simp: Ur_def Let_def)
qed
lemma Ur: "(s,t) ∈ (rstep R)^* ⟹ (s,t) ∈ (rstep (Ur s))^*"
proof (induct rule: converse_rtrancl_induct)
case (step s u)
from Ur_2[OF step(1)] have subset: "Ur u ⊆ Ur s" by auto
from rstepE[OF step(1)] obtain C σ l r where lr: "(l,r) ∈ R"
and s: "s = C ⟨ l ⋅ σ ⟩" and u: "u = C ⟨ r ⋅ σ ⟩" .
from Ur_1[OF s u lr] lr have "(l,r) ∈ Ur s" unfolding Ur_def by auto
from rstepI[OF this s u] rtrancl_mono[OF rstep_mono[OF subset]] step(3)
show ?case by auto
qed simp
end
abbreviation usable_rules_reach where "usable_rules_reach ≡ usable_rules_reachability.Ur"
lemmas usable_rules_reach = usable_rules_reachability.Ur
lemma usable_rules_reach_nj: "¬ (∃ u. (s,u) ∈ (rstep (usable_rules_reach Rs s))^* ∧ (t,u) ∈ (rstep (usable_rules_reach Rt t))^*) ⟹
¬ (∃ u. (s,u) ∈ (rstep Rs)^* ∧ (t,u) ∈ (rstep Rt)^*)"
using usable_rules_reach by auto
lemma subterm_tcap_nj: assumes p: "p ∈ pos_gctxt (tcap Rs s)" "p ∈ pos_gctxt (tcap Rt t)"
and nj: "¬ (∃ u. (s |_ p, u) ∈ (rstep Rs)^* ∧ (t |_ p, u) ∈ (rstep Rt)^*)"
shows "¬ (∃ u. (s, u) ∈ (rstep Rs)^* ∧ (t, u) ∈ (rstep Rt)^*)"
using tcap_subterm_rsteps[OF _ p(1)]
tcap_subterm_rsteps[OF _ p(2)] nj by blast
end