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.

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, [], [])"

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)+,

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)"],

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"

lemma l_count_app: "l_count x (ys @ zs) = l_count x ys + l_count x zs"

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)
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)
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

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
```