Theory Boustrophedon_Transform
section ‹The Boustrophedon transform›
theory Boustrophedon_Transform
imports "HOL-Computational_Algebra.Computational_Algebra" Alternating_Permutations
begin
text ‹
The Boustrophedon transform maps one sequence of numbers to another sequence of numbers --
or, equivalently, one exponential generating function to another exponential generating function.
It was first described in its full generality by Millar et al.~\<^cite>‹millar›.
Its name derives from the Ancient Greek \greekbous\ (``ox''), \greekstrofe\ (``turn''), and
\greekdon\ (``in the manner of'') because the number triangle from which it is obtained can
be visualised as being traversed left-to-right, then right-to-left, etc.\ the same way an ox
plows a field.
›
subsection ‹The Seidel triangle›
no_syntax
"_Sum_any" :: "pttrn ⇒ 'a ⇒ 'a::comm_monoid_add" ("(3∑_. _)" [0, 10] 10)
syntax
"_Sum_any" :: "pttrn ⇒ 'a ⇒ 'a::comm_monoid_add" ("(3∑⇩?_. _)" [0, 10] 10)
text ‹
We define the triangle via its simplest recurrence. Let $T_{n,k}$ denote the $k$-th entry
of the $n$-th row. The first entry of the $n$-th row is always $a(n)$, where $a$ is the input
sequence. The $k+1$-th entry of a row is the sum of the previous entry in the same row and
the $k$-th last entry of the previous row.
That is: $T_{n, 0} = a(n)$ and $T_{n+1,k+1} = T_{n+1,k} + T_{n, n-k}$.
In other words: one produces a new row of the triangle by starting with $a(n)$ and then
adding the entries of the previous row, in right-to-left order, adding each intermediate
sum to the new row.
›
fun seidel_triangle :: "(nat ⇒ 'a :: monoid_add) ⇒ nat ⇒ nat ⇒ 'a" where
"seidel_triangle a n 0 = a n"
| "seidel_triangle a 0 (Suc k) = 0"
| "seidel_triangle a (Suc n) (Suc k) =
(if k > n then 0 else seidel_triangle a (Suc n) k + seidel_triangle a n (n - k))"
lemmas seidel_triangle_rec [simp del] = seidel_triangle.simps(3)
lemma seidel_triangle_greater_eq_0 [simp]: "k > n ⟹ seidel_triangle a n k = 0"
by (cases n; cases k) (auto simp: seidel_triangle_rec)
text ‹
There is also the following recurrence where the right-hand side contains only the entries
of the previous row. Namely: The entry $T_{n,k}$ is equal to the sum of $a_n$ and the last
$k$ entries of the previous row.
›
lemma seidel_triangle_conv_rowsum:
assumes "k ≤ n"
shows "seidel_triangle a n k = a n + (∑j<k. seidel_triangle a (n - 1) (n - Suc j))"
using assms
proof (induction k)
case (Suc k)
then obtain n' where [simp]: "n = Suc n'"
by (cases n) auto
show ?case
using Suc.IH Suc.prems by (simp add: seidel_triangle_rec add_ac)
qed auto
text ‹
The following function is the function $\pi(n,k,i)$ from the paper by Millar et al.
They define it via the number of paths from one node to another node in a triangular directed
graph.
However, they also give a closed-form expression for $\pi(n,k,i)$ as a sum of binomial
coefficients and Entringer numbers, and we directly use this since it seemed easier to formalise.
›
definition seidel_triangle_aux :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"seidel_triangle_aux n k i =
(∑s≤min k (n-i). (k choose s) * ((n-k) choose (n-i-s)) * entringer_number (n-i) s)"
lemma seidel_triangle_aux_same:
assumes i: "i ≤ n"
shows "seidel_triangle_aux n n i = (n choose i) * zigzag_number (n - i)"
proof -
have "seidel_triangle_aux n n i =
(∑s≤n - i. (n choose s) * (0 choose (n - (i + s))) * entringer_number (n - i) s)"
by (simp add: seidel_triangle_aux_def)
also have "… = (∑s∈{n-i}. (n choose s) * (0 choose (n - (i + s))) * entringer_number (n - i) s)"
by (rule sum.mono_neutral_right) auto
also have "… = (n choose i) * zigzag_number (n - i)"
using i by (simp flip: binomial_symmetric)
finally show ?thesis .
qed
lemma seidel_triangle_aux_same2 [simp]: "seidel_triangle_aux n k n = 1"
by (simp add: seidel_triangle_aux_def)
lemma seidel_triangle_aux_0_middle [simp]:
"i < n ⟹ seidel_triangle_aux n 0 i = 0"
by (simp add: seidel_triangle_aux_def flip: binomial_symmetric)
lemma seidel_triangle_aux_0_right [simp]:
assumes "k ≤ n"
shows "seidel_triangle_aux n k 0 = entringer_number n k"
proof -
have "seidel_triangle_aux n k 0 = (∑s≤k. (k choose s) * (n - k choose (n - s)) * entringer_number n s)"
using assms by (simp add: seidel_triangle_aux_def)
also have "… = (∑s∈{k}. (k choose s) * (n - k choose (n - s)) * entringer_number n s)"
by (rule sum.mono_neutral_right) (use assms in auto)
finally show ?thesis
by simp
qed
text ‹
The following lemma is where most of the proof work is done. Millar et al.\ do not mention it
expicitly, but $\pi$ satistifies the recurrence
$\pi(n+1, k+1, i) = \pi(n+1, k, i) + \pi(n, n-k, i)$.
Note that this is the same type of recurrence that we have in the Seidel triangle and
the Entringer numbers.
›
lemma seidel_triangle_aux_rec:
defines "S ≡ seidel_triangle_aux"
assumes k: "k ≤ n" and i: "i ≤ n"
shows "S (Suc n) (Suc k) i = S (Suc n) k i + S n (n - k) i"
proof -
define N where "N = int n"
define K where "K = int k"
define I where "I = int i"
define B where "B = (λn k. if n < 0 ∨ k < 0 then 0 else ((nat n) choose (nat k)))"
have [simp]: "B n k = 0" if "k < 0 ∨ k > n ∨ n < 0" for n k
using that by (auto simp: B_def)
have B_rec: "B (N+1) (K+1) = B N (K+1) + B N K" if "N ≥ 0" for N K
using that by (auto simp: B_def nat_add_distrib not_less)
have B_eq: "B n' k' = (n choose k)" if "int n = n'" "int k = k'" for n n' k k'
unfolding B_def using that by auto
have B_mult_cong: "B x y * z = B x y * z'" if "x ≥ 0 ∧ y ≥ 0 ∧ y ≤ x ⟶ z = z'" for x y z z'
using that by (auto simp: B_def)
define E where "E = (λn k. if n < 0 ∨ k < 0 then 0 else entringer_number (nat n) (nat k))"
have [simp]: "E n k = 0" if "k < 0 ∨ k > n ∨ n < 0" for n k
using that by (auto simp: E_def)
have E_rec: "E (n+1) (k+1) = E (n+1) k + E n (n-k)" if "n ≥ 0" "k ≤ n" for n k
using that by (auto simp: E_def nat_add_distrib entringer_number_rec nat_diff_distrib)
have E_eq: "E n' k' = entringer_number n k" if "int n = n'" "int k = k'" for n n' k k'
unfolding E_def using that by auto
have S_eq: "S n k i = (∑⇩?s. B k' s * B (n'-k') (n'-i'-s) * E (n'-i') s)"
if "k ≤ n" "i ≤ n" "k' = int k" "n' = int n" "i' = int i" for k n i :: nat and k' n' i' :: int
proof -
have "S n k i = (∑s≤min k (n - i). B k' s * B (n'-k') (n'-i'-s) * E (n'-i') s)"
unfolding S_def seidel_triangle_aux_def using that
by (intro sum.cong arg_cong2[of _ _ _ _ "(*)"] B_eq[symmetric] E_eq[symmetric]) auto
also have "… = (∑s∈{0..min k' (n' - i')}. B k' s * B (n'-k') (n'-i'-s) * E (n'-i') s)"
by (rule sum.reindex_bij_witness[of _ nat int]) (use that in auto)
also have "… = (∑⇩?s. B k' s * B (n'-k') (n'-i'-s) * E (n'-i') s)"
by (rule Sum_any.expand_superset_cong [symmetric]) auto
finally show ?thesis .
qed
have "S (Suc n) (Suc k) i =
(∑⇩?s. B (K+1) s * B ((N+1)-(K+1)) (N+1-I-s) * E (N+1-I) s)"
by (rule S_eq) (use assms in ‹auto simp: N_def K_def I_def›)
also have "… = (∑⇩?s. B (K+1) (s+1) * (B (N-K) (N-I-s) * E (N-I+1) (s+1)))"
by (rule Sum_any.reindex_bij_witness[of "λs. s+1" "λs. s-1"]) (auto simp: algebra_simps)
also have "… = (∑⇩?s. B (K+1) (s+1) * (B (N-K) (N-I-s) * (E (N-I+1) s + E (N-I) (N-I-s))))"
by (intro Sum_any.cong B_mult_cong impI, subst E_rec)
(use assms in ‹auto simp: N_def I_def›)
also have "… = (∑⇩?s. B (K+1) (s+1) * B (N-K) (N-I-s) * E (N-I+1) s) +
(∑⇩?s. B (K+1) (s+1) * B (N-K) (N-I-s) * E (N-I) (N-I-s))"
unfolding ring_distribs mult.assoc [symmetric]
by (rule Sum_any.distrib'[where A = "{0..N-I}"]) auto
also have "(∑⇩?s. B (K+1) (s+1) * B (N-K) (N-I-s) * E (N-I) (N-I-s)) =
(∑⇩?s. B (K+1) (N-I-s+1) * B (N-K) s * E (N-I) s)"
by (rule Sum_any.reindex_bij_witness[of "λs. N-I-s" "λs. N-I-s"]) auto
also have "K ≥ 0"
by (simp add: K_def)
have "(∑⇩?s. B (K+1) (s+1) * B (N-K) (N-I-s) * E (N-I+1) s) =
(∑⇩?s. B K (s+1) * B (N-K) (N-I-s) * E (N-I+1) s) +
(∑⇩?s. B K s * B (N-K) (N-I-s) * E (N-I+1) s)"
unfolding B_rec[OF ‹K ≥ 0›] ring_distribs
by (rule Sum_any.distrib'[where A = "{0..K}"]) auto
also have "(∑⇩?s. B (K+1) (N-I-s+1) * B (N-K) s * E (N-I) s) =
(∑⇩?s. B K (N-I-s+1) * B (N-K) s * E (N-I) s) +
(∑⇩?s. B K (N-I-s) * B (N-K) s * E (N-I) s)"
unfolding B_rec[OF ‹K ≥ 0›] ring_distribs
by (rule Sum_any.distrib'[where A = "{0..N-I+1}"]) auto
finally have eq: "S (Suc n) (Suc k) i =
(∑⇩?s. B K (s+1) * B (N-K) (N-I-s) * E (N-I+1) s) +
(∑⇩?s. B K s * B (N-K) (N-I-s) * E (N-I+1) s) +
(∑⇩?s. B K (N-I-s+1) * B (N-K) s * E (N-I) s) +
(∑⇩?s. B (N-K) s * B K (N-I-s) * E (N-I) s)"
(is "_ = ?S1 + ?S2 + ?S3 + ?S4")
by (simp only: add_ac mult.commute)
have "S (Suc n) k i + S n (n - k) i =
(∑⇩?s. B K s * B (N+1-K) (N+1-I-s) * E (N+1-I) s) +
(∑⇩?s. B (N - K) s * B (N-(N - K)) (N-I-s) * E (N-I) s)"
using assms by (intro arg_cong2[of _ _ _ _ "(+)"] S_eq) (auto simp: N_def K_def I_def)
also have "… = (∑⇩?s. B K s * B (N-K+1) (N-I-s+1) * E (N-I+1) s) +
(∑⇩?s. B (N - K) s * B K (N-I-s) * E (N-I) s)"
by (simp add: algebra_simps)
also have "N - K ≥ 0"
using assms by (simp add: N_def K_def)
have "(∑⇩?s. B K s * B (N-K+1) (N-I-s+1) * E (N-I+1) s) =
(∑⇩?s. B K s * B (N-K) (N-I-s+1) * E (N-I+1) s) + ?S2"
unfolding B_rec[OF ‹N - K ≥ 0›] ring_distribs
by (rule Sum_any.distrib'[where A = "{0..K}"]) auto
also have "(∑⇩?s. B K s * B (N-K) (N-I-s+1) * E (N-I+1) s) = ?S1 + ?S3"
proof -
have "N - I ≥ 0"
using assms by (auto simp: N_def I_def)
have "(∑⇩?s. B K s * B (N-K) (N-I-s+1) * E (N-I+1) s) =
(∑⇩?s. B K (s+1) * (B (N-K) (N-I-s) * E (N-I+1) (s+1)))"
by (rule Sum_any.reindex_bij_witness[of "λs. s+1" "λs. s-1"]) (auto simp: algebra_simps)
also have "… = (∑⇩?s. B K (s+1) * (B (N-K) (N-I-s) * (E (N-I+1) s + E (N-I) (N-I-s))))"
by (intro Sum_any.cong B_mult_cong impI, subst E_rec) (use ‹N - I ≥ 0› in auto)
also have "… = ?S1 + (∑⇩?s. B K (s+1) * B (N-K) (N-I-s) * E (N-I) (N-I-s))"
unfolding ring_distribs mult.assoc [symmetric]
by (rule Sum_any.distrib'[where A = "{0..K}"]) auto
also have "(∑⇩?s. B K (s+1) * B (N-K) (N-I-s) * E (N-I) (N-I-s)) =
(∑⇩?s. B K (N-I-s+1) * B (N-K) s * E (N-I) s)"
by (rule Sum_any.reindex_bij_witness[of "λs. N-I-s" "λs. N-I-s"]) (auto simp: algebra_simps)
finally show ?thesis .
qed
finally show ?thesis
using eq by algebra
qed
text ‹
With this, we can prove the following closed form for the entry $T_{n,k}$ in the
Seidel triangle.
›
theorem seidel_triangle_eq:
assumes "k ≤ n"
shows "seidel_triangle a n k = (∑i≤n. of_nat (seidel_triangle_aux n k i) * a i)"
using assms
proof (induction a n k rule: seidel_triangle.induct)
case (1 a n)
have "(∑i≤n. of_nat (seidel_triangle_aux n 0 i) * a i) =
(∑i∈{n}. of_nat (seidel_triangle_aux n 0 i) * a i)"
by (rule sum.mono_neutral_right) (auto simp: seidel_triangle_aux_def)
thus ?case
by (simp add: seidel_triangle_aux_def)
next
case (3 a n k)
define S where "S = (λn k i. of_nat (seidel_triangle_aux n k i) :: 'a)"
from "3.prems" have "k ≤ n"
by simp
have "seidel_triangle a (Suc n) (Suc k) =
seidel_triangle a (Suc n) k + seidel_triangle a n (n - k)"
using ‹k ≤ n› by (simp add: seidel_triangle_rec)
also have "seidel_triangle a (Suc n) k = (∑i≤n. S (Suc n) k i * a i) + a (Suc n)"
unfolding S_def by (subst "3.IH") (use ‹k ≤ n› in auto)
also have "seidel_triangle a n (n - k) = (∑i≤n. S n (n - k) i * a i)"
unfolding S_def by (subst "3.IH") (use ‹k ≤ n› in auto)
also have "(∑i≤n. S (Suc n) k i * a i) + a (Suc n) + (∑i≤n. S n (n - k) i * a i) =
(∑i≤n. (S (Suc n) k i + S n (n - k) i) * a i) + a (Suc n)"
by (simp add: sum.distrib add_ac ring_distribs)
also have "(∑i≤n. (S (Suc n) k i + S n (n - k) i) * a i) = (∑i≤n. S (Suc n) (Suc k) i * a i)"
by (rule sum.cong) (use ‹k ≤ n› in ‹simp_all add: S_def seidel_triangle_aux_rec›)
also have "… + a (Suc n) = (∑i≤Suc n. S (Suc n) (Suc k) i * a i)"
by (simp add: S_def)
finally show ?case
by (simp add: S_def)
qed auto
subsection ‹The Boustrophedon transform of a sequence›
text ‹
The Boustrophedon transform of a sequence $a_n$ is defined by taking the last entry
of each row of the Seidel triangle of $a_n$.
›
definition boustrophedon :: "(nat ⇒ 'a :: monoid_add) ⇒ nat ⇒ 'a" where
"boustrophedon a n = seidel_triangle a n n"
definition inv_boustrophedon :: "(nat ⇒ 'a :: comm_ring_1) ⇒ nat ⇒ 'a" where
"inv_boustrophedon a n = (-1)^n * boustrophedon (λk. (-1)^k * a k) n"
text ‹
The Boustrophedon transform has the following nice closed form, which of course follows
directly from our above closed form for the Seidel triangle:
›
theorem boustrophedon_eq:
fixes a :: "nat ⇒ 'a :: comm_semiring_1"
shows "boustrophedon a n = (∑k≤n. of_nat (n choose k) * a k * of_nat (zigzag_number (n - k)))"
by (simp add: boustrophedon_def seidel_triangle_eq seidel_triangle_aux_same mult_ac)
text ‹
The inverse Boustrophedon transform is the same as the normal Boustrophedon transform except
that we must negate every other number in the input and output sequences.
›
theorem inv_boustrophedon_eq:
fixes a :: "nat ⇒ 'a :: comm_ring_1"
shows "inv_boustrophedon a n = (∑k≤n. (-1) ^ (n - k) * of_nat (n choose k) * a k * of_nat (zigzag_number (n - k)))"
unfolding inv_boustrophedon_def boustrophedon_eq sum_distrib_left
by (intro sum.cong) (auto simp: uminus_power_if)
text ‹
In particular, the Entringer numbers are the Seidel triangle of the sequence
$1, 0, 0, 0, \ldots$.
›
corollary entringer_number_conv_seidel_triangle:
"seidel_triangle (λn. if n = 0 then 1 else 0 :: 'a :: comm_semiring_1) n k =
of_nat (entringer_number n k)"
proof (cases "k ≤ n")
case True
have "k ≤ n"
using True by auto
have "seidel_triangle (λn. if n = 0 then 1 else 0 :: 'a) n k =
of_nat (∑i≤n. seidel_triangle_aux n k i * (if i = 0 then 1 else 0))"
unfolding seidel_triangle_eq[OF ‹k ≤ n›] of_nat_sum
by (rule sum.cong) (use True in auto)
also have "(∑i≤n. seidel_triangle_aux n k i * (if i = 0 then 1 else 0)) =
(∑i∈{0}. seidel_triangle_aux n k i * (if i = 0 then 1 else 0))"
by (rule sum.mono_neutral_right) auto
also have "… = entringer_number n k"
using True by simp
finally show ?thesis .
qed auto
text ‹
And consequently, the zigzag numbers are the Boustrophedon transform of the sequence
$1, 0, 0, 0, \ldots$.
›
corollary zigzag_number_conv_boustrophedon:
"boustrophedon (λn. if n = 0 then 1 else 0 :: 'a :: comm_semiring_1) n =
of_nat (zigzag_number n)"
unfolding boustrophedon_def
by (subst entringer_number_conv_seidel_triangle) auto
subsection ‹The Boustrophedon transform of a function›
text ‹
Analogously, one can define the Boustrophedon transform $\mathcal B(f)(x)$ of an exponential
generating function $f(x) = \sum_{n\geq 0} f(n)/n! x^n$ and its inverse $\mathcal B^{-1}(f)(x)$:
›
definition Boustrophedon :: "'a :: field_char_0 fps ⇒ 'a fps" where
"Boustrophedon A = Abs_fps (λn. boustrophedon (λn. fps_nth A n * fact n) n / fact n)"
definition inv_Boustrophedon :: "'a :: field_char_0 fps ⇒ 'a fps" where
"inv_Boustrophedon A = Abs_fps (λn. inv_boustrophedon (λn. fps_nth A n * fact n) n / fact n)"
lemma fps_nth_Boustrophedon:
fixes A :: "'a :: field_char_0 fps"
shows "fps_nth (Boustrophedon A) n =
(∑k≤n. fps_nth A k * of_nat (zigzag_number (n - k)) / fact (n - k))"
by (simp add: Boustrophedon_def boustrophedon_eq field_simps sum_distrib_left sum_distrib_right
binomial_fact)
lemma fps_nth_inv_Boustrophedon:
fixes A :: "'a :: field_char_0 fps"
shows "fps_nth (inv_Boustrophedon A) n =
(∑k≤n. (-1)^(n-k) * fps_nth A k * of_nat (zigzag_number (n - k)) / fact (n - k))"
by (simp add: inv_Boustrophedon_def inv_boustrophedon_eq field_simps
sum_distrib_left sum_distrib_right binomial_fact)
text ‹
We have the closed form $\mathcal B(f) = (\sec + \tan)f$:
›
theorem Boustrophedon_altdef:
fixes A :: "'a :: field_char_0 fps"
shows "Boustrophedon A = (fps_sec 1 + fps_tan 1) * A"
by (subst mult.commute, rule fps_ext,
subst exponential_generating_function_zigzag_number [symmetric])
(simp add: fps_nth_Boustrophedon fps_mult_nth atLeast0AtMost)
text ‹
It is also easy to see from the definition of $\mathcal B^{-1}$ that we have
$\mathcal B^{-1}(f)(x) = \mathcal B(g)(-x)$, where $g(x) = f(-x)$.
›
theorem inv_Boustrophedon_altdef1:
fixes A :: "'a :: field_char_0 fps"
shows "inv_Boustrophedon A = fps_compose (Boustrophedon (fps_compose A (-fps_X))) (-fps_X)"
by (rule fps_ext)
(simp_all add: inv_Boustrophedon_def Boustrophedon_def fps_nth_compose_uminus
inv_boustrophedon_def mult.assoc)
text ‹
Or, yet another view on $\mathcal B^{-1}$:
$\mathcal B^{-1}(f)(x) = (\sec (-x) + \tan (-x)) f(x)$.
›
lemma inv_Boustrophedon_altdef2:
fixes A :: "'a :: field_char_0 fps"
shows "inv_Boustrophedon A = (fps_sec 1 - fps_tan 1) * A"
proof -
have "inv_Boustrophedon A =
(A * fps_compose (Abs_fps (λk. of_nat (zigzag_number k) / fact k)) (-fps_X))"
unfolding fps_eq_iff fps_nth_inv_Boustrophedon fps_mult_nth
by (simp add: fps_nth_compose_uminus mult_ac atLeast0AtMost)
also have "Abs_fps (λk. of_nat (zigzag_number k) / fact k) = fps_sec (1::'a) + fps_tan 1"
by (simp add: exponential_generating_function_zigzag_number)
also have "fps_compose … (-fps_X) = fps_sec 1 - fps_tan 1"
by (simp add: fps_compose_add_distrib fps_sec_even fps_tan_odd)
finally show ?thesis by (simp add: mult.commute)
qed
lemma fps_sec_plus_tan_times_sec_minus_tan:
"(fps_sec (c ::'a :: field_char_0) + fps_tan c) * (fps_sec c - fps_tan c) = 1"
proof -
define S where "S = fps_to_fls (fps_sin c)"
define C where "C = fps_to_fls (fps_cos c)"
have "fls_nth C 0 = 1"
by (simp add: C_def)
hence [simp]: "C ≠ 0"
by auto
have "fps_to_fls ((fps_sec c + fps_tan c) * (fps_sec c - fps_tan c)) =
(inverse C + S / C) * (inverse C - S / C)"
by (simp add: fps_sec_def fps_tan_def fls_times_fps_to_fls S_def C_def
flip: fls_inverse_fps_to_fls fls_divide_fps_to_fls)
also have "(inverse C - S / C) = (1 - S) / C"
by (simp add: divide_simps)
also have "(inverse C + S / C) = (1 + S) / C"
by (simp add: divide_simps)
also have "(1 + S) / C * ((1 - S) / C) = (1 - S ^ 2) / C ^ 2"
by (simp add: algebra_simps power2_eq_square)
also have "1 - S ^ 2 = C ^ 2"
proof -
have "1 - S ^ 2 = fps_to_fls (1 - fps_sin c ^ 2)"
by (simp add: S_def fps_to_fls_power)
also have "1 - fps_sin c ^ 2 = fps_cos c ^ 2"
using fps_sin_cos_sum_of_squares[of c] by algebra
also have "fps_to_fls … = C ^ 2"
by (simp add: C_def fps_to_fls_power)
finally show ?thesis .
qed
also have "C ^ 2 / C ^ 2 = fps_to_fls 1"
by simp
finally show ?thesis
by (simp only: fps_to_fls_eq_iff)
qed
text ‹
Or, equivalently: $\mathcal B^{-1}(f) = f / (\sec + \tan)$.
›
theorem inv_Boustrophedon_altdef3:
fixes A :: "'a :: field_char_0 fps"
shows "inv_Boustrophedon A = A / (fps_sec 1 + fps_tan 1)"
proof (rule sym, rule divide_fps_eqI)
have "inv_Boustrophedon A * (fps_sec 1 + fps_tan 1) =
((fps_sec 1 + fps_tan 1) * (fps_sec 1 - fps_tan 1)) * A"
unfolding inv_Boustrophedon_altdef2 by (simp only: mult_ac)
thus "inv_Boustrophedon A * (fps_sec 1 + fps_tan 1) = A"
by (simp only: fps_sec_plus_tan_times_sec_minus_tan mult_1_left)
next
have "fps_nth (fps_sec 1 + fps_tan (1::'a)) 0 = 1"
by auto
hence "fps_sec 1 + fps_tan (1::'a) ≠ 0"
by (intro notI) simp_all
thus "A ≠ 0 ∨ fps_sec 1 + fps_tan (1::'a) ≠ 0 ∨ inv_Boustrophedon A = 0"
by blast
qed
text ‹
It is now obvious that $\mathcal B$ and $\mathcal B^{-1}$ really are inverse to one another.
›
lemma Boustrophedon_inv_Boustrophedon [simp]:
fixes A :: "'a :: field_char_0 fps"
shows "Boustrophedon (inv_Boustrophedon A) = A"
proof -
have "Boustrophedon (inv_Boustrophedon A) =
A * ((fps_sec (1::'a) + fps_tan 1) * (fps_sec 1 - fps_tan 1))"
by (simp add: Boustrophedon_altdef inv_Boustrophedon_altdef2)
also have "(fps_sec (1::'a) + fps_tan 1) * (fps_sec 1 - fps_tan 1) = 1"
by (rule fps_sec_plus_tan_times_sec_minus_tan)
finally show ?thesis
by simp
qed
lemma inv_Boustrophedon_Boustrophedon [simp]:
fixes A :: "'a :: field_char_0 fps"
shows "inv_Boustrophedon (Boustrophedon A) = A"
proof -
have "inv_Boustrophedon (Boustrophedon A) =
A * ((fps_sec (1::'a) + fps_tan 1) * (fps_sec 1 - fps_tan 1))"
by (simp add: Boustrophedon_altdef inv_Boustrophedon_altdef2)
also have "(fps_sec (1::'a) + fps_tan 1) * (fps_sec 1 - fps_tan 1) = 1"
by (rule fps_sec_plus_tan_times_sec_minus_tan)
finally show ?thesis
by simp
qed
syntax
"_Sum_any" :: "pttrn ⇒ 'a ⇒ 'a::comm_monoid_add" ("(3∑_. _)" [0, 10] 10)
no_syntax
"_Sum_any" :: "pttrn ⇒ 'a ⇒ 'a::comm_monoid_add" ("(3∑⇩?_. _)" [0, 10] 10)
end