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.