(* Certified Functional (Co)programming with Isabelle/HOL *)
(* Jasmin Christian Blanchette, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel *)
section \Programming examples\
theory Induction
imports Main "~~/src/HOL/Library/Code_Test"
begin
(* disable list syntax and functions from Isabelle's standard library *)
no_type_notation list ("[_]" [0] 999)
no_notation
Nil ("[]") and
Cons (infixr "#" 65) and
append (infixr "@" 65)
hide_const (open) rev append Nil Cons map concat set
hide_type (open) list
datatype (set: 'a) list
= Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
for map: map
translations (* syntax for list enumerations *)
"[x, xs]" == "x # [xs]"
"[x]" == "x # []"
declare list.map_cong [cong] list.map_ident [simp]
primrec append :: "'a list \ 'a list \ 'a list" (infixr "@" 65)
where
append_Nil: "[] @ ys = ys"
| append_Cons: "(x # xs) @ ys = x # (xs @ ys)"
export_code append in Haskell
value "[1,2,3] @ [4,5,6] :: int list"
primrec rev :: "'a list \ 'a list" where
"rev [] = []"
| "rev (x # xs) = rev xs @ [x]"
export_code rev in Haskell
primrec qrev :: "'a list \ 'a list \ 'a list" where
qrev_Nil: "qrev [] ys = ys"
| qrev_Cons: "qrev (x # xs) ys = qrev xs (x # ys)"
export_code qrev in Haskell
lemma append_Nil2 [simp]: "xs @ [] = xs"
by(induction xs) simp_all
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
by(induction xs)(simp_all)
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
by(induction xs)(simp_all)
lemma rev_rev [simp]: "rev (rev xs) = xs"
by(induction xs)(simp_all)
lemma qrev_aux: "qrev xs zs @ ys = qrev xs (zs @ ys)"
by(induction xs arbitrary: zs) simp_all
lemma rev_qrev': "rev xs @ ys = qrev xs ys"
by(induction xs arbitrary: ys)(simp_all add: qrev_aux)
lemma rev_qrev: "rev xs = qrev xs []"
by(simp add: rev_qrev'[symmetric])
declare rev_qrev [code]
export_code rev in Haskell
thm rev_def
subsection \List concatenation\
(* Define a function concat :: "'a list list \ 'a list" that concatenates a list of lists. *)
primrec concat :: "'a list list \ 'a list" where
"concat [] = ..."
| "concat (xs # xss) = ..."
(* How does concat behave w.r.t. append and rev? Find appropriate right-hand sides
for the lemmas and prove them. *)
lemma concat_append: "concat (xss @ yss) = ..."
lemma rev_concat: "rev (concat xss) = ..."
text \
Termination proofs
Task: Define a function merge that merges two lists:
merge [a,b,c] [1,2,3,4] = [a,1,b,2,c,3,4]
\
function merge :: "'a list \ 'a list \ 'a list" where
"merge [] ys = ys"
| "merge (x # xs) ys = x # merge ys xs"
by pat_completeness auto
termination
apply(relation "measure (\(xs, ys). size xs + size ys)")
apply auto
done
(* by size_change *)
value "merge [1,2,3] [4,5,6,7] :: int list"
text \Rose trees\
datatype 'a rtree = Node 'a "'a rtree list"
primrec rmirror :: "'a rtree \ 'a rtree"
where "rmirror (Node x ts) = Node x (rev (map rmirror ts))"
(* Define a function preorder :: "'a rtree \ 'a list" that traverses an
arbitrarily branching tree in preorder and returns the list of nodes it visits. Also define a
function postorder that does the same for a postorder traversal. *)
primrec preorder :: "'a rtree \ 'a list" where
end