Download the archive: labs05.tar.gz

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

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.

Prove reverse xs1 = reverse xs2 ⟹ xs1 = xs2.

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.

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.

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

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.