Session MuchAdoAboutTwo

Theory MuchAdoAboutTwo

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


section ‹Much Ado about Two›

(*<*)
theory MuchAdoAboutTwo
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},
see also \cite{LogicalAbstractionsInHaskell}).
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.
Recently, in \cite{MuchAdoAboutTwo}, a similar result as Knuth's 0-1-principle
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.
One way to answer this question is given in \cite{MuchAdoAboutTwo}.
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.



Th article at hand formalises the proofs given in \cite{MuchAdoAboutTwo},
which is called here ``the original paper''. Compared to that paper, there are 
several differences in this article. The major differences are listed below.
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
(and also this article's structure). They also highlight the challenges which
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"
by (simp add: fun_eq_iff)

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])" 
      by (simp add: L1)
  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])" 
      by (simp add: Fun.o_def)
  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" 
              by (simp add: L2)
          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" 
              using List.replicate_add 
                      [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])" 
      by (simp add: L2)
      
  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])"] 
      by (simp add: Fun.o_def)
  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])"
      by (simp add: L1)
  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
(*>*)