theory Usable_Rules_NJ_Unif_Impl
imports
Usable_Rules_NJ_Unif
"Check-NT.Tcap_Impl"
begin
definition check_contains where "check_contains U V =
check_allm (λ lr. check (lr ∈ rstep U) (shows ''rule '' +@+ shows_rule lr +@+ shows '' is not contained'')) V"
lemma contains_code[code]: "contains U V = (∀ lr ∈ V. lr ∈ rstep U)"
unfolding contains_def by auto
lemma check_contains[simp]: "isOK(check_contains U V) = contains U (set V)"
unfolding contains_code check_contains_def by auto
definition check_contains_U0 where
"check_contains_U0 R U s ≡
check_allm (λ fts. case fts of
Var _ ⇒ succeed
| Fun f ts ⇒ let tcapb = tcap_below U f ts
in check_allm (λ lr.
case gc_matcher tcapb (fst lr) of
None ⇒ succeed
| Some σ ⇒ let irule = (fst lr ⋅ σ, snd lr ⋅ σ)
in check (irule ∈ rstep U) (
shows ''When considering the subterm '' +@+ shows fts +@+ shows_nl
+@+ shows ''and the rule '' +@+ shows_rule lr +@+ shows_nl
+@+ shows ''the capped subterm is '' +@+ shows tcapb +@+ shows_nl
+@+ shows ''leading to the mgu with the lhs: '' +@+ shows (map (λ x. (x, σ x)) (vars_term_list (fst lr))) +@+ shows_nl
+@+ shows ''The instantiated rule '' +@+ shows irule +@+ shows_nl
+@+ shows ''cannot be simulated by the given set of usable rules''
)) R) (supteq_list s)"
lemma isOK_case_term [simp]:
"isOK (case t of Var x ⇒ P x | Fun f ts ⇒ Q f ts) =
(case t of Var x ⇒ isOK (P x) | Fun f ts ⇒ isOK (Q f ts))"
by (cases t) auto
lemma check_contains_U0[simp]: "isOK(check_contains_U0 R U s) = contains U (U0 (set R) U s)" (is "?l = ?r")
proof -
note cd = contains_def
note ccd = check_contains_U0_def
note simps = isOK_check_allm isOK_check
let ?p = "λ f ts. (∀lr∈ set R. case gc_matcher (tcap_below U f ts) (fst lr) of None ⇒ True | Some σ ⇒ (fst lr ⋅ σ, snd lr ⋅ σ) ∈ rstep U)"
{
assume "¬ ?l"
from this[unfolded ccd Let_def, simplified, unfolded simps]
obtain f ts where s: "s ⊵ Fun f ts" and not: "¬ ?p f ts"
by (force split: term.splits option.splits)
from not obtain l r σ where lr: "(l,r) ∈ set R" and mgu: "gc_matcher (tcap_below U f ts) l = Some σ" and
not: "(l ⋅ σ, r ⋅ σ) ∉ rstep U" by (auto split: option.splits)
from match_non_var[OF lr s mgu] not have "¬ ?r" unfolding cd by auto
}
moreover
{
assume ?l
have ?r unfolding cd
proof
fix ls rs
assume "(ls,rs) ∈ U0 (set R) U s"
thus "(ls,rs) ∈ rstep U"
proof (cases)
case (match_non_var l r f ts σ)
from match_non_var(4) ‹?l›[unfolded ccd Let_def, simplified, unfolded simps]
have "?p f ts" by (auto split: option.splits term.splits)
with match_non_var show ?thesis by auto
qed
qed
}
ultimately show ?thesis by auto
qed
definition check_usable_instantiation where
"check_usable_instantiation R U s ≡ do {
let UU = set U;
check_contains_U0 R UU s
<+? (λ s. shows ''U <= U0(R,s) required'' +@+ shows_nl +@+ s);
check_allm (λ r. check_contains_U0 R UU r
<+? (λ s. shows ''U <= U0(R,r) for rhs r = '' +@+ shows r +@+ shows '' required'' +@+ shows_nl +@+ s))
(map snd U)
}"
lemma check_usable_instantiation[simp]:
"isOK(check_usable_instantiation R U s) = usable_instantiation (set R) (set U) s"
unfolding check_usable_instantiation_def usable_instantiation_def Let_def
by simp
definition check_usable_rules_unif where "
check_usable_rules_unif R U s ≡ do {
check (ground s ∨ (∀ l ∈ set (map fst R). is_Fun l)) (''since '' +#+ shows s
+@+ shows '' is not ground, left-hand sides of R must not be variables'');
check_varcond_subset U;
check_usable_instantiation R U s <+? (λ s. ''closure properties of usable rules not satisfied'' +#+ shows_nl +@+ s)
} <+? (λ e. ''problem in checking validity of usable rules U = '' +#+ shows_nl +@+ shows_trs U +@+ shows_nl +@+ shows ''for term '' +@+ shows s +@+
shows_nl +@+ ''wrt TRS R = '' +#+ shows_nl +@+ shows_trs R +@+ shows_nl +@+ e)"
lemma check_usable_rules_unif_left: assumes ok: "isOK(check_usable_rules_unif Rs U s)"
and nj: "¬ (∃ u. (s,u) ∈ (rstep (set U))^* ∧ (t,u) ∈ (rstep Rt)^*)"
shows "¬ (∃ u. (s,u) ∈ (rstep (set Rs))^* ∧ (t,u) ∈ (rstep Rt)^*)" (is "¬ ?join")
proof
assume ?join
then obtain u where su: "(s,u) ∈ (rstep (set Rs))^*" and tu: "(t,u) ∈ (rstep Rt)^*" by auto
have "(s,u) ∈ (rstep (set U))^*"
by (rule usable_instantiation_rsteps_main[OF _ _ su, of "set U", THEN conjunct1],
insert ok[unfolded check_usable_rules_unif_def], auto simp: no_lhs_var_def)
with tu nj show False by auto
qed
lemma check_usable_rules_unif_right: assumes ok: "isOK(check_usable_rules_unif Rt U t)"
and nj: "¬ (∃ u. (s,u) ∈ (rstep Rs)^* ∧ (t,u) ∈ (rstep (set U))^*)"
shows "¬ (∃ u. (s,u) ∈ (rstep Rs)^* ∧ (t,u) ∈ (rstep (set Rt))^*)"
using check_usable_rules_unif_left[OF ok, of s Rs] nj by blast
end