# Labs 05: Isabelle

## Part 1: Warm-up Problems

### Example: Append nil

Here are two different proofs of the same fact “app xs nil = xs”. The first one uses a detailed proof mode to show you the explicit steps, and to give you an example of syntax for Isabelle. This example shows you how you can structure your proofs. The second one uses apply scripts, which are more step-oriented form of proof that may be more readable. Note that structured proofs transition to apply script state in places where 'by' keyword occurs. Conversely, once in apply script state, the directive 'proof' transitions to structured proof.

```lemma app_nil_manual "app xs nil = xs"
proof (induction xs)
case nil
then show ?case by auto
next
case (cons x1 xs)
have 1: "app (cons x1 xs) nil = cons x1 (app xs nil)" by simp
have 2: "cons x1 (app xs nil) = cons x1 xs" by (simp add: cons.IH)
show "app (cons x1 xs) nil = cons x1 xs" using 1 2 by simp
qed

lemma app_nil: "app xs nil = xs"
apply (induction xs)
by auto```

### Problem 1: Associativity of append

Prove app xs (app ys zs) = app (app xs ys) zs using both styles. After this problem, you can choose the style you want to write your proofs.

### Problem 2: Injectivity of reverse

Prove reverse xs1 = reverse xs2 ⟹ xs1 = xs2.

### Problem 3: Folding a list in reverse

```fun fold_left :: "'a list ⇒ 'b ⇒ ('b ⇒ 'a ⇒ 'b) ⇒ 'b" where
"fold_left nil acc f = acc"
| "fold_left (cons x xs) acc f = fold_left xs (f acc x) f"```

Find a (reasonable) sufficient condition on f so that fold_left (reverse xs) b f = fold_left xs b f holds, and prove the corresponding lemma.

### Problem 4: Fold left and fold right

```fun fold_right :: "'a list ⇒ 'b ⇒ ('a ⇒ 'b ⇒ 'b) ⇒ 'b" where
"fold_right nil b f = b"
| "fold_right (cons x xs) b f = f x (fold_right xs b f)"```

Find a (reasonable) sufficient condition on f so that fold_right xs b (λa.λb. f b a) = fold_left xs b f holds, and prove the corresponding lemma.

### Problem 5: Insert tree/list

Prove the tree_insert_list lemma: is_search_tree t ⟹ insert (tree_to_list t) v = tree_to_list (tree_insert t v)

## Part 2: Programs as Relations

Complete all proofs in this theory about modelling programs as relations, so that no “sorry” remains. The proofs will be short thanks to automation. You are not allowed to change the definitions that are already in the file.