Theory CaseStudy1

(*  Title:       A General Method for the Proof of Theorems on Tail-recursive Functions
    Author:      Pasquale Noce
                 Security Certification Specialist at Arjo Systems - Gep S.p.A.
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at arjowiggins-it dot com
*)

section "Case study 1"

theory CaseStudy1
imports Main
begin

text ‹
\null

In the first case study, the problem will be examined of defining a function
‹l_sort› performing insertion sort on lists of elements of a linear order,
and then proving the correctness of this definition, i.e. that the lists output by
the function actually be sorted and contain as many occurrences of any value as
the input lists.

Such function constitutes a paradigmatic example of a function admitting a
straightforward tail-recursive definition. Here below is a naive one:

\null
›

fun l_sort_naive :: "'a::linorder list ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
"l_sort_naive (x # xs) ys [] = l_sort_naive xs [] (ys @ [x])" |
"l_sort_naive (x # xs) ys (z # zs) = (if x ≤ z
  then l_sort_naive xs [] (ys @ x # z # zs)
  else l_sort_naive (x # xs) (ys @ [z]) zs)" |
"l_sort_naive [] ys zs = zs"

text ‹
\null

The first argument is deputed to contain the values still having to be inserted
into the sorted list, accumulated in the third argument. For each of such values,
the items of the sorted list are orderly moved into a temporary one (second
argument) to search the insertion position. Once found, the sorted list is
restored, the processed value is moved from the unsorted list to the sorted one,
and another iteration of the loop is performed up to the exhaustion of the former
list.

A further couple of functions are needed to express the aforesaid correctness
properties of function ‹l_sort_naive›:

\null
›

fun l_sorted :: "'a::linorder list ⇒ bool" where
"l_sorted (x # x' # xs) = (x ≤ x' ∧ l_sorted (x' # xs))" |
"l_sorted _ = True"

definition l_count :: "'a ⇒ 'a list ⇒ nat" where
"l_count x xs ≡ length [x'←xs. x' = x]"

text ‹
\null

Then, the target correctness theorems can be enunciated as follows:

\null

‹l_sorted (l_sort_naive xs [] [])›

\null

‹l_count x (l_sort_naive xs [] []) = l_count x xs›

\null

Unfortunately, attempts to apply recursion induction to such goals turn out to be
doomed, as can easily be ascertained by considering the former theorem:

\null
›

theorem "l_sorted (l_sort_naive xs [] [])"
proof (rule l_sort_naive.induct [of "λxs ys zs. l_sorted (l_sort_naive xs ys zs)"],
 simp_all del: l_sort_naive.simps(3))

txt ‹
\null

Simplification deletes all the subgoals generated by recursive equations.
However, the following subgoal arises from the non-recursive one:

\null

@{subgoals [display]}

\null

which is hopeless as the formula is false for any unsorted list ‹zs›.

\null
›

oops

subsection "Step 1"

type_synonym 'a l_type = "'a list × 'a list × 'a list"

fun l_sort_aux :: "'a::linorder l_type ⇒ 'a l_type" where
"l_sort_aux (x # xs, ys, []) = l_sort_aux (xs, [], ys @ [x])" |
"l_sort_aux (x # xs, ys, z # zs) = (if x ≤ z
  then l_sort_aux (xs, [], ys @ x # z # zs)
  else l_sort_aux (x # xs, ys @ [z], zs))" |
"l_sort_aux ([], ys, zs) = ([], ys, zs)"

text ‹
\null

Observe that the Cartesian product of the input types has been implemented as a
product type.
›

subsection "Step 2"

definition l_sort_in :: "'a list ⇒ 'a l_type" where
"l_sort_in xs ≡ (xs, [], [])"

definition l_sort_out :: "'a l_type ⇒ 'a list" where
"l_sort_out X ≡ snd (snd X)"

definition l_sort :: "'a::linorder list ⇒ 'a list" where
"l_sort xs ≡ l_sort_out (l_sort_aux (l_sort_in xs))"

text ‹
\null

Since the significant inputs of function ‹l_sort_naive› match pattern
‹_›, ‹[]›, ‹[]›, those of function ‹l_sort_aux›
match pattern ‹(_, [], [])›, thus being in a one-to-one correspondence
with the type of the first component.

The target correctness theorems can then be put into the following equivalent
form:

\null

‹l_sorted (l_sort xs)›

\null

‹l_count x (l_sort xs) = l_count x xs›
›

subsection "Step 3"

text ‹
The conditional recursive equation in the definition of function
‹l_sort_aux› will equivalently be associated to two distinct introduction
rules in the definition of the inductive set ‹l_sort_set›, one for either
truth value of the Boolean condition, handled as an additional assumption. The
advantage is twofold: simpler introduction rules are obtained, and case
distinctions are saved as rule induction is applied.

\null
›

inductive_set l_sort_set :: "'a::linorder l_type ⇒ 'a l_type set"
for X :: "'a l_type" where
R0: "X ∈ l_sort_set X" |
R1: "(x # xs, ys, []) ∈ l_sort_set X ⟹ (xs, [], ys @ [x]) ∈ l_sort_set X" |
R2: "⟦(x # xs, ys, z # zs) ∈ l_sort_set X; x ≤ z⟧ ⟹
     (xs, [], ys @ x # z # zs) ∈ l_sort_set X" |
R3: "⟦(x # xs, ys, z # zs) ∈ l_sort_set X; ¬ x ≤ z⟧ ⟹
     (x # xs, ys @ [z], zs) ∈ l_sort_set X"

subsection "Step 4"

lemma l_sort_subset:
  assumes XY: "Y ∈ l_sort_set X"
  shows "l_sort_set Y ⊆ l_sort_set X"
proof (rule subsetI, erule l_sort_set.induct)
  show "Y ∈ l_sort_set X" using XY .
next
  fix x xs ys
  assume "(x # xs, ys, []) ∈ l_sort_set X"
  thus "(xs, [], ys @ [x]) ∈ l_sort_set X" by (rule R1)
next
  fix x xs ys z zs
  assume "(x # xs, ys, z # zs) ∈ l_sort_set X" and "x ≤ z"
  thus "(xs, [], ys @ x # z # zs) ∈ l_sort_set X" by (rule R2)
next
  fix x xs ys z zs
  assume "(x # xs, ys, z # zs) ∈ l_sort_set X" and "¬ x ≤ z"
  thus "(x # xs, ys @ [z], zs) ∈ l_sort_set X" by (rule R3)
qed

lemma l_sort_aux_set: "l_sort_aux X ∈ l_sort_set X"
proof (induction rule: l_sort_aux.induct, simp_all del: l_sort_aux.simps(2))
  fix ys :: "'a list" and zs
  show "([], ys, zs) ∈ l_sort_set ([], ys, zs)" by (rule R0)
next
  fix x :: 'a and xs ys
  have "(x # xs, ys, []) ∈ l_sort_set (x # xs, ys, [])" by (rule R0)
  hence "(xs, [], ys @ [x]) ∈ l_sort_set (x # xs, ys, [])" by (rule R1)
  hence "l_sort_set (xs, [], ys @ [x]) ⊆ l_sort_set (x # xs, ys, [])"
   by (rule l_sort_subset)
  moreover assume "l_sort_aux (xs, [], ys @ [x]) ∈ l_sort_set (xs, [], ys @ [x])"
  ultimately show "l_sort_aux (xs, [], ys @ [x]) ∈ l_sort_set (x # xs, ys, [])"
   by (rule subsetD)
next
  fix x :: 'a and xs ys z zs
  assume
   case1: "x ≤ z ⟹
    l_sort_aux (xs, [], ys @ x # z # zs) ∈ l_sort_set (xs, [], ys @ x # z # zs)"
  and
   case2: "¬ x ≤ z ⟹
    l_sort_aux (x # xs, ys @ [z], zs) ∈ l_sort_set (x # xs, ys @ [z], zs)"
  have 0: "(x # xs, ys, z # zs) ∈ l_sort_set (x # xs, ys, z # zs)" by (rule R0)
  show "l_sort_aux (x # xs, ys, z # zs) ∈ l_sort_set (x # xs, ys, z # zs)"
  proof (cases "x ≤ z", simp_all)
    assume "x ≤ z"
    with 0 have "(xs, [], ys @ x # z # zs) ∈ l_sort_set (x # xs, ys, z # zs)"
     by (rule R2)
    hence "l_sort_set (xs, [], ys @ x # z # zs) ⊆ l_sort_set (x # xs, ys, z # zs)"
     by (rule l_sort_subset)
    moreover have "l_sort_aux (xs, [], ys @ x # z # zs) ∈
     l_sort_set (xs, [], ys @ x # z # zs)" using case1 and ‹x ≤ z› by simp
    ultimately show "l_sort_aux (xs, [], ys @ x # z # zs) ∈
     l_sort_set (x # xs, ys, z # zs)" by (rule subsetD)
  next
    assume "¬ x ≤ z"
    with 0 have "(x # xs, ys @ [z], zs) ∈ l_sort_set (x # xs, ys, z # zs)"
     by (rule R3)
    hence "l_sort_set (x # xs, ys @ [z], zs) ⊆ l_sort_set (x # xs, ys, z # zs)"
     by (rule l_sort_subset)
    moreover have "l_sort_aux (x # xs, ys @ [z], zs) ∈
     l_sort_set (x # xs, ys @ [z], zs)" using case2 and ‹¬ x ≤ z› by simp
    ultimately show "l_sort_aux (x # xs, ys @ [z], zs) ∈
     l_sort_set (x # xs, ys, z # zs)" by (rule subsetD)
  qed
qed

text ‹
\null

The reader will have observed that the simplification rule arising from the
second equation in the definition of function ‹l_sort_aux›, i.e. the one
whose right-hand side contains a conditional, has been ignored in the initial
backward steps of the previous proof. The reason is that it would actually make
more complex the conclusion of the corresponding subgoal, as can easily be
verified by trying to leave it enabled.

\null
›

lemma "l_sort_aux X ∈ l_sort_set X"
proof (induction rule: l_sort_aux.induct, simp_all)

(*<*)
prefer 2
(*>*)

txt ‹
\null

As a result of the application of the rule, the related subgoal takes the
following form:

\null

@{subgoals [display, goals_limit = 1]}

\null

Now the conclusion is comprised of a conjunction of two implications. This is
pointless, since case distinction is faster than the application of conjunction
and implication introduction rules in providing sufficient assumptions for the
simplification of both the induction hypotheses and the conclusion.

\null
›

oops

text ‹
\null

These considerations clearly do not depend on the particular function under
scrutiny, so that postponing the application of conditional simplification rules
to case distinction turns out to be a generally advisable strategy for the
accomplishment of step 4.
›

subsection "Step 5"

text ‹
Two invariants are defined here below, one for each of the target correctness
theorems:

\null
›

fun l_sort_inv_1 :: "'a::linorder l_type ⇒ bool" where
"l_sort_inv_1 (x # xs, y # ys, z # zs) =
  (l_sorted (y # ys) ∧ l_sorted (z # zs) ∧
  last (y # ys) ≤ x ∧ last (y # ys) ≤ z)" |
"l_sort_inv_1 (x # xs, y # ys, []) =
  (l_sorted (y # ys) ∧ last (y # ys) ≤ x)" |
"l_sort_inv_1 (_, _, zs) =
  l_sorted zs"

definition l_sort_inv_2 :: "'a ⇒ 'a list ⇒ 'a l_type ⇒ bool" where
"l_sort_inv_2 x xs X ≡ (fst X = [] ⟶ fst (snd X) = []) ∧
  l_count x (fst X) + l_count x (fst (snd X)) + l_count x (snd (snd X)) =
  l_count x xs"

text ‹
\null

More precisely, the second invariant, whose type has to match
‹'a l_type ⇒ bool› according to the method specification, shall be
comprised of function ‹l_sort_inv_2 x xs›, where ‹x›, ‹xs›
are the free variables appearing in the latter target theorem.

Both of the above definitions are non-recursive; command ‹fun› is used in
the former for the sole purpose of taking advantage of pattern matching.
›

subsection "Step 6"

lemma l_sort_input_1: "l_sort_inv_1 (xs, [], [])"
by simp

lemma l_sort_input_2: "l_sort_inv_2 x xs (xs, [], [])"
by (simp add: l_sort_inv_2_def l_count_def)

subsection "Step 7"

definition l_sort_form :: "'a l_type ⇒ bool" where
"l_sort_form X ≡ fst X = []"

lemma l_sort_intro_1:
 "l_sort_inv_1 X ⟹ l_sorted (l_sort_out X)"
by (rule l_sort_inv_1.cases [of X], simp_all add: l_sort_out_def)

lemma l_sort_intro_2:
 "⟦l_sort_inv_2 x xs X; l_sort_form X⟧ ⟹
  l_count x (l_sort_out X) = l_count x xs"
by (simp add: l_sort_inv_2_def, (erule conjE)+,
 simp add: l_sort_form_def l_sort_out_def l_count_def)

subsection "Step 8"

lemma l_sort_form_aux_all: "l_sort_form (l_sort_aux X)"
by (rule l_sort_aux.induct [of "λX. l_sort_form (l_sort_aux X)"],
 simp_all add: l_sort_form_def)

lemma l_sort_form_aux: "l_sort_form (l_sort_aux (xs, [], []))"
by (rule l_sort_form_aux_all)

subsection "Step 9"

text ‹
The proof of the first invariance property requires the following lemma, stating
that in case two lists are sorted, their concatenation still is such as long as
the last item of the former is not greater than the first one of the latter.

\null
›

lemma l_sorted_app [rule_format]:
 "l_sorted xs ⟶ l_sorted ys ⟶ last xs ≤ hd ys ⟶ l_sorted (xs @ ys)"
proof (induction xs rule: l_sorted.induct, simp_all, (rule impI)+)
  fix x
  assume "l_sorted ys" and "x ≤ hd ys"
  thus "l_sorted (x # ys)" by (cases ys, simp_all)
qed

lemma l_sort_invariance_1:
  assumes XY: "Y ∈ l_sort_set X" and X: "l_sort_inv_1 X"
  shows "l_sort_inv_1 Y"
using XY
proof (rule l_sort_set.induct, simp_all)
  show "l_sort_inv_1 X" using X .
next
  fix x :: 'a and xs ys
  assume I: "l_sort_inv_1 (x # xs, ys, [])"
  show "l_sorted (ys @ [x])"
  proof (cases ys, simp)
    fix a as
    assume "ys = a # as"
    hence "l_sorted ys ∧ last ys ≤ x" using I by simp
    moreover have "l_sorted [x]" by simp
    ultimately show ?thesis by (simp add: l_sorted_app)
  qed
next
  fix x :: 'a and xs ys z zs
  assume XZ: "x ≤ z" and I: "l_sort_inv_1 (x # xs, ys, z # zs)"
  thus "l_sorted (ys @ x # z # zs)"
  proof (cases ys, simp)
    fix a as
    assume "ys = a # as"
    hence *: "l_sorted ys ∧ l_sorted (z # zs) ∧ last ys ≤ x" using I by simp
    with XZ have "l_sorted (x # z # zs)" by simp
    with * show ?thesis by (simp add: l_sorted_app)
  qed
next
  fix x :: 'a and xs ys z zs
  assume "¬ x ≤ z"
  hence XZ: "z ≤ x" by simp
  assume "l_sort_inv_1 (x # xs, ys, z # zs)"
  thus "l_sort_inv_1 (x # xs, ys @ [z], zs)"
  proof (cases ys, simp)
    assume I: "l_sorted (z # zs)"
    show "l_sort_inv_1 (x # xs, [z], zs)"
    proof (cases zs, simp)
      show "z ≤ x" using XZ .
    next
      fix a as
      assume zs: "zs = a # as"
      then have *: "z ≤ a ∧ l_sorted zs" using I by simp
      have "l_sorted [z]" by simp
      with zs * show ?thesis using XZ by simp
    qed
  next
    fix a as
    assume YS: "ys = a # as" and "l_sort_inv_1 (x # xs, ys, z # zs)"
    hence I: "l_sorted ys ∧ l_sorted (z # zs) ∧ last ys ≤ z" by simp
    have "l_sorted [z]" by simp
    hence I': "l_sorted (ys @ [z])" using I by (simp add: l_sorted_app)
    show ?thesis
    proof (cases zs, simp)
      show "l_sort_inv_1 (x # xs, ys @ [z], [])" using I' and XZ and YS by simp
    next
      fix b bs
      assume zs: "zs = b # bs"
      then have "z ≤ b ∧ l_sorted zs" using I by simp
      with zs show ?thesis using I and I' and XZ and YS by simp
    qed
  qed
qed

text ‹
\null

Likewise, the proof of the second invariance property calls for the following
lemmas, stating that the number of occurrences of a value in a list is
additive with respect to both item prepending and list concatenation.

\null
›

lemma l_count_cons: "l_count x (y # ys) = l_count x [y] + l_count x ys"
by (simp add: l_count_def)

lemma l_count_app: "l_count x (ys @ zs) = l_count x ys + l_count x zs"
by (simp add: l_count_def)

lemma l_sort_invariance_2:
  assumes XY: "Y ∈ l_sort_set X" and X: "l_sort_inv_2 w ws X"
  shows "l_sort_inv_2 w ws Y"
using XY
proof (rule l_sort_set.induct)
  show "l_sort_inv_2 w ws X" using X .
next
  fix x xs ys
  assume "l_sort_inv_2 w ws (x # xs, ys, [])"
  thus "l_sort_inv_2 w ws (xs, [], ys @ [x])"
  proof (simp add: l_sort_inv_2_def, subst (asm) l_count_cons, subst l_count_app)
  qed (simp add: l_count_def ac_simps)
next
  fix x xs ys z zs
  assume "l_sort_inv_2 w ws (x # xs, ys, z # zs)"
  thus "l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)"
  proof (simp add: l_sort_inv_2_def, subst (asm) l_count_cons, subst l_count_app,
   subst l_count_cons)
  qed (simp add: l_count_def ac_simps)
next
  fix x xs ys z zs
  assume "l_sort_inv_2 w ws (x # xs, ys, z # zs)"
  thus "l_sort_inv_2 w ws (x # xs, ys @ [z], zs)"
  proof (simp add: l_sort_inv_2_def, subst (asm) (2) l_count_cons,
   subst l_count_app)
  qed (simp add: l_count_def ac_simps)
qed

subsection "Step 10"

theorem "l_sorted (l_sort xs)"
proof -
  let ?X = "(xs, [], [])"
  have "l_sort_aux ?X ∈ l_sort_set ?X" by (rule l_sort_aux_set)
  moreover have "l_sort_inv_1 ?X" by (rule l_sort_input_1)
  ultimately have "l_sort_inv_1 (l_sort_aux ?X)" by (rule l_sort_invariance_1)
  hence "l_sorted (l_sort_out (l_sort_aux ?X))" by (rule l_sort_intro_1)
  moreover have "?X = l_sort_in xs" by (simp add: l_sort_in_def)
  ultimately show ?thesis by (simp add: l_sort_def)
qed

theorem "l_count x (l_sort xs) = l_count x xs"
proof -
  let ?X = "(xs, [], [])"
  have "l_sort_aux ?X ∈ l_sort_set ?X" by (rule l_sort_aux_set)
  moreover have "l_sort_inv_2 x xs ?X" by (rule l_sort_input_2)
  ultimately have "l_sort_inv_2 x xs (l_sort_aux ?X)" by (rule l_sort_invariance_2)
  moreover have "l_sort_form (l_sort_aux ?X)" by (rule l_sort_form_aux)
  ultimately have "l_count x (l_sort_out (l_sort_aux ?X)) = l_count x xs"
   by (rule l_sort_intro_2)
  moreover have "?X = l_sort_in xs" by (simp add: l_sort_in_def)
  ultimately show ?thesis by (simp add: l_sort_def)
qed

end