theory Generic_Usable_Rules_Impl
imports
Generic_Usable_Rules
"Check-NT.Innermost_Usable_Rules_Impl"
Usable_Rules_Impl
begin
definition smart_usable_rules_checker :: "('f,string)usable_rules_checker"
where "smart_usable_rules_checker nfs m wwf π Q R U_opt sts ≡ case U_opt of None ⇒ Some R
| Some U ⇒ if NF_terms Q ⊆ NF_trs (set R) ∧ (nfs ∨ (∀ (s,t) ∈ sts. vars_term t ⊆ vars_term s)) ∧ (nfs ∨ m ∨ wwf) then
(let urc = is_ur_closed_term_mv' (set R) (set U) Q icap' π
in if (∀ (s,t) ∈ sts. urc {s} t) ∧ (∀ (l,r) ∈ set U. urc (set (args l)) r) then Some U else None) else
(let us = UNIV in if m ∧ (nfs ⟶ Q ≠ {} ⟶ wwf) ∧ ur_closed_af (set R) (set U) us π ∧ ur_P_closed_af (set R) (set U) us π sts then Some U else None)"
lemma smart_usable_rules_checker: "usable_rules_checker (smart_usable_rules_checker :: ('f,string)usable_rules_checker)"
unfolding usable_rules_checker_def
proof (intro allI impI)
fix Q R π U_opt sts U and S NS :: "('f,string)trs" and nfs m
assume check: "smart_usable_rules_checker nfs m (wwf_qtrs Q (set R)) π Q R U_opt sts = Some U"
and pair: "ce_af_redpair S NS π"
and orient: "set U ⊆ NS"
note check = check[unfolded smart_usable_rules_checker_def]
interpret ce_af_redpair S NS π by fact
let ?Q = "NF_terms Q"
let ?R = "qrstep nfs Q (set R)"
let ?wwf = "wwf_qtrs Q (set R)"
show "∃ f. ∀ s t u σ τ. (s,t) ∈ sts ⟶ s ⋅ σ ∈ ?Q ⟶ NF_subst nfs (s,t) σ Q ⟶ (t ⋅ σ, u ⋅ τ) ∈ ?R^* ⟶ (m ⟶ SN_on ?R {t ⋅ σ}) ⟶ (t ⋅ f σ, u ⋅ f τ) ∈ NS^*"
proof (cases U_opt)
case None
with check have U: "U = R" by simp
show ?thesis
proof (rule exI[of _ "λ x. x"], intro allI impI)
fix t u and σ τ :: "('f,string)subst"
assume steps: "(t ⋅ σ, u ⋅ τ) ∈ ?R^*"
show "(t ⋅ σ, u ⋅ τ) ∈ NS^*"
proof (rule set_mp[OF rtrancl_mono[OF subset_trans] steps])
show "?R ⊆ rstep (set R)" by auto
next
show "rstep (set R) ⊆ NS"
by (rule rstep_subset[OF wm_NS subst_NS orient[unfolded U]])
qed
qed
next
case (Some U')
note check = check[unfolded Some option.simps Let_def]
let ?inntest = "?Q ⊆ NF_trs (set R) ∧ (nfs ∨ (∀ (s,t) ∈ sts. vars_term t ⊆ vars_term s)) ∧ (nfs ∨ m ∨ ?wwf)"
show ?thesis
proof (cases ?inntest)
case True
hence "?inntest = True" by simp
note check = check[unfolded this if_True]
let ?urc = "is_ur_closed_term_mv' (set R) (set U') Q icap' π"
let ?urctest = "(∀ (s,t) ∈ sts. ?urc {s} t) ∧ (∀ (l,r) ∈ set U'. ?urc (set (args l)) r)"
have ?urctest
proof (cases ?urctest)
case False
hence "?urctest = False" by simp
from check[unfolded this] show ?thesis by simp
qed
with check have U: "U = U'" by simp
show ?thesis
proof (rule exI[of _ "λ x. x"], intro allI impI)
fix s t u and σ τ :: "('f,string)subst"
assume st: "(s,t) ∈ sts" and NF: "s ⋅ σ ∈ ?Q"
and nfsigma: "NF_subst nfs (s,t) σ Q"
and steps: "(t ⋅ σ, u ⋅ τ) ∈ ?R^*"
and SN: "m ⟶ SN_on ?R {t ⋅ σ}"
from ‹?inntest› st have vars: "¬ nfs ⟹ vars_term t ⊆ vars_term s" by auto
interpret R_Q_U_ecap "set R" "set U'" Q icap'
by (unfold_locales, rule icap, insert ‹?inntest› U, auto)
show "(t ⋅ σ, u ⋅ τ) ∈ NS^*"
proof (rule is_ur_closed_term_af[OF steps _ _ _ _])
assume "¬ nfs"
with SN True show "wwf_qtrs Q (set R) ∨ SN_on ?R {t ⋅ σ}" by auto
next
show "af_redpair S NS π" ..
next
show "{s} ⋅⇩s⇩e⇩t σ ⊆ ?Q" using NF by auto
next
{
fix x
assume x: "x ∈ vars_term t"
have "σ x ∈ ?Q"
proof (cases nfs)
case False
with vars x have "x ∈ vars_term s" by auto
hence "Var x ⊴ s" by auto
hence "Var x ⋅ σ ⊴ s ⋅ σ" by (rule supteq_subst)
from NF_subterm[OF NF this]
show ?thesis by simp
next
case True
with x nfsigma show ?thesis unfolding NF_subst_def vars_rule_def by auto
qed
}
thus "σ ` vars_term t ⊆ NF_terms Q" by auto
next
show "set U' ⊆ NS" using orient U by auto
qed (insert ‹?urctest› U st, auto)
qed
next
case False
hence "?inntest = False" by simp
note check = check[unfolded this if_False]
let ?u1 = "ur_closed_af (set R) (set U') UNIV π"
let ?u2 = "ur_P_closed_af (set R) (set U') UNIV π sts"
let ?urctest = "m ∧ (nfs ⟶ Q ≠ {} ⟶ ?wwf) ∧ ?u1 ∧ ?u2"
from check have ?urctest by (cases ?urctest, auto)
with check have U: "U = U'" and u1: ?u1 and u2: ?u2 by auto
from NS_ce_compat obtain k where ce: "⋀ m. m ≥ k ⟹ ce_trs (c,m) ⊆ NS" by blast
hence ce: "ce_trs (c,k + n) ⊆ NS" by auto
interpret itrans Q "set R" "set R" "{}" "set U'" UNIV "(c,k+n)" by (rule itrans, insert itrans_ac_empty, auto)
let ?I = "i_trans_subst"
from orient U have orient: "set U' ⊆ mode_left False" unfolding mode_left_def by auto
show ?thesis
proof (rule exI[of _ ?I], intro allI impI)
fix s t u :: "('f,string)term" and σ τ
assume st: "(s,t) ∈ sts" and NF: "s ⋅ σ ∈ ?Q"
and steps: "(t ⋅ σ, u ⋅ τ) ∈ ?R^*"
and SNt: "m ⟶ SN_on ?R {t ⋅ σ}"
from wwf_qtrs_imp_nfs_False_switch[of nfs Q "set R"] ‹?urctest›
have switch: "?R = qrstep False Q (set R)" (is "_ = ?R'") by auto
from switch SNt ‹?urctest› have SNt: "SN_on ?R' {t ⋅ σ}" by simp
note steps = steps[unfolded switch]
show "(t ⋅ ?I σ, u ⋅ ?I τ) ∈ NS^*"
by (rule i_trans_sound_dp[OF _ _ _ _ st steps SNt u1 _ orient, unfolded mode_NS_def if_False],
insert mode_cond_def u2 st, auto)
qed
qed
qed
qed
type_synonym ('d,'f)usable_rules_checker_impl = "('d,'f,string)dpp_ops ⇒ 'd ⇒ 'f af ⇒ ('f,string)rules option ⇒ ('f,string)rules ⇒ ('f,string)rules result"
definition smart_usable_rules_checker_impl :: "('d,'f :: {key,show})usable_rules_checker_impl"
where "smart_usable_rules_checker_impl I d π U_opt sts ≡
let nfs = dpp_ops.nfs I d;
m = dpp_ops.minimal I d;
wwf = dpp_ops.wwf_rules I d;
qempty = dpp_ops.Q_empty I d
in case U_opt of None ⇒ return (dpp_ops.rules I d)
| Some U ⇒ if
dpp_ops.NFQ_subset_NF_rules I d
∧ (nfs ∨ isOK(check_varcond_subset sts))
∧ (nfs ∨ m ∨ wwf)
then do {
let urc = is_ur_closed_af_impl_dpp_mv I d π U;
let check_urc = (λ S t. check (urc S t) (shows ''term '' +@+ shows t +@+ shows '' is not closed under usable rules''));
check_allm (λ(s, t). check_urc [s] t) sts;
check_allm (λ(l,r). check_urc (args l) r) U;
return U
}
else do {
check (m ∧ (nfs ⟶ qempty ∨ wwf)) (shows ''minimality and well formedness required'');
check_allm (λ (l,r). check (is_Fun l) (shows ''variables as lhss not allowed'')) (dpp_ops.rules I d);
let rm = dpp_ops.rules_map I d;
check_ur_P_closed_rm_af rm U π sts;
return U
}"
lemma smart_usable_rules_checker_impl: assumes I: "dpp_spec I"
and check: "smart_usable_rules_checker_impl I d π U_opt sts = return U"
shows "smart_usable_rules_checker (dpp_ops.nfs I d) (dpp_ops.minimal I d) (wwf_qtrs (set (dpp_ops.Q I d)) (set (dpp_ops.rules I d))) π (set (dpp_ops.Q I d)) (dpp_ops.rules I d) U_opt (set sts) = Some U" (is "?l = Some U")
proof -
interpret dpp_spec I by fact
let ?nfs = "NFS d"
let ?m = "M d"
let ?R = "set (R d) ∪ set (Rw d)"
have id: "set (rules d) = ?R" by auto
let ?wwf = "wwf_qtrs (set (Q d)) ?R"
note check = check[unfolded smart_usable_rules_checker_impl_def Let_def]
note d = smart_usable_rules_checker_def[of ?nfs ?m ?wwf π _ _ U_opt "set sts"]
show ?thesis
proof (cases U_opt)
case None
with check have U: "U = dpp_ops.rules I d" by simp
thus ?thesis using d unfolding None U by simp
next
case (Some U')
note d = d[unfolded Some option.simps]
let ?Q = "set (Q d)"
note d = d[of ?Q "rules d", unfolded id]
note check = check[unfolded Some option.simps dpp_spec_sound check_varcond_subset set_vars_term_list]
let ?inntest = "NF_terms ?Q ⊆ NF_trs ?R ∧ (?nfs ∨ (∀ (s,t) ∈ set sts. vars_term t ⊆ vars_term s)) ∧ (?nfs ∨ ?m ∨ ?wwf)"
show ?thesis
proof (cases ?inntest)
case True
hence inn: "?inntest = True" by simp
note d = d[unfolded dpp_spec_sound, unfolded inn if_True Let_def]
note check = check[unfolded inn if_True Let_def, simplified, unfolded is_ur_closed_af_impl_dpp_mv[OF I], simplified dpp_spec_sound]
thus ?thesis unfolding Some using d by auto
next
case False
hence ninn: "?inntest = False" by simp
note d = d[unfolded dpp_spec_sound, unfolded ninn if_False Let_def]
note check' = check[unfolded ninn if_False Let_def, simplified]
from check' have check: "isOK(check_ur_P_closed_rm_af (rules_map d) U' π sts)" and U: "U' = U" by auto
have id': "?R = set (rules d)" by simp
have "ur_closed_af ?R (set U') UNIV π ∧
ur_P_closed_af ?R (set U') UNIV π (set sts)" (is "?ur1 ∧ ?ur2")
unfolding id'
by (rule check_ur_P_closed_rm_af_sound[OF _ _ check], insert check', auto)
thus ?thesis unfolding Some id unfolding d unfolding U using check' by auto
qed
qed
qed
end