Theory TRS.Q_Restricted_Rewriting_Impl
theory Q_Restricted_Rewriting_Impl
imports
First_Order_Rewriting.Trs_Impl
Q_Restricted_Rewriting
begin
definition prop_rstep_r_p_s where
"prop_rstep_r_p_s nfs P R r p σ = {(s, t).
(∀ u ∈ set (args (s |_ p)). P u) ∧
p ∈ poss s ∧ r ∈ R ∧ s |_ p = fst r ⋅ σ ∧ t = replace_at s p (snd r ⋅ σ) ∧
(nfs ⟶ Ball (σ ` vars_rule r) P)}"
definition
check_prop_rstep_rule ::
"bool ⇒ ((_, _) term ⇒ showsl check) ⇒
pos ⇒ (_,_) rule ⇒ (_,_) term ⇒ (_,_) term ⇒
showsl check"
where
"check_prop_rstep_rule nfs P p rule s t ≡ do {
check (p ∈ poss s) (showsl_pos p ∘ showsl (STR '' is not a position of '') ∘ showsl s ∘ showsl_nl);
check (p ∈ poss t) (showsl_pos p ∘ showsl (STR '' is not a position of '') ∘ showsl t ∘ showsl_nl);
let C = ctxt_of_pos_term p s;
let D = ctxt_of_pos_term p t;
let u = subt_at s p;
let v = subt_at t p;
(case match_list Var [(fst rule, u), (snd rule, v)] of
Some τ ⇒
check_allm P (args u @ (if nfs then map τ (vars_rule_list rule) else []))
>> check (C = D)
(showsl (STR ''the term '') ∘ showsl t
∘ showsl (STR '' does not result from a proper application of rule⏎'')
∘ showsl_rule rule ∘ showsl (STR '' at position '') ∘ showsl_pos p ∘ showsl_nl)
| None ⇒
error (showsl (STR ''the term '') ∘ showsl t
∘ showsl (STR '' does not result from a proper application of rule⏎'')
∘ showsl_rule rule ∘ showsl (STR '' at position '') ∘ showsl_pos p ∘ showsl_nl))
}"
lemma check_prop_rstep_rule [simp]:
"isOK (check_prop_rstep_rule nfs P p r s t) =
(∃σ. (s, t) ∈ prop_rstep_r_p_s nfs (λ t. isOK (P t)) {r} r p σ)" (is "?l = ?r")
proof
assume ok: ?l
let ?C = "ctxt_of_pos_term p s"
let ?D = "ctxt_of_pos_term p t"
let ?mlist = "[(subt_at s p, fst r), (subt_at t p, snd r)]"
note ok = ok[unfolded check_prop_rstep_rule_def Let_def, simplified]
from ok have "p ∈ poss s" and "p ∈ poss t" by auto
from ok obtain σ where some: "match_list Var [(fst r, s |_ p), (snd r, t |_ p)] = Some σ"
by force
let ?σ = "σ"
note ok = ok[unfolded some option.simps, simplified]
from match_list_sound [OF some] have "fst r ⋅ ?σ = s |_ p" and "snd r ⋅ ?σ = t |_ p" by auto
then have "s |_ p = fst r ⋅ ?σ" and "t = ?D⟨snd r ⋅ ?σ⟩"
using ctxt_supt_id[OF ‹p ∈ poss t›] by simp+
moreover from ok
have "?D = ?C" by simp
moreover from ok
have "⋀ t. t ∈ set (args (s |_ p)) ⟹ isOK (P t)" by simp
moreover from ok
have "nfs ⟹ Ball (?σ ` vars_rule r) (λ x. isOK( P x))" by auto
ultimately have "(s, t) ∈ prop_rstep_r_p_s nfs (λ t. isOK (P t)) {r} r p ?σ"
using ‹p ∈ poss s› unfolding prop_rstep_r_p_s_def some by force
then show ?r by blast
next
assume r: ?r
let ?P = "λ t. isOK (P t)"
from r obtain σ where step: "(s, t) ∈ prop_rstep_r_p_s nfs ?P {r} r p σ" by auto
let ?C = "ctxt_of_pos_term p s"
let ?D = "ctxt_of_pos_term p t"
from step have "p ∈ poss s"
and P: "∀u ∈ set (args (s |_ p)). ?P u"
and s: "s |_ p = fst r ⋅ σ" and t: "t = ?C⟨snd r ⋅ σ⟩"
and P2: "nfs ⟹ Ball (σ ` vars_rule r) ?P"
unfolding prop_rstep_r_p_s_def by auto
from hole_pos_ctxt_of_pos_term[OF ‹p ∈ poss s›]
have p: "p = hole_pos ?C" by simp
obtain τ where match: "match_list Var [(fst r, s |_ p), (snd r, t |_ p)] = Some τ"
and tau: "∀x∈lvars [(fst r, s |_ p), (snd r, t |_ p)]. τ x = σ x"
proof -
from subt_at_hole_pos[of "?C" "snd r ⋅ σ", unfolded t[symmetric]]
have 2: "t |_ p = snd r ⋅ σ" unfolding p[symmetric] .
assume *: "⋀τ. ⟦match_list Var [(fst r, s |_ p), (snd r, t |_ p)] = Some τ;
∀x∈lvars [(fst r, s |_ p), (snd r, t |_ p)]. τ x = σ x⟧ ⟹ thesis"
show ?thesis
proof -
from match_list_complete' [of "[(fst r, s |_ p), (snd r, t |_ p)]" σ, unfolded s 2]
obtain σ' where "match_list Var [(fst r, s |_ p), (snd r, t |_ p)] = Some σ'"
and "∀x ∈ lvars [(fst r, s |_ p), (snd r, t |_ p)]. σ x = σ' x"
unfolding s 2 by (metis (lifting, no_types) Pair_inject empty_iff empty_set set_ConsD)
from * [OF this(1)] and this(2) show ?thesis by simp
qed
qed
have "p ∈ set (poss_list s)" by (simp add: ‹p ∈ poss s›)
moreover have "p ∈ set (poss_list t)"
using p and hole_pos_poss[of "?C" "snd r ⋅ σ"] by (simp add: t)
moreover have "isOK(check_allm P (args (s |_ p)))" using P by auto
moreover have "?C = ?D"
proof -
from hole_pos_id_ctxt[OF t[symmetric]]
show ?thesis unfolding p[symmetric] ..
qed
ultimately show ?l using match tau P2 unfolding check_prop_rstep_rule_def Let_def by (auto simp: vars_rule_def)
qed
definition
check_prop_rstep ::
"bool ⇒ ((_,_) term ⇒ showsl check) ⇒
(_,_) rules ⇒
pos ⇒ (_,_) rule ⇒ (_,_) term ⇒ (_,_) term ⇒
showsl check"
where
"check_prop_rstep nfs P R p rule s t ≡ do {
check (∃ r ∈ set R. (rule =⇩v r) ∧ isOK(check_prop_rstep_rule nfs P p r s t))
(showsl (STR ''the step from '') ∘ showsl s ∘ showsl (STR '' to '') ∘ showsl t ∘
showsl (STR '' via rule '') ∘ showsl_rule rule ∘
showsl (STR '' at position '') ∘ showsl_pos p ∘ showsl (STR '' is problematic⏎''))
}"
lemma check_prop_rstep_sound:
assumes ok: "isOK (check_prop_rstep nfs P R p r s t)"
shows "∃σ r'. (s, t) ∈ prop_rstep_r_p_s nfs (λ t. isOK(P t)) (set R) r' p σ ∧ r =⇩v r'"
proof -
note ok = ok[unfolded check_prop_rstep_def, simplified]
from ok obtain rule σ where rule: "rule ∈ set R" and instr: "r =⇩v rule"
and step: "(s, t) ∈ prop_rstep_r_p_s nfs (λt. isOK (P t)) {rule} rule p σ" by auto
from instr have inst: "(fst r, snd r) =⇩v (fst rule, snd rule)" by simp
from step rule have step: "(s, t) ∈ prop_rstep_r_p_s nfs (λt. isOK (P t)) (set R) rule p σ"
unfolding prop_rstep_r_p_s_def by auto
from eq_rule_mod_varsE[OF inst] obtain δ where fst: "fst r = fst rule ⋅ δ" and snd: "snd r = snd rule ⋅ δ" by auto
show ?thesis
by (intro exI conjI, rule step, rule instr)
qed
lemma check_prop_rstep_complete:
assumes "∃σ. (s, t) ∈ prop_rstep_r_p_s nfs (λ t. isOK (P t)) (set R) r p σ"
shows "isOK (check_prop_rstep nfs P R p r s t)"
proof -
let ?P = "λ t. isOK (P t)"
from assms obtain σ where step: "(s, t) ∈ prop_rstep_r_p_s nfs ?P (set R) r p σ" by auto
from step have step: "(s, t) ∈ prop_rstep_r_p_s nfs ?P {r} r p σ" and rule: "r ∈ set R"
unfolding prop_rstep_r_p_s_def by auto
have "r =⇩v r" by simp
with rule step show ?thesis unfolding check_prop_rstep_def by force
qed
definition
check_prop_rstep' ::
"bool ⇒ ((_,_) term ⇒ showsl check) ⇒
(_,_) rules ⇒
pos ⇒ (_,_) rule ⇒ (_,_) term ⇒ (_,_) term ⇒
showsl check"
where
"check_prop_rstep' nfs P R p rule s t ≡ do {
check (rule ∈ set R)
(showsl_rule rule ∘ showsl (STR '' is not a rule of⏎'') ∘ showsl_trs R ∘ showsl_nl);
check_prop_rstep_rule nfs P p rule s t
}"
lemma check_prop_rstep'[simp]:
"isOK (check_prop_rstep' nfs P R p r s t) =
(∃σ. (s, t) ∈ prop_rstep_r_p_s nfs (λ t. isOK(P t)) (set R) r p σ)"
unfolding check_prop_rstep'_def
by (auto simp: prop_rstep_r_p_s_def)
lemma prop_rstep_qrstep: "prop_rstep_r_p_s nfs (λ t. t ∈ NF_terms Q) = qrstep_r_p_s nfs Q" (is "?l = ?r")
proof (intro ext)
fix R r p σ
show "?l R r p σ = ?r R r p σ"
unfolding prop_rstep_r_p_s_def qrstep_r_p_s_def NF_terms_args_conv[symmetric]
using subt_at_ctxt_of_pos_term[of p "fst r ⋅ σ"]
by (auto simp: NF_subst_def)
qed
lemma prop_rstep_rstep: "prop_rstep_r_p_s nfs (λ t. True) = rstep_r_p_s" (is "?l = ?r")
by (intro ext, unfold prop_rstep_r_p_s_def rstep_r_p_s_def', simp)
lemma prop_rstep_qrstep_subst:
fixes μ :: "('f,'v)subst"
assumes nvar: "is_Fun (fst r)"
shows "(s,t) ∈ prop_rstep_r_p_s nfs (λ t. (∀ i. t ⋅ μ ^^ i ∈ NF_terms Q)) R r p σ = (∀ i. (s ⋅ μ ^^ i, t ⋅ μ ^^ i) ∈ qrstep_r_p_s nfs Q R r p (σ ∘⇩s μ ^^ i))" (is "?l = ?r")
proof -
let ?NF = "λ t i. (∀ i. t ⋅ μ ^^ i ∈ NF_terms Q)"
let ?c = "ctxt_of_pos_term p s"
let ?QR = "qrstep_r_p_s nfs Q R r p"
from nvar obtain f ls where l: "fst r = Fun f ls" by force
show ?thesis
proof
assume ?l
from this[unfolded prop_rstep_r_p_s_def Let_def, simplified]
have p: "p ∈ poss s" and r: "r ∈ R" and s: "s |_ p = fst r ⋅ σ" and t: "t = ?c⟨snd r ⋅ σ⟩"
and NF: "⋀ u i. u ∈ set (args (s |_ p)) ⟹ u ⋅ μ ^^ i ∈ NF_terms Q"
and nfs: "⋀ x i. nfs ⟹ x ∈ vars_rule r ⟹ σ x ⋅ μ ^^ i ∈ NF_terms Q" by auto
then obtain us where sp: "s |_ p = Fun f us" unfolding l by (cases "s |_ p", auto)
from p have p': "⋀ i. p ∈ poss (s ⋅ μ ^^ i)" by (rule poss_imp_subst_poss)
show ?r
proof
fix i
let ?C = "ctxt_of_pos_term p (s ⋅ μ ^^ i)"
show "(s ⋅ μ ^^ i, t ⋅ μ ^^ i) ∈ ?QR (σ ∘⇩s μ ^^ i)"
unfolding prop_rstep_qrstep[symmetric] prop_rstep_r_p_s_def Let_def
proof (rule, rule, intro conjI ballI impI)
fix u
assume "u ∈ set (args (s ⋅ μ ^^ i |_ p))"
then obtain v where v: "v ∈ set (args (s |_ p))" and u: "u = v ⋅ μ ^^ i" unfolding subt_at_subst[OF p] sp
by auto
show "u ∈ NF_terms Q" unfolding u using NF[OF v] .
next
show "p ∈ poss (s ⋅ μ ^^ i)" by (rule p')
next
show "r ∈ R" by (rule r)
next
have "fst r ⋅ σ ∘⇩s μ ^^ i = s |_ p ⋅ μ ^^ i" using s[symmetric] by simp
also have "... = s ⋅ μ ^^ i |_ p" unfolding subt_at_subst[OF p] ..
finally show "s ⋅ μ ^^ i |_ p = fst r ⋅ σ ∘⇩s μ ^^ i" by simp
next
show "t ⋅ μ ^^ i = ?C⟨snd r ⋅ σ ∘⇩s μ ^^ i⟩"
unfolding t subst_apply_term_ctxt_apply_distrib ctxt_of_pos_term_subst[OF p] ctxt_eq by simp
next
fix t
assume nfs and t: "t ∈ (σ ∘⇩s μ ^^ i) ` vars_rule r"
then obtain x where t: "t = (σ ∘⇩s μ ^^ i) x" and x: "x ∈ vars_rule r" by auto
from nfs[OF ‹nfs› x, of i]
show "t ∈ NF_terms Q" unfolding t subst_compose_def .
qed
qed
next
assume ?r
then have step: "⋀ i. (s ⋅ μ ^^ i, t ⋅ μ ^^ i) ∈ prop_rstep_r_p_s nfs (λ t. t ∈ NF_terms Q) R r p (σ ∘⇩s μ ^^ i)"
unfolding prop_rstep_qrstep ..
note step = step[unfolded prop_rstep_r_p_s_def Let_def]
from step[of 0]
have p: "p ∈ poss s" and r: "r ∈ R" and s: "s |_ p = fst r ⋅ σ" and t: "t = ?c⟨snd r ⋅ σ⟩" by auto
then have rs: "fst r ⋅ σ = s |_ p" by simp
then obtain us where sp: "s |_ p = Fun f us" unfolding l by (cases "s |_ p", auto)
show ?l
unfolding prop_rstep_r_p_s_def Let_def
proof (rule, rule, intro conjI ballI impI allI)
fix u i
assume u: "u ∈ set (args (s |_ p))"
from step[of i]
have "⋀ v. v ∈ set (args (s ⋅ μ ^^ i |_ p)) ⟹ v ∈ NF_terms Q" by auto
with u show "u ⋅ μ ^^ i ∈ NF_terms Q" unfolding subt_at_subst[OF p] sp by auto
next
fix t i
assume "t ∈ σ ` vars_rule r" nfs
then obtain x where t: "t = σ x" and x: "x ∈ vars_rule r" by auto
then have "t ⋅ μ ^^ i ∈ (σ ∘⇩s μ ^^ i) ` vars_rule r" unfolding subst_compose_def by auto
with step[of i] ‹nfs›
show "t ⋅ μ ^^ i ∈ NF_terms Q" by auto
qed (insert p r s t, auto)
qed
qed
definition
check_rstep' ::
"('f::showl, 'v::showl) rules ⇒ pos ⇒ ('f, 'v) rule ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒
showsl check"
where
"check_rstep' = check_prop_rstep' False (λ _. succeed)"
lemma check_rstep' [simp]:
"isOK (check_rstep' R p r s t) = (∃ σ. (s, t) ∈ rstep_r_p_s (set R) r p σ)"
unfolding check_rstep'_def by (simp add: prop_rstep_rstep)
definition
check_qrstep ::
"(('f::showl, 'v::showl) term ⇒ bool) ⇒ bool ⇒ ('f, 'v) rules ⇒ pos ⇒ ('f, 'v) rule ⇒
('f, 'v) term ⇒ ('f, 'v) term ⇒ showsl check"
where
"check_qrstep nf nfs =
check_prop_rstep nfs (λ t. check (nf t) (showsl t ∘ showsl (STR '' is not in Q-normal form'')))"
lemma check_qrstep_sound:
assumes nf: "⋀t. nf t ⟷ t ∈ NF_terms (set Q)"
and ok: "isOK (check_qrstep nf nfs R p r s t)"
shows "∃ σ r. (s, t) ∈ qrstep_r_p_s nfs (set Q) (set R) r p σ"
using check_prop_rstep_sound[OF ok[unfolded check_qrstep_def]]
unfolding isOK_check prop_rstep_qrstep[symmetric] using nf by auto
lemma check_qrstep_complete:
assumes nf: "⋀t. nf t ⟷ t ∈ NF_terms (set Q)"
and ok: "∃ σ. (s, t) ∈ qrstep_r_p_s nfs (set Q) (set R) r p σ"
shows "isOK (check_qrstep nf nfs R p r s t)"
unfolding check_qrstep_def nf
by (rule check_prop_rstep_complete, insert ok[unfolded prop_rstep_qrstep[symmetric]], auto)
lemma check_qrstep_qrstep:
assumes nf: "⋀t. nf t ⟷ t ∈ NF_terms (set Q)"
and ok: "isOK (check_qrstep nf nfs R p r s t)"
shows "(s, t) ∈ qrstep nfs (set Q) (set R)"
unfolding qrstep_qrstep_r_p_s_conv
using check_qrstep_sound[OF nf ok] by auto
definition
check_no_defined_root :: "((_ × nat) ⇒ bool) ⇒ (_,_) term ⇒ showsl check"
where
"check_no_defined_root isdef t =
check (¬ isdef (the (root t))) (
showsl (STR ''the root of '') ∘ showsl t ∘ showsl (STR '' is defined''))"
lemma check_no_defined_root_sound[simp]:
"isOK (check_no_defined_root isdef t) ⟷ ¬ isdef (the (root t))"
by (cases t) (auto simp: check_no_defined_root_def)
definition
"check_rqrstep nf nfs R rule s t ≡ check_qrstep nf nfs R [] rule s t"
lemma check_rqrstep_sound':
assumes nf: "⋀t. nf t ⟷ t ∈ NF_terms (set Q)"
and ok: "isOK (check_rqrstep nf nfs R r s t)"
shows "∃σ r. (s, t) ∈ qrstep_r_p_s nfs (set Q) (set R) r [] σ"
using check_qrstep_sound[OF assms[unfolded check_rqrstep_def]] .
lemma check_rqrstep_sound:
assumes nf: "⋀t. nf t ⟷ t ∈ NF_terms (set Q)"
and ok: "isOK (check_rqrstep nf nfs R r s t)"
shows "(s, t) ∈ rqrstep nfs (set Q) (set R)"
using check_qrstep_sound[OF assms[unfolded check_rqrstep_def]]
unfolding rqrstep_def qrstep_r_p_s_def by auto
type_synonym ('f, 'v) prseq = "(pos × ('f, 'v) rule × bool × ('f, 'v) term) list"
type_synonym ('f, 'v) rseq = "(pos × ('f, 'v) rule × ('f, 'v) term) list"
fun
check_qsteps ::
"(('f::showl, 'v::showl) term ⇒ bool) ⇒ bool ⇒
('f, 'v) rules ⇒ ('f, 'v) rules ⇒
('f, 'v) prseq ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ showsl check"
where
"check_qsteps nf nfs P R [] s u = check (s = u) (
showsl (STR ''the last term of the rewrite sequence⏎'') ∘ showsl s ∘
showsl (STR ''⏎does not correspond to the goal term⏎'') ∘ showsl u ∘ showsl_nl)"
| "check_qsteps nf nfs P R ((_, r, True, t) # prts) s u = do {
check_rqrstep nf nfs P r s t;
check_qsteps nf nfs P R prts t u
}"
| "check_qsteps nf nfs P R ((p, r, False, t) # prts) s u = do {
check_qrstep nf nfs R p r s t;
check_qsteps nf nfs P R prts t u
}"
lemma check_qsteps_sound:
assumes nf: "⋀t. nf t ⟷ t ∈ NF_terms (set Q)"
and ok: "isOK (check_qsteps nf nfs P R rseq s t)"
shows "(s, t) ∈ (rqrstep nfs (set Q) (set P) ∪ qrstep nfs (set Q) (set R))^^(length rseq)"
proof -
obtain PR where PR: "PR = rqrstep nfs (set Q) (set P) ∪ qrstep nfs (set Q) (set R)" by auto
from ok show ?thesis unfolding PR[symmetric]
proof (induct rseq arbitrary: s)
case Nil then show ?case by simp
next
case (Cons prt rseq)
obtain p r or u where prt: "prt = (p, r, or, u)" by (cases prt, blast)
from Cons[unfolded prt]
have IH: "(u, t) ∈ PR ^^ (length rseq)" by (cases or, induct rseq) auto
have "(s, u) ∈ PR"
proof (cases or)
case True
with Cons[unfolded prt]
have "isOK (check_rqrstep nf nfs P r s u)" by simp
from check_rqrstep_sound[OF nf this]
have "(s, u) ∈ rqrstep nfs (set Q) (set P)" .
then show ?thesis unfolding PR ..
next
case False
with Cons[unfolded prt]
have "isOK (check_qrstep nf nfs R p r s u)" by simp
from check_qrstep_qrstep[OF nf this]
have "(s, u) ∈ qrstep nfs (set Q) (set R)" .
then show ?thesis unfolding PR ..
qed
with IH show ?case unfolding prt o_def using relpow_Suc_I2[of s u PR] by simp
qed
qed
definition
"check_qrsteps nf nfs R prts s u ≡
check_qsteps nf nfs [] R (map (λ(p, r, t). (p, r, False, t)) prts) s u"
lemma check_qrsteps_sound:
assumes nf: "⋀t. nf t ⟷ t ∈ NF_terms (set Q)"
and ok: "isOK (check_qrsteps nf nfs R rseq s t)"
shows "(s, t) ∈ (qrstep nfs (set Q) (set R))^^(length rseq)"
proof -
have empty: "rqrstep nfs (set Q) {} ∪ qrstep nfs (set Q) (set R) = qrstep nfs (set Q) (set R)"
unfolding rqrstep_def qrstep_r_p_s_def by auto
from check_qsteps_sound[OF assms[unfolded check_qrsteps_def]]
show ?thesis by (auto simp: Let_def empty)
qed
definition "check_rsteps ≡ check_qrsteps (λ _. True) False"
lemma check_rsteps_sound:
assumes ok: "isOK (check_rsteps R rseq s t)"
shows "(s, t) ∈ (rstep (set R))^^(length rseq)"
unfolding qrstep_rstep_conv[symmetric]
using check_qrsteps_sound[OF _ ok[unfolded check_rsteps_def], of Nil]
by auto
lemma check_rsteps_sound_star:
assumes ok: "isOK (check_rsteps R rseq s t)"
shows "(s, t) ∈ (rstep (set R))^*"
using relpow_imp_rtrancl[OF check_rsteps_sound[OF ok]] .
definition rseq_last :: "('f,'v)term ⇒ ('f,'v) rseq ⇒ ('f,'v)term"
where "rseq_last s steps ≡ last (s # map (λ (_,_,s). s) steps)"
definition "check_rsteps_last ≡ λ R s steps. check_rsteps R steps s (rseq_last s steps)"
lemma check_rsteps_last_sound_length:
assumes ok: "isOK (check_rsteps_last R s rseq)"
shows "(s, rseq_last s rseq) ∈ (rstep (set R))^^ (length rseq)"
by (rule check_rsteps_sound[OF ok[unfolded check_rsteps_last_def]])
lemma check_rsteps_last_sound:
assumes ok: "isOK (check_rsteps_last R s rseq)"
shows "(s, rseq_last s rseq) ∈ (rstep (set R))^*"
by (rule check_rsteps_sound_star[OF ok[unfolded check_rsteps_last_def]])
fun check_rsteps' ::
"('f :: showl, 'v :: showl) rules ⇒ ('f, 'v) rseq ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ showsl check"
where
"check_rsteps' R [] s u = check (s = u) (
showsl (STR ''the last term of the rewrite sequence⏎'') ∘ showsl s ∘
showsl (STR ''⏎does not correspond to the goal term⏎'') ∘ showsl u ∘ showsl_nl)"
| "check_rsteps' R ((p, lr, t) # rs) s u = do {
check_rstep' R p lr s t;
check_rsteps' R rs t u
}"
subsection ‹Efficient Normal Form Checking›
definition NF_subst_impl :: "(('f,'v)term ⇒ bool) ⇒ bool ⇒ ('f,'v)rule ⇒ ('f,'v) subst ⇒ bool"
where "NF_subst_impl nf nfs r σ ≡ if nfs then (∀ x ∈ set (vars_rule_list r). nf (σ x)) else True"
lemma NF_subst_impl[simp]: "NF_subst_impl (λ t. t ∈ NF_terms Q) nfs r σ = NF_subst nfs r σ Q"
unfolding NF_subst_impl_def NF_subst_def by auto
definition NF_vars_subset :: "('f,'v)terms ⇒ ('f,'v)terms ⇒ bool"
where "NF_vars_subset Q Q' ≡ ∀ q ∈ Q. ∃ q' ∈ Q'. matches q q'"
lemma NF_vars_subsetI[intro]: assumes "⋀ q. q ∈ Q ⟹ ∃ q' ∈ Q'. matches q q'"
shows "NF_vars_subset Q Q'" using assms unfolding NF_vars_subset_def by auto
lemma NF_vars_subset[simp]: assumes "NF_vars_subset Q Q'"
shows "NF_terms Q' ⊆ NF_terms Q"
proof
fix t
assume Q: "t ∈ NF_terms Q'"
show "t ∈ NF_terms Q"
proof
fix C l σ
assume t: "t = C ⟨ l ⋅ σ ⟩" and l: "l ∈ Q"
from assms[unfolded NF_vars_subset_def matches_iff] l obtain l' μ where l: "l' ∈ Q'"
and mu: "l = l' ⋅ μ" by auto
have t: "t = C ⟨ l' ⋅ (μ ∘⇩s σ) ⟩" unfolding t mu by simp
then obtain δ where "t = C ⟨ l' ⋅ δ ⟩" by blast
with l Q show False by auto
qed
qed
definition check_NF_vars_subset :: "('f,'v)term list ⇒ ('f,'v)term list ⇒ ('f,'v)term check"
where "check_NF_vars_subset Q Q' ≡ check_allm (λ q. check (∃ q' ∈ set Q'. matches q q') q) Q"
lemma check_NF_vars_subset[simp]: "isOK(check_NF_vars_subset Q Q') = NF_vars_subset (set Q) (set Q')"
unfolding check_NF_vars_subset_def NF_vars_subset_def by auto
definition check_NF_terms_subset :: "(('f,'v)term ⇒ bool) ⇒ ('f,'v)term list ⇒ ('f,'v)term check"
where "check_NF_terms_subset is_Q_nf ≡ (λ Q'. check_all (λ q. ¬ is_Q_nf q) Q')"
lemma check_NF_terms_subset[simp]: "isOK(check_NF_terms_subset (λ t. t ∈ NF_trs R) Q') = (NF_trs R ⊆ NF_terms (set Q'))"
unfolding check_NF_terms_subset_def
using NF_terms_subset_criterion[of "set Q'" "lhss R", unfolded NF_terms_lhss[of R]] by auto
definition check_NF_trs_subset :: "('f :: compare_order,'v)rules ⇒ ('f,'v)term list ⇒ ('f,'v)term check"
where "check_NF_trs_subset R ≡ check_NF_terms_subset (is_NF_trs R)"
lemma check_NF_trs_subset[simp]: "isOK(check_NF_trs_subset R Q) = (NF_trs (set R) ⊆ NF_terms (set Q))"
unfolding check_NF_trs_subset_def is_NF_trs by simp
definition is_NF_subset :: "(('f,'v)term ⇒ bool) ⇒ ('f,'v)term list ⇒ bool"
where "is_NF_subset is_Q_nf Q' ≡ ∀ q ∈ set Q'. ¬ is_Q_nf q"
lemma is_NF_subset[simp]: "is_NF_subset (λ t. t ∈ NF_terms Q) Q' = (NF_terms Q ⊆ NF_terms (set Q'))"
unfolding NF_terms_subset_criterion[symmetric] is_NF_subset_def by auto
definition is_NF_trs_subset :: "(('f,'v)term ⇒ bool) ⇒ ('f,'v)rules ⇒ bool"
where "is_NF_trs_subset is_Q_nf R ≡ is_NF_subset is_Q_nf (map fst R)"
lemma is_NF_trs_subset[simp]: "is_NF_trs_subset (λ t. t ∈ NF_terms Q) R = (NF_terms Q ⊆ NF_trs (set R))"
unfolding is_NF_trs_subset_def is_NF_subset using NF_terms_lhss[of "set R"] by auto
definition check_NF_terms_eq :: "('f :: compare_order,'v)term list ⇒ ('f,'v)term list ⇒ ('f,'v)term check"
where "check_NF_terms_eq Q Q' ≡ do {
check_NF_terms_subset (is_NF_terms Q) Q';
check_NF_terms_subset (is_NF_terms Q') Q
}"
lemma check_NF_terms_eq[simp]: "isOK(check_NF_terms_eq Q Q') = (NF_terms (set Q) = NF_terms (set Q'))" unfolding check_NF_terms_eq_def by auto
definition applicable_rule_impl :: "(('f,'v)term ⇒ bool) ⇒ ('f,'v)rule ⇒ bool"
where "applicable_rule_impl isNF ≡ λ (l,r). Ball (set (args l)) isNF"
lemma applicable_rule_impl[simp]: assumes isNF: "⋀ s. isNF s = (s ∈ NF_terms Q)"
shows "applicable_rule_impl isNF lr = applicable_rule Q lr"
unfolding applicable_rule_def NF_terms_args_conv[symmetric]
unfolding applicable_rule_impl_def isNF[symmetric] by (cases lr, auto)
definition check_non_applicable_rules :: "(('f,'v)term ⇒ bool) ⇒ ('f,'v)rule list ⇒ ('f,'v)rule check"
where "check_non_applicable_rules isNF r ≡ check_all (λ lr. ¬ applicable_rule_impl isNF lr) r"
lemma check_non_applicable_rules: assumes isNF: "⋀ s. isNF s = (s ∈ NF_terms Q)"
and ok: "isOK(check_non_applicable_rules isNF r)"
shows "qrstep nfs Q (R - set r) = qrstep nfs Q R" (is "?r = ?l")
proof
show "?r ⊆ ?l" by (rule qrstep_mono, auto)
have "?l = qrstep nfs Q (applicable_rules Q R)" unfolding qrstep_applicable_rules ..
also have "... ⊆ ?r"
proof (rule qrstep_mono[OF _ subset_refl])
show "applicable_rules Q R ⊆ R - set r" (is "?l ⊆ ?r")
proof
fix l r
assume "(l,r) ∈ ?l"
from this[unfolded applicable_rules_def] have lr: "(l,r) ∈ R"
and app: "applicable_rule Q (l,r)" by auto
from lr app ok[unfolded check_non_applicable_rules_def, unfolded applicable_rule_impl[OF isNF]]
show "(l,r) ∈ ?r" by auto
qed
qed
finally show "?l ⊆ ?r" .
qed
definition
"check_wwf_qtrs nf R ≡ (
check_allm (λr. if applicable_rule_impl nf r
then (do {
check (is_Fun (fst r)) (showsl (STR ''variable left-hand side in''));
check_subseteq (vars_term_list (snd r)) (vars_term_list (fst r))
<+? (λx. showsl (STR ''free variable '') ∘ showsl x
∘ showsl (STR '' in right-hand side of''))
} <+? (λs. s ∘ showsl (STR '' rule '') ∘ showsl_rule r ∘ showsl_nl)) else succeed) R
<+? (λe. showsl (STR ''the Q-TRS is not weakly well-formed⏎'') ∘ e))"
lemma check_wwf_qtrs_sound[simp]:
shows "isOK (check_wwf_qtrs (λ t. t ∈ NF_terms Q) R) = wwf_qtrs Q (set R)"
unfolding check_wwf_qtrs_def wwf_qtrs_def applicable_rule_impl[OF refl]
split_def by auto
definition
wwf_qtrs_impl :: "(('f, 'v) term ⇒ bool) ⇒ ('f, 'v) rules ⇒ bool"
where
"wwf_qtrs_impl nf R ⟷ (∀ r ∈ set R. wf_rule r ∨ ¬ applicable_rule_impl nf r)"
lemma wwf_qtrs_impl[simp]:
"wwf_qtrs_impl (λ t. t ∈ NF_terms Q) R = wwf_qtrs Q (set R)"
unfolding wwf_qtrs_impl_def
unfolding wwf_qtrs_wwf_rules
unfolding applicable_rule_impl[OF refl]
unfolding wwf_rule_def wf_rule_def by force
context
fixes nfs :: bool
and nfq :: "(('f,'v)term ⇒ bool)"
and R :: "('f,'v)rules"
begin
fun qrewrite :: "('f, 'v) term ⇒ ('f, 'v) term list"
where
"qrewrite s = remdups [ r ⋅ σ . Ball (set (args s)) nfq, (l,r) ← R, σ ← option_to_list (match s l), case l of Var x ⇒ nfs ⟶ nfq (σ x) | _ ⇒ True]
@ (case s of Var _ ⇒ [] | Fun f ss ⇒ [ Fun f (ss [i := ti]) . i ← [0 ..< length ss], ti ← qrewrite (ss ! i)])"
declare qrewrite.simps[simp del]
lemma qrewrite: assumes varcond: "⋀ l r. (l,r) ∈ set R ⟹ vars_term r ⊆ vars_term l"
and nfq: "⋀ t. nfq t = (t ∈ NF_terms Q)"
shows "set (qrewrite s) = { t. (s,t) ∈ qrstep nfs Q (set R)}"
proof -
define vartest where "vartest l σ = (case l of Var x ⇒ nfs ⟶ nfq (σ x) | _ ⇒ True)"
for l :: "('f,'v)term" and σ :: "('f,'v)subst"
{
fix t
assume "(s,t) ∈ qrstep nfs Q (set R)"
hence "t ∈ set (qrewrite s)"
proof (standard, goal_cases)
case (1 C σ l r)
from supt_imp_args[OF 1(1)]
have args: "Ball (set (args (l ⋅ σ))) nfq = True" using nfq by auto
from 1(2) have lr: "(l,r) ∈ set R" .
show ?case unfolding 1(3-4)
proof (induct C)
case Hole
from match_complete'[of l σ, OF refl]
obtain τ where match: "match (l ⋅ σ) l = Some τ"
and vars: "(∀x∈vars_term l. σ x = τ x)" by auto
from varcond[OF lr] vars have same: "(∀x∈vars_term r. σ x = τ x)" by auto
hence r: "r ⋅ σ = r ⋅ τ" by (meson term_subst_eq)
from match_sound[OF match] have l: "l ⋅ σ = l ⋅ τ" by auto
{
fix x
assume "l = Var x" nfs
with 1(5) have "nfq (τ x)" using vars unfolding NF_subst_def by (auto simp: vars_rule_def nfq)
}
hence vtest: "vartest l τ" by (cases l, auto simp: vartest_def)
show ?case unfolding intp_actxt.simps
apply (subst qrewrite.simps)
apply (unfold args if_True set_append set_concat vartest_def[symmetric])
apply (rule UnI1)
using match l r lr vtest by auto
next
case (More f bef C aft)
show ?case unfolding intp_actxt.simps
apply (subst qrewrite.simps)
apply (unfold args term.simps set_append set_concat set_map image_comp o_def set_upt)
apply (rule UnI2)
apply (rule UN_I[of "length bef"])
using More by auto
qed
qed
}
moreover
{
fix t
assume "t ∈ set (qrewrite s)"
hence "(s,t) ∈ qrstep nfs Q (set R)"
proof (induct s arbitrary: t rule: qrewrite.induct)
case (1 s t)
show ?case
proof (cases "(∃ss f. s = Fun f ss ∧ (∃i∈{0..<length ss}. t ∈ (λti. Fun f (ss[i := ti])) ` set (qrewrite (ss ! i))))")
case False
with 1(2)[unfolded qrewrite.simps[of s] vartest_def[symmetric]] obtain l r σ where
args: "(∀x∈set (args s). nfq x)" and lr: "(l,r) ∈set R"
and match: "match s l = Some σ" and t: "t = r ⋅ σ"
and vtest: "vartest l σ" by auto
from match_sound[OF match] have s: "s = l ⋅ σ" by auto
from args[unfolded nfq] have args2: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" unfolding s by (simp add: NF_rstep_supt_args_conv)
have "NF_subst nfs (l, r) σ Q"
proof (cases l)
case (Fun f ll)
thus ?thesis using args varcond[OF lr] s by (intro NF_subst_from_NF_args, auto simp: wf_rule_def nfq)
next
case (Var x)
thus ?thesis using vtest[unfolded vartest_def] varcond[OF lr] by (auto simp: NF_subst_def vars_rule_def nfq)
qed
from rqrstepI[OF args2 lr s t this]
show ?thesis by blast
next
case True
then obtain f ss i ti where s: "s = Fun f ss" and i: "i < length ss" and ti: "ti ∈ set (qrewrite (ss ! i))"
and t: "t = Fun f (ss [i := ti])" by auto
from 1(1)[OF s _ ti] i have IH: "(ss ! i, ti) ∈ qrstep nfs Q (set R)" by auto
have "((More f (take i ss) □ (drop (Suc i) ss))⟨ss ! i⟩, (More f (take i ss) □ (drop (Suc i) ss))⟨ti⟩) = (s,t)"
unfolding s t using i
by (simp add: id_take_nth_drop[symmetric] upd_conv_take_nth_drop)
from qrstep.ctxt[OF IH, of "More f (take i ss) Hole (drop (Suc i) ss)", unfolded this]
show ?thesis .
qed
qed
}
ultimately show ?thesis by blast
qed
end
end