# 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.