Theory Ord.WPO_Impl
theory WPO_Impl
imports
Weighted_Path_Order.WPO
Efficient_Weighted_Path_Order.WPO_Mem_Impl
Term_Order_Impl
Status_Impl
TRS.Term_Impl
Auxx.Name
Show.Shows_Literal
begin
lemma (in wpo_with_assms) wpo_rewrite_order: "rewrite_order WPO_S WPO_NS"
proof -
interpret order_pair WPO_S WPO_NS by (rule wpo_order_pair)
show ?thesis
proof
show "subst.closed WPO_S" using wpo_stable by auto
show "subst.closed WPO_NS" using wpo_stable by auto
show "ctxt.closed WPO_NS" using wpo_ns_mono one_imp_ctxt_closed[of WPO_NS] by blast
qed
qed
lemma (in wpo_with_assms) wpo_co_rewrite_pair: "co_rewrite_pair WPO_S WPO_NS"
proof -
interpret rewrite_order WPO_S WPO_NS by (rule wpo_rewrite_order)
interpret order_pair WPO_S WPO_NS by (rule wpo_order_pair)
show ?thesis
proof (unfold_locales, rule refl_NS, rule trans_NS)
show "WPO_NS ∩ WPO_S¯ = {}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain a where "(a,a) ∈ WPO_S" using compat_S_NS by blast
thus False using wpo_irrefl unfolding irrefl_def by auto
qed
qed
qed
context wpo_with_SN_assms
begin
lemma wpo_redtriple_order: "redtriple_order WPO_S WPO_NS WPO_NS"
proof -
interpret rewrite_order WPO_S WPO_NS by (rule wpo_rewrite_order)
interpret SN_order_pair WPO_S WPO_NS by (rule wpo_SN_order_pair)
show ?thesis
proof (unfold_locales; (intro trans_NS refl_NS compat_NS_S WPO_S_subset_WPO_NS)?)
show "subst.closed WPO_NS" using wpo_stable by auto
qed
qed
end
definition af_compatible_status :: "'f af ⇒ 'f status ⇒ bool"
where
"af_compatible_status π σ ⟷ (∀ f m. set (status σ (f, m)) ⊆ π (f, m))"
lemma af_compatible_status_full_af: "af_compatible_status full_af σ"
unfolding af_compatible_status_def full_af_def using status[of σ] by auto
locale wpo_params = ws_rewrite_order S NS σσ + precedence prc prl
for NS S :: "('f, 'v) trs"
and prc :: "'f × nat ⇒ 'f × nat ⇒ bool × bool"
and prl :: "'f × nat ⇒ bool"
and ssimple :: bool
and large :: "'f × nat ⇒ bool"
and c :: "'f × nat ⇒ order_tag"
and n :: nat
and σσ :: "'f status" +
assumes large: "ssimple ⟹ large fn ⟹ fst (prc fn gm) ∨ snd (prc fn gm) ∧ status σσ gm = []"
and large_trans: "ssimple ⟹ large fn ⟹ snd (prc gm fn) ⟹ large gm"
and strictly_simple: "ssimple ⟹ ss_rewrite_order S NS σσ"
and irrefl_S: "irrefl S"
begin
sublocale wpo_with_assms
proof (unfold_locales; (intro S_imp_NS large ws_status S_stable NS_stable NS_mono irrefl_S; assumption)?)
assume ssimple
show "large fn ⟹ snd (prc gm fn) ⟹ large gm" for fn gm by (rule large_trans[OF `ssimple`])
interpret ss_rewrite_order S NS σσ by (rule strictly_simple[OF `ssimple`])
show "S ≠ {}" by (rule S_non_empty)
show "i ∈ set (status σσ fn) ⟹ simple_arg_pos S fn i " for fn i by (rule ss_status)
qed
lemma wpo_with_SN_assms: assumes "SN S"
shows "wpo_with_SN_assms S NS prc prl σσ ssimple large"
by (unfold_locales, rule assms)
lemma ce_σ: assumes "{0,1} ⊆ set (σ (f,Suc (Suc k)))"
shows "ce_trs (f,k) ⊆ WPO_S ∧ ce_trs (f,k) ⊆ WPO_NS"
proof -
{
fix s t :: "('f,'v)term"
assume "(s,t) ∈ ce_trs (f,k)"
from this[unfolded ce_trs.simps]
obtain u v where s: "s = Fun f (u # v # replicate k (Var undefined))" (is "_ = Fun _ ?ss")
and t: "t = u ∨ t = v" by auto
from t subterm_wpo_s_arg[of 0 f ?ss] subterm_wpo_s_arg[of 1 f ?ss] assms
have "(s,t) ∈ WPO_S" unfolding s by (cases, auto)
}
then show ?thesis using wpo_s_imp_ns by blast
qed
context
fixes π :: "'f af"
assumes af_NS: "af_compatible π NS"
and af_σ: "af_compatible_status π σσ"
begin
lemma af_σ: "i < m ⟹ i ∈ π (f,m) ∨ i ∉ set (σ (f,m))"
using af_σ[unfolded af_compatible_status_def] by blast
lemma wpo_af_compatible: "af_compatible π WPO_NS"
unfolding af_compatible_def
proof (intro allI)
fix f and bef aft :: "('f,'v)term list" and s t
let ?i = "length bef"
let ?n = "Suc (?i + length aft)"
let ?ss = "bef @ s # aft"
let ?ts = "bef @ t # aft"
let ?s = "Fun f ?ss"
let ?t = "Fun f ?ts"
let ?σ = "σ (f,?n)"
show "?i ∈ π (f, ?n) ∨ (?s, ?t) ∈ WPO_NS"
proof (cases "?i ∈ π (f, ?n)")
case False
have i: "?i < ?n" by auto
from af_σ[OF i, of f] False have iσ: "?i ∉ set ?σ" by auto
from af_NS[unfolded af_compatible_def, rule_format, of bef f aft s t] False
have id: "((?s, ?t) ∈ NS) = True" "length ?ss = ?n" "length ?ts = ?n" by auto
have "∀j∈set ?σ. wpo_s ?s (?ts ! j)" (is ?one)
proof
fix j
assume j: "j ∈ set ?σ"
with iσ have ji: "j ≠ ?i" by auto
then have id: "?ts ! j = ?ss ! j" by (rule append_Cons_nth_not_middle)
show "wpo_s ?s (?ts ! j)" unfolding id
by (rule subterm_wpo_s_arg, insert j, auto)
qed
then have one: "?one = True" by simp
have two: "map ((!) ?ts) ?σ = map ((!) ?ss) ?σ" (is "?mts = ?mss")
proof (rule nth_equalityI, force, unfold length_map)
fix i
assume i: "i < length ?σ"
with iσ have "?σ ! i ≠ ?i" unfolding set_conv_nth by auto
then show "?mts ! i = ?mss ! i" using i by (simp add: nth_append)
qed
have "snd (lex_ext wpo n ?mss ?mts)" unfolding two
by (rule all_nstri_imp_lex_nstri, insert wpo_ns_refl, auto)
moreover have "snd (mul_ext wpo ?mss ?mts)" unfolding two
by (rule all_nstri_imp_mul_nstri, insert wpo_ns_refl, auto)
ultimately have "wpo_ns ?s ?t" unfolding wpo.simps[of ?s ?t] term.simps id one
prc_refl by (cases "c (f,?n)", auto simp: Let_def)
then show ?thesis by blast
qed simp
qed
end
lemma wpo_ce_compat:
assumes ce: "∃n. ∀m≥n. ∀ f. {0,1} ⊆ set (σ (f, Suc (Suc m)))"
shows "ce_compatible WPO_NS" "ce_compatible WPO_S"
proof -
from assms obtain n where "⋀ m f. m ≥ n ⟹ {0,1} ⊆ set (σ (f, Suc (Suc m)))" by blast
from ce_σ[OF this] show "ce_compatible WPO_NS" "ce_compatible WPO_S"
unfolding ce_compatible_def by blast+
qed
lemma wpo_ce_af_redtriple_order:
assumes ce: "∃n. ∀m≥n. ∀ f. {0,1} ⊆ set (σ (f, Suc (Suc m)))"
and pi: "af_compatible π NS" "af_compatible_status π σσ"
and SN: "SN S"
shows "ce_af_redtriple_order WPO_S WPO_NS WPO_NS π"
proof -
from wpo_with_SN_assms[OF SN]
interpret wpo_with_SN_assms n S NS prc prl σσ c ssimple large .
interpret redtriple_order WPO_S WPO_NS WPO_NS by (rule wpo_redtriple_order)
from wpo_ce_compat[OF ce] have "ce_compatible WPO_NS" "ce_compatible WPO_S" by auto
with wpo_af_compatible[OF pi]
show ?thesis using full_af by (unfold_locales, blast+)
qed
context
assumes σ_full: "⋀ f k. set (σ (f,k)) = {0 ..< k}"
begin
lemma ctxt_closed_WPO_S: "ctxt.closed WPO_S"
using one_imp_ctxt_closed[OF WPO_S_ctxt[OF σ_full]] by blast
lemma wpo_mono_ce_af_redtriple_order:
assumes ce: "∃n. ∀m≥n. ∀ f. {0,1} ⊆ set (σ (f, Suc (Suc m)))"
and pi: "af_compatible π NS" "af_compatible_status π σσ"
and SN: "SN S"
shows "mono_ce_af_redtriple_order WPO_S WPO_NS WPO_NS π"
proof -
interpret ce_af_redtriple_order WPO_S WPO_NS WPO_NS π
by (rule wpo_ce_af_redtriple_order[OF ce pi SN])
show ?thesis
proof (unfold_locales)
show "ctxt.closed WPO_S" by (rule ctxt_closed_WPO_S)
show "ce_compatible WPO_S" unfolding ce_compatible_def
using ce_σ[unfolded σ_full] by auto
qed
qed
end
end
definition af_wpo :: "'f af ⇒ 'f status ⇒ 'f af"
where
"af_wpo π σ f = set (status σ f) ∪ π f"
lemma af_wpo_compat: "af_compatible π NS ⟹ af_compatible (af_wpo π σ) NS"
unfolding af_compatible_def af_wpo_def by auto
lemma af_wpo_status: "af_compatible_status (af_wpo π σ) σ"
unfolding af_compatible_status_def af_wpo_def by auto
abbreviation var_x_i :: "nat => ('f, string) term"
where
"var_x_i i == Var (''x'' @ show i)"
fun check_status_ws_info :: "'f status ⇒ (('f, string) rule ⇒ showsl check) ⇒ (('f :: showl) × nat) list option ⇒ showsl check"
where
"check_status_ws_info σ cns None = error (showsl_lit (STR ''missing weak-subterm status of base reduction pair''))"
| "check_status_ws_info σ cns (Some fs) = check_allm (λ(f, n).
check_allm (λi.
let s = Fun f (map var_x_i [0..<n]); t = var_x_i i in
cns (s, t)
<+? (λ_. showsl_lit (STR ''argument #'') ∘ showsl (Suc i) ∘
showsl_lit (STR '' is in status of '') ∘ showsl_funa (f, n) ∘ showsl_nl ∘
showsl_lit (STR ''but '') ∘ showsl s ∘ showsl_lit (STR '' >= '') ∘ showsl_nat_var i ∘
showsl_lit (STR '' is not satisfied''))) (status σ (f, n))) fs"
type_synonym 'f wpo_params = "(('f × nat) × (nat × nat list × order_tag)) list"
definition showsl_wpo_params :: "('f :: showl) wpo_params ⇒ showsl" where
"showsl_wpo_params params = showsl_lit (STR ''status and precedence:⏎'') ∘
showsl_sep (λ(f, (p, s, lm)).
showsl_lit (STR ''precedence('') ∘ showsl_funa f ∘ showsl_lit (STR '') = '') ∘ showsl p ∘ showsl_nl ∘
showsl_lit (STR '' status('') ∘ showsl_funa f ∘ showsl_lit (STR '') = '') ∘ showsl_list s ∘ showsl_nl o
showsl_lit (STR '' arg-status('') ∘ showsl_funa f ∘ showsl_lit (STR '') = '') ∘ showsl (case lm of Mul ⇒ STR ''mul'' | Lex ⇒ STR ''lex'') ∘ showsl_nl
) showsl_nl params"
definition large_of where
"large_of pr σ fs = (let m = max_list (map pr fs);
ls = filter (λ f. pr f = m) fs
in if m > 0 ∧ (∀ f ∈ set ls. status σ f = []) then Some m else None)"
definition wpo_rel_impl :: "('f :: {compare_order, showl}, string) rel_impl ⇒ 'f wpo_params ⇒ ('f, string) rel_impl"
where
"wpo_rel_impl rt params ≡
(let
stat = map (λ (f,ps). (f, fst (snd ps))) params;
mparams = ceta_map_of params;
pr = fun_of_map_fun' mparams (λ _. 0) fst;
ot = fun_of_map_fun' mparams (λ _. Lex) (snd o snd);
desc1 = showsl_lit (STR ''WPO '');
desc2 = showsl_lit (STR ''with '') o showsl_wpo_params params ∘
showsl_lit (STR ''⏎over the following reduction pair:⏎'') ∘ rel_impl.desc rt
in
(case status_of stat of
None ⇒ faulty_rel_impl (TYPE('f)) (TYPE(string)) (showsl_lit (STR ''problem with indices in status of WPO!'')) (desc1 o desc2)
| Some σ ⇒
let
large_opt = large_of pr σ (map fst params);
ssimple = ¬ is_None large_opt ∧ isOK(check_status_ws_info σ (rel_impl.s rt) (rel_impl.not_sst rt));
large = (if ssimple then λ f. pr f = the large_opt else (λ _. False));
s = (λ s t. isOK (rel_impl.s rt (s, t)));
ns = (λ s t. isOK (rel_impl.ns rt (s, t)));
wpo = wpo_ub (prc_nat pr) (prl_nat pr) ssimple large s ns σ ot;
wpo_s = (λ (s,t). check (fst (wpo s t)) (showsl s ∘ showsl_lit (STR '' >wpo '') ∘ showsl t ∘ showsl_lit (STR '' could not be ensured'')));
wpo_ns = (λ (s,t). check (snd (wpo s t)) (showsl s ∘ showsl_lit (STR '' >=wpo '') ∘ showsl t ∘ showsl_lit (STR '' could not be ensured'')))
in ⦇
rel_impl.valid = do {
rel_impl.valid rt;
rel_impl.standard rt;
rel_impl.subst_s rt <+? (λ e. showsl_lit (STR ''WPO requires stability of strict base relation⏎'') o e);
check_status_ws_info σ (rel_impl.ns rt) (rel_impl.not_wst rt)
},
standard = succeed,
desc = if ssimple then desc1 o showsl_lit (STR ''(strictly simple) '') o desc2 else desc1 o desc2,
s = wpo_s,
ns = wpo_ns,
nst = wpo_ns,
af = af_wpo (rel_impl.af rt) σ,
top_af = af_wpo (rel_impl.af rt) σ,
SN = rel_impl.SN rt,
subst_s = succeed,
ce_compat = succeed,
co_rewr = succeed,
top_mono = succeed,
top_refl = succeed,
mono_af = empty_af,
mono = (λ_. check_allm (λ((f, n), idx). check (set idx = set [0..<n]) (
showsl_lit (STR ''for monotonicity, status must be complete, but status of '') ∘
showsl_funa (f, n) ∘ showsl_lit (STR '' is '') ∘ showsl (map Suc idx))) stat),
not_wst = Some (map fst stat),
not_sst = Some (map fst stat),
cpx = no_complexity_check
⦈))"
lemma wpo_rel_impl: assumes rt: "rel_impl rt"
shows "rel_impl (wpo_rel_impl rt param)"
unfolding rel_impl_def
proof (intro impI allI, goal_cases)
case (1 U)
let ?rp = "wpo_rel_impl rt param"
let ?pi = "rel_impl.af ?rp"
let ?mpi = "rel_impl.mono_af ?rp"
let ?cpx = "rel_impl.cpx ?rp"
let ?Cpx = "λ cm cc. isOK(?cpx cm cc)"
let ?s = "λ s t. isOK(rel_impl.s ?rp (s,t))"
let ?ns = "λ s t. isOK(rel_impl.ns ?rp (s,t))"
let ?stat = "map (λ (f,ps). (f, fst (snd ps))) param"
let ?ot = "fun_of_map_fun' (ceta_map_of param) (λ _. Lex) (snd o snd)"
let ?rp' = "rt"
let ?pi' = "rel_impl.af ?rp'"
let ?mpi' = "rel_impl.mono_af ?rp'"
let ?cpx' = "rel_impl.cpx ?rp'"
let ?Cpx' = "λ cm cc. isOK(?cpx' cm cc)"
let ?s' = "λ s t. isOK(rel_impl.s ?rp' (s,t))"
let ?ns' = "λ s t. isOK(rel_impl.ns ?rp' (s,t))"
let ?pr = "fun_of_map_fun' (ceta_map_of param) (λ _. 0) fst"
let ?ws' = "rel_impl.not_wst ?rp'"
let ?ss' = "rel_impl.not_sst ?rp'"
define pr where "pr = ?pr"
define ot where "ot = ?ot"
let ?prc = "prc_nat pr"
let ?prl = "prl_nat pr"
note d = wpo_rel_impl_def[of rt param, unfolded Let_def]
from 1 d obtain σ where stat: "status_of ?stat = Some σ" by (cases "status_of ?stat", auto)
note d = d[unfolded stat option.simps rel_impl.simps]
have top_af: "rel_impl.top_af ?rp = ?pi" unfolding d by auto
let ?large_opt = "large_of pr σ (map fst param)"
define ssimple where "ssimple = (¬ is_None ?large_opt ∧ isOK (check_status_ws_info σ (rel_impl.s rt) (rel_impl.not_sst rt)))"
define large where "large = (if ssimple then λ f. pr f = (the ?large_opt) else (λ _ :: ('a × nat). False))"
note d = d[folded pr_def, folded ssimple_def, folded large_def, folded ot_def]
note 1 = 1[unfolded d, simplified]
let ?wpo = "wpo_ub (prc_nat pr) (prl_nat pr) ssimple large ?s' ?ns' σ ot"
from 1 have status_ws: "isOK(check_status_ws_info σ (rel_impl.ns ?rp') ?ws')"
and "isOK(rel_impl.valid ?rp')" by auto
note rt = rt[unfolded rel_impl_def, rule_format, OF this(2)]
from status_ws obtain fs where ws': "?ws' = Some fs" by (cases ?ws', auto)
from status_ws[unfolded ws']
have status_ws: "⋀f n i. (f, n) ∈ set fs ⟹ i ∈ set (status σ (f, n)) ⟹
?ns' (Fun f (map var_x_i [0..<n])) (var_x_i i)" by auto
have status_ss: "⋀f n i. ssimple ⟹ (f, n) ∈ set (the ?ss') ⟹ i ∈ set (status σ (f, n)) ⟹
?s' (Fun f (map var_x_i [0..<n])) (var_x_i i)" unfolding ssimple_def by (cases ?ss', auto)
define subts where "subts = [(u,v) . (s,t) <- U, u <- supteq_list s, v <- supteq_list t]"
define s where "s = subts @ [(Fun f (map var_x_i [0..<n]), var_x_i i :: ('a, _) Term.term). (f, n) <- the ?ss', i <- status σ (f, n)]"
define ns where "ns = subts @ [(Fun f (map var_x_i [0..<n]), var_x_i i). (f, n) <- fs, i <- status σ (f, n)]"
let ?U = "s @ ns"
from rt[of ?U] obtain S NS NST where rt: "rel_impl_prop rt ?U S NS NST" by presburger
from rt 1 have
*: "S ⊆ NS" "irrefl S" "ctxt.closed NS" "S O NS ⊆ S" "NS O S ⊆ S" "trans NS" "refl NS"
and subst_NS: "subst.closed NS"
and subst_S: "subst.closed S"
and af_compat: "af_compatible (rel_impl.af rt) NS"
and ws: "not_subterm_rel_info NS ?ws'"
and sst: "not_subterm_rel_info S ?ss'"
and SN: "isOK( rel_impl.SN rt) ⟹ SN S"
by (auto simp: rel_impl_def)
have "set s ⊆ set ?U" "set ns ⊆ set ?U"
by (auto simp: ns_def)
with rt[THEN conjunct1]
have orient: "⋀ l r. ?s' l r ⟹ (l,r) ∈ set s ⟹ (l,r) ∈ S"
"⋀ l r. ?ns' l r ⟹ (l,r) ∈ set ns ⟹ (l,r) ∈ NS"
by auto
define n where "n = max_list [ length (status σ f) . (s,t) <- U, f <- funas_term_list t]"
interpret precedence ?prc ?prl ..
note cb = compare_bools_def
let ?wpoo = "wpo_orig ?prc ?prl ssimple large σ ot n S NS"
{
fix s t
assume st: "(s,t) ∈ set U"
have "?wpo s t ≤⇩c⇩b ?wpoo s t"
proof (rule wpo_ub)
fix si tj
assume "s ⊵ si" "t ⊵ tj"
with st have sitj: "(si,tj) ∈ set subts" unfolding subts_def by force
with orient
show "(?s' si tj, ?ns' si tj)
≤⇩c⇩b ((si, tj) ∈ S, (si, tj) ∈ NS)" unfolding s_def ns_def cb by auto
next
fix f
assume f: "f ∈ funas_term t"
show "length (status σ f) ≤ n" unfolding n_def
by (rule max_list, insert f st, auto)
qed
} note cb_all = this[unfolded cb]
interpret wpo_params NS S ?prc ?prl ssimple large ot n σ
proof (unfold_locales; (intro subst_S subst_NS *)?)
from ‹S O NS ⊆ S› ‹S ⊆ NS› show "trans S" unfolding trans_def by auto
show "trans S" by fact
fix i fn
assume i: "i ∈ set (status σ fn)"
obtain f n where f: "fn = (f,n)" by force
show "simple_arg_pos NS fn i"
proof (cases "fn ∈ set fs")
case False
with ws[unfolded ws'] show ?thesis by (auto simp: f)
next
case True
let ?l = "Fun f (map var_x_i [0..<n])"
let ?r = "var_x_i i"
have ns: "(?l, ?r) ∈ NS" using orient(2)[OF status_ws] i True unfolding ns_def f by force
show ?thesis unfolding f
proof (rule simple_arg_posI)
fix ts :: "('a,string)term list"
assume len: "length ts = n" and i: "i < n"
define inv where "inv = (λs. ts ! the_inv show (tl s))"
{
fix i
have "inv (the_Var (var_x_i i)) = ts ! i" unfolding inv_def
using the_inv_f_f[OF inj_show_nat] by auto
}
with subst.closedD[OF subst_NS ns, of inv]
show "(Fun f ts, ts ! i) ∈ NS"
by (auto simp: o_def len[symmetric] map_nth)
qed
qed
show "simple_arg_pos NS fn i" by fact
next
assume ssimple: ssimple
then obtain gs where sst': "?ss' = Some gs" unfolding ssimple_def by (cases ?ss', auto)
{
fix i fn
assume i: "i ∈ set (status σ fn)"
obtain f n where f: "fn = (f,n)" by force
show "simple_arg_pos S fn i"
proof (cases "fn ∈ set gs")
case False
with sst[unfolded sst'] show ?thesis by (auto simp: f)
next
case True
let ?l = "Fun f (map var_x_i [0..<n])"
let ?r = "var_x_i i"
have s: "(?l, ?r) ∈ S" using orient(1)[OF status_ss[OF ssimple]] i True unfolding s_def f sst' by force
show ?thesis unfolding f
proof (rule simple_arg_posI)
fix ts :: "('a,string)term list"
assume len: "length ts = n" and i: "i < n"
define inv where "inv = (λs. ts ! the_inv show (tl s))"
{
fix i
have "inv (the_Var (var_x_i i)) = ts ! i" unfolding inv_def
using the_inv_f_f[OF inj_show_nat] by auto
}
with subst.closedD[OF subst_S s, of inv]
show "(Fun f ts, ts ! i) ∈ S"
by (auto simp: o_def len[symmetric] map_nth)
qed
qed
}
{
obtain f :: 'a where True by auto
define n where "n = 1 + max_list (map snd gs)"
have "(f,n) ∉ set gs"
proof
assume "(f,n) ∈ set gs"
hence "n ∈ set (map snd gs)" by auto
from max_list[OF this] show False unfolding n_def by simp
qed
from sst[unfolded sst', simplified, rule_format, OF this]
have "simple_arg_pos S (f, n) 0" unfolding n_def by auto
from this[unfolded simple_arg_pos_def, simplified, rule_format, of "replicate n undefined"]
obtain a b where ab: "(a,b) ∈ S" unfolding n_def by auto
thus "S ≠ {}" by auto
}
from ssimple obtain m where large_opt: "?large_opt = Some m" unfolding ssimple_def by (cases ?large_opt, auto)
fix f g
assume lf: "large f"
have large: "⋀ g. large g = (pr g = m)" unfolding large_def large_opt using ssimple by auto
note large_opt = large_opt[unfolded large_of_def Let_def]
from large_opt have m: "m > 0" by (auto split: if_splits)
have snd: "snd (?prc g f) = (pr g ≥ pr f)" for g f unfolding prc_nat_def Let_def by simp
have fst: "fst (?prc g f) = (pr g > pr f)" for g f unfolding prc_nat_def Let_def by simp
from large_opt have max: "⋀ f. f ∈ set (map fst param) ⟹ pr f ≤ m"
by (force split: if_splits option.splits intro!: max_list)
have 0: "⋀ f. f ∉ set (map fst param) ⟹ pr f = 0" unfolding pr_def ceta_map_of fun_of_map_fun'.simps
using map_of_eq_None_iff[of param] by force
from large_opt have status: "⋀ f. f ∈ set (map fst param) ⟹ pr f = m ⟹ status σ f = []"
by (auto split: if_splits)
show "snd (?prc g f) ⟹ large g" using max[of g] 0 lf unfolding large fst snd by fastforce
thus "fst (?prc f g) ∨ snd (?prc f g) ∧ status σ g = []" using status[of g] max[of g] m 0
unfolding large fst snd by (metis large lf status nat_le_linear nat_less_le)
qed
from af_compat have "af_compatible ?pi' NS" .
from af_wpo_compat[OF this, of σ] have pi: "af_compatible ?pi NS"
unfolding param d split by auto
from af_wpo_status[of ?pi' σ] have pi2: "af_compatible_status ?pi σ"
unfolding param d split by auto
let ?m = "max_list (map (snd o fst) ?stat)"
have σ: "∃n. ∀m≥n. ∀f. {0, 1} ⊆ set (status σ (f, Suc (Suc m)))"
proof (rule exI[of _ ?m], intro allI impI)
fix k f
assume k: "?m ≤ k"
let ?k = "Suc (Suc k)"
from k have "?m < ?k" by auto
with max_list[of ?k "map (snd o fst) ?stat"]
have "(f,?k) ∉ fst ` set ?stat" by force
from status_of_default[OF stat this]
show "{0,1} ⊆ set (status σ (f,Suc (Suc k)))" by auto
qed
let ?S = WPO_S
let ?NS = WPO_NS
from wpo_rewrite_order
interpret rewrite_order WPO_S WPO_NS .
from wpo_co_rewrite_pair
interpret co_rewrite_pair WPO_S WPO_NS .
from wpo_order_pair
interpret order_pair WPO_S WPO_NS .
have mpi: "?mpi = empty_af" unfolding wpo_rel_impl_def Let_def stat
by simp
let ?ws = "rel_impl.not_wst ?rp"
let ?ss = "rel_impl.not_sst ?rp"
have "not_subterm_rel_info ?NS (Some (map fst ?stat)) ∧ not_subterm_rel_info ?S (Some (map fst ?stat))"
unfolding not_subterm_rel_info.simps
proof (intro allI impI conjI)
fix fk i
assume nmem: "fk ∉ set (map fst ?stat)"
obtain f k where f: "fk = (f,k)" by force
with nmem have "(f,k) ∉ fst ` set ?stat" by force
from status_of_default[OF stat this]
subterm_wpo_s_arg[of _ f] subterm_wpo_ns_arg[of _ f]
show "simple_arg_pos ?S fk i" "simple_arg_pos ?NS fk i" unfolding f
by (intro simple_arg_posI, auto)+
qed
then have 4: "not_subterm_rel_info ?NS ?ws"
and 5: "not_subterm_rel_info ?S ?ss" by (auto simp add: d)
show ?case unfolding top_af mpi
proof (rule exI[of _ ?S], intro exI[of _ ?NS] conjI 4 5 impI allI
S_imp_NS ctxt_NS refl_NS trans_NS trans_S compat_NS_S compat_S_NS subst_S subst_NS
af_compat empty_af top_mono_same irrefl_S disj_NS_S)
{
fix st
assume stU: "st ∈ set U"
obtain s t where st: "st = (s,t)" by force
hence "(s,t) ∈ set U" using stU by auto
note cb_all = cb_all[OF this]
show "isOK (rel_impl.s ?rp st) ⟹ st ∈ WPO_S"
using cb_all unfolding d st by auto
show "isOK (rel_impl.ns ?rp st) ⟹ st ∈ WPO_NS"
using cb_all unfolding d st by auto
show "isOK (rel_impl.nst ?rp st) ⟹ st ∈ WPO_NS"
using cb_all unfolding d st by auto
}
{
fix sig
assume mono: "isOK (rel_impl.mono ?rp sig)"
have "set (status σ (f, m)) = {0..<m}" for f m
proof (cases "map_of ?stat (f,m)")
case None
from status_of_default[OF stat this[unfolded map_of_eq_None_iff]]
show ?thesis by auto
next
case (Some idx)
from map_of_SomeD[OF this] mono show ?thesis
by (auto simp: d status_of_Some[OF stat] Some)
qed
from ctxt_closed_WPO_S[OF this]
show "ctxt.closed ?S" .
}
show "ce_compatible ?NS" "ce_compatible ?S" using wpo_ce_compat[OF σ] by auto
show "af_compatible ?pi ?NS" "af_compatible ?pi ?NS" using wpo_af_compatible[OF pi pi2] by auto
show "WPO_S ⊆ WPO_NS" by (rule WPO_S_subset_WPO_NS)
{
assume "isOK (rel_impl.SN ?rp)"
hence "isOK (rel_impl.SN rt)" unfolding d by auto
from SN[OF this] have SN: "SN S" .
from wpo_with_SN_assms.WPO_S_SN[OF wpo_with_SN_assms[OF this], of]
show "SN ?S" .
}
show "irrefl WPO_S" using wpo_irrefl unfolding irrefl_on_def by auto
qed (auto simp: wpo_rel_impl_def stat Let_def isOK_no_complexity)
qed
end