theory Linear_Poly_Order
imports
Term_Order_Extension
Linear_Polynomial
QTRS.Term_Impl
"Check-NT.Name"
QTRS.Map_Choice
begin
text ‹we first head for polynomial interpretations›
type_synonym ('f, 'a) lpoly_inter = "'f × nat ⇒ ('a × 'a list)"
type_synonym ('f, 'a) lpoly_interL = "(('f × nat) × ('a × 'a list)) list"
context
fixes R :: "('a, 'b) lpoly_order_semiring_scheme" (structure)
begin
definition to_lpoly_inter :: "('f :: key, 'a) lpoly_interL ⇒ ('f, 'a) lpoly_inter" where
"to_lpoly_inter I = fun_of_map_fun (ceta_map_of I) (λ fn. (default R,replicate (snd fn) 𝟭))"
definition create_af :: "('f :: key, 'a) lpoly_interL ⇒ 'f af" where
"create_af I ≡ fun_of_map_fun' (ceta_map_of I) (λ (f,n) . {0 ..< n}) (λ (c,coeffs).
set ([ i . (c,i) <- zip coeffs [0 ..< length coeffs], c ≠ 𝟬]))"
definition create_mono_af :: "('f :: key, 'a) lpoly_interL ⇒ 'f af" where
"create_mono_af I ≡ if psm then fun_of_map_fun' (ceta_map_of I) (λ (f,n) . {0 ..< n})
(λ (c,coeffs). set ([ i . c ≽ 𝟬, (c',i) <- zip coeffs [0 ..< length coeffs], c' = 𝟭 ∨ check_mono c'])) else empty_af"
end
context
fixes R :: "('a, 'b) ordered_semiring_scheme" (structure)
begin
fun
eval_termI :: "('f, 'a) lpoly_inter ⇒ ('v, 'a) p_ass ⇒ ('f, 'v) term ⇒ 'a"
where
"eval_termI pi α (Var x) = α x"
| "eval_termI pi α (Fun f ts) =
(let (a, as) = pi (f, length ts) in
Max 𝟬 (a ⊕ (list_sum R (map (λ at. fst at ⊗ (eval_termI pi α (snd at))) (zip as ts)))))"
context
notes [[function_internals, inductive_internals]]
begin
fun PleftI :: "('f, 'a) lpoly_inter ⇒ ('f, 'v) term ⇒ ('v, 'a) l_poly"
where
"PleftI pi (Var x) = (LPoly 𝟬 [(x, 𝟭)] )"
| "PleftI pi (Fun f ts) = (
let (c, as) = pi (f, length ts) in
(case (sum_lpoly R (LPoly c []) (list_sum_lpoly R (map (λ at .
(mul_lpoly R (fst at) (PleftI pi (snd at)))) (zip as ts)))) :: ('v, 'a) l_poly of
LPoly d [] ⇒ LPoly (Max 𝟬 d) []
| p ⇒ p))"
fun PrightI :: "('f, 'a) lpoly_inter ⇒ ('f, 'v) term ⇒ ('v, 'a) l_poly"
where
"PrightI pi (Var x) = (LPoly 𝟬 [(x, 𝟭)] )"
| "PrightI pi (Fun f ts) = (
let (c, as) = pi (f, length ts) in
(case (sum_lpoly R (LPoly c []) (list_sum_lpoly R (map (λ at .
(mul_lpoly R (fst at) (PrightI pi (snd at)))) (zip as ts)))) :: ('v, 'a) l_poly of
LPoly d vp ⇒ LPoly (Max 𝟬 d) vp))"
end
definition coeffs_of_constraint :: "('f, 'a) lpoly_inter ⇒ ('f, 'v) rule ⇒ ('a × 'a) list"
where
"coeffs_of_constraint pi st =
[(a, b). a ← coeffs_of_lpoly R (PleftI pi (fst st)),
b ← coeffs_of_lpoly R (PrightI pi (snd st))]"
end
context
fixes R :: "('a :: show, 'b) lpoly_order_semiring_scheme" (structure)
begin
fun
check_polo_ns
where
"check_polo_ns pi (s, t) = do {
let left = PleftI R pi s;
let right = PrightI R pi t;
check_lpoly_ns R left right
<+? (λe. ''could not ensure '' +#+ shows s +@+ '' >= '' +#+ shows t +@+ shows_nl +@+ e)
}"
fun
check_polo_s
where
"check_polo_s pi (s, t) = do {
let left = PleftI R pi s;
let right = PrightI R pi t;
check_lpoly_s R left right
<+? (λe. ''could not ensure '' +#+ shows s +@+ '' > '' +#+ shows t +@+ shows_nl +@+ e)
}"
definition
check_poly_mono_npsm :: "('f × nat) list ⇒ ('f :: show, 'a) lpoly_interL ⇒ shows check"
where
"check_poly_mono_npsm F pi = check_allm (λ((f, n), (c, cs)). do {
check (n = Suc 0 ⟶ c = 𝟬) (''constant part '' +#+ shows c +@+ '' must be 0 '' +#+ shows_nl);
check (n = length cs) (''the arity is not the same as the number of arguments'' +#+ shows_nl);
check (n ≤ Suc 0) (''symbol has arity larger than 1'' +#+ shows_nl)
} <+? (λs. ''problem with monotonicity due to interpretation of '' +#+ shows f +@+ ''/'' +#+ shows n +@+ shows_nl +@+ s)
) pi >>
check_subseteq F (map fst pi)
<+? (λ fn. ''unknown interpretation for '' +#+ shows fn +@+ shows_nl)"
definition
check_poly_mono :: "('f :: show, 'a) lpoly_interL ⇒ shows check"
where
"check_poly_mono = check_allm (λ((f, n), (c, cs)). do {
check (c ≽ 𝟬)
(''constant part '' +#+ shows c +@+ '' must be at least '' +#+ shows 𝟬 +@+ shows_nl);
check (n ≤ length cs) (''the last argument is ignored'' +#+ shows_nl);
check_allm (λd. check (check_mono d)
(''coefficient '' +#+ shows d +@+ '' is not allowed'' +#+ shows_nl)) cs
} <+? (λs. ''problem with monotonicity due to interpretation of '' +#+ shows f +@+ ''/'' +#+ shows n +@+ shows_nl +@+ s)
)"
fun
check_lpoly_coeffs :: "('f :: show, 'a) lpoly_interL ⇒ shows check"
where
"check_lpoly_coeffs I =
check_allm (λ((f, n), (c, cs)). do {
check (c ∈ carrier R)
(''constant part '' +#+ shows c +@+ '' is not well-formed'' +#+ shows_nl);
check (length cs ≤ n)
(''number of coefficients exceeds arity of symbol '' +#+ shows f);
check (arc_pos c ∨ Bex (set cs) arc_pos)
(''could not find positive entry which is required for arctic interpretations'' +#+ shows_nl);
check_allm (λa. check (a ≽ 𝟬 ∧ a ∈ carrier R)
(''coefficient '' +#+ shows a +@+ '' is not allowed'' +#+ shows_nl)) cs
} <+? (λs. ''problem with interpretation of '' +#+ shows f +@+ ''/'' +#+ shows n +@+ shows_nl +@+ s)
) I"
end
context lpoly_order
begin
declare poly_simps[simp] poly_order_simps[simp]
abbreviation
eval_term ::
"('f, 'a) lpoly_inter ⇒ ('v, 'a) p_ass ⇒ ('f, 'v) term ⇒ 'a" ("_«_,_>>" [1000, 0, 0] 50)
where
"eval_term ≡ eval_termI R"
abbreviation wf_lpoly_inter :: "('f, 'a) lpoly_inter ⇒ bool"
where
"wf_lpoly_inter pi ≡
(∀ fn. fst (pi fn) ∈ carrier R ∧ (∀ a. a ∈ set (snd (pi fn)) ⟶ a ∈ carrier R ∧ a ≽ 𝟬)) ∧
(∀ fn. arc_pos (fst (pi fn)) ∨ (∃ a ∈ set (take (snd fn) (snd (pi fn))). arc_pos a))"
end
locale linear_poly_order =
lpoly_order R for R :: "('a :: show) lpoly_order_semiring" (structure) +
fixes pi :: "('f :: {show, key}, 'a) lpoly_inter"
assumes wf_pi: "wf_lpoly_inter pi"
begin
lemma wf_terms [simp]:
assumes wf_ass: "wf_ass R α"
shows "(pi«α, t>>) ∈ carrier R"
proof (induct t)
case (Var x)
from wf_ass have "α x ∈ carrier R" unfolding wf_ass_def by auto
thus ?case by auto
next
case (Fun f ts)
show ?case
proof (cases "pi (f,length ts)")
case (Pair a as)
have "list_sum R (map (λat. fst at ⊗ (pi«α,snd at>>)) (zip as ts)) ∈ carrier R" (is "?ls ∈ _")
proof (rule wf_list_sum, rule)
fix p
assume "p ∈ set (map (λat. fst at ⊗ (pi«α,snd at>>)) (zip as ts))" (is "p ∈ set (map _ ?zip)")
from this obtain a' t where p: "p = a' ⊗ (pi«α,t>>)" and ab: "(a',t) ∈ set ?zip" by auto
from ab have a': "a' ∈ set as" and t: "t ∈ set ts" using set_zip_leftD[where x = a' and y = t] set_zip_rightD[where y = t and x = a'] by auto
from a' Pair have "a' ∈ set (snd (pi (f,length ts)))" by auto
with Fun wf_pi have "a' ∈ carrier R" by auto
with Fun t p show "p ∈ carrier R" by auto
qed
from wf_pi have "fst (pi (f,length ts)) ∈ carrier R" by auto
with Pair ‹?ls ∈ carrier R› have "(a ⊕ ?ls) ∈ carrier R" by auto
thus ?thesis using Pair by (auto simp: wf_max0)
qed
qed
lemma pos_term [simp]:
assumes wf_ass: "wf_ass R α"
and pos_ass: "pos_ass α"
shows "(pi«α, t>>) ≽ 𝟬"
proof (induct t)
case (Var x)
from wf_ass pos_ass have "α x ∈ carrier R ∧ α x ≽ 𝟬" unfolding wf_ass_def pos_ass_def by auto
thus ?case by auto
next
case (Fun f ts)
show ?case
proof (cases "pi (f,length ts)")
case (Pair a as)
have "list_sum R (map (λat. fst at ⊗ (pi«α,snd at>>)) (zip as ts)) ∈ carrier R" (is "?ls ∈ _")
proof (rule wf_list_sum, rule)
fix p
assume "p ∈ set (map (λat. fst at ⊗ (pi«α,snd at>>)) (zip as ts))" (is "p ∈ set (map _ ?zip)")
from this obtain a' t where p: "p = a' ⊗ (pi«α,t>>)" and ab: "(a',t) ∈ set ?zip" by auto
from ab have a': "a' ∈ set as" and t: "t ∈ set ts" using set_zip_leftD[where x = a' and y = t] set_zip_rightD[where y = t and x = a'] by auto
from a' Pair have "a' ∈ set (snd (pi (f,length ts)))" by auto
with Fun wf_pi have "a' ∈ carrier R" by auto
with Fun t p wf_ass wf_pi show "p ∈ carrier R" by auto
qed
from wf_pi have "fst (pi (f,length ts)) ∈ carrier R" by auto
with Pair ‹?ls ∈ carrier R› have "a ⊕ ?ls ∈ carrier R" by auto
thus ?thesis using Pair by (auto simp: wf_max0 max_ge)
qed
qed
definition apos_ass :: "('v, 'a) p_ass ⇒ bool"
where
"apos_ass α ⟷ (∀ x. arc_pos (α x))"
lemma apos_term [simp]:
assumes wf_ass: "wf_ass R α"
and apos_ass: "apos_ass α"
shows "arc_pos (pi«α, t>>)"
proof (induct t)
case (Var x)
from apos_ass show ?case unfolding apos_ass_def by auto
next
case (Fun f ts)
show ?case
proof (cases "pi (f,length ts)")
case (Pair a as)
have wf_args: "set (map (λat. fst at ⊗ (pi«α,snd at>>)) (zip as ts)) ⊆ carrier R"
proof
fix p
assume "p ∈ set (map (λat. fst at ⊗ (pi«α,snd at>>)) (zip as ts))" (is "p ∈ set (map _ ?zip)")
from this obtain a' t where p: "p = a' ⊗ (pi«α,t>>)" and ab: "(a',t) ∈ set ?zip" by auto
from ab have a': "a' ∈ set as" and t: "t ∈ set ts" using set_zip_leftD[where x = a' and y = t] set_zip_rightD[where y = t and x = a'] by auto
from a' Pair have "a' ∈ set (snd (pi (f,length ts)))" by auto
with Fun wf_pi have "a' ∈ carrier R" by auto
with Fun t p wf_ass wf_pi show "p ∈ carrier R" by auto
qed
have "list_sum R (map (λat. fst at ⊗ (pi«α,snd at>>)) (zip as ts)) ∈ carrier R" (is "?ls ∈ _")
by (rule wf_list_sum, rule wf_args)
from wf_pi have "fst (pi (f,length ts)) ∈ carrier R" by auto
with Pair have wf_a: "a ∈ carrier R" by auto
with wf_pi have "arc_pos (fst (pi (f,length ts))) ∨ (∃ a ∈ set (take (length ts) (snd (pi (f,length ts)))). arc_pos a)" (is "?ac ∨ ?aa") by auto
thus ?thesis
proof
assume "?ac"
hence "arc_pos (a ⊕ ?ls)" and "(a ⊕ ?ls) ∈ carrier R" using Pair ‹?ls ∈ carrier R› wf_a arc_pos_plus by auto
thus ?thesis using Pair by auto
next
assume ?aa
from this obtain c where c: "c ∈ set (take (length ts) as) ∧ arc_pos c" using Pair by auto
from wf_pi have "(∀ b ∈ set (snd (pi (f,length ts))). b ∈ carrier R)" by auto
with Pair have wf_as: "∀ b ∈ set as. b ∈ carrier R" by auto
from Pair Fun have rec: "∀ t ∈ set ts. arc_pos (pi«α,t>>)" by auto
from c wf_as rec wf_args have aa: "arc_pos ?ls"
proof (induct ts arbitrary: as)
case (Cons t ts) note oCons = this
show ?case
proof (cases as)
case Nil
with Cons show ?thesis by auto
next
case (Cons b bs)
let ?prod = "b ⊗ (pi«α,t>>)"
have wf: "(pi«α,t>>) ∈ carrier R ∧ b ∈ carrier R ∧ ?prod ∈ carrier R" using wf_ass Cons oCons by auto
hence wf_p: "?prod ∈ carrier R" by auto
show ?thesis
proof (cases "b = c")
case True
show ?thesis
by (simp add: Cons, rule arc_pos_plus[OF arc_pos_mult wf_p], simp add: True c, insert wf Cons oCons, auto)
next
case False
with Cons oCons have "c ∈ set (take (length ts) bs)" by auto
with Cons oCons have ap: "arc_pos (list_sum R (map (λ at. fst at ⊗ (pi«α,snd at>>)) (zip bs ts)))" (is "arc_pos ?ls") by auto
with Cons oCons have "?ls ∈ carrier R" by auto
show ?thesis
by (simp add: Cons, simp only: a_comm[OF ‹?prod ∈ carrier R› ‹?ls ∈ carrier R›], rule arc_pos_plus[OF ap], insert Cons oCons wf, auto)
qed
qed
qed simp
have "a ⊕ ?ls = ?ls ⊕ a" using wf_a ‹?ls ∈ carrier R› by (rule a_comm)
hence "arc_pos (a ⊕ ?ls)" and "a ⊕ ?ls ∈ carrier R" using aa ‹?ls ∈ carrier R› wf_a arc_pos_plus by auto
thus ?thesis using Pair by auto
qed
qed
qed
definition inter_s :: "('f, 'v) trs"
where
"inter_s = {(s, t). (∀ α. wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α, s>>) ≻ (pi«α, t>>))}"
definition inter_ns :: "('f, 'v) trs"
where
"inter_ns = {(s, t). (∀ α. wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α, s>>) ≽ (pi«α, t>>))}"
definition default_ass :: "('v, 'a) p_ass"
where
"default_ass = (λ x. default R)"
lemma wf_pos_apos_default_ass [simp]:
"wf_ass R default_ass ∧ pos_ass default_ass ∧ apos_ass default_ass"
unfolding wf_ass_def pos_ass_def apos_ass_def default_ass_def
by auto
lemma interpr_subst:
assumes wf_ass: "wf_ass R α"
shows "(pi«α, t ⋅ σ>>) = (pi«(λ x. (pi«α, σ x>>)),t>>)"
proof -
have "(pi«α, t ⋅ σ>>) = (pi«(λ x. (pi«α, σ x>>)),t>>)" (is "_ = (pi«?B, t>>)")
proof (induct t)
case (Fun f ss)
let ?ts = "map (λ s. s ⋅ σ) ss"
have wf_assB: "wf_ass R ?B" unfolding wf_ass_def using wf_ass wf_pi by auto
have map: "(map (eval_term pi α) (?ts))
= (map (eval_term pi ?B) ss)" using Fun by (induct ss, auto)
let ?i = "pi (f, length ss)"
show ?case
proof (cases "?i")
case (Pair c cs)
from wf_pi have "∀ d ∈ set (snd ?i). d ∈ carrier R" by auto
with Pair have wf_i: "∀ d ∈ set cs. d ∈ carrier R" by auto
from wf_i map have "map (λat. fst at ⊗ (pi«α,snd at>>)) (zip cs (map (λt. t ⋅ σ) ss)) =
map (λat. fst at ⊗ (pi«λx. (pi«α, σ x>>),snd at>>)) (zip cs ss)"
proof (induct cs arbitrary: ss)
case (Cons c cs) note oCons = this
thus ?case
proof (cases ss, simp)
case (Cons s sss)
with oCons show ?thesis by auto
qed
qed simp
with Pair show ?thesis by auto
qed
qed auto
thus ?thesis by simp
qed
end
context linear_poly_order
begin
lemma wf_list_sum_lpoly:
assumes "∀ p ∈ set ps. wf_lpoly R p"
shows "wf_lpoly R (list_sum_lpoly R ps)"
using wf_list_sum_lpoly[of ps] assms by auto
lemma pos_list_sum_lpoly:
assumes "∀ p ∈ set ps. wf_lpoly R p"
and "∀ p ∈ set ps. pos_coeffs p"
shows "pos_coeffs (list_sum_lpoly R ps)"
using assms
proof (induct ps)
case Nil thus ?case by (simp add: pos_coeffs_def pos_pvars_def)
next
case (Cons p ps)
show ?case
by (simp only: list_prod.simps monoid.simps, rule pos_sum_lpoly, auto simp: Cons, rule wf_list_sum_lpoly, auto simp: Cons)
qed
lemma list_sum_lpoly_sound:
assumes wf_ps: "∀ p ∈ set ps. wf_lpoly R p"
and wf_ass: "wf_ass R α"
shows "eval_lpoly α (list_sum_lpoly R ps) = list_sum R (map (eval_lpoly α) ps)"
using wf_ps
proof (induct ps)
case (Cons p ps)
have "eval_lpoly α (list_sum_lpoly R (p # ps)) = eval_lpoly α (sum_lpoly R p (list_sum_lpoly R ps))" by auto
also have "… = eval_lpoly α p ⊕ eval_lpoly α (list_sum_lpoly R ps)"
by (rule sum_poly_sound, rule wf_ass, simp add: Cons, rule wf_list_sum_lpoly, auto simp: Cons)
also have "… = eval_lpoly α p ⊕ list_sum R (map (eval_lpoly α) ps)" using Cons by auto
finally show ?case by (auto simp: Cons wf_ass)
qed simp
abbreviation Pleft :: "('f, 'v) term ⇒ ('v, 'a) l_poly"
where "Pleft ≡ PleftI R pi"
abbreviation Pright :: "('f, 'v) term ⇒ ('v, 'a) l_poly"
where "Pright ≡ PrightI R pi"
lemma Pleft_both:
assumes wf_ass: "wf_ass R α"
and pos_ass: "pos_ass α"
shows "((pi«α,t>>) ≽ eval_lpoly α (Pleft t)) ∧ wf_lpoly R (Pleft t)"
proof (induct t)
case (Var x)
from wf_ass[unfolded wf_ass_def] have wfx: "α x ∈ carrier R" by auto
hence "?case = (α x ≽ α x)" by (auto simp: wf_pvars_def)
also have "…" using wfx by auto
finally show ?case .
next
case (Fun f ts)
let ?I = "λ s. pi«α,s>>"
let ?E = "λ p. eval_lpoly α p"
show ?case
proof (cases "pi (f,length ts)")
case (Pair c cs)
from wf_pi have "fst (pi (f,length ts)) ∈ carrier R ∧ (∀ c ∈ set (snd (pi (f,length ts))). c ∈ carrier R ∧ c ≽ 𝟬)" by auto
with Pair have wf_c: "c ∈ carrier R" and wf_cs: "∀ c ∈ set cs. c ∈ carrier R" and pos_cs: "∀ c ∈ set cs. c ≽ 𝟬" by auto
let ?plist = "map (λ at. mul_lpoly R (fst at) (Pleft (snd at))) (zip cs ts)"
have wf_ps: "∀ p ∈ set ?plist. wf_lpoly R p"
proof
fix p
assume "p ∈ set ?plist"
from this obtain a t where p: "p = mul_lpoly R a (Pleft t)" and at: "(a,t) ∈ set (zip cs ts)" by auto
from at have a: "a ∈ set cs" and t: "t ∈ set ts" using set_zip_leftD[where x = a and y = t] set_zip_rightD[where x = a and y = t] by auto
show "wf_lpoly R p" by (simp only: p, rule wf_mul_lpoly, auto simp: wf_cs a t Fun)
qed
have wf_sum: "wf_lpoly R (list_sum_lpoly R ?plist)"
by (rule wf_list_sum_lpoly, rule wf_ps)
have "(list_sum R (map (λ at. fst at ⊗ (?I (snd at))) (zip cs ts))) ≽ list_sum R (map ?E ?plist)" (is "list_sum R ?vlist ≽ _")
proof (simp only: o_def map_map, rule list_sum_mono)
fix ct
assume mem: "ct ∈ set (zip cs ts)"
from this obtain c t where ct: "ct = (c,t)" by force
from ct mem have c: "c ∈ set cs" and t: "t ∈ set ts" using set_zip_leftD[where x = c and y = t] set_zip_rightD[where x = c and y = t] by auto
have "((c ⊗ (?I t)) ≽ ?E (mul_lpoly R c (Pleft t))) ∧ (c ⊗ ?I t) ∈ carrier R ∧ (?E (mul_lpoly R c (Pleft t))) ∈ carrier R"
proof (rule conjI)
have id: "?E (mul_lpoly R c (Pleft t)) = c ⊗ (?E (Pleft t))" by (rule mul_poly_sound, auto simp: c wf_cs Fun t wf_ass)
show "c ⊗ (?I t) ≽ ?E (mul_lpoly R c (Pleft t))"
by (simp only: id, rule times_right_mono, auto simp: c wf_cs pos_cs t Fun wf_ass)
show "(c ⊗ (?I t)) ∈ carrier R ∧ (?E (mul_lpoly R c (Pleft t))) ∈ carrier R"
by (rule conjI, rule m_closed, auto simp: c wf_cs wf_ass, rule wf_eval_lpoly, auto simp: wf_ass t Fun, rule wf_mul_lpoly, auto simp: c wf_cs t Fun)
qed
with ct show " (fst ct ⊗ (pi«α,snd ct>>) ≽ eval_lpoly α (mul_lpoly R (fst ct) (Pleft (snd ct)))) ∧ (fst ct ⊗ (pi«α,snd ct>>)) ∈ carrier R ∧ (eval_lpoly α (mul_lpoly R (fst ct) (Pleft (snd ct)))) ∈ carrier R" by simp
qed
also have "… = ?E (list_sum_lpoly R ?plist)" by (rule list_sum_lpoly_sound[symmetric], rule wf_ps, rule wf_ass)
finally have part1: "list_sum R ?vlist ≽ ?E (list_sum_lpoly R ?plist)" .
have wf_csump: "wf_lpoly R (sum_lpoly R (c_lpoly c) (list_sum_lpoly R ?plist))" (is "wf_lpoly R ?csump")
by (rule wf_sum_lpoly, auto simp: wf_c wf_pvars_def, rule wf_sum)
from Pair Fun have id: "Pleft (Fun f ts) = (case ?csump of LPoly d [] ⇒ LPoly (Max 𝟬 d) [] | p ⇒ p)" by auto
from wf_csump have wf_final: "wf_lpoly R (Pleft (Fun f ts))" by (simp only: id, cases ?csump, cases "get_nc_lpoly ?csump", auto simp: wf_pvars_def)
have "?E ?csump = ?E (c_lpoly c) ⊕ ?E (list_sum_lpoly R ?plist)" by (rule sum_poly_sound, auto simp: wf_ass wf_c wf_pvars_def wf_sum)
also have "… = c ⊕ ?E (list_sum_lpoly R ?plist)" by (simp add: wf_c)
finally have idr: "?E ?csump = c ⊕ ?E (list_sum_lpoly R ?plist)" .
have wf_suml: "list_sum R ?vlist ∈ carrier R"
proof (rule wf_list_sum, rule)
fix v
assume "v ∈ set ?vlist"
from this obtain c t where v: "v = c ⊗ (?I t)" and ct: "(c,t) ∈ set (zip cs ts)" by auto
from ct have c: "c ∈ set cs" and t: "t ∈ set ts" using set_zip_leftD[where x = c and y = t] set_zip_rightD[where x = c and y = t] by auto
show "v ∈ carrier R" by (simp only: v, insert wf_cs c wf_ass, auto)
qed
have ge_csum: "c ⊕ list_sum R ?vlist ≽ ?E ?csump"
by (simp only: idr, rule plus_right_mono, rule part1, rule wf_c, rule wf_suml,
rule wf_eval_lpoly, rule wf_ass, rule wf_sum)
have wf_csuml: "c ⊕ list_sum R ?vlist ∈ carrier R" using wf_suml wf_c by auto
from Pair have left: "?I (Fun f ts) = Max 𝟬 ( c ⊕ list_sum R ?vlist)" by auto
have "… ≽ Max 𝟬 ( ?E ?csump)"
by (rule max_mono, rule ge_csum, rule wf_csuml, rule wf_eval_lpoly, rule wf_ass, rule wf_csump, auto)
hence part2: "?I (Fun f ts) ≽ Max 𝟬 ( ?E ?csump)" by (simp only: left)
have part3: "Max 𝟬 ( ?E ?csump) ≽ ?E (Pleft (Fun f ts))"
using wf_csump by (simp only: id, cases ?csump, cases "get_nc_lpoly ?csump", auto simp: max_ge_right wf_ass)
have ge_final: "?I (Fun f ts) ≽ ?E (Pleft (Fun f ts))"
by (rule geq_trans, rule part2, rule part3, rule wf_terms, rule wf_ass, rule wf_max0,
rule wf_eval_lpoly, rule wf_ass, rule wf_csump, rule wf_eval_lpoly, rule wf_ass, rule wf_final)
from wf_final ge_final show ?thesis by auto
qed
qed
lemma Pleft_sound: assumes wf_ass: "wf_ass R α"
and pos_ass: "pos_ass α"
shows "(pi«α,t>>) ≽ eval_lpoly α (Pleft t)"
using Pleft_both assms by auto
lemma wf_Pleft[simp]: "wf_lpoly R (Pleft t)"
using Pleft_both[where α = zero_ass] by auto
lemma pos_eval_pvars: assumes wf_ass: "wf_ass R α"
and pos_ass: "pos_ass α"
and wf_vas: "wf_pvars R vas"
and pos_vas: "pos_pvars vas"
shows "eval_pvars α vas ≽ 𝟬"
using wf_vas pos_vas
proof (induct vas)
case (Cons xa vas)
show ?case
proof (cases xa)
case (Pair x a)
from pos_ass wf_ass have pos_x: "α x ≽ 𝟬" and wf_x: "α x ∈ carrier R" unfolding pos_ass_def wf_ass_def by auto
from Pair Cons have pos_a: "a ≽ 𝟬" and wf_a: "a ∈ carrier R" unfolding wf_pvars_def pos_pvars_def by auto
have "a ⊗ α x ≽ 𝟬 ⊗ 𝟬" by (rule geq_trans[where y = "a ⊗ 𝟬"], rule times_right_mono, auto simp: wf_a pos_a wf_x pos_x)
hence pos_ax: "a ⊗ α x ≽ 𝟬" by auto
have wf_ax: "a ⊗ α x ∈ carrier R" by (auto simp: wf_x wf_a)
from Cons have pos_rec: "eval_pvars α vas ≽ 𝟬" unfolding wf_pvars_def pos_pvars_def by auto
from Cons have "wf_pvars R vas" unfolding wf_pvars_def by auto
with Cons have wf_rec: "eval_pvars α vas ∈ carrier R" using wf_ass by auto
have "a ⊗ α x ⊕ eval_pvars α vas ≽ 𝟬 ⊕ 𝟬" by (rule plus_left_right_mono, auto simp: pos_ax wf_ax pos_rec wf_rec)
thus ?thesis by (simp add: Pair)
qed
qed simp
lemma Pright_both: assumes wf_ass: "wf_ass R α"
and pos_ass: "pos_ass α"
shows "(eval_lpoly α (Pright t) ≽ (pi«α,t>>)) ∧ wf_lpoly R (Pright t) ∧ pos_coeffs (Pright t)"
proof (induct t)
case (Var x)
from wf_ass[unfolded wf_ass_def] have wfx: "α x ∈ carrier R" by auto
hence "?case = (α x ≽ α x)" by (auto simp: wf_pvars_def pos_coeffs_def pos_pvars_def)
also have "…" using wfx by auto
finally show ?case .
next
case (Fun f ts)
let ?I = "λ s. pi«α,s>>"
let ?E = "λ p. eval_lpoly α p"
show ?case
proof (cases "pi (f,length ts)")
case (Pair c cs)
from wf_pi have "fst (pi (f,length ts)) ∈ carrier R ∧ (∀ c ∈ set (snd (pi (f,length ts))). c ∈ carrier R ∧ c ≽ 𝟬)" by auto
with Pair have wf_c: "c ∈ carrier R" and wf_cs: "∀ c ∈ set cs. c ∈ carrier R" and pos_cs: "∀ c ∈ set cs. c ≽ 𝟬" by auto
let ?plist = "map (λ at. mul_lpoly R (fst at) (Pright (snd at))) (zip cs ts)"
have wf_ps: "∀ p ∈ set ?plist. wf_lpoly R p"
proof
fix p
assume "p ∈ set ?plist"
from this obtain a t where p: "p = mul_lpoly R a (Pright t)" and at: "(a,t) ∈ set (zip cs ts)" by auto
from at have a: "a ∈ set cs" and t: "t ∈ set ts" using set_zip_leftD[where x = a and y = t] set_zip_rightD[where x = a and y = t] by auto
show "wf_lpoly R p" by (simp only: p, rule wf_mul_lpoly, auto simp: wf_cs a t Fun)
qed
have wf_sum: "wf_lpoly R (list_sum_lpoly R ?plist)"
by (rule wf_list_sum_lpoly, rule wf_ps)
have pos_ps: "∀ p ∈ set ?plist. pos_coeffs p"
proof
fix p
assume "p ∈ set ?plist"
from this obtain a t where p: "p = mul_lpoly R a (Pright t)" and at: "(a,t) ∈ set (zip cs ts)" by auto
from at have a: "a ∈ set cs" and t: "t ∈ set ts" using set_zip_leftD[where x = a and y = t] set_zip_rightD[where x = a and y = t] by auto
show "pos_coeffs p" by (simp only: p, rule pos_mul_lpoly, auto simp: a pos_cs wf_cs t Fun)
qed
have pos_sum: "pos_coeffs (list_sum_lpoly R ?plist)"
by (rule pos_list_sum_lpoly, rule wf_ps, rule pos_ps)
have id1: "?E (list_sum_lpoly R ?plist) = list_sum R (map ?E ?plist)" by (rule list_sum_lpoly_sound, rule wf_ps, rule wf_ass)
have "… ≽ (list_sum R (map (λ at. fst at ⊗ (?I (snd at))) (zip cs ts)))" (is "_ ≽ (list_sum R ?vlist)")
proof (simp only: o_def map_map, rule list_sum_mono)
fix ct
assume mem: "ct ∈ set (zip cs ts)"
from this obtain c t where ct: "ct = (c,t)" by force
from ct mem have c: "c ∈ set cs" and t: "t ∈ set ts" using set_zip_leftD[where x = c and y = t] set_zip_rightD[where x = c and y = t] by auto
have "(?E (mul_lpoly R c (Pright t)) ≽ (c ⊗ (?I t))) ∧ c ⊗ ?I t ∈ carrier R ∧ ?E (mul_lpoly R c (Pright t)) ∈ carrier R"
proof (rule conjI)
have id: "?E (mul_lpoly R c (Pright t)) = c ⊗ (?E (Pright t))" by (rule mul_poly_sound, auto simp: c wf_cs Fun t wf_ass)
show "?E (mul_lpoly R c (Pright t)) ≽ c ⊗ (?I t)"
by (simp only: id, rule times_right_mono[OF _ _ _ wf_eval_lpoly], auto simp: c wf_cs Fun[OF t] pos_cs wf_ass)
next
show "c ⊗ (?I t) ∈ carrier R ∧ ?E (mul_lpoly R c (Pright t)) ∈ carrier R"
by (rule conjI[OF m_closed wf_eval_lpoly[OF _ wf_mul_lpoly]], auto simp: c wf_cs wf_ass Fun[OF t])
qed
with ct show " (eval_lpoly α (mul_lpoly R (fst ct) (Pright (snd ct))) ≽ fst ct ⊗ (pi«α,snd ct>>)) ∧ eval_lpoly α (mul_lpoly R (fst ct) (Pright (snd ct))) ∈ carrier R ∧ fst ct ⊗ (pi«α,snd ct>>) ∈ carrier R" by simp
qed
hence part1: "?E (list_sum_lpoly R ?plist) ≽ list_sum R ?vlist" by (simp only: id1)
have wf_csump: "wf_lpoly R (sum_lpoly R (c_lpoly c) (list_sum_lpoly R ?plist))" (is "wf_lpoly R ?csump")
by (rule wf_sum_lpoly[OF _ wf_sum], auto simp: wf_c wf_pvars_def)
have pos_csump: "pos_coeffs ?csump"
by (rule pos_sum_lpoly, auto simp: wf_sum wf_c pos_sum, auto simp: wf_c wf_pvars_def pos_coeffs_def pos_pvars_def)
from Pair Fun have id: "Pright (Fun f ts) = (case ?csump of LPoly d nc ⇒ LPoly (Max 𝟬 d) nc)" by auto
from wf_csump have wf_final: "wf_lpoly R (Pright (Fun f ts))" by (simp only: id, cases ?csump, auto simp: wf_pvars_def wf_max0)
from pos_csump have pos_final: "pos_coeffs (Pright (Fun f ts))" unfolding pos_coeffs_def by (simp only: id, cases ?csump, auto)
have "?E ?csump = ?E (c_lpoly c) ⊕ ?E (list_sum_lpoly R ?plist)" by (rule sum_poly_sound, auto simp: wf_ass wf_c wf_pvars_def wf_sum)
also have "… = c ⊕ ?E (list_sum_lpoly R ?plist)" by (simp add: wf_c)
finally have idr: "?E ?csump = c ⊕ ?E (list_sum_lpoly R ?plist)" .
have wf_sumr: "list_sum R ?vlist ∈ carrier R"
proof (rule wf_list_sum, rule)
fix v
assume "v ∈ set ?vlist"
from this obtain c t where v: "v = c ⊗ (?I t)" and ct: "(c,t) ∈ set (zip cs ts)" by auto
from ct have c: "c ∈ set cs" and t: "t ∈ set ts" using set_zip_leftD[where x = c and y = t] set_zip_rightD[where x = c and y = t] by auto
show "v ∈ carrier R" by (simp only: v, rule m_closed, auto simp: wf_cs c wf_ass)
qed
have ge_csum: "?E ?csump ≽ c ⊕ list_sum R ?vlist"
by (simp only: idr, rule plus_right_mono, rule part1, rule wf_c,
rule wf_eval_lpoly, rule wf_ass, rule wf_sum, rule wf_sumr)
have wf_csuml: "c ⊕ list_sum R ?vlist ∈ carrier R" using wf_sumr wf_c by auto
from Pair have right: "?I (Fun f ts) = Max 𝟬 ( c ⊕ list_sum R ?vlist)" by auto
have "Max 𝟬 ( ?E ?csump) ≽ …"
by (rule max_mono, rule ge_csum, rule wf_eval_lpoly, rule wf_ass, rule wf_csump, rule wf_csuml, auto)
hence part2: "Max 𝟬 ( ?E ?csump) ≽ ?I (Fun f ts)" by (simp only: right)
have part3: "?E (Pright (Fun f ts)) ≽ Max 𝟬 (?E ?csump)"
proof (cases ?csump)
case (LPoly d nc)
have wf_nc: "wf_pvars R nc" using wf_csump LPoly by (simp only: id, auto)
have wf_enc: "eval_pvars α nc ∈ carrier R" using wf_csump LPoly by (simp only: id, auto simp: wf_ass)
have wf_d: "d ∈ carrier R" using wf_csump LPoly by (simp only: id, auto)
have pos_nc: "pos_pvars nc" using pos_csump LPoly unfolding pos_coeffs_def by (simp only: id, auto)
have nc_pos: "eval_pvars α nc ≽ 𝟬" by (rule pos_eval_pvars, auto simp: wf_ass pos_ass pos_nc wf_nc)
have md_pos: "Max 𝟬 d ≽ 𝟬" by (rule max_ge, insert wf_d, auto)
have "Max 𝟬 d ⊕ eval_pvars α nc ≽ 𝟬 ⊕ 𝟬" (is "?pr ≽ _") by (rule plus_left_right_mono, rule md_pos, rule nc_pos, auto simp: wf_enc wf_d wf_max0)
hence "?pr ≽ 𝟬" by simp
hence max_id: "Max 𝟬 ?pr = ?pr" by (rule max0_id_pos, auto simp: wf_enc wf_d wf_max0)
have "?pr ≽ Max 𝟬 (d ⊕ eval_pvars α nc)"
proof (rule geq_trans[where ?y = "Max 𝟬 (?pr)"], simp only: max_id, rule geq_refl)
show "Max 𝟬 ?pr ≽ Max 𝟬 (d ⊕ eval_pvars α nc)"
by (rule max_mono[OF plus_left_mono[OF max_ge_right]], auto simp: wf_d wf_max0 wf_enc)
qed (auto simp: wf_d wf_max0 wf_enc)
thus ?thesis by (simp only: id, simp only: LPoly, simp)
qed
have ge_final: "?E (Pright (Fun f ts)) ≽ ?I (Fun f ts)"
by (rule geq_trans, rule part3, rule part2, rule wf_eval_lpoly, rule wf_ass, rule wf_final, rule wf_max0,
rule wf_eval_lpoly, rule wf_ass, rule wf_csump, rule wf_terms, rule wf_ass)
from wf_final ge_final pos_final show ?thesis by auto
qed
qed
lemma Pright_sound:
assumes wf_ass: "wf_ass R α"
and pos_ass: "pos_ass α"
shows "eval_lpoly α (Pright t) ≽ (pi«α,t>>)"
using Pright_both assms by auto
lemma wf_Pright[simp]:
"wf_lpoly R (Pright t)"
using Pright_both[where α = zero_ass] by auto
end
definition create_arity :: "('f, 'a) lpoly_interL ⇒ nat" where
"create_arity fcns = Suc (max_list (map (snd o fst) fcns))"
lemma replicate_prop:
assumes "x ∈ P"
shows "set (replicate n x) ⊆ P"
using assms by (induct n) simp_all
lemma replicate_prop_elem:
assumes "P x"
shows "y ∈ set (replicate n x) ⟹ P y"
using assms by (induct n) auto
context lpoly_order
begin
lemma create_arity_sound:
assumes m: "m ≥ create_arity I"
shows "to_lpoly_inter R I (f, m) = (default R, replicate m 𝟭)" (is "?I (f, m) = _")
proof (cases "map_of I (f, m)")
case None thus ?thesis by (auto simp: to_lpoly_inter_def)
next
case (Some val)
hence one: "((f,m),val) ∈ set I" by (rule map_of_SomeD)
hence "m ∈ set (map (snd o fst) I)" unfolding o_def by force
from max_list[OF this] m show ?thesis unfolding create_arity_def by auto
qed
end
context linear_poly_order
begin
lemma default_interpretation_subterm_inter_ns:
assumes pi: "pi (f, n) = (default R, replicate n 𝟭)"
and n: "n = length ts"
and t: "(t :: ('f,'v)term) ∈ set ts"
shows "(Fun f ts, t) ∈ inter_ns"
unfolding inter_ns_def
proof (clarify)
fix α :: "('v,'a)p_ass"
assume wf_ass: "wf_ass R α" and pos_ass: "pos_ass α" and "apos_ass α"
let ?C = "λ c. c ∈ carrier R"
def c ≡ "default R"
note wf[simp] = wf_terms[OF wf_ass]
note pos[simp] = pos_term[OF wf_ass pos_ass]
have c0: "c ≽ 𝟬" "?C c" unfolding c_def by auto
have id: "map (λat. fst at ⊗ (pi«α,snd at>>)) (zip (replicate (length ts) 𝟭) ts) =
map (λ t. pi«α,t>>) ts"
by (rule nth_equalityI, auto simp: l_one[OF wf])
let ?e = "Max 𝟬 (c ⊕ list_sum R (map (λat. fst at ⊗ (pi«α,snd at>>)) (zip (replicate (length ts) 𝟭) ts))) ≻
(pi«α,t>>)"
show "(pi«α,Fun f ts>>) ≽ (pi«α,t>>)"
unfolding eval_termI.simps pi[unfolded n] split Let_def c_def[symmetric] id
using c0 t
proof (induct ts arbitrary: c t)
case (Cons t ts c s)
note c = Cons(3)
let ?sum' = "λ ts. list_sum R (map (eval_term pi α) ts)"
let ?sum = "?sum' ts"
have Csum: "⋀ ts. ?C (?sum' ts)" by auto
hence id: "c ⊕ ((pi«α,t>>) ⊕ ?sum) =
c ⊕ (pi«α,t>>) ⊕ ?sum" using c wf[of t] by algebra
from plus_left_right_mono[OF Cons(2) pos[of t] c] c
have ge: "c ⊕ (pi«α,t>>) ≽ 𝟬" "?C (c ⊕ (pi«α,t>>))" by auto
show ?case
proof (cases "s = t")
case False
hence s: "s ∈ set ts" using Cons by auto
from Cons(1)[OF ge s]
show ?thesis by (simp add: id)
next
case True
have "c ⊕ (pi«α,t>>) ⊕ ?sum ≽ c ⊕ (pi«α,t>>) ⊕ 𝟬"
proof (rule plus_right_mono, induct ts)
case (Cons t ts)
from plus_left_right_mono[OF pos[of t] Cons wf _ Csum]
show ?case by simp
qed (insert c, auto)
with c have ge1: "c ⊕ (pi«α,t>>) ⊕ ?sum ≽ c ⊕ (pi«α,t>>)" by simp
from geq_trans[OF this ge(1)] Csum c have "c ⊕ (pi«α,t>>) ⊕ ?sum ≽ 𝟬" by auto
from max0_id_pos[OF this] Csum c have id2: "Max 𝟬 (c ⊕ (pi«α,t>>) ⊕ ?sum) = c ⊕ (pi«α,t>>) ⊕ ?sum" by auto
show ?thesis unfolding True
proof (simp add: id id2)
have "c ⊕ (pi«α,t>>) ≽ 𝟬 ⊕ (pi«α,t>>)"
by (rule plus_left_mono[OF geq_trans[OF Cons(2)]], insert c, auto)
thus "c ⊕ (pi«α,t>>) ⊕ ?sum ≽ (pi«α,t>>)"
by (intro geq_trans[OF ge1], insert c Csum, auto)
qed
qed
qed simp
qed
lemma inter_ns_ce_compat:
assumes pi: "pi = to_lpoly_inter R I" (is "_ = ?pi")
shows "∃ n. ∀ m. m ≥ n ⟶ (∀ c. ce_trs (c, m) ⊆ inter_ns)"
proof (rule exI[of _ "create_arity I"], intro allI impI, rule subsetI, unfold ce_trs.simps)
fix m c x
let ?n = "create_arity I"
assume m: "?n ≤ m"
let ?m = "Suc (Suc m)"
from m have "?m ≥ ?n" by auto
hence inter: "pi (c, ?m) = (default R, replicate ?m 𝟭)" by (simp only: pi, rule create_arity_sound)
assume "x ∈ {(Fun c (t # s # replicate m (Var undefined)), t)| t s. True} ∪
{(Fun c (t # s # replicate m (Var undefined)), s)| t s. True}" (is "_ ∈ ?tc ∪ ?sc")
then obtain t s u where x: "x = (Fun c (t # s # replicate m (Var undefined)), u)"
and u: "u = t ∨ u = s" by auto
show "x ∈ inter_ns" unfolding x
by (rule default_interpretation_subterm_inter_ns[OF inter], insert u, auto)
qed
lemma inter_s_subset_inter_ns: "inter_s ⊆ inter_ns"
unfolding inter_s_def inter_ns_def using gt_imp_ge wf_terms by auto
lemma create_af_sound:
assumes not: "i ∉ create_af R I fn"
shows "length (snd (to_lpoly_inter R I fn)) ≤ i ∨ (snd (to_lpoly_inter R I fn)) ! i = 𝟬"
(is "?len ∨ ?zero")
proof -
obtain f n where fn: "fn = (f,n)" by force
note not = not[unfolded create_af_def fn]
show ?thesis
proof (cases "map_of I (f,n)")
case (Some cc)
obtain c coeffs where cc: "cc = (c,coeffs)" by force
note look = Some[unfolded cc]
from not look Some have
i: "i ∉ set ([ i . (c,i) <- zip coeffs [0 ..< length coeffs], c ≠ 𝟬])" (is "_ ∉ ?set") by auto
have "length coeffs ≤ i ∨ coeffs ! i = 𝟬"
proof (rule ccontr)
assume "¬ ?thesis"
hence ii: "i < length coeffs" and c: "coeffs ! i ≠ 𝟬" by auto
hence "i ∈ ?set" by (force simp: set_zip)
with i show False by blast
qed
thus ?thesis unfolding fn by (simp add: look to_lpoly_inter_def)
next
case None
with not have i: "i ≥ n" by auto
thus ?thesis unfolding fn
by (auto simp: to_lpoly_inter_def None)
qed
qed
lemma inter_ns_af_compat:
assumes pi: "pi = to_lpoly_inter R I" (is "_ = ?pi")
shows "af_compatible (create_af R I) inter_ns"
proof (unfold af_compatible_def, intro allI)
fix f :: 'f and bef and s t :: "('f,'v)term" and aft
obtain v :: 'v where True by simp
let ?st = "Fun f (bef @ s # aft)"
let ?tt = "Fun f (bef @ t # aft)"
let ?pair = "(?st, ?tt)"
let ?n = "Suc (length bef + length aft)"
let ?i = "length bef"
show "?i ∈ create_af R I (f, ?n) ∨ ?pair ∈ inter_ns"
proof (cases "?i ∈ create_af R I (f, ?n)")
case False
hence "length (snd (?pi (f,?n))) ≤ ?i ∨ snd (?pi (f, ?n)) ! ?i = 𝟬" by (rule create_af_sound)
with pi have pi3: "length (snd (pi (f,?n))) ≤ ?i ∨ snd (pi (f,?n)) ! ?i = 𝟬" by simp
obtain c cs where pi2: "pi (f, ?n) = (c,cs)" by force
with pi3 have short_0: "length cs ≤ ?i ∨ cs ! ?i = 𝟬" by auto
have "∀ α. wf_ass R α ∧ pos_ass α ⟶ ((pi«α,?st>>) ≽ (pi«α,?tt>>))" (is "∀ α. ?wfpos α ⟶ ?rel α")
proof
fix α
show "?wfpos α ⟶ ?rel α"
proof
assume wfpos: "?wfpos α"
hence wf_ass: "wf_ass R α" ..
let ?in = "λ t :: ('f,'v) term. (pi«α,t>>)"
let ?inter = "λ s bef cs. list_sum R (map (λ at. fst at ⊗ (?in (snd at))) (zip cs (bef @ s # aft)))"
let ?intre = "λ aft cs. list_sum R (map (λ at. fst at ⊗ (?in (snd at))) (zip cs aft))"
have int_s: "?in ?st = Max 𝟬 (c ⊕ ?inter s bef cs)" by (auto simp: pi2)
have int_t: "?in ?tt = Max 𝟬 (c ⊕ ?inter t bef cs)" by (auto simp: pi2)
from short_0 have "?inter s bef cs = ?inter t bef cs"
proof (induct cs arbitrary: bef)
case (Cons c cs) note oCons = this
show ?case
proof (cases bef)
case Nil
with Cons show ?thesis by (simp add: wf_ass)
next
case (Cons b befs)
with oCons have "length cs ≤ length befs ∨ cs ! length befs = 𝟬" by auto
with Cons oCons show ?thesis by auto
qed
qed auto
with int_s int_t have eq: "?in ?st = ?in ?tt" by auto
show "?rel α" by (simp only: eq, rule geq_refl, rule wf_terms, auto simp: wf_ass)
qed
qed
hence "?pair ∈ inter_ns" unfolding inter_ns_def by auto
thus ?thesis ..
qed simp
qed
end
context lpoly_order
begin
abbreviation pi_of where "pi_of ≡ to_lpoly_inter R"
lemma check_poly_mono_npsm_sound:
assumes ok: "isOK(check_poly_mono_npsm R F I)"
shows "∀ fn ∈ set F ∪ set (map fst I). snd fn ≤ Suc 0 ∧ (snd fn = Suc 0 ⟶ fst (pi_of I fn) = 𝟬 ∧ length (snd (pi_of I fn)) = Suc 0)" (is "∀ fn ∈ set F ∪ set (map fst I). ?P fn")
proof
fix fn
assume fn: "fn ∈ set F ∪ set (map fst I)"
note ok = ok[unfolded check_poly_mono_npsm_def, simplified]
from ok[THEN conjunct2] fn obtain ccs where mem: "(fn,ccs) ∈ set I" by auto
obtain f n where fn: "fn = (f,n)" by force
from ok[THEN conjunct1, rule_format, OF mem]
have le_1: "snd fn ≤ Suc 0" unfolding fn by (cases ccs, auto)
show "?P fn"
proof (rule conjI[OF le_1], intro impI)
assume eq_1: "snd fn = Suc 0"
have "∃ ccs. map_of I fn = Some ccs"
proof (cases "map_of I fn")
case None
from None[unfolded map_of_eq_None_iff[of I fn]] mem show ?thesis by force
qed auto
then obtain c cs where look: "map_of I fn = Some (c,cs)" by force
from map_of_SomeD[OF look] have mem: "(fn, (c,cs)) ∈ set I" .
have pi: "pi_of I fn = (c,cs)" unfolding to_lpoly_inter_def look ceta_map_of fun_of_map_fun.simps Let_def by simp
note ok = ok[THEN conjunct1, rule_format, OF mem, unfolded fn split, simplified]
from ok eq_1
show "fst (pi_of I fn) = 𝟬 ∧ length (snd (pi_of I fn)) = Suc 0"
unfolding pi unfolding fn by simp
qed
qed
end
context mono_linear_poly_order_carrier
begin
lemma plus_gt_right_mono: "⟦y ≻ z; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R⟧ ⟹ x ⊕ y ≻ x ⊕ z"
by (simp add: a_comm[where x = x], rule plus_gt_left_mono, auto simp: plus_single_mono)
lemma check_poly_mono_sound:
assumes "isOK (check_poly_mono R I)"
shows "∀ f n. (fst (pi_of I (f,n)) ≽ 𝟬) ∧ (length (snd (pi_of I (f, n))) ≥ n ∧ (∀ c ∈ set (snd (pi_of I (f, n))). check_mono c ∨ c = 𝟭))" (is "∀ f n. ?prop f n")
proof (intro allI)
fix f n
note to_lpoly_inter_def[simp]
show "?prop f n"
proof (cases "map_of I (f, n)")
case None
hence id: "pi_of I (f,n) = (default R, replicate n 𝟭)" by auto
show ?thesis
by (simp only: id, rule conjI, simp, rule conjI, simp, simp)
next
case (Some ccs)
from this obtain c cs where map_of: "map_of I (f, n) = Some (c,cs)" by force
hence "((f,n),(c,cs)) ∈ set I" by (rule map_of_SomeD)
with assms[unfolded check_poly_mono_def] map_of show "?prop f n" by auto
qed
qed
end
context lpoly_order
begin
definition check_poly_strict_mono where
"check_poly_strict_mono p i ≡ fst p ≽ 𝟬 ∧ i < length (snd p) ∧ (let c = snd p ! i in check_mono c ∨ c = 𝟭)"
end
locale pre_mono_linear_poly_order = linear_poly_order R pi + mono_linear_poly_order_carrier
for pi :: "('f :: {show, key}, 'a :: show) lpoly_inter"
begin
lemma check_poly_strict_mono: assumes
mono: "check_poly_strict_mono (pi (f,Suc (length bef + length aft))) (length bef)"
and st: "(s,t) ∈ (inter_s :: ('f,'v)trs)" (is "_ ∈ ?inter_s")
shows "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ inter_s"
proof -
let ?st = "Fun f (bef @ s # aft)"
let ?tt = "Fun f (bef @ t # aft)"
let ?pair = "(?st, ?tt)"
let ?n = "Suc (length bef + length aft)"
let ?i = "length bef"
obtain c cs where ccs: "pi (f,?n) = (c,cs)" by force
from mono[unfolded this check_poly_strict_mono_def Let_def, simplified]
have c: "c ≽ 𝟬" and mono: "?i < length cs ∧ (check_mono (cs ! ?i) ∨ cs ! ?i = 𝟭)" by auto
from wf_pi have "fst (pi (f,?n)) ∈ carrier R" and "∀ d ∈ set (snd (pi (f,?n))). d ∈ carrier R ∧ d ≽ 𝟬" by auto
with ccs have wf_c: "c ∈ carrier R" and wf_cs: "∀ d ∈ set cs. d ∈ carrier R ∧ d ≽ 𝟬" by auto
show "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ ?inter_s"
unfolding inter_s_def
proof (clarify)
fix α :: "('v,'a)p_ass"
assume wf_ass: "wf_ass R α" and pos_ass: "pos_ass α" and apos_ass: "apos_ass α"
let ?in = "λ t :: ('f,'v) term. (pi«α,t>>)"
let ?inter = "λ s bef cs. list_sum R (map (λ at. fst at ⊗ (?in (snd at))) (zip cs (bef @ s # aft)))"
have int_s: "?in ?st = Max 𝟬 (c ⊕ ?inter s bef cs)" by (auto simp: ccs)
have int_t: "?in ?tt = Max 𝟬 (c ⊕ ?inter t bef cs)" by (auto simp: ccs)
from mono wf_cs have main: "?inter s bef cs ≻ ?inter t bef cs"
proof (induct cs arbitrary: bef)
case (Cons c cs) note oCons = this
hence wf_c: "c ∈ carrier R" and c_0: "c ≽ 𝟬" by auto
{
fix aft and a :: 'a and b :: "('f,'v)term"
assume "(a,b) ∈ set (zip cs aft)"
hence "a ∈ set cs" by (rule set_zip_leftD)
with Cons have "a ∈ carrier R" by auto
hence "a ⊗ ?in b ∈ carrier R" using wf_ass by auto
} note wf_zip = this
hence wf_rec: "⋀ aft. list_sum R (map (λat. fst at ⊗ (pi«α,snd at>>)) (zip cs aft)) ∈ carrier R"
by (intro wf_list_sum, auto)
show ?case
proof (cases bef)
case Nil
from st have st: "?in s ≻ ?in t" unfolding inter_s_def using wf_ass pos_ass apos_ass by auto
from Cons Nil have "check_mono c ∨ c = 𝟭" by auto
hence cst: "c ⊗ ?in s ≻ c ⊗ ?in t"
proof
assume "c = 𝟭"
with st show ?thesis by (simp add: wf_ass)
next
assume "check_mono c"
thus ?thesis
by (rule check_mono[OF _ st], auto simp: wf_ass wf_c c_0)
qed
show ?thesis
by (simp add: Nil Cons, rule plus_gt_left_mono2, rule cst,
auto simp: Cons wf_ass plus_single_mono wf_zip geq_refl[OF wf_rec])
next
case (Cons b befs)
with oCons have "Suc (length befs) ≤ length cs" by auto
with Cons oCons have rec: "?inter s befs cs ≻ ?inter t befs cs" by auto
show ?thesis by (simp add: Cons oCons, rule plus_gt_right_mono[OF rec, simplified, OF _ wf_rec wf_rec],
auto simp: wf_c wf_ass)
qed
qed auto
have wf_inter: "⋀ t. ?inter t bef cs ∈ carrier R"
proof (rule wf_list_sum, auto)
fix t a b
assume "(a,b) ∈ set (zip cs (bef @ t # aft))"
hence "a ∈ set cs" by (rule set_zip_leftD)
with wf_cs wf_ass show "(a ⊗ (?in b)) ∈ carrier R" by auto
qed
have wf_cint: "⋀ t. c ⊕ ?inter t bef cs ∈ carrier R"
by (rule a_closed, rule wf_c, rule wf_inter)
have pos_inter: "⋀ t. (?inter t bef cs) ≽ 𝟬"
proof (rule pos_list_sum, simp, clarify, simp)
fix t a b
assume "(a,b) ∈ set (zip cs (bef @ t # aft))"
hence "a ∈ set cs" by (rule set_zip_leftD)
hence pos_a: "a ≽ 𝟬" and wf_a: "a ∈ carrier R" using wf_cs by auto
show "a ⊗ (?in b) ∈ carrier R ∧ (a ⊗ (?in b) ≽ 𝟬)"
proof (rule conjI, auto simp: wf_ass wf_a)
have int: "(a ⊗ (?in b) ≽ a ⊗ 𝟬)"
by (rule times_right_mono, rule pos_a, rule pos_term, auto simp: wf_a wf_ass pos_ass)
show "(a ⊗ (?in b)) ≽ 𝟬" by (rule geq_trans[where y = "a ⊗ 𝟬"], rule int, auto simp: wf_a wf_ass)
qed
qed
have "⋀ t. c ⊕ (?inter t bef cs) ≽ 𝟬 ⊕ 𝟬"
by (rule plus_left_right_mono[OF _ pos_inter wf_c _ wf_inter], auto simp: c)
hence pos_cint: "⋀ t. c ⊕ (?inter t bef cs) ≽ 𝟬" by auto
have id_cint: "⋀ t. Max 𝟬 (c ⊕ (?inter t bef cs)) = c ⊕ (?inter t bef cs)"
by (rule max0_id_pos, rule pos_cint, rule wf_cint)
{
fix t aft and a :: 'a and b :: "('f,'v)term"
assume "(a,b) ∈ set (zip cs (bef @ t # aft))"
hence "a ∈ set cs" by (rule set_zip_leftD)
with wf_cs have "a ∈ carrier R" by auto
hence "a ⊗ ?in b ∈ carrier R" using wf_ass by auto
}
hence wf_rec: "⋀ t aft. list_sum R (map (λat. fst at ⊗ (pi«α,snd at>>)) (zip cs (bef @ t # aft))) ∈ carrier R"
by (intro wf_list_sum, auto)
show "?in ?st ≻ ?in ?tt" by (simp only: int_s int_t id_cint, rule plus_gt_right_mono, rule main, rule wf_c, (rule wf_rec)+)
qed
qed
lemma create_mono_af:
assumes pi: "pi = to_lpoly_inter R I" (is "_ = ?pi")
shows "af_monotone (create_mono_af R I) inter_s"
proof (rule af_monotoneI[OF check_poly_strict_mono])
fix f and bef aft :: "('f,'v)term list"
note d = check_poly_strict_mono_def Let_def to_lpoly_inter_def create_mono_af_def
let ?n = "Suc (length bef + length aft)"
let ?i = "length bef"
obtain n where n: "?n = n" and i: "?i < n" by auto
assume mono: "?i ∈ create_mono_af R I (f, ?n)"
show "check_poly_strict_mono (pi (f, ?n)) ?i"
proof (cases "map_of I (f,?n)")
case None
hence "pi (f, ?n) = ((default R, replicate n 𝟭))"
unfolding pi d n by simp
thus ?thesis unfolding d using i by simp
next
case (Some p)
hence pi: "pi (f,?n) = p" unfolding pi d by auto
obtain c cs where p: "p = (c,cs)" by force
from mono[unfolded d] Some
obtain c' where "c ≽ 𝟬" and "c' = 𝟭 ∨ check_mono c'" and
"(c',length bef) ∈ set (zip cs [0..<length cs])"
by (auto split: if_splits simp: empty_af_def pi p)
with i show ?thesis unfolding pi p d
by (auto simp: set_zip)
qed
qed
end
locale mono_linear_poly_order = pre_mono_linear_poly_order +
assumes pi_mono: "∀ f n. (fst (pi (f, n)) ≽ 𝟬) ∧ (length (snd (pi (f, n))) ≥ n ∧ (∀ c ∈ set (snd (pi (f, n))). check_mono c ∨ c = 𝟭))"
begin
lemma inter_s_ce_compat: assumes pi: "pi = to_lpoly_inter R I" (is "_ = ?pi")
shows "∃ n. ∀ m. m ≥ n ⟶ (∀ c. ce_trs (c, m) ⊆ inter_s)"
unfolding inter_s_def
proof (rule exI[of _ "create_arity I"], intro allI impI, rule subsetI, unfold ce_trs.simps)
fix m c x
let ?n = "create_arity I"
assume m: "?n ≤ m"
let ?m = "Suc (Suc m)"
from m have "?m ≥ ?n" by auto
hence inter: "pi (c, ?m) = (default R, replicate ?m 𝟭)" by (simp only: pi, rule create_arity_sound)
let ?sum = "λ α. list_sum R (replicate m (𝟭 ⊗ α undefined))"
{
fix α
assume alpha: "wf_ass R α ∧ pos_ass α ∧ apos_ass α"
let ?sum' = "list_sum R (replicate m (α undefined))"
have id: "?sum α = ?sum'"
by (subst l_one, insert alpha, auto simp: wf_ass_def)
have wf_sum: "?sum α ∈ carrier R" unfolding id
by (rule wf_list_sum, rule replicate_prop, insert alpha, auto simp: wf_ass_def)
have pos_sum: "?sum α ≽ 𝟬" unfolding id
by (rule pos_list_sum, insert alpha, auto simp: wf_ass_def pos_ass_def)
from wf_sum pos_sum have "∃ d. ?sum α = d ∧ d ∈ carrier R ∧ d ≽ 𝟬" by force
} note sum = this
fix x
assume "x ∈ {(Fun c (t # s # replicate m (Var undefined)), t) | t s. True} ∪
{(Fun c (t # s # replicate m (Var undefined)), s) | t s. True}" (is "_ ∈ ?tc ∪ ?sc")
thus "x ∈ {(s,t). ∀α. wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α,s>>) ≻ (pi«α,t>>)}"
proof
assume "x ∈ ?tc"
then obtain t s where id: "x = (Fun c (t # s # replicate m (Var undefined)), t)" (is "x = (?l, _)") by auto
have "∀ α. wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α,?l>>) ≻ (pi«α,t>>)"
proof (intro allI)
fix α
show "wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α,?l>>) ≻ (pi«α,t>>)" (is "?wf_pos ⟶ ?goal")
proof
assume wf_pos_ass: ?wf_pos
let ?term = "((default R ⊕ (pi«α,t>>)) ⊕ (pi«α,s>>)) ⊕ ?sum α"
from sum[OF wf_pos_ass] obtain d where id: "?sum α = d" and d: "d ∈ carrier R" "d ≽ 𝟬" by auto
have max: "Max 𝟬 ?term = ?term" unfolding id
by (rule max0_id_pos, auto simp: wf_pos_ass d, (rule sum_pos)+, auto simp: wf_pos_ass d)
have "Max 𝟬 ?term ≻ ((𝟬 ⊕ (pi«α,t>>)) ⊕ 𝟬) ⊕ 𝟬" unfolding max unfolding id
by ((rule plus_gt_left_mono2)+, auto simp: wf_pos_ass d plus_single_mono default_gt_zero)
hence "Max 𝟬 ?term ≻ (pi«α,t>>)" by (auto simp: wf_pos_ass)
with wf_pos_ass show ?goal using inter
by (auto simp: d wf_max0 a_assoc id)
qed
qed
thus ?thesis using id by simp
next
assume "x ∈ ?sc"
then obtain t s where id: "x = (Fun c (t # s # replicate m (Var undefined)), s)" (is "x = (?l, _)") by auto
have "∀ α. wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α,?l>>) ≻ (pi«α,s>>)"
proof (intro allI)
fix α
show "wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α,?l>>) ≻ (pi«α,s>>)" (is "?wf_pos ⟶ ?goal")
proof
assume wf_pos_ass: ?wf_pos
let ?term = "((default R ⊕ (pi«α,t>>)) ⊕ (pi«α,s>>)) ⊕ ?sum α"
from sum[OF wf_pos_ass] obtain d where id: "?sum α = d" and d: "d ∈ carrier R" "d ≽ 𝟬" by auto
have max: "Max 𝟬 ?term = ?term" unfolding id
by (rule max0_id_pos, auto simp: wf_pos_ass d, (rule sum_pos)+, auto simp: wf_pos_ass d)
have "Max 𝟬 ?term ≻ ((𝟬 ⊕ 𝟬) ⊕ (pi«α,s>>)) ⊕ 𝟬" unfolding max unfolding id
by ((rule plus_gt_left_mono2)+, auto simp: wf_pos_ass d plus_single_mono default_gt_zero)
hence "Max 𝟬 ?term ≻ (pi«α,s>>)" by (auto simp: wf_pos_ass)
with wf_pos_ass show ?goal using inter
by (auto simp: d wf_max0 a_assoc id)
qed
qed
thus ?thesis using id by simp
qed
qed
lemma inter_s_mono:
shows "ctxt.closed inter_s"
proof (rule one_imp_ctxt_closed[OF check_poly_strict_mono])
fix f bef s t aft
show "check_poly_strict_mono (pi (f, Suc (length bef + length aft))) (length bef)"
unfolding check_poly_strict_mono_def Let_def
using pi_mono[rule_format, of f "Suc (length bef + length aft)"]
by auto
qed
end
context linear_poly_order
begin
lemmas compat_orig = compat
end
sublocale linear_poly_order ⊆ redtriple_order inter_s inter_ns inter_ns
proof
show "SN inter_s"
proof
fix f
assume steps: "(∀ i. (f i, f (Suc i)) ∈ inter_s)"
let ?b = default_ass
have "∀ i. ((pi«?b,f i>>) ≻ (pi«?b, f (Suc i)>>)) ∧ (arc_pos (pi«?b, f (Suc i)>>))"
proof
fix i
from steps have "(f i, f (Suc i)) ∈ inter_s" ..
hence dec: "(pi«?b, f i>>) ≻ (pi«?b, f (Suc i)>>)" (is ?dec) unfolding inter_s_def
by auto
show "?dec ∧ arc_pos (pi«?b, f (Suc i)>>)" by (rule conjI, rule dec, rule apos_term, auto)
qed
from this obtain g
where nSN: "∀ i. ((g i) :: 'a) ≻ (g (Suc i)) ∧ g i ∈ carrier R ∧ g (Suc i) ∈ carrier R
∧ g (Suc i) ≽ 𝟬 ∧ arc_pos (g (Suc i))" by fastforce
with SN show False by (auto simp: SN_defs)
qed
next
show "inter_ns O inter_s ⊆ inter_s"
proof (clarify)
fix s t u :: "('f,'v)term"
assume st: "(s,t) ∈ inter_ns" and tu: "(t,u) ∈ inter_s"
show "(s,u) ∈ inter_s" unfolding inter_s_def
proof(rule, unfold split, clarify)
fix α :: "'v ⇒ 'a"
assume wf: "wf_ass R α" "pos_ass α" "apos_ass α"
show "(pi«α,s>>) ≻ (pi«α,u>>)"
by (rule compat, insert st tu wf, unfold inter_s_def inter_ns_def, auto intro: wf_terms)
qed
qed
next
show "inter_s O inter_ns ⊆ inter_s"
proof (clarify)
fix s t u :: "('f,'v)term"
assume st: "(s,t) ∈ inter_s" and tu: "(t,u) ∈ inter_ns"
show "(s,u) ∈ inter_s" unfolding inter_s_def
proof(rule, unfold split, clarify)
fix α :: "'v ⇒ 'a"
assume wf: "wf_ass R α" "pos_ass α" "apos_ass α"
show "(pi«α,s>>) ≻ (pi«α,u>>)"
by (rule compat2, insert st tu wf, unfold inter_s_def inter_ns_def, auto intro: wf_terms)
qed
qed
next
show "ctxt.closed inter_ns" unfolding inter_ns_def
proof (rule one_imp_ctxt_closed)
fix f :: 'f
and bef :: "('f,'v) term list"
and s :: "('f,'v) term"
and t :: "('f,'v) term"
and aft :: "('f,'v) term list"
let ?P = "{(s,t). ∀ α. wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α,s>>) ≽ (pi«α,t>>)}"
assume "(s, t) ∈ ?P"
hence st: "∀ α. wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α, s>>) ≽ (pi«α, t>>)" by (simp)
let ?inter = "pi (f, (Suc (length bef + length aft)))"
show "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ ?P"
proof (cases "?inter")
case (Pair c list)
have "∀ α. wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α, Fun f (bef @ s # aft)>>) ≽ (pi«α,Fun f (bef @ t # aft)>>)" (is "∀ α. ?ass α ⟶ ?ge α")
proof
fix α
show "?ass α ⟶ ?ge α"
proof
assume "?ass α"
hence wf_ass: "wf_ass R α" and pos_ass: "pos_ass α" and apos_ass: "apos_ass α" by auto
with st have sta: "(pi«α,s>>) ≽ (pi«α,t>>)" by auto
from wf_pi have "fst ?inter ∈ carrier R ∧ (∀ a. a ∈ set (snd ?inter) ⟶ a ∈ carrier R ∧ a ≽ 𝟬)" by auto
with Pair have wf_c: "c ∈ carrier R" and wf_list: "∀ a ∈ set list. a ∈ carrier R" and pos_list: "∀ a ∈ set list. a ≽ 𝟬" by auto
let ?expr = "λ list rest. list_sum R (map (λat. fst at ⊗ (pi«α,snd at>>)) (zip list rest))"
from wf_list pos_list have main: "(?expr list (bef @ s # aft) ≽ ?expr list (bef @ t # aft)) ∧ (?expr list (bef @ s # aft)) ∈ carrier R ∧ (?expr list (bef @ t # aft)) ∈ carrier R"
proof (induct list arbitrary:bef)
case (Cons a as) note oCons = this
hence wf_a: "a ∈ carrier R" and pos_a: "a ≽ 𝟬" and wf_as: "∀ a ∈ set as. a ∈ carrier R" and pos_as: "∀ a ∈ set as. a ≽ 𝟬" by auto
thus ?case
proof (cases bef)
case Nil
{
fix aas aaft
assume "(aas,aaft) ∈ set (zip as aft)"
hence "aas ∈ set as" using set_zip_leftD[where x = aas and y = aaft] by auto
with wf_as have wfaas: "aas ∈ carrier R" by auto
hence "(aas ⊗ (pi«α,aaft>>)) ∈ carrier R" by (auto simp: wf_ass wfaas)
}
hence wf_as_aft: "?expr as aft ∈ carrier R"
by (intro wf_list_sum, auto)
show ?thesis
by (rule conjI, simp add: Nil, rule plus_left_mono, rule times_right_mono,
auto simp: wf_a pos_a wf_ass Nil wf_as_aft sta)
next
case (Cons u us)
with oCons wf_as pos_as have wf_rec: "?expr as (us @ s # aft) ∈ carrier R ∧ ?expr as (us @ t # aft) ∈ carrier R" by auto
show ?thesis
by (simp add: Cons, rule conjI, rule plus_right_mono, auto simp: Cons oCons wf_ass wf_as pos_as)
qed
qed simp
show "?ge α" by (simp add: Pair, rule max_mono, rule plus_right_mono, auto simp: main wf_c)
qed
qed
thus ?thesis by auto
qed
qed
next
show "subst.closed inter_s"
proof (unfold subst.closed_def inter_s_def, rule subsetI)
fix st_sig :: "('f,'v)term × ('f,'v)term"
assume st_sig: "st_sig ∈ subst.closure {(s,t). ∀α. wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α,s>>) ≻ (pi«α,t>>) }" (is "_ ∈ subst.closure ?P")
thus "st_sig ∈ ?P"
proof (cases st_sig)
case (Pair s_sig t_sig)
with st_sig have "(s_sig, t_sig) ∈ subst.closure ?P" by simp
hence "(s_sig, t_sig) ∈ ?P"
proof induct
case (subst s t σ)
{ fix α
have "wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α, s ⋅ σ>>) ≻ (pi«α, t ⋅ σ>>)" (is "?wf ∧ ?ps ⟶ ?go")
proof -
{
assume ?wf and ?ps
have wf_assB: "wf_ass R (λx. pi«α,σ x>>)" (is "wf_ass R ?bet") unfolding wf_ass_def using ‹?wf› by auto
have pos_assB: "pos_ass ?bet" unfolding pos_ass_def using ‹?ps› ‹?wf› by auto
have apos_assB: "apos_ass ?bet" unfolding apos_ass_def using ‹?ps› ‹?wf› by auto
with Pair subst Cons wf_assB pos_assB have "(pi«?bet,s>>) ≻ (pi«?bet,t>>)" by force
with ‹?wf› have "?go" by (simp add: interpr_subst)
}
thus ?thesis by blast
qed }
then show ?case by simp
qed
with Pair show ?thesis by simp
qed
qed
next
show "subst.closed inter_ns"
proof (unfold subst.closed_def inter_ns_def, rule subsetI)
fix st_sig :: "('f,'v)term × ('f,'v)term"
assume st_sig: "st_sig ∈ subst.closure {(s,t). ∀α. wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α,s>>) ≽ (pi«α,t>>) }" (is "_ ∈ subst.closure ?P")
thus "st_sig ∈ ?P"
proof (cases st_sig)
case (Pair s_sig t_sig)
with st_sig have "(s_sig, t_sig) ∈ subst.closure ?P" by simp
hence "(s_sig, t_sig) ∈ ?P"
proof induct
case (subst s t σ)
{ fix α
have "wf_ass R α ∧ pos_ass α ∧ apos_ass α ⟶ (pi«α, s ⋅ σ>>) ≽ (pi«α, t ⋅ σ>>)" (is "?wf ∧ ?ps ⟶ ?go")
proof -
{
assume ?wf and ?ps
have wf_assB: "wf_ass R (λx. pi«α, σ x>>)" (is "wf_ass R ?bet") unfolding wf_ass_def using ‹?wf› by auto
have pos_assB: "pos_ass ?bet" unfolding pos_ass_def using ‹?ps› ‹?wf› by auto
have apos_assB: "apos_ass ?bet" unfolding apos_ass_def using ‹?ps› ‹?wf› by auto
with Cons subst Pair wf_assB pos_assB have "(pi«?bet,s>>) ≽ (pi«?bet,t>>)" by force
with ‹?wf› have "?go" by (simp add: interpr_subst)
}
thus ?thesis by blast
qed }
then show ?case by simp
qed
with Pair show ?thesis by simp
qed
qed
next
show "trans inter_ns" unfolding trans_def
proof (clarify)
fix s t u :: "('f,'v)term"
assume st: "(s,t) ∈ inter_ns" and tu: "(t,u) ∈ inter_ns"
show "(s,u) ∈ inter_ns" unfolding inter_ns_def
proof(rule, unfold split, clarify)
fix α :: "'v ⇒ 'a"
assume wf: "wf_ass R α" "pos_ass α" "apos_ass α"
show "(pi«α,s>>) ≽ (pi«α,u>>)"
by (rule geq_trans, insert st tu wf, unfold inter_ns_def, auto intro: wf_terms)
qed
qed
next
show "trans inter_s" unfolding trans_def
proof (clarify)
fix s t u :: "('f,'v)term"
assume st: "(s,t) ∈ inter_s" and tu: "(t,u) ∈ inter_s"
show "(s,u) ∈ inter_s" unfolding inter_s_def
proof(rule, unfold split, clarify)
fix α :: "'v ⇒ 'a"
assume wf: "wf_ass R α" "pos_ass α" "apos_ass α"
show "(pi«α,s>>) ≻ (pi«α,u>>)"
by (rule gt_trans, insert st tu wf, unfold inter_s_def, auto intro: wf_terms)
qed
qed
next
show "refl inter_ns"
unfolding inter_ns_def refl_on_def using geq_refl by (auto intro: wf_terms)
show "inter_s ⊆ inter_ns" by (rule inter_s_subset_inter_ns)
qed
context linear_poly_order
begin
lemma eval_term_subst_eq: "⟦⋀ x. x ∈ vars_term t ⟹ α x = β x⟧ ⟹ (pi«α,t>>) = (pi«β,t>>)"
proof (induction t)
case (Var x)
thus ?case by simp
next
case (Fun f ts)
{
fix t x
assume t: "t ∈ set ts" and x: "x ∈ vars_term t"
with Fun.prems[of x] have "α x = β x" by auto
} note id = this
{
fix t
assume t: "t ∈ set ts"
from Fun.IH[OF t id[OF t]]
have "(pi«α,t>>) = (pi«β,t>>)" .
} note IH = this
obtain d ds where pi: "pi (f,length ts) = (d,ds)" by force
show ?case unfolding eval_termI.simps Let_def pi split
proof (rule arg_cong[where f = "λ a. Max 𝟬 (d ⊕ list_sum R a)"],
rule map_cong[OF refl])
fix x
assume "x ∈ set (zip ds ts)"
from zip_snd[OF this] have "snd x ∈ set ts" .
from IH[OF this]
show "fst x ⊗ (pi«α,snd x>>) = fst x ⊗ (pi«β,snd x>>)" by simp
qed
qed
end
locale npsm_mono_linear_poly_order = linear_poly_order +
fixes F :: "'b sig"
assumes F_unary: "⋀ fn. fn ∈ F ⟹ snd fn ≤ Suc 0"
and pi_mono: "⋀ fn. fn ∈ F ⟹ snd fn = Suc 0 ⟹ fst (pi fn) = 𝟬 ∧ length (snd (pi fn)) = Suc 0"
and mode: "¬ psm"
begin
lemma inter_s_F_mono:
fixes s :: "('b,'v)term"
assumes st: "(s,t) ∈ inter_s"
and F: "(f,Suc (length bef + length aft)) ∈ F"
shows "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ inter_s"
proof -
let ?f = "(f,Suc 0)"
from F_unary[OF F] have empty: "bef = []" "aft = []" by auto
from F empty have "?f ∈ F" by auto
from pi_mono[OF this] have pi: "fst (pi ?f) = 𝟬" "length (snd (pi ?f)) = Suc 0" by auto
let ?st' = "Fun f (bef @ s # aft)"
let ?tt' = "Fun f (bef @ t # aft)"
let ?pair' = "(?st', ?tt')"
let ?s = "Fun f [s]"
let ?t = "Fun f [t]"
let ?pair = "(?s, ?t)"
have pair: "?pair' = ?pair" unfolding empty by simp
obtain c cs where ccs: "pi ?f = (c,cs)" by force
with pi obtain c where pi: "pi ?f = (𝟬,[c])" by (cases "snd (pi ?f)", auto)
from wf_pi[THEN conjunct1] have "∀ d ∈ set (snd (pi ?f)). d ∈ carrier R ∧ d ≽ 𝟬" by auto
with pi have wf_c: "c ∈ carrier R" and c_0: "c ≽ 𝟬" by auto
from wf_pi[THEN conjunct2] have "arc_pos (fst (pi ?f)) ∨ (∃ a ∈ set (take (snd ?f) (snd (pi ?f))). arc_pos a)" by auto
show "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ inter_s"
unfolding inter_s_def pair
proof (clarify)
fix α :: "('v,'a)p_ass"
assume wf_ass: "wf_ass R α" and pos_ass: "pos_ass α" and apos_ass: "apos_ass α"
let ?in = "λ t :: ('b,'v) term. (pi«α,t>>)"
let ?inter = "λ s. c ⊗ ?in s"
from st[unfolded inter_s_def] wf_ass pos_ass apos_ass have gt: "?in s ≻ ?in t"
by simp
from times_gt_right_mono[OF gt mode _ _ wf_c]
have gt: "?inter s ≻ ?inter t" using wf_ass by simp
from wf_c wf_ass have wf_s: "?inter s ∈ carrier R" by simp
from wf_c wf_ass have wf_t: "?inter t ∈ carrier R" by simp
note max0 = max0_npsm_id[OF mode]
have int_s: "?in ?s = ?inter s" using max0 wf_s by (simp add: pi)
have int_t: "?in ?t = ?inter t" using max0 wf_t by (simp add: pi)
show "?in ?s ≻ ?in ?t" unfolding int_s int_t by (rule gt)
qed
qed
lemma rel_subterm_terminating:
fixes Rs Rw :: "('b, 'v) trs"
assumes F: "funas_trs Rs ⊆ F" "funas_trs Rw ⊆ F"
and orient: "Rs ⊆ inter_s" "Rw ⊆ inter_ns"
and ST: "ST ⊆ {(Fun f ts, t) | f ts t. t ∈ set ts ∧ (f,length ts) ∉ F}"
shows "SN_rel (rstep (Rs ∪ ST)) (rstep (Rw ∪ ST))"
proof (rule sig_mono_imp_SN_rel_subterm[OF inter_s_F_mono F_unary orient _ F ST])
fix l r
assume "(l,r) ∈ inter_ns ∩ Rw"
with F have ns: "(l,r) ∈ inter_ns" and Fl: "funas_term l ⊆ F"
and Fr: "funas_term r ⊆ F" unfolding funas_trs_def funas_rule_def [abs_def] by force+
show "vars_term r ⊆ vars_term l"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain x where xr: "x ∈ vars_term r" and xl: "x ∉ vars_term l" by auto
from Fr xr have "∃ c. c ∈ carrier R ∧ arc_pos c ∧ (∀ α. wf_ass R α ⟶ pi«α,r>> = c ⊗ α x)"
proof (induction r)
case (Var y)
from Var.prems have xy: "x = y" by simp
show ?case using wf_terms[of _ "Var y"]
by (intro exI[of _ 𝟭], unfold xy, auto simp: arc_pos_one)
next
case (Fun f ss)
from Fun.prems(1) have "(f,length ss) ∈ F" by simp
with F_unary[OF this] Fun.prems(2) obtain s where ss: "ss = [s]"
and F: "(f,Suc 0) ∈ F"
by (cases ss, auto)
with Fun.prems have "funas_term s ⊆ F" "x ∈ vars_term s" by auto
from Fun.IH[OF _ this, unfolded ss] obtain c where c: "c ∈ carrier R"
and ac: "arc_pos c"
and eval: "⋀ α. wf_ass R α ⟹ (pi«α,s>>) = c ⊗ α x" by auto
obtain d ds where "pi (f,Suc 0) = (d,ds)" by force
with pi_mono[OF F] obtain d where pi: "pi (f, length [s]) = (𝟬,[d])" by (cases ds, auto)
from wf_pi[THEN conjunct1, rule_format, of "(f,Suc 0)"] pi
have d: "d ∈ carrier R" by auto
from wf_pi[THEN conjunct2, rule_format, of "(f,Suc 0)"] pi
arc_pos_zero[OF mode] have ad: "arc_pos d" by auto
show ?case unfolding ss
proof (rule exI[of _ "d ⊗ c"], intro conjI allI impI)
show "d ⊗ c ∈ carrier R" using d c by simp
show "arc_pos (d ⊗ c)" using ad ac d c by simp
next
fix α :: "('v,'a)p_ass"
assume wf: "wf_ass R α"
hence x: "α x ∈ carrier R" unfolding wf_ass_def by auto
have "(pi«α,Fun f [s]>>) = Max 𝟬 (𝟬 ⊕ (d ⊗ (c ⊗ α x) ⊕ 𝟬))"
unfolding eval_termI.simps Let_def pi split
using eval[OF wf] by simp
also have "... = d ⊗ (c ⊗ α x)"
using max0_npsm_id[OF mode] d c x by simp
also have "… = (d ⊗ c) ⊗ α x" using d c x by algebra
finally show "(pi«α,Fun f [s]>>) = (d ⊗ c) ⊗ α x" .
qed
qed
then obtain c where c: "c ∈ carrier R" and ac: "arc_pos c" and
evalr: "⋀ α. wf_ass R α ⟹ (pi«α,r>>) = c ⊗ α x"
by auto
let ?d = "default_ass :: ('v,'a)p_ass"
from wf_pos_apos_default_ass
have wd: "wf_ass R ?d" and pd: "pos_ass ?d" and ad: "apos_ass ?d" by auto
from not_all_ge[OF mode wf_terms[OF wd] c ac, of l] obtain e where
we: "e ∈ carrier R" and pe: "e ≽ 𝟬" and ae: "arc_pos e"
and nge: "¬ (pi«?d,l>>) ≽ c ⊗ e" by blast
let ?e = "λ y. if y = x then e else ?d y"
from wd we have wae: "wf_ass R ?e" unfolding wf_ass_def by auto
from pd pe have pae: "pos_ass ?e" unfolding pos_ass_def by auto
from ad ae have aae: "apos_ass ?e" unfolding apos_ass_def by auto
have id: "(pi«?d,l>>) = (pi«?e,l>>)"
by (rule eval_term_subst_eq, insert xl, auto)
have "... ≽ (pi«?e,r>>)" using ns[unfolded inter_ns_def] wae pae aae by auto
also have "... = c ⊗ e" unfolding evalr[OF wae] by simp
finally have "(pi«?d,l>>) ≽ c ⊗ e" unfolding id .
with nge show False by blast
qed
qed
end
lemma pow_update[simp]: "x (^)⇘(C ⦇gt := a, bound := b⦈)⇙ (n :: nat) = x (^)⇘C⇙ n"
unfolding nat_pow_def by auto
lemma to_lpoly_inter_update[simp]:
"to_lpoly_inter (C ⦇gt := a, bound := b⦈) I = to_lpoly_inter C I"
unfolding to_lpoly_inter_def by auto
lemma create_af_update[simp]: "create_af (C ⦇gt := a, bound := b⦈) I = create_af C I"
unfolding create_af_def by auto
lemma create_mono_af_update[simp]: "create_mono_af (C ⦇gt := a, bound := b⦈) I = create_mono_af C I"
unfolding create_mono_af_def by auto
lemma add_var_update[simp]: "add_var (R⦇ gt := gt, bound := bnd ⦈) = add_var R"
proof (intro ext, goal_cases)
case (1 x a xs)
show ?case
by (induct x a xs rule: add_var.induct, auto)
qed
lemma wf_pvars_update[simp]: "wf_pvars (R⦇ gt := gt, bound := bnd ⦈) = wf_pvars R"
by (rule ext, simp add: wf_pvars_def)
lemma wf_lpoly_update[simp]: "wf_lpoly (R⦇ gt := gt, bound := bnd ⦈) = wf_lpoly R"
proof (intro ext, goal_cases)
case (1 x)
show ?case by (cases x, auto)
qed
lemma list_prod_update[simp]: "list_prod (R⦇ gt := gt, bound := bnd ⦈) = list_prod R"
proof (intro ext, goal_cases)
case (1 xs)
show ?case by (induct xs rule: list_prod.induct, auto)
qed
lemma sum_pvars_update[simp]: "sum_pvars (R⦇ gt := gt, bound := bnd ⦈) = sum_pvars R"
proof (intro ext, goal_cases)
case (1 x xs)
show ?case by (induct x xs rule: sum_pvars.induct, auto)
qed
lemma sum_lpoly_update[simp]: "sum_lpoly (R⦇ gt := gt, bound := bnd ⦈) = sum_lpoly R"
proof (intro ext, goal_cases)
case (1 x xs)
show ?case by (induct x xs rule: sum_lpoly.induct, auto)
qed
lemma mul_pvars_update[simp]: "mul_pvars (R⦇ gt := gt, bound := bnd ⦈) = mul_pvars R"
proof (intro ext, goal_cases)
case (1 x xs)
show ?case by (induct x xs rule: mul_pvars.induct, auto simp: Let_def)
qed
lemma mul_lpoly_update[simp]: "mul_lpoly (R⦇ gt := gt, bound := bnd ⦈) = mul_lpoly R"
proof (intro ext, goal_cases)
case (1 x xs)
show ?case by (induct x xs rule: mul_lpoly.induct, auto)
qed
lemma update_manual:
"Max⇘R⦇gt := gt, bound := bnd⦈⇙ = Max⇘R⇙"
"𝟬⇘R⦇gt := gt, bound := bnd⦈⇙ = 𝟬⇘R⇙" by auto
lemma Pleft_update[simp]: "PleftI (R⦇ gt := gt, bound := bnd ⦈) = PleftI R"
unfolding PleftI_def PleftI_sumC_def PleftI_graph_def by (simp, unfold update_manual, simp)
lemma Pright_update[simp]: "PrightI (R⦇ gt := gt, bound := bnd ⦈) = PrightI R"
unfolding PrightI_def PrightI_sumC_def PrightI_graph_def by (simp, unfold update_manual, simp)
context linear_poly_order
begin
lemma wf_elem_coeff_left:
assumes "a ∈ set (coeffs_of_lpoly R (Pleft t))"
shows "a ∈ carrier R"
proof -
have "wf_ass R default_ass" and "pos_ass default_ass" by auto
from Pleft_both[OF this] have "wf_lpoly R (Pleft t)" ..
from wf_lpoly_coeff[OF this] show ?thesis using assms by auto
qed
lemma wf_elem_coeff_right: assumes "a ∈ set (coeffs_of_lpoly R (Pright t))" shows "a ∈ carrier R"
proof -
have "wf_ass R default_ass" and "pos_ass default_ass" by auto
from Pright_both[OF this] have "wf_lpoly R (Pright t)" by auto
from wf_lpoly_coeff[OF this] show ?thesis using assms by auto
qed
lemma check_polo_ns: fixes st :: "('f,'v :: show)rule"
assumes ok: "isOK(check_polo_ns (R ⦇ gt := gt, bound := bnd ⦈) pi st)"
shows "st ∈ inter_ns"
proof -
let ?R = "R ⦇ gt := gt, bound := bnd ⦈"
obtain s t where st: "st = (s,t)" by force
from ok st have "isOK(check_lpoly_ns ?R (Pleft s) (Pright t))" by simp
from check_lpoly_ns_sound[OF this wf_Pleft wf_Pright] have poly: "(Pleft s, Pright t) ∈ poly_ns" .
show ?thesis unfolding st inter_ns_def
proof (simp, intro allI impI, elim conjE)
fix α :: "'v ⇒ 'a"
assume [simp]: "wf_ass R α" "pos_ass α" "apos_ass α"
have ge1: "(pi«α,s>>) ≽ eval_lpoly α (Pleft s)" by (rule Pleft_sound, auto)
have mid: "… ≽ eval_lpoly α (Pright t)" using poly unfolding poly_ns_def by auto
have ge2: "… ≽ (pi«α,t>>)" by (rule Pright_sound, auto)
show "(pi«α,s>>) ≽ (pi«α,t>>)"
by (rule geq_trans[OF ge1 geq_trans[OF mid ge2]], auto)
qed
qed
lemma check_polo_s:
fixes st :: "('f,'v :: show)rule"
assumes ok: "isOK(check_polo_s (R ⦇ gt := gt, bound := bnd ⦈) pi st)"
and gt: "⋀ a b. (a,b) ∈ set (coeffs_of_constraint (R ⦇ gt := gt, bound := bnd ⦈) pi st)
⟹ a ∈ carrier R ⟹ b ∈ carrier R ⟹ gt a b ⟹ a ≻ b"
shows "st ∈ inter_s"
proof -
let ?R = "R ⦇ gt := gt, bound := bnd ⦈"
obtain s t where st: "st = (s,t)" by force
from ok st have ok: "isOK(check_lpoly_s ?R (Pleft s) (Pright t))" by simp
have poly: "(Pleft s, Pright t) ∈ poly_s"
by (rule check_lpoly_s_sound[OF ok wf_Pleft wf_Pright gt],
auto simp: coeffs_of_constraint_def st)
show ?thesis unfolding st inter_s_def
proof (simp, intro allI impI, elim conjE)
fix α :: "'v ⇒ 'a"
assume [simp]: "wf_ass R α" "pos_ass α" "apos_ass α"
have ge1: "(pi«α,s>>) ≽ eval_lpoly α (Pleft s)" by (rule Pleft_sound, auto)
have mid: "… ≻ eval_lpoly α (Pright t)" using poly unfolding poly_s_def by auto
have ge2: "… ≽ (pi«α,t>>)" by (rule Pright_sound, auto)
show "(pi«α,s>>) ≻ (pi«α,t>>)"
by (rule compat_orig[OF ge1 compat2[OF mid ge2]], auto)
qed
qed
end
context lpoly_order
begin
definition bound_entry :: "'a ⇒ 'a ⇒ 'a × 'a list ⇒ bool"
where "bound_entry bcoeff bconst ≡ λ (a,as). bconst ≽ a ∧ (∀ a ∈ set as. bcoeff ≽ a ∨ 𝟭 ≽ a)"
definition bound_entry_strict :: "'a ⇒ 'a ⇒ 'a × 'a list ⇒ bool"
where "bound_entry_strict bcoeff bconst ≡ λ (a,as). bconst ≽ a ∧ (∀ a ∈ set as. bcoeff ≽ a)"
lemma pow_ge_zero[intro]: assumes a: "a ≽ 𝟬"
and wf: "a ∈ carrier R"
shows "a (^) (n :: nat) ≽ 𝟬"
proof (induct n)
case (Suc n)
have "a (^) (Suc n) ≽ 𝟬 ⊗ a" unfolding nat_pow_Suc
by (rule times_left_mono[OF a Suc], insert wf, auto)
thus ?case using wf by auto
qed auto
lemma pow_commute_left: assumes wf[simp]: "a ∈ carrier R"
shows "a (^) (n :: nat) ⊗ a = a ⊗ a (^) n"
proof (induct n)
case (Suc n)
have "a (^) (Suc n) ⊗ a = (a ⊗ a (^) n) ⊗ a"
unfolding nat_pow_Suc unfolding Suc ..
also have "... = a ⊗ (a (^) n ⊗ a)" using wf nat_pow_closed[OF wf] by algebra
finally show ?case by simp
qed simp
lemma pow_ge_1: assumes 1: "𝟭 ≽ a"
and 0: "a ≽ 𝟬"
and wf: "a ∈ carrier R"
shows "𝟭 ≽ a (^) (n :: nat)"
proof (induct n)
case (Suc n)
have "(𝟭 ≽ (a (^) (Suc n))) = ((𝟭 ⊗ 𝟭) ≽ (a (^) n ⊗ a))" by simp
also have "..."
by (rule geq_trans[OF times_right_mono[OF one_geq_zero 1] times_left_mono[OF 0 Suc]], insert wf, auto)
thus ?case by simp
qed simp
lemma list_sum_append[simp]: assumes as: "set as ⊆ carrier R"
and bs: "set bs ⊆ carrier R"
shows "list_sum R (as @ bs) = list_sum R as ⊕ list_sum R bs"
using as
proof (induct as)
case Nil
with wf_list_sum[OF bs] show ?case by auto
next
case (Cons a as)
hence IH: "list_sum R (as @ bs) = list_sum R as ⊕ list_sum R bs"
and wf: "a ∈ carrier R" "set as ⊆ carrier R"
by auto
show ?case using IH wf_list_sum[OF wf(2)] wf(1) wf_list_sum[OF bs]
by (simp, algebra)
qed
end
context linear_poly_order
begin
lemma bound_eval_term_main_0:
assumes bF: "⋀ fn. fn ∈ F ⟹ bound_entry_strict 𝟬 bcv (pi fn)"
and bcv: "bcv ≽ 𝟬"
and wfbcv: "bcv ∈ carrier R"
and t: "funas_term (t :: ('f,'v)term) ⊆ F"
shows "bcv ≽ (pi«zero_ass,t>>)"
proof (cases t)
case (Var x)
thus ?thesis using bcv by (auto simp: zero_ass_def)
next
case (Fun f ts)
let ?e = "λ t. pi«zero_ass,t>>"
let ?n = "length ts"
obtain a as where pi: "pi (f, ?n) = (a,as)" by force
let ?map = "map (λ at. fst at ⊗ ?e (snd at)) (zip as ts)"
let ?map' = "map (λ at. 𝟬) (zip as ts)"
let ?nn = "length (zip as ts)"
note wf = wf_pi[THEN conjunct1, rule_format, of "(f, ?n)", unfolded pi fst_conv snd_conv]
from wf have wfa: "a ∈ carrier R" and wfas: "⋀ a. a ∈ set as ⟹ a ∈ carrier R"
and as0: "⋀ a. a ∈ set as ⟹ a ≽ 𝟬" by auto
from Fun t have "(f,?n) ∈ F" by auto
from bF[OF this, unfolded pi bound_entry_strict_def split]
have b_a: "bcv ≽ a" and b_as: "⋀ a. a ∈ set as ⟹ 𝟬 ≽ a" by auto
have "𝟬 = list_sum R ?map'"
by (induct "zip as ts", auto)
also have "list_sum R ?map' ≽ list_sum R ?map"
proof (rule list_sum_mono)
fix at
assume mem: "at ∈ set (zip as ts)"
then obtain a t where at: "at = (a,t)" by force
from set_zip_leftD[OF mem[unfolded at]] have a: "a ∈ set as" .
have et0: "?e t ≽ 𝟬" and etC: "?e t ∈ carrier R" by auto
from times_left_mono[OF et0 b_as[OF a] _ wfas[OF a] etC] etC wfas[OF a]
show "𝟬 ≽ fst at ⊗ ?e (snd at) ∧ 𝟬 ∈ carrier R ∧ fst at ⊗ ?e (snd at) ∈ carrier R"
unfolding at by auto
qed
finally have map0: "𝟬 ≽ list_sum R ?map" .
have wfmap: "list_sum R ?map ∈ carrier R"
by (rule wf_list_sum, insert wfas, auto dest: set_zip_leftD)
have "?e t = Max 𝟬 (a ⊕ list_sum R ?map)"
unfolding Fun by (simp add: pi)
also have "Max 𝟬 (a ⊕ 𝟬) ≽ …"
by (rule max_mono, rule plus_right_mono[OF map0], insert wfa wfmap, auto)
also have "a ⊕ 𝟬 = a" using wfa by simp
finally have ge2: "Max 𝟬 a ≽ ?e t" .
have "bcv ≽ Max 𝟬 a" using b_a bcv wfbcv wfa
by (metis max_mono max0_id_pos zero_closed)
from geq_trans[OF this ge2 wfbcv] wfa
show ?thesis by auto
qed
lemma bound_eval_term_main:
assumes bF: "⋀ fn. fn ∈ F ⟹ bound_entry bc bcv (pi fn)"
and bc: "bc ≽ 𝟬"
and bcv: "bcv ≽ 𝟬"
and wfbcv: "bcv ∈ carrier R"
and wfbc: "bc ∈ carrier R"
and t: "funas_term (t :: ('f,'v)term) ⊆ F"
shows "∃ bs. length bs ≤ term_size t ∧ (∀ b ∈ set bs. b ∈ carrier R
∧ (∃ n < term_size t. b = bc (^) n ⊗ bcv)) ∧ (list_sum R bs ≽ (pi«zero_ass,t>>))"
using t
proof (induct t)
case (Var x)
show ?case
by (rule exI[of _ Nil], auto simp: zero_ass_def)
next
case (Fun f ts)
let ?e = "λ t. pi«zero_ass,t>>"
let ?n = "length ts"
obtain a as where pi: "pi (f, ?n) = (a,as)" by force
let ?map = "map (λ at. fst at ⊗ ?e (snd at)) (zip as ts)"
let ?nn = "length (zip as ts)"
note wf = wf_pi[THEN conjunct1, rule_format, of "(f, ?n)", unfolded pi fst_conv snd_conv]
from wf have wfa: "a ∈ carrier R" and wfas: "⋀ a. a ∈ set as ⟹ a ∈ carrier R"
and as0: "⋀ a. a ∈ set as ⟹ a ≽ 𝟬" by auto
from Fun(2) have "(f,?n) ∈ F" by auto
from bF[OF this, unfolded pi bound_entry_def split]
have b_a: "bcv ≽ a" and b_as: "⋀ a. a ∈ set as ⟹ (bc ≽ a) ∨ (𝟭 ≽ a)" by auto
obtain Pow where Pow: "Pow = (λ b (t :: ('f,'v)term). (∃ n < term_size t. b = bc (^) n ⊗ bcv))" by auto
let ?P = "λ bs i. length bs ≤ term_size (ts ! i) ∧ (∀ b ∈ set bs. Pow b (Fun f ts)) ∧ (∀ b ∈ set bs. b ∈ carrier R) ∧ (list_sum R bs ≽ ?map ! i)"
{
fix i
assume i: "i < ?nn"
hence ias: "i < length as" and its: "i < ?n" by auto
from ias have asi: "as ! i ∈ set as" by auto
from its have tsi: "ts ! i ∈ set ts" by auto
from Fun(2) tsi have "funas_term (ts ! i) ⊆ F" by auto
note IH = Fun(1)[OF tsi this]
from as0[OF asi] have asi0: "as ! i ≽ 𝟬" .
from b_as[OF asi] have b_asi: "(bc ≽ as ! i) ∨ (𝟭 ≽ as ! i)" .
from wfas[OF asi] have wfasi: "as ! i ∈ carrier R" .
from i have id: "?map ! i = (as ! i ⊗ ?e (ts ! i))" by auto
have wf_map: "?map ! i ∈ carrier R" unfolding id using wfasi by auto
from IH obtain bs where len: "length bs ≤ term_size (ts ! i)"
and bs: "⋀ b. b ∈ set bs ⟹ Pow b (ts ! i)"
and wf_bs: "⋀ b. b ∈ set bs ⟹ b ∈ carrier R"
and ge2: "list_sum R bs ≽ ?e (ts ! i)" unfolding Pow by auto
let ?bs = "map (op ⊗ bc) bs"
have lsum: "list_sum R ?bs = bc ⊗ list_sum R bs" using wf_bs
proof (induct bs)
case (Cons b bs)
hence wfb: "b ∈ carrier R" and wfbs: "⋀ b. b ∈ set bs ⟹ b ∈ carrier R" and
IH: "list_sum R (map (op ⊗ bc) bs) = bc ⊗ (list_sum R bs)" by auto
show ?case unfolding list.map list_prod.simps
unfolding IH monoid.simps
by (rule r_distr[symmetric], insert wfb wfbc wfbs, auto)
qed (auto simp: wfbc)
{
fix bbc
assume "bbc ∈ set ?bs"
then obtain b where bbc: "bbc = bc ⊗ b" and b: "b ∈ set bs" by auto
hence "bbc ∈ carrier R" using wfbc wf_bs by auto
} note wf_bs2 = this
have size_tsi: "term_size (ts ! i) < term_size (Fun f ts)"
by (rule supt_term_size, insert tsi, auto)
{
fix bbc
assume "bbc ∈ set ?bs"
then obtain b where bbc: "bbc = bc ⊗ b" and b: "b ∈ set bs" by auto
from bs[OF b] obtain n where b: "b = bc (^) n ⊗ bcv" and n: "n < term_size (ts ! i)" unfolding Pow by auto
have bbc: "bbc = bc (^) (Suc n) ⊗ bcv" unfolding bbc b nat_pow_Suc pow_commute_left[OF wfbc]
by (rule m_assoc[symmetric], insert wfbc wfbcv, auto)
from size_tsi n have "Suc n < term_size (Fun f ts)" by auto
with bbc have "∃ n < term_size (Fun f ts). bbc = bc (^) n ⊗ bcv" by blast
hence "Pow bbc (Fun f ts)" unfolding Pow .
} note bs2 = this
from b_asi have "∃ bs2. ?P bs2 i"
proof
assume b_asi: "bc ≽ as ! i"
have ge: "(bc ⊗ ?e (ts ! i)) ≽ ?map ! i" unfolding id
by (rule times_left_mono[OF _ b_asi wfbc wfasi], auto)
have ge2: "list_sum R ?bs ≽ (bc ⊗ (?e (ts ! i)))" unfolding lsum
by (rule times_right_mono[OF bc ge2 wfbc wf_list_sum], insert wf_bs wfbcv, auto)
have ge: "list_sum R ?bs ≽ ?map ! i"
by (rule geq_trans[OF ge2 ge wf_list_sum _ wf_map], insert wf_bs2 wfbc, auto)
show "∃ bs2. ?P bs2 i"
by (rule exI[of _ ?bs], unfold length_map, insert len ge bs2 wf_bs2, blast)
next
assume asi: "𝟭 ≽ as ! i"
show "∃ bs2. ?P bs2 i"
proof (rule exI[of _ bs], rule conjI[OF len conjI[OF ballI conjI[OF ballI[OF wf_bs]]]])
fix b
assume "b ∈ set bs"
from bs[OF this, unfolded Pow] obtain n where n: "n < term_size (ts ! i)" and b: "b = bc (^) n ⊗ bcv"
by auto
with size_tsi have "n < term_size (Fun f ts)" by auto
with b show "Pow b (Fun f ts)" unfolding Pow by blast
next
have "(𝟭 ⊗ ?e (ts ! i)) ≽ ?map ! i" unfolding id
by (rule times_left_mono[OF _ asi _ wfasi], auto)
hence ge: "?e (ts ! i) ≽ ?map ! i" by simp
show "list_sum R bs ≽ ?map ! i"
by (rule geq_trans[OF ge2 ge wf_list_sum _ wf_map], insert wf_bs, auto)
qed
qed
note this ‹?map ! i ∈ carrier R›
}
hence bsi: "∀ i. ∃ bs. i < ?nn ⟶ ?P bs i" and wfmi: "⋀ i. i < ?nn ⟹ ?map ! i ∈ carrier R"
by blast+
from choice[OF bsi] obtain bs where bs: "⋀ i. i < ?nn ⟹ ?P (bs i) i" by auto
let ?bs' = "concat (map bs [0 ..< ?nn])"
let ?bs = "bcv # ?bs'"
have "length ?bs' ≤ sum_list (map term_size ts)" unfolding length_concat
unfolding map_map o_def
using bs[THEN conjunct1]
proof (induct ts arbitrary: as bs)
case (Cons t ts aas bs)
note oCons = this
show ?case
proof (cases aas)
case (Cons a as)
note oCons = oCons[unfolded Cons]
note IH = oCons(1)[of as "λ i. bs (Suc i)"]
note pre = oCons(2)
from pre[of "0 :: nat"] have le: "length (bs 0) ≤ term_size t" by auto
{
fix i
assume i: "i < length (zip as ts)"
hence i: "Suc i < length (zip (a # as) (t # ts))" by simp
from pre[OF this] have "length (bs (Suc i)) ≤ term_size (ts ! i)" by auto
}
from IH[OF this] have
le2: " (∑x←[0..<length (zip as ts)]. length (bs (Suc x))) ≤ sum_list (map term_size ts)"
by simp
have "(∑x←[0..<length (zip aas (t # ts))]. length (bs x)) =
(∑x←[0..< Suc (length (zip as ts))]. length (bs x))"
unfolding Cons by simp
also have "... = length (bs 0) + (∑x←[0..< length (zip as ts)]. length (bs (Suc x)))"
unfolding map_upt_Suc by simp
also have "... ≤ term_size t + sum_list (map term_size ts)" using le le2 by auto
finally
show ?thesis by simp
qed auto
qed auto
hence len: "length ?bs ≤ term_size (Fun f ts)" by auto
{
fix b
assume "b ∈ set ?bs"
hence "b = bcv ∨ b ∈ set ?bs'" by auto
hence "b ∈ carrier R ∧ Pow b (Fun f ts) ∧ (b ≽ 𝟬)"
proof
assume b: "b = bcv"
show ?thesis
unfolding b Pow
by (rule conjI[OF wfbcv], rule conjI, rule exI[of _ "0 :: nat"], insert wfbcv bcv, auto)
next
assume "b ∈ set ?bs'"
then obtain i where i: "i < ?nn" and b: "b ∈ set (bs i)" by auto
from i have ias: "i < length as" by auto
hence asi: "as ! i ∈ set as" by auto
from bs[OF i] b have "Pow b (Fun f ts)" by auto
from this[unfolded Pow] obtain n where bpow: "b = bc (^) (n :: nat) ⊗ bcv" by auto
have "b ≽ 𝟬 ⊗ bcv" unfolding bpow
by (rule times_left_mono[OF bcv pow_ge_zero], insert wfbc wfbcv bc, auto)
hence "b ≽ 𝟬" using wfbcv by auto
with bs[OF i] b show ?thesis by auto
qed
} note bs_wf_pow = this
show ?case
proof (rule exI[of _ ?bs], intro conjI, rule len, intro ballI)
fix b
assume "b ∈ set ?bs"
from bs_wf_pow[OF this]
show "b ∈ carrier R ∧ (∃ n < term_size (Fun f ts). b = bc (^) n ⊗ bcv)"
unfolding Pow by simp
next
have wf_bs: "list_sum R ?bs ∈ carrier R"
using bs_wf_pow by auto
let ?sum = "a ⊕ list_sum R ?map"
have e: "?e (Fun f ts) = Max 𝟬 ?sum" unfolding eval_termI.simps Let_def pi split ..
{
fix p
assume "p ∈ set ?map"
from this[unfolded set_map set_zip]
obtain i where i: "i < length as" and p: "p = (as ! i ⊗ ?e (ts ! i))" by auto
from i have asi: "as ! i ∈ set as" by auto
from wfas[OF asi] have "p ∈ carrier R" unfolding p by auto
} note wf_prods = this
hence wf_sum: "list_sum R ?map ∈ carrier R" by auto
with wfa have wf_asum: "?sum ∈ carrier R" by auto
have "list_sum R ?bs = Max 𝟬 (list_sum R ?bs)"
by (rule max0_id_pos[symmetric, OF pos_list_sum wf_bs], insert bs_wf_pow, auto)
also have "... ≽ ?e (Fun f ts)" unfolding e
proof (rule max_mono[OF _ wf_bs wf_asum])
have wf_bs': "list_sum R ?bs' ∈ carrier R" using bs_wf_pow by auto
have id: "list_sum R ?bs = bcv ⊕ list_sum R ?bs'" by simp
have ge1: "... ≽ a ⊕ list_sum R ?bs'"
by (rule plus_left_mono[OF b_a wfbcv wfa wf_bs'])
have ge2: "... ≽ ?sum"
proof (rule plus_right_mono[OF _ wfa wf_bs' wf_sum])
obtain z where z: "z = zip as ts" by auto
obtain f where f: "f = (λ (at :: 'a × ('f,'v)term). fst at ⊗ ?e (snd at))" by auto
from wf_prods have "⋀ p. p ∈ set (map f z) ⟹ p ∈ carrier R"
unfolding f z .
thus "list_sum R ?bs' ≽ list_sum R ?map" using bs[THEN conjunct2, THEN conjunct2] unfolding z[symmetric] f[symmetric]
proof (induct z arbitrary: bs)
case (Cons a z bs)
note IH = Cons(1)[of "λ i. bs (Suc i)"]
note wfaz = Cons(2)
hence wfa: "f a ∈ carrier R" and wfz: "⋀ p. p ∈ set (map f z) ⟹ p ∈ carrier R" by auto
note bs = Cons(3)
{
fix i
assume "i < length z"
hence "Suc i < length (a # z)" by auto
from bs[OF this]
have "(∀ a ∈ set (bs (Suc i)). a ∈ carrier R) ∧ (list_sum R (bs (Suc i)) ≽ map f z ! i)" by auto
} note bsz = this
let ?cc = "concat (map (λ i. bs (Suc i)) [0 ..< length z])"
from IH[OF wfz bsz] have ge2: "list_sum R ?cc ≽ list_sum R (map f z)" .
from bs[of "0 :: nat"] have wfbs0: "⋀ a. a ∈ set (bs 0) ⟹ a ∈ carrier R"
and ge1: "list_sum R (bs 0) ≽ f a" by auto
let ?start = "list_sum R (concat (map bs [0..<length (a # z)]))"
have "list_sum R (concat (map bs [0..<length (a # z)]))
= list_sum R (concat (map bs [0..< Suc (length z)]))" by simp
also have "... = list_sum R (bs 0 @ ?cc)"
unfolding map_upt_Suc by auto
also have "... = list_sum R (bs 0) ⊕ list_sum R ?cc"
by (rule list_sum_append, insert wfbs0 bsz, auto)
finally have id: "?start = list_sum R (bs 0) ⊕ list_sum R ?cc" "list_sum R (map f (a # z)) = f a ⊕ list_sum R (map f z)" by auto
show ?case unfolding id
by (rule plus_left_right_mono[OF ge1 ge2], insert wfbs0 wfa wfz bsz, auto)
qed simp
qed
show "list_sum R ?bs ≽ ?sum" unfolding id
by (rule geq_trans[OF ge1 ge2 _ _ wf_asum], insert wfa wfbcv bs_wf_pow, auto)
qed auto
finally
show "list_sum R ?bs ≽ ?e (Fun f ts)" .
qed
qed
end
locale complexity_linear_poly_order = linear_poly_order + complexity_linear_poly_order_carrier
begin
lemma bound_eval_term_derivational_0:
assumes bF: "⋀ fn. fn ∈ set F ⟹ bound_entry_strict 𝟬 bcv (pi fn)"
and bcv: "bcv ≽ 𝟬"
and wfbcv: "bcv ∈ carrier R"
and deriv: "t ∈ terms_of (Derivational_Complexity F)"
shows "bound R bcv ≥ bound R (pi«zero_ass,t>>)"
by (rule bound_mono[OF bound_eval_term_main_0[OF bF bcv], of "set F"],
insert deriv wfbcv, auto)
lemma bound_eval_term_derivational:
assumes bF: "⋀ fn. fn ∈ set F ⟹ bound_entry bc bcv (pi fn)"
and bc: "bc ≽ 𝟬"
and bcv: "bcv ≽ 𝟬"
and wfbcv: "bcv ∈ carrier R"
and wfbc: "bc ∈ carrier R"
and mono: "⋀ n m. n ≤ m ⟹ g n ≤ g m"
and bG: "⋀ n. bound R (bc (^) n ⊗ bcv) ≤ g n"
and deriv: "t ∈ terms_of_nat (Derivational_Complexity F) N"
shows "g N * N ≥ bound R (pi«zero_ass,t>>)"
proof -
from deriv have t: "funas_term t ⊆ set F" and N: "term_size t ≤ N" by auto
from bound_eval_term_main[OF bF bc bcv wfbcv wfbc t]
obtain bs where len: "length bs ≤ term_size t"
and bs: "⋀ b. b ∈ set bs ⟹ b ∈ carrier R ∧ (∃ n < term_size t. b = bc (^) n ⊗ bcv)"
and ge: "list_sum R bs ≽ (pi«zero_ass,t>>)"
by auto
{
fix b
assume "b ∈ set bs"
from bs[OF this] obtain n where wf: "b ∈ carrier R" and n: "n < term_size t" and b: "b = bc (^) n ⊗ bcv"
by auto
from bG[of n] have ge: "g n ≥ bound R b" unfolding b .
from n N have "n ≤ N" by auto
from mono[OF this] ge wf have "g N ≥ bound R b" "b ∈ carrier R" by auto
} note bs = this
hence "bound R (list_sum R bs) ≤ g N * length bs"
proof (induct bs)
case (Cons b bs)
from Cons have ge1: "g N ≥ bound R b" by auto
from Cons have ge2: "g N * length bs ≥ bound R (list_sum R bs)" by auto
have id: "bound R (list_sum R (b # bs)) ≤ bound R b + bound R (list_sum R bs)"
unfolding list_prod.simps monoid.simps
by (rule bound_plus, insert Cons, auto)
also have "... ≤ g N + g N * length bs" using ge1 ge2 by arith
finally show ?case by simp
qed simp
also have "... ≤ g N * size N"
using len N by auto
finally have "bound R (list_sum R bs) ≤ g N * N" by simp
from order_trans[OF bound_mono[OF ge] this]
show ?thesis using bs by auto
qed
lemma bound_eval_term_runtime_0:
assumes bF: "⋀ fn. fn ∈ set C ⟹ bound_entry_strict 𝟬 bcv (pi fn)"
and bcv: "bcv ≽ 𝟬"
and wfbcv: "bcv ∈ carrier R"
and bD: "⋀ fn. fn ∈ set D ⟹ bound_entry_strict bd bdv (pi fn)"
and bn: "⋀ fn. fn ∈ set D ⟹ snd fn ≤ bn"
and bd: "bd ≽ 𝟬"
and bdv: "bdv ≽ 𝟬"
and wfbdv: "bdv ∈ carrier R"
and wfbd: "bd ∈ carrier R"
and rt: "t ∈ terms_of (Runtime_Complexity C D)"
shows "bound R bdv + bn * bound R (bd ⊗ bcv) ≥ bound R (pi«zero_ass,t>>)"
proof -
let ?e = "λ t. (pi«zero_ass,t>>)"
from rt obtain f ts where t: "t = Fun f ts" by (cases t, auto)
let ?n = "length ts"
from rt t have fD: "(f,length ts) ∈ set D" and ti: "⋀ t. t ∈ set ts ⟹ funas_term t ⊆ set C"
by (auto simp: funas_args_term_def)
from bound_eval_term_main_0[OF bF bcv wfbcv ti] have ti: "⋀ t. t ∈ set ts ⟹ bcv ≽ ?e t" by auto
obtain a as where pi: "pi (f, ?n) = (a,as)" by force
let ?map = "map (λ at. fst at ⊗ ?e (snd at)) (zip as ts)"
let ?nn = "length (zip as ts)"
note wf = wf_pi[THEN conjunct1, rule_format, of "(f, ?n)", unfolded pi fst_conv snd_conv]
from wf have wfa: "a ∈ carrier R" and wfas: "⋀ a. a ∈ set as ⟹ a ∈ carrier R"
and as0: "⋀ a. a ∈ set as ⟹ a ≽ 𝟬" by auto
from bD[OF fD, unfolded pi bound_entry_strict_def split]
have b_a: "bdv ≽ a" and b_as: "⋀ a. a ∈ set as ⟹ bd ≽ a" by auto
def prods ≡ "?map"
{
fix p
assume p: "p ∈ set prods"
from this[unfolded prods_def set_map]
obtain at where mem: "at ∈ set (zip as ts)" and p: "p = fst at ⊗ ?e (snd at)" by auto
obtain a t where at: "at = (a,t)" by force
from set_zip_leftD[OF mem[unfolded at]] have a: "a ∈ set as" .
from set_zip_rightD[OF mem[unfolded at]] have t: "t ∈ set ts" .
have et0: "?e t ≽ 𝟬" and etC: "?e t ∈ carrier R" by auto
from times_left_mono[OF et0 b_as[OF a] wfbd wfas[OF a] etC]
have ge1: "bd ⊗ ?e t ≽ a ⊗ ?e t" .
from pos_term[of zero_ass t] have "?e t ≽ 𝟬" by auto
from times_right_mono[OF as0[OF a] this _ etC] wfas[OF a] have a0: "a ⊗ ?e t ≽ 𝟬" by auto
from times_right_mono[OF bd ti[OF t] wfbd wfbcv etC] have "bd ⊗ bcv ≽ bd ⊗ ?e t" .
from bound_mono[OF geq_trans[OF this ge1]] wfbd wfbcv etC wfas[OF a] as0[OF a] a0
have "bound R p ≤ bound R (bd ⊗ bcv)"
"p ∈ carrier R"
"p ≽ 𝟬" unfolding p at by auto
} note bound_prods = this
from bn[OF fD] have bn: "length prods ≤ bn" unfolding prods_def by simp
have "bound R (?e t) = bound R (Max 𝟬 (a ⊕ list_sum R prods))"
unfolding t using pi by (simp add: prods_def)
also have "... ≤ bound R (Max 𝟬 (bdv ⊕ list_sum R prods))"
by (rule bound_mono[OF max_mono[OF plus_left_mono[OF b_a]]], insert wfa wfbdv bound_prods, auto simp: wf_max0)
also have "Max 𝟬 (bdv ⊕ list_sum R prods) = bdv ⊕ list_sum R prods"
proof (rule max0_id_pos)
have "bdv ⊕ list_sum R prods ≽ 𝟬 ⊕ 𝟬"
by (rule geq_trans[OF plus_right_mono[OF pos_list_sum] plus_left_mono[OF bdv]], insert wfa wfbdv bound_prods, auto)
thus "bdv ⊕ list_sum R prods ≽ 𝟬" by simp
qed (insert bound_prods wfbdv, auto)
also have "bound R (bdv ⊕ list_sum R prods) ≤ bound R bdv + bound R (list_sum R prods)"
by (rule bound_plus, insert bound_prods wfbdv, auto)
also have "bound R (list_sum R prods) ≤ bn * bound R (bd ⊗ bcv)" using bn bound_prods(1-2)
proof (induct prods arbitrary: bn)
case (Cons p ps sbn)
from Cons(2) obtain bn where sbn: "sbn = Suc bn" and len: "length ps ≤ bn" by (cases sbn, auto)
from Cons(1)[OF len Cons(3-4)] have
IH: "bound R (list_sum R ps) ≤ bn * bound R (bd ⊗ bcv)" by auto
have "bound R (list_sum R (p # ps)) ≤ bound R p + bound R (list_sum R ps)" using Cons(3-4)
by (auto intro: bound_plus)
also have "… ≤ bound R p + bn * bound R (bd ⊗ bcv)" using IH by simp
also have "bound R p ≤ bound R (bd ⊗ bcv)"
by (rule Cons(3), auto)
finally show ?case unfolding sbn by auto
qed simp
finally show "bound R (?e t) ≤ bound R bdv + bn * bound R (bd ⊗ bcv)" by auto
qed
lemma bound_eval_term_runtime:
assumes bC: "⋀ fn. fn ∈ set C ⟹ bound_entry bc bcv (pi fn)"
and bc: "bc ≽ 𝟬"
and bcv: "bcv ≽ 𝟬"
and wfbcv: "bcv ∈ carrier R"
and wfbc: "bc ∈ carrier R"
and bD: "⋀ fn. fn ∈ set D ⟹ bound_entry_strict bd bdv (pi fn)"
and bn: "⋀ fn. fn ∈ set D ⟹ snd fn ≤ bn"
and bd: "bd ≽ 𝟬"
and bdv: "bdv ≽ 𝟬"
and wfbdv: "bdv ∈ carrier R"
and wfbd: "bd ∈ carrier R"
and mono: "⋀ n m. n ≤ m ⟹ g n ≤ g m"
and bG: "⋀ n. bound R (bd ⊗ (bc (^) n ⊗ bcv)) ≤ g n"
and deriv: "t ∈ terms_of_nat (Runtime_Complexity C D) N"
shows "bound R bdv + g N * N * bn ≥ bound R (pi«zero_ass,t>>)"
proof -
from deriv[simplified] obtain f ts where t: "t = Fun f ts" and f: "(f,length ts) ∈ set D" and
ts: "⋀ ti. ti ∈ set ts ⟹ funas_term ti ⊆ set C" and size: "term_size t ≤ N"
by (cases t) (auto simp: funas_args_term_def)
obtain a as where pi: "pi (f,length ts) = (a,as)" by force
from bn[OF f] have bn: "length ts ≤ bn" by simp
from bD[OF f] have ge_a: "bdv ≽ a" and ge_as: "⋀ a . a ∈ set as ⟹ bd ≽ a"
unfolding pi bound_entry_strict_def by auto
from wf_pi[THEN conjunct1, rule_format, of "(f,length ts)", unfolded pi]
have wfa: "a ∈ carrier R" and wfas: "⋀ a. a ∈ set as ⟹ a ∈ carrier R" and as0: "⋀ a. a ∈ set as ⟹ a ≽ 𝟬" by auto
let ?eval = "λ t. (pi«zero_ass,t>>)"
let ?p = "λ at. fst at ⊗ ?eval (snd at)"
let ?map = "map ?p (zip as ts)"
obtain prods where prods: "prods = ?map" by auto
{
fix p
assume "p ∈ set prods"
from this[unfolded prods set_conv_nth] obtain i where ias: "i < length as" and its: "i < length ts"
and p: "p = ?map ! i" by auto
let ?asi = "as ! i"
let ?tsi = "ts ! i"
from p ias its have p: "p = (?asi ⊗ ?eval ?tsi)" by auto
from ias have asi: "?asi ∈ set as" by auto
from wfas[OF this] as0[OF this] ge_as[OF this] have wfasi: "?asi ∈ carrier R" and asi0: "?asi ≽ 𝟬"
and bd_ge: "bd ≽ as ! i" .
from its have tsi: "?tsi ∈ set ts" by auto
from ts[OF tsi] have tsiC: "funas_term ?tsi ⊆ set C" .
from tsi have "t ⊳ ?tsi" unfolding t by auto
from supt_term_size[OF this] size have size: "term_size ?tsi ≤ N" by simp
from bound_eval_term_main[OF bC bc bcv wfbcv wfbc tsiC]
obtain bs where len: "length bs ≤ term_size ?tsi"
and bs: "⋀ b. b ∈ set bs ⟹ b ∈ carrier R ∧ (∃ n < term_size ?tsi. b = bc (^) n ⊗ bcv)"
and ge: "list_sum R bs ≽ ?eval ?tsi"
by auto
have bd_p: "bd ⊗ list_sum R bs ≽ p" unfolding p
by (rule geq_trans[OF times_left_mono[OF geq_trans[OF ge pos_term] bd_ge wfbd wfasi] times_right_mono[OF asi0 ge]], insert bs wfasi wfbd, auto)
from bs have gn_bd: "g N * length bs ≥ bound R (bd ⊗ list_sum R bs)"
proof (induct bs)
case (Cons b bs)
from Cons(2)[of b] obtain n where n: "n < term_size ?tsi" and b: "b = bc (^) n ⊗ bcv" by auto
from n size have n: "n ≤ N" by auto
from Cons(2) have wf: "b ∈ carrier R" "set bs ⊆ carrier R" by auto
have "bound R (bd ⊗ list_sum R (b # bs)) = bound R (bd ⊗ b ⊕ bd ⊗ list_sum R bs)"
by (rule arg_cong[of _ _ "bound R"], simp, insert wf wfbd wf_list_sum[OF wf(2)], algebra)
also have "... ≤ bound R (bd ⊗ b) + bound R (bd ⊗ list_sum R bs)"
by (rule bound_plus, insert Cons(2) wfbd, auto)
also have "... ≤ bound R (bd ⊗ b) + g N * length bs"
using Cons by auto
also have "bound R (bd ⊗ b) ≤ g n" unfolding b by (rule bG)
also have "... ≤ g N"
by (rule mono[OF n])
finally show ?case by simp
qed (simp add: wfbd)
from le_trans[OF bound_mono[OF bd_p] gn_bd]
have "bound R p ≤ g N * length bs" using bs wfbd wfasi unfolding p by auto
also have "... ≤ g N * N"
using le_trans[OF len size] by auto
finally have main: "bound R p ≤ g N * N" "p ∈ carrier R" unfolding p using wfasi by auto
have "p ≽ 𝟬 ⊗ 𝟬" unfolding p
by (rule geq_trans[OF times_left_mono[OF pos_term asi0]], insert wfasi, auto)
hence "p ≽ 𝟬" by simp
note main this
} note bound_prods = this
have "bound R (?eval t) = bound R (Max 𝟬 (a ⊕ list_sum R prods))"
unfolding t using pi by (simp add: Let_def prods)
also have "... ≤ bound R (Max 𝟬 ( bdv ⊕ list_sum R prods))"
by (rule bound_mono[OF max_mono[OF plus_left_mono[OF ge_a]]], insert wfa wfbdv bound_prods, auto simp: wf_max0)
also have "Max 𝟬 (bdv ⊕ list_sum R prods) = bdv ⊕ list_sum R prods"
proof (rule max0_id_pos)
have "bdv ⊕ list_sum R prods ≽ 𝟬 ⊕ 𝟬"
by (rule geq_trans[OF plus_right_mono[OF pos_list_sum] plus_left_mono[OF bdv]], insert wfa wfbdv bound_prods, auto)
thus "bdv ⊕ list_sum R prods ≽ 𝟬" by simp
qed (insert bound_prods wfbdv, auto)
also have "bound R (bdv ⊕ list_sum R prods) ≤ bound R bdv + bound R (list_sum R prods)"
by (rule bound_plus, insert bound_prods wfbdv, auto)
also have "bound R (list_sum R prods) ≤ g N * N * length (prods)"
using bound_prods(1) bound_prods(2)
proof (induct prods)
case (Cons p prods)
have "bound R (list_sum R (p # prods)) ≤ bound R p + bound R (list_sum R prods)"
unfolding list_prod.simps monoid.simps
by (rule bound_plus, insert Cons(3), auto)
also have "bound R (list_sum R prods) ≤ g N * N * length prods"
using Cons by auto
also have "bound R p ≤ g N * N" using Cons(2)[of p] by auto
finally show ?case by simp
qed simp
also have "... ≤ g N * N * bn"
proof -
from prods bn have "length prods ≤ bn" by simp
thus ?thesis by simp
qed
finally show "bound R (?eval t) ≤ bound R bdv + g N * N * bn" by auto
qed
end
context ordered_semiring
begin
lemma poly_c_max_list:
assumes init: "init ∈ carrier R"
shows "⟦ ⋀ a. a ∈ set as ⟹ a ∈ carrier R⟧ ⟹
(foldr Max as init) ∈ carrier R ∧ (foldr Max as init) ≽ init ∧ (∀ a ∈ set as. (foldr Max as init) ≽ a)"
proof (induct as)
case (Cons a as)
let ?w = "λ a. a ∈ carrier R"
from Cons(2) have a: "?w a" and as: "⋀ a. a ∈ set as ⟹ ?w a" by auto
let ?mf = "foldr Max as init"
let ?mm = "Max a ?mf"
note IH = Cons(1)[OF as]
from IH have mf: "?w ?mf" and ge_init: "?mf ≽ init" and ge_as: "⋀ a. a ∈ set as ⟹ ?mf ≽ a" by auto
from wf_max[OF a mf] have mm: "?w ?mm" .
from max_ge[OF a mf] have mm_a: "?mm ≽ a" .
from max_ge_right[OF a mf] have mm_mf: "?mm ≽ ?mf" .
note mm_mf = geq_trans[OF mm_mf _ mm mf]
from mm_mf[OF ge_init init] have mm_init: "?mm ≽ init" .
from mm_mf[OF ge_as as] have mm_as: "⋀ a. a ∈ set as ⟹ ?mm ≽ a" .
from mm mm_init mm_as mm_a
show ?case by simp
qed (simp add: init)
end
context
fixes R :: "('a,'b)ordered_semiring_scheme" (structure)
begin
definition poly_c_max_inter_bcoeff :: "('f × nat)list ⇒ ('f,'a)lpoly_inter ⇒ 'a"
where "poly_c_max_inter_bcoeff F pi = foldr Max (concat (map (λ fn. filter (λ b. ¬ (𝟭 ≽ b)) (snd (pi fn))) F)) 𝟬"
definition poly_c_max_inter_bcoeff_strict :: "('f × nat)list ⇒ ('f,'a)lpoly_inter ⇒ 'a"
where "poly_c_max_inter_bcoeff_strict F pi = foldr Max (concat (map (λ fn. snd (pi fn)) F)) 𝟬"
definition poly_c_max_inter_bconst :: "('f × nat)list ⇒ ('f,'a)lpoly_inter ⇒ 'a"
where "poly_c_max_inter_bconst F pi = foldr Max (map (λ fn. fst (pi fn)) F) 𝟬"
end
context linear_poly_order
begin
lemma poly_c_max_inter_bcoeff:
"poly_c_max_inter_bcoeff R F pi ∈ carrier R ∧ poly_c_max_inter_bcoeff R F pi ≽ 𝟬 ∧
(∀ a ∈ set (concat (map (λ fn. filter (λ b. ¬ (𝟭 ≽ b)) (snd (pi fn))) F)). poly_c_max_inter_bcoeff R F pi ≽ a)"
unfolding poly_c_max_inter_bcoeff_def
by (rule poly_c_max_list[OF zero_closed], insert wf_pi, auto)
lemma poly_c_max_inter_bcoeff_strict:
"poly_c_max_inter_bcoeff_strict R F pi ∈ carrier R ∧ poly_c_max_inter_bcoeff_strict R F pi ≽ 𝟬 ∧
(∀ a ∈ set (concat (map (λ fn. snd (pi fn)) F)). poly_c_max_inter_bcoeff_strict R F pi ≽ a)"
unfolding poly_c_max_inter_bcoeff_strict_def
by (rule poly_c_max_list[OF zero_closed], insert wf_pi, auto)
lemma poly_c_max_inter_bconst:
"poly_c_max_inter_bconst R F pi ∈ carrier R ∧ poly_c_max_inter_bconst R F pi ≽ 𝟬 ∧
(∀ a ∈ set (map (λ fn. fst (pi fn)) F). poly_c_max_inter_bconst R F pi ≽ a)"
unfolding poly_c_max_inter_bconst_def
by (rule poly_c_max_list[OF zero_closed], insert wf_pi, auto)
end
context complexity_linear_poly_order
begin
lemma bound_eval_term_max_derivational:
assumes mono: "⋀ n m. n ≤ m ⟹ g n ≤ g m"
and bG: "⋀ n. bound R ( poly_c_max_inter_bcoeff R F pi (^) n ⊗ (poly_c_max_inter_bconst R F pi)) ≤ g n"
and t: "t ∈ terms_of_nat (Derivational_Complexity F) N"
shows "g N * N ≥ bound R (pi«zero_ass,t>>)"
proof -
let ?bc = "poly_c_max_inter_bcoeff R F pi"
let ?bcv = "poly_c_max_inter_bconst R F pi"
let ?c = "concat (map (λ fn. filter (λ b. ¬ (𝟭 ≽ b)) (snd (pi fn))) F)"
let ?cv = "map (λ fn. fst (pi fn)) F"
have bc: "?bc ∈ carrier R ∧ ?bc ≽ 𝟬 ∧ (∀ a ∈ set ?c. ?bc ≽ a)"
by (rule poly_c_max_inter_bcoeff)
have bcv: "?bcv ∈ carrier R ∧ ?bcv ≽ 𝟬 ∧ (∀ a ∈ set ?cv. ?bcv ≽ a)"
by (rule poly_c_max_inter_bconst)
{
fix fn
assume fn: "fn ∈ set F"
obtain a as where pi: "pi fn = (a,as)" by force
have "bound_entry ?bc ?bcv (pi fn)"
unfolding bound_entry_def pi split
using fn bcv bc pi by force+
} note bound_entry = this
show ?thesis
by (rule bound_eval_term_derivational[OF bound_entry _ _ _ _ mono bG t], insert bc bcv, auto)
qed
lemma bound_eval_term_max_derivational_0:
assumes c0: "poly_c_max_inter_bcoeff_strict R F pi = 𝟬"
shows "∃ c. ∀ t. t ∈ terms_of (Derivational_Complexity F) ⟶ c ≥ bound R (pi«zero_ass,t>>)"
proof -
let ?bc = "poly_c_max_inter_bcoeff_strict R F pi"
let ?bcv = "poly_c_max_inter_bconst R F pi"
let ?c = "concat (map (λ fn. (snd (pi fn))) F)"
let ?cv = "map (λ fn. fst (pi fn)) F"
have bc: "?bc ∈ carrier R ∧ ?bc ≽ 𝟬 ∧ (∀ a ∈ set ?c. ?bc ≽ a)"
by (rule poly_c_max_inter_bcoeff_strict)
have bcv: "?bcv ∈ carrier R ∧ ?bcv ≽ 𝟬 ∧ (∀ a ∈ set ?cv. ?bcv ≽ a)"
by (rule poly_c_max_inter_bconst)
show ?thesis
by (intro exI impI allI, rule bound_eval_term_derivational_0[of F ?bcv],
insert bc bcv c0, auto simp: bound_entry_strict_def)
qed
lemma bound_eval_term_max_runtime_0:
assumes c0: "poly_c_max_inter_bcoeff_strict R C pi = 𝟬"
shows "∃ c. ∀ t. t ∈ terms_of (Runtime_Complexity C D) ⟶ c ≥ bound R (pi«zero_ass,t>>)"
proof -
let ?bc = "poly_c_max_inter_bcoeff_strict R C pi"
let ?bcv = "poly_c_max_inter_bconst R C pi"
let ?c = "concat (map (λ fn. (snd (pi fn))) C)"
let ?cv = "map (λ fn. fst (pi fn)) C"
let ?bd = "poly_c_max_inter_bcoeff_strict R D pi"
let ?bdv = "poly_c_max_inter_bconst R D pi"
let ?d = "concat (map (λ fn. snd (pi fn)) D)"
let ?dv = "map (λ fn. fst (pi fn)) D"
let ?bn = "max_list (map snd D)"
have bd: "?bd ∈ carrier R ∧ ?bd ≽ 𝟬 ∧ (∀ a ∈ set ?d. ?bd ≽ a)"
by (rule poly_c_max_inter_bcoeff_strict)
have bdv: "?bdv ∈ carrier R ∧ ?bdv ≽ 𝟬 ∧ (∀ a ∈ set ?dv. ?bdv ≽ a)"
by (rule poly_c_max_inter_bconst)
have bc: "?bc ∈ carrier R ∧ ?bc ≽ 𝟬 ∧ (∀ a ∈ set ?c. ?bc ≽ a)"
by (rule poly_c_max_inter_bcoeff_strict)
have bcv: "?bcv ∈ carrier R ∧ ?bcv ≽ 𝟬 ∧ (∀ a ∈ set ?cv. ?bcv ≽ a)"
by (rule poly_c_max_inter_bconst)
show ?thesis
by (intro exI impI allI, rule bound_eval_term_runtime_0[of C ?bcv D ?bd ?bdv ?bn],
insert bc bcv c0 bd bdv, auto simp: bound_entry_strict_def max_list)
qed
lemma bound_eval_term_max_runtime:
assumes mono: "⋀ n m. n ≤ m ⟹ g n ≤ g m"
and bG: "⋀ n. bound R (poly_c_max_inter_bcoeff_strict R D pi ⊗ (poly_c_max_inter_bcoeff R C pi (^) n ⊗ (poly_c_max_inter_bconst R C pi))) ≤ g n"
and t: "t ∈ terms_of_nat (Runtime_Complexity C D) N"
shows "bound R (poly_c_max_inter_bconst R D pi) + g N * N * max_list (map snd D) ≥ bound R (pi«zero_ass,t>>)"
proof -
let ?bc = "poly_c_max_inter_bcoeff R C pi"
let ?bcv = "poly_c_max_inter_bconst R C pi"
let ?bd = "poly_c_max_inter_bcoeff_strict R D pi"
let ?bdv = "poly_c_max_inter_bconst R D pi"
let ?c = "concat (map (λ fn. filter (λ b. ¬ (𝟭 ≽ b)) (snd (pi fn))) C)"
let ?d = "concat (map (λ fn. snd (pi fn)) D)"
let ?cv = "map (λ fn. fst (pi fn)) C"
let ?dv = "map (λ fn. fst (pi fn)) D"
have bc: "?bc ∈ carrier R ∧ ?bc ≽ 𝟬 ∧ (∀ a ∈ set ?c. ?bc ≽ a)"
by (rule poly_c_max_inter_bcoeff)
have bcv: "?bcv ∈ carrier R ∧ ?bcv ≽ 𝟬 ∧ (∀ a ∈ set ?cv. ?bcv ≽ a)"
by (rule poly_c_max_inter_bconst)
have bd: "?bd ∈ carrier R ∧ ?bd ≽ 𝟬 ∧ (∀ a ∈ set ?d. ?bd ≽ a)"
by (rule poly_c_max_inter_bcoeff_strict)
have bdv: "?bdv ∈ carrier R ∧ ?bdv ≽ 𝟬 ∧ (∀ a ∈ set ?dv. ?bdv ≽ a)"
by (rule poly_c_max_inter_bconst)
{
fix fn
assume fn: "fn ∈ set C"
obtain a as where pi: "pi fn = (a,as)" by force
have "bound_entry ?bc ?bcv (pi fn)"
unfolding bound_entry_def pi split
using fn bcv bc pi by force+
} note bound_entry = this
{
fix fn
assume fn: "fn ∈ set D"
obtain a as where pi: "pi fn = (a,as)" by force
have "bound_entry_strict ?bd ?bdv (pi fn)"
unfolding bound_entry_strict_def pi split
using fn bdv bd pi by force+
} note bound_entry_strict = this
let ?bn = "max_list (map snd D)"
{
fix fn
assume fn: "fn ∈ set D"
hence "snd fn ∈ set (map snd D)" by simp
from max_list[OF this] have "snd fn ≤ ?bn" .
} note bn = this
show ?thesis
by (rule bound_eval_term_runtime[OF bound_entry _ _ _ _ bound_entry_strict _ _ _ _ _ mono bG t],
insert bc bcv bd bdv bn, auto)
qed
end
context
fixes R :: "('a, 'b) lpoly_order_semiring_scheme" (structure)
begin
fun convert_lpoly_complexity :: "('f, 'a)lpoly_inter ⇒ ('f, 'v) complexity_measure ⇒ complexity_class ⇒ shows check" where
"convert_lpoly_complexity pi cm (Comp_Poly deg) = (let
F = (case cm of Derivational_Complexity F ⇒ F | Runtime_Complexity C D ⇒ C);
bc = poly_c_max_inter_bcoeff R F pi;
bc' = poly_c_max_inter_bcoeff_strict R F pi
in do {
check (deg > 0 ∨ bc' = 𝟬)
(shows ''constant complexity not fully supported for linear (poly/matrix)-interpretations'');
check_complexity R bc (deg - 1)
})"
end
locale linear_poly_order_impl =
fixes C :: "('a :: show)lpoly_order_semiring" (structure)
and check_inter :: "shows check"
assumes carrier: "⋀ as. isOK(check_inter) ⟹ ∃ gt bnd. lpoly_order (C ⦇gt := gt, bound := bnd⦈) ∧
(∀ (a,b) ∈ set as. a ∈ carrier C ⟶ b ∈ carrier C ⟶ a ≻ b ⟶ gt a b) ∧
(psm ⟶
complexity_linear_poly_order_carrier (C ⦇gt := gt, bound := bnd⦈))"
begin
lemma linear_poly_order:
fixes I :: "('f :: {show, key}, 'a) lpoly_interL"
defines [simp]: "II ≡ to_lpoly_inter C I :: ('f, 'a) lpoly_inter"
assumes check_coeffs: "isOK (check_lpoly_coeffs C I)"
and check_inter: "isOK (check_inter)"
shows "∃ (S :: ('f, 'v :: show) trs) NS. ce_af_redtriple_order S NS NS (create_af C I) ∧
(∀ st ∈ set sts. isOK (check_polo_s C II st) ⟶ st ∈ S) ∧
(∀ st ∈ set sts. isOK (check_polo_ns C II st) ⟶ st ∈ NS) ∧
(not_ws_info NS (Some (map fst I))) ∧
(psm ⟶ (cpx_ce_af_redtriple_order S NS NS (create_af C I) (create_mono_af C I) (λ cm cc. isOK(convert_lpoly_complexity C II cm cc))) ∧
(isOK (check_poly_mono C I) ⟶
mono_ce_af_redtriple_order S NS NS (create_af C I) ∧ ctxt.closed S)) ∧
(¬ psm ∧ isOK (check_poly_mono_npsm C (funas_trs_list sts) I) ⟶
mono_ce_af_redtriple_order S NS NS (create_af C I) ∧ ctxt.closed S)"
proof -
let ?as = "[ab. st ← sts, ab ← coeffs_of_constraint C II st]"
from carrier[OF check_inter, of ?as]
obtain gt bnd where carrier:
"lpoly_order (C ⦇gt := gt, bound := bnd⦈)"
and gt: "∀ (a,b) ∈ set ?as. a ∈ carrier C ⟶ b ∈ carrier C ⟶ a ≻ b ⟶ gt a b"
and mono: "psm ⟶ complexity_linear_poly_order_carrier (C ⦇gt := gt, bound := bnd⦈)" by auto
let ?C = "C ⦇gt := gt, bound := bnd⦈"
let ?I = "to_lpoly_inter C I"
let ?II = "to_lpoly_inter ?C I"
let ?pi = "create_af ?C I"
let ?mono_af = "create_mono_af ?C I"
let ?zero = "𝟬⇘?C⇙"
let ?one = "𝟭⇘?C⇙"
let ?arcpos = "arc_pos ⇘?C⇙"
let ?carrier = "carrier ?C"
let ?ge = "op ≽⇘?C⇙"
interpret lpoly_order ?C by fact
have C:
"?carrier = carrier C"
"?arcpos = arc_pos"
"?ge = op ≽"
"?zero = 𝟬"
"?one = 𝟭"
"create_af C I = ?pi"
"create_mono_af C I = ?mono_af"
by auto
interpret linear_poly_order ?C ?II
proof
note [simp] = to_lpoly_inter_def
show "wf_lpoly_inter ?II"
proof (rule conjI, intro allI, unfold C)
fix fn
let ?goal = "λfn. fst (?II fn) ∈ carrier C ∧ (∀a. a ∈ set (snd (?II fn)) ⟶ a ∈ carrier C ∧ (a ≽ 𝟬))"
show "?goal fn"
proof (cases "map_of I fn")
case None
hence repl: "?II fn = (default C, replicate (snd fn) 𝟭)" by auto
have "∀ x ∈ set (replicate (snd fn) 𝟭). x = 𝟭" by (induct "snd fn", auto)
with repl wf_default one_closed one_geq_zero show "?goal fn" by auto
next
case (Some aas)
hence aas: "II fn = aas" by auto
from Some have "(fn ,aas) ∈ set I" by (rule map_of_SomeD)
with check_coeffs have "(fst aas) ∈ carrier C ∧ (∀ a ∈ set (snd aas). a ∈ carrier C ∧ a ≽ 𝟬)"
by (cases fn, cases aas, auto)
with aas show "?goal fn" by auto
qed
next
let ?goal2 = "λ fn. arc_pos (fst (?II fn)) ∨
(∃a∈set (take (snd fn) (snd (?II fn))). arc_pos a)"
show "∀ fn. ?goal2 fn"
proof (intro impI allI)
fix fn
show "?goal2 fn"
proof (cases "map_of I fn")
case None
hence "?II fn = (default C, replicate (snd fn) 𝟭)" by auto
thus "?goal2 fn" using arc_pos_one arc_pos_default by auto
next
case (Some aas)
hence aas: "?II fn = aas" by auto
from Some have "(fn, aas) ∈ set I" by (rule map_of_SomeD)
with check_coeffs have "arc_pos (fst aas) ∨ Bex (set (take (snd fn) (snd aas))) arc_pos" by (cases fn, cases aas, auto)
with aas show "?goal2 fn" by auto
qed
qed
qed
qed
let ?inter_s = "inter_s :: ('f,'v)trs"
let ?inter_ns = "inter_ns :: ('f,'v)trs"
have ws: "not_ws_info ?inter_ns (Some (map fst I))" unfolding not_ws_info.simps
proof (intro allI impI, clarify, intro ws_fun_argI)
fix f n i and ts :: "('f,'v)term list"
assume
nmem: "(f, n) ∉ set (map fst I)"
and n: "length ts = n"
and i: "i < n"
from map_of_eq_None_iff[of I "(f,n)"] nmem
have "map_of I (f, n) = None" by auto
hence default: "?II (f,n) = (default C, replicate n 𝟭)" by (simp add: to_lpoly_inter_def)
show "(Fun f ts, ts ! i) ∈ ?inter_ns"
by (rule default_interpretation_subterm_inter_ns, insert default n i, auto)
qed
interpret ce_af_redtriple_order ?inter_s ?inter_ns ?inter_ns ?pi
proof
show "∃ n. ∀ m ≥ n . ∀ c. ce_trs (c,m) ⊆ inter_ns"
by (rule inter_ns_ce_compat, simp)
show "af_compatible ?pi inter_ns"
by (rule inter_ns_af_compat[OF refl])
qed
have order: "ce_af_redtriple_order ?inter_s inter_ns inter_ns ?pi" ..
{
fix st
assume st: "st ∈ set sts" and ok: "isOK(check_polo_s C ?I st)"
have "st ∈ inter_s"
proof (rule check_polo_s[of "bound C" "op ≻"], simp add: ok, simp)
fix a b
assume mem: "(a,b) ∈ set (coeffs_of_constraint C ?I st)" and ab: "a ≻ b"
and a: "a ∈ carrier C" and b: "b ∈ carrier C"
show "gt a b"
by (rule gt[rule_format, of "(a,b)", unfolded split, rule_format, OF _ a b ab],
insert mem st, auto)
qed
} note S = this
{
fix st
assume st: "st ∈ set sts" and ok: "isOK(check_polo_ns C ?I st)"
have "st ∈ inter_ns"
by (rule check_polo_ns[of "bound C" "op ≻"], insert ok, auto)
} note NS = this
let ?amono = "¬ psm ∧ isOK(check_poly_mono_npsm C (funas_trs_list sts) I)"
show ?thesis
proof (cases ?amono)
case False
hence id: "?amono = False" by simp
show ?thesis unfolding id C
proof (intro exI conjI allI ballI,
rule order,
(intro impI, rule S, auto)[1],
(intro impI, rule NS, auto)[1],
rule ws,
intro impI, rule conjI)
assume psm
from mono ‹psm› have "complexity_linear_poly_order_carrier ?C"
by auto
interpret complexity_linear_poly_order_carrier ?C by fact
interpret complexity_linear_poly_order ?C ?II ..
show "isOK(check_poly_mono C I) ⟶
mono_ce_af_redtriple_order ?inter_s inter_ns inter_ns ?pi ∧ ctxt.closed inter_s"
proof
assume ok: "isOK(check_poly_mono C I)"
interpret mono_linear_poly_order ?C ?II
by (unfold_locales, rule check_poly_mono_sound,
insert ok, auto simp: check_poly_mono_def)
interpret mono_ce_af_redtriple_order ?inter_s inter_ns inter_ns ?pi
by (unfold_locales, rule inter_s_ce_compat[OF refl])
show "mono_ce_af_redtriple_order ?inter_s inter_ns inter_ns ?pi ∧ ctxt.closed inter_s"
by (rule conjI[OF _ inter_s_mono], unfold_locales)
qed
let ?conv' = "convert_lpoly_complexity C II :: ('f,'v)complexity_measure ⇒ complexity_class ⇒ shows check"
let ?conv = "convert_lpoly_complexity ?C ?II :: ('f,'v)complexity_measure ⇒ complexity_class ⇒ shows check"
show "cpx_ce_af_redtriple_order ?inter_s inter_ns inter_ns ?pi ?mono_af (λ cm cc. isOK(?conv' cm cc))"
proof
fix cm cc
assume ok: "isOK(?conv' cm cc)"
obtain deg where cc_deg: "cc = Comp_Poly deg" by (cases cc, auto)
have "?conv' cm cc = ?conv cm cc"
by (auto simp: poly_c_max_inter_bcoeff_def poly_c_max_inter_bcoeff_strict_def Let_def cc_deg)
with ok have conv: "isOK(?conv cm cc)" by simp
let ?bcF = "λ F. poly_c_max_inter_bcoeff ?C F ?II"
let ?smone = "λ F. if (𝟭 ≽ (?bcF F)) then succeed else check_complexity C (?bcF F) deg"
let ?d1 = "deg - 1"
from conv cc_deg obtain F D where choice: "cm = Derivational_Complexity F ∨ cm = Runtime_Complexity F D"
and cc: "isOK(check_complexity ?C (?bcF F) ?d1)"
by (auto split: complexity_measure.splits)
let ?F = "get_signature_of_cm cm"
let ?bc = "?bcF F"
let ?bcv = "poly_c_max_inter_bconst ?C F ?II"
let ?bd = "poly_c_max_inter_bcoeff_strict ?C D ?II"
let ?bc' = "poly_c_max_inter_bcoeff_strict ?C F ?II"
from conv cc_deg choice have deg: "?bc' = 𝟬 ∨ Suc ?d1 = deg" by auto
from poly_c_max_inter_bcoeff[of F] have wfbc: "?bc ∈ carrier ?C" and gebc: "?bc ≽⇘?C⇙ 𝟬⇘?C⇙" by auto
from poly_c_max_inter_bcoeff_strict[of D] have wfbd: "?bd ∈ carrier ?C" and gebd: "?bd ≽⇘?C⇙ 𝟬⇘?C⇙" by auto
from poly_c_max_inter_bconst[of F] have wfbcv: "?bcv ∈ carrier ?C" and gebcv: "?bcv ≽⇘?C⇙ 𝟬⇘?C⇙" by auto
from arc_pos_True have apos: "apos_ass zero_ass" unfolding apos_ass_def by simp
let ?eval = "λ t :: ('f,'v)term. eval_term ?II zero_ass t"
let ?S = "{(a,b). a ∈ carrier ?C ∧ b ∈ carrier ?C ∧ b ≽ 𝟬 ∧ arc_pos b ∧ gt a b}"
{
fix s t
assume "(s,t) ∈ ?inter_s"
from this[unfolded inter_s_def]
have "⋀ α. wf_ass ?C α ⟹ pos_ass α ⟹ apos_ass α ⟹ gt (eval_term II α s) (eval_term II α t)"
by auto
from this[OF wf_zero_ass pos_zero_ass apos]
have gt: "gt (?eval s) (?eval t)" by auto
from pos_term[OF wf_zero_ass pos_zero_ass] have ge: "(?eval t) ≽ 𝟬" by auto
from apos_term[OF wf_zero_ass apos] have apos: "arc_pos (?eval t)" by auto
from ge gt apos wf_terms[OF wf_zero_ass] have "(?eval s,?eval t) ∈ ?S" by (auto simp: Let_def)
} note image = this
{
fix bd
assume wfbd: "bd ∈ carrier ?C" and gebd: "bd ≽⇘?C⇙ 𝟬⇘?C⇙"
have "∃ g. g ∈ O_of (Comp_Poly (deg - 1)) ∧ (∀ n. bound ?C (bd ⊗⇘?C⇙ ( (?bc (^)⇘?C⇙ n) ⊗⇘?C⇙ ?bcv)) ≤ g n)"
by (rule complexity_cond[OF wfbc wfbcv wfbd gebc gebcv gebd cc])
} note get_g = this
from choice
have "∃ c d g. g ∈ complexity_of (Comp_Poly ?d1) ∧ (∀ n t. t ∈ terms_of_nat cm n ⟶ bound ?C (?eval t) ≤ c + g n * n * d)"
proof
assume cm: "cm = Derivational_Complexity F"
from get_g[OF one_closed one_geq_zero] obtain g where g: "g ∈ O_of (Comp_Poly ?d1)"
and bnd2: "⋀ n. bound ?C (𝟭 ⊗ (?bc (^) n ⊗ ?bcv)) ≤ g n" by auto
from g[unfolded O_of_def] obtain gg where gg: "gg ∈ complexity_of (Comp_Poly ?d1)" and ggg: "⋀ n. g n ≤ gg n" by auto
{
fix n :: nat
have "?bc (^) n ⊗⇘?C⇙ ?bcv = 𝟭 ⊗ (?bc (^) n ⊗ ?bcv)"
using l_one[OF m_closed[OF nat_pow_closed[OF wfbc] wfbcv]] by simp
moreover from le_trans[OF bnd2[of n] ggg] have "bound ?C (𝟭 ⊗ (?bc (^) n ⊗ ?bcv)) ≤ gg n" by auto
ultimately have "bound ?C (?bc (^)⇘?C⇙ n ⊗⇘?C⇙ ?bcv) ≤ gg n" by auto
} note bnd2 = this
from complexity_poly_mono[OF gg] have gg_mono: "⋀ n m. n ≤ m ⟹ gg n ≤ gg m" .
from bound_eval_term_max_derivational[of gg, OF gg_mono bnd2]
have bound2: "⋀ t N. t ∈ terms_of_nat cm N ⟹ bound ?C (?eval t) ≤ gg N * N"
unfolding cm by auto
show ?thesis
by (rule exI[of _ 0], rule exI[of _ 1], rule exI, rule conjI[OF gg], insert bound2, auto)
next
assume cm: "cm = Runtime_Complexity F D"
from get_g[OF wfbd gebd] obtain g where g: "g ∈ O_of (Comp_Poly ?d1)"
and bnd2: "⋀ n. bound ?C (?bd ⊗ (?bc (^) n ⊗ ?bcv)) ≤ g n" by auto
from g[unfolded O_of_def] obtain gg where gg: "gg ∈ complexity_of (Comp_Poly ?d1)" and ggg: "⋀ n. g n ≤ gg n" by auto
from le_trans[OF bnd2 ggg] have bnd2: "⋀ n. bound ?C (?bd ⊗⇘?C⇙ (?bc (^)⇘?C⇙ n ⊗⇘?C⇙ ?bcv)) ≤ gg n" by auto
from complexity_poly_mono[OF gg] have gg_mono: "⋀ n m. n ≤ m ⟹ gg n ≤ gg m" .
let ?bn = "max_list (map snd D)"
let ?bdv = "poly_c_max_inter_bconst ?C D ?II"
from bound_eval_term_max_runtime[of gg, OF gg_mono bnd2]
have bound2: "⋀ t N. t ∈ terms_of_nat cm N ⟹ bound ?C (?eval t) ≤ bound ?C ?bdv + gg N * N * ?bn"
unfolding cm by auto
show ?thesis
by (rule exI[of _ "bound ?C ?bdv"], rule exI[of _ ?bn], rule exI, rule conjI[OF gg], insert bound2, auto)
qed
then obtain c d g where g: "g ∈ complexity_of (Comp_Poly ?d1)"
and bound2: "⋀ n t. t ∈ terms_of_nat cm n ⟹ bound ?C (?eval t) ≤ c + g n * n * d" by blast
from g[simplified] obtain c' e where g: "g = (λ n. c' * n ^ ?d1 + e)" by auto
obtain c'' where c'': "c'' = c' * d + e * d" by auto
let ?h = "(λ n. c'' * n ^ Suc ?d1 + c)"
obtain h where h: "h = ?h" by auto
{
fix n :: nat
{
assume n: "1 ≤ n"
have le: "(e * d) * (n * 1) ≤ (e * d) * (n * n ^ ?d1)"
by (rule mult_left_mono[OF mult_left_mono[OF one_le_power[OF n]]], auto)
have "c + g n * n * d = c + (c' * d) * (n ^ Suc ?d1) + (e * d * n)" unfolding g
by (simp add: field_simps)
also have "... ≤ h n" unfolding h c'' using le by (simp add: field_simps)
finally have "c + g n * n * d ≤ h n" .
} note le = this
have "c + g n * n * d ≤ h n" using le unfolding h g c'' by (cases n, auto simp: field_simps)
}
from le_trans[OF bound2 this] have bound2: "⋀ t n . t ∈ terms_of_nat cm n ⟹ bound ?C (?eval t) ≤ h n" .
from deg have "∃ c d. ∀ t n. t ∈ terms_of_nat cm n ⟶ bound ?C (?eval t) ≤ c * n ^ deg + d"
proof
assume deg: "Suc ?d1 = deg"
show ?thesis using bound2 unfolding h deg by blast
next
assume "?bc' = 𝟬"
hence 0: "?bc' = ?zero" by simp
have "∃ c. ∀ t. t ∈ terms_of cm ⟶ bound ?C (?eval t) ≤ c"
using choice
proof
assume "cm = Derivational_Complexity F"
with bound_eval_term_max_derivational_0[OF 0]
show ?thesis by blast
next
assume "cm = Runtime_Complexity F D"
with bound_eval_term_max_runtime_0[OF 0]
show ?thesis by blast
qed
then obtain c where bnd: "⋀ t n. t ∈ terms_of_nat cm n ⟹ bound ?C (?eval t) ≤ c"
unfolding terms_of by auto
show ?thesis
by (rule exI[of _ 0], rule exI[of _ c], insert bnd, auto)
qed
then obtain c d where bound2: "⋀ t n. t ∈ terms_of_nat cm n ⟹ bound ?C (?eval t) ≤ c * n ^ deg + d" by auto
let ?h = "λ n. c * n ^ deg + d"
have one: "⋀ t n. ⟦t ∈ terms_of_nat cm n⟧
⟹ deriv_bound ?inter_s t (?h n)"
by (rule deriv_bound_image[of _ ?eval, OF deriv_bound_mono[OF bound2 bound]], insert image, auto)
show deriv_bound: "deriv_bound_measure_class ?inter_s cm cc" unfolding cc
unfolding deriv_bound_measure_class_def cc_deg
by (rule deriv_bound_rel_class_polyI[of _ _ c _ d], insert one, auto)
next
show "af_monotone ?mono_af ?inter_s"
by (rule pre_mono_linear_poly_order.create_mono_af[OF _ refl], unfold_locales)
qed
qed simp
next
case True
hence npsm: "isOK(check_poly_mono_npsm C (funas_trs_list sts) I)" and nmono: "¬ psm" by auto
from npsm have npsm: "isOK(check_poly_mono_npsm ?C (funas_trs_list sts) I)"
unfolding check_poly_mono_npsm_def by auto
let ?F = "funas_trs (set sts)"
interpret npsm_mono_linear_poly_order ?C ?II ?F
by (unfold_locales, insert check_poly_mono_npsm_sound[OF npsm] nmono, auto)
let ?x = "Var undefined :: ('f,'v)term"
def R_ws ≡ "{(Fun f [?x], ?x) | f. (f,1) ∉ fst ` set I ∧ (f,1) ∈ ?F} :: ('f,'v)trs"
have R_ws: "R_ws ⊆ ?inter_ns" unfolding R_ws_def
proof (clarify)
fix f
assume "(f,1) ∉ fst ` set I"
with ws[unfolded not_ws_info.simps ws_fun_arg_def, rule_format, of "(f,1)" 0 "[?x]"]
show "(Fun f [?x], ?x) ∈ ?inter_ns" by auto
qed
have R_wsF: "funas_trs R_ws ⊆ ?F" unfolding R_ws_def funas_trs_def
by (auto simp: funas_rule_def)
obtain R where R: "R = set (filter (λ st. isOK(check_polo_s C II st)) sts)" by auto
obtain Rw where Rw: "Rw = R_ws ∪ set (filter (λ st. isOK(check_polo_ns C II st)) sts)" by auto
from S R have RS: "R ⊆ inter_s" by auto
from NS Rw R_ws have RwNS: "Rw ⊆ inter_ns" by auto
from R Rw R_wsF have F: "funas_trs R ⊆ ?F" "funas_trs Rw ⊆ ?F" unfolding funas_trs_def by auto
let ?Ce = "⋃(ce_trs ` UNIV) :: ('f,'v)trs"
let ?ST = "{(Fun f ts, t) |f ts t. t ∈ set ts ∧ (f, length ts) ∉ ?F}"
let ?R = "rstep (R ∪ ?ST)"
let ?Rw = "rstep (Rw ∪ ?ST)"
from rel_subterm_terminating[OF F RS RwNS subset_refl] have
SN_rel: "SN_rel (?R) (?Rw)" .
let ?S = "(relto (?R) (?Rw))^+"
let ?NS = "(?R ∪ ?Rw)^*"
interpret mono_ce_af_redtriple_order ?S ?NS ?NS ?pi
proof (rule ce_SN_rel_imp_redtriple[OF SN_rel])
fix f and n :: nat
show "?pi (f, n) = {0 ..< n}"
proof (cases "map_of I (f, n)")
case None
thus ?thesis unfolding create_af_def by auto
next
case (Some ccs)
then obtain c cs where look: "map_of I (f, n) = Some (c,cs)" by force
from map_of_SomeD[OF look] have mem: "((f,n),(c,cs)) ∈ set I" by auto
with check_coeffs have apos: "arc_pos c ∨ Bex (set (take n cs)) arc_pos"
and len: "length cs ≤ n" by auto
from mem have "(f,n) ∈ set (map fst I)" by force
with check_poly_mono_npsm_sound[OF npsm]
have mono: "n ≤ Suc 0" "n = Suc 0 ⟹ fst (?II (f,n)) = 𝟬 ∧ length (snd (?II (f,n))) = Suc 0" by force+
from look have II: "?II (f,n) = (c,cs)" unfolding to_lpoly_inter_def by auto
note mono = mono[unfolded II fst_conv snd_conv]
show ?thesis
proof (cases n)
case (Suc n')
with mono have n: "n = Suc 0" by auto
from mono(2)[OF this] obtain d where c: "c = 𝟬" and cs: "cs = [d]" by (cases cs, auto)
from apos[unfolded c n cs] arc_pos_zero[OF mode]
have ad: "arc_pos d" by auto
with arc_pos_zero[OF mode] have d: "d ≠ 𝟬" by auto
show ?thesis unfolding create_af_def look cs Let_def ceta_map_of fun_of_map_fun'.simps
using d n by auto
next
case 0
thus ?thesis unfolding create_af_def look ceta_map_of fun_of_map_fun'.simps
using len by auto
qed
qed
qed (insert F_unary, force simp: ce_trs.simps)
show ?thesis unfolding C
proof (rule exI[of _ ?S], rule exI[of _ ?NS], intro conjI impI ballI)
show "ce_af_redtriple_order ?S ?NS ?NS ?pi" ..
next
fix st
assume "st ∈ set sts" and "isOK(check_polo_s C II st)"
hence "st ∈ ?R" unfolding R by (cases st rule: prod.exhaust) (auto)
also have "?R ⊆ ?S" unfolding relto_trancl_conv by regexp
finally show "st ∈ ?S" .
next
fix st
assume "st ∈ set sts" and "isOK(check_polo_ns C II st)"
hence "st ∈ ?Rw" unfolding Rw by (cases st rule: prod.exhaust) (auto)
also have "?Rw ⊆ ?NS" by regexp
finally show "st ∈ ?NS" .
next
show "mono_ce_af_redtriple_order ?S ?NS ?NS ?pi" ..
show "mono_ce_af_redtriple_order ?S ?NS ?NS ?pi" ..
show "ctxt.closed ?S" unfolding relto_trancl_conv by blast
next
show "not_ws_info ?NS (Some (map fst I))" unfolding not_ws_info.simps
proof (intro allI impI)
fix fn i
assume nmem: "fn ∉ set (map fst I)"
then obtain f n where f: "fn = (f,n)" by force
show "ws_fun_arg ?NS fn i" unfolding f
proof (rule ws_fun_argI)
fix ts :: "('f,'v)term list"
assume len: "length ts = n" and i: "i < n"
hence t: "ts ! i ∈ set ts" by auto
let ?f = "(f,length ts)"
have "(Fun f ts, ts ! i) ∈ ?Rw"
proof (cases "?f ∈ ?F")
case False
thus ?thesis using t by auto
next
case True
from F_unary[OF this] t have ts: "length ts = 1" by (cases ts, auto)
with i[folded len] obtain t where ts: "ts = [t]" and i: "i = 0" by (cases ts, auto)
with True f len nmem have rule: "⋀ R. (Fun f [?x], ?x) ∈ Rw ∪ R"
unfolding Rw R_ws_def by auto
show ?thesis unfolding ts i
by (rule rstepI[OF rule, of _ Hole "λ _. t"], auto)
qed
thus "(Fun f ts, ts ! i) ∈ ?NS" by regexp
qed
qed
qed (insert nmono, auto)
qed
qed
end
context
fixes C :: "('a :: show)lpoly_order_semiring" (structure)
begin
definition create_lpoly_repr :: "('f::{key,show},'a::show)lpoly_interL ⇒ shows"
where "create_lpoly_repr I = (let pi = to_lpoly_inter C I in (
''polynomial interpretration over '' +#+ description C +#+ shows_nl +@+ (shows_sep (λ(f,n).
let t = Fun f (map Var (fresh_strings_list ''x_'' 1 [] n)) in (
''Pol('' +#+ shows t +@+ '') = '' +#+
shows_lpoly C (PleftI C pi t)
)) shows_nl (remdups (map fst I)))))"
definition create_poly_redtriple :: "shows check ⇒ ('f :: {show,key}, 'a :: show)lpoly_interL ⇒ ('f,'v :: show)redtriple"
where "create_poly_redtriple cI I = (let pi = to_lpoly_inter C I; ns = check_polo_ns C pi in
⦇redtriple.valid = do {cI; check_lpoly_coeffs C I},
s = check_polo_s C pi,
ns = ns, nst = ns,
af = create_af C I,
mono_af = create_mono_af C I,
mono = (λ s_ns_nst. if psm then check_poly_mono C I else check_poly_mono_npsm C (funas_trs_list s_ns_nst) I),
desc = create_lpoly_repr I,
not_ws_ns = Some (map fst I),
cpx = (if psm then convert_lpoly_complexity C pi else no_complexity_check) ⦈)"
lemma create_poly_redtriple:
assumes "linear_poly_order_impl C check_inter"
shows "generic_redtriple_impl (create_poly_redtriple check_inter)"
proof
fix I :: "('f :: {show,key},'a) lpoly_interL" and s_list ns_list nst_list :: "('f,'v :: show)rule list" and π
let ?c = "create_poly_redtriple check_inter I :: ('f,'v)redtriple"
let ?pi = "redtriple.af ?c :: 'f af"
let ?mono_af = "redtriple.mono_af ?c :: 'f af"
assume valid: "isOK (redtriple.valid ?c)" and
check_s: "isOK(check_allm (redtriple.s ?c) s_list)" and
check_ns: "isOK(check_allm (redtriple.ns ?c) ns_list)" and
check_nst: "isOK(check_allm (redtriple.nst ?c) nst_list)"
from valid have carrier_valid: "isOK (check_inter)" and polo_valid: "isOK(check_lpoly_coeffs C I)" unfolding create_poly_redtriple_def by (auto simp: Let_def)
let ?I = "to_lpoly_inter C I :: ('f,'a)lpoly_inter"
let ?cpx = "redtriple.cpx ?c"
let ?cpx' = "λ cm cc. isOK(redtriple.cpx ?c cm cc)"
let ?all = "s_list @ ns_list @ nst_list"
interpret linear_poly_order_impl C check_inter by fact
from linear_poly_order[of I ?all, OF polo_valid carrier_valid] obtain S NS cpx where order: "ce_af_redtriple_order S NS NS ?pi"
and S: "(∀ st ∈ set ?all. isOK(check_polo_s C ?I st) ⟶ st ∈ S)"
and NS: "(∀ st ∈ set ?all. isOK(check_polo_ns C ?I st) ⟶ st ∈ NS)"
and cpx: "psm ⟹ cpx_ce_af_redtriple_order S NS NS ?pi ?mono_af (λ cm cc. isOK(convert_lpoly_complexity C ?I cm cc))"
and ws: "not_ws_info NS (Some (map fst I))"
and mono: "psm ⟹ isOK(check_poly_mono C I) ⟹ mono_ce_af_redtriple_order S NS NS ?pi ∧ ctxt.closed S"
and nmono: "¬ psm ⟹ isOK(check_poly_mono_npsm C (funas_trs_list ?all) I) ⟹ mono_ce_af_redtriple_order S NS NS ?pi ∧ ctxt.closed S"
unfolding create_poly_redtriple_def Let_def redtriple.simps by blast
interpret ce_af_redtriple_order S NS NS ?pi by fact
have order: "cpx_ce_af_redtriple_order S NS NS ?pi ?mono_af ?cpx'"
proof (cases psm)
case True
show ?thesis using cpx[OF True] True
unfolding create_poly_redtriple_def Let_def by simp
next
case False
hence id: "?cpx = no_complexity_check" "?mono_af = empty_af" unfolding create_poly_redtriple_def Let_def
by (auto simp: create_mono_af_def)
show ?thesis unfolding id
by (unfold_locales, force simp: no_complexity_check_def, rule empty_af)
qed
from check_s[unfolded create_poly_redtriple_def Let_def] S have S: "set s_list ⊆ S" by auto
from check_nst[unfolded create_poly_redtriple_def Let_def] NS have NST: "set nst_list ⊆ NS" by auto
from check_ns[unfolded create_poly_redtriple_def Let_def] NS have NS: "set ns_list ⊆ NS" by auto
let ?ws = "redtriple.not_ws_ns ?c"
have ws: "not_ws_info NS ?ws" using ws
by (auto simp: create_poly_redtriple_def Let_def)
show "∃ S NS NST. cpx_ce_af_redtriple_order S NS NST ?pi ?mono_af ?cpx'
∧ set s_list ⊆ S ∧ set ns_list ⊆ NS ∧ set nst_list ⊆ NST ∧
not_ws_info NS ?ws ∧
(isOK (redtriple.mono ?c ?all) ⟶ mono_ce_af_redtriple_order S NS NST ?pi ∧ ctxt.closed S)"
proof (intro exI conjI, rule order, rule S, rule NS, rule NST, rule ws, intro impI)
assume ok: "isOK(redtriple.mono ?c ?all)"
note ok = ok[unfolded create_poly_redtriple_def Let_def, simplified]
show "mono_ce_af_redtriple_order S NS NS ?pi ∧ ctxt.closed S"
proof (cases psm)
case True
with ok have "isOK (check_poly_mono C I)" by simp
from mono[OF True this] show ?thesis .
next
case False
with ok have "isOK(check_poly_mono_npsm C (funas_trs_list ?all) I)"
by simp
from nmono[OF False this] show ?thesis .
qed
qed
qed
end
context lpoly_order
begin
declare poly_simps[simp del] poly_order_simps[simp del]
end
no_notation arcpos ("arc'_posı")
end