(*  Title:       Much Ado about Two
Author:      Sascha Böhme <boehmes@informatik.tu-muenchen.de>, 2007
Maintainer:  Sascha Böhme <boehmes@informatik.tu-muenchen.de>
*)

(*<*)
imports "HOL-Combinatorics.Permutations"
begin
(*>*)

text ‹

Due to Donald E. Knuth, it is known for some time that certain sorting
functions for lists of arbitrary types can be proved correct by only showing
that they are correct for boolean lists (\cite{KnuthSortingAndSearching},
This reduction idea, i.e. reducing a proof for an arbitrary type to a proof for a fixed type with a fixed number of values, has also instances in other
fields.
is explained for the problem of parallel prefix computation
\cite{PrefixSumsAndTheirApplications}.
That is the task to compute, for given $x_1, \ldots, x_n$ and an associative
operation $\oplus$, the values $x_1$, $x_1 \oplus x_2$, $\ldots$,
$x_1 \oplus x_2 \oplus \cdots \oplus x_n$.
There are several solutions which optimise this computation, and an
obvious question is to ask whether these solutions are correct.
There, a 0-1-2-principle'' is proved which relates an unspecified solution
of the parallel prefix computation, expressed as a function ‹candidate›,
with ‹scanl1›, a functional representation of the parallel prefix
computation. The essence proved in the mentioned paper is as follows:
If ‹candidate› and ‹scanl1› behave identical on all lists over
a type which has three elements, then ‹candidate› is semantically
equivalent to ‹scanl1›, that is, ‹candidate› is a correct solution
of the parallel prefix computation.

Although it seems that nearly nothing is known about the function
‹candidate›, it turns out that the type of ‹candidate› already
suffices for the proof of the paper's result. The key is relational
parametricity \cite{TypesAbstractionsAndParametricPolymorphism} in the form of
a free theorem \cite{TheoremsForFree}. This, some rewriting and a few
properties about list-processing functions thrown in allow to proof the
0-1-2-principle''.

The paper first shows some simple properties and derives a specialisation of
the free theorem. The proof of the main theorem itself is split up in two
parts. The first, and considerably more complicated part relates lists over a
type with three values to lists of integer lists. Here, the paper uses
several figures to demonstrate and shorten several proofs. The second part then
relates lists of integer list with lists over arbitrary types, and consists of
applying the free theorem and some rewriting. The combination of these two
parts then yields the theorem.

which is called here the original paper''. Compared to that paper, there are
A more detailed collection follows thereafter.

\begin{itemize}
\item The original paper requires lists to be non-empty. Eventhough lists in
Isabelle may also be empty, we stick to Isabelle's list datatype instead of
declaring a new datatype, due to the huge, already existing theory about
lists in Isabelle. As a consequence, however, several modifications become
necessary.

\item The figure-based proofs of the original paper are replaced by formal
proofs. This forms a major part of this article (see Section 6).

\item Instead of integers, we restrict ourselves to natural numbers. Thus,
several conditions can be simplified since every natural number is greater
than or equal to ‹0›. This decision has no further influence on the
proofs because they never consider negative integers.

\item Mainly due to differences between Haskell and Isabelle, certain notations
are different here compared to the original paper. List concatenation is
denoted by ‹@› instead of $++$, and in writing down intervals, we use
‹[0..<k + 1]› instead of ‹[0..k]›. Moreover, we write ‹f›
instead of $\oplus$ and ‹g› instead of $\otimes$. Functions mapping
an element of the three-valued type to an arbitrary type are denoted by
‹h›.

\end{itemize}

Whenever we use lemmas from already existing Isabelle theories, we qualify
them by their theory name. For example, instead of ‹map_map›, we
write ‹List.map_map› to point out that this lemma is taken from
Isabelle's list theory.

The following comparison shows all differences of this article compared to the
original paper. The items below follow the structure of the original paper
needed to be solved in formalising the original paper.

\begin{itemize}
\item Introductions of several list functions (e.g. ‹length›,
‹map›, ‹take›) are dropped. They exist already in Isabelle's list
theory and are be considered familiar to the reader.

\item The free theorem given in Lemma 1 of the original paper is not sufficient
for later proofs, because the assumption is not appropriate in the context
of Isabelle's lists, which may also be empty. Thus, here, Lemma 1 is a
derived version of the free theorem given as Lemma 1 in the original paper,
and some additional proof-work is done.

\item Before proceeding in the original paper's way, we state and proof
additional lemmas, which are not part of Isabelle's libraries. These lemmas
are not specific to this article and may also be used in other theories.

\item Laws 1 to 8 and Lemma 2 of the original paper are explicitly proved.
Most of the proofs follow directly from existing results of Isabelle's list
theory. To proof Law 7, Law 8 and Lemma 2, more work was necessary, especially
for Law 8.

\item Lemma 3 and its proof are nearly the same here as in the original paper.
Only the additional assumptions of Lemma 1, due to Isabelle's list datatype,
have to be shown.

\item Lemma 4 is split up in several smaller lemmas, and the order of them
tries to follow the structure of the original paper's Lemma 4.

For every figure of the original paper, there is now one separate proof.
These proofs constitute the major difference in the structure of this article
compared to the original paper.

The proof of Lemma 4 in the original paper concludes by combining the results
of the figure-based proofs to a non-trivial permutation property. These three
sentences given in the original paper are split up in five separate lemmas
and according proofs, and therefore, they as well form a major difference to
the original paper.

\item Lemma 5 is mostly identical to the version in the original paper. It has
one additional assumption required by Lemma 4. Moreover, the proof is slightly
more structured, and some steps needed a bit more argumentation than in the
original paper.

\item In principle, Proposition 1 is identical to the according proposition in
the original paper. However, to fulfill the additional requirement of Lemma 5,
an additional lemma was proved. This, however, is only necessary, because we
use Isabelle's list type which allows lists to be empty.

\item Proposition 2 contains one non-trivial step, which is proved as a
seperate lemma. Note that this is not due to any decisions of using special
datatypes, but inherent in the proof itself.  Apart from that, the proof is
identical to the original paper's proof of Proposition 2.

\item The final theorem is, as in the original paper, just a combination of
Proposition 1 and Proposition 2. Only the assumptions are extended due to
Isabelle's list datatype.

\end{itemize}

›

section ‹Basic definitions›

fun foldl1 :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a list ⇒ 'a"
where
"foldl1 f (x # xs) = foldl f x xs"

fun scanl1 :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a list ⇒ 'a list"
where
"scanl1 f xs = map (λk. foldl1 f (take k xs))
[1..<length xs + 1]"

text ‹
The original paper further relies on associative functions. Thus, we define
another predicate to be able to express this condition:
›

definition
"associative f ≡ (∀x y z. f x (f y z) = f (f x y) z)"

text ‹
The following constant symbols represents our unspecified function. We want to
show that this function is semantically equivalent to ‹scanl1›, provided
that the first argument is an associative function.
›

consts
candidate :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a list ⇒ 'a list"

text ‹
With the final theorem, it suffices to show that ‹candidate› behaves like
‹scanl1› on all lists of the following type, to conclude that
‹canditate› is semantically equivalent to ‹scanl1›.
›

datatype three = Zero | One | Two

text ‹
Although most of the functions mentioned in the original paper already exist
in Isabelle's list theory, we still need to define two more functions:
›

fun wrap :: "'a ⇒ 'a list"
where
"wrap x = [x]"

fun ups :: "nat ⇒ nat list list"
where
"ups n = map (λk. [0..<k + 1]) [0..<n + 1]"

section ‹A Free Theorem›

text ‹
The key to proof the final theorem is the following free theorem \cite{TypesAbstractionsAndParametricPolymorphism,TheoremsForFree} of ‹candidate›.
Since there is no proof possible without specifying the underlying
(functional) language (which would be beyond the scope of this work),
this lemma is expected to hold. As a consequence, all following lemmas and also
the final theorem only hold under this provision.
›

axiomatization where
candidate_free_theorem:
"⋀x y. h (f x y) = g (h x) (h y) ⟹ map h (candidate f zs) = candidate g (map h zs)"

text ‹
In what follows in this section, the previous lemma is specialised to a lemma
for non-empty lists. More precisely, we want to restrict the above assumption
to be applicable for non-empty lists. This is already possible without
modifications when having a list datatype which does not allow for empty lists.
However, before being able to also use Isabelle's list datatype, further
conditions on ‹f› and ‹zs› are necessary.

To prove the derived lemma, we first introduce a datatype for non-empty lists,
and we furthermore define conversion functions to map the new datatype on
Isabelle lists and back.
›

datatype 'a nel
= NE_One 'a
| NE_Cons 'a "'a nel"

fun n2l :: "'a nel ⇒ 'a list"
where
"n2l (NE_One x)     = [x]"
| "n2l (NE_Cons x xs) = x # n2l xs"

fun l2n :: "'a list ⇒ 'a nel"
where
"l2n [x]      = NE_One x"
| "l2n (x # xs) = (case xs of []      ⇒ NE_One x
| (_ # _) ⇒ NE_Cons x (l2n xs))"

text ‹
The following results relate Isabelle lists and non-empty lists:
›

lemma non_empty_n2l: "n2l xs ≠ []"
by (cases xs, auto)

lemma n2l_l2n_id: "x ≠ [] ⟹ n2l (l2n x) = x"
proof (induct x)
case Nil thus ?case by simp
next
case (Cons x xs) thus ?case by (cases xs, auto)
qed

lemma n2l_l2n_map_id:
assumes "⋀x. x ∈ set zs ⟹ x ≠ []"
shows "map (n2l ∘ l2n) zs = zs"
using assms
proof (induct zs)
case Nil thus ?case by simp
next
case (Cons z zs)
hence "⋀x. x ∈ set zs ⟹ x ≠ []" using List.set_subset_Cons by auto
with Cons have IH: "map (n2l ∘ l2n) zs = zs" by blast

have
"map (n2l ∘ l2n) (z # zs)
= (n2l ∘ l2n) z # map (n2l ∘ l2n) zs" by simp
also have
"… = z # map (n2l ∘ l2n) zs" using Cons and n2l_l2n_id by auto
also have
"… = z # zs" using IH by simp
finally show ?case .
qed

text ‹
Based on the previous lemmas, we can state and proof a specialised version
of ‹candidate›'s free theorem, suitable for our setting as explained
before.
›

lemma Lemma_1:
assumes A1: "⋀(x::'a list) (y::'a list).
x ≠ [] ⟹ y ≠ [] ⟹ h (f x y) = g (h x) (h y)"
and A2: "⋀x y. x ≠ [] ⟹ y ≠ [] ⟹ f x y ≠ []"
and A3: "⋀x. x ∈ set zs ⟹ x ≠ []"
shows "map h (candidate f zs) = candidate g (map h zs)"
proof -
― ‹We define two functions, @{text "fn :: 'a nel ⇒ 'a nel ⇒ 'a nel"} and›
― ‹@{text "hn :: 'a nel ⇒ b"}, which wrap @{text f} and @{text h} in the›
― ‹setting of non-empty lists.›
let ?fn = "λx y. l2n (f (n2l x) (n2l y))"
let ?hn = "h ∘ n2l"

― ‹Our new functions fulfill the preconditions of @{text candidate}'s›
― ‹free theorem:›
have "⋀(x::'a nel) (y::'a nel). ?hn (?fn x y) = g (?hn x) (?hn y)"
proof -
fix x y
let ?xl = "n2l (x :: 'a nel)"
let ?yl = "n2l (y :: 'a nel)"
have
"?hn (?fn x y)
= h (n2l (l2n (f (n2l x) (n2l y))))" by simp
also have
"… = h (f ?xl ?yl)"
using A2 [where x="?xl" and y="?yl"]
and n2l_l2n_id [where x="f (n2l x) (n2l y)"]
and non_empty_n2l [where xs=x]
and non_empty_n2l [where xs=y] by simp
also have
"… = g (h ?xl) (h ?yl)"
using A1 and non_empty_n2l and non_empty_n2l by auto
also have
"… = g (?hn x) (?hn y)" by simp
finally show "?hn (?fn x y) = g (?hn x) (?hn y)" .
qed
with candidate_free_theorem [where f="?fn" and h="?hn" and g = g]
have ne_free_theorem:
"map ?hn (candidate ?fn (map l2n zs)) = candidate g (map ?hn (map l2n zs))"
by auto

― ‹We use @{text candidate}'s free theorem again to show the following›
― ‹property:›
have n2l_candidate:
"⋀zs. map n2l (candidate ?fn zs) = candidate f (map n2l zs)"
proof -
fix zs
have "⋀x y. n2l (?fn x y) = f (n2l x) (n2l y)"
proof -
fix x y
show "n2l (?fn x y) = f (n2l x) (n2l y)"
using n2l_l2n_id [where x="f (n2l x) (n2l y)"]
and A2 [where x="n2l x" and y="n2l y"]
and non_empty_n2l [where xs=x] and non_empty_n2l [where xs=y]
by simp
qed
with candidate_free_theorem [where h=n2l and f="?fn" and g=f]
show "map n2l (candidate ?fn zs) = candidate f (map n2l zs)" by simp
qed

― ‹Now, with the previous preparations, we conclude the thesis by the›
― ‹following rewriting:›
have
"map h (candidate f zs)
= map h (candidate f (map (n2l ∘ l2n) zs))"
using n2l_l2n_map_id [where zs=zs] and A3 by simp
also have
"… = map h (candidate f (map n2l (map l2n zs)))"
using List.map_map [where f=n2l and g=l2n and xs=zs] by simp
also have
"…= map h (map n2l (candidate ?fn (map l2n zs)))"
using n2l_candidate by auto
also have
"… = map ?hn (candidate ?fn (map l2n zs))"
using List.map_map by auto
also have
"… = candidate g (map ?hn (map l2n zs))"
using ne_free_theorem by simp
also have
"… = candidate g (map ((h ∘ n2l) ∘ l2n) zs)"
using List.map_map [where f="h ∘ n2l" and g=l2n] by simp
also have
"… = candidate g (map (h ∘ (n2l ∘ l2n)) zs)"
using Fun.o_assoc [symmetric, where f=h and g=n2l and h=l2n] by simp
also have
"… = candidate g (map h (map (n2l ∘ l2n) zs))"
using List.map_map [where f=h and g="n2l ∘ l2n"] by simp
also have
"… = candidate g (map h zs)"
using n2l_l2n_map_id [where zs=zs] and A3 by auto
finally show ?thesis .
qed

section ‹Useful lemmas›

text ‹
In this section, we state and proof several lemmas, which neither occur in the
original paper nor in Isabelle's libraries.
›

lemma upt_map_Suc:
"k > 0 ⟹ [0..<k + 1] = 0 # map Suc [0..<k]"
using List.upt_conv_Cons and List.map_Suc_upt by simp

lemma divide_and_conquer_induct:
assumes A1: "P []"
and A2: "⋀x. P [x]"
and A3: "⋀xs ys. ⟦ xs ≠ [] ; ys ≠ [] ; P xs ; P ys ⟧ ⟹ P (xs @ ys)"
shows "P zs"
proof (induct zs)
case Nil with A1 show ?case by simp
next
case (Cons z zs)
hence IH: "P zs" by simp
show ?case
proof (cases zs)
case Nil with A2 show ?thesis by simp
next
case Cons with IH and A2 and A3 [where xs="[z]" and ys=zs]
show ?thesis by auto
qed
qed

lemmas divide_and_conquer
= divide_and_conquer_induct [case_names Nil One Partition]

lemma all_set_inter_empty_distinct:
assumes "⋀xs ys. js = xs @ ys ⟹ set xs ∩ set ys = {}"
shows "distinct js"
using assms proof (induct js rule: divide_and_conquer)
case Nil thus ?case by simp
next
case One thus ?case by simp
next
case (Partition xs ys)
hence P: "⋀as bs. xs @ ys = as @ bs ⟹ set as ∩ set bs = {}" by simp

have "⋀xs1 xs2. xs = xs1 @ xs2 ⟹ set xs1 ∩ set xs2 = {}"
proof -
fix xs1 xs2
assume "xs = xs1 @ xs2"
hence "set xs1 ∩ set (xs2 @ ys) = {}"
using P [where as=xs1 and bs="xs2 @ ys"] by simp
thus "set xs1 ∩ set xs2 = {}"
using List.set_append and Set.Int_Un_distrib by auto
qed
with Partition have distinct_xs: "distinct xs" by simp
have "⋀ys1 ys2. ys = ys1 @ ys2 ⟹ set ys1 ∩ set ys2 = {}"
proof -
fix ys1 ys2
assume "ys = ys1 @ ys2"
hence "set (xs @ ys1) ∩ set ys2 = {}"
using P [where as="xs @ ys1" and bs=ys2] by simp
thus "set ys1 ∩ set ys2 = {}"
using List.set_append and Set.Int_Un_distrib by auto
qed
with Partition have distinct_ys: "distinct ys" by simp
from Partition and distinct_xs and distinct_ys show ?case by simp
qed

lemma partitions_sorted:
assumes "⋀xs ys x y. ⟦ js = xs @ ys ; x ∈ set xs ; y ∈ set ys ⟧ ⟹ x ≤ y"
shows "sorted js"
using assms proof (induct js rule: divide_and_conquer)
case Nil thus ?case by simp
next
case One thus ?case by simp
next
case (Partition xs ys)
hence P: "⋀as bs x y. ⟦ xs @ ys = as @ bs ; x ∈ set as ; y ∈ set bs⟧ ⟹ x ≤ y"
by simp

have "⋀xs1 xs2 x y. ⟦ xs = xs1 @ xs2 ; x ∈ set xs1 ; y ∈ set xs2 ⟧ ⟹ x ≤ y"
proof -
fix xs1 xs2
assume "xs = xs1 @ xs2"
hence "⋀x y. ⟦ x ∈ set xs1 ; y ∈ set (xs2 @ ys) ⟧ ⟹ x ≤ y"
using P [where as=xs1 and bs="xs2 @ ys"] by simp
thus "⋀x y. ⟦ x ∈ set xs1 ; y ∈ set xs2 ⟧ ⟹ x ≤ y"
using List.set_append by auto
qed
with Partition have sorted_xs: "sorted xs" by simp
have "⋀ys1 ys2 x y. ⟦ ys = ys1 @ ys2 ; x ∈ set ys1 ; y ∈ set ys2 ⟧ ⟹ x ≤ y"
proof -
fix ys1 ys2
assume "ys = ys1 @ ys2"
hence "⋀x y. ⟦ x ∈ set (xs @ ys1) ; y ∈ set ys2 ⟧ ⟹ x ≤ y"
using P [where as="xs @ ys1" and bs=ys2] by simp
thus "⋀x y. ⟦ x ∈ set ys1 ; y ∈ set ys2 ⟧ ⟹ x ≤ y"
using List.set_append by auto
qed
with Partition have sorted_ys: "sorted ys" by simp

have "∀x ∈ set xs. ∀y ∈ set ys. x ≤ y"
using P [where as=xs and bs=ys] by simp
with sorted_xs and sorted_ys show ?case using List.sorted_append by auto
qed

section ‹Preparatory Material›

text ‹
In the original paper, the following lemmas L1 to L8 are given without a proof,
although it is hinted there that most of them follow from parametricity
properties \cite{TypesAbstractionsAndParametricPolymorphism,TheoremsForFree}.
Alternatively, most of them can be shown by induction over lists.
However, since we are using Isabelle's list datatype, we rely on already
existing results.
›

lemma L1: "map g (map f xs) = map (g ∘ f) xs"
using List.map_map by auto

lemma L2: "length (map f xs) = length xs"
using List.length_map by simp

lemma L3: "take k (map f xs) = map f (take k xs)"
using List.take_map by auto

lemma L4: "map f ∘ wrap = wrap ∘ f"

lemma L5: "map f (xs @ ys) = (map f xs) @ (map f ys)"
using List.map_append by simp

lemma L6: "k < length xs ⟹ (map f xs) ! k = f (xs ! k)"
using List.nth_map by simp

lemma L7: "⋀k. k < length xs ⟹ map (nth xs) [0..<k + 1] = take (k + 1) xs"
proof (induct xs)
case Nil thus ?case by simp
next
case (Cons x xs)
thus ?case
proof (cases k)
case 0 thus ?thesis by simp
next
case (Suc k')
hence "k > 0" by simp
hence "map (nth (x # xs)) [0..<k + 1]
= map (nth (x # xs)) (0 # map Suc [0..<k])"
using upt_map_Suc by simp
also have "… = ((x # xs) ! 0) # (map (nth (x # xs) ∘ Suc) [0..<k])"
using L1 by simp
also have "… = x # map (nth xs) [0..<k]" by simp
also have "… = x # map (nth xs) [0..<k' + 1]" using Suc by simp
also have "… = x # take (k' + 1) xs" using Cons and Suc by simp
also have "… = take (k + 1) (x # xs)" using Suc by simp
finally show ?thesis .
qed
qed

text ‹
In Isabelle's list theory, a similar result for ‹foldl› already exists.
Therefore, it is easy to prove the following lemma for ‹foldl1›.
Note that this lemma does not occur in the original paper.
›

lemma foldl1_append:
assumes "xs ≠ []"
shows "foldl1 f (xs @ ys) = foldl1 f (foldl1 f xs # ys)"
proof -
have non_empty_list: "xs ≠ [] ⟹ ∃y ys. xs = y # ys" by (cases xs, auto)
with assms obtain x xs' where x_xs_def: "xs = x # xs'" by auto

have "foldl1 f (xs @ ys) = foldl f x (xs' @ ys)" using x_xs_def by simp
also have "… = foldl f (foldl f x xs') ys" using List.foldl_append by simp
also have "… = foldl f (foldl1 f (x # xs')) ys" by simp
also have "… = foldl1 f (foldl1 f xs # ys)" using x_xs_def by simp
finally show ?thesis .
qed

text ‹
This is a special induction scheme suitable for proving L8. It is not mentioned
in the original paper.
›

lemma foldl1_induct':
assumes "⋀f x. P f [x]"
and "⋀f x y. P f [x, y]"
and "⋀f x y z zs. P f (f x y # z # zs) ⟹ P f (x # y # z # zs)"
and "⋀f. P f []"
shows "P f xs"
proof (induct xs rule: List.length_induct)
fix xs
assume A: "∀ys::'a list. length ys < length (xs::'a list) ⟶ P f ys"
thus "P f xs"
proof (cases xs)
case Nil with assms show ?thesis by simp
next
case (Cons x1 xs1)
hence xs1: "xs = x1 # xs1" by simp
thus ?thesis
proof (cases xs1)
case Nil with assms and xs1 show ?thesis by simp
next
case (Cons x2 xs2)
hence xs2: "xs1 = x2 # xs2" by simp
thus ?thesis
proof (cases xs2)
case Nil with assms and xs1 and xs2 show ?thesis by simp
next
case (Cons x3 xs3)
hence "xs2 = x3 # xs3" by simp
with assms and xs1 xs2 and A show ?thesis by simp
qed
qed
qed
qed

lemmas foldl1_induct = foldl1_induct' [case_names One Two More Nil]

lemma L8:
assumes "associative f"
and "xs ≠ []"
and "ys ≠ []"
shows "foldl1 f (xs @ ys) = f (foldl1 f xs) (foldl1 f ys)"
using assms proof (induct f ys rule: foldl1_induct)
case (One f y)
have
"foldl1 f (xs @ [y])
= foldl1 f (foldl1 f xs # [y])"
using foldl1_append [where xs=xs] and One by simp
also have
"… = f (foldl1 f xs) y" by simp
also have
"… = f (foldl1 f xs) (foldl1 f [y])" by simp
finally show ?case .
next
case (Two f x y)
have
"foldl1 f (xs @ [x, y])
= foldl1 f (foldl1 f xs # [x, y])"
using foldl1_append [where xs=xs] and Two by simp
also have
"… = foldl1 f (f (foldl1 f xs) x # [y])" by simp
also have
"… = f (f (foldl1 f xs) x) y" by simp
also have
"… = f (foldl1 f xs) (f x y)" using Two
unfolding associative_def by simp
also have
"… = f (foldl1 f xs) (foldl1 f [x, y])" by simp
finally show ?case .
next
case (More f x y z zs)
hence IH: "foldl1 f (xs @ f x y # z # zs)
= f (foldl1 f xs) (foldl1 f (f x y # z # zs))" by simp

have
"foldl1 f (xs @ x # y # z # zs)
= foldl1 f (foldl1 f xs # x # y # z # zs)"
using foldl1_append [where xs=xs] and More by simp
also have
"… = foldl1 f (f (foldl1 f xs) x # y # z # zs)" by simp
also have
"… = foldl1 f (f (f (foldl1 f xs) x) y # z # zs)" by simp
also have
"… = foldl1 f (f (foldl1 f xs) (f x y) # z # zs)"
using More unfolding associative_def by simp
also have
"… = foldl1 f (foldl1 f xs # f x y # z # zs)" by simp
also have
"… = foldl1 f (xs @ f x y # z # zs)"
using foldl1_append [where xs=xs] and More by simp
also have
"… = f (foldl1 f xs) (foldl1 f (x # y # z # zs))"
using IH by simp
finally show ?case .
next
case Nil thus ?case by simp
qed

text ‹
The next lemma is applied in several following proofs whenever the equivalence
of two lists is shown.
›

lemma Lemma_2:
assumes "length xs = length ys"
and "⋀k. k < length xs ⟹ xs ! k = ys ! k"
shows "xs = ys"
using assms by (auto simp: List.list_eq_iff_nth_eq)

text ‹
In the original paper, this lemma and its proof appear inside of Lemma 3.
However, this property will be useful also in later proofs and is thus
separated.
›

lemma foldl1_map:
assumes "associative f"
and "xs ≠ []"
and "ys ≠ []"
shows "foldl1 f (map h (xs @ ys))
= f (foldl1 f (map h xs)) (foldl1 f (map h ys))"
proof -
have
"foldl1 f (map h (xs @ ys))
= foldl1 f (map h xs @ map h ys)"
using L5 by simp
also have
"… = f (foldl1 f (map h xs)) (foldl1 f (map h ys))"
using assms and L8 [where f=f] by auto
finally show ?thesis .
qed

lemma Lemma_3:
fixes f :: "'a ⇒ 'a ⇒ 'a"
and h :: "nat ⇒ 'a"
assumes "associative f"
shows "map (foldl1 f ∘ map h) (candidate (@) (map wrap [0..<n+1]))
= candidate f (map h [0..<n+1])"
proof -
― ‹The following three properties @{text P1}, @{text P2} and @{text P3}›
― ‹are preconditions of Lemma 1.›
have P1:
"⋀x y. ⟦ x ≠ [] ; y ≠ [] ⟧
⟹ foldl1 f (map h (x @ y)) = f (foldl1 f (map h x)) (foldl1 f (map h y))"
using assms and foldl1_map by blast

have P2: "⋀x y. x ≠ [] ⟹ y ≠ [] ⟹ x @ y  ≠ []" by auto

have P3: "⋀x. x ∈ set (map wrap [0..<n+1]) ⟹ x ≠ []" by auto

― ‹The proof for the thesis is now equal to the one of the original paper:›
from Lemma_1 [where h="foldl1 f ∘ map h" and zs="map wrap [0..<n+1]"
and f="(@)"] and P1 P2 P3
have
"map (foldl1 f ∘ map h) (candidate (@) (map wrap [0..<n+1]))
= candidate f (map (foldl1 f ∘ map h) (map wrap [0..<n+1]))"
by auto
also have
"… = candidate f (map (foldl1 f ∘ map h ∘ wrap) [0..<n+1])"
also have
"… = candidate f (map (foldl1 f ∘ wrap ∘ h) [0..<n+1])"
using L4 by (simp add: Fun.o_def)
also have
"… = candidate f (map h [0..<n+1])"
finally show ?thesis .
qed

section ‹Proving Proposition 1›

subsection ‹Definitions of Lemma 4›

text ‹
In the same way as in the original paper, the following two functions are
defined:
›

fun f1 :: "three ⇒ three ⇒ three"
where
"f1 x    Zero = x"
| "f1 Zero One  = One"
| "f1 x    y    = Two"

fun f2 :: "three ⇒ three ⇒ three"
where
"f2 x Zero = x"
| "f2 x One  = One"
| "f2 x Two  = Two"

text ‹
Both functions are associative as is proved by case analysis:
›

lemma f1_assoc: "associative f1"
unfolding associative_def proof auto
fix x y z
show "f1 x (f1 y z) = f1 (f1 x y) z"
proof (cases z)
case Zero thus ?thesis by simp
next
case One
hence z_One: "z = One" by simp
thus ?thesis by (cases y, simp_all, cases x, simp_all)
next
case Two thus ?thesis by simp
qed
qed

lemma f2_assoc: "associative f2"
unfolding associative_def proof auto
fix x y z
show "f2 x (f2 y z) = f2 (f2 x y) z" by (cases z, auto)
qed

text ‹
Next, we define two other functions, again according to the original paper.
Note that ‹h1› has an extra parameter ‹k› which is only implicit in
the original paper.
›

fun h1 :: "nat ⇒ nat ⇒ nat ⇒ three"
where
"h1 k i j = (if i = j then One
else if j ≤ k then Zero
else Two)"

fun h2 :: "nat ⇒ nat ⇒ three"
where
"h2 i j = (if i = j then One
else if i + 1 = j then Two
else Zero)"

subsection ‹Figures and Proofs›

text ‹
In the original paper, this lemma is depicted in (and proved by) Figure~2.
Therefore, it carries this unusual name here.
›

lemma Figure_2:
assumes "i ≤ k"
shows "foldl1 f1 (map (h1 k i) [0..<k + 1]) = One"
proof -
let ?mr = "replicate i Zero @ [One] @ replicate (k - i) Zero"

have P1: "map (h1 k i) [0..<k + 1] = ?mr"
proof -
have Q1: "length (map (h1 k i) [0..<k + 1]) = length ?mr"
using assms by simp

have Q2: "⋀j. j < length (map (h1 k i) [0..<k + 1])
⟹ (map (h1 k i) [0..<k + 1]) ! j = ?mr ! j"
proof -
fix j
assume "j < length (map (h1 k i) [0..<k + 1])"
hence j_k: "j < k + 1" by simp
have M1: "(map (h1 k i) [0..<k + 1]) ! i = One"
using L6 [where f="h1 k i" and xs="[0..<k + 1]"] and assms
and List.nth_upt [where i=0 and k=i and j="k + 1"] by simp
have M2: "j ≠ i ⟹ (map (h1 k i) [0..<k + 1]) ! j = Zero"
using L6 [where f="h1 k i" and xs="[0..<k + 1]"] and j_k
and List.nth_upt [where i=0 and j="k + 1"] by simp
have R1: "?mr ! i = One"
using List.nth_append [where xs="replicate i Zero"] by simp
have R2: "j < i ⟹ ?mr ! j = Zero"
using List.nth_append [where xs="replicate i Zero"] by simp
have R3: "j > i ⟹ ?mr ! j = Zero"
using List.nth_append [where xs="replicate i Zero @ [One]"]
and j_k by simp

show "(map (h1 k i) [0..<k + 1]) ! j = ?mr ! j"
proof (cases "i = j")
assume "i = j"
with M1 and R1 show ?thesis by simp
next
assume i_ne_j: "i ≠ j"
thus ?thesis
proof (cases "i < j")
assume "i < j"
with M2 and R3 show ?thesis by simp
next
assume "¬(i < j)"
with i_ne_j have "i > j" by simp
with M2 and R2 show ?thesis by simp
qed
qed
qed

from Q1 Q2 and Lemma_2 show ?thesis by blast
qed

have P2: "⋀j. j > 0 ⟹ foldl1 f1 (replicate j Zero) = Zero"
proof -
fix j
assume "(j::nat) > 0"
thus "foldl1 f1 (replicate j Zero) = Zero"
proof (induct j)
case 0 thus ?case by simp
next
case (Suc j) thus ?case by (cases j, auto)
qed
qed

have P3: "⋀j. foldl1 f1 ([One] @ replicate j Zero) = One"
proof -
fix j
show "foldl1 f1 ([One] @ replicate j Zero) = One"
using L8 [where f=f1 and xs="[One]" and ys="replicate (Suc j) Zero"]
and f1_assoc and P2 [where j="Suc j"] by simp
qed

have "foldl1 f1 ?mr = One"
proof (cases i)
case 0
thus ?thesis using P3 by simp
next
case (Suc i)
hence
"foldl1 f1 (replicate (Suc i) Zero @ [One] @ replicate (k - Suc i) Zero)
= f1 (foldl1 f1 (replicate (Suc i) Zero))
(foldl1 f1 ([One] @ replicate (k - Suc i) Zero))"
using L8 [where xs="replicate (Suc i) Zero"
and ys="[One] @ replicate (k - Suc i) Zero"]
and f1_assoc by simp
also have
"… = One"
using P2 [where j="Suc i"] and P3 [where j="k - Suc i"] by simp
finally show ?thesis using Suc by simp
qed
with P1 show ?thesis by simp
qed

text ‹
In the original paper, this lemma is depicted in (and proved by) Figure~3.
Therefore, it carries this unusual name here.
›

lemma Figure_3:
assumes "i < k"
shows "foldl1 f2 (map (h2 i) [0..<k + 1]) = Two"
proof -
let ?mr = "replicate i Zero @ [One, Two] @ replicate (k - i - 1) Zero"

have P1: "map (h2 i) [0..<k + 1] = ?mr"
proof -
have Q1: "length (map (h2 i) [0..<k + 1]) = length ?mr"
using assms by simp

have Q2: "⋀j. j < length (map (h2 i) [0..<k + 1])
⟹ (map (h2 i) [0..<k + 1]) ! j = ?mr ! j"
proof -
fix j
assume "j < length (map (h2 i) [0..<k + 1])"
hence j_k: "j < k + 1" by simp
have M1: "(map (h2 i) [0..<k + 1]) ! i = One"
using L6 [where xs="[0..<k + 1]" and f="h2 i" and k=i] and assms
and List.nth_upt [where i=0 and k=i and j="k + 1"] by simp
have M2: "(map (h2 i) [0..<k + 1]) ! (i + 1) = Two"
using L6 [where xs="[0..<k + 1]" and f="h2 i" and k="i + 1"]
and assms and List.nth_upt [where i=0 and k="i + 1" and j="k + 1"]
by simp
have M3: "j < i ∨ j > i + 1 ⟹ (map (h2 i) [0..<k + 1]) ! j = Zero"
using L6 [where xs="[0..<k + 1]" and f="h2 i" and k=j]
and assms and List.nth_upt [where i=0 and k=j and j="k + 1"]
and j_k by auto
have R1: "j < i ⟹ ?mr ! j = Zero"
using List.nth_append [where xs="replicate i Zero"] by simp
have R2: "?mr ! i = One"
using List.nth_append [where xs="replicate i Zero"] by simp
have R3: "?mr ! (i + 1) = Two"
using List.nth_append [where xs="replicate i Zero @ [One]"] by simp
have R4: "j > i + 1 ⟹ ?mr ! j = Zero"
using List.nth_append [where xs="replicate i Zero @ [One,Two]"]
and j_k by simp
show "(map (h2 i) [0..<k + 1]) ! j = ?mr ! j"
proof (cases "j < i")
assume "j < i" with M3 and R1 show ?thesis by simp
next
assume "¬(j < i)"
hence j_ge_i: "j ≥ i" by simp
thus ?thesis
proof (cases "j = i")
assume "j = i" with M1 and R2 show ?thesis by simp
next
assume "¬(j = i)"
with j_ge_i have j_gt_i: "j > i" by simp
thus ?thesis
proof (cases "j = i + 1")
assume "j = i + 1" with M2 and R3 show ?thesis by simp
next
assume "¬(j = i + 1)"
with j_gt_i have "j > i + 1" by simp
with M3 and R4 show ?thesis by simp
qed
qed
qed
qed
from Q1 Q2 and Lemma_2 show ?thesis by blast
qed

have P2: "⋀j. j > 0 ⟹ foldl1 f2 (replicate j Zero) = Zero"
proof -
fix j
assume j_0: "(j::nat) > 0"
show "foldl1 f2 (replicate j Zero) = Zero"
using j_0 proof (induct j)
case 0 thus ?case by simp
next
case (Suc j) thus ?case by (cases j, auto)
qed
qed

have P3: "⋀j. foldl1 f2 ([One, Two] @ replicate j Zero) = Two"
proof -
fix j
show "foldl1 f2 ([One, Two] @ replicate j Zero) = Two"
using L8 [where f=f2 and xs="[One,Two]"
and ys="replicate (Suc j) Zero"] and f2_assoc and P2 [where j="Suc j"]
by simp
qed

have "foldl1 f2 ?mr = Two"
proof (cases i)
case 0 thus ?thesis using P3 by simp
next
case (Suc i)
hence
"foldl1 f2 (replicate (Suc i) Zero @ [One, Two]
@ replicate (k - Suc i - 1) Zero)
= f2 (foldl1 f2 (replicate (Suc i) Zero))
(foldl1 f2 ([One, Two] @  replicate (k - Suc i - 1) Zero))"
using L8 [where f=f2 and xs="replicate (Suc i) Zero"
and ys="[One, Two] @ replicate (k - Suc i - 1) Zero"]
and f2_assoc by simp
also have
"… = Two"
using P2 [where j="Suc i"] and P3 [where j="k - Suc i - 1"] by simp
finally show ?thesis using Suc by simp
qed
with P1 show ?thesis by simp
qed

text ‹
Counterparts of the following two lemmas are shown in the proof of Lemma 4 in
the original paper. Since here, the proof of Lemma 4 is seperated in several
smaller lemmas, also these two properties are given separately.
›

lemma L9:
assumes "⋀ (f :: three ⇒ three ⇒ three) h. associative f
⟹ foldl1 f (map h js) = foldl1 f (map h [0..<k + 1])"
and "i ≤ k"
shows "foldl1 f1 (map (h1 k i) js) = One"
using assms and f1_assoc and Figure_2 by auto

lemma L10:
assumes "⋀ (f :: three ⇒ three ⇒ three) h. associative f
⟹ foldl1 f (map h js) = foldl1 f (map h [0..<k + 1])"
and "i < k"
shows "foldl1 f2 (map (h2 i) js) = Two"
using assms and f2_assoc and Figure_3 by auto

text ‹
In the original paper, this lemma is depicted in (and proved by) Figure~4.
Therefore, it carries this unusual name here. This lemma expresses that every
‹i ≤ k› is contained in ‹js› at least once.
›

lemma Figure_4:
assumes "foldl1 f1 (map (h1 k i) js) = One"
and "js ≠ []"
shows "i ∈ set js"
proof (rule ccontr)
assume i_not_in_js: "i ∉ set js"

have One_not_in_map_js: "One ∉ set (map (h1 k i) js)"
proof
assume "One ∈ set (map (h1 k i) js)"
hence "One ∈ (h1 k i)  (set js)" by simp
then obtain j where j_def: "j ∈ set js ∧ One = h1 k i j"
using Set.image_iff [where f="h1 k i"] by auto
hence "i = j" by (simp split: if_splits)
with i_not_in_js and j_def show False by simp
qed

have f1_One: "⋀x y. x ≠ One ∧ y ≠ One ⟹ f1 x y ≠ One"
proof -
fix x y
assume "x ≠ One ∧ y ≠ One"
thus "f1 x y ≠ One" by (cases y, cases x, auto)
qed

have "⋀xs. ⟦ xs ≠ [] ; One ∉ set xs ⟧ ⟹ foldl1 f1 xs ≠ One"
proof -
fix xs
assume A: "(xs :: three list) ≠ []"
thus "One ∉ set xs ⟹ foldl1 f1 xs ≠ One"
proof (induct xs rule: divide_and_conquer)
case Nil thus ?case by simp
next
case (One x)
thus "foldl1 f1 [x] ≠ One" by simp
next
case (Partition xs ys)
hence "One ∉ set xs ∧ One ∉ set ys" by simp
with Partition have "foldl1 f1 xs ≠ One ∧ foldl1 f1 ys ≠ One" by simp
with f1_One have "f1 (foldl1 f1 xs) (foldl1 f1 ys) ≠ One" by simp
with L8 [symmetric, where f=f1] and f1_assoc and Partition
show "foldl1 f1 (xs @ ys) ≠ One" by auto
qed
qed
with One_not_in_map_js and assms show False by auto
qed

text ‹
In the original paper, this lemma is depicted in (and proved by) Figure~5.
Therefore, it carries this unusual name here. This lemma expresses that every
‹i ≤ k› is contained in ‹js› at most once.
›

lemma Figure_5:
assumes "foldl1 f1 (map (h1 k i) js) = One"
and "js = xs @ ys"
shows "¬(i ∈ set xs ∧ i ∈ set ys)"
proof (rule ccontr)
assume "¬¬(i ∈ set xs ∧ i ∈ set ys)"
hence i_xs_ys: "i ∈ set xs ∧ i ∈ set ys" by simp

from i_xs_ys have xs_not_empty: "xs ≠ []" by auto
from i_xs_ys have ys_not_empty: "ys ≠ []" by auto

have f1_Zero: "⋀x y. x ≠ Zero ∨ y ≠ Zero ⟹ f1 x y ≠ Zero"
proof -
fix x y
show "x ≠ Zero ∨ y ≠ Zero ⟹ f1 x y ≠ Zero"
by (cases y, simp_all, cases x, simp_all)
qed

have One_foldl1: "⋀xs. One ∈ set xs ⟹ foldl1 f1 xs ≠ Zero"
proof -
fix xs
assume One_xs: "One ∈ set xs"
thus "foldl1 f1 xs ≠ Zero"
proof (induct xs rule: divide_and_conquer)
case Nil thus ?case by simp
next
case One thus ?case by simp
next
case (Partition xs ys)
hence "One ∈ set xs ∨ One ∈ set ys" by simp
with Partition have "foldl1 f1 xs ≠ Zero ∨ foldl1 f1 ys ≠ Zero" by auto
with f1_Zero have "f1 (foldl1 f1 xs) (foldl1 f1 ys) ≠ Zero" by simp
thus ?case using L8 [symmetric, where f=f1] and f1_assoc and Partition
by auto
qed
qed

have f1_Two: "⋀x y. x ≠ Zero ∧ y ≠ Zero ⟹ f1 x y = Two"
proof -
fix x y
show "x ≠ Zero ∧ y ≠ Zero ⟹ f1 x y = Two"
by (cases y, simp_all, cases x, simp_all)
qed

from i_xs_ys
have "One ∈ set (map (h1 k i) xs) ∧ One ∈ set (map (h1 k i) ys)" by simp
hence "foldl1 f1 (map (h1 k i) xs) ≠ Zero
∧ foldl1 f1 (map (h1 k i) ys) ≠ Zero"
using One_foldl1 by simp
hence "f1 (foldl1 f1 (map (h1 k i) xs)) (foldl1 f1 (map (h1 k i) ys)) = Two"
using f1_Two by simp
hence "foldl1 f1 (map (h1 k i) (xs @ ys)) = Two"
using foldl1_map [symmetric, where h="h1 k i"] and f1_assoc
and xs_not_empty and ys_not_empty by auto
with assms show False by simp
qed

text ‹
In the original paper, this lemma is depicted in (and proved by) Figure~6.
Therefore, it carries this unusual name here. This lemma expresses that
‹js› contains only elements of ‹[0..<k + 1]›.
›

lemma Figure_6:
assumes "⋀i. i ≤ k ⟹ foldl1 f1 (map (h1 k i) js) = One"
and "i > k"
shows "i ∉ set js"
proof
assume i_in_js: "i ∈ set js"

have Two_map: "Two ∈ set (map (h1 k 0) js)"
proof -
have "Two = h1 k 0 i" using assms by simp
with i_in_js show ?thesis using IntI by (auto split: if_splits)
qed

have f1_Two: "⋀x y. x = Two ∨ y = Two ⟹ f1 x y = Two"
proof -
fix x y
show "x = Two ∨ y = Two ⟹ f1 x y = Two" by (cases y, auto)
qed

have "⋀xs. Two ∈ set xs ⟹ foldl1 f1 xs = Two"
proof -
fix xs
assume Two_xs: "Two ∈ set xs"
thus "foldl1 f1 xs = Two" using Two_xs
proof (induct xs rule: divide_and_conquer)
case Nil thus ?case by simp
next
case One thus ?case by simp
next
case (Partition xs ys)
hence "Two ∈ set xs ∨ Two ∈ set ys" by simp
hence "foldl1 f1 xs = Two ∨ foldl1 f1 ys = Two" using Partition by auto
with f1_Two have "f1 (foldl1 f1 xs) (foldl1 f1 ys) = Two" by simp
thus "foldl1 f1 (xs @ ys) = Two"
using L8 [symmetric, where f=f1] and f1_assoc and Partition by auto
qed
qed

with Two_map have "foldl1 f1 (map (h1 k 0) js) = Two" by simp
with assms show False by auto
qed

text ‹
In the original paper, this lemma is depicted in (and proved by) Figure~7.
Therefore, it carries this unusual name here. This lemma expresses that every
‹i ≤ k› in ‹js› is eventually followed by ‹i + 1›.
›

lemma Figure_7:
assumes "foldl1 f2 (map (h2 i) js) = Two"
and "js = xs @ ys"
and "xs ≠ []"
and "i = last xs"
shows "(i + 1) ∈ set ys"
proof (rule ccontr)
assume Suc_i_not_in_ys: "(i + 1) ∉ set ys"

have last_map_One: "last (map (h2 i) xs) = One"
proof -
have
"last (map (h2 i) xs)
= (map (h2 i) xs) ! (length (map (h2 i) xs) - 1)"
using List.last_conv_nth [where xs="map (h2 i) xs"] and assms by simp
also have
"… = (map (h2 i) xs) ! (length xs - 1)" using L2 by simp
also have
"… = h2 i (xs ! (length xs - 1))"
using L6 and assms by simp
also have
"… = h2 i (last xs)"
using List.last_conv_nth [symmetric,where xs=xs] and assms by simp
also have
"… = One" using assms by simp
finally show ?thesis .
qed

have "⋀xs. ⟦  xs ≠ [] ; last xs = One ⟧ ⟹ foldl1 f2 xs = One"
proof -
fix xs
assume last_xs_One: "last xs = One"
assume xs_not_empty: "xs ≠ []"
hence xs_partition: "xs = butlast xs @ [last xs]" by simp
show "foldl1 f2 xs = One"
proof (cases "butlast xs")
case Nil with xs_partition and last_xs_One show ?thesis by simp
next
case Cons
hence butlast_not_empty: "butlast xs ≠ []" by simp

have
"foldl1 f2 xs = foldl1 f2 (butlast xs @ [last xs])"
using xs_partition by simp
also have
"… = f2 (foldl1 f2 (butlast xs)) (foldl1 f2 [last xs])"
using L8 [where f=f2] and f2_assoc and butlast_not_empty by simp
also have
"… = One" using last_xs_One by simp
finally show ?thesis .
qed
qed
with last_map_One have foldl1_map_xs: "foldl1 f2 (map (h2 i) xs) = One"
using assms by simp

have ys_not_empty: "ys ≠ []" using foldl1_map_xs and assms by auto

have Two_map_ys: "Two ∉ set (map (h2 i) ys)"
proof
assume "Two ∈ set (map (h2 i) ys)"
hence "Two ∈ (h2 i)  (set ys)" by simp
then obtain j where j_def: "j ∈ set ys ∧ Two = h2 i j"
using Set.image_iff [where f="h2 i"] by auto
hence "i + 1 = j" by (simp split: if_splits)
with Suc_i_not_in_ys and j_def show False by simp
qed

have f2_One: "⋀x y. x ≠ Two ∧ y ≠ Two ⟹ f2 x y ≠ Two"
proof -
fix x y
show "x ≠ Two ∧ y ≠ Two ⟹ f2 x y ≠ Two" by (cases y, auto)
qed

have "⋀xs. ⟦ xs ≠ [] ; Two ∉ set xs ⟧ ⟹ foldl1 f2 xs ≠ Two"
proof -
fix xs
assume xs_not_empty: "(xs :: three list) ≠ []"
thus "Two ∉ set xs ⟹ foldl1 f2 xs ≠ Two"
proof (induct xs rule: divide_and_conquer)
case Nil thus ?case by simp
next
case One thus ?case by simp
next
case (Partition xs ys)
hence "Two ∉ set xs ∧ Two ∉ set ys" by simp
hence "foldl1 f2 xs ≠ Two ∧ foldl1 f2 ys ≠ Two" using Partition by simp
hence "f2 (foldl1 f2 xs) (foldl1 f2 ys) ≠ Two" using f2_One by simp
thus "foldl1 f2 (xs @ ys) ≠ Two"
using L8 [symmetric, where f=f2] and f2_assoc and Partition by simp
qed
qed
with Two_map_ys have foldl1_map_ys: "foldl1 f2 (map (h2 i) ys) ≠ Two"
using ys_not_empty by simp

from f2_One
have "f2 (foldl1 f2 (map (h2 i) xs)) (foldl1 f2 (map (h2 i) ys)) ≠ Two"
using foldl1_map_xs and foldl1_map_ys by simp
hence "foldl1 f2 (map (h2 i) (xs @ ys)) ≠ Two"
using foldl1_map [symmetric, where h="h2 i" and f=f2] and f2_assoc
and assms and ys_not_empty by simp
with assms show False by simp
qed

subsection ‹Permutations and Lemma 4›

text ‹
In the original paper, the argumentation goes as follows:
From ‹Figure_4› and ‹Figure_5› we can show that ‹js›
contains every ‹i ≤ k› exactly once, and from ‹Figure_6› we can
furthermore show that ‹js› contains no other elements. Thus, ‹js›
must be a permutation of ‹[0..<k + 1]›.

Here, however, the argumentation is different, because we want to use already
existing results. Therefore, we show first, that the sets of ‹js› and
‹[0..<k + 1]› are equal using the results of ‹Figure_4› and
‹Figure_6›. Second, we show that ‹js› is a distinct list, i.e. no
element occurs twice in ‹js›. Since also ‹[0..<k + 1]› is
distinct, the multisets of ‹js› and ‹[0..<k + 1]› are equal,
and therefore, both lists are permutations.
›

lemma js_is_a_permutation:
assumes A1: "⋀ (f :: three ⇒ three ⇒ three) h. associative f
⟹ foldl1 f (map h js) = foldl1 f (map h [0..<k + 1])"
and A2: "js ≠ []"
shows "mset js = mset [0..<k + 1]"
proof -
from A1 and L9 have L9':
"⋀i. i ≤ k ⟹ foldl1 f1 (map (h1 k i) js) = One" by auto

from L9' and Figure_4 and A2 have P1: "⋀i. i ≤ k ⟹ i ∈ set js" by auto
from L9' and Figure_5 have P2:
"⋀i xs ys. ⟦ i ≤ k ; js = xs @ ys ⟧ ⟹ ¬(i ∈ set xs ∧ i ∈ set ys)" by blast
from L9' and Figure_6 have P3: "⋀i. i > k ⟹ i ∉ set js" by auto

have set_eq: "set [0..<k + 1] = set js"
proof
from P1 show "set [0..<k + 1] ⊆ set js" by auto
next
show "set js ⊆ set [0..<k + 1]"
proof
fix j
assume "j ∈ set js"
hence "¬(j ∉ set js)" by simp
with P3 have "¬(j > k)" using HOL.contrapos_nn by auto
hence "j ≤ k" by simp
thus "j ∈ set [0..<k + 1]" by auto
qed
qed

have "⋀xs ys. js = xs @ ys ⟹ set xs ∩ set ys = {}"
proof -
fix xs ys
assume js_xs_ys: "js = xs @ ys"
with set_eq have i_xs_ys: "⋀i. i ∈ set xs ∨ i ∈ set ys ⟹ i ≤ k" by auto
have "⋀i. i ≤ k ⟹ (i ∈ set xs) = (i ∉ set ys)"
proof
fix i
assume "i ∈ set xs"
moreover assume "i ≤ k"
ultimately show "i ∉ set ys" using js_xs_ys and P2 by simp
next
fix i
assume "i ∉ set ys"
moreover assume "i ≤ k"
ultimately show "i ∈ set xs" using js_xs_ys and P2 and P1 by auto
qed
thus "set xs ∩ set ys = {}" using i_xs_ys by auto
qed
with all_set_inter_empty_distinct have "distinct js" using A2 by auto
with set_eq show "mset js = mset [0..<k + 1]"
using Multiset.set_eq_iff_mset_eq_distinct
[where x=js and y="[0..<k + 1]"] by simp
qed

text ‹
The result of ‹Figure_7› is too specific. Instead of having that every
‹i› is eventually followed by ‹i + 1›, it more useful to know
that every ‹i› is followed by all ‹i + r›, where
‹r > 0›. This result follows easily by induction from
‹Figure_7›.
›

lemma Figure_7_trans:
assumes A1: "⋀i xs ys. ⟦ i < k ; js = xs @ ys ; xs ≠ [] ; i = last xs ⟧
⟹ (i + 1) ∈ set ys"
and A2: "(r::nat) > 0"
and A3: "i + r ≤ k"
and A4: "js = xs @ ys"
and A5: "xs ≠ []"
and A6: "i = last xs"
shows "(i + r) ∈ set ys"
using A2 A3 proof (induct r)
case 0 thus ?case by simp
next
case (Suc r)
hence IH: "0 < r ⟹ (i + r) ∈ set ys" by simp
from Suc have i_r_k: "i + Suc r ≤ k" by simp
show ?case
proof (cases r)
case 0 thus ?thesis using A1 and i_r_k and A4 and A5 and A6 by auto
next
case Suc
with IH have "(i + r) ∈ set ys" by simp
then obtain p where p_def: "p < length ys ∧ ys ! p = i + r"
using List.in_set_conv_nth [where x="i + r"] by auto

let ?xs = "xs @ take (p + 1) ys"
let ?ys = "drop (p + 1) ys"

have "i + r < k" using i_r_k by simp
moreover have "js = ?xs @ ?ys" using A4 by simp
moreover have "?xs ≠ []" using A5 by simp
moreover have "i + r = last ?xs"
using p_def and List.take_Suc_conv_app_nth [where i=p and xs=ys] by simp
ultimately have "(i + Suc r) ∈ set ?ys" using A1 [where i="i + r"] by auto
thus "(i + Suc r) ∈ set ys"
using List.set_drop_subset [where xs=ys] by auto
qed
qed

text ‹
Since we want to use Lemma ‹partitions_sorted› to show that ‹js›
is sorted, we need yet another result which can be obtained using the
previous lemma and some further argumentation:
›

lemma js_partition_order:
assumes A1: "mset js = mset [0..<k + 1]"
and A2: "⋀i xs ys. ⟦ i < k ; js = xs @ ys ; xs ≠ [] ; i = last xs ⟧
⟹ (i + 1) ∈ set ys"
and A3: "js = xs @ ys"
and A4: "i ∈ set xs"
and A5: "j ∈ set ys"
shows "i ≤ j"
proof (rule ccontr)
from A1 have A1': ‹set js = {..<k + 1}›
by (metis atLeast_upt mset_eq_setD)
assume "¬(i ≤ j)"
hence i_j: "i > j" by simp

from A5 obtain pj where pj_def: "pj < length ys ∧ ys ! pj = j"
using List.in_set_conv_nth [where x=j] by auto

let ?xs = "xs @ take (pj + 1) ys"
let ?ys = "drop (pj + 1) ys"

let ?r = "i - j"

from A1 and A3 have "distinct (xs @ ys)"
using distinct_upt mset_eq_imp_distinct_iff by blast

hence xs_ys_inter_empty: "set xs ∩ set ys = {}" by simp

from A2 and Figure_7_trans have
"⋀i r xs ys. ⟦ r > 0 ; i + r ≤ k ; js = xs @ ys ; xs ≠ [] ; i = last xs ⟧
⟹ (i + r) ∈ set ys" by blast
moreover from i_j have "?r > 0" by simp
moreover have "j + ?r ≤ k"
proof -
have "i ∈ set js" using A4 and A3 by simp
hence "i ∈ set [0..<k + 1]"
using A1' by (auto simp add: less_Suc_eq)
hence "i ≤ k" by auto
thus ?thesis using i_j by simp
qed
moreover have "js = ?xs @ ?ys" using A3 by simp
moreover have "?xs ≠ []" using A4 by auto
moreover have "j = last (?xs)"
using pj_def and List.take_Suc_conv_app_nth [where i=pj and xs=ys] by simp
ultimately have "(j + ?r) ∈ set ?ys" by blast
hence "i ∈ set ys" using i_j and List.set_drop_subset [where xs=ys] by auto
with A4 and xs_ys_inter_empty show False by auto
qed

text ‹
With the help of the previous lemma, we show now that ‹js› equals
‹[0..<k + 1]›, if both lists are permutations and every ‹i› is
eventually followed by ‹i + 1› in ‹js›.
›

lemma js_equals_upt_k:
assumes A1: "mset js = mset [0..<k + 1]"
and A2: "⋀i xs ys. ⟦ i < k ; js = xs @ ys ; xs ≠ [] ; i = last xs ⟧
⟹ (i + 1) ∈ set ys"
shows "js = [0..<k + 1]"
proof -
from A1 and A2 and js_partition_order
have "⋀xs ys x y. ⟦ js = xs @ ys ; x ∈ set xs ; y ∈ set ys ⟧ ⟹ x ≤ y"
by blast
hence "sorted js" using partitions_sorted by blast
moreover have "distinct js"
using A1 distinct_upt mset_eq_imp_distinct_iff by blast
moreover have "sorted [0..<k + 1]"
using List.sorted_upt by blast
moreover have "distinct [0..<k + 1]" by simp
moreover have "set js = set [0..<k + 1]"
using A1 mset_eq_setD by blast
ultimately show "js = [0..<k + 1]" using List.sorted_distinct_set_unique
by blast
qed

text ‹
From all the work done before, we conclude now Lemma 4:
›

lemma Lemma_4:
assumes "⋀(f :: three ⇒ three ⇒ three) h. associative f
⟹ foldl1 f (map h js) = foldl1 f (map h [0..<k + 1])"
and "js ≠ []"
shows "js = [0..<k + 1]"
proof -
from assms and js_is_a_permutation have "mset js = mset[0..<k + 1]" by auto
moreover
from assms and L10 and Figure_7
have "⋀i xs ys. ⟦ i < k ; js = xs @ ys ; xs ≠ [] ; i = last xs ⟧
⟹ (i + 1) ∈ set ys" by blast
ultimately show ?thesis using js_equals_upt_k by auto
qed

subsection ‹Lemma 5›

text ‹
This lemma is a lifting of Lemma 4 to the overall computation of
‹scanl1›. Its proof follows closely the one given in the original paper.
›

lemma Lemma_5:
assumes "⋀(f :: three ⇒ three ⇒ three) h. associative f
⟹ map (foldl1 f ∘ map h) jss = scanl1 f (map h [0..<n + 1])"
and "⋀js. js ∈ set jss ⟹ js ≠ []"
shows "jss = ups n"
proof -
have P1: "length jss = length (ups n)"
proof -
obtain f :: "three ⇒ three ⇒ three" where f_assoc: "associative f"
using f1_assoc by auto

fix h
have
"length jss = length (map (foldl1 f ∘ map h) jss)" by (simp add: L2)
also have
"… = length (scanl1 f (map h [0..<n + 1]))"
using assms and f_assoc by simp
also have
"… = length (map (λk. foldl1 f (take (k + 1) (map h [0..<n + 1])))
[0..<length (map h [0..<n + 1])])" by simp
also have
"… = length [0..<length (map h [0..<n + 1])]" by (simp add: L2)
also have
"… = length [0..<length [0..<n + 1]]" by (simp add: L2)
also have
"… = length [0..<n + 1]" by simp
also have
"… = length (map (λk. [0..<k + 1]) [0..<n + 1])" by (simp add: L2)
also have
"… = length (ups n)" by simp
finally show ?thesis .
qed

have P2: "⋀k. k < length jss ⟹ jss ! k = (ups n) ! k"
proof -
fix k
assume k_length_jss: "k < length jss"
hence non_empty_jss_k: "jss ! k ≠ []" using assms by simp

from k_length_jss
have k_length_length: "k < length [1..<length [0..<n + 1] + 1]"
using P1 by simp
hence k_length: "k < length [0..<n + 1]"
using List.length_upt [where i=1 and j="length [0..<n + 1] + 1"]
by simp

have "⋀(f :: three ⇒ three ⇒ three) h. associative f
⟹ foldl1 f (map h (jss ! k)) = foldl1 f (map h [0..<k + 1])"
proof -
fix f h
assume f_assoc: "associative (f :: three ⇒ three ⇒ three)"
have
"foldl1 f (map h (jss ! k))
= (map (foldl1 f ∘ map h) jss) ! k"
using L6 and k_length_jss by auto
also have
"… = (scanl1 f (map h [0..<n + 1])) ! k"
using assms and f_assoc by simp
also have
"… = (map (λk. foldl1 f (take k (map h [0..<n + 1])))
[1..<length (map h [0..<n + 1]) + 1]) ! k" by simp
also have
"… = (map (λk. foldl1 f (take k (map h [0..<n + 1])))
[1..<length [0..<n + 1] + 1]) ! k"
also have
"… = (λk. foldl1 f (take k (map h [0..<n + 1])))
([1..<length [0..<n + 1] + 1] ! k)"
using L6 [where xs="[1..<length [0..<n + 1] + 1]"
and f="(λk. foldl1 f (take k (map h [0..<n + 1])))"]
and k_length_length by auto
also have
"… = foldl1 f (take (k + 1) (map h [0..<n + 1]))"
proof -
have "[1..<length [0..<n + 1] + 1] ! k  = k + 1"
using List.nth_upt [where i=1 and j="length [0..<n + 1] + 1"]
and k_length by simp
thus ?thesis by simp
qed
also have
"… = foldl1 f (map h (take (k + 1) [0..<n + 1]))"
using L3 [where k="k + 1" and xs="[0..<n + 1]" and f=h] by simp
also have "… = foldl1 f (map h [0..<k + 1])"
using List.take_upt [where i=0 and m="k + 1" and n="n + 1"]
and k_length by simp
finally show
"foldl1 f (map h (jss ! k)) = foldl1 f (map h [0..<k + 1])" .
qed
with Lemma_4 and non_empty_jss_k have P3: "jss ! k = [0..<k + 1]"
by blast

have
"(ups n) ! k
= (map (λk. [0..<k + 1]) [0..<n + 1]) ! k" by simp
also have
"… = (λk. [0..<k + 1]) ([0..<n + 1] ! k)"
using L6 [where xs="[0..<n + 1]"] and k_length by auto
also have
"… = [0..<k + 1]"
using List.nth_upt [where i=0 and j="n + 1"] and k_length by simp
finally have "(ups n) ! k = [0..<k + 1]" .

with P3 show "jss ! k = (ups n) ! k" by simp
qed

from P1 P2 and Lemma_2 show "jss = ups n" by blast
qed

subsection ‹Proposition 1›

text ‹
In the original paper, only non-empty lists where considered, whereas here,
the used list datatype allows also for empty lists. Therefore, we need to
exclude non-empty lists to have a similar setting as in the original paper.

In the case of Proposition 1, we need to show that every list contained in
the result of ‹candidate (@) (map wrap [0..<n + 1])› is non-empty.
The idea is to interpret empty lists by the value ‹Zero› and non-empty
lists by the value ‹One›, and to apply the assumptions.
›

lemma non_empty_candidate_results:
assumes "⋀ (f :: three ⇒ three ⇒ three) (xs :: three list).
⟦ associative f ; xs ≠ [] ⟧  ⟹ candidate f xs = scanl1 f xs"
and "js ∈ set (candidate (@) (map wrap [0..<n + 1]))"
shows   "js ≠ []"
proof -
― ‹We define a mapping of lists to values of @{text three} as explained›
― ‹above, and a function which behaves like @{text @} on values of›
― ‹@{text three}.›
let ?h = "λxs. case xs of [] ⇒ Zero | (_#_) ⇒ One"
let ?g = "λx y. if (x = One ∨ y = One) then One else Zero"
have g_assoc: "associative ?g" unfolding associative_def by auto

― ‹Our defined functions fulfill the requirements of the free theorem of›
― ‹@{text candidate}, that is:›
have req_free_theorem: "⋀xs ys. ?h (xs @ ys) = ?g (?h xs) (?h ys)"
proof -
fix xs ys
show "?h (xs @ ys) = ?g (?h xs) (?h ys)"
by (cases xs, simp_all, cases ys, simp_all)
qed

― ‹Before applying the assumptions, we show that @{text candidate}'s›
― ‹counterpart @{text scanl1}, applied to a non-empty list, returns only›
― ‹a repetition of the value @{text One}.›
have set_scanl1_is_One:
"set (scanl1 ?g (map ?h (map wrap [0..<n + 1]))) = {One}"
proof -
have const_One: "map (λx. One) [0..<n + 1] = replicate (n + 1) One"
proof (induct n)
case 0 thus ?case by simp
next
case (Suc n)
have
"map (λx. One) [0..<Suc n + 1]
= map (λx. One) ([0..<Suc n] @ [Suc n])" by simp
also have
"… = map (λx. One) [0..<Suc n] @ map (λx. One) [Suc n]"
by simp
also have "… = replicate (Suc n) One @ replicate 1 One"
using Suc by simp
also have "… = replicate (Suc n + 1) One"
[symmetric, where x=One and n="Suc n" and m=1]
by simp
finally show ?case .
qed

have foldl1_One: "⋀xs. foldl1 ?g (One # xs) = One"
proof -
fix xs
show "foldl1 ?g (One # xs) = One"
proof (induct xs rule: measure_induct [where f=length])
fix x
assume "∀y. length y < length (x::three list)
⟶ foldl1 ?g (One # y) = One"
thus "foldl1 ?g (One # x) = One" by (cases x, auto)
qed
qed

have
"scanl1 ?g (map ?h (map wrap [0..<n + 1]))
= scanl1 ?g (map (?h ∘ wrap) [0..<n + 1])"
using L1 [where g="?h" and f=wrap and xs="[0..<n + 1]"] by simp
also have
"… = scanl1 ?g (map (λx. One) [0..<n + 1])" by (simp add: Fun.o_def)
also have
"… = scanl1 ?g (replicate (n + 1) One)" using const_One by auto
also have
"… = map (λk. foldl1 ?g (take k (replicate (n + 1) One)))
[1..<length (replicate (n + 1) One) + 1]" by simp
also have
"… = map (λk. foldl1 ?g (take k (replicate (n + 1) One)))
(map Suc [0..<length (replicate (n + 1) One)])"
using List.map_Suc_upt by simp
also have
"… = map ((λk. foldl1 ?g (take k (replicate (n + 1) One))) ∘ Suc)
[0..<length (replicate (n + 1) One)]"
using L1 by simp
also have
"… = map (λk. foldl1 ?g (replicate (min (k + 1) (n + 1)) One))
[0..<n + 1]" using Fun.o_def by simp
also have
"… = map (λk. foldl1 ?g (One # replicate (min k n) One))
[0..<n + 1]" by simp
also have
"… = map (λk. One) [0..<n + 1]" using foldl1_One by simp
also have
"… = replicate (n + 1) One" using const_One by simp
finally show ?thesis using List.set_replicate [where n="n + 1"] by simp
qed

― ‹Thus, with the assumptions and the free theorem of candidate, we show›
― ‹that results of @{text candidate}, after applying @{text h}, can only›
― ‹have the value @{text One}.›
have
"scanl1 ?g (map ?h (map wrap [0..<n + 1]))
= candidate ?g (map ?h (map wrap [0..<n + 1]))"
using assms and g_assoc by auto
also have
"… = map ?h (candidate (@) (map wrap [0..<n + 1]))"
using candidate_free_theorem [symmetric, where f="(@)" and g="?g"
and h="?h" and zs="(map wrap [0..<n + 1])"] and req_free_theorem by auto
finally have set_is_One:
"⋀x. x ∈ set (map ?h (candidate (@) (map wrap [0..<n + 1])))
⟹ x = One"
using set_scanl1_is_One by auto

― ‹Now, it is easy to conclude the thesis.›
from assms
have "?h js ∈ ?h  set (candidate (@) (map wrap [0..<n + 1]))" by auto
with set_is_One have "?h js = One" by simp
thus "js ≠ []" by auto
qed

text ‹
Proposition 1 is very similar to the corresponding one shown in the original
paper except of a slight modification due to the choice of using Isabelle's
list datatype.

Strictly speaking, the requirement that ‹xs› must be non-empty in the
assumptions of Proposition 1 is not necessary, because only non-empty lists
are applied in the proof. However, the additional requirement eases the proof
obligations of the final theorem, i.e. this additions allows more (or easier)
applications of the final theorem.
›

lemma Proposition_1:
assumes "⋀ (f :: three ⇒ three ⇒ three) (xs :: three list).
⟦ associative f ; xs ≠ [] ⟧  ⟹ candidate f xs = scanl1 f xs"
shows "candidate (@) (map wrap [0..<n + 1]) = ups n"
proof -
― ‹This addition is necessary because we are using Isabelle's list datatype›
― ‹which allows for empty lists.›
from assms and non_empty_candidate_results have non_empty_candidate:
"⋀js. js ∈ set (candidate (@) (map wrap [0..<n + 1])) ⟹ js ≠ []"
by auto

have "⋀(f:: three ⇒ three ⇒ three) h. associative f
⟹ map (foldl1 f ∘ map h) (candidate (@) (map wrap [0..<n + 1]))
= scanl1 f (map h [0..<n + 1])"
proof -
fix f h
assume f_assoc: "associative (f :: three ⇒ three ⇒ three)"
hence
"map (foldl1 f ∘ map h) (candidate (@) (map wrap [0..<n + 1]))
= candidate f (map h [0..<n + 1])" using Lemma_3 by auto
also have
"… = scanl1 f (map h [0..<n + 1])"
using assms [where xs="map h [0..<n + 1]"] and f_assoc by simp
finally show
"map (foldl1 f ∘ map h) (candidate (@) (map wrap [0..<n + 1]))
= scanl1 f (map h [0..<n + 1])" .
qed
with Lemma_5 and non_empty_candidate show ?thesis by auto
qed

section ‹Proving Proposition 2›

text ‹
Before proving Proposition 2, a non-trivial step of that proof is shown first.
In the original paper, the argumentation simply applies L7 and the definition
of ‹map› and ‹[0..<k + 1]›. However, since, L7 requires that
‹k› must be less than ‹length [0..<length xs]› and this does
not simply follow for the bound occurrence of ‹k›, a more complicated
proof is necessary. Here, it is shown based on Lemma 2.
›

lemma Prop_2_step_L7:
"map (λk. foldl1 g (map (nth xs) [0..<k + 1])) [0..<length xs]
= map (λk. foldl1 g (take (k + 1) xs)) [0..<length xs]"
proof -
have P1:
"length (map (λk. foldl1 g (map (nth xs) [0..<k + 1])) [0..<length xs])
= length (map (λk. foldl1 g (take (k + 1) xs)) [0..<length xs])"

have P2:
"⋀k. k < length (map (λk. foldl1 g (map (nth xs) [0..<k + 1]))
[0..<length xs])
⟹ (map (λk. foldl1 g (map (nth xs) [0..<k + 1])) [0..<length xs]) ! k
= (map (λk. foldl1 g (take (k + 1) xs)) [0..<length xs]) ! k"
proof -
fix k
assume k_length:
"k < length (map (λk. foldl1 g (map (nth xs) [0..<k + 1]))
[0..<length xs])"
hence k_length': "k < length xs" by (simp add: L2)

have
"(map (λk. foldl1 g (map (nth xs) [0..<k + 1])) [0..<length xs]) ! k
= (λk. foldl1 g (map (nth xs) [0..<k + 1])) ([0..<length xs] ! k)"
using L6 and k_length by (simp add: L2)
also have
"… = foldl1 g (map (nth xs) [0..<k + 1])"
using k_length' by (auto simp: L2)
also have
"… = foldl1 g (take (k + 1) xs)"
using L7 [where k=k and xs=xs] and k_length' by simp
also have
"… = (λk. foldl1 g (take (k + 1) xs)) ([0..<length xs] ! k)"
using k_length' by (auto simp: L2)
also have
"… = (map (λk. foldl1 g (take (k + 1) xs)) [0..<length xs]) ! k"
using L6 [symmetric] and k_length by (simp add: L2)
finally show
"(map (λk. foldl1 g (map (nth xs) [0..<k + 1])) [0..<length xs]) ! k
= (map (λk. foldl1 g (take (k + 1) xs)) [0..<length xs]) ! k" .
qed

from P1 P2 and Lemma_2 show ?thesis by blast
qed

text ‹
Compared to the original paper, here, Proposition 2 has the additional
assumption that ‹xs› is non-empty. The proof, however, is identical
to the the one given in the original paper, except for the non-trivial step
shown before.
›

lemma Proposition_2:
assumes A1: "⋀ n. candidate (@) (map wrap [0..<n + 1]) = ups n"
and A2: "associative g"
and A3: "xs ≠ []"
shows "candidate g xs = scanl1 g xs"
proof -
― ‹First, based on Lemma 2, we show that›
― ‹@{term "xs = map (nth xs) [0..<length xs]"}›
― ‹by the following facts P1 and P2.›

have P1: "length xs = length (map (nth xs) [0..<length xs])"
proof -
have
"length xs
= length [0..<length xs]" by simp
also have
"… = length (map (nth xs) [0..<length xs])"
using L2 [symmetric] by auto
finally show ?thesis .
qed

have P2: "⋀k. k < length xs ⟹ xs ! k = (map (nth xs) [0..<length xs]) ! k"
proof -
fix k
assume k_length_xs: "k < length xs"
hence k_length_xs': "k < length [0..<length xs]" by simp
have
"xs ! k = nth xs ([0..<length xs] ! k)"
using k_length_xs by simp
also have
"… = (map (nth xs) [0..<length xs]) ! k"
using L6 [symmetric] and k_length_xs' by auto
finally show "xs ! k = (map (nth xs) [0..<length xs]) ! k" .
qed

from P1 P2 and Lemma_2 have "xs = map (nth xs) [0..<length xs]" by blast

― ‹Thus, with some rewriting, we show the thesis.›
hence
"candidate g xs
= candidate g (map (nth xs) [0..<length xs])" by simp
also have
"… = map (foldl1 g ∘ map (nth xs))
(candidate (@) (map wrap [0..<length xs]))"
using Lemma_3 [symmetric, where h="nth xs" and n="length xs - 1"]
and A2 and A3 by auto
also have
"… = map (foldl1 g ∘ map (nth xs)) (ups (length xs - 1))"
using A1 [where n="length xs - 1"] and A3 by simp
also have
"… = map (foldl1 g ∘ map (nth xs)) (map (λk. [0..<k + 1]) [0..<length xs])"
using A3 by simp
also have
"… = map (λk. foldl1 g (map (nth xs) [0..<k + 1])) [0..<length xs]"
using L1 [where g="foldl1 g ∘ map (nth xs)" and f="(λk. [0..<k + 1])"]
also have
"… = map (λk. foldl1 g (take (k + 1) xs)) [0..<length xs]"
using Prop_2_step_L7 by simp
also have
"… = map (λk. foldl1 g (take k xs)) (map (λk. k + 1) [0..<length xs])"
also have
"… = map (λk. foldl1 g (take k xs)) [1..<length xs + 1]"
using List.map_Suc_upt by simp
also have
"… = scanl1 g xs" by simp
finally show ?thesis .
qed

section ‹The Final Result›

text ‹
Finally, we the main result follows directly from Proposition 1 and
Proposition 2.
›

theorem The_0_1_2_Principle:
assumes "⋀ (f :: three ⇒ three ⇒ three) (xs :: three list).
⟦ associative f ; xs ≠ [] ⟧ ⟹ candidate f xs = scanl1 f xs"
and "associative g"
and "ys ≠ []"
shows "candidate g ys = scanl1 g ys"
using Proposition_1 Proposition_2 and assms by blast

text ‹
\section*{Acknowledgments}

I thank Janis Voigtl\"ander for sharing a draft of his paper before its
publication with me.

›

(*<*)
end
(*>*)

`