section ‹Nonreachability›
theory Nonreachability
imports
"Check-NT.Gtcap_Impl"
"../Framework/Rule_Map"
TA.Exact_Tree_Automata_Completion_Impl
begin
hide_const (open) Ground_Context_Impl.match_list
hide_fact (open) Ground_Context_Impl.match_list_sound Ground_Context_Impl.match_list_complete
lemma rsteps_imp_rev_rsteps:
assumes "(s, t) ∈ (rstep R)⇧*"
shows "(t, s) ∈ (rstep (R¯))⇧*"
using assms using rtrancl_converse by force
lemma rstep_subst_overapproximation:
assumes "∀(l, r) ∈ R. ∃(l', r') ∈ R'. ∃σ. l = l' ⋅ σ ∧ r = r' ⋅ σ"
shows "rstep R ⊆ rstep R'"
using assms by force
definition "is_instance_rule r r' ⟷
(case match_list Var [(fst r', fst r), (snd r', snd r)] of
Some σ ⇒ True
| None ⇒ False)"
lemma is_instance_rule [simp]:
"is_instance_rule r r' ⟷ (∃σ. fst r = fst r' ⋅ σ ∧ snd r = snd r' ⋅ σ)"
by (auto simp: is_instance_rule_def dest!: match_list_sound match_list_complete split: option.splits)
metis
definition "check_subst_overapproximation R R' =
check_allm (λr. check_exm (λr'.
check (is_instance_rule r r') id
) R' (λ_. shows ''growing rule for '' ∘ shows_rule r ∘ shows '' is missing'' ∘ shows_nl)) R
<+? (λe. shows R' ∘ shows_nl ∘
shows ''is not an overapproximation of'' ∘ shows_nl ∘ shows R ∘ shows_nl ∘ e)"
lemma check_subst_overapproximation [simp]:
"isOK (check_subst_overapproximation R R') ⟷
(∀(l, r) ∈ set R. ∃(l', r') ∈ set R'. ∃σ. l = l' ⋅ σ ∧ r = r' ⋅ σ)"
by (force simp: check_subst_overapproximation_def)
datatype ('f, 'v) nonreachability_proof =
Nonreachable_Tcap
| Nonreachable_Gtcap
| Nonreachable_ETAC "('f × nat) list" "'f" "'f" "('f, 'v) etac_ta"
| Nonreachable_Subst_Approx "('f, 'v) rules" "('f, 'v) nonreachability_proof"
| Nonreachable_Reverse "('f, 'v) nonreachability_proof"
definition "rule_map R fn =
case_option [] (map snd) (rm.lookup fn (insert_rules () R (rm.empty ())))"
lemma rule_map:
"set (rule_map R fn) = {(l, r) ∈ set R. root l = Some fn}" (is "?A = ?B")
proof
let ?rm = "insert_rules () R (rm.empty ())"
have rm_inj: "rm_inj ?rm" by (simp)
show "?A ⊆ ?B"
proof
fix l r assume *: "(l, r) ∈ set (rule_map R fn)"
then show "(l, r) ∈ ?B"
proof (cases "rm.lookup fn ?rm")
case (Some rs)
with * have 2: "(l, r) ∈ snd `set rs" by (simp add: rule_map_def)
from Some and rm_inj have "∀r∈set rs. key r = Some fn"
by (metis (no_types, lifting) mmap_inj_def rm.correct(5) rm.invar rm_inj_def)
moreover from 2 obtain a where "(a, l, r) ∈ set rs" by auto
ultimately have "key ((), l, r) = Some fn" by simp
then have root: "root l = Some fn" by (cases l, simp_all)
from Some_in_values[OF Some] have "set rs ⊆ set (values ?rm)" .
then have "(l, r) ∈ snd ` set (values ?rm)" using 2 by auto
then have "(l, r) ∈ set R" by (auto simp: values_rules_with_conv_unit)
with root show ?thesis by simp
qed (simp add: rule_map_def)
qed
next
let ?rm = "insert_rules () R (rm.empty ())"
have rm_inj: "rm_inj ?rm" by (simp)
show "?B ⊆ ?A"
proof
fix l r assume "(l, r) ∈ ?B"
then have 1: "(l, r) ∈ set R" and "root l = Some fn" by auto
from ‹root l = Some fn› obtain f and n and ts where [simp]: "fn = (f, n)" "length ts = n"
and l: "l = Fun f ts" by (cases l) auto
from 1
have "(l, r) ∈ set (Rule_Map.rules ?rm)"
unfolding l by (auto simp: values_rules_with_conv_unit)
then have "((), l, r) ∈ set (values ?rm)" by auto
from this[unfolded values_ran[unfolded ran_def]]
obtain k vs where lookup: "rm.lookup k ?rm = Some vs"
and "((), l, r) ∈ set vs" by (auto simp: rm.correct)
then have 2: "(l, r) ∈ set (rule_map R k)" by (force simp: rule_map_def)
have k: "k = (f, n)"
proof -
from ‹root l = Some fn› have "length ts = n" by (simp add: l)
from lookup and ‹((), l, r) ∈ set vs›
have "key ((), l, r) = Some k"
apply (auto simp: rm.correct)
by (meson mmap_inj_def rm_inj rm_inj_def)
thus ?thesis by (simp add: l)
qed
from 2 show "(l, r) ∈ ?A" unfolding k by simp
qed
qed
fun check_nonreachable :: "('f::{key, show}, 'v::{key, show}) rules ⇒ _"
where
"check_nonreachable R s t Nonreachable_Tcap =
check (¬ Ground_Context.match (tcapI R s) t)
(shows ''could not show nonreachability via tcap'')"
| "check_nonreachable R s t Nonreachable_Gtcap = do {
let nlv = (∀lr ∈ set R. is_Fun (fst lr));
let fs = funas_trs_list R in
check (¬ Ground_Context.match (tcapI R s) t ∨
nonreachable_gtcapRM fs nlv (R ≠ []) (mk_gt_fun R) (rule_map R) s t)
(shows ''could not show nonreachability via generalized tcap'')
}"
| "check_nonreachable R s t (Nonreachable_ETAC F a c A) =
check_etac_nonreachable F a c A R s t"
| "check_nonreachable R s t (Nonreachable_Subst_Approx R' p) =
check_subst_overapproximation R R' ⪢ check_nonreachable R' s t p"
| "check_nonreachable R s t (Nonreachable_Reverse p) =
check_nonreachable (map (λ(x, y). (y, x)) R) t s p"
lemma check_nonreachable [simp]:
assumes "isOK (check_nonreachable R s t p)"
shows "¬ (∃σ τ. (s ⋅ σ, t ⋅ τ) ∈ (rstep (set R))⇧*)"
using assms
proof (induct p arbitrary: R s t)
case Nonreachable_Tcap
with match_tcap_sound [of s _ t _ "set R"] show ?case by auto
next
case Nonreachable_Gtcap
with match_tcap_sound [of s _ t _ "set R"]
nonreach_gtcap [OF refl rule_map, of R s t]
show ?case by auto
next
case (Nonreachable_ETAC F a c A)
with check_etac_nonreachable [of F a c A R s t] show ?case by auto
next
case (Nonreachable_Subst_Approx R' p)
then have "(∀(l, r) ∈ set R. ∃(l', r') ∈ set R'. ∃σ. l = l' ⋅ σ ∧ r = r' ⋅ σ)"
and "¬ (∃σ τ. (s ⋅ σ, t ⋅ τ) ∈ (rstep (set R'))⇧*)" by auto
with rstep_subst_overapproximation [OF this(1), THEN rtrancl_mono] show ?case by blast
next
case *: (Nonreachable_Reverse p)
have [simp]: "(λ(x, y). (y, x)) ` set R = (set R)¯" by auto
have "¬ (∃σ τ. (t ⋅ σ, s ⋅ τ) ∈ (rstep ((set R)¯))⇧*)" using * by force
with rsteps_imp_rev_rsteps [of "s ⋅ σ" "t ⋅ τ" "set R" for σ τ]
show ?case by auto
qed
datatype ('f, 'v) nonjoinability_proof =
Nonjoinable_Tcap
| Nonjoinable_Ground_NF "('f, 'v) nonreachability_proof"
fun check_nonjoinable
where
"check_nonjoinable R s t Nonjoinable_Tcap =
check (¬ Ground_Context.unifiable (tcapI R s) (tcapI R t))
(shows ''could not show nonjoinability via tcap'')"
| "check_nonjoinable R s t (Nonjoinable_Ground_NF p) =
(if is_NF_trs R s ∧ ground s then check_nonreachable R t s p
else if is_NF_trs R t ∧ ground t then check_nonreachable R s t p
else error (shows ''non NF''))"
lemma check_nonjoinable [simp]:
assumes "isOK (check_nonjoinable R s t p)"
shows "¬ (∃σ. (s ⋅ σ, t ⋅ σ) ∈ (rstep (set R))⇧↓)"
proof (cases p)
case Nonjoinable_Tcap
with assms show ?thesis using join_imp_unifiable_tcaps [of s _ t] by auto
next
case (Nonjoinable_Ground_NF q)
then show ?thesis
using assms by (auto dest!: check_nonreachable split: if_splits)
(metis NF_join_imp_reach join_sym ground_subst_apply)+
qed
end