theory Argument_Filter
imports
"Check-NT.Term_Order_Impl"
QTRS.Trs_Impl
QTRS.Map_Choice
begin
hide_const (open) Almost_Full.af
datatype af_entry = Collapse nat | AFList "nat list"
datatype 'f filtered = FPair (fpair_f: 'f) nat
derive compare_order filtered
instantiation filtered :: (key)key
begin
instance ..
end
fun filtered_fun :: "'f filtered ⇒ 'f"
where
"filtered_fun (FPair f n) = f"
instantiation filtered :: ("show") "show"
begin
definition "shows_prec (p::nat) (f :: 'a filtered) = shows (filtered_fun f)"
lemma shows_prec_filtered_append [show_law_simps]:
"shows_prec p (f ::'a filtered) (r @ s) = shows_prec p f r @ s"
by (simp add: shows_prec_filtered_def show_law_simps)
definition "shows_list (fs :: 'a filtered list) = showsp_list shows_prec 0 fs"
instance by standard (simp_all add: shows_list_filtered_def show_law_simps)
end
fun apply_af_entry :: "'f ⇒ af_entry ⇒ ('f,'v)term list ⇒ ('f,'v)term" where
"apply_af_entry _ (Collapse i) ts = ts ! i"
| "apply_af_entry f (AFList is) ts = Fun f (map (λ i. ts ! i) is)"
fun wf_af_entry :: "nat ⇒ af_entry ⇒ bool"
where "wf_af_entry n (Collapse i) = (i < n)"
| "wf_af_entry n (AFList is) = Ball (set is) (λ i. i < n)"
definition default_af_entry :: "nat ⇒ af_entry"
where "default_af_entry n ≡ AFList [0..<n]"
lemma wf_default_af_entry[simp]:
"wf_af_entry n (default_af_entry n)"
unfolding default_af_entry_def by auto
typedef 'f afs = "{(pi :: 'f × nat ⇒ af_entry, fs :: ('f × nat) set).
(∀ f n. wf_af_entry n (pi (f,n)) ∧ ((f,n) ∈ fs ∨ pi (f,n) = default_af_entry n))}"
by (rule exI[of _ "(λ (f,n). default_af_entry n, {})"], auto)
setup_lifting type_definition_afs
lift_definition afs :: "'f afs ⇒ 'f × nat ⇒ af_entry" is fst .
lift_definition afs_syms :: "'f afs ⇒ ('f × nat) set" is snd .
lemma afs: "wf_af_entry n (afs pi (f,n))"
by (transfer, auto)
lemma afs_syms: "(f,n) ∉ afs_syms pi ⟹ afs pi (f,n) = default_af_entry n"
by (transfer, force)
fun afs_term :: "'f afs ⇒ ('f,'v)term ⇒ ('f filtered,'v)term" where
"afs_term π (Fun f ts) = (let l = length ts in apply_af_entry (FPair f l) (afs π (f,l)) (map (afs_term π) ts))"
| "afs_term π (Var x) = Var x"
definition af_term :: "'f afs ⇒ ('f,'v)term ⇒ ('f,'v)term" where
"af_term π t = map_funs_term filtered_fun (afs_term π t)"
definition afs_rule :: "'f afs ⇒ ('f,'v)rule ⇒ ('f filtered,'v)rule"
where "afs_rule π lr ≡ (afs_term π (fst lr), afs_term π (snd lr))"
definition af_rule :: "'f afs ⇒ ('f,'v)rule ⇒ ('f,'v)rule" where
"af_rule π ≡ λ t. map_funs_rule filtered_fun (afs_rule π t)"
definition afs_rules :: "'f afs ⇒ ('f,'v)rules ⇒ ('f filtered,'v)rules"
where "afs_rules π R = map (afs_rule π) R"
definition af_rules :: "'f afs ⇒ ('f,'v)rules ⇒ ('f,'v)rules"
where "af_rules π R = map (af_rule π) R"
definition
afs_check ::
"shows ⇒ 'f::show afs ⇒ (('f filtered,'v::show)rule ⇒ shows check) ⇒ ('f,'v)rule ⇒ shows check"
where
"afs_check r π g lr ≡ let pl = afs_term π (fst lr); pr = afs_term π (snd lr) in g (pl,pr) <+? (λs.
''could not orient '' +#+ shows(fst lr) +@+ '' '' +#+ r +@+ '' '' +#+ shows(snd lr) +@+ shows_nl +@+
''pi( '' +#+ shows(fst lr) +@+ '' ) = '' +#+ shows pl +@+ shows_nl +@+
''pi( '' +#+ shows(snd lr) +@+ '' ) = '' +#+ shows pr +@+ shows_nl +@+ s
)"
lemma af_rules[simp]: "set (af_rules π R) = af_rule π ` (set R)" unfolding af_rules_def by auto
context
fixes π :: "'f afs"
begin
abbreviation afs_subst :: "('f,'v)subst ⇒ ('f filtered,'v)subst"
where "afs_subst σ ≡ (λx. afs_term π (σ x))"
definition afs_rel :: "('f filtered,'v)term rel ⇒ ('f,'v)term rel"
where "afs_rel R = {lr | lr. afs_rule π lr ∈ R}"
lemma afs_subst[simp]: "afs_term π (t ⋅ σ) = afs_term π t ⋅ afs_subst σ"
proof -
have "afs_term π (t ⋅ σ) = afs_term π t ⋅ afs_subst (σ)"
proof (induct t)
case (Fun f ss)
let ?l = "length ss"
let ?e = "afs π (f,?l)"
have wf_e: "wf_af_entry ?l ?e" by (rule afs)
show ?case
proof (cases ?e)
case (Collapse i)
with wf_e have "i < ?l" by simp
with Collapse Fun(1)[of "ss ! i"] show ?thesis
by (auto simp: Let_def)
next
case (AFList "is")
with wf_e have wf: "∀ i ∈ set is. i < ?l" by auto
with AFList Fun(1) show ?thesis
by auto
qed
qed simp
thus ?thesis by simp
qed
lemma afs_rsteps:
"(s,t) ∈ (rstep R)^* ⟹ (afs_term π s, afs_term π t) ∈ (rstep (afs_rule π ` R))^*"
proof (induct rule: rtrancl_induct)
case (step t u)
let ?a = "afs_term π"
let ?R = "afs_rule π ` R"
let ?RR = "(rstep ?R)^*"
from rstepE[OF step(2)] obtain C l r σ where t: "t = C ⟨ l ⋅ σ ⟩" and u: "u = C ⟨ r ⋅ σ ⟩" and lr: "(l,r) ∈ R" .
def ll ≡ "l ⋅ σ" def rr ≡ "r ⋅ σ"
note ctxt = all_ctxt_closedD[OF all_ctxt_closed_rsteps[of _ ?R], of _ _ UNIV]
have "(?a t, ?a u) ∈ ?RR" unfolding t u ll_def[symmetric] rr_def[symmetric]
proof (induct C)
case Hole
from lr have "(?a l, ?a r) ∈ ?R" by (force simp: afs_rule_def)
from rstep.subst[OF rstep.rule[OF this], of "afs_subst σ"]
show ?case unfolding ll_def rr_def by simp
next
case (More f bef C aft)
let ?n = "Suc (length bef + length aft)"
let ?pi = "afs π (f, ?n)"
show ?case
proof (cases ?pi)
case (Collapse i)
thus ?thesis
by (cases "i = length bef", insert More, auto simp: nth_append)
next
case (AFList ls)
show ?thesis
by (simp add: AFList, rule ctxt, auto, case_tac "ls ! i = length bef", insert More, auto simp: nth_append)
qed
qed
with step(3) show ?case by simp
qed simp
lemma af_rsteps: assumes steps: "(s,t) ∈ (rstep R)^*"
shows "(af_term π s, af_term π t) ∈ (rstep (af_rule π ` R))^*"
proof -
let ?f = "filtered_fun"
have id: "map_funs_trs ?f (afs_rule π ` R) = af_rule π ` R"
by (force simp: af_rule_def afs_rule_def af_term_def map_funs_trs.simps)
from rsteps_imp_map_rsteps[OF afs_rsteps[OF steps], of ?f, folded af_term_def]
show ?thesis unfolding id .
qed
lemma argument_filter_nj: "¬ (∃ u. (af_term π s,u) ∈ (rstep (af_rule π ` Rs))^* ∧ (af_term π t,u) ∈ (rstep (af_rule π ` Rt))^*) ⟹
¬ (∃ u. (s,u) ∈ (rstep Rs)^* ∧ (t,u) ∈ (rstep Rt)^*)"
using af_rsteps by auto
lemma afs_subst_closed:
assumes "subst.closed R"
shows "subst.closed (afs_rel R)"
unfolding subst.closed_def
proof (rule subsetI, simp only: split_paired_all)
fix ss ts
assume "(ss,ts) ∈ subst.closure (afs_rel R)"
thus "(ss,ts) ∈ afs_rel R"
proof (induct)
case (subst s t σ)
from this have "(afs_term π s, afs_term π t) ∈ R" unfolding afs_rel_def afs_rule_def by simp
with assms have "(afs_term π s ⋅ afs_subst σ, afs_term π t ⋅ afs_subst σ) ∈ R" unfolding subst.closed_def
using subst by auto
thus ?case unfolding afs_rel_def afs_rule_def by auto
qed
qed
lemma afs_SN:
assumes "SN R"
shows "SN (afs_rel R)"
proof -
have id: "afs_rel R = inv_image R (afs_term π)"
unfolding afs_rel_def afs_rule_def inv_image_def by auto
show ?thesis unfolding id by (rule SN_inv_image[OF assms])
qed
lemma afs_compat:
assumes "NS O S ⊆ S"
shows "afs_rel NS O afs_rel S ⊆ afs_rel S"
using assms
by (unfold afs_rel_def afs_rule_def, clarify, auto)
lemma afs_compat2:
assumes "S O NS ⊆ S"
shows "afs_rel S O afs_rel NS ⊆ afs_rel S"
using assms
by (unfold afs_rel_def afs_rule_def, clarify, auto)
lemma afs_refl:
assumes "refl NS"
shows "refl (afs_rel NS)"
using assms unfolding refl_on_def
by (unfold afs_rel_def afs_rule_def, auto)
lemma afs_trans:
assumes "trans r"
shows "trans (afs_rel r)"
unfolding trans_def
proof (unfold afs_rel_def afs_rule_def, clarify, unfold fst_conv snd_conv)
fix a b c
assume gt: "(afs_term π a, afs_term π b) ∈ r" "(afs_term π b, afs_term π c) ∈ r"
show "∃ lr. (a,c) = lr ∧ (afs_term π (fst lr), afs_term π (snd lr)) ∈ r"
by (intro exI conjI, rule refl, insert assms[unfolded trans_def, THEN spec, THEN spec, THEN spec, THEN mp[OF _ gt(1)], THEN mp[OF _ gt(2)]], simp)
qed
lemma afs_NS_mono:
assumes acc: "all_ctxt_closed UNIV R"
shows "ctxt.closed (afs_rel R)"
proof (rule one_imp_ctxt_closed)
fix f bef s t aft
assume st: "(s,t) ∈ afs_rel R"
let ?ps = "afs_term π s"
let ?pt = "afs_term π t"
let ?bsa = "bef @ s # aft"
let ?bta = "bef @ t # aft"
from st have pst: "(?ps,?pt) ∈ R" unfolding afs_rel_def afs_rule_def by auto
let ?l = "Suc (length bef + length aft)"
let ?ls = "length (bef @ s # aft)"
let ?lt = "length (bef @ t # aft)"
let ?af = "afs π (f,?l)"
have wf_af: "wf_af_entry ?l ?af" by (rule afs)
let ?msa = "map (afs_term π) ?bsa"
let ?mta = "map (afs_term π) ?bta"
let ?pfs = "apply_af_entry (FPair f ?l) ?af ?msa"
let ?pft = "apply_af_entry (FPair f ?l) ?af ?mta"
have all2: "∀ i < ?l. (?msa ! i, ?mta ! i) ∈ R"
proof (intro allI impI)
fix i
assume "i < ?l"
hence i_s: "i < ?ls" and i_t: "i < ?lt" by simp_all
{
assume bef: "i < length bef"
with all_ctxt_closed_reflE[OF acc] have "(?msa ! i, ?mta ! i) ∈ R"
by (simp only: nth_map[OF i_s], simp add: nth_append)
}
moreover
{
assume "i = length bef"
with pst have "(?msa ! i, ?mta ! i) ∈ R" unfolding refl_on_def
by (simp only: nth_map[OF i_s], simp add: nth_append)
}
moreover
{
assume i: "i > length bef"
from this obtain k where k1: "i - length bef = Suc k" by (cases "i - length bef", arith+)
with i_s have k2: "k < length aft" by auto
from i all_ctxt_closed_reflE[OF acc] have "(?msa ! i, ?mta ! i) ∈ R"
by (simp only: nth_map[OF i_s] nth_map[OF i_t], simp add: nth_append k1)
}
moreover
{
have "i < length bef ∨ i = length bef ∨ i > length bef" by auto
}
ultimately
show "(?msa ! i, ?mta ! i) ∈ R" by blast
qed
have "(?pfs,?pft) ∈ R"
proof (cases ?af)
case (Collapse i)
with wf_af have "i < ?l" by simp
with all2 Collapse show ?thesis by auto
next
case (AFList ids)
with wf_af have ids: "∀ i ∈ set ids. i < ?l" by simp
show ?thesis
proof (simp only: AFList apply_af_entry.simps)
let ?msi = "map (op ! (map (afs_term π) ?bsa)) ids"
let ?mti = "map (op ! (map (afs_term π) ?bta)) ids"
from ids all2 have args: "∀ i < length ids. (?msi ! i, ?mti ! i) ∈ R" by auto
show "(Fun (FPair f ?l) ?msi, Fun (FPair f ?l) ?mti) ∈ R"
by (rule all_ctxt_closedD[OF acc], insert args, auto)
qed
qed
thus "(Fun f ?bsa, Fun f ?bta) ∈ afs_rel R" unfolding afs_rel_def afs_rule_def by simp
qed
end
locale afs_redtriple = redtriple_order S NS NST
for π :: "('f)afs" and S NS NST :: "('f filtered,'v)trs"
locale afs_redtriple_impl = afs_redtriple π S NS NST + redtriple_impl S NS NST cS cNS cNST
for π :: "('f::show)afs" and S NS NST :: "('f filtered,'v::show)trs" and cS cNS cNST
+ assumes fin: "finite (afs_syms π)"
locale mono_afs_redtriple_impl = afs_redtriple_impl π S NS NST cS cNS cNST + mono_redtriple_impl S NS NST cS cNS cNST cm
for π :: "('f::show)afs" and S NS NST :: "('f filtered,'v::show)trs" and cS cNS cNST cm
sublocale afs_redtriple ⊆ redtriple "afs_rel π S" "afs_rel π NS" "afs_rel π NST"
proof -
let ?S = "afs_rel π S"
let ?NS = "afs_rel π NS"
let ?NST = "afs_rel π NST"
show "redtriple ?S ?NS ?NST"
proof
show "SN ?S" by (rule afs_SN, rule SN)
show "?NS O ?S ⊆ ?S" by (rule afs_compat, rule compat_NS_S)
show "?S O ?NS ⊆ ?S" by (rule afs_compat2, rule compat_S_NS)
show "subst.closed ?S" by (rule afs_subst_closed, rule subst_S)
show "subst.closed ?NS" by (rule afs_subst_closed, rule subst_NS)
show "subst.closed ?NST" by (rule afs_subst_closed, rule subst_NST)
show "ctxt.closed ?NS" by (rule afs_NS_mono, rule all_ctxt_closed)
show "?NST O ?S ⊆ ?S" by (rule afs_compat[OF compat_NST])
show "?S ⊆ ?NS" unfolding afs_rel_def using S_imp_NS by blast
qed
qed
fun mono_af_entry :: "nat ⇒ af_entry ⇒ bool" where
"mono_af_entry n (Collapse i) = (n ≤ 1)"
| "mono_af_entry n (AFList ids) = Ball (set [0 ..< n]) (λ i. i ∈ set ids)"
definition mono_afs :: "'f afs ⇒ bool" where
"mono_afs π = (∀ (f,n) ∈ afs_syms π. mono_af_entry n (afs π (f,n)))"
lemma mono_afs: assumes "mono_afs π"
shows "mono_af_entry n (afs π (f,n))"
proof (cases "(f,n) ∈ afs_syms π")
case True
thus ?thesis using assms unfolding mono_afs_def by auto
next
case False
from afs_syms[OF this] show ?thesis unfolding default_af_entry_def by simp
qed
context afs_redtriple
begin
lemma ctxt_closed:
assumes mono_pi: "mono_afs π"
and monoS: "ctxt.closed S"
shows "ctxt.closed (afs_rel π S)"
proof -
let ?S = "afs_rel π S"
let ?pi = "afs_term π"
{
fix f bef s t aft
assume st: "(?pi s, ?pi t) ∈ S"
let ?bsa = "bef @ s # aft"
let ?bta = "bef @ t # aft"
let ?fs = "Fun f ?bsa"
let ?ft = "Fun f ?bta"
let ?l = "Suc (length bef + length aft)"
let ?lba = "length bef + length aft"
let ?e = "afs π (f,?l)"
from mono_afs[OF mono_pi] have mono_e: "mono_af_entry ?l ?e" .
have wf_e: "wf_af_entry ?l ?e" by (rule afs)
have "(?pi ?fs, ?pi ?ft) ∈ S"
proof (cases ?e)
case (Collapse i)
with mono_e wf_e show ?thesis using st by auto
next
case (AFList ids)
let ?ids = "{n | n. n < ?l}"
let ?f = "FPair f ?l"
obtain l where l: "?l = l" by auto
from AFList wf_e have ids1: "set ids ⊆ ?ids" by auto
from AFList mono_e have ids2: "?ids ⊆ set ids"
by (simp only: l, auto)
from ids1 ids2 have ids: "set ids = ?ids" by auto
let ?eq = "λ i. ?pi (?bsa ! i) = ?pi (?bta ! i)"
let ?gr = "λ i. (?pi (?bsa ! i), ?pi (?bta ! i)) ∈ S"
let ?lb = "length bef"
have geq: "∀ i. ?eq i ∨ ?gr i"
proof
fix i
{
assume "i < ?lb" hence "?eq i" by (simp add: nth_append)
}
moreover
{
assume "i = ?lb"
with st have "?gr i" by (simp add: nth_append)
}
moreover
{
assume i2: "i > ?lb"
then obtain k where k1: "i - length bef = Suc k" by (cases "i - length bef", arith+)
have "?eq i" unfolding nth_append using i2 k1 by auto
}
moreover
{
have "i < ?lb ∨ i = ?lb ∨ i > ?lb" by arith
}
ultimately show "?eq i ∨ ?gr i" by blast
qed
from ids have lb: "?lb ∈ set ids" by auto
from st have "?gr ?lb" by (simp add: nth_append)
with lb have gr: "∃ i ∈ set ids. ?gr i ∧ i = ?lb" by auto
obtain ss ts pi g where g: "g = ?f" and ss: "ss = ?bsa" and ts: "ts = ?bta" and pi: "pi = (?pi :: ('f,'v)term ⇒ ('f filtered,'v)term)" by auto
let ?eq = "λ i. pi (ss ! i) = pi (ts ! i)"
let ?gr = "λ i. (pi (ss ! i), pi (ts ! i)) ∈ S"
let ?ss = "map (op ! (map pi ss))"
let ?ts = "map (op ! (map pi ts))"
let ?both = "λ n. ?ts (take n ids) @ ?ss (drop n ids)"
let ?gss = "Fun g (?ss ids)"
let ?gboth = "λ n. Fun g (?both n)"
from geq ss ts pi have geq: "∀ i. ?eq i ∨ ?gr i" by auto
from gr ss ts pi have "∃ i ∈ set ids. ?gr i ∧ i = ?lb" by auto
from this obtain i where i: "?gr i" and iids: "i ∈ set ids" and idef: "i = ?lb" by auto
have "∀ n. (i ∈ set (take n ids) ⟶ (?gss, ?gboth n) ∈ S) ∧ (i ∉ set (take n ids) ⟶ ?gss = ?gboth n)" (is "∀ n. ?p n")
proof (intro allI)
fix n
show "?p n"
proof (induct n, simp)
case (Suc n)
show ?case
proof (cases "n ≥ length ids")
case True
with Suc show ?thesis by simp
next
case False
hence n: "n < length ids" by auto
let ?bef = "?ts (take n ids)"
let ?aft = "?ss (drop (Suc n) ids)"
let ?ssn = "pi (ss ! (ids ! n))"
let ?tsn = "pi (ts ! (ids ! n))"
from n ids have ids_n: "ids ! n < ?l" by force
have gn: "?both n = ?bef @ ?ssn # ?aft"
by (simp only: Cons_nth_drop_Suc[OF n, symmetric], simp, simp add: nth_map[of "ids ! n" ?bsa pi, simplified, OF ids_n] ss)
have gsn: "?both (Suc n) = ?bef @ ?tsn # ?aft"
by (simp only: take_Suc_conv_app_nth[OF n], simp, simp add: nth_map[of "ids ! n" ?bta pi, simplified, OF ids_n] ts)
{
assume "?ssn ≠ ?tsn ∨ ids ! n = i"
with geq i have "(?ssn, ?tsn) ∈ S" by blast
from ctxt_closed_one[OF monoS this]
have gnsn: "(?gboth n, ?gboth (Suc n)) ∈ S"
by (simp only: gn gsn)
} note noteq_i = this
{
assume "ids ! n ≠ i"
{
assume "ids ! n < ?lb"
hence "?gboth (Suc n) = ?gboth n"
by (simp add: gn gsn, simp add: ss ts)
}
moreover
{
assume i2: "ids ! n > ?lb"
have "?gboth (Suc n) = ?gboth n" unfolding term.simps gn gsn
using i2 ss ts by (simp add: nth_append)
}
moreover
{
from ‹ids ! n ≠ i› have "ids ! n < ?lb ∨ ids ! n > ?lb" by (simp only: idef, arith)
}
ultimately have "?gboth (Suc n) = ?gboth n" by blast
} note eq = this
show ?thesis
proof (cases "i ∈ set (take (Suc n) ids)")
case False
hence i_not: "i ∉ set (take n ids)" and i_not2: "ids ! n ≠ i" using take_Suc_conv_app_nth[OF n] by auto
from i_not Suc have rec: "?gss = ?gboth n" by blast
with False eq[OF i_not2] rec show ?thesis by simp
next
case True note oTrue = this
show ?thesis
proof (cases "i ∈ set (take n ids)")
case False
with True have id: "ids ! n = i" using take_Suc_conv_app_nth[OF n] by auto
from False Suc have rec: "?gss = ?gboth n" by blast
from noteq_i id have "(?gboth n, ?gboth (Suc n)) ∈ S" by blast
with True rec show ?thesis by simp
next
case True
with Suc have rec: "(?gss, ?gboth n) ∈ S" by blast
show ?thesis
proof (cases "ids ! n = i")
case False
from rec eq[OF False] oTrue show ?thesis by simp
next
case True
with noteq_i have "(?gboth n, ?gboth (Suc n)) ∈ S" by blast
from rec this have "(?gss, ?gboth (Suc n)) ∈ S" using trans_S unfolding trans_def by blast
with oTrue show ?thesis by simp
qed
qed
qed
qed
qed
qed
with spec[OF this, of "length ids"] iids have "(Fun g (?ss ids), Fun g (?ts ids)) ∈ S" by auto
with g ss ts pi have "(Fun ?f (map (op ! (map ?pi bef @ ?pi s # map ?pi aft)) ids),
Fun ?f (map (op ! (map ?pi bef @ ?pi t # map ?pi aft)) ids)) ∈ S"
by auto
thus ?thesis using AFList by simp
qed
} note main = this
show "ctxt.closed ?S"
unfolding afs_rel_def afs_rule_def
by (rule one_imp_ctxt_closed, insert main, auto)
qed
end
sublocale afs_redtriple ⊆ redtriple_order "afs_rel π S" "afs_rel π NS" "afs_rel π NST"
proof -
let ?S = "afs_rel π S"
let ?NS = "afs_rel π NS"
let ?NST = "afs_rel π NST"
show "redtriple_order ?S ?NS ?NST"
proof
show "refl ?NS" by (rule afs_refl[OF refl_NS])
show "refl ?NST" by (rule afs_refl[OF refl_NST])
show "trans ?S" by (rule afs_trans[OF trans_S])
show "trans ?NS" by (rule afs_trans[OF trans_NS])
show "trans ?NST" by (rule afs_trans[OF trans_NST])
qed
qed
sublocale afs_redtriple_impl ⊆ redtriple_impl "afs_rel π S" "afs_rel π NS" "afs_rel π NST" "afs_check rS π cS" "afs_check rNS π cNS" "afs_check rNST π cNST"
proof -
let ?S = "afs_rel π S"
let ?NS = "afs_rel π NS"
let ?NST = "afs_rel π NST"
let ?cS = "afs_check rS π cS"
let ?cNS = "afs_check rNS π cNS"
let ?cNST = "afs_check rNST π cNST"
show "redtriple_impl ?S ?NS ?NST ?cS ?cNS ?cNST"
proof
fix lr
assume "isOK (afs_check rS π cS lr)"
thus "lr ∈ ?S" unfolding afs_check_def afs_rel_def
using checkSSound by (auto simp: split_paired_all Let_def afs_rule_def)
next
fix lr
assume "isOK (afs_check rNS π cNS lr)"
thus "lr ∈ ?NS" unfolding afs_check_def afs_rel_def
using checkNSSound by (auto simp: split_paired_all Let_def afs_rule_def)
next
fix lr
assume "isOK (afs_check rNST π cNST lr)"
thus "lr ∈ ?NST" unfolding afs_check_def afs_rel_def
using checkNSTSound by (auto simp: split_paired_all Let_def afs_rule_def)
qed
qed
sublocale mono_afs_redtriple_impl ⊆ mono_redtriple_impl "afs_rel π S" "afs_rel π NS" "afs_rel π NST" "afs_check rS π cS" "afs_check rNS π cNS" "afs_check rNST π cNST" "cm >> check (mono_afs π) mess"
proof
assume "isOK (cm >> check (mono_afs π) mess)"
with checkMonoSound have monoS: "ctxt.closed S" and mono_pi: "mono_afs π" by auto
from ctxt_closed[OF mono_pi monoS] show "ctxt.closed (afs_rel π S)" .
qed
definition permutation_afs :: "'f afs ⇒ bool" where
"permutation_afs π ≡ ∀ (f,n) ∈ afs_syms π.
case afs π (f,n) of
AFList xs ⇒ set xs = {0 ..< n} ∧ distinct xs
| _ ⇒ False"
context
fixes π :: "'f afs"
assumes perm: "permutation_afs π"
begin
lemma perm: "∃xs. afs π (f, n) = AFList xs ∧ set xs = {0..<n} ∧ distinct xs"
proof (cases "(f,n) ∈ afs_syms π")
case True
with perm show ?thesis unfolding permutation_afs_def by (cases "afs π (f,n)", auto)
next
case False
from afs_syms[OF this] show ?thesis unfolding default_af_entry_def by auto
qed
fun af_ctxt :: "('f,'v)ctxt ⇒ ('f,'v)ctxt" where
"af_ctxt Hole = Hole"
| "af_ctxt (More f bef C aft) = (let i = length bef;
n = Suc (i + length aft);
ts = map (af_term π) (bef @ C⟨undefined⟩ # aft) in case afs π (f,n) of
AFList xs ⇒ let i' = SOME i'. i' < n ∧ xs ! i' = i
in More f (map (λ j. ts ! (xs ! j)) [0 ..< i']) (af_ctxt C) (map (λ j. ts ! (xs ! j)) [Suc i' ..< n]))"
lemma af_ctxt[simp]: "af_term π (C ⟨ t ⟩) = (af_ctxt C) ⟨ af_term π t ⟩"
proof (induct C)
case (More f bef C aft)
let ?i = "length bef"
let ?n = "Suc (?i + length aft)"
from perm[of f ?n] obtain xs where pi: "afs π (f,?n) = AFList xs" and xs: "set xs = {0 ..< ?n}" and d: "distinct xs" by auto
from distinct_card[OF d] have len: "length xs = ?n" unfolding xs by simp
let ?p = "λ i'. i' < ?n ∧ xs ! i' = ?i"
def i' ≡ "SOME i'. ?p i'"
have "?i ∈ set xs" unfolding xs by auto
with len have "∃ i'. ?p i'" unfolding set_conv_nth by auto
from someI_ex[OF this] have i': "?p i'" unfolding i'_def by simp
let ?ts = "map (af_term π) (bef @ C⟨undefined⟩ # aft)"
have "(af_ctxt (More f bef C aft)) ⟨ af_term π t ⟩ = (More f (map (λj. ?ts ! (xs ! j)) [0..<i']) (af_ctxt C)
(map (λj. ?ts ! (xs ! j)) [Suc i'..<?n]))⟨af_term π t⟩" (is "?l = _")
unfolding af_ctxt.simps Let_def pi af_entry.simps i'_def by simp
also have "… = Fun f ((map (λj. ?ts ! (xs ! j)) [0..<i']) @ af_term π (C ⟨ t ⟩) # (map (λj. ?ts ! (xs ! j)) [Suc i'..<length xs]))"
(is "_ = Fun f ?r") using More len by simp
finally have id1: "?l = Fun f ?r" .
let ?is = "[0..<i'] @ i' # [Suc i' ..< length xs]"
have "xs = map (λ i. xs ! i) [0..<?n]" unfolding len[symmetric] by (rule nth_equalityI, auto)
also have "[0..<?n] = ?is" using i'
by (metis len upt_append upt_conv_Cons)
finally have id3: "(map (λ i. xs ! i) ?is) = xs" by simp
have "af_term π (More f bef C aft)⟨t⟩ =
Fun f (map (λx. map_funs_term filtered_fun ((map (afs_term π) bef @ afs_term π C⟨t⟩ # map (afs_term π) aft) ! x)) xs)"
(is "?l = _") unfolding af_term_def by (simp add: pi o_def)
also have "… = Fun f (map (λx. ((map (af_term π) bef @ af_term π C⟨t⟩ # map (af_term π) aft) ! x)) xs)"
by (simp add: xs af_term_def[abs_def], auto simp: nth_append, case_tac "x - length bef", auto)
also have "… = Fun f (map (λx. ((map (af_term π) bef @ af_term π C⟨t⟩ # map (af_term π) aft) ! x)) (map (λ i. xs ! i) ?is))"
(is "_ = Fun f ?r'") unfolding id3 ..
finally have id2: "?l = Fun f ?r'" by simp
have id4: "(Fun f ?r' = Fun f ?r) = (?r' = ?r)" by simp
show ?case unfolding id1 id2 id4
proof -
note i' = i'[folded len]
have i: "?i < length xs" unfolding len by simp
show "?r' = ?r"
proof (rule nth_equalityI, simp, intro allI impI)
fix j
assume "j < length ?r'"
from this[unfolded id3] have j: "j < length xs" by simp
with xs have xsj: "xs ! j < length xs" unfolding len[symmetric] by auto
show "?r' ! j = ?r ! j"
proof (cases "j = i'")
case True
show ?thesis using i' unfolding True
by (simp add: nth_append)
next
case False
let ?ts' = "map (af_term π) (bef @ C⟨undefined⟩ # aft)"
from False d j i' have xsji: "xs ! j ≠ ?i"
by (metis nth_eq_iff_index_eq)
have "?r' ! j = ?ts' ! (xs ! j)" unfolding id3 nth_map[OF j]
using xsji xsj unfolding len by (auto simp: nth_append)
also have "… = ?r ! j" using False i' j by (simp add: nth_append)
finally show ?thesis .
qed
qed
qed
qed simp
lemma step_imp_afs_rstep: "(s,t) ∈ rstep R ⟹ (af_term π s, af_term π t) ∈ rstep (af_rule π ` R)"
proof (induct rule: rstep_induct)
case (IH C σ l r)
let ?a = "af_term π"
let ?R = "af_rule π ` R"
def s ≡ "?a (l ⋅ σ)"
def t ≡ "?a (r ⋅ σ)"
from IH have rule: "(?a l, ?a r) ∈ ?R" unfolding af_rule_def af_term_def afs_rule_def by force
have "(?a (l ⋅ σ), ?a (r ⋅ σ)) ∈ rstep ?R"
by (rule rstepI[OF rule, of _ Hole], auto simp: af_term_def)
from rstep.ctxt[OF this, of "af_ctxt C"] show ?case by simp
qed
lemmas steps_imp_afs_rsteps = af_rsteps
lemma step_imp_afs_rel_rstep: assumes st: "(s,t) ∈ relto (rstep R) (rstep S)"
shows "(af_term π s, af_term π t) ∈ relto (rstep (af_rule π ` R)) (rstep (af_rule π ` S))"
proof -
let ?a = "af_term π"
from st obtain u v where su: "(s,u) ∈ (rstep S)^*" and uv: "(u,v) ∈ (rstep R)" and vt: "(v,t) ∈ (rstep S)^*" by auto
from steps_imp_afs_rsteps[OF su] step_imp_afs_rstep[OF uv] steps_imp_afs_rsteps[OF vt]
show ?thesis by blast
qed
lemma af_SN_relto_rstep: assumes SN: "SN (relto (rstep (af_rule π ` R)) (rstep (af_rule π ` S)))" (is "SN ?R'")
shows "SN (relto (rstep R) (rstep S))" (is "SN ?R")
proof
fix f
assume steps: "∀ i. (f i, f (Suc i)) ∈ ?R"
def g ≡ "λ i. (af_term π (f i))"
from step_imp_afs_rel_rstep[OF spec[OF steps]]
have "⋀ i. (g i, g (Suc i)) ∈ ?R'" unfolding g_def by auto
with SN show False unfolding SN_defs by auto
qed
lemma af_SN_rstep: assumes SN: "SN (rstep (af_rule π ` R))"
shows "SN (rstep R)" using af_SN_relto_rstep[of "{}" R] SN by simp
end
type_synonym 'f afs_list = "(('f × nat) × af_entry)list"
abbreviation (input) afs_of' :: "('f :: key) afs_list ⇒ 'f × nat ⇒ af_entry" where
"afs_of' π ≡ fun_of_map_fun (ceta_map_of π) (λ fn. default_af_entry (snd fn))"
lift_definition (code_dt) afs_of :: "('f :: key) afs_list ⇒ 'f afs option"
is "λ π. if (∀ fn_entry ∈ set π. case fn_entry of ((f,n),e) ⇒
wf_af_entry n e) then
Some (afs_of' π, set (map fst π)) else None"
using map_of_SomeD by (fastforce split: option.splits)
lemma afs_of_Some_afs_syms: "afs_of π = Some pair
⟹ afs_syms pair = set (map fst π)"
using afs_of.rep_eq[of π]
by (transfer, auto split: if_splits)
definition afs_to_unused_arity :: "'f afs ⇒ nat" where
"afs_to_unused_arity π ≡ if finite (afs_syms π)
then (SOME x. (∀ f n. n ≥ x ⟶ afs π (f,n) = default_af_entry n))
else 0"
lemma afs_to_unused_arity: assumes fin: "finite (afs_syms π)"
and n: "n ≥ afs_to_unused_arity π"
shows "afs π (f,n) = default_af_entry n"
proof -
from finite_list[OF fin] obtain fs where fs: "afs_syms π = set fs" by blast
let ?P = "λ x. ∀ f n. n ≥ x ⟶ afs π (f,n) = default_af_entry n"
let ?m = "(Suc (max_list (map snd fs)))"
let ?u = "afs_to_unused_arity π"
from fin have u: "?u = (SOME x. ?P x)" unfolding afs_to_unused_arity_def by auto
have "?P ?m"
proof (intro allI impI)
fix f n
assume "?m ≤ n"
hence "(f,n) ∉ set fs" using max_list[of n "map snd fs"] by auto
from afs_syms[OF this[folded fs]] show "afs π (f,n) = default_af_entry n" .
qed
from someI[of ?P, OF this, folded u] n
show ?thesis by auto
qed
lemma default_af_entry_id:
assumes "afs π (f,length ts) = default_af_entry (length ts)"
shows "afs_term π (Fun f ts) = Fun (FPair f (length ts)) (map (afs_term π) ts)"
by (simp add: default_af_entry_def assms Let_def, simp only: list_eq_iff_nth_eq, simp)
definition afs_to_af :: "('f :: key) afs ⇒ 'f af" where
"afs_to_af pi fn ≡ case afs pi fn of
Collapse j ⇒ {j}
| AFList ids ⇒ set ids"
lemma apply_af_entry_const_is_id: "apply_af_entry (FPair f (0 :: nat)) (afs π (f, 0)) [] = Fun (FPair f 0) []"
proof -
let ?e = "afs π (f, 0)"
have "wf_af_entry 0 ?e" by (rule afs)
thus ?thesis by (cases ?e, simp_all)
qed
lemma af_compatible:
fixes pi :: "('f :: key) afs"
assumes refl_NS: "refl NS"
and all_ctxt_closed: "all_ctxt_closed UNIV NS"
shows "af_compatible (afs_to_af pi) (afs_rel pi (NS :: ('f filtered,'v)term rel))" (is "af_compatible ?af ?NS")
unfolding af_compatible_def
proof (intro allI)
fix f :: 'f and bef :: "('f,'v)term list" and s t :: "('f,'v)term" and aft
let ?pi = pi
let ?bsa = "bef @ s # aft"
let ?bta = "bef @ t # aft"
let ?lb = "length bef"
let ?l = "Suc (?lb + length aft)"
let ?s = "Fun f ?bsa"
let ?t = "Fun f ?bta"
show "?lb ∈ ?af (f, ?l) ∨ (?s,?t) ∈ ?NS"
proof (cases "?lb ∈ ?af (f, ?l)")
case False
let ?e = "afs ?pi (f, ?l)"
have wf: "wf_af_entry ?l ?e" by (rule afs)
let ?ls = "length (bef @ s # aft)"
let ?lt = "length (bef @ t # aft)"
let ?msa = "map (afs_term ?pi) ?bsa"
let ?mta = "map (afs_term ?pi) ?bta"
let ?pfs = "apply_af_entry (FPair f ?l) ?e ?msa"
let ?pft = "apply_af_entry (FPair f ?l) ?e ?mta"
have all2: "∀ i < ?l. i ≠ ?lb ⟶ (?msa ! i, ?mta ! i) ∈ NS"
proof (intro allI impI)
fix i
assume "i < ?l" and ib: "i ≠ ?lb"
hence i_s: "i < ?ls" and i_t: "i < ?lt" by simp_all
{
assume bef: "i < length bef"
with refl_NS have "(?msa ! i, ?mta ! i) ∈ NS" unfolding refl_on_def
by (simp only: nth_map[OF i_s], simp add: nth_append)
}
moreover
{
assume i: "i > length bef"
from this obtain k where k1: "i - length bef = Suc k" by (cases "i - length bef", arith+)
with i_s have k2: "k < length aft" by auto
from i refl_NS have "(?msa ! i, ?mta ! i) ∈ NS" unfolding refl_on_def
by (simp only: nth_map[OF i_s] nth_map[OF i_t], simp add: nth_append k1)
}
moreover
have "i < length bef ∨ i = length bef ∨ i > length bef" by auto
ultimately
show "(?msa ! i, ?mta ! i) ∈ NS" using ib by blast
qed
have "(?pfs,?pft) ∈ NS"
proof (cases ?e)
case (Collapse i)
with wf have len: "i < ?l" by simp
from Collapse[simplified] False have "i ≠ ?lb" unfolding afs_to_af_def by auto
with all2 len Collapse show ?thesis by auto
next
case (AFList ids)
with wf have ids: "∀ i ∈ set ids. i < ?l" by simp
show ?thesis
proof (unfold AFList apply_af_entry.simps)
let ?msi = "map (op ! (map (afs_term ?pi) ?bsa)) ids"
let ?mti = "map (op ! (map (afs_term ?pi) ?bta)) ids"
from ids False AFList[simplified] have "∀ i ∈ set ids. i ≠ ?lb" unfolding afs_to_af_def
by auto
with ids all2 have args: "∀ i < length ids. (?msi ! i, ?mti ! i) ∈ NS" by auto
show "(Fun (FPair f ?l) ?msi, Fun (FPair f ?l) ?mti) ∈ NS"
by (rule all_ctxt_closedD[OF all_ctxt_closed], insert args, auto)
qed
qed
thus "?lb ∈ afs_to_af pi (f, ?l) ∨ (Fun f ?bsa, Fun f ?bta) ∈ afs_rel ?pi NS" unfolding afs_rel_def afs_rule_def by (simp add: afs)
qed simp
qed
lemma af_ce_compat:
fixes pi :: "('f :: {show,key}) afs"
and NS :: "('f filtered, 'v :: show) term rel"
assumes fin: "finite (afs_syms pi)"
and ce_compat: "∃ n. ∀ m ≥ n. ∀ c. ce_trs (c,m) ⊆ NS"
shows "∃ n. ∀ m ≥ n. ∀ c. ce_trs (c,m) ⊆ afs_rel pi NS"
proof -
let ?pi = "afs pi"
let ?NS = "afs_rel pi NS"
let ?ar = "afs_to_unused_arity pi"
let ?sar = "Suc (Suc ?ar)"
have pi2: "⋀ m c. m ≥ ?sar ⟹ ?pi (c, m) = default_af_entry m"
by (rule afs_to_unused_arity[OF fin], simp)
from ce_compat obtain n where ce_NS: "⋀ m c . m ≥ n ⟹ ce_trs (c,m) ⊆ NS" by blast
let ?n = "max n ?sar"
show "∃ n. ∀ m ≥ n. ∀ c. ce_trs (c,m) ⊆ ?NS"
proof (rule exI[of _ ?n], intro allI impI)
fix m c d
assume m: "m ≥ ?n"
hence mn: "m ≥ n" by simp
{
fix t s :: "('f,'v)term"
let ?list = "t # s # replicate m (Var undefined)"
from pi2 m have id: "?pi (c,length ?list) = default_af_entry (length ?list)" by simp
have "(afs_term pi (Fun c ?list), afs_term pi t) ∈ NS"
using ce_NS[OF mn, simplified ce_trs.simps, of "FPair c (Suc (Suc m))"]
by (simp only: default_af_entry_id[of pi c ?list, OF id], auto simp: apply_af_entry_const_is_id)
}
moreover
{
fix t s :: "('f,'v)term"
let ?list = "t # s # replicate m (Var undefined)"
from pi2 m have id: "?pi (c,length ?list) = default_af_entry (length ?list)" by simp
have "(afs_term pi (Fun c ?list), afs_term pi s) ∈ NS"
using ce_NS[OF mn, simplified ce_trs.simps, of "FPair c (Suc (Suc m))"]
by (simp only: default_af_entry_id[of pi c ?list, OF id], auto simp: apply_af_entry_const_is_id)
}
ultimately
show "ce_trs (c,m) ⊆ ?NS"
by (auto simp: ce_trs.simps afs_rel_def afs_rule_def pi2)
qed
qed
locale afs_ce_redtriple_impl = afs_redtriple_impl π S NS NST cS cNS cNST + filtered: redtriple_impl S NS NST cS cNS cNST + ce: ce_redtriple S NS NST + order: redtriple_order S NS NST
for π and S NS NST :: "(('f::{show,key})filtered,'v::show)trs" and cS cNS cNST
locale afs_ce_mono_redtriple_impl = mono_afs_redtriple_impl π S NS NST cS cNS cNST cm + filtered: ce_mono_redtriple_impl S NS NST cS cNS cNST cm + order: redtriple_order S NS NST
for π and S NS NST :: "(('f::{show,key})filtered,'v::show)trs" and cS cNS cNST cm
sublocale afs_ce_mono_redtriple_impl ⊆ afs_ce_redtriple_impl ..
sublocale afs_ce_redtriple_impl ⊆ ce_af_redtriple_impl
"afs_rel π S" "afs_rel π NS" "afs_rel π NST"
"afs_check rS π cS" "afs_check rNS π cNS" "afs_check rNST π cNST" "afs_to_af π"
proof -
let ?pi = π
let ?S = "afs_rel π S"
let ?NS = "afs_rel π NS"
let ?NST = "afs_rel π NST"
let ?cS = "afs_check rS ?pi cS"
let ?cNS = "afs_check rNS ?pi cNS"
let ?cNST = "afs_check rNST ?pi cNST"
let ?af = "afs_to_af π"
show "ce_af_redtriple_impl ?S ?NS ?NST ?cS ?cNS ?cNST ?af"
proof
have rp1: "pre_order_pair S NS" ..
have rp2: "redpair_order S NS" ..
show "af_compatible ?af ?NS"
by (rule af_compatible[OF pre_order_pair.refl_NS[OF rp1] redpair_order.all_ctxt_closed[OF rp2]])
next
show "∃ n. ∀ m ≥ n. ∀ c. ce_trs (c,m) ⊆ ?NS"
by (rule af_ce_compat[OF fin ce.NS_ce_compat])
qed
qed
definition check_mono_afs where "check_mono_afs π = check (mono_afs π) (shows ''argument filter is not monotone'')"
sublocale afs_ce_mono_redtriple_impl ⊆ ce_mono_redtriple_impl
"afs_rel π S" "afs_rel π NS" "afs_rel π NST"
"afs_check rS π cS" "afs_check rNS π cNS" "afs_check rNST π cNST" "cm >> check_mono_afs π"
proof
assume "isOK (cm >> check_mono_afs π)"
thus "ctxt.closed (afs_rel π S)"
by (intro checkMonoSound, auto simp: check_mono_afs_def)
next
let ?S = "afs_rel π S"
show "∃ n. ∀ m ≥ n. ∀ c. ce_trs (c,m) ⊆ ?S"
by (rule af_ce_compat[OF fin filtered.S_ce_compat])
qed
fun shows_afs :: "('f :: show) afs_list ⇒ shows"
where
"shows_afs af = foldr (λ((f, n), e).
shows ''pi('' ∘ shows f ∘ shows ''/'' ∘ shows n ∘ shows '') = '' ∘
(case e of
Collapse i ⇒ shows (Suc i)
| AFList ids ⇒ shows (map Suc ids)) ∘ shows_nl) af"
definition
af_redtriple :: "'f afs_list ⇒ ('f filtered, 'v) redtriple ⇒ ('f :: {show, key}, 'v :: show) redtriple"
where
"af_redtriple pi rp = (
let afso = afs_of pi; afs = the afso; af = afs_to_af afs in ⦇
redtriple.valid = do {
check (afso ≠ None) (shows ''invalid positions in argument filter'');
redtriple.valid rp
},
s = afs_check (shows ''>'') afs (redtriple.s rp),
ns = afs_check (shows ''>='') afs (redtriple.ns rp),
nst = afs_check (shows ''>='') afs (redtriple.nst rp),
af = af,
mono_af = empty_af, (* TODO: this is is crude underapproximation *)
mono = λ cs. do {check_mono_afs afs; redtriple.mono rp (map (afs_rule afs) cs)},
desc = shows ''Argument Filter: '' ∘ shows_nl ∘ shows_afs pi ∘ shows_nl ∘ redtriple.desc rp,
not_ws_ns = map_option (λ fs. map fst pi @ map (λ(f, n). (fpair_f f, n)) fs) (redtriple.not_ws_ns rp),
cpx = no_complexity_check
⦈)"
lemma af_redtriple:
fixes pi :: "('f :: {show,key}) afs_list" and
rp :: "'a ⇒ ('f filtered, 'v :: show)redtriple"
assumes rp: "generic_redtriple_impl rp" shows
"generic_redtriple_impl (λ I. (af_redtriple pi (rp I)))"
proof
fix I s_list ns_list nst_list
let ?rp = "af_redtriple pi (rp I) :: ('f, 'v)redtriple"
assume valid: "isOK(redtriple.valid ?rp)" and stri: "isOK (check_allm (redtriple.s ?rp) s_list)" and nstri: "isOK (check_allm (redtriple.ns ?rp) ns_list)"
and nstrit: "isOK (check_allm (redtriple.nst ?rp) nst_list)"
let ?pi = "the (afs_of pi)"
let ?p = "afs_to_af ?pi"
let ?pi' = "redtriple.af (rp I)"
let ?pi'' = "redtriple.af (af_redtriple pi (rp I))"
let ?mpi'' = "redtriple.mono_af (af_redtriple pi (rp I))"
let ?cpx = "redtriple.cpx ?rp"
let ?cpx' = "λ cm cc. isOK(?cpx cm cc)"
let ?ws = "redtriple.not_ws_ns ?rp"
have cpx: "?cpx = no_complexity_check" unfolding af_redtriple_def Let_def by simp
have pi'': "?pi'' = ?p" unfolding af_redtriple_def Let_def by simp
have mpi'': "?mpi'' = empty_af" unfolding af_redtriple_def Let_def by simp
let ?af_term = "afs_term ?pi"
let ?af_list = "map (λ (s,t). (?af_term s, ?af_term t))"
let ?as_list = "?af_list s_list"
let ?ans_list = "?af_list ns_list"
let ?anst_list = "?af_list nst_list"
from valid have valid: "isOK(redtriple.valid (rp I))" and wf_afs: "afs_of pi ≠ None" unfolding af_redtriple_def by (auto simp: Let_def)
then obtain π where π: "afs_of pi = Some π" by (cases, auto)
from afs_of_Some_afs_syms[OF π] have fin: "finite (afs_syms ?pi)" unfolding π by auto
from stri have stri: "isOK(check_allm (redtriple.s (rp I)) ?as_list)" by (auto simp: Let_def af_redtriple_def afs_check_def)
from nstri have nstri: "isOK(check_allm (redtriple.ns (rp I)) ?ans_list)" by (auto simp: Let_def af_redtriple_def afs_check_def)
from nstrit have nstrit: "isOK(check_allm (redtriple.nst (rp I)) ?anst_list)" by (auto simp: Let_def af_redtriple_def afs_check_def)
from generic_redtriple_impl.generate_redtriple[of rp, OF rp valid stri nstri nstrit]
obtain S NS NST mono_af where redtriple: "cpx_ce_af_redtriple_order S NS NST ?pi' mono_af (λ cm cc. isOK(redtriple.cpx (rp I) cm cc))"
and stri: "set ?as_list ⊆ S"
and nstri: "set ?ans_list ⊆ NS"
and nstrit: "set ?anst_list ⊆ NST"
and ws': "not_ws_info NS (redtriple.not_ws_ns (rp I))"
and cmono: "isOK (redtriple.mono (rp I) (?as_list @ ?ans_list @ ?anst_list)) ⟶ mono_ce_af_redtriple_order S NS NST ?pi' ∧ ctxt.closed S" by auto
let ?aS = "afs_rel ?pi S"
let ?aNS = "afs_rel ?pi NS"
let ?aNST = "afs_rel ?pi NST"
from redtriple interpret cpx_ce_af_redtriple_order S NS NST ?pi' mono_af "λ cm cc. isOK(redtriple.cpx (rp I) cm cc)" .
have rp1: "pre_order_pair S NS" ..
have rp2: "redpair_order S NS" ..
interpret afs_redtriple ?pi S NS NST ..
interpret cpx_ce_af_redtriple_order ?aS ?aNS ?aNST ?p empty_af "λ cm cc. isOK (?cpx cm cc)" unfolding cpx
proof(unfold_locales, rule af_ce_compat[OF fin NS_ce_compat])
show "af_compatible ?p ?aNS"
by (rule af_compatible[OF pre_order_pair.refl_NS[OF rp1] redpair_order.all_ctxt_closed[OF rp2]])
show "af_monotone empty_af ?aS" by (rule empty_af)
qed (simp add: no_complexity_check_def)
show "∃S NS NST. cpx_ce_af_redtriple_order S NS NST ?pi'' ?mpi'' ?cpx' ∧
set s_list ⊆ S ∧
set ns_list ⊆ NS ∧
set nst_list ⊆ NST ∧
not_ws_info NS ?ws ∧
(isOK (redtriple.mono (af_redtriple pi (rp I)) (s_list @ ns_list @ nst_list)) ⟶
mono_ce_af_redtriple_order S NS NST ?pi'' ∧ ctxt.closed S)" unfolding pi'' mpi''
proof (intro exI conjI)
show "set s_list ⊆ ?aS" using stri unfolding afs_rel_def afs_rule_def by auto
show "set ns_list ⊆ ?aNS" using nstri unfolding afs_rel_def afs_rule_def by auto
show "set nst_list ⊆ ?aNST" using nstrit unfolding afs_rel_def afs_rule_def by auto
show "cpx_ce_af_redtriple_order ?aS ?aNS ?aNST ?p empty_af ?cpx'" ..
let ?ws' = "redtriple.not_ws_ns (rp I)"
let ?fs' = "λfs. map fst pi @ map (λ(f, y). (fpair_f f, y)) fs"
show "not_ws_info ?aNS ?ws" unfolding af_redtriple_def Let_def redtriple.simps
proof (cases "redtriple.not_ws_ns (rp I)")
case (Some fs)
show "not_ws_info ?aNS (map_option ?fs' ?ws')" unfolding Some option.simps not_ws_info.simps
proof (intro allI impI)
fix fn i
assume nmem1: "fn ∉ set (?fs' fs)"
hence "fn ∉ fst ` set pi" by auto
hence nmem: "fn ∉ afs_syms ?pi" using afs_of_Some_afs_syms[OF π] unfolding π by auto
obtain f n where f: "fn = (f,n)" by force
from afs_syms[OF nmem[unfolded f]]
have pi: "afs ?pi (f,n) = default_af_entry n" .
show "ws_fun_arg ?aNS fn i" unfolding f
proof (rule ws_fun_argI)
fix ts :: "('f,'v)term list"
assume n: "length ts = n" and i: "i < n"
thus "(Fun f ts, ts ! i) ∈ ?aNS" unfolding afs_rel_def afs_rule_def
proof (simp del: afs_term.simps add: default_af_entry_id[of ?pi, OF pi[folded n]])
from nmem1 have "(FPair f n, length ts) ∉ set fs" unfolding f n
by force
from ws'[unfolded Some, simplified, rule_format, OF this]
have "ws_fun_arg NS (FPair f n, length ts) i" .
from this[unfolded ws_fun_arg_def, rule_format, of "map (afs_term ?pi) ts"]
show "(Fun (FPair f n) (map (afs_term ?pi) ts), afs_term ?pi (ts ! i)) ∈ NS"
using n[symmetric] i by auto
qed
qed
qed
qed simp
show "isOK (redtriple.mono (af_redtriple pi (rp I)) (s_list @ ns_list @ nst_list)) ⟶
mono_ce_af_redtriple_order ?aS ?aNS ?aNST ?p ∧ ctxt.closed ?aS" (is "?prem ⟶ ?mono ∧ ?ctxt")
proof
assume prem: ?prem
have afs: "afs_rule ?pi = (λ (l,r). (afs_term ?pi l, afs_term ?pi r))"
by (rule ext, unfold afs_rule_def, force)
from prem cmono have mono: "mono_ce_af_redtriple_order S NS NST ?pi'"
and cmono: "mono_afs ?pi" and ctxt: "ctxt.closed S"
unfolding af_redtriple_def check_mono_afs_def by (auto simp: Let_def afs)
from mono interpret mono_ce_af_redtriple_order S NS NST ?pi' .
have ?mono
by (unfold_locales, rule af_ce_compat[OF fin S_ce_compat])
have ?ctxt
by (rule ctxt_closed[OF cmono ctxt])
from ‹?mono› ‹?ctxt› show "?mono ∧ ?ctxt" ..
qed
qed
qed
end