# Theory Affine_Arithmetic_Auxiliarities

theory Affine_Arithmetic_Auxiliarities
imports "HOL-Analysis.Multivariate_Analysis"
begin

subsection ‹@{term sum_list}›

lemma sum_list_nth_eqI:
shows
"length xs = length ys ⟹ (⋀x y. (x, y) ∈ set (zip xs ys) ⟹ x = y) ⟹
sum_list xs = sum_list ys"
by (induct xs ys rule: list_induct2) auto

lemma fst_sum_list: "fst (sum_list xs) = sum_list (map fst xs)"
by (induct xs) auto

lemma snd_sum_list: "snd (sum_list xs) = sum_list (map snd xs)"
by (induct xs) auto

lemma take_greater_eqI: "take c xs = take c ys ⟹ c ≥ a ⟹ take a xs = take a ys"
proof (induct xs arbitrary: a c ys)
case (Cons x xs) note ICons = Cons
thus ?case
proof (cases a)
case (Suc b)
thus ?thesis using Cons(2,3)
proof (cases ys)
case (Cons z zs)
from ICons obtain d where c: "c = Suc d"
by (auto simp: Cons Suc dest!: Suc_le_D)
show ?thesis
using ICons(2,3)
by (auto simp: Suc Cons c intro: ICons(1))
qed simp
qed simp
qed (metis le_0_eq take_eq_Nil)

lemma take_max_eqD:
"take (max a b) xs = take (max a b) ys ⟹ take a xs = take a ys ∧ take b xs = take b ys"
by (metis max.cobounded1 max.cobounded2 take_greater_eqI)

lemma take_Suc_eq: "take (Suc n) xs = (if n < length xs then take n xs @ [xs ! n] else xs)"
by (auto simp: take_Suc_conv_app_nth)

definition "rad_of w = w * pi / 180"

definition "deg_of w = 180 * w / pi"

and deg_of_inverse[simp]: "rad_of (deg_of w) = w"

lemma deg_of_monoI: "x ≤ y ⟹ deg_of x ≤ deg_of y"
by (auto simp: deg_of_def intro!: divide_right_mono)

lemma deg_of_strict_monoI: "x < y ⟹ deg_of x < deg_of y"
by (auto simp: deg_of_def intro!: divide_strict_right_mono)

lemma deg_of_mono[simp]: "deg_of x ≤ deg_of y ⟷ x ≤ y"
by (fastforce intro!: deg_of_monoI)

by (fastforce intro!: deg_of_monoI)

lemma deg_of_strict_mono[simp]: "deg_of x < deg_of y ⟷ x < y"
by (fastforce intro!: deg_of_strict_monoI)

by (fastforce intro!: deg_of_strict_monoI)

by auto

end


# Theory Executable_Euclidean_Space

section ‹Euclidean Space: Executability›
theory Executable_Euclidean_Space
imports
"HOL-Analysis.Multivariate_Analysis"
"List-Index.List_Index"
"HOL-Library.Float"
Affine_Arithmetic_Auxiliarities
begin

subsection ‹Ordered representation of Basis and Rounding of Components›

class executable_euclidean_space = ordered_euclidean_space +
fixes Basis_list eucl_down eucl_truncate_down eucl_truncate_up
assumes eucl_down_def:
"eucl_down p b = (∑i ∈ Basis. round_down p (b ∙ i) *⇩R i)"
assumes eucl_truncate_down_def:
"eucl_truncate_down q b = (∑i ∈ Basis. truncate_down q (b ∙ i) *⇩R i)"
assumes eucl_truncate_up_def:
"eucl_truncate_up q b = (∑i ∈ Basis. truncate_up q (b ∙ i) *⇩R i)"
assumes Basis_list[simp]: "set Basis_list = Basis"
assumes distinct_Basis_list[simp]: "distinct Basis_list"
begin

lemma length_Basis_list:
"length Basis_list = card Basis"
by (metis Basis_list distinct_Basis_list distinct_card)

end

lemma eucl_truncate_down_zero[simp]: "eucl_truncate_down p 0 = 0"
by (auto simp: eucl_truncate_down_def truncate_down_zero)

lemma eucl_truncate_up_zero[simp]: "eucl_truncate_up p 0 = 0"
by (auto simp: eucl_truncate_up_def)

subsection ‹Instantiations›

instantiation real::executable_euclidean_space
begin

definition Basis_list_real :: "real list" where
"Basis_list_real = [1]"

definition "eucl_down prec b = round_down prec b"
definition "eucl_truncate_down prec b = truncate_down prec b"
definition "eucl_truncate_up prec b = truncate_up prec b"

instance proof qed (auto simp: Basis_list_real_def eucl_down_real_def eucl_truncate_down_real_def
eucl_truncate_up_real_def)

end

instantiation prod::(executable_euclidean_space, executable_euclidean_space)
executable_euclidean_space
begin

