theory Subterm_Criterion_Impl
imports
Subterm_Criterion
QTRS.QDP_Framework_Impl
QTRS.Map_Choice
"Check-NT.Q_Restricted_Rewriting_Impl"
begin
definition
check_strict_rstep ::
"('f::show, 'v::show) rules ⇒
(('f, 'v) rule ⇒ ('f, 'v) rseq option) ⇒
'f proj ⇒ ('f, 'v) rule ⇒ shows check"
where
"check_strict_rstep R rseqm p r = (
let s = proj_term p (fst r); t = proj_term p (snd r) in
case rseqm r of
None ⇒ check_supt s t
| Some rseq ⇒ (if length rseq = 0
then check_supt s t
else (
check_rsteps_last R s rseq
>> check_supteq (rseq_last s rseq) t)))"
definition
check_strict_one_rstep ::
"('f::show, 'v::show) rules ⇒
(('f, 'v) rule ⇒ ('f, 'v) rseq option) ⇒
'f proj ⇒ ('f, 'v) rule ⇒ shows check"
where
"check_strict_one_rstep R rseqm p r = (
let s = proj_term p (fst r); t = proj_term p (snd r) in
case rseqm r of
None ⇒ check_supt s t
| Some [(pos, rule, u)] ⇒ (
check_qrstep (λ _. True) False R pos rule s u
>> check_supteq u t)
| Some _ ⇒ error (shows_string ''more than a single rewrite step is not allowed''))"
lemma check_strict_rstep_sound:
assumes "isOK (check_strict_rstep R rseqm p r)"
shows "(proj_term p (fst r), proj_term p (snd r)) ∈ ({⊳} ∪ rstep (set R))^+"
(is "(?s, ?t) ∈ ({⊳} ∪ rstep (set R))^+")
proof (cases "rseqm r")
case None
from assms[unfolded check_strict_rstep_def None]
have "isOK (check_supt ?s ?t)" by simp
hence "(?s, ?t) ∈ {⊳}" by simp
thus ?thesis by auto
next
case (Some rseq)
show ?thesis
proof (cases "length rseq = 0")
case True
with assms[unfolded check_strict_rstep_def Some]
have "isOK (check_supt ?s ?t)" by simp
hence "(?s, ?t) ∈ {⊳}" by simp
thus ?thesis by auto
next
let ?u = "rseq_last ?s rseq"
case False
with assms[unfolded check_strict_rstep_def Some]
have "isOK (check_rsteps_last R ?s rseq >> check_supteq ?u ?t)" unfolding Let_def by simp
hence "(?s, ?u) ∈ (rstep (set R))^^(length rseq)" and "(?u, ?t) ∈ {⊵}"
using check_rsteps_last_sound_length[of R ?s rseq] by auto
with False obtain n where "(?s, ?u) ∈ (rstep (set R))^^(Suc n)" by (induct rseq) simp_all
hence "(?s, ?u) ∈ (rstep (set R))^+" using trancl_power[of _ "rstep (set R)"] by blast
from ‹(?u, ?t) ∈ {⊵}› show ?thesis unfolding supteq_supt_conv
proof
assume "?u = ?t"
from ‹(?s, ?u) ∈ (rstep (set R))^+›
show ?thesis unfolding ‹?u = ?t› using trancl_union_right[of "rstep (set R)" "{⊳}"] by blast
next
assume "(?u, ?t) ∈ {⊳}"
hence "(?u, ?t) ∈ ({⊳} ∪ rstep (set R))^+" by auto
moreover from ‹(?s, ?u) ∈ (rstep (set R))^+›
have "(?s, ?u) ∈ ({⊳} ∪ rstep (set R))^+" using trancl_union_right by blast
ultimately show ?thesis by simp
qed
qed
qed
lemma check_strict_one_rstep_sound:
assumes ok: "isOK (check_strict_one_rstep R rseqm p r)"
shows "(proj_term p (fst r), proj_term p (snd r)) ∈ ({⊳} ∪ rstep (set R) O {⊵})"
(is "(?s, ?t) ∈ ({⊳} ∪ ?S)")
proof (cases "rseqm r")
case None
from ok[unfolded check_strict_one_rstep_def None]
show ?thesis by auto
next
case (Some prus)
show ?thesis
proof (cases prus)
case Nil
from ok[unfolded check_strict_one_rstep_def Some Nil]
show ?thesis by simp
next
case (Cons pru prus')
note Cons' = this
show ?thesis
proof (cases prus')
case (Cons pru' prus'')
from ok[unfolded check_strict_one_rstep_def Some Cons' Cons]
show ?thesis by simp
next
case Nil
with Cons obtain p r u where pru: "pru = (p, r, u)" by (cases pru) auto
with Nil and Cons have prus: "prus = [(p, r, u)]" by simp
from ok[unfolded check_strict_one_rstep_def Some Cons Nil, simplified]
have okstep: "isOK (check_qrstep (λ _. True) False R p r ?s u)"
and supteq: "isOK (check_supteq u ?t)" unfolding pru by auto
from check_qrstep_qrstep[OF _ okstep, of Nil]
and supteq[unfolded isOK_check_supteq]
show ?thesis by auto
qed
qed
qed
definition
check_weak :: "'f proj ⇒ ('f::show, 'v::show) rule ⇒ shows check"
where
"check_weak p r ≡ check (proj_term p (fst r) = proj_term p (snd r))
(''the projected lhs is not equal to the projected rhs'' +#+ shows_nl)
<+? (λs. ''Could not orient rule '' +#+ shows_rule r +@+ '', since'' +#+ shows_nl +@+
shows (proj_term p (fst r)) +@+ '' != '' +#+ shows (proj_term p (snd r)) +@+
shows_nl +@+ s)"
lemma check_weak_sound[simp]:
assumes "isOK (check_weak p r)"
shows "proj_term p (fst r) = proj_term p (snd r)"
using assms unfolding check_weak_def by auto
datatype ('f) projL = Projection "(('f × nat) × nat) list"
fun
create_proj :: "('f :: key) projL ⇒ 'f proj"
where
"create_proj (Projection p) = (let I = ceta_map_of p in (λ f. case I f of None ⇒ 0 | Some n ⇒ n))"
fun
create_rseq_map :: "(('f :: key, 'v :: key) rule × ('f, 'v) rseq) list ⇒ (('f, 'v) rule ⇒ ('f, 'v) rseq option)"
where
"create_rseq_map rseqs = ceta_map_of rseqs"
definition
subterm_criterion_proc ::
"('dpp, 'f::{key,show}, 'v::{key,show}) dpp_ops ⇒
'f projL ⇒ (('f, 'v) rule × ('f, 'v) rseq)list ⇒
('f, 'v) rules ⇒ 'dpp proc"
where
"subterm_criterion_proc I pL rseqmL Prm dpp = check_return (do {
let p = create_proj pL;
let rseqm = create_rseq_map rseqmL;
let P = dpp_ops.pairs I dpp;
let nfs = dpp_ops.nfs I dpp;
let R = dpp_ops.rules I dpp;
let P' = snd (dpp_ops.split_pairs I dpp Prm);
let wfR = wf_rules_impl R;
check_allm (λ(l, r). do {
check_no_var l;
check_no_var r;
check_no_defined_root (dpp_spec.is_defined I dpp) r
}) P;
check (dpp_ops.minimal I dpp ∨ dpp_ops.NFQ_subset_NF_rules I dpp) (shows ''minimality or innermost required'');
check_allm (λ(l, r). check_no_var l) R;
(if dpp_ops.Q_empty I dpp
then check_allm (check_strict_rstep R rseqm p) Prm
else check_allm (check_strict_one_rstep wfR rseqm p) Prm);
check_allm (check_weak p) P'
}) (dpp_spec.delete_pairs I dpp Prm)"
lemma subterm_criterion_proc: assumes "dpp_spec I"
shows "dpp_spec.sound_proc_impl I (subterm_criterion_proc I p rseqm ps)"
proof -
interpret dpp_spec I by fact
show ?thesis
proof
fix d d'
assume ok: "subterm_criterion_proc I p rseqm ps d = return d'"
and fin: "finite_dpp (dpp_ops.dpp I d')"
let ?S = "set ps"
let ?P = "set (dpp_ops.P I d)"
let ?Pw = "set (dpp_ops.Pw I d)"
let ?P' = "?P ∪ ?Pw"
let ?Q = "set (dpp_ops.Q I d)"
let ?R = "set (dpp_ops.R I d)"
let ?Rw = "set (dpp_ops.Rw I d)"
let ?nfs = "dpp_ops.nfs I d"
let ?m = "dpp_ops.minimal I d"
let ?R' = "?R ∪ ?Rw"
let ?wfR = "wf_rules (?R')"
let ?π = "proj_term (create_proj p)"
let ?rseqm = "create_rseq_map rseqm"
show "finite_dpp (dpp_ops.dpp I d)"
proof (cases "dpp_ops.split_pairs I d ps")
case (Pair D P')
from split_pairs_sound[OF Pair]
have D: "set D = (?P ∪ ?Pw) ∩ ?S"
and P': "set P' = (?P ∪ ?Pw) - ?S" by auto
let ?D = "set D"
note ok = ok[unfolded subterm_criterion_proc_def, simplified, simplified Pair, unfolded Let_def, simplified]
from ok
have cond: "∀(l, r)∈?P'.
is_Fun l ∧ is_Fun r ∧ ¬ defined ?R' (the (root r))" by simp
from ok have nvar: "∀(l, r)∈?R'. is_Fun l" by simp
from ok
have weak: "∀(l, r)∈set P'. ?π l = ?π r"
by (simp_all add: split_def Let_def Pair)
from ok
have strict: "?Q = {} ∧ (∀(l, r)∈?S. (?π l, ?π r) ∈ ({⊳} ∪ rstep ?R')^+) ∨
(∀(l, r)∈?S. (?π l, ?π r) ∈ {⊳} ∪ rstep ?wfR O {⊵})"
using check_strict_rstep_sound[of "dpp_ops.rules I d" ?rseqm "create_proj p"]
using check_strict_one_rstep_sound[of "wf_rules_impl (dpp_ops.rules I d)" ?rseqm "create_proj p"]
by (cases "?Q = {}", simp_all add: split_def Pair D P')
from ok have m: "?m ∨ NF_terms ?Q ⊆ NF_trs ?R'" by simp
from ok have d': "d' = dpp_spec.delete_pairs I d ps" by simp
have proc: "Subterm_Criterion.subterm_criterion_proc (create_proj p) ?S
(?nfs,?m,?P, ?Pw, ?Q, ?R, ?Rw) (?nfs,?m,?P - ?S, ?Pw - ?S, ?Q, ?R, ?Rw)"
by (simp add: subterm_criterion_cond_def cond P' weak, insert strict m nvar, auto)
note fin = fin[unfolded d' delete_P_Pw_sound]
show ?thesis unfolding dpp_spec_sound d'
by (rule subset_proc[OF fin proc subset_subterm_criterion_proc])
qed
qed
qed
end