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