definition Basis_list_prod :: "('a × 'b) list" where
"Basis_list_prod =
zip Basis_list (replicate (length (Basis_list::'a list)) 0) @
zip (replicate (length (Basis_list::'b list)) 0) Basis_list"

definition "eucl_down p a = (eucl_down p (fst a), eucl_down p (snd a))"
definition "eucl_truncate_down p a = (eucl_truncate_down p (fst a), eucl_truncate_down p (snd a))"
definition "eucl_truncate_up p a = (eucl_truncate_up p (fst a), eucl_truncate_up p (snd a))"

instance
proof
show "set Basis_list = (Basis::('a*'b) set)"
by (auto simp: Basis_list_prod_def Basis_prod_def elim!: in_set_zipE)
(auto simp: Basis_list[symmetric] in_set_zip in_set_conv_nth simp del: Basis_list)
show "distinct (Basis_list::('a*'b)list)"
using distinct_Basis_list[where 'a='a] distinct_Basis_list[where 'a='b]
by (auto simp: Basis_list_prod_def Basis_list intro: distinct_zipI1 distinct_zipI2
elim!: in_set_zipE)
qed
(auto simp: eucl_down_prod_def eucl_truncate_down_prod_def eucl_truncate_up_prod_def
eucl_truncate_down_def eucl_truncate_up_def
intro!: euclidean_eqI[where 'a="'a*'b"])

end

lemma eucl_truncate_down_Basis[simp]:
"i ∈ Basis ⟹ eucl_truncate_down e x ∙ i = truncate_down e (x ∙ i)"

lemma eucl_truncate_down_correct:
"dist (x::'a::executable_euclidean_space) (eucl_down e x) ∈
{0..sqrt (DIM('a)) * 2 powr of_int (- e)}"
proof -
have "dist x (eucl_down e x) = sqrt (∑i∈Basis. (dist (x ∙ i) (eucl_down e x ∙ i))⇧2)"
unfolding euclidean_dist_l2[where 'a='a] L2_set_def ..
also have "… ≤ sqrt (∑i∈(Basis::'a set). ((2 powr of_int (- e))⇧2))"
by (intro real_sqrt_le_mono sum_mono power_mono)
(auto simp: dist_real_def eucl_down_def abs_round_down_le)
finally show ?thesis
qed

lemma eucl_down: "eucl_down e (x::'a::executable_euclidean_space) ≤ x"
by (auto simp add: eucl_le[where 'a='a] round_down eucl_down_def)

lemma eucl_truncate_down: "eucl_truncate_down e (x::'a::executable_euclidean_space) ≤ x"
by (auto simp add: eucl_le[where 'a='a] truncate_down)

lemma eucl_truncate_down_le:
"x ≤ y ⟹ eucl_truncate_down w x ≤ (y::'a::executable_euclidean_space)"
using eucl_truncate_down
by (rule order.trans)

lemma eucl_truncate_up_Basis[simp]: "i ∈ Basis ⟹ eucl_truncate_up e x ∙ i = truncate_up e (x ∙ i)"

lemma eucl_truncate_up: "x ≤ eucl_truncate_up e (x::'a::executable_euclidean_space)"
by (auto simp add: eucl_le[where 'a='a] round_up truncate_up_def)

lemma eucl_truncate_up_le: "x ≤ y ⟹ x ≤ eucl_truncate_up e (y::'a::executable_euclidean_space)"
using _ eucl_truncate_up
by (rule order.trans)

lemma eucl_truncate_down_mono:
fixes x::"'a::executable_euclidean_space"
shows "x ≤ y ⟹ eucl_truncate_down p x ≤ eucl_truncate_down p y"
by (auto simp: eucl_le[where 'a='a] intro!: truncate_down_mono)

lemma eucl_truncate_up_mono:
fixes x::"'a::executable_euclidean_space"
shows "x ≤ y ⟹ eucl_truncate_up p x ≤ eucl_truncate_up p y"
by (auto simp: eucl_le[where 'a='a] intro!: truncate_up_mono)

lemma infnorm[code]:
fixes x::"'a::executable_euclidean_space"
shows "infnorm x = fold max (map (λi. abs (x ∙ i)) Basis_list) 0"
by (auto simp: Max.set_eq_fold[symmetric] infnorm_Max[symmetric] infnorm_pos_le
intro!: max.absorb2[symmetric])

declare Inf_real_def[code del]
declare Sup_real_def[code del]
declare Inf_prod_def[code del]
declare Sup_prod_def[code del]
declare [[code abort: "Inf::real set ⇒ real"]]
declare [[code abort: "Sup::real set ⇒ real"]]
declare [[code abort: "Inf::('a::Inf * 'b::Inf) set ⇒ 'a * 'b"]]
declare [[code abort: "Sup::('a::Sup * 'b::Sup) set ⇒ 'a * 'b"]]

lemma nth_Basis_list_in_Basis[simp]:
"n < length (Basis_list::'a::executable_euclidean_space list) ⟹ Basis_list ! n ∈ (Basis::'a set)"
by (metis Basis_list nth_mem)

subsection ‹Representation as list›

lemma nth_eq_iff_index:
"distinct xs ⟹ n < length xs ⟹ xs ! n = i ⟷ n = index xs i"
using index_nth_id by fastforce

lemma in_Basis_index_Basis_list: "i ∈ Basis ⟹ i = Basis_list ! index Basis_list i"
by simp

lemmas [simp] = length_Basis_list

lemma sum_Basis_sum_nth_Basis_list:
"(∑i∈Basis. f i) = (∑i<DIM('a::executable_euclidean_space). f ((Basis_list::'a list) ! i))"
apply (rule sum.reindex_cong[OF _ _ refl])
apply (auto intro!: inj_on_nth)
by (metis Basis_list image_iff in_Basis_index_Basis_list index_less_size_conv length_Basis_list lessThan_iff)

definition "eucl_of_list xs = (∑(x, i)←zip xs Basis_list. x *⇩R i)"

lemma eucl_of_list_nth:
assumes "length xs = DIM('a)"
shows "eucl_of_list xs = (∑i<DIM('a::executable_euclidean_space). (xs ! i) *⇩R ((Basis_list::'a list) ! i))"
by (auto simp: eucl_of_list_def sum_list_sum_nth length_Basis_list assms atLeast0LessThan)

lemma eucl_of_list_inner:
fixes i::"'a::executable_euclidean_space"
assumes i: "i ∈ Basis"
assumes l: "length xs = DIM('a)"
shows "eucl_of_list xs ∙ i = xs ! (index Basis_list i)"
by (simp add: eucl_of_list_nth[OF l] inner_sum_left assms inner_Basis
nth_eq_iff_index sum.delta if_distrib cong: if_cong)

lemma inner_eucl_of_list:
fixes i::"'a::executable_euclidean_space"
assumes i: "i ∈ Basis"
assumes l: "length xs = DIM('a)"
shows "i ∙ eucl_of_list xs = xs ! (index Basis_list i)"
using eucl_of_list_inner[OF assms] by (auto simp: inner_commute)

definition "list_of_eucl x = map ((∙) x) Basis_list"

lemma index_Basis_list_nth[simp]:
"i < DIM('a::executable_euclidean_space) ⟹ index Basis_list ((Basis_list::'a list) ! i) = i"

lemma list_of_eucl_eucl_of_list[simp]:
"length xs = DIM('a::executable_euclidean_space) ⟹ list_of_eucl (eucl_of_list xs::'a) = xs"
by (auto simp: list_of_eucl_def eucl_of_list_inner intro!: nth_equalityI)

lemma eucl_of_list_list_of_eucl[simp]:
"eucl_of_list (list_of_eucl x) = x"
by (auto simp: list_of_eucl_def eucl_of_list_inner intro!: euclidean_eqI[where 'a='a])

lemma length_list_of_eucl[simp]: "length (list_of_eucl (x::'a::executable_euclidean_space)) = DIM('a)"
by (auto simp: list_of_eucl_def)

lemma list_of_eucl_nth[simp]: "n < DIM('a::executable_euclidean_space) ⟹ list_of_eucl x ! n = x ∙ (Basis_list ! n::'a)"
by (auto simp: list_of_eucl_def)

lemma nth_ge_len: "n ≥ length xs ⟹ xs ! n = [] ! (n - length xs)"
by (induction xs arbitrary: n) auto

lemma list_of_eucl_nth_if: "list_of_eucl x ! n = (if n < DIM('a::executable_euclidean_space) then x ∙ (Basis_list ! n::'a) else [] ! (n - DIM('a)))"
apply (auto simp: list_of_eucl_def )
apply (subst nth_ge_len)
apply auto
done

lemma list_of_eucl_eq_iff:
"list_of_eucl (x::'a::executable_euclidean_space) = list_of_eucl (y::'b::executable_euclidean_space) ⟷
(DIM('a) = DIM('b) ∧ (∀i < DIM('b). x ∙ Basis_list ! i = y ∙ Basis_list ! i))"
by (auto simp: list_eq_iff_nth_eq)

lemma eucl_le_Basis_list_iff:
"(x::'a::executable_euclidean_space) ≤ y ⟷
(∀i<DIM('a). x ∙ Basis_list ! i ≤ y ∙ Basis_list ! i)"
apply (auto simp:  eucl_le[where 'a='a])
subgoal for i
subgoal by (auto dest!: spec[where x="index Basis_list i"])
done
done

lemma eucl_of_list_inj: "length xs = DIM('a::executable_euclidean_space) ⟹ length ys = DIM('a) ⟹
(eucl_of_list xs::'a) = eucl_of_list (ys) ⟹ xs = ys"
apply (auto intro!: nth_equalityI simp: euclidean_eq_iff[where 'a="'a"] eucl_of_list_inner)
using nth_Basis_list_in_Basis[where 'a="'a"]
by fastforce

lemma eucl_of_list_map_plus[simp]:
assumes [simp]: "length xs = DIM('a::executable_euclidean_space)"
shows "(eucl_of_list (map (λx. f x + g x) xs)::'a) =
eucl_of_list (map f xs) + eucl_of_list (map g xs)"
by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner)

lemma eucl_of_list_map_uminus[simp]:
assumes [simp]: "length xs = DIM('a::executable_euclidean_space)"
shows "(eucl_of_list (map (λx. - f x) xs)::'a) = - eucl_of_list (map f xs)"
by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner)

lemma eucl_of_list_map_mult_left[simp]:
assumes [simp]: "length xs = DIM('a::executable_euclidean_space)"
shows "(eucl_of_list (map (λx. r * f x) xs)::'a) = r *⇩R eucl_of_list (map f xs)"
by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner)

lemma eucl_of_list_map_mult_right[simp]:
assumes [simp]: "length xs = DIM('a::executable_euclidean_space)"
shows "(eucl_of_list (map (λx. f x * r) xs)::'a) = r *⇩R eucl_of_list (map f xs)"
by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner)

lemma eucl_of_list_map_divide_right[simp]:
assumes [simp]: "length xs = DIM('a::executable_euclidean_space)"
shows "(eucl_of_list (map (λx. f x / r) xs)::'a) = eucl_of_list (map f xs) /⇩R r"
by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner divide_simps)

lemma eucl_of_list_map_const[simp]:
assumes [simp]: "length xs = DIM('a::executable_euclidean_space)"
shows "(eucl_of_list (map (λx. c) xs)::'a) = c *⇩R One"
by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner)

lemma replicate_eq_list_of_eucl_zero: "replicate DIM('a::executable_euclidean_space) 0 = list_of_eucl (0::'a)"
by (auto intro!: nth_equalityI)

lemma eucl_of_list_append_zeroes[simp]: "eucl_of_list (xs @ replicate n 0) = eucl_of_list xs"
unfolding eucl_of_list_def
apply (auto simp: sum_list_sum_nth)
apply (rule sum.mono_neutral_cong_right)
by (auto simp: nth_append)

lemma Basis_prodD:
assumes "(i, j) ∈ Basis"
shows "i ∈ Basis ∧ j = 0 ∨ i = 0 ∧ j ∈ Basis"
using assms
by (auto simp: Basis_prod_def)

lemma eucl_of_list_take_DIM[simp]:
assumes "d = DIM('b::executable_euclidean_space)"
shows "(eucl_of_list (take d xs)::'b) = (eucl_of_list xs)"
by (auto simp: eucl_of_list_inner eucl_of_list_def fst_sum_list sum_list_sum_nth assms dest!: Basis_prodD)

lemma eucl_of_list_eqI:
assumes "take DIM('a) (xs @ replicate (DIM('a) - length xs) 0) =
take DIM('a) (ys @ replicate (DIM('a) - length ys) 0)"
shows "eucl_of_list xs = (eucl_of_list ys::'a::executable_euclidean_space)"
proof -
have "(eucl_of_list xs::'a) = eucl_of_list (take DIM('a) (xs @ replicate (DIM('a) - length xs) 0))"
also note assms
also have "eucl_of_list (take DIM('a) (ys @ replicate (DIM('a) - length ys) 0)) = (eucl_of_list ys::'a)"
by simp
finally show ?thesis .
qed

lemma eucl_of_list_replicate_zero[simp]: "eucl_of_list (replicate E 0) = 0"
proof -
have "eucl_of_list (replicate E 0) = (eucl_of_list (replicate E 0 @ replicate (DIM('a) - E) 0)::'a)"
by simp
also have "… = eucl_of_list (replicate DIM('a) 0)"
apply (rule eucl_of_list_eqI)
by (auto simp: min_def nth_append intro!: nth_equalityI)
also have "… = 0"
finally show ?thesis by simp
qed

lemma eucl_of_list_Nil[simp]: "eucl_of_list [] = 0"
using eucl_of_list_replicate_zero[of 0] by simp

lemma fst_eucl_of_list_prod:
shows "fst (eucl_of_list xs::'b::executable_euclidean_space  × _) = (eucl_of_list (take DIM('b) xs)::'b)"
apply (auto simp: eucl_of_list_inner eucl_of_list_def fst_sum_list dest!: Basis_prodD)
apply (rule sum.mono_neutral_cong_right)
subgoal by simp
subgoal by auto
subgoal by (auto simp: Basis_list_prod_def nth_append)
subgoal by (auto simp: Basis_list_prod_def nth_append)
done

lemma index_zip_replicate1[simp]: "index (zip (replicate d a) bs) (a, b) = index bs b"
if "d = length bs"
using that
by (induction bs arbitrary: d) auto

lemma index_zip_replicate2[simp]: "index (zip as (replicate d b)) (a, b) = index as a"
if "d = length as"
using that
by (induction as arbitrary: d) auto

lemma index_Basis_list_prod[simp]:
fixes a::"'a::executable_euclidean_space" and b::"'b::executable_euclidean_space"
shows "a ∈ Basis ⟹ index Basis_list (a, 0::'b) = index Basis_list a"
"b ∈ Basis ⟹ index Basis_list (0::'a, b) = DIM('a) + index Basis_list b"
by (auto simp: Basis_list_prod_def index_append
in_set_zip zip_replicate index_map_inj dest: spec[where x="index Basis_list a"])

lemma eucl_of_list_eq_takeI:
assumes "(eucl_of_list (take DIM('a::executable_euclidean_space) xs)::'a) = x"
shows "eucl_of_list xs = x"
using eucl_of_list_take_DIM[OF refl, of xs, where 'b='a] assms
by auto

lemma eucl_of_list_inner_le:
fixes i::"'a::executable_euclidean_space"
assumes i: "i ∈ Basis"
assumes l: "length xs ≥ DIM('a)"
shows "eucl_of_list xs ∙ i = xs ! (index Basis_list i)"
proof -
have "(eucl_of_list xs::'a) = eucl_of_list (take DIM('a) (xs @ (replicate (DIM('a) - length xs) 0)))"
by (rule eucl_of_list_eq_takeI) simp
also have "… ∙ i = xs ! (index Basis_list i)"
using assms
by (subst eucl_of_list_inner) auto
finally show ?thesis .
qed

lemma eucl_of_list_prod_if:
assumes "length xs = DIM('a::executable_euclidean_space) + DIM('b::executable_euclidean_space)"
shows "eucl_of_list xs =
(eucl_of_list (take DIM('a) xs)::'a, eucl_of_list (drop DIM('a) xs)::'b)"
apply (rule euclidean_eqI)
using assms
apply (auto simp: eucl_of_list_inner dest!: Basis_prodD)
apply (subst eucl_of_list_inner_le)
apply (auto simp: Basis_list_prod_def index_append in_set_zip)
done

lemma snd_eucl_of_list_prod:
shows "snd (eucl_of_list xs::'b::executable_euclidean_space  × 'c::executable_euclidean_space) =
(eucl_of_list (drop DIM('b) xs)::'c)"
proof (cases "length xs ≤ DIM('b)")
case True
then show ?thesis
by (auto simp: eucl_of_list_inner eucl_of_list_def snd_sum_list dest!: Basis_prodD)
next
case False
have "xs = take DIM('b) xs @ drop DIM('b) xs" by simp
also have "eucl_of_list … = (eucl_of_list (… @ replicate (length xs - DIM('c)) 0)::'b × 'c)"
by simp
finally have "eucl_of_list xs = (eucl_of_list (xs @ replicate (DIM('b) + DIM('c) - length xs) 0)::'b × 'c)"
by simp
also have "… = eucl_of_list (take (DIM ('b × 'c)) (xs @ replicate (DIM('b) + DIM('c) - length xs) 0))"
finally have *: "(eucl_of_list xs::'b×'c) = eucl_of_list (take DIM('b × 'c) (xs @ replicate (DIM('b) + DIM('c) - length xs) 0))"
by simp
show ?thesis
apply (subst *)
apply (subst eucl_of_list_prod_if)
subgoal by simp
subgoal
apply simp
apply (subst (2) eucl_of_list_take_DIM[OF refl, symmetric])
apply (subst (2) eucl_of_list_take_DIM[OF refl, symmetric])
apply (rule arg_cong[where f=eucl_of_list])
by (auto intro!: nth_equalityI simp: nth_append min_def split: if_splits)
done
qed

lemma eucl_of_list_prod:
shows "eucl_of_list xs = (eucl_of_list (take DIM('b) xs)::'b::executable_euclidean_space,
eucl_of_list (drop DIM('b) xs)::'c::executable_euclidean_space)"
using snd_eucl_of_list_prod[of xs, where 'b='b and 'c='c]
using fst_eucl_of_list_prod[of xs, where 'b='b and 'a='c]
by (auto simp del: snd_eucl_of_list_prod fst_eucl_of_list_prod simp add: prod_eq_iff)

lemma eucl_of_list_real[simp]: "eucl_of_list [x] = (x::real)"
by (auto simp: eucl_of_list_def Basis_list_real_def)

lemma eucl_of_list_append[simp]:
assumes "length xs = DIM('i::executable_euclidean_space)"
assumes "length ys = DIM('j::executable_euclidean_space)"
shows "eucl_of_list (xs @ ys) = (eucl_of_list xs::'i, eucl_of_list ys::'j)"
using assms
by (auto simp: eucl_of_list_prod)

lemma list_allI: "(⋀x. x ∈ set xs ⟹ P x) ⟹ list_all P xs"
by (auto simp: list_all_iff)

lemma
concat_map_nthI:
assumes "⋀x y. x ∈ set xs ⟹ y ∈ set (f x) ⟹ P y"
assumes "j < length (concat (map f xs))"
shows "P (concat (map f xs) ! j)"
proof -
have "list_all P (concat (map f xs))"
by (rule list_allI) (auto simp: assms)
then show ?thesis
by (auto simp: list_all_length assms)
qed

lemma map_nth_append1:
assumes "length xs = d"
shows "map ((!) (xs @ ys)) [0..<d] = xs"
using assms
by (auto simp: nth_append intro!: nth_equalityI)

lemma map_nth_append2:
assumes "length ys = d"
shows "map ((!) (xs @ ys)) [length xs..<length xs + d] = ys"
using assms
by (auto simp: intro!: nth_equalityI)

lemma length_map2 [simp]: "length (map2 f xs ys) = min (length xs) (length ys)"
by simp

lemma map2_nth [simp]: "map2 f xs ys ! n = f (xs ! n) (ys ! n)"
if "n < length xs" "n < length ys"
using that by simp

lemma list_of_eucl_add: "list_of_eucl (x + y) = map2 (+) (list_of_eucl x) (list_of_eucl y)"
by (auto intro!: nth_equalityI simp: inner_simps)

lemma list_of_eucl_inj:
"list_of_eucl z = list_of_eucl y ⟹ y = z"
by (metis eucl_of_list_list_of_eucl)

lemma length_Basis_list_pos[simp]: "length Basis_list > 0"
by (metis length_pos_if_in_set Basis_list SOME_Basis)

lemma Basis_list_nth_nonzero:
"i < length (Basis_list::'a::executable_euclidean_space list) ⟹ (Basis_list::'a list) ! i ≠ 0"
by (auto dest!: nth_mem simp: nonzero_Basis)

lemma nth_Basis_list_prod:
"i < DIM('a) + DIM('b) ⟹ (Basis_list::('a::executable_euclidean_space × 'b::executable_euclidean_space) list) ! i =
(if i < DIM('a) then (Basis_list ! i, 0) else (0, Basis_list ! (i - DIM('a))))"
by (auto simp: Basis_list_nth_nonzero prod_eq_iff Basis_list_prod_def nth_append not_less)

lemma eucl_of_list_if:
assumes [simp]: "length xs = DIM('a::executable_euclidean_space)" "distinct xs"
shows "eucl_of_list (map (λxa. if xa = x then 1 else 0) (xs::nat list)) =
(if x ∈ set xs then Basis_list ! index xs x else 0::'a)"
by (rule euclidean_eqI) (auto simp: eucl_of_list_inner inner_Basis index_nth_id)

lemma take_append_take_minus_idem: "take n XS @ map ((!) XS) [n..<length XS] = XS"
by (auto intro!: nth_equalityI simp: nth_append min_def)

lemma sum_list_Basis_list[simp]: "sum_list (map f Basis_list) = (∑b∈Basis. f b)"
by (subst sum_list_distinct_conv_sum_set) (auto simp: Basis_list distinct_Basis_list)

lemma hd_Basis_list[simp]: "hd Basis_list ∈ Basis"
unfolding Basis_list[symmetric]
by (rule hd_in_set) (auto simp: set_empty[symmetric])

definition "inner_lv_rel a b = sum_list (map2 (*) a b)"

lemma eucl_of_list_inner_eq: "(eucl_of_list xs::'a) ∙ eucl_of_list ys = inner_lv_rel xs ys"
if "length xs = DIM('a::executable_euclidean_space)" "length ys = DIM('a)"
using that
by (subst euclidean_inner[abs_def], subst sum_list_Basis_list[symmetric])
(auto simp: eucl_of_list_inner sum_list_sum_nth index_nth_id inner_lv_rel_def)

lemma euclidean_vec_componentwise:
"(∑(xa::'a::euclidean_space^'b::finite)∈Basis. f xa) = (∑a∈Basis. (∑b::'b∈UNIV. f (axis b a)))"
apply (auto simp: Basis_vec_def)
apply (subst sum.swap)
apply (subst sum.Union_disjoint)
apply auto
apply (subst sum.reindex)
apply (auto intro!: injI)
subgoal
apply (auto simp: set_eq_iff)
by (metis (full_types) all_not_in_conv inner_axis_axis inner_eq_zero_iff nonempty_Basis nonzero_Basis)
apply (rule sum.cong[OF refl])
apply (auto )
apply (rule sum.reindex_cong[OF _ _ refl])
apply (auto intro!: inj_onI)
using axis_eq_axis by blast

lemma vec_nth_inner_scaleR_craziness:
"f (x $i ∙ j) *⇩R j = (∑xa∈UNIV. f (x$ xa ∙ j) *⇩R axis xa j) $i" by vector (auto simp: axis_def if_distrib scaleR_vec_def sum.delta' cong: if_cong) instantiation vec :: ("{executable_euclidean_space}", enum) executable_euclidean_space begin definition Basis_list_vec :: "('a, 'b) vec list" where "Basis_list_vec = concat (map (λn. map (axis n) Basis_list) enum_class.enum)" definition eucl_down_vec :: "int ⇒ ('a, 'b) vec ⇒ ('a, 'b) vec" where "eucl_down_vec p x = (χ i. eucl_down p (x$ i))"

definition eucl_truncate_down_vec :: "nat ⇒ ('a, 'b) vec ⇒ ('a, 'b) vec" where
"eucl_truncate_down_vec p x = (χ i. eucl_truncate_down p (x $i))" definition eucl_truncate_up_vec :: "nat ⇒ ('a, 'b) vec ⇒ ('a, 'b) vec" where "eucl_truncate_up_vec p x = (χ i. eucl_truncate_up p (x$ i))"

instance
proof
show *: "set (Basis_list::('a, 'b) vec list) = Basis"
unfolding Basis_list_vec_def Basis_vec_def
apply (auto simp: Basis_list_vec_def vec_eq_iff distinct_map Basis_vec_def
intro!: distinct_concat inj_onI split: if_splits)
apply (auto simp: Basis_list_vec_def vec_eq_iff distinct_map enum_distinct
UNIV_enum[symmetric]
intro!: distinct_concat inj_onI split: if_splits)
done
have "length (Basis_list::('a, 'b) vec list) = CARD('b) * DIM('a)"
by (auto simp: Basis_list_vec_def length_concat o_def enum_distinct
sum_list_distinct_conv_sum_set UNIV_enum[symmetric])
then show "distinct (Basis_list::('a, 'b) vec list)"
using * by (auto intro!: card_distinct)
qed (simp_all only: vector_cart[symmetric] vec_eq_iff
eucl_down_vec_def eucl_down_def
eucl_truncate_down_vec_def eucl_truncate_down_def
eucl_truncate_up_vec_def eucl_truncate_up_def,
auto simp: euclidean_vec_componentwise inner_axis Basis_list_vec_def
vec_nth_inner_scaleR_craziness
intro!: sum.cong[OF refl])
end

lemma concat_same_lengths_nth:
assumes "⋀xs. xs ∈ set XS ⟹ length xs = N"
assumes "i < length XS * N" "N > 0"
shows "concat XS ! i = XS ! (i div N) ! (i mod N)"
using assms
apply (induction XS arbitrary: i)
apply (auto simp: nth_append nth_Cons split: nat.splits)
by (metis Suc_inject div_geq mod_geq)

lemma concat_map_map_index:
shows "concat (map (λn. map (f n) xs) ys) =
map (λi. f (ys ! (i div length xs)) (xs ! (i mod length xs))) [0..<length xs * length ys]"
apply (auto intro!: nth_equalityI simp: length_concat o_def sum_list_sum_nth)
apply (subst concat_same_lengths_nth)
apply (auto simp: )
apply (subst nth_map_upt)
apply (auto simp: ac_simps)
apply (subst nth_map)
apply (metis div_eq_0_iff div_mult2_eq mult.commute mult_0 not_less0)
apply (subst nth_map)
subgoal for i
using gr_implies_not_zero by fastforce
subgoal by simp
done

lemma
sum_list_zip_map:
assumes "distinct xs"
shows "(∑(x, y)←zip xs (map g xs). f x y) = (∑x∈set xs. f x (g x))"
by (force simp add: sum_list_distinct_conv_sum_set assms distinct_zipI1 split_beta'
in_set_zip in_set_conv_nth inj_on_convol_ident
intro!: sum.reindex_cong[where l="λx. (x, g x)"])

lemma
sum_list_zip_map_of:
assumes "distinct bs"
assumes "length xs = length bs"
shows "(∑(x, y)←zip xs bs. f x y) = (∑x∈set bs. f (the (map_of (zip bs xs) x)) x)"
proof -
have "(∑(x, y)←zip xs bs. f x y) = (∑(y, x)←zip bs xs. f x y)"
by (subst zip_commute) (auto simp: o_def split_beta')
also have "… = (∑(x, y)←zip bs (map (the o map_of (zip bs xs)) bs). f y x)"
proof (rule arg_cong, rule map_cong)
have "xs = (map (the ∘ map_of (zip bs xs)) bs)"
using assms
by (auto intro!: nth_equalityI simp: map_nth map_of_zip_nth)
then show "zip bs xs = zip bs (map (the ∘ map_of (zip bs xs)) bs)"
by simp
qed auto
also have "… = (∑x∈set bs. f (the (map_of (zip bs xs) x)) x)"
using assms(1)
by (subst sum_list_zip_map) (auto simp: o_def)
finally show ?thesis .
qed

lemma vec_nth_matrix:
"vec_nth (vec_nth (matrix y) i) j = vec_nth (y (axis j 1)) i"
unfolding matrix_def by simp

lemma matrix_eqI:
assumes "⋀x. x ∈ Basis ⟹ A *v x = B *v x"
shows "(A::real^'n^'n) = B"
apply vector
using assms
apply (auto simp: Basis_vec_def)
by (metis cart_eq_inner_axis matrix_vector_mul_component)

lemma matrix_columnI:
assumes "⋀i. column i A = column i B"
shows "(A::real^'n^'n) = B"
using assms
apply vector
apply (auto simp: column_def)
apply vector
by (metis iso_tuple_UNIV_I vec_lambda_inject)

lemma
vec_nth_Basis:
fixes x::"real^'n"
shows "x ∈ Basis ⟹ vec_nth x i = (if x = axis i 1 then 1 else 0)"
apply (auto simp: Basis_vec_def)
by (metis cart_eq_inner_axis inner_axis_axis)

lemma vec_nth_eucl_of_list_eq: "length M = CARD('n) ⟹
vec_nth (eucl_of_list M::real^'n::enum) i = M ! index Basis_list (axis i (1::real))"
apply (auto simp: eucl_of_list_def)
apply (subst sum_list_zip_map_of)
apply (auto intro!: distinct_zipI2 simp: split_beta')
apply (subst sum.cong[OF refl])
apply (subst vec_nth_Basis)
apply (force simp: set_zip)
apply (rule refl)
apply (auto simp: if_distrib sum.delta cong: if_cong)
subgoal
apply (cases "map_of (zip Basis_list M) (axis i 1::real^'n::enum)")
subgoal premises prems
proof -
have "fst  set (zip Basis_list M) = (Basis::(real^'n::enum) set)" using prems
by (auto simp: in_set_zip)
then show ?thesis
using prems
by (subst (asm) map_of_eq_None_iff) simp
qed
subgoal for a
apply (auto simp: in_set_zip)
subgoal premises prems for n
by (metis DIM_cart DIM_real index_Basis_list_nth mult.right_neutral prems(2) prems(3))
done
done
done

lemma index_Basis_list_axis1: "index Basis_list (axis i (1::real)) = index enum_class.enum i"
apply (auto simp: Basis_list_vec_def Basis_list_real_def )
apply (subst index_map_inj)
by (auto intro!: injI simp: axis_eq_axis)

lemma vec_nth_eq_list_of_eucl1:
"(vec_nth (M::real^'n::enum) i) = list_of_eucl M ! (index enum_class.enum i)"
apply (subst eucl_of_list_list_of_eucl[of M, symmetric])
apply (subst vec_nth_eucl_of_list_eq)
unfolding index_Basis_list_axis1
by auto

lemma enum_3[simp]: "(enum_class.enum::3 list) = [0, 1, 2]"
by code_simp+

lemma three_eq_zero: "(3::3) = 0" by simp

lemma forall_3': "(∀i::3. P i) ⟷ P 0 ∧ P 1 ∧ P 2"
using forall_3 three_eq_zero by auto

lemma euclidean_eq_list_of_euclI: "x = y" if "list_of_eucl x = list_of_eucl y"
using that
by (metis eucl_of_list_list_of_eucl)

lemma axis_one_neq_zero[simp]: "axis xa (1::'a::zero_neq_one) ≠ 0"
by (auto simp: axis_def vec_eq_iff)

lemma eucl_of_list_vec_nth3[simp]:
"(eucl_of_list [g, h, i]::real^3) $0 = g" "(eucl_of_list [g, h, i]::real^3)$ 1 = h"
"(eucl_of_list [g, h, i]::real^3) $2 = i" "(eucl_of_list [g, h, i]::real^3)$ 3 = g"
by (auto simp: cart_eq_inner_axis eucl_of_list_inner vec_nth_eq_list_of_eucl1 index_Basis_list_axis1)

type_synonym R3 = "real*real*real"

lemma Basis_list_R3: "Basis_list = [(1,0,0), (0, 1, 0), (0, 0, 1)::R3]"
by (auto simp: Basis_list_prod_def Basis_list_real_def zero_prod_def)

lemma Basis_list_vec3: "Basis_list = [axis 0 1::real^3, axis 1 1, axis 2 1]"
by (auto simp: Basis_list_vec_def Basis_list_real_def)

lemma eucl_of_list3[simp]: "eucl_of_list [a, b, c] = (a, b, c)"
by (auto simp: eucl_of_list_inner Basis_list_vec_def zero_prod_def
Basis_prod_def Basis_list_vec3 Basis_list_R3
intro!: euclidean_eqI[where 'a=R3])

subsection ‹Bounded Linear Functions›

subsection ‹bounded linear functions›

locale blinfun_syntax
begin
no_notation vec_nth (infixl "$" 90) notation blinfun_apply (infixl "$" 999)
end

lemma bounded_linear_via_derivative:
fixes f::"'a::real_normed_vector ⇒ 'b::euclidean_space ⇒⇩L 'c::real_normed_vector" ― ‹TODO: generalize?›
assumes "⋀i. ((λx. blinfun_apply (f x) i) has_derivative (λx. f' y x i)) (at y)"
shows "bounded_linear (f' y x)"
proof -
interpret linear "f' y x"
proof (unfold_locales, goal_cases)
case (1 v w)
from has_derivative_unique[OF assms[of "v + w", unfolded blinfun.bilinear_simps]
has_derivative_add[OF assms[of v] assms[of w]], THEN fun_cong, of x]
show ?case .
next
case (2 r v)
from has_derivative_unique[OF assms[of "r *⇩R v", unfolded blinfun.bilinear_simps]
has_derivative_scaleR_right[OF assms[of v], of r], THEN fun_cong, of x]
show ?case .
qed
let ?bnd = "∑i∈Basis. norm (f' y x i)"
{
fix v
have "f' y x v = (∑i∈Basis. (v ∙ i) *⇩R f' y x i)"
by (subst euclidean_representation[symmetric]) (simp add: sum scaleR)
also have "norm … ≤ norm v * ?bnd"
by (auto intro!: order.trans[OF norm_sum] sum_mono mult_right_mono
simp: sum_distrib_left Basis_le_norm)
finally have "norm (f' y x v) ≤ norm v * ?bnd" .
}
then show ?thesis by unfold_locales auto
qed

definition blinfun_scaleR::"('a::real_normed_vector ⇒⇩L real) ⇒ 'b::real_normed_vector ⇒ ('a ⇒⇩L 'b)"
where "blinfun_scaleR a b = blinfun_scaleR_left b o⇩L a"

lemma blinfun_scaleR_transfer[transfer_rule]:
"rel_fun (pcr_blinfun (=) (=)) (rel_fun (=) (pcr_blinfun (=) (=)))
(λa b c. a c *⇩R b) blinfun_scaleR"
by (auto simp: blinfun_scaleR_def rel_fun_def pcr_blinfun_def cr_blinfun_def OO_def)

lemma blinfun_scaleR_rep_eq[simp]:
"blinfun_scaleR a b c = a c *⇩R b"

lemma bounded_linear_blinfun_scaleR: "bounded_linear (blinfun_scaleR a)"
unfolding blinfun_scaleR_def[abs_def]
by (auto intro!: bounded_linear_intros)

lemma blinfun_scaleR_has_derivative[derivative_intros]:
assumes "(f has_derivative f') (at x within s)"
shows "((λx. blinfun_scaleR a (f x)) has_derivative (λx. blinfun_scaleR a (f' x))) (at x within s)"
using bounded_linear_blinfun_scaleR assms
by (rule bounded_linear.has_derivative)

lemma blinfun_componentwise:
fixes f::"'a::real_normed_vector ⇒ 'b::euclidean_space ⇒⇩L 'c::real_normed_vector"
shows "f = (λx. ∑i∈Basis. blinfun_scaleR (blinfun_inner_left i) (f x i))"
by (auto intro!: blinfun_eqI
simp: blinfun.sum_left euclidean_representation blinfun.scaleR_right[symmetric]
blinfun.sum_right[symmetric])

lemma
blinfun_has_derivative_componentwiseI:
fixes f::"'a::real_normed_vector ⇒ 'b::euclidean_space ⇒⇩L 'c::real_normed_vector"
assumes "⋀i. i ∈ Basis ⟹ ((λx. f x i) has_derivative blinfun_apply (f' i)) (at x)"
shows "(f has_derivative (λx. ∑i∈Basis. blinfun_scaleR (blinfun_inner_left i) (f' i x))) (at x)"
by (subst blinfun_componentwise) (force intro: derivative_eq_intros assms simp: blinfun.bilinear_simps)

lemma
has_derivative_BlinfunI:
fixes f::"'a::real_normed_vector ⇒ 'b::euclidean_space ⇒⇩L 'c::real_normed_vector"
assumes "⋀i. ((λx. f x i) has_derivative (λx. f' y x i)) (at y)"
shows "(f has_derivative (λx. Blinfun (f' y x))) (at y)"
proof -
have 1: "f = (λx. ∑i∈Basis. blinfun_scaleR (blinfun_inner_left i) (f x i))"
by (rule blinfun_componentwise)
moreover have 2: "(… has_derivative (λx. ∑i∈Basis. blinfun_scaleR (blinfun_inner_left i) (f' y x i))) (at y)"
by (force intro: assms derivative_eq_intros)
moreover
interpret f': bounded_linear "f' y x" for x
by (rule bounded_linear_via_derivative) (rule assms)
have 3: "(∑i∈Basis. blinfun_scaleR (blinfun_inner_left i) (f' y x i)) i = f' y x i" for x i
by (auto simp: if_distrib if_distribR blinfun.bilinear_simps
f'.scaleR[symmetric] f'.sum[symmetric] euclidean_representation
intro!: blinfun_euclidean_eqI)
have 4: "blinfun_apply (Blinfun (f' y x)) = f' y x" for x
apply (subst bounded_linear_Blinfun_apply)
subgoal by unfold_locales
subgoal by simp
done
show ?thesis
apply (subst 1)
apply (rule 2[THEN has_derivative_eq_rhs])
apply (rule ext)
apply (rule blinfun_eqI)
apply (subst 3)
apply (subst 4)
apply (rule refl)
done
qed

lemma
has_derivative_Blinfun:
assumes "(f has_derivative f') F"
shows "(f has_derivative Blinfun f') F"
using assms
by (subst bounded_linear_Blinfun_apply) auto

lift_definition flip_blinfun::
"('a::real_normed_vector ⇒⇩L 'b::real_normed_vector ⇒⇩L 'c::real_normed_vector) ⇒ 'b ⇒⇩L 'a ⇒⇩L 'c" is
"λf x y. f y x"
using bounded_bilinear.bounded_linear_left bounded_bilinear.bounded_linear_right bounded_bilinear.flip
by auto

lemma flip_blinfun_apply[simp]: "flip_blinfun f a b = f b a"
by transfer simp

lemma le_norm_blinfun:
shows "norm (blinfun_apply f x) / norm x ≤ norm f"
by transfer (rule le_onorm)

lemma norm_flip_blinfun[simp]: "norm (flip_blinfun x) = norm x" (is "?l = ?r")
proof (rule antisym)
from order_trans[OF norm_blinfun, OF mult_right_mono, OF norm_blinfun, OF norm_ge_zero, of x]
show "?l ≤ ?r"
by (auto intro!: norm_blinfun_bound simp: ac_simps)
have "norm (x a b) ≤ norm (flip_blinfun x) * norm a * norm b" for a b
proof -
have "norm (x a b) / norm a ≤ norm (flip_blinfun x b)"
by (rule order_trans[OF _ le_norm_blinfun]) auto
also have "… ≤ norm (flip_blinfun x) * norm b"
by (rule norm_blinfun)
finally show ?thesis
by (auto simp add: divide_simps blinfun.bilinear_simps algebra_simps split: if_split_asm)
qed
then show "?r ≤ ?l"
by (auto intro!: norm_blinfun_bound)
qed

lemma bounded_linear_flip_blinfun[bounded_linear]: "bounded_linear flip_blinfun"
by unfold_locales (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI exI[where x=1])

lemma dist_swap2_swap2[simp]: "dist (flip_blinfun f) (flip_blinfun g) = dist f g"
by (metis (no_types) bounded_linear_flip_blinfun dist_blinfun_def linear_simps(2)
norm_flip_blinfun)

context includes blinfun.lifting begin

lift_definition blinfun_of_vmatrix::"(real^'m^'n) ⇒ ((real^('m::finite)) ⇒⇩L (real^('n::finite)))" is
"matrix_vector_mult:: ((real, 'm) vec, 'n) vec ⇒ ((real, 'm) vec ⇒ (real, 'n) vec)"
unfolding linear_linear
by (rule matrix_vector_mul_linear)

lemma matrix_blinfun_of_vmatrix[simp]: "matrix (blinfun_of_vmatrix M) = M"
apply vector
apply (auto simp: matrix_def)
apply transfer
by (metis cart_eq_inner_axis matrix_vector_mul_component)

end

lemma blinfun_apply_componentwise:
"B = (∑i∈Basis. blinfun_scaleR (blinfun_inner_left i) (blinfun_apply B i))"
using blinfun_componentwise[of "λx. B", unfolded fun_eq_iff]
by blast

lemma blinfun_apply_eq_sum:
assumes [simp]: "length v = CARD('n)"
shows "blinfun_apply (B::(real^'n::enum)⇒⇩L(real^'m::enum)) (eucl_of_list v) =
(∑i<CARD('m). ∑j<CARD('n). ((B (Basis_list ! j) ∙ Basis_list ! i) * v ! j) *⇩R (Basis_list ! i))"
apply (subst blinfun_apply_componentwise[of B])
apply (auto intro!: euclidean_eqI[where 'a="(real,'m) vec"]
simp: blinfun.bilinear_simps eucl_of_list_inner inner_sum_left inner_Basis if_distrib
sum_Basis_sum_nth_Basis_list nth_eq_iff_index if_distribR
cong: if_cong)
apply (subst sum.swap)
by (auto simp: sum.delta algebra_simps)

lemma in_square_lemma[intro, simp]: "x * C + y < D * C" if "x < D" "y < C" for x::nat
proof -
have "x * C + y < (D - 1) * C + C"
apply (rule mult_right_mono)
using that
by auto
also have "… ≤ D * C"
using that
by (auto simp: algebra_simps)
finally show ?thesis .
qed

lemma less_square_imp_div_less[intro, simp]: "i < E * D ⟹  i div E < D" for i::nat
by (metis div_eq_0_iff div_mult2_eq gr_implies_not0 mult_not_zero)

lemma in_square_lemma'[intro, simp]: "i < L ⟹ n < N ⟹ i * N + n < N * L" for i n::nat
by (metis in_square_lemma mult.commute)

lemma
distinct_nth_eq_iff:
"distinct xs ⟹ x < length xs ⟹ y < length xs ⟹ xs ! x = xs ! y ⟷ x = y"
by (drule inj_on_nth[where I="{..<length xs}"]) (auto simp: inj_onD)

lemma index_Basis_list_axis2:
"index Basis_list (axis (j::'j::enum) (axis (i::'i::enum) (1::real))) =
(index enum_class.enum j) * CARD('i) + index enum_class.enum i"
apply (auto simp: Basis_list_vec_def Basis_list_real_def o_def)
apply (subst concat_map_map_index)
unfolding card_UNIV_length_enum[symmetric]
subgoal
proof -
have index_less_cardi: "index enum_class.enum k < CARD('i)" for k::'i
by (rule index_less) (auto simp: enum_UNIV card_UNIV_length_enum)
have index_less_cardj: "index enum_class.enum k < CARD('j)" for k::'j
by (rule index_less) (auto simp: enum_UNIV card_UNIV_length_enum)
have *: "axis j (axis i 1) =
(λi. axis (enum_class.enum ! (i div CARD('i)))
(axis (enum_class.enum ! (i mod CARD('i))) 1))
((index enum_class.enum j) * CARD('i) + index enum_class.enum i)"
by (auto simp: index_less_cardi enum_UNIV)
note less=in_square_lemma[OF index_less_cardj index_less_cardi, of j i]
show ?thesis
apply (subst *)
apply (subst index_map_inj_on[where S="{..<CARD('j)*CARD('i)}"])
subgoal
apply (auto intro!: inj_onI simp: axis_eq_axis )
apply (subst (asm) distinct_nth_eq_iff)
apply (auto simp: enum_distinct card_UNIV_length_enum)
subgoal for x y
using gr_implies_not0 by fastforce
subgoal for x y
using gr_implies_not0 by fastforce
subgoal for x y
apply (drule inj_onD[OF inj_on_nth[OF enum_distinct[where 'a='j], where I = "{..<CARD('j)}"], rotated])
apply (auto simp: card_UNIV_length_enum mult.commute)
subgoal
by (metis mod_mult_div_eq)
done
done
subgoal using less by (auto simp: )
subgoal by (auto simp: card_UNIV_length_enum ac_simps)
subgoal apply (subst index_upt)
subgoal using less by auto
subgoal using less by (auto simp: ac_simps)
subgoal using less by auto
done
done
qed
done

lemma
vec_nth_Basis2:
fixes x::"real^'n^'m"
shows "x ∈ Basis ⟹ vec_nth (vec_nth x i) j = ((if x = axis i (axis j 1) then 1 else 0))"
by (auto simp: Basis_vec_def axis_def)

lemma vec_nth_eucl_of_list_eq2: "length M = CARD('n) * CARD('m) ⟹
vec_nth (vec_nth (eucl_of_list M::real^'n::enum^'m::enum) i) j = M ! index Basis_list (axis i (axis j (1::real)))"
apply (auto simp: eucl_of_list_def)
apply (subst sum_list_zip_map_of)
apply (auto intro!: distinct_zipI2 simp: split_beta')
apply (subst sum.cong[OF refl])
apply (subst vec_nth_Basis2)
apply (force simp: set_zip)
apply (rule refl)
apply (auto simp: if_distrib sum.delta cong: if_cong)
subgoal
apply (cases "map_of (zip Basis_list M) (axis i (axis j 1)::real^'n::enum^'m::enum)")
subgoal premises prems
proof -
have "fst  set (zip Basis_list M) = (Basis::(real^'n::enum^'m::enum) set)" using prems
by (auto simp: in_set_zip)
then show ?thesis
using prems
by (subst (asm) map_of_eq_None_iff) auto
qed
subgoal for a
apply (auto simp: in_set_zip)
subgoal premises prems for n
proof -
have "n < card (Basis::(real^'n::_^'m::_) set)"
then show ?thesis
by (metis index_Basis_list_nth prems(2))
qed
done
done
done

lemma vec_nth_eq_list_of_eucl2:
"vec_nth (vec_nth (M::real^'n::enum^'m::enum) i) j =
list_of_eucl M ! (index enum_class.enum i * CARD('n) + index enum_class.enum j)"
apply (subst eucl_of_list_list_of_eucl[of M, symmetric])
apply (subst vec_nth_eucl_of_list_eq2)
unfolding index_Basis_list_axis2
by auto

theorem
eucl_of_list_matrix_vector_mult_eq_sum_nth_Basis_list:
assumes "length M = CARD('n) * CARD('m)"
assumes "length v = CARD('n)"
shows "(eucl_of_list M::real^'n::enum^'m::enum) *v eucl_of_list v =
(∑i<CARD('m).
(∑j<CARD('n). M ! (i * CARD('n) + j) * v ! j) *⇩R Basis_list ! i)"
apply (vector matrix_vector_mult_def)
apply (auto simp: )
apply (subst vec_nth_eucl_of_list_eq2)
apply (auto simp: assms)
apply (subst vec_nth_eucl_of_list_eq)
apply (auto simp: assms index_Basis_list_axis2 index_Basis_list_axis1 vec_nth_Basis sum.delta
nth_eq_iff_index
if_distrib cong: if_cong)
subgoal for i
apply (rule sum.reindex_cong[where l="nth enum_class.enum"])
apply (auto simp: enum_distinct card_UNIV_length_enum distinct_nth_eq_iff intro!: inj_onI)
apply (rule image_eqI[OF ])
apply (rule nth_index[symmetric])
apply (auto simp: enum_UNIV)
by (auto simp: algebra_simps enum_UNIV enum_distinct index_nth_id)
subgoal for i
using index_less[of i "enum_class.enum" "CARD('n)"]
by (auto simp: enum_UNIV card_UNIV_length_enum)
done

lemma index_enum_less[intro, simp]: "index enum_class.enum (i::'n::enum) < CARD('n)"
by (auto intro!: index_less simp: enum_UNIV card_UNIV_length_enum)

lemmas [intro, simp] = enum_distinct
lemmas [simp] = card_UNIV_length_enum[symmetric] enum_UNIV

lemma sum_index_enum_eq:
"(∑(k::'n::enum)∈UNIV. f (index enum_class.enum k)) = (∑i<CARD('n). f i)"
by (rule sum.reindex_cong[where l="nth enum_class.enum"])
(force intro!: inj_onI simp: distinct_nth_eq_iff index_nth_id)+

end

# Theory Affine_Form

section ‹Affine Form›
theory Affine_Form
imports
"HOL-Analysis.Multivariate_Analysis"
"HOL-Combinatorics.List_Permutation"
Affine_Arithmetic_Auxiliarities
Executable_Euclidean_Space
begin

subsection ‹Auxiliary developments›

lemma sum_list_mono:
shows
"length xs = length ys ⟹ (⋀x y. (x, y) ∈ set (zip xs ys) ⟹ x ≤ y) ⟹
sum_list xs ≤ sum_list ys"
by (induct xs ys rule: list_induct2) (auto simp: algebra_simps intro: add_mono)

lemma
shows sum_list_nonneg: "(⋀x. x ∈ set xs ⟹ x ≥ 0) ⟹ sum_list xs ≥ 0"
by (induct xs) (auto intro!: add_nonneg_nonneg)

lemma map_filter:
"map f (filter (λx. P (f x)) xs) = filter P (map f xs)"
by (induct xs) simp_all

lemma
map_of_zip_upto2_length_eq_nth:
assumes "distinct B"
assumes "i < length B"
shows "(map_of (zip B [0..<length B]) (B ! i)) = Some i"
proof -
have "length [0..<length B] = length B"
by simp
from map_of_zip_is_Some[OF this, of i] assms
have "map_of (zip B [0..<length B]) (B ! i) = Some i"
using assms by (auto simp: in_set_zip)
thus ?thesis by simp
qed

lemma distinct_map_fst_snd_eqD:
"distinct (map fst xs) ⟹ (i, a) ∈ set xs ⟹ (i, b) ∈ set xs ⟹ a = b"
by (metis (lifting) map_of_is_SomeI option.inject)

lemma length_filter_snd_zip:
"length ys = length xs ⟹ length (filter (p ∘ snd) (zip ys xs)) = length (filter p xs)"
by (induct ys xs rule: list_induct2) (auto )

lemma filter_snd_nth:
"length ys = length xs ⟹ n < length (filter p xs) ⟹
snd (filter (p ∘ snd) (zip ys xs) ! n) = filter p xs ! n"
by (induct ys xs arbitrary: n rule: list_induct2) (auto simp: o_def nth_Cons split: nat.split)

lemma distinct_map_snd_fst_eqD:
"distinct (map snd xs) ⟹ (i, a) ∈ set xs ⟹ (j, a) ∈ set xs ⟹ i = j"
by (metis Pair_inject inj_on_contraD snd_conv distinct_map)

lemma map_of_mapk_inj_on_SomeI:
"inj_on f (fst  (set t)) ⟹ map_of t k = Some x ⟹
map_of (map (case_prod (λk. Pair (f k))) t) (f k) = Some x"
by (induct t) (auto simp add: inj_on_def dest!: map_of_SomeD split: if_split_asm)

lemma map_abs_nonneg[simp]:
shows "list_all (λx. x ≥ 0) xs ⟹ map abs xs = xs"
by (induct xs) auto

lemma the_inv_into_image_eq: "inj_on f A ⟹ Y ⊆ f  A ⟹ the_inv_into A f  Y = f - Y ∩ A"
using f_the_inv_into_f the_inv_into_f_f[where f = f and A = A]
by force

lemma image_fst_zip: "length ys = length xs ⟹ fst  set (zip ys xs) = set ys"
by (metis dom_map_of_conv_image_fst dom_map_of_zip)

lemma inj_on_fst_set_zip_distinct[simp]:
"distinct xs ⟹ length xs = length ys ⟹ inj_on fst (set (zip xs ys))"
by (force simp add: in_set_zip distinct_conv_nth intro!: inj_onI)

lemma mem_greaterThanLessThan_absI:
fixes x::real
assumes "abs x < 1"
shows "x ∈ {-1 <..< 1}"
using assms by (auto simp: abs_real_def split: if_split_asm)

lemma minus_one_less_divideI: "b > 0 ⟹ -b < a ⟹ -1 < a / (b::real)"
by (auto simp: field_simps)

lemma divide_less_oneI: "b > 0 ⟹ b > a ⟹ a / (b::real) < 1"
by (auto simp: field_simps)

lemma closed_segment_real:
fixes a b::real
shows "closed_segment a b = (if a ≤ b then {a .. b} else {b .. a})" (is "_ = ?if")
proof safe
fix x assume "x ∈ closed_segment a b"
from segment_bound[OF this]
show "x ∈ ?if" by (auto simp: abs_real_def split: if_split_asm)
next
fix x
assume "x ∈ ?if"
thus "x ∈ closed_segment a b"
by (auto simp: closed_segment_def intro!: exI[where x="(x - a)/(b - a)"]
simp: divide_simps algebra_simps)
qed

subsection ‹Partial Deviations›

typedef (overloaded) 'a pdevs = "{x::nat ⇒ 'a::zero. finite {i. x i ≠ 0}}"
― ‹TODO: unify with polynomials›
morphisms pdevs_apply Abs_pdev
by (auto intro!: exI[where x="λx. 0"])

setup_lifting type_definition_pdevs

lemma pdevs_eqI: "(⋀i. pdevs_apply x i = pdevs_apply y i) ⟹ x = y"
by transfer auto

definition pdevs_val :: "(nat ⇒ real) ⇒ 'a::real_normed_vector pdevs ⇒ 'a"
where "pdevs_val e x = (∑i. e i *⇩R pdevs_apply x i)"

definition valuate:: "((nat ⇒ real) ⇒ 'a) ⇒ 'a set"
where "valuate x = x  (UNIV → {-1 .. 1})"

lemma valuate_ex: "x ∈ valuate f ⟷ (∃e. (∀i. e i ∈ {-1 .. 1}) ∧ x = f e)"
unfolding valuate_def
by (auto simp add: valuate_def Pi_iff) blast

instantiation pdevs :: (equal) equal
begin

definition equal_pdevs::"'a pdevs ⇒ 'a pdevs ⇒ bool"
where "equal_pdevs a b ⟷ a = b"

instance proof qed (simp add: equal_pdevs_def)
end

subsection ‹Affine Forms›

text ‹The data structure of affine forms represents particular sets, zonotopes›

type_synonym 'a aform = "'a × 'a pdevs"

subsection ‹Evaluation, Range, Joint Range›

definition aform_val :: "(nat ⇒ real) ⇒ 'a::real_normed_vector aform ⇒ 'a"
where "aform_val e X = fst X + pdevs_val e (snd X)"

definition Affine ::
"'a::real_normed_vector aform ⇒ 'a set"
where "Affine X = valuate (λe. aform_val e X)"

definition Joints ::
"'a::real_normed_vector aform list ⇒ 'a list set"
where "Joints XS = valuate (λe. map (aform_val e) XS)"

lemma Joints_nthE:
assumes "zs ∈ Joints ZS"
obtains e where
"⋀i. i < length zs ⟹ zs ! i = aform_val e (ZS ! i)"
"⋀i. e i ∈ {-1..1}"
using assms
by atomize_elim (auto simp: Joints_def Pi_iff valuate_ex)

lemma Joints_mapE:
assumes "ys ∈ Joints YS"
obtains e where
"ys = map (λx. aform_val e x) YS"
"⋀i. e i ∈ {-1 .. 1}"
using assms
by (force simp: Joints_def valuate_def)

lemma
zipped_subset_mapped_Elem:
assumes "xs = map (aform_val e) XS"
assumes e: "⋀i. e i ∈ {-1 .. 1}"
assumes [simp]: "length xs = length XS"
assumes [simp]: "length ys = length YS"
assumes "set (zip ys YS) ⊆ set (zip xs XS)"
shows "ys = map (aform_val e) YS"
proof -
from assms have ys: "⋀i. i < length xs ⟹ xs ! i = aform_val e (XS ! i)"
by auto
from assms have set_eq: "{(ys ! i, YS ! i) |i. i < length ys ∧ i < length YS} ⊆
{(xs ! i, XS ! i) |i. i < length xs ∧ i < length XS}"
using assms(2)
by (auto simp: set_zip)
hence "∀i<length YS. ∃j<length XS. ys ! i = xs ! j ∧ YS ! i = XS ! j"
by auto
then obtain j where j: "⋀i. i < length YS ⟹ ys ! i = xs ! (j i)"
"⋀i. i < length YS ⟹ YS ! i = XS ! (j i)"
"⋀i. i < length YS ⟹ j i < length XS"
by metis
show ?thesis
using assms
by (auto simp: Joints_def j ys intro!: exI[where x=e] nth_equalityI)
qed

lemma Joints_set_zip_subset:
assumes "xs ∈ Joints XS"
assumes "length xs = length XS"
assumes "length ys = length YS"
assumes "set (zip ys YS) ⊆ set (zip xs XS)"
shows "ys ∈ Joints YS"
proof -
from Joints_mapE assms obtain e where
ys: "xs = map (λx. aform_val e x) XS"
and e: "⋀i. e i ∈ {-1 .. 1}"
by blast
show "ys ∈ Joints YS"
using e zipped_subset_mapped_Elem[OF ys e assms(2-4)]
by (auto simp: Joints_def valuate_def intro!: exI[where x=e])
qed

lemma Joints_set_zip:
assumes "ys ∈ Joints YS"
assumes "length xs = length XS"
assumes "length YS = length XS"
assumes sets_eq: "set (zip xs XS) = set (zip ys YS)"
shows "xs ∈ Joints XS"
proof -
from assms have "length ys = length YS"
by (auto simp: Joints_def valuate_def)
from assms(1) this assms(2) show ?thesis
by (rule Joints_set_zip_subset) (simp add: assms)
qed

definition Joints2 ::
"'a::real_normed_vector aform list ⇒'b::real_normed_vector aform ⇒ ('a list × 'b) set"
where "Joints2 XS Y = valuate (λe. (map (aform_val e) XS, aform_val e Y))"

lemma Joints2E:
assumes "zs_y ∈ Joints2 ZS Y"
obtains e where
"⋀i. i < length (fst zs_y) ⟹ (fst zs_y) ! i = aform_val e (ZS ! i)"
"snd (zs_y) = aform_val e Y"
"⋀i. e i ∈ {-1..1}"
using assms
by atomize_elim (auto simp: Joints2_def Pi_iff valuate_ex)

lemma nth_in_AffineI:
assumes "xs ∈ Joints XS"
assumes "i < length XS"
shows "xs ! i ∈ Affine (XS ! i)"
using assms by (force simp: Affine_def Joints_def valuate_def)

lemma Cons_nth_in_Joints1:
assumes "xs ∈ Joints XS"
assumes "i < length XS"
shows "((xs ! i) # xs) ∈ Joints ((XS ! i) # XS)"
using assms by (force simp: Joints_def valuate_def)

lemma Cons_nth_in_Joints2:
assumes "xs ∈ Joints XS"
assumes "i < length XS"
assumes "j < length XS"
shows "((xs ! i) #(xs ! j) # xs) ∈ Joints ((XS ! i)#(XS ! j) # XS)"
using assms by (force simp: Joints_def valuate_def)

lemma Joints_swap:
"x#y#xs∈Joints (X#Y#XS) ⟷ y#x#xs ∈ Joints (Y#X#XS)"
by (force simp: Joints_def valuate_def)

lemma Joints_swap_Cons_append:
"length xs = length XS ⟹ x#ys@xs∈Joints (X#YS@XS) ⟷ ys@x#xs ∈ Joints (YS@X#XS)"
by (auto simp: Joints_def valuate_def)

lemma Joints_ConsD:
"x#xs∈Joints (X#XS) ⟹ xs ∈ Joints XS"
by (force simp: Joints_def valuate_def)

lemma Joints_appendD1:
"ys@xs∈Joints (YS@XS) ⟹ length xs = length XS ⟹ xs ∈ Joints XS"
by (force simp: Joints_def valuate_def)

lemma Joints_appendD2:
"ys@xs∈Joints (YS@XS) ⟹ length ys = length YS ⟹ ys ∈ Joints YS"
by (force simp: Joints_def valuate_def)

lemma Joints_imp_length_eq: "xs ∈ Joints XS ⟹ length xs = length XS"
by (auto simp: Joints_def valuate_def)

lemma Joints_rotate[simp]: "xs@[x] ∈ Joints (XS @[X]) ⟷ x#xs ∈ Joints (X#XS)"
by (auto simp: Joints_def valuate_def)

subsection ‹Domain›

definition "pdevs_domain x = {i. pdevs_apply x i ≠ 0}"

lemma finite_pdevs_domain[intro, simp]: "finite (pdevs_domain x)"
unfolding pdevs_domain_def by transfer

lemma in_pdevs_domain[simp]: "i ∈ pdevs_domain x ⟷ pdevs_apply x i ≠ 0"
by (auto simp: pdevs_domain_def)

subsection ‹Least Fresh Index›

definition degree::"'a::real_vector pdevs ⇒ nat"
where "degree x = (LEAST i. ∀j≥i. pdevs_apply x j = 0)"

lemma degree[rule_format, intro, simp]:
shows "∀j≥degree x. pdevs_apply x j = 0"
unfolding degree_def
proof (rule LeastI_ex)
have "⋀j. j > Max (pdevs_domain x) ⟹ j ∉ (pdevs_domain x)"
by (metis Max_less_iff all_not_in_conv less_irrefl_nat finite_pdevs_domain)
then show "∃xa. ∀j≥xa. pdevs_apply x j = 0"
by (auto intro!: exI[where x="Max (pdevs_domain x) + 1"])
qed

lemma degree_le:
assumes d: "∀j ≥ d. pdevs_apply x j = 0"
shows "degree x ≤ d"
unfolding degree_def
by (rule Least_le) (rule d)

lemma degree_gt: "pdevs_apply x j ≠ 0 ⟹ degree x > j"
by auto

lemma pdevs_val_pdevs_domain: "pdevs_val e X = (∑i∈pdevs_domain X. e i *⇩R pdevs_apply X i)"
by (auto simp: pdevs_val_def intro!: suminf_finite)

lemma pdevs_val_sum_le: "degree X ≤ d ⟹ pdevs_val e X = (∑i < d. e i *⇩R pdevs_apply X i)"
by (force intro!: degree_gt sum.mono_neutral_cong_left simp: pdevs_val_pdevs_domain)

lemmas pdevs_val_sum = pdevs_val_sum_le[OF order_refl]

lemma pdevs_val_zero[simp]: "pdevs_val (λ_. 0) x = 0"
by (auto simp: pdevs_val_sum)

lemma degree_eqI:
assumes "pdevs_apply x d ≠ 0"
assumes "⋀j. j > d ⟹ pdevs_apply x j = 0"
shows "degree x = Suc d"
unfolding eq_iff
by (auto intro!: degree_gt degree_le assms simp: Suc_le_eq)

lemma finite_degree_nonzero[intro, simp]: "finite {i. pdevs_apply x i ≠ 0}"
by transfer (auto simp: vimage_def Collect_neg_eq)

lemma degree_eq_Suc_max:
"degree x = (if (∀i. pdevs_apply x i = 0) then 0 else Suc (Max {i. pdevs_apply x i ≠ 0}))"
proof -
{
assume "⋀i. pdevs_apply x i = 0"
hence ?thesis
by auto (metis degree_le le_0_eq)
} moreover {
fix i assume "pdevs_apply x i ≠ 0"
hence ?thesis
using Max_in[OF finite_degree_nonzero, of x]
by (auto intro!: degree_eqI) (metis Max.coboundedI[OF finite_degree_nonzero] in_pdevs_domain
le_eq_less_or_eq less_asym pdevs_domain_def)
} ultimately show ?thesis
by blast
qed

lemma pdevs_val_degree_cong:
assumes "b = d"
assumes "⋀i. i < degree b ⟹ a i = c i"
shows "pdevs_val a b = pdevs_val c d"
using assms
by (auto simp: pdevs_val_sum)

abbreviation degree_aform::"'a::real_vector aform ⇒ nat"
where "degree_aform X ≡ degree (snd X)"

lemma degree_cong: "(⋀i. (pdevs_apply x i = 0) = (pdevs_apply y i = 0)) ⟹ degree x = degree y"
unfolding degree_def
by auto

lemma Least_True_nat[intro, simp]: "(LEAST i::nat. True) = 0"
by (metis (lifting) One_nat_def less_one not_less_Least not_less_eq)

lemma sorted_list_of_pdevs_domain_eq:
"sorted_list_of_set (pdevs_domain X) = filter ((≠) 0 o pdevs_apply X) [0..<degree X]"
by (auto simp: degree_gt intro!: sorted_distinct_set_unique sorted_filter[of "λx. x", simplified])

subsection ‹Total Deviation›

definition tdev::"'a::ordered_euclidean_space pdevs ⇒ 'a" where
"tdev x = (∑i<degree x. ¦pdevs_apply x i¦)"

lemma abs_pdevs_val_le_tdev: "e ∈ UNIV → {-1 .. 1} ⟹ ¦pdevs_val e x¦ ≤ tdev x"
by (force simp: pdevs_val_sum tdev_def abs_scaleR Pi_iff
intro!: order_trans[OF sum_abs] sum_mono scaleR_left_le_one_le
intro: abs_leI)

subsection ‹Binary Pointwise Operations›

definition binop_pdevs_raw::"('a::zero ⇒ 'b::zero ⇒ 'c::zero) ⇒
(nat ⇒ 'a) ⇒ (nat ⇒ 'b) ⇒ nat ⇒ 'c"
where "binop_pdevs_raw f x y i = (if x i = 0 ∧ y i = 0 then 0 else f (x i) (y i))"

lemma nonzeros_binop_pdevs_subset:
"{i. binop_pdevs_raw f x y i ≠ 0} ⊆ {i. x i ≠ 0} ∪ {i. y i ≠ 0}"
by (auto simp: binop_pdevs_raw_def)

lift_definition binop_pdevs::
"('a ⇒ 'b ⇒ 'c) ⇒ 'a::zero pdevs ⇒ 'b::zero pdevs ⇒ 'c::zero pdevs"
is binop_pdevs_raw
using nonzeros_binop_pdevs_subset
by (rule finite_subset) auto

lemma pdevs_apply_binop_pdevs[simp]: "pdevs_apply (binop_pdevs f x y) i =
(if pdevs_apply x i = 0 ∧ pdevs_apply y i = 0 then 0 else f (pdevs_apply x i) (pdevs_apply y i))"
by transfer (auto simp: binop_pdevs_raw_def)

definition add_pdevs::"'a::real_vector pdevs ⇒ 'a pdevs ⇒ 'a pdevs"

"pdevs_apply (add_pdevs X Y) n = pdevs_apply X n + pdevs_apply Y n"

fixes x y::"'a::euclidean_space"
shows "pdevs_val e (add_pdevs X Y) = pdevs_val e X + pdevs_val e Y"
proof -
let ?sum = "λm X. ∑i < m. e i *⇩R pdevs_apply X i"
let ?m = "max (degree X) (degree Y)"
have "pdevs_val e X + pdevs_val e Y = ?sum (degree X) X + ?sum (degree Y) Y"
also have "?sum (degree X) X = ?sum ?m X"
by (rule sum.mono_neutral_cong_left) auto
also have "?sum (degree Y) Y = ?sum ?m Y"
by (rule sum.mono_neutral_cong_left) auto
also have "?sum ?m X + ?sum ?m Y = (∑i < ?m. e i *⇩R (pdevs_apply X i + pdevs_apply Y i))"
also have "… = (∑i. e i *⇩R (pdevs_apply X i + pdevs_apply Y i))"
by (rule suminf_finite[symmetric]) auto
also have "… = pdevs_val e (add_pdevs X Y)"
finally show "pdevs_val e (add_pdevs X Y) = pdevs_val e X + pdevs_val e Y" by simp
qed

subsection ‹Total Deviation›

lemma tdev_eq_zero_iff: fixes X::"real pdevs" shows "tdev X = 0 ⟷ (∀e. pdevs_val e X = 0)"
by (force simp add: pdevs_val_sum tdev_def sum_nonneg_eq_0_iff
dest!: spec[where x="λi. if pdevs_apply X i ≥ 0 then 1 else -1"] split: if_split_asm)

lemma tdev_nonneg[intro, simp]: "tdev X ≥ 0"
by (auto simp: tdev_def)

lemma tdev_nonpos_iff[simp]: "tdev X ≤ 0 ⟷ tdev X = 0"
by (auto simp: order.antisym)

subsection ‹Unary Operations›

definition unop_pdevs_raw::
"('a::zero ⇒ 'b::zero) ⇒ (nat ⇒ 'a) ⇒ nat ⇒ 'b"
where "unop_pdevs_raw f x i = (if x i = 0 then 0 else f (x i))"

lemma nonzeros_unop_pdevs_subset: "{i. unop_pdevs_raw f x i ≠ 0} ⊆ {i. x i ≠ 0}"
by (auto simp: unop_pdevs_raw_def)

lift_definition unop_pdevs::
"('a ⇒ 'b) ⇒ 'a::zero pdevs ⇒ 'b::zero pdevs"
is unop_pdevs_raw
using nonzeros_unop_pdevs_subset
by (rule finite_subset) auto

lemma pdevs_apply_unop_pdevs[simp]: "pdevs_apply (unop_pdevs f x) i =
(if pdevs_apply x i = 0 then 0 else f (pdevs_apply x i))"
by transfer (auto simp: unop_pdevs_raw_def)

lemma pdevs_domain_unop_linear:
assumes "linear f"
shows "pdevs_domain (unop_pdevs f x) ⊆ pdevs_domain x"
proof -
interpret f: linear f by fact
show ?thesis
by (auto simp: f.zero)
qed

lemma
pdevs_val_unop_linear:
assumes "linear f"
shows "pdevs_val e (unop_pdevs f x) = f (pdevs_val e x)"
proof -
interpret f: linear f by fact
have *: "⋀i. (if pdevs_apply x i = 0 then 0 else f (pdevs_apply x i)) = f (pdevs_apply x i)"
by (auto simp: f.zero)
have "pdevs_val e (unop_pdevs f x) =
(∑i∈pdevs_domain (unop_pdevs f x). e i *⇩R f (pdevs_apply x i))"
by (auto simp add: pdevs_val_pdevs_domain *)
also have "… = (∑xa∈pdevs_domain x. e xa *⇩R f (pdevs_apply x xa))"
by (auto intro!: sum.mono_neutral_cong_left)
also have "… = f (pdevs_val e x)"
by (auto simp add: pdevs_val_pdevs_domain f.sum f.scaleR)
finally show ?thesis .
qed

subsection ‹Pointwise Scaling of Partial Deviations›

definition scaleR_pdevs::"real ⇒ 'a::real_vector pdevs ⇒ 'a pdevs"
where "scaleR_pdevs r x = unop_pdevs ((*⇩R) r) x"

lemma pdevs_apply_scaleR_pdevs[simp]:
"pdevs_apply (scaleR_pdevs x Y) n = x *⇩R pdevs_apply Y n"
by (auto simp: scaleR_pdevs_def)

lemma degree_scaleR_pdevs[simp]: "degree (scaleR_pdevs r x) = (if r = 0 then 0 else degree x)"
unfolding degree_def
by auto

lemma pdevs_val_scaleR_pdevs[simp]:
fixes x::real and Y::"'a::real_normed_vector pdevs"
shows "pdevs_val e (scaleR_pdevs x Y) = x *⇩R pdevs_val e Y"
by (auto simp: pdevs_val_sum scaleR_sum_right ac_simps)

subsection ‹Partial Deviations Scale Pointwise›

definition pdevs_scaleR::"real pdevs ⇒ 'a::real_vector ⇒ 'a pdevs"
where "pdevs_scaleR r x = unop_pdevs (λr. r *⇩R x) r"

lemma pdevs_apply_pdevs_scaleR[simp]:
"pdevs_apply (pdevs_scaleR X y) n = pdevs_apply X n *⇩R y"
by (auto simp: pdevs_scaleR_def)

lemma degree_pdevs_scaleR[simp]: "degree (pdevs_scaleR r x) = (if x = 0 then 0 else degree r)"
unfolding degree_def
by auto

lemma pdevs_val_pdevs_scaleR[simp]:
fixes X::"real pdevs" and y::"'a::real_normed_vector"
shows "pdevs_val e (pdevs_scaleR X y) = pdevs_val e X *⇩R y"
by (auto simp: pdevs_val_sum scaleR_sum_left)

subsection ‹Pointwise Unary Minus›

definition uminus_pdevs::"'a::real_vector pdevs ⇒ 'a pdevs"
where "uminus_pdevs = unop_pdevs uminus"

lemma pdevs_apply_uminus_pdevs[simp]: "pdevs_apply (uminus_pdevs x) = - pdevs_apply x"
by (auto simp: uminus_pdevs_def)

lemma degree_uminus_pdevs[simp]: "degree (uminus_pdevs x) = degree x"
by (rule degree_cong) simp

lemma pdevs_val_uminus_pdevs[simp]: "pdevs_val e (uminus_pdevs x) = - pdevs_val e x"
unfolding pdevs_val_sum
by (auto simp: sum_negf)

definition "uminus_aform X = (- fst X, uminus_pdevs (snd X))"

lemma fst_uminus_aform[simp]: "fst (uminus_aform Y) = - fst Y"

lemma aform_val_uminus_aform[simp]: "aform_val e (uminus_aform X) = - aform_val e X"
by (auto simp: uminus_aform_def aform_val_def)

subsection ‹Constant›

lift_definition zero_pdevs::"'a::zero pdevs" is "λ_. 0" by simp

lemma pdevs_apply_zero_pdevs[simp]: "pdevs_apply zero_pdevs i = 0"
by transfer simp

lemma pdevs_val_zero_pdevs[simp]: "pdevs_val e zero_pdevs = 0"
by (auto simp: pdevs_val_def)

definition "num_aform f = (f, zero_pdevs)"

subsection ‹Inner Product›

definition pdevs_inner::"'a::euclidean_space pdevs ⇒ 'a ⇒ real pdevs"
where "pdevs_inner x b = unop_pdevs (λx. x ∙ b) x"

lemma pdevs_apply_pdevs_inner[simp]: "pdevs_apply (pdevs_inner p a) i = pdevs_apply p i ∙ a"

lemma pdevs_val_pdevs_inner[simp]: "pdevs_val e (pdevs_inner p a) = pdevs_val e p ∙ a"
by (auto simp add: inner_sum_left pdevs_val_pdevs_domain intro!: sum.mono_neutral_cong_left)

definition inner_aform::"'a::euclidean_space aform ⇒ 'a ⇒ real aform"
where "inner_aform X b = (fst X ∙ b, pdevs_inner (snd X) b)"

subsection ‹Inner Product Pair›

definition inner2::"'a::euclidean_space ⇒ 'a ⇒ 'a ⇒ real*real"
where "inner2 x n l = (x ∙ n, x ∙ l)"

definition pdevs_inner2::"'a::euclidean_space pdevs ⇒ 'a ⇒ 'a ⇒ (real*real) pdevs"
where "pdevs_inner2 X n l = unop_pdevs (λx. inner2 x n l) X"

lemma pdevs_apply_pdevs_inner2[simp]: "pdevs_apply (pdevs_inner2 p a b) i = (pdevs_apply p i ∙ a, pdevs_apply p i ∙ b)"
by (simp add: pdevs_inner2_def inner2_def zero_prod_def)

definition inner2_aform::"'a::euclidean_space aform ⇒ 'a ⇒ 'a ⇒ (real*real) aform"
where "inner2_aform X a b = (inner2 (fst X) a b, pdevs_inner2 (snd X) a b)"

lemma linear_inner2[intro, simp]: "linear (λx. inner2 x n i)"
by unfold_locales (auto simp: inner2_def algebra_simps)

lemma aform_val_inner2_aform[simp]: "aform_val e (inner2_aform Z n i) = inner2 (aform_val e Z) n i"
proof -
have "aform_val e (inner2_aform Z n i) = inner2 (fst Z) n i + inner2 (pdevs_val e (snd Z)) n i"
by (auto simp: aform_val_def inner2_aform_def pdevs_inner2_def pdevs_val_unop_linear)
also have "… = inner2 (aform_val e Z) n i"
by (simp add: inner2_def algebra_simps aform_val_def)
finally show ?thesis .
qed

subsection ‹Update›

lemma pdevs_val_upd[simp]:
"pdevs_val (e(n := e')) X = pdevs_val e X - e n * pdevs_apply X n + e' * pdevs_apply X n"
unfolding pdevs_val_def
by (subst suminf_finite[OF finite.insertI[OF finite_degree_nonzero], of n X],
auto simp: pdevs_val_def sum.insert_remove)+

lemma nonzeros_fun_upd:
"{i. (f(n := a)) i ≠ 0} ⊆ {i. f i ≠ 0} ∪ {n}"
by (auto split: if_split_asm)

lift_definition pdev_upd::"'a::real_vector pdevs ⇒ nat ⇒ 'a ⇒ 'a pdevs"
is "λx n a. x(n:=a)"
by (rule finite_subset[OF nonzeros_fun_upd]) simp

lemma pdevs_apply_pdev_upd[simp]:
"pdevs_apply (pdev_upd X n x) = (pdevs_apply X)(n:=x)"
by transfer simp

lemma pdevs_val_pdev_upd[simp]:
"pdevs_val e (pdev_upd X n x) = pdevs_val e X + e n *⇩R x - e n *⇩R pdevs_apply X n"
unfolding pdevs_val_def
by (subst suminf_finite[OF finite.insertI[OF finite_degree_nonzero], of n X],
auto simp: pdevs_val_def sum.insert_remove)+

lemma degree_pdev_upd:
assumes "x = 0 ⟷ pdevs_apply X n = 0"
shows "degree (pdev_upd X n x) = degree X"
using assms
by (auto intro!: degree_cong split: if_split_asm)

lemma degree_pdev_upd_le:
assumes "degree X ≤ n"
shows "degree (pdev_upd X n x) ≤ Suc n"
using assms
by (auto intro!: degree_le)

subsection ‹Inf/Sup›

definition "Inf_aform X = fst X - tdev (snd X)"

definition "Sup_aform X = fst X + tdev (snd X)"

lemma Inf_aform:
assumes "e ∈ UNIV → {-1 .. 1}"
shows "Inf_aform X ≤ aform_val e X"
using order_trans[OF abs_ge_minus_self abs_pdevs_val_le_tdev[OF assms]]
by (auto simp: Inf_aform_def aform_val_def minus_le_iff)

lemma Sup_aform:
assumes "e ∈ UNIV → {-1 .. 1}"
shows "aform_val e X ≤ Sup_aform X"
using order_trans[OF abs_ge_self abs_pdevs_val_le_tdev[OF assms]]
by (auto simp: Sup_aform_def aform_val_def)

subsection ‹Minkowski Sum›

definition msum_pdevs_raw::"nat⇒(nat ⇒ 'a::real_vector)⇒(nat ⇒ 'a)⇒(nat⇒'a)" where
"msum_pdevs_raw n x y i = (if i < n then x i else y (i - n))"

lemma nonzeros_msum_pdevs_raw:
"{i. msum_pdevs_raw n f g i ≠ 0} = ({0..<n} ∩ {i. f i ≠ 0}) ∪ (+) n  ({i. g i ≠ 0})"
by (force simp: msum_pdevs_raw_def not_less split: if_split_asm)

lift_definition msum_pdevs::"nat⇒'a::real_vector pdevs⇒'a pdevs⇒'a pdevs" is msum_pdevs_raw
unfolding nonzeros_msum_pdevs_raw by simp

lemma pdevs_apply_msum_pdevs: "pdevs_apply (msum_pdevs n f g) i =
(if i < n then pdevs_apply f i else pdevs_apply g (i - n))"
by transfer (auto simp: msum_pdevs_raw_def)

lemma degree_least_nonzero:
assumes "degree f ≠ 0"
shows "pdevs_apply f (degree f - 1) ≠ 0"
proof
assume H: "pdevs_apply f (degree f - 1) = 0"
{
fix j
assume "j≥degree f - 1"
with H have "pdevs_apply f j = 0"
by (cases "degree f - 1 = j") auto
}
from degree_le[rule_format, OF this]
have "degree f ≤ degree f - 1"
by blast
with assms show False by simp
qed

lemma degree_leI:
assumes "(⋀i. pdevs_apply y i = 0 ⟹ pdevs_apply x i = 0)"
shows "degree x ≤ degree y"
proof cases
assume "degree x ≠ 0"
from degree_least_nonzero[OF this]
have "pdevs_apply y (degree x - 1) ≠ 0"
by (auto simp: assms split: if_split_asm)
from degree_gt[OF this] show ?thesis
by simp
qed simp

lemma degree_msum_pdevs_ge1:
shows "degree f ≤ n ⟹ degree f ≤ degree (msum_pdevs n f g)"
by (rule degree_leI) (auto simp: pdevs_apply_msum_pdevs split: if_split_asm)

lemma degree_msum_pdevs_ge2:
assumes "degree f ≤ n"
shows "degree g ≤ degree (msum_pdevs n f g) - n"
proof cases
assume "degree g ≠ 0"
hence "pdevs_apply g (degree g - 1) ≠ 0" by (rule degree_least_nonzero)
hence "pdevs_apply (msum_pdevs n f g) (n + degree g - 1) ≠ 0"
using assms
by (auto simp: pdevs_apply_msum_pdevs)
from degree_gt[OF this]
show ?thesis
by simp
qed simp

lemma degree_msum_pdevs_le:
shows "degree (msum_pdevs n f g) ≤ n + degree g"
by (auto intro!: degree_le simp: pdevs_apply_msum_pdevs)

lemma
sum_msum_pdevs_cases:
assumes "degree f ≤ n"
assumes [simp]: "⋀i. e i 0 = 0"
shows
"(∑i <degree (msum_pdevs n f g).
e i (if i < n then pdevs_apply f i else pdevs_apply g (i - n))) =
(∑i <degree f. e i (pdevs_apply f i)) + (∑i <degree g. e (i + n) (pdevs_apply g i))"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∑i∈{..<degree (msum_pdevs n f g)} ∩ {i. i < n}. e i (pdevs_apply f i)) +
(∑i∈{..<degree (msum_pdevs n f g)} ∩ - {i. i < n}. e i (pdevs_apply g (i - n)))"
(is "_ = ?sum_f + ?sum_g")
also have "?sum_f = (∑i = 0..<degree f. e i (pdevs_apply f i))"
using assms degree_msum_pdevs_ge1[of f n g]
by (intro sum.mono_neutral_cong_right) auto
also
have "?sum_g = (∑i∈{0 + n..<degree (msum_pdevs n f g) - n + n}. e i (pdevs_apply g (i - n)))"
by (rule sum.cong) auto
also have "… = (∑i = 0..<degree (msum_pdevs n f g) - n. e (i + n) (pdevs_apply g (i + n - n)))"
by (rule sum.shift_bounds_nat_ivl)
also have "… = (∑i = 0..<degree g. e (i + n) (pdevs_apply g i))"
using assms degree_msum_pdevs_ge2[of f n]
by (intro sum.mono_neutral_cong_right) (auto intro!: sum.mono_neutral_cong_right)
finally show ?thesis
qed

lemma tdev_msum_pdevs: "degree f ≤ n ⟹ tdev (msum_pdevs n f g) = tdev f + tdev g"
by (auto simp: tdev_def pdevs_apply_msum_pdevs intro!: sum_msum_pdevs_cases)

lemma pdevs_val_msum_pdevs:
"degree f ≤ n ⟹ pdevs_val e (msum_pdevs n f g) = pdevs_val e f + pdevs_val (λi. e (i + n)) g"
by (auto simp: pdevs_val_sum pdevs_apply_msum_pdevs intro!: sum_msum_pdevs_cases)

definition msum_aform::"nat ⇒ 'a::real_vector aform ⇒ 'a aform ⇒ 'a aform"
where "msum_aform n f g = (fst f + fst g, msum_pdevs n (snd f) (snd g))"

lemma fst_msum_aform[simp]: "fst (msum_aform n f g) = fst f + fst g"

lemma snd_msum_aform[simp]: "snd (msum_aform n f g) = msum_pdevs n (snd f) (snd g)"

lemma finite_nonzero_summable: "finite {i. f i ≠ 0} ⟹ summable f"
by (auto intro!: sums_summable sums_finite)

lemma aform_val_msum_aform:
assumes "degree_aform f ≤ n"
shows "aform_val e (msum_aform n f g) = aform_val e f + aform_val (λi. e (i + n)) g"
using assms
by (auto simp: pdevs_val_msum_pdevs aform_val_def)

lemma Inf_aform_msum_aform:
"degree_aform X ≤ n ⟹ Inf_aform (msum_aform n X Y) = Inf_aform X + Inf_aform Y"

lemma Sup_aform_msum_aform:
"degree_aform X ≤ n ⟹ Sup_aform (msum_aform n X Y) = Sup_aform X + Sup_aform Y"

definition "independent_from d Y = msum_aform d (0, zero_pdevs) Y"

definition "independent_aform X Y = independent_from (degree_aform X) Y"

lemma degree_zero_pdevs[simp]: "degree zero_pdevs = 0"
by (metis degree_least_nonzero pdevs_apply_zero_pdevs)

lemma independent_aform_Joints:
assumes "x ∈ Affine X"
assumes "y ∈ Affine Y"
shows "[x, y] ∈ Joints [X, independent_aform X Y]"
using assms
unfolding Affine_def valuate_def Joints_def
apply safe
subgoal premises prems for e ea
using prems
by (intro image_eqI[where x="λi. if i < degree_aform X then e i else ea (i - degree_aform X)"])
(auto simp: aform_val_def pdevs_val_msum_pdevs Pi_iff
independent_aform_def independent_from_def intro!: pdevs_val_degree_cong)
done

lemma msum_aform_Joints:
assumes "d ≥ degree_aform X"
assumes "⋀X. X ∈ set XS ⟹ d ≥ degree_aform X"
assumes "(x#xs) ∈ Joints (X#XS)"
assumes "y ∈ Affine Y"
shows "((x + y)#x#xs) ∈ Joints (msum_aform d X Y#X#XS)"
using assms
unfolding Joints_def valuate_def Affine_def
proof (safe, goal_cases)
case (1 e ea a b zs)
then show ?case
by (intro image_eqI[where x = "λi. if i < d then e i else ea (i - d)"])
(force simp: aform_val_def pdevs_val_msum_pdevs intro!: intro!: pdevs_val_degree_cong)+
qed

lemma Joints_msum_aform:
assumes "d ≥ degree_aform X"
assumes "⋀Y. Y ∈ set YS ⟹ d ≥ degree_aform Y"
shows "Joints (msum_aform d X Y#YS) = {((x + y)#ys) |x y ys. y ∈ Affine Y ∧ x#ys ∈ Joints (X#YS)}"
unfolding Affine_def valuate_def Joints_def
proof (safe, goal_cases)
case (1 x e)
thus ?case
using assms
by (intro exI[where x = "aform_val e X"] exI[where x = "aform_val ((λi. e (i + d))) Y"])
next
case (2 x xa y ys e ea)
thus ?case using assms
by (intro image_eqI[where x="λi. if i < d then ea i else e (i - d)"])
(force simp: aform_val_def pdevs_val_msum_pdevs Pi_iff intro!: pdevs_val_degree_cong)+
qed

lemma Joints_singleton_image: "Joints [x] = (λx. [x])  Affine x"
by (auto simp: Joints_def Affine_def valuate_def)

lemma Collect_extract_image: "{g (f x y) |x y. P x y} = g  {f x y |x y. P x y}"
by auto

lemma inj_Cons: "inj (λx. x#xs)"
by (auto intro!: injI)

lemma Joints_Nil[simp]: "Joints [] = {[]}"
by (force simp: Joints_def valuate_def)

lemma msum_pdevs_zero_ident[simp]: "msum_pdevs 0 zero_pdevs x = x"
by transfer (auto simp: msum_pdevs_raw_def)

lemma msum_aform_zero_ident[simp]: "msum_aform 0 (0, zero_pdevs) x = x"

lemma mem_Joints_singleton: "(x ∈ Joints [X]) = (∃y. x = [y] ∧ y ∈ Affine X)"
by (auto simp: Affine_def valuate_def Joints_def)

lemma singleton_mem_Joints[simp]: "[x] ∈ Joints [X] ⟷ x ∈ Affine X"
by (auto simp: mem_Joints_singleton)

lemma msum_aform_Joints_without_first:
assumes "d ≥ degree_aform X"
assumes "⋀X. X ∈ set XS ⟹ d ≥ degree_aform X"
assumes "(x#xs) ∈ Joints (X#XS)"
assumes "y ∈ Affine Y"
assumes "z = x + y"
shows "z#xs ∈ Joints (msum_aform d X Y#XS)"
unfolding ‹z = x + y›
using msum_aform_Joints[OF assms(1-4)]
by (force simp: Joints_def valuate_def)

lemma Affine_msum_aform:
assumes "d ≥ degree_aform X"
shows "Affine (msum_aform d X Y) = {x + y |x y. x ∈ Affine X ∧ y ∈ Affine Y}"
using Joints_msum_aform[OF assms, of Nil Y, simplified, unfolded mem_Joints_singleton]
by (auto simp add: Joints_singleton_image Collect_extract_image[where g="λx. [x]"]
inj_image_eq_iff[OF inj_Cons] )

lemma Affine_zero_pdevs[simp]: "Affine (0, zero_pdevs) = {0}"
by (force simp: Affine_def valuate_def aform_val_def)

lemma Affine_independent_aform:
"Affine (independent_aform X Y) = Affine Y"
by (auto simp: independent_aform_def independent_from_def Affine_msum_aform)

lemma
abs_diff_eq1:
fixes l u::"'a::ordered_euclidean_space"
shows "l ≤ u ⟹ ¦u - l¦ = u - l"

lemma compact_sum:
fixes f :: "'a ⇒ 'b::topological_space ⇒ 'c::real_normed_vector"
assumes "finite I"
assumes "⋀i. i ∈ I ⟹ compact (S i)"
assumes "⋀i. i ∈ I ⟹ continuous_on (S i) (f i)"
assumes "I ⊆ J"
shows "compact {∑i∈I. f i (x i) | x. x ∈ Pi J S}"
using assms
proof (induct I)
case empty
thus ?case
proof (cases "∃x. x ∈ Pi J S")
case False
hence *: "{∑i∈{}. f i (x i) |x. x ∈ Pi J S} = {}"
by (auto simp: Pi_iff)
show ?thesis unfolding * by simp
qed auto
next
case (insert a I)
hence "{∑i∈insert a I. f i (xa i) |xa. xa ∈ Pi J S}
= {x + y |x y. x ∈ f a  S a ∧ y ∈ {∑i∈I. f i (x i) |x. x ∈ Pi J S}}"
proof safe
fix s x
assume "s ∈ S a" "x ∈ Pi J S"
thus "∃xa. f a s + (∑i∈I. f i (x i)) = (∑i∈insert a I. f i (xa i)) ∧ xa ∈ Pi J S"
using insert
by (auto intro!: exI[where x="x(a:=s)"] sum.cong)
qed force
also have "compact …"
using insert
by (intro compact_sums) (auto intro!: compact_continuous_image)
finally show ?case .
qed

lemma compact_Affine:
fixes X::"'a::ordered_euclidean_space aform"
shows "compact (Affine X)"
proof -
have "Affine X = {x + y|x y. x ∈ {fst X} ∧
y ∈ {(∑i ∈ {0..<degree_aform X}. e i *⇩R pdevs_apply (snd X) i) | e. e ∈ UNIV → {-1 .. 1}}}"
by (auto simp: Affine_def valuate_def aform_val_def pdevs_val_sum atLeast0LessThan)
also have "compact …"
by (rule compact_sums) (auto intro!: compact_sum continuous_intros)
finally show ?thesis .
qed

lemma Joints2_JointsI:
"(xs, x) ∈ Joints2 XS X ⟹ x#xs ∈ Joints (X#XS)"
by (auto simp: Joints_def Joints2_def valuate_def)

subsection ‹Splitting›

definition "split_aform X i =
(let xi = pdevs_apply (snd X) i /⇩R 2
in ((fst X - xi, pdev_upd (snd X) i xi), (fst X + xi, pdev_upd (snd X) i xi)))"

lemma split_aformE:
assumes "e ∈ UNIV → {-1 .. 1}"
assumes "x = aform_val e X"
obtains err where "x = aform_val (e(i:=err)) (fst (split_aform X i))" "err ∈ {-1 .. 1}"
| err where "x = aform_val (e(i:=err)) (snd (split_aform X i))" "err ∈ {-1 .. 1}"
proof (atomize_elim)
let ?thesis = "(∃err. x = aform_val (e(i := err)) (fst (split_aform X i)) ∧ err ∈ {- 1..1}) ∨
(∃err. x = aform_val (e(i := err)) (snd (split_aform X i)) ∧ err ∈ {- 1..1})"
{
assume "pdevs_apply (snd X) i = 0"
hence "X = fst (split_aform X i)"
by (auto simp: split_aform_def intro!: prod_eqI pdevs_eqI)
with assms have ?thesis by (auto intro!: exI[where x="e i"])
} moreover {
assume "pdevs_apply (snd X) i ≠ 0"
hence [simp]: "degree_aform X > i"
by (rule degree_gt)
note assms(2)
also
have "aform_val e X = fst X + (∑i<degree_aform X. e i *⇩R pdevs_apply (snd X) i)"
also
have rewr: "{..<degree_aform X} = {0..<degree_aform X} - {i} ∪ {i}"
by auto
have "(∑i<degree_aform X. e i *⇩R pdevs_apply (snd X) i) =
(∑i ∈ {0..<degree_aform X} - {i}. e i *⇩R pdevs_apply (snd X) i) +
e i *⇩R pdevs_apply (snd X) i"
by (subst rewr, subst sum.union_disjoint) auto
finally have "x = fst X + …" .
hence "x = aform_val (e(i:=2 * e i - 1)) (snd (split_aform X i))"
"x = aform_val (e(i:=2 * e i + 1)) (fst (split_aform X i))"
by (auto simp: aform_val_def split_aform_def Let_def pdevs_val_sum atLeast0LessThan
Diff_eq degree_pdev_upd if_distrib sum.If_cases field_simps
scaleR_left_distrib[symmetric])
moreover
have "2 * e i - 1 ∈ {-1 .. 1} ∨ 2 * e i + 1 ∈ {-1 .. 1}"
using assms by (auto simp: not_le Pi_iff dest!: spec[where x=i])
ultimately have ?thesis by blast
} ultimately show ?thesis by blast
qed

lemma pdevs_val_add: "pdevs_val (λi. e i + f i) xs = pdevs_val e xs + pdevs_val f xs"
by (auto simp: pdevs_val_pdevs_domain algebra_simps sum.distrib)

lemma pdevs_val_minus: "pdevs_val (λi. e i - f i) xs = pdevs_val e xs - pdevs_val f xs"
by (auto simp: pdevs_val_pdevs_domain algebra_simps sum_subtractf)

lemma pdevs_val_cmul: "pdevs_val (λi. u * e i) xs = u *⇩R pdevs_val e xs"
by (auto simp: pdevs_val_pdevs_domain scaleR_sum_right)

lemma atLeastAtMost_absI: "- a ≤ a ⟹ ¦x::real¦ ≤ ¦a¦ ⟹ x ∈ atLeastAtMost (- a) a"
by auto

lemma divide_atLeastAtMost_1_absI: "¦x::real¦ ≤ ¦a¦ ⟹ x/a ∈ {-1 .. 1}"
by (intro atLeastAtMost_absI) (auto simp: divide_le_eq_1)

lemma convex_scaleR_aux: "u + v = 1 ⟹ u *⇩R x + v *⇩R x = (x::'a::real_vector)"

lemma convex_mult_aux: "u + v = 1 ⟹ u * x + v * x = (x::real)"
using convex_scaleR_aux[of u v x] by simp

lemma convex_Affine: "convex (Affine X)"
proof (rule convexI)
fix x y::'a and u v::real
assume "x ∈ Affine X" "y ∈ Affine X" and convex: "0 ≤ u" "0 ≤ v" "u + v = 1"
then obtain e f where x: "x = aform_val e X" "e ∈ UNIV → {-1 .. 1}"
and y: "y = aform_val f X" "f ∈ UNIV → {-1 .. 1}"
by (auto simp: Affine_def valuate_def)
let ?conv = "λi. u * e i + v * f i"
{
fix i
have "¦?conv i¦ ≤ u * ¦e i¦ + v * ¦f i¦"
using convex by (intro order_trans[OF abs_triangle_ineq]) (simp add: abs_mult)
also have "… ≤ 1"
using convex x y
by (intro convex_bound_le) (auto simp: Pi_iff abs_real_def)
finally have "?conv i ≤ 1" "-1 ≤ ?conv i"
by (auto simp: abs_real_def split: if_split_asm)
}
thus "u *⇩R x + v *⇩R y ∈ Affine X"
using convex x y
by (auto simp: Affine_def valuate_def aform_val_def pdevs_val_add pdevs_val_cmul algebra_simps
convex_scaleR_aux intro!: image_eqI[where x="?conv"])
qed

lemma segment_in_aform_val:
assumes "e ∈ UNIV → {-1 .. 1}"
assumes "f ∈ UNIV → {-1 .. 1}"
shows "closed_segment (aform_val e X) (aform_val f X) ⊆ Affine X"
proof -
have "aform_val e X ∈ Affine X" "aform_val f X ∈ Affine X"
using assms by (auto simp: Affine_def valuate_def)
with convex_Affine[of X, simplified convex_contains_segment]
show ?thesis
by simp
qed

subsection ‹From List of Generators›

lift_definition pdevs_of_list::"'a::zero list ⇒ 'a pdevs"
is "λxs i. if i < length xs then xs ! i else 0"
by auto

lemma pdevs_apply_pdevs_of_list:
"pdevs_apply (pdevs_of_list xs) i = (if i < length xs then xs ! i else 0)"
by transfer simp

lemma pdevs_apply_pdevs_of_list_Nil[simp]:
"pdevs_apply (pdevs_of_list []) i = 0"
by transfer auto

lemma pdevs_apply_pdevs_of_list_Cons:
"pdevs_apply (pdevs_of_list (x # xs)) i =
(if i = 0 then x else pdevs_apply (pdevs_of_list xs) (i - 1))"
by transfer auto

lemma pdevs_domain_pdevs_of_list_Cons[simp]: "pdevs_domain (pdevs_of_list (x # xs)) =
(if x = 0 then {} else {0}) ∪ (+) 1  pdevs_domain (pdevs_of_list xs)"
by (force simp: pdevs_apply_pdevs_of_list_Cons split: if_split_asm)

lemma pdevs_val_pdevs_of_list_eq[simp]:
"pdevs_val e (pdevs_of_list (x # xs)) = e 0 *⇩R x + pdevs_val (e o (+) 1) (pdevs_of_list xs)"
proof -
have "pdevs_val e (pdevs_of_list (x # xs)) =
(∑i∈pdevs_domain (pdevs_of_list (x # xs)) ∩ {0}. e i *⇩R x) +
(∑i∈pdevs_domain (pdevs_of_list (x # xs)) ∩ - {0}.
e i *⇩R pdevs_apply (pdevs_of_list xs) (i - Suc 0))"
(is "_ = ?l + ?r")
by (simp add: pdevs_val_pdevs_domain if_distrib sum.If_cases pdevs_apply_pdevs_of_list_Cons)
also
have "?r = (∑i∈pdevs_domain (pdevs_of_list xs). e (Suc i) *⇩R pdevs_apply (pdevs_of_list xs) i)"
by (rule sum.reindex_cong[of "λi. i + 1"]) auto
also have "… = pdevs_val (e o (+) 1) (pdevs_of_list xs)"
also have "?l = (∑i∈{0}. e i *⇩R x)"
by (rule sum.mono_neutral_cong_left) auto
also have "… = e 0 *⇩R x" by simp
finally show ?thesis .
qed

lemma
less_degree_pdevs_of_list_imp_less_length:
assumes "i < degree (pdevs_of_list xs)"
shows "i < length xs"
proof -
from assms have "pdevs_apply (pdevs_of_list xs) (degree (pdevs_of_list xs) - 1) ≠ 0"
by (metis degree_least_nonzero less_nat_zero_code)
hence "degree (pdevs_of_list xs) - 1 < length xs"
by (simp add: pdevs_apply_pdevs_of_list split: if_split_asm)
with assms show ?thesis
by simp
qed

lemma tdev_pdevs_of_list[simp]: "tdev (pdevs_of_list xs) = sum_list (map abs xs)"
by (auto simp: tdev_def pdevs_apply_pdevs_of_list sum_list_sum_nth
less_degree_pdevs_of_list_imp_less_length
intro!: sum.mono_neutral_cong_left degree_gt)

lemma pdevs_of_list_Nil[simp]: "pdevs_of_list [] = zero_pdevs"
by (auto intro!: pdevs_eqI)

lemma pdevs_val_inj_sumI:
fixes K::"'a set" and g::"'a ⇒ nat"
assumes "finite K"
assumes "inj_on g K"
assumes "pdevs_domain x ⊆ g  K"
assumes "⋀i. i ∈ K ⟹ g i ∉ pdevs_domain x ⟹ f i = 0"
assumes "⋀i. i ∈ K ⟹ g i ∈ pdevs_domain x ⟹ f i = e (g i) *⇩R pdevs_apply x (g i)"
shows "pdevs_val e x = (∑i∈K. f i)"
proof -
have [simp]: "inj_on (the_inv_into K g) (pdevs_domain x)"
using assms
by (auto simp: intro!: subset_inj_on[OF inj_on_the_inv_into])
{
fix y assume y: "y ∈ pdevs_domain x"
have g_inv: "g (the_inv_into K g y) = y"
by (meson assms(2) assms(3) y f_the_inv_into_f subset_eq)
have inv_in: "the_inv_into K g y ∈ K"
by (meson assms(2) assms(3) y subset_iff in_pdevs_domain the_inv_into_into)
have inv3: "the_inv_into (pdevs_domain x) (the_inv_into K g) (the_inv_into K g y) =
g (the_inv_into K g y)"
using assms y
by (subst the_inv_into_f_f) (auto simp: f_the_inv_into_f[OF assms(2)])
note g_inv inv_in inv3
} note this[simp]
have "pdevs_val e x = (∑i∈pdevs_domain x. e i *⇩R pdevs_apply x i)"
also have "… = (∑i ∈ the_inv_into K g  pdevs_domain x. e (g i) *⇩R pdevs_apply x (g i))"
by (rule sum.reindex_cong[OF inj_on_the_inv_into]) auto
also have "… = (∑i∈K. f i)"
using assms
by (intro sum.mono_neutral_cong_left) (auto simp: the_inv_into_image_eq)
finally show ?thesis .
qed

lemma pdevs_domain_pdevs_of_list_le: "pdevs_domain (pdevs_of_list xs) ⊆ {0..<length xs}"
by (auto simp: pdevs_apply_pdevs_of_list split: if_split_asm)

lemma pdevs_val_zip: "pdevs_val e (pdevs_of_list xs) = (∑(i,x)←zip [0..<length xs] xs. e i *⇩R x)"
by (auto simp: sum_list_distinct_conv_sum_set
in_set_zip image_fst_zip pdevs_apply_pdevs_of_list distinct_zipI1
intro!: pdevs_val_inj_sumI[of _ fst]
split: if_split_asm)

lemma scaleR_sum_list:
fixes xs::"'a::real_vector list"
shows "a *⇩R sum_list xs = sum_list (map (scaleR a) xs)"
by (induct xs) (auto simp: algebra_simps)

lemma pdevs_val_const_pdevs_of_list: "pdevs_val (λ_. c) (pdevs_of_list xs) = c *⇩R sum_list xs"
unfolding pdevs_val_zip split_beta' scaleR_sum_list
by (rule arg_cong) (auto intro!: nth_equalityI)

lemma pdevs_val_partition:
assumes "e ∈ UNIV → I"
obtains f g where "pdevs_val e (pdevs_of_list xs) =
pdevs_val f (pdevs_of_list (filter p xs)) +
pdevs_val g (pdevs_of_list (filter (Not o p) xs))"
"f ∈ UNIV → I"
"g ∈ UNIV → I"
proof -
obtain i where i: "i ∈ I"
by (metis assms funcset_mem iso_tuple_UNIV_I)
let ?zip = "zip [0..<length xs] xs"
define part where "part = partition (p ∘ snd) ?zip"
let ?f =
"(λn. if n < degree (pdevs_of_list (filter p xs)) then e (map fst (fst part) ! n) else i)"
let ?g =
"(λn. if n < degree (pdevs_of_list (filter (Not ∘ p) xs))
then e (map fst (snd part) ! n)
else i)"
show ?thesis
proof
have "pdevs_val e (pdevs_of_list xs) = (∑(i,x)←?zip. e i *⇩R x)"
by (rule pdevs_val_zip)
also have "… = (∑(i, x)∈set ?zip. e i *⇩R x)"
also
have [simp]: "set (fst part) ∩ set (snd part) = {}"
by (auto simp: part_def)
from partition_set[of "p o snd" ?zip "fst part" "snd part"]
have "set ?zip = set (fst part) ∪ set (snd part)"
by (auto simp: part_def)
also have "(∑a∈set (fst part) ∪ set (snd part). case a of (i, x) ⇒ e i *⇩R x) =
(∑(i, x)∈set (fst part). e i *⇩R x) + (∑(i, x)∈set (snd part). e i *⇩R x)"
by (auto simp: split_beta sum_Un)
also
have "(∑(i, x)∈set (fst part). e i *⇩R x) = (∑(i, x)←(fst part). e i *⇩R x)"
by (simp add: sum_list_distinct_conv_sum_set distinct_zipI1 part_def)
also have "… = (∑i<length (fst part). case (fst part ! i) of (i, x) ⇒ e i *⇩R x)"
by (subst sum_list_sum_nth) (simp add: split_beta' atLeast0LessThan)
also have "… =
pdevs_val (λn. e (map fst (fst part) ! n)) (pdevs_of_list (map snd (fst part)))"
by (force
simp: pdevs_val_zip sum_list_distinct_conv_sum_set distinct_zipI1 split_beta' in_set_zip
intro!:
sum.reindex_cong[where l=fst] image_eqI[where x = "(x, map snd (fst part) ! x)" for x])
also
have "(∑(i, x)∈set (snd part). e i *⇩R x) = (∑(i, x)←(snd part). e i *⇩R x)"
by (simp add: sum_list_distinct_conv_sum_set distinct_zipI1 part_def)
also have "… = (∑i<length (snd part). case (snd part ! i) of (i, x) ⇒ e i *⇩R x)"
by (subst sum_list_sum_nth) (simp add: split_beta' atLeast0LessThan)
also have "… =
pdevs_val (λn. e (map fst (snd part) ! n)) (pdevs_of_list (map snd (snd part)))"
by (force simp: pdevs_val_zip sum_list_distinct_conv_sum_set distinct_zipI1 split_beta'
in_set_zip
intro!: sum.reindex_cong[where l=fst]
image_eqI[where x = "(x, map snd (snd part) ! x)" for x])
also
have "pdevs_val (λn. e (map fst (fst part) ! n)) (pdevs_of_list (map snd (fst part))) =
pdevs_val (λn.
if n < degree (pdevs_of_list (map snd (fst part))) then e (map fst (fst part) ! n) else i)
(pdevs_of_list (map snd (fst part)))"
by (rule pdevs_val_degree_cong) simp_all
also
have "pdevs_val (λn. e (map fst (snd part) ! n)) (pdevs_of_list (map snd (snd part))) =
pdevs_val (λn.
if n < degree (pdevs_of_list (map snd (snd part))) then e (map fst (snd part) ! n) else i)
(pdevs_of_list (map snd (snd part)))"
by (rule pdevs_val_degree_cong) simp_all
also have "map snd (snd part) = filter (Not o p) xs"
by (simp add: part_def filter_map[symmetric] o_assoc)
also have "map snd (fst part) = filter p xs"
finally
show
"pdevs_val e (pdevs_of_list xs) =
pdevs_val ?f (pdevs_of_list (filter p xs)) +
pdevs_val ?g (pdevs_of_list (filter (Not ∘ p) xs))" .
show "?f ∈ UNIV → I" "?g ∈ UNIV → I"
using assms ‹i∈I›
by (auto simp: Pi_iff)
qed
qed

lemma pdevs_apply_pdevs_of_list_append:
"pdevs_apply (pdevs_of_list (xs @ zs)) i =
(if i < length xs
then pdevs_apply (pdevs_of_list xs) i else pdevs_apply (pdevs_of_list zs) (i - length xs))"
by (auto simp: pdevs_apply_pdevs_of_list nth_append)

lemma degree_pdevs_of_list_le_length[intro, simp]: "degree (pdevs_of_list xs) ≤ length xs"
by (metis less_irrefl_nat le_less_linear less_degree_pdevs_of_list_imp_less_length)

lemma degree_pdevs_of_list_append:
"degree (pdevs_of_list (xs @ ys)) ≤ length xs + degree (pdevs_of_list ys)"
by (rule degree_le) (auto simp: pdevs_apply_pdevs_of_list_append)

lemma pdevs_val_pdevs_of_list_append:
assumes "f ∈ UNIV → I"
assumes "g ∈ UNIV → I"
obtains e where
"pdevs_val f (pdevs_of_list xs) + pdevs_val g (pdevs_of_list ys) =
pdevs_val e (pdevs_of_list (xs @ ys))"
"e ∈ UNIV → I"
proof
let ?e = "(λi. if i < length xs then f i else g (i - length xs))"
have f: "pdevs_val f (pdevs_of_list xs) =
(∑i∈{..<length xs}. ?e i *⇩R pdevs_apply (pdevs_of_list (xs @ ys)) i)"
by (auto simp: pdevs_val_sum degree_gt pdevs_apply_pdevs_of_list_append
intro: sum.mono_neutral_cong_left)
have g: "pdevs_val g (pdevs_of_list ys) =
(∑i=length xs ..<length xs + degree (pdevs_of_list ys).
?e i *⇩R pdevs_apply (pdevs_of_list (xs @ ys)) i)"
(is "_ = ?sg")
by (auto simp: pdevs_val_sum pdevs_apply_pdevs_of_list_append
intro!: inj_onI image_eqI[where x="length xs + x" for x]
sum.reindex_cong[where l="λi. i - length xs"])
show "pdevs_val f (pdevs_of_list xs) + pdevs_val g (pdevs_of_list ys) =
pdevs_val ?e (pdevs_of_list (xs @ ys))"
unfolding f g
by (subst sum.union_disjoint[symmetric])
(force simp: pdevs_val_sum ivl_disj_un degree_pdevs_of_list_append
intro!: sum.mono_neutral_cong_right
split: if_split_asm)+
show "?e ∈ UNIV → I"
using assms by (auto simp: Pi_iff)
qed

lemma
sum_general_mono:
assumes [simp,intro]: "finite s" "finite t"
assumes f: "⋀x. x ∈ s - t ⟹ f x ≤ 0"
assumes g: "⋀x. x ∈ t - s ⟹ g x ≥ 0"
assumes fg: "⋀x. x ∈ s ∩ t ⟹ f x ≤ g x"
shows "(∑x ∈ s. f x) ≤ (∑x ∈ t. g x)"
proof -
have "s = (s - t) ∪ (s ∩ t)" and [intro, simp]: "(s - t) ∩ (s ∩ t) = {}" by auto
hence "(∑x ∈ s. f x) = (∑x ∈ s - t ∪ s ∩ t. f x)"
using assms by simp
also have "… = (∑x ∈ s - t. f x) + (∑x ∈ s ∩ t. f x)"
also have "(∑x ∈ s - t. f x) ≤ 0"
by (auto intro!: sum_nonpos f)
also have "0 ≤ (∑x ∈ t - s. g x)"
by (auto intro!: sum_nonneg g)
also have "(∑x ∈ s ∩ t. f x) ≤ (∑x ∈ s ∩ t. g x)"
by (auto intro!: sum_mono fg)
also
have [intro, simp]: "(t - s) ∩ (s ∩ t) = {}" by auto
hence "sum g (t - s) + sum g (s ∩ t) = sum g ((t - s) ∪ (s ∩ t))"
also have "… = sum g t"
by (auto intro!: sum.cong)
finally show ?thesis by simp
qed

lemma pdevs_val_perm_ex:
assumes "xs <~~> ys"
assumes mem: "e ∈ UNIV → I"
shows "∃e'. e' ∈ UNIV → I ∧ pdevs_val e (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list ys)"
using assms
proof (induct arbitrary: e)
case Nil
thus ?case
by auto
next
case (Cons xs ys z)
hence "(e ∘ (+) (Suc 0)) ∈ UNIV → I" by auto
from Cons(2)[OF this] obtain e' where "e' ∈ UNIV → I"
"pdevs_val (e ∘ (+) (Suc 0)) (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list ys)"
by metis
thus ?case using Cons
by (auto intro!: exI[where x="λx. if x = 0 then e 0 else e' (x - 1)"] simp: o_def Pi_iff)
next
case (trans xs ys zs)
thus ?case by metis
next
case (swap y x l)
thus ?case
by (auto intro!: exI[where x="λi. if i = 0 then e 1 else if i = 1 then e 0 else e i"]
simp: o_def Pi_iff)
qed

lemma pdevs_val_perm:
assumes "xs <~~> ys"
assumes mem: "e ∈ UNIV → I"
obtains e' where "e' ∈ UNIV → I"
"pdevs_val e (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list ys)"
using assms
by (metis pdevs_val_perm_ex)

lemma set_distinct_permI: "set xs = set ys ⟹ distinct xs ⟹ distinct ys ⟹ xs <~~> ys"
by (metis eq_set_perm_remdups remdups_id_iff_distinct)

lemmas pdevs_val_permute = pdevs_val_perm[OF set_distinct_permI]

lemma partition_permI:
"filter p xs @ filter (Not o p) xs <~~> xs"
proof (induct xs)
case (Cons x xs)
have swap_app_Cons: "filter p xs @ x # [a←xs . ¬ p a] <~~> x # filter p xs @ [a←xs . ¬ p a]"
by (metis perm_sym perm_append_Cons)
also have "… <~~> x#xs"
using Cons by auto
finally (trans)
show ?case using Cons
by simp
qed simp

lemma pdevs_val_eqI:
assumes "⋀i. i ∈ pdevs_domain y ⟹ i ∈ pdevs_domain x ⟹
e i *⇩R pdevs_apply x i = f i *⇩R pdevs_apply y i"
assumes "⋀i. i ∈ pdevs_domain y ⟹ i ∉ pdevs_domain x ⟹ f i *⇩R pdevs_apply y i = 0"
assumes "⋀i. i ∈ pdevs_domain x ⟹ i ∉ pdevs_domain y ⟹ e i *⇩R pdevs_apply x i = 0"
shows "pdevs_val e x = pdevs_val f y"
using assms
by (force simp: pdevs_val_pdevs_domain
intro!:
sum.reindex_bij_witness_not_neutral[where
i=id and j = id and
S'="pdevs_domain x - pdevs_domain y" and
T'="pdevs_domain y - pdevs_domain x"])

definition
filter_pdevs_raw::"(nat ⇒ 'a ⇒ bool) ⇒ (nat ⇒ 'a::real_vector) ⇒ (nat ⇒ 'a)"
where "filter_pdevs_raw I X = (λi. if I i (X i) then X i else 0)"

lemma filter_pdevs_raw_nonzeros: "{i. filter_pdevs_raw s f i ≠ 0} = {i. f i ≠ 0} ∩ {x. s x (f x)}"
by (auto simp: filter_pdevs_raw_def)

lift_definition filter_pdevs::"(nat ⇒ 'a ⇒ bool) ⇒ 'a::real_vector pdevs ⇒ 'a pdevs"
is filter_pdevs_raw

lemma pdevs_apply_filter_pdevs[simp]:
"pdevs_apply (filter_pdevs I x) i = (if I i (pdevs_apply x i) then pdevs_apply x i else 0)"
by transfer (auto simp: filter_pdevs_raw_def)

lemma degree_filter_pdevs_le: "degree (filter_pdevs I x) ≤ degree x"
by (rule degree_leI) (simp split: if_split_asm)

lemma pdevs_val_filter_pdevs:
"pdevs_val e (filter_pdevs I x) =
(∑i ∈ {..<degree x} ∩ {i. I i (pdevs_apply x i)}. e i *⇩R pdevs_apply x i)"
by (auto simp: pdevs_val_sum if_distrib sum.inter_restrict degree_filter_pdevs_le degree_gt
intro!: sum.mono_neutral_cong_left split: if_split_asm)

lemma pdevs_val_filter_pdevs_dom:
"pdevs_val e (filter_pdevs I x) =
(∑i ∈ pdevs_domain x ∩ {i. I i (pdevs_apply x i)}. e i *⇩R pdevs_apply x i)"
by (auto
simp: pdevs_val_pdevs_domain if_distrib sum.inter_restrict degree_filter_pdevs_le degree_gt
intro!: sum.mono_neutral_cong_left split: if_split_asm)

lemma pdevs_val_filter_pdevs_eval:
"pdevs_val e (filter_pdevs p x) = pdevs_val (λi. if p i (pdevs_apply x i) then e i else 0) x"
by (auto split: if_split_asm intro!: pdevs_val_eqI)

definition "pdevs_applys X i = map (λx. pdevs_apply x i) X"
definition "pdevs_vals e X = map (pdevs_val e) X"
definition "aform_vals e X = map (aform_val e) X"
definition "filter_pdevs_list I X = map (filter_pdevs (λi _. I i (pdevs_applys X i))) X"

lemma pdevs_applys_filter_pdevs_list[simp]:
"pdevs_applys (filter_pdevs_list I X) i = (if I i (pdevs_applys X i) then pdevs_applys X i else
map (λ_. 0) X)"
by (auto simp: filter_pdevs_list_def o_def pdevs_applys_def)

definition "degrees X = Max (insert 0 (degree  set X))"

abbreviation "degree_aforms X ≡ degrees (map snd X)"

lemma degrees_leI:
assumes "⋀x. x ∈ set X ⟹ degree x ≤ K"
shows "degrees X ≤ K"
using assms
by (auto simp: degrees_def intro!: Max.boundedI)

lemma degrees_leD:
assumes "degrees X ≤ K"
shows "⋀x. x ∈ set X ⟹ degree x ≤ K"
using assms
by (auto simp: degrees_def intro!: Max.boundedI)

lemma degree_filter_pdevs_list_le: "degrees (filter_pdevs_list I x) ≤ degrees x"
by (rule degrees_leI) (auto simp: filter_pdevs_list_def intro!: degree_le dest!: degrees_leD)

definition "dense_list_of_pdevs x = map (λi. pdevs_apply x i) [0..<degree x]"

subsubsection ‹(reverse) ordered coefficients as list›

definition "list_of_pdevs x =
map (λi. (i, pdevs_apply x i)) (rev (sorted_list_of_set (pdevs_domain x)))"

lemma list_of_pdevs_zero_pdevs[simp]: "list_of_pdevs zero_pdevs = []"
by (auto simp: list_of_pdevs_def)

lemma sum_list_list_of_pdevs: "sum_list (map snd (list_of_pdevs x)) = sum_list (dense_list_of_pdevs x)"
by (auto intro!: sum.mono_neutral_cong_left
simp add: degree_gt sum_list_distinct_conv_sum_set dense_list_of_pdevs_def list_of_pdevs_def)

lemma sum_list_filter_dense_list_of_pdevs[symmetric]:
"sum_list (map snd (filter (p o snd) (list_of_pdevs x))) =
sum_list (filter p (dense_list_of_pdevs x))"
by (auto intro!: sum.mono_neutral_cong_left
simp add: degree_gt sum_list_distinct_conv_sum_set dense_list_of_pdevs_def list_of_pdevs_def
o_def filter_map)

lemma pdevs_of_list_dense_list_of_pdevs: "pdevs_of_list (dense_list_of_pdevs x) = x"
by (auto simp: pdevs_apply_pdevs_of_list dense_list_of_pdevs_def pdevs_eqI)

lemma pdevs_val_sum_list: "pdevs_val (λ_. c) X = c *⇩R sum_list (map snd (list_of_pdevs X))"
by (auto simp: pdevs_val_sum sum_list_list_of_pdevs pdevs_val_const_pdevs_of_list[symmetric]
pdevs_of_list_dense_list_of_pdevs)

lemma list_of_pdevs_all_nonzero: "list_all (λx. x ≠ 0) (map snd (list_of_pdevs xs))"
by (auto simp: list_of_pdevs_def list_all_iff)

lemma list_of_pdevs_nonzero: "x ∈ set (map snd (list_of_pdevs xs)) ⟹ x ≠ 0"
by (auto simp: list_of_pdevs_def)

lemma pdevs_of_list_scaleR_0[simp]:
fixes xs::"'a::real_vector list"
shows "pdevs_of_list (map ((*⇩R) 0) xs) = zero_pdevs"
by (auto simp: pdevs_apply_pdevs_of_list intro!: pdevs_eqI)

lemma degree_pdevs_of_list_scaleR:
"degree (pdevs_of_list (map ((*⇩R) c) xs)) = (if c ≠ 0 then degree (pdevs_of_list xs) else 0)"
by (auto simp: pdevs_apply_pdevs_of_list intro!: degree_cong)

lemma list_of_pdevs_eq:
"rev (list_of_pdevs X) = (filter ((≠) 0 o snd) (map (λi. (i, pdevs_apply X i)) [0..<degree X]))"
(is "_ = filter ?P (map ?f ?xs)")
using map_filter[of ?f ?P ?xs]
by (auto simp: list_of_pdevs_def o_def sorted_list_of_pdevs_domain_eq rev_map)

lemma sum_list_take_pdevs_val_eq:
"sum_list (take d xs) = pdevs_val (λi. if i < d then 1 else 0) (pdevs_of_list xs)"
proof -
have "sum_list (take d xs) = 1 *⇩R sum_list (take d xs)" by simp
also note pdevs_val_const_pdevs_of_list[symmetric]
also have "pdevs_val (λ_. 1) (pdevs_of_list (take d xs)) =
pdevs_val (λi. if i < d then 1 else 0) (pdevs_of_list xs)"
by (auto simp: pdevs_apply_pdevs_of_list split: if_split_asm intro!: pdevs_val_eqI)
finally show ?thesis .
qed

lemma zero_in_range_pdevs_apply[intro, simp]:
fixes X::"'a::real_vector pdevs" shows "0 ∈ range (pdevs_apply X)"
by (metis degree_gt less_irrefl rangeI)

lemma dense_list_in_range: "x ∈ set (dense_list_of_pdevs X) ⟹ x ∈ range (pdevs_apply X)"
by (auto simp: dense_list_of_pdevs_def)

lemma not_in_dense_list_zeroD:
assumes "pdevs_apply X i ∉ set (dense_list_of_pdevs X)"
shows "pdevs_apply X i = 0"
proof (rule ccontr)
assume "pdevs_apply X i ≠ 0"
hence "i < degree X"
by (rule degree_gt)
thus False using assms
by (auto simp: dense_list_of_pdevs_def)
qed

lemma list_all_list_of_pdevsI:
assumes "⋀i. i ∈ pdevs_domain X ⟹ P (pdevs_apply X i)"
shows "list_all (λx. P x) (map snd (list_of_pdevs X))"
using assms by (auto simp: list_all_iff list_of_pdevs_def)

lemma pdevs_of_list_map_scaleR:
"pdevs_of_list (map (scaleR r) xs) = scaleR_pdevs r (pdevs_of_list xs)"
by (auto intro!: pdevs_eqI simp: pdevs_apply_pdevs_of_list)

lemma
map_permI:
assumes "xs <~~> ys"
shows "map f xs <~~> map f ys"
using assms by induct auto

lemma rev_perm: "rev xs <~~> ys ⟷ xs <~~> ys"
by (metis perm.trans perm_rev rev_rev_ident)

lemma list_of_pdevs_perm_filter_nonzero:
"map snd (list_of_pdevs X) <~~> (filter ((≠) 0) (dense_list_of_pdevs X))"
proof -
have zip_map:
"zip [0..<degree X] (dense_list_of_pdevs X) = map (λi. (i, pdevs_apply X i)) [0..<degree X]"
by (auto simp: dense_list_of_pdevs_def intro!: nth_equalityI)
have "rev (list_of_pdevs X) <~~>
filter ((≠) 0 o snd) (zip [0..<degree X] (dense_list_of_pdevs X))"
by (auto simp: list_of_pdevs_eq o_def zip_map)
from map_permI[OF this, of snd]
have "map snd (list_of_pdevs X) <~~>
map snd (filter ((≠) 0 ∘ snd) (zip [0..<degree X] (dense_list_of_pdevs X)))"
also have "map snd (filter ((≠) 0 ∘ snd) (zip [0..<degree X] (dense_list_of_pdevs X))) =
filter ((≠) 0) (dense_list_of_pdevs X)"
using map_filter[of snd "(≠) 0" "(zip [0..<degree X] (dense_list_of_pdevs X))"]
finally
show ?thesis .
qed

lemma pdevs_val_filter:
assumes mem: "e ∈ UNIV → I"
assumes "0 ∈ I"
obtains e' where
"pdevs_val e (pdevs_of_list (filter p xs)) = pdevs_val e' (pdevs_of_list xs)"
"e' ∈ UNIV → I"
unfolding pdevs_val_filter_pdevs_eval
proof -
have "(λ_::nat. 0) ∈ UNIV → I" using assms by simp
have "pdevs_val e (pdevs_of_list (filter p xs)) =
pdevs_val e (pdevs_of_list (filter p xs)) +
pdevs_val (λ_. 0) (pdevs_of_list (filter (Not o p) xs))"
also
from pdevs_val_pdevs_of_list_append[OF ‹e ∈ _› ‹(λ_. 0) ∈ _›]
obtain e' where "e' ∈ UNIV → I"
"… = pdevs_val e' (pdevs_of_list (filter p xs @ filter (Not o p) xs))"
by metis
note this(2)
also
from pdevs_val_perm[OF partition_permI ‹e' ∈ _›]
obtain e'' where "… = pdevs_val e'' (pdevs_of_list xs)" "e'' ∈ UNIV → I" by metis
note this(1)
finally show ?thesis using ‹e'' ∈ _› ..
qed

lemma
pdevs_val_of_list_of_pdevs:
assumes "e ∈ UNIV → I"
assumes "0 ∈ I"
obtains e' where
"pdevs_val e (pdevs_of_list (map snd (list_of_pdevs X))) = pdevs_val e' X"
"e' ∈ UNIV → I"
proof -
obtain e' where "e' ∈ UNIV → I"
and "pdevs_val e (pdevs_of_list (map snd (list_of_pdevs X))) =
pdevs_val e' (pdevs_of_list (filter ((≠) 0) (dense_list_of_pdevs X)))"
by (rule pdevs_val_perm[OF list_of_pdevs_perm_filter_nonzero assms(1)])
note this(2)
also from pdevs_val_filter[OF ‹e' ∈ _› ‹0 ∈ I›, of "(≠) 0" "dense_list_of_pdevs X"]
obtain e'' where "e'' ∈ UNIV → I"
and "… = pdevs_val e'' (pdevs_of_list (dense_list_of_pdevs X))"
by metis
note this(2)
also have "… = pdevs_val e'' X" by (simp add: pdevs_of_list_dense_list_of_pdevs)
finally show ?thesis using ‹e'' ∈ UNIV → I› ..
qed

lemma
pdevs_val_of_list_of_pdevs2:
assumes "e ∈ UNIV → I"
obtains e' where
"pdevs_val e X = pdevs_val e' (pdevs_of_list (map snd (list_of_pdevs X)))"
"e' ∈ UNIV → I"
proof -
from list_of_pdevs_perm_filter_nonzero[of X]
have perm: "(filter ((≠) 0) (dense_list_of_pdevs X)) <~~> map snd (list_of_pdevs X)"
have "pdevs_val e X = pdevs_val e (pdevs_of_list (dense_list_of_pdevs X))"
also from pdevs_val_partition[OF ‹e ∈ _›, of "dense_list_of_pdevs X" "(≠) 0"]
obtain f g where "f ∈ UNIV → I" "g ∈ UNIV → I"
"… = pdevs_val f (pdevs_of_list (filter ((≠) 0) (dense_list_of_pdevs X))) +
pdevs_val g (pdevs_of_list (filter (Not ∘ (≠) 0) (dense_list_of_pdevs X)))"
(is "_ = ?f + ?g")
by metis
note this(3)
also
have "pdevs_of_list [x←dense_list_of_pdevs X . x = 0] = zero_pdevs"
by (auto intro!: pdevs_eqI simp: pdevs_apply_pdevs_of_list dest!: nth_mem)
hence "?g = 0" by (auto simp: o_def )
also
obtain e' where "e' ∈ UNIV → I"
and "?f = pdevs_val e' (pdevs_of_list (map snd (list_of_pdevs X)))"
by (rule pdevs_val_perm[OF perm ‹f ∈ _›])
note this(2)
finally show ?thesis using ‹e' ∈ UNIV → I› by (auto intro!: that)
qed

lemma dense_list_of_pdevs_scaleR:
"r ≠ 0 ⟹ map ((*⇩R) r) (dense_list_of_pdevs x) = dense_list_of_pdevs (scaleR_pdevs r x)"
by (auto simp: dense_list_of_pdevs_def)

lemma degree_pdevs_of_list_eq:
"(⋀x. x ∈ set xs ⟹ x ≠ 0) ⟹ degree (pdevs_of_list xs) = length xs"
by (cases xs) (auto simp add: pdevs_apply_pdevs_of_list nth_Cons
intro!: degree_eqI
split: nat.split)

lemma dense_list_of_pdevs_pdevs_of_list:
"(⋀x. x ∈ set xs ⟹ x ≠ 0) ⟹ dense_list_of_pdevs (pdevs_of_list xs) = xs"
by (auto simp: dense_list_of_pdevs_def degree_pdevs_of_list_eq pdevs_apply_pdevs_of_list
intro!: nth_equalityI)

lemma pdevs_of_list_sum:
assumes "distinct xs"
assumes "e ∈ UNIV → I"
obtains f where "f ∈ UNIV → I" "pdevs_val e (pdevs_of_list xs) = (∑P∈set xs. f P *⇩R P)"
proof -
define f where "f X = e (the (map_of (zip xs [0..<length xs]) X))" for X
from assms have "f ∈ UNIV → I"
by (auto simp: f_def)
moreover
have "pdevs_val e (pdevs_of_list xs) = (∑P∈set xs. f P *⇩R P)"
by (auto simp add: pdevs_val_zip f_def assms sum_list_distinct_conv_sum_set[symmetric]
in_set_zip map_of_zip_upto2_length_eq_nth
intro!: sum_list_nth_eqI)
ultimately show ?thesis ..
qed

lemma pdevs_domain_eq_pdevs_of_list:
assumes nz: "⋀x. x ∈ set (xs) ⟹ x ≠ 0"
shows "pdevs_domain (pdevs_of_list xs) = {0..<length xs}"
using nz
by (auto simp: pdevs_apply_pdevs_of_list split: if_split_asm)

lemma length_list_of_pdevs_pdevs_of_list:
assumes nz: "⋀x. x ∈ set xs ⟹ x ≠ 0"
shows "length (list_of_pdevs (pdevs_of_list xs)) = length xs"
using nz by (auto simp: list_of_pdevs_def pdevs_domain_eq_pdevs_of_list)

lemma nth_list_of_pdevs_pdevs_of_list:
assumes nz: "⋀x. x ∈ set xs ⟹ x ≠ 0"
assumes l: "n < length xs"
shows "list_of_pdevs (pdevs_of_list xs) ! n  = ((length xs - Suc n), xs ! (length xs - Suc n))"
using nz l
by (auto simp: list_of_pdevs_def pdevs_domain_eq_pdevs_of_list rev_nth pdevs_apply_pdevs_of_list)

lemma list_of_pdevs_pdevs_of_list_eq:
"(⋀x. x ∈ set xs ⟹ x ≠ 0) ⟹
list_of_pdevs (pdevs_of_list xs) = zip (rev [0..<length xs]) (rev xs)"
by (auto simp: nth_list_of_pdevs_pdevs_of_list length_list_of_pdevs_pdevs_of_list rev_nth
intro!: nth_equalityI)

lemma sum_list_filter_list_of_pdevs_of_list:
assumes "⋀x. x ∈ set xs ⟹ x ≠ 0"
shows "sum_list (filter p (map snd (list_of_pdevs (pdevs_of_list xs)))) = sum_list (filter p xs)"
using assms
by (auto simp: list_of_pdevs_pdevs_of_list_eq rev_filter[symmetric])

lemma
sum_list_partition:
shows "sum_list (filter p xs) + sum_list (filter (Not o p) xs) = sum_list xs"
by (induct xs) (auto simp: ac_simps)

subsection ‹2d zonotopes›

definition "prod_of_pdevs x y = binop_pdevs Pair x y"

lemma apply_pdevs_prod_of_pdevs[simp]:
"pdevs_apply (prod_of_pdevs x y) i = (pdevs_apply x i, pdevs_apply y i)"
unfolding prod_of_pdevs_def

lemma pdevs_domain_prod_of_pdevs[simp]:
"pdevs_domain (prod_of_pdevs x y) = pdevs_domain x ∪ pdevs_domain y"
by (auto simp: zero_prod_def)

lemma pdevs_val_prod_of_pdevs[simp]:
"pdevs_val e (prod_of_pdevs x y) = (pdevs_val e x, pdevs_val e y)"
proof -
have "pdevs_val e x = (∑i∈pdevs_domain x ∪ pdevs_domain y. e i *⇩R pdevs_apply x i)"
(is "_ = ?x")
unfolding pdevs_val_pdevs_domain
by (rule sum.mono_neutral_cong_left) auto
moreover have "pdevs_val e y = (∑i∈pdevs_domain x ∪ pdevs_domain y. e i *⇩R pdevs_apply y i)"
(is "_ = ?y")
unfolding pdevs_val_pdevs_domain
by (rule sum.mono_neutral_cong_left) auto
ultimately have "(pdevs_val e x, pdevs_val e y) = (?x, ?y)"
by auto
also have "… = pdevs_val e (prod_of_pdevs x y)"
finally show ?thesis by simp
qed

definition prod_of_aforms (infixr "×⇩a" 80)
where "prod_of_aforms x y = ((fst x, fst y), prod_of_pdevs (snd x) (snd y))"

subsection ‹Intervals›

definition One_pdevs_raw::"nat ⇒ 'a::executable_euclidean_space"
where "One_pdevs_raw i = (if i < length (Basis_list::'a list) then Basis_list ! i else 0)"

lemma zeros_One_pdevs_raw:
"One_pdevs_raw - {0::'a::executable_euclidean_space} = {length (Basis_list::'a list)..}"
by (auto simp: One_pdevs_raw_def nonzero_Basis split: if_split_asm dest!: nth_mem)

lemma nonzeros_One_pdevs_raw:
"{i. One_pdevs_raw i ≠ (0::'a::executable_euclidean_space)} = - {length (Basis_list::'a list)..}"
using zeros_One_pdevs_raw
by blast

lift_definition One_pdevs::"'a::executable_euclidean_space pdevs" is One_pdevs_raw
by (auto simp: nonzeros_One_pdevs_raw)

lemma pdevs_apply_One_pdevs[simp]: "pdevs_apply One_pdevs i =
(if i < length (Basis_list::'a::executable_euclidean_space list) then Basis_list ! i else 0::'a)"

lemma Max_Collect_less_nat: "Max {i::nat. i < k} = (if k = 0 then Max {} else k - 1)"
by (auto intro!: Max_eqI)

lemma degree_One_pdevs[simp]: "degree (One_pdevs::'a pdevs) =
length (Basis_list::'a::executable_euclidean_space list)"
by (auto simp: degree_eq_Suc_max Basis_list_nth_nonzero Max_Collect_less_nat
intro!: Max_eqI DIM_positive)

definition inner_scaleR_pdevs::"'a::euclidean_space ⇒ 'a pdevs ⇒ 'a pdevs"
where "inner_scaleR_pdevs b x = unop_pdevs (λx. (b ∙ x) *⇩R x) x"

lemma pdevs_apply_inner_scaleR_pdevs[simp]:
"pdevs_apply (inner_scaleR_pdevs a x) i = (a ∙ (pdevs_apply x i)) *⇩R (pdevs_apply x i)"

lemma degree_inner_scaleR_pdevs_le:
"degree (inner_scaleR_pdevs (l::'a::executable_euclidean_space) One_pdevs) ≤
degree (One_pdevs::'a pdevs)"
by (rule degree_leI) (auto simp: inner_scaleR_pdevs_def One_pdevs_raw_def)

definition "pdevs_of_ivl l u = scaleR_pdevs (1/2) (inner_scaleR_pdevs (u - l) One_pdevs)"

lemma degree_pdevs_of_ivl_le:
"degree (pdevs_of_ivl l u::'a::executable_euclidean_space pdevs) ≤ DIM('a)"
using degree_inner_scaleR_pdevs_le

lemma pdevs_apply_pdevs_of_ivl:
defines "B ≡ Basis_list::'a::executable_euclidean_space list"
shows "pdevs_apply (pdevs_of_ivl l u) i = (if i < length B then ((u - l)∙(B!i)/2)*⇩R(B!i) else 0)"
by (auto simp: pdevs_of_ivl_def B_def)

lemma deg_length_less_imp[simp]:
"k < degree (pdevs_of_ivl l u::'a::executable_euclidean_space pdevs) ⟹
k < length (Basis_list::'a list)"
by (metis (no_types, hide_lams) degree_One_pdevs degree_inner_scaleR_pdevs_le degree_scaleR_pdevs
dual_order.strict_trans length_Basis_list_pos nat_neq_iff not_le pdevs_of_ivl_def)

lemma tdev_pdevs_of_ivl: "tdev (pdevs_of_ivl l u) = ¦u - l¦ /⇩R 2"
proof -
have "tdev (pdevs_of_ivl l u) =
(∑i <degree (pdevs_of_ivl l u). ¦pdevs_apply (pdevs_of_ivl l u) i¦)"
by (auto simp: tdev_def)
also have "… = (∑i = 0..<length (Basis_list::'a list). ¦pdevs_apply (pdevs_of_ivl l u) i¦)"
using degree_pdevs_of_ivl_le[of l u]
by (intro sum.mono_neutral_cong_left) auto
also have "… = (∑i = 0..<length (Basis_list::'a list).
¦((u - l) ∙ Basis_list ! i / 2) *⇩R Basis_list ! i¦)"
by (auto simp: pdevs_apply_pdevs_of_ivl)
also have "… = (∑b ← Basis_list. ¦((u - l) ∙ b / 2) *⇩R b¦)"
by (auto simp: sum_list_sum_nth)
also have "… = (∑b∈Basis. ¦((u - l) ∙ b / 2) *⇩R b¦)"
by (auto simp: sum_list_distinct_conv_sum_set)
also have "… = ¦u - l¦ /⇩R 2"
by (subst euclidean_representation[symmetric, of "¦u - l¦ /⇩R 2"])
finally show ?thesis .
qed

definition "aform_of_ivl l u = ((l + u)/⇩R2, pdevs_of_ivl l u)"

definition "aform_of_point x = aform_of_ivl x x"

lemma Elem_affine_of_ivl_le:
assumes "e ∈ UNIV → {-1 .. 1}"
assumes "l ≤ u"
shows "l ≤ aform_val e (aform_of_ivl l u)"
proof -
have "l =  (1 / 2) *⇩R l + (1 / 2) *⇩R l"
also have "… = (l + u)/⇩R2 - tdev (pdevs_of_ivl l u)"
by (auto simp: assms tdev_pdevs_of_ivl algebra_simps)
also have "… ≤ aform_val e (aform_of_ivl l u)"
using abs_pdevs_val_le_tdev[OF assms(1), of "pdevs_of_ivl l u"]
by (auto simp: aform_val_def aform_of_ivl_def minus_le_iff dest!: abs_le_D2)
finally show ?thesis .
qed

lemma Elem_affine_of_ivl_ge:
assumes "e ∈ UNIV → {-1 .. 1}"
assumes "l ≤ u"
shows "aform_val e (aform_of_ivl l u) ≤ u"
proof -
have "aform_val e (aform_of_ivl l u) ≤  (l + u)/⇩R2 + tdev (pdevs_of_ivl l u)"
using abs_pdevs_val_le_tdev[OF assms(1), of "pdevs_of_ivl l u"]
by (auto simp: aform_val_def aform_of_ivl_def minus_le_iff dest!: abs_le_D1)
also have "… = (1 / 2) *⇩R u + (1 / 2) *⇩R u"
by (auto simp: assms tdev_pdevs_of_ivl algebra_simps)
also have "… = u"
finally show ?thesis .
qed

lemma
map_of_zip_upto_length_eq_nth:
assumes "i < length B"
assumes "d = length B"
shows "(map_of (zip [0..<d] B) i) = Some (B ! i)"
proof -
have "length [0..<length B] = length B"
by simp
from map_of_zip_is_Some[OF this, of i] assms
have "map_of (zip [0..<length B] B) i = Some (B ! i)"
by (auto simp: in_set_zip)
thus ?thesis by (simp add: assms)
qed

lemma in_ivl_affine_of_ivlE:
assumes "k ∈ {l .. u}"
obtains e where "e ∈ UNIV → {-1 .. 1}" "k = aform_val e (aform_of_ivl l u)"
proof atomize_elim
define e where [abs_def]: "e i = (let b = if i <length (Basis_list::'a list) then
(the (map_of (zip [0..<length (Basis_list::'a list)] (Basis_list::'a list)) i)) else 0 in
((k - (l + u) /⇩R 2) ∙ b) / (((u - l) /⇩R 2) ∙ b))" for i
let ?B = "Basis_list::'a list"

have "k = (1 / 2) *⇩R (l + u) +
(∑b ∈ Basis. (if (u - l) ∙ b = 0 then 0 else ((k - (1 / 2) *⇩R (l + u)) ∙ b)) *⇩R b)"
(is "_ = _ + ?dots")
using assms
by (force simp add: algebra_simps eucl_le[where 'a='a] intro!: euclidean_eqI[where 'a='a])
also have
"?dots = (∑b ∈ Basis. (if (u - l) ∙ b = 0 then 0 else ((k - (1 / 2) *⇩R (l + u)) ∙ b) *⇩R b))"
by (auto intro!: sum.cong)
also have "… = (∑b ← ?B. (if (u - l) ∙ b = 0 then 0 else ((k - (1 / 2) *⇩R (l + u)) ∙ b) *⇩R b))"
by (auto simp: sum_list_distinct_conv_sum_set)
also have "… =
(∑i = 0..<length ?B.
(if (u - l) ∙ ?B ! i = 0 then 0 else ((k - (1 / 2) *⇩R (l + u)) ∙ ?B ! i) *⇩R ?B ! i))"
by (auto simp: sum_list_sum_nth)
also have "… =
(∑i = 0..<degree (inner_scaleR_pdevs (u - l) One_pdevs).
(if (u - l) ∙ Basis_list ! i = 0 then 0
else ((k - (1 / 2) *⇩R (l + u)) ∙ Basis_list ! i) *⇩R Basis_list ! i))"
using degree_inner_scaleR_pdevs_le[of "u - l"]
by (intro sum.mono_neutral_cong_right) (auto dest!: degree)
also have "(1 / 2) *⇩R (l + u) +
(∑i = 0..<degree (inner_scaleR_pdevs (u - l) One_pdevs).
(if (u - l) ∙ Basis_list ! i = 0 then 0
else ((k - (1 / 2) *⇩R (l + u)) ∙ Basis_list ! i) *⇩R Basis_list ! i)) =
aform_val e (aform_of_ivl l u)"
using degree_inner_scaleR_pdevs_le[of "u - l"]
by (auto simp: aform_val_def aform_of_ivl_def pdevs_of_ivl_def map_of_zip_upto_length_eq_nth
e_def Let_def pdevs_val_sum
intro!: sum.cong)
finally have "k = aform_val e (aform_of_ivl l u)" .

moreover
{
fix k l u::real assume *: "l ≤ k" "k ≤ u"
let ?m = "l / 2 + u / 2"
have "¦k - ?m¦ ≤ ¦if k ≤ ?m then ?m - l else u - ?m¦"
using * by auto
also have "… ≤ ¦u / 2 - l / 2¦"
by (auto simp: abs_real_def)
finally have "¦k - (l / 2 + u / 2)¦ ≤ ¦u / 2 - l/2¦" .
} note midpoint_abs = this
have "e ∈ UNIV → {- 1..1}"
using assms
unfolding e_def Let_def
by (intro Pi_I divide_atLeastAtMost_1_absI)
(auto simp: map_of_zip_upto_length_eq_nth eucl_le[where 'a='a]
divide_le_eq_1 not_less inner_Basis algebra_simps intro!: midpoint_abs
dest!: nth_mem)
ultimately show "∃e. e ∈ UNIV → {- 1..1} ∧ k = aform_val e (aform_of_ivl l u)"
by blast
qed

lemma Inf_aform_aform_of_ivl:
assumes "l ≤ u"
shows "Inf_aform (aform_of_ivl l u) = l"
using assms
by (auto simp: Inf_aform_def aform_of_ivl_def tdev_pdevs_of_ivl abs_diff_eq1 algebra_simps)

lemma Sup_aform_aform_of_ivl:
assumes "l ≤ u"
shows "Sup_aform (aform_of_ivl l u) = u"
using assms
by (auto simp: Sup_aform_def aform_of_ivl_def tdev_pdevs_of_ivl abs_diff_eq1 algebra_simps)

lemma Affine_aform_of_ivl:
"a ≤ b ⟹ Affine (aform_of_ivl a b) = {a .. b}"
by (force simp: Affine_def valuate_def intro!: Elem_affine_of_ivl_ge Elem_affine_of_ivl_le
elim!: in_ivl_affine_of_ivlE)

end


# Theory Floatarith_Expression

section ‹Operations on Expressions›
theory Floatarith_Expression
imports
"HOL-Decision_Procs.Approximation"
Affine_Arithmetic_Auxiliarities
Executable_Euclidean_Space
begin

text ‹Much of this could move to the distribution...›

subsection ‹Approximating Expression*s*›

unbundle floatarith_notation

text ‹\label{sec:affineexpr}›

primrec interpret_floatariths :: "floatarith list ⇒ real list ⇒ real list"
where
"interpret_floatariths [] vs = []"
| "interpret_floatariths (a#bs) vs = interpret_floatarith a vs#interpret_floatariths bs vs"

lemma length_interpret_floatariths[simp]: "length (interpret_floatariths fas xs) = length fas"
by (induction fas) auto

lemma interpret_floatariths_nth[simp]:
"interpret_floatariths fas xs ! n = interpret_floatarith (fas ! n) xs"
if "n < length fas"
using that
by (induction fas arbitrary: n) (auto simp: nth_Cons split: nat.splits)

abbreviation "einterpret ≡ λfas vs. eucl_of_list (interpret_floatariths fas vs)"

subsection ‹Syntax›

syntax interpret_floatarith::"floatarith ⇒ real list ⇒ real"

instantiation floatarith :: "{plus, minus, uminus, times, inverse, zero, one}"
begin

definition "- f = Minus f"
lemma interpret_floatarith_uminus[simp]:
"interpret_floatarith (- f) xs = - interpret_floatarith f xs"
by (auto simp: uminus_floatarith_def)

definition "f + g = Add f g"
lemma interpret_floatarith_plus[simp]:
"interpret_floatarith (f + g) xs = interpret_floatarith f xs + interpret_floatarith g xs"
by (auto simp: plus_floatarith_def)

definition "f - g = Add f (Minus g)"
lemma interpret_floatarith_minus[simp]:
"interpret_floatarith (f - g) xs = interpret_floatarith f xs - interpret_floatarith g xs"
by (auto simp: minus_floatarith_def)

definition "inverse f = Inverse f"
lemma interpret_floatarith_inverse[simp]:
"interpret_floatarith (inverse f) xs = inverse (interpret_floatarith f xs)"
by (auto simp: inverse_floatarith_def)

definition "f * g = Mult f g"
lemma interpret_floatarith_times[simp]:
"interpret_floatarith (f * g) xs = interpret_floatarith f xs * interpret_floatarith g xs"
by (auto simp: times_floatarith_def)

definition "f div g = f * Inverse g"
lemma interpret_floatarith_divide[simp]:
"interpret_floatarith (f div g) xs = interpret_floatarith f xs / interpret_floatarith g xs"
by (auto simp: divide_floatarith_def inverse_eq_divide)

definition "1 = Num 1"
lemma interpret_floatarith_one[simp]:
"interpret_floatarith 1 xs = 1"
by (auto simp: one_floatarith_def)

definition "0 = Num 0"
lemma interpret_floatarith_zero[simp]:
"interpret_floatarith 0 xs = 0"
by (auto simp: zero_floatarith_def)

instance proof qed
end

subsection ‹Derived symbols›

definition "R⇩e r = (case quotient_of r of (n, d) ⇒ Num (of_int n) / Num (of_int d))"
declare [[coercion R⇩e ]]

lemma interpret_R⇩e[simp]: "interpret_floatarith (R⇩e x) xs = real_of_rat x"
by (auto simp: R⇩e_def of_rat_divide dest!: quotient_of_div split: prod.splits)

definition "Sin x = Cos ((Pi * (Num (Float 1 (-1)))) - x)"

lemma interpret_floatarith_Sin[simp]:
"interpret_floatarith (Sin x) vs = sin (interpret_floatarith x vs)"
by (auto simp: Sin_def approximation_preproc_floatarith(11))

definition "Half x = Mult (Num (Float 1 (-1))) x"
lemma interpret_Half[simp]: "interpret_floatarith (Half x) xs = interpret_floatarith x xs / 2"
by (auto simp: Half_def)

definition "Tan x = (Sin x) / (Cos x)"

lemma interpret_floatarith_Tan[simp]:
"interpret_floatarith (Tan x) vs = tan (interpret_floatarith x vs)"
by (auto simp: Tan_def approximation_preproc_floatarith(12) inverse_eq_divide)

primrec Sum⇩e where
"Sum⇩e f [] = 0"
| "Sum⇩e f (x#xs) = f x + Sum⇩e f xs"

lemma interpret_floatarith_Sum⇩e[simp]:
"interpret_floatarith (Sum⇩e f x) vs = (∑i←x. interpret_floatarith (f i) vs)"
by (induction x) auto

definition Norm where "Norm is = Sqrt (Sum⇩e (λi. i * i) is)"

lemma interpret_floatarith_norm[simp]:
assumes [simp]: "length x = DIM('a)"
shows "interpret_floatarith (Norm x) vs = norm (einterpret x vs::'a::executable_euclidean_space)"
apply (auto simp: Norm_def norm_eq_sqrt_inner)
apply (subst euclidean_inner[where 'a='a])
apply (auto simp: power2_eq_square[symmetric] )
apply (subst sum_list_Basis_list[symmetric])
apply (rule sum_list_nth_eqI)
by (auto simp: in_set_zip eucl_of_list_inner)

notation floatarith.Power (infixr "^⇩e" 80)

subsection ‹Constant Folding›

fun dest_Num_fa where
"dest_Num_fa (floatarith.Num x) = Some x"
| "dest_Num_fa _ = None"

fun_cases dest_Num_fa_None: "dest_Num_fa fa = None"
and dest_Num_fa_Some: "dest_Num_fa fa = Some x"

fun fold_const_fa where
(let (ffa1, ffa2) = (fold_const_fa fa1, fold_const_fa fa2)
in case (dest_Num_fa ffa1, dest_Num_fa (ffa2)) of
(Some a, Some b) ⇒ Num (a + b)
| (Some a, None) ⇒ (if a = 0 then ffa2 else Add (Num a) ffa2)
| (None, Some a) ⇒ (if a = 0 then ffa1 else Add ffa1 (Num a))
| (None, None) ⇒ Add ffa1 ffa2)"
| "fold_const_fa (Minus a) =
(case (fold_const_fa a) of
(Num x) ⇒ Num (-x)
| x ⇒ Minus x)"
| "fold_const_fa (Mult fa1 fa2) =
(let (ffa1, ffa2) = (fold_const_fa fa1, fold_const_fa fa2)
in case (dest_Num_fa ffa1, dest_Num_fa (ffa2)) of
(Some a, Some b) ⇒ Num (a * b)
| (Some a, None) ⇒ (if a = 0 then Num 0 else if a = 1 then ffa2 else Mult (Num a) ffa2)
| (None, Some a) ⇒ (if a = 0 then Num 0 else if a = 1 then ffa1 else Mult ffa1 (Num a))
| (None, None) ⇒ Mult ffa1 ffa2)"
| "fold_const_fa (Inverse a) = Inverse (fold_const_fa a)"
| "fold_const_fa (Abs a) =
(case (fold_const_fa a) of
(Num x) ⇒ Num (abs x)
| x ⇒ Abs x)"
| "fold_const_fa (Max a b) =
(case (fold_const_fa a, fold_const_fa b) of
(Num x, Num y) ⇒ Num (max x y)
| (x, y) ⇒ Max x y)"
| "fold_const_fa (Min a b) =
(case (fold_const_fa a, fold_const_fa b) of
(Num x, Num y) ⇒ Num (min x y)
| (x, y) ⇒ Min x y)"
| "fold_const_fa (Floor a) =
(case (fold_const_fa a) of
(Num x) ⇒ Num (floor_fl x)
| x ⇒ Floor x)"
| "fold_const_fa (Power a b) =
(case (fold_const_fa a) of
(Num x) ⇒ Num (x ^ b)
| x ⇒ Power x b)"
| "fold_const_fa (Cos a) = Cos (fold_const_fa a)"
| "fold_const_fa (Arctan a) = Arctan (fold_const_fa a)"
| "fold_const_fa (Sqrt a) = Sqrt (fold_const_fa a)"
| "fold_const_fa (Exp a) = Exp (fold_const_fa a)"
| "fold_const_fa (Ln a) = Ln (fold_const_fa a)"
| "fold_const_fa (Powr a b) = Powr (fold_const_fa a) (fold_const_fa b)"
| "fold_const_fa Pi = Pi"
| "fold_const_fa (Var v) = Var v"
| "fold_const_fa (Num x) = Num x"

fun_cases fold_const_fa_Num: "fold_const_fa fa = Num y"
and fold_const_fa_Minus: "fold_const_fa fa = Minus y"

lemma fold_const_fa[simp]: "interpret_floatarith (fold_const_fa fa) xs = interpret_floatarith fa xs"
by (induction fa) (auto split!: prod.splits floatarith.splits option.splits
elim!: dest_Num_fa_None dest_Num_fa_Some
simp: max_def min_def floor_fl_def)

subsection ‹Free Variables›

primrec max_Var_floatarith where― ‹TODO: include bound in predicate›
"max_Var_floatarith (Add a b) = max (max_Var_floatarith a) (max_Var_floatarith b)"
| "max_Var_floatarith (Mult a b) = max (max_Var_floatarith a) (max_Var_floatarith b)"
| "max_Var_floatarith (Inverse a) = max_Var_floatarith a"
| "max_Var_floatarith (Minus a) = max_Var_floatarith a"
| "max_Var_floatarith (Num a) = 0"
| "max_Var_floatarith (Var i) = Suc i"
| "max_Var_floatarith (Cos a) = max_Var_floatarith a"
| "max_Var_floatarith (floatarith.Arctan a) = max_Var_floatarith a"
| "max_Var_floatarith (Abs a) = max_Var_floatarith a"
| "max_Var_floatarith (floatarith.Max a b) = max (max_Var_floatarith a) (max_Var_floatarith b)"
| "max_Var_floatarith (floatarith.Min a b) = max (max_Var_floatarith a) (max_Var_floatarith b)"
| "max_Var_floatarith (floatarith.Pi) = 0"
| "max_Var_floatarith (Sqrt a) = max_Var_floatarith a"
| "max_Var_floatarith (Exp a) = max_Var_floatarith a"
| "max_Var_floatarith (Powr a b) = max (max_Var_floatarith a) (`