Isabelle/HOL solutions to Exercises on Generalizing the Induction Hypothesis

IndGen.thy

theory IndGen
  imports Main
begin

(* From "Exercises on Generalizing the Induction Hypothesis" by James Wilcox
   https://jamesrwilcox.com/InductionExercises.html
*)

section ‹Summing lists›

primrec sum :: "nat list ⇒ nat" where
"sum [] = 0" |
"sum (x # xs) = x + sum xs"

primrec sum_tail' :: "nat list ⇒ nat ⇒ nat" where
"sum_tail' [] acc = acc" |
"sum_tail' (x # xs) acc = sum_tail' xs (x + acc)"

definition sum_tail :: "nat list ⇒ nat" where
"sum_tail l ≡ sum_tail' l 0"


lemma sum_tail'_correct: "∀acc. sum_tail' l acc = sum l + acc"
proof (induction l)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  have "sum_tail' (a # l) acc = sum_tail' l (a + acc)" by simp
  also have "... = sum l + (a + acc)" using "Cons.IH" by simp
  also have "... = (sum l + a) + acc" by simp
  also have "... = sum (a # l) + acc" by simp
  finally have "sum_tail' (a # l) acc =  sum (a # l) + acc" .
  then show ?case using local.Cons by force
qed

corollary sum_tail_correct: "sum_tail l = sum l" by (simp add: sum_tail_def sum_tail'_correct)


primrec sum_cont' :: "nat list ⇒ (nat ⇒ 'a) ⇒ 'a" where
"sum_cont' [] k = k 0" |
"sum_cont' (x # xs) k = sum_cont' xs (λans. k (x + ans))"

definition sum_cont :: "nat list ⇒ nat" where
"sum_cont l = sum_cont' l (λx. x)"

lemma sum_cont'_correct: "∀f. sum_cont' l f = f (sum l)"
proof (induction l)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  then show ?case by simp
qed

corollary sum_cont_correct: "sum_cont l = sum l"
  by (simp add: sum_cont_def sum_cont'_correct)

section ‹Tail recursion›

primrec rev :: "'a list ⇒ 'a list" where
"rev [] = []" |
"rev (x # xs) = rev xs @ [x]"

primrec rev_tail' :: "'a list ⇒ 'a list ⇒ 'a list" where
"rev_tail' [] acc = acc" |
"rev_tail' (x # xs) acc = rev_tail' xs (x # acc)"

definition rev_tail :: "'a list ⇒ 'a list" where
"rev_tail l = rev_tail' l []"


lemma rev_tail'_correct: "∀acc. rev_tail' l acc = rev l @ acc"
proof (induction l)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  then show ?case by simp
qed


corollary rev_tail_correct: "rev_tail l = rev l"
  by (simp add: rev_tail_def rev_tail'_correct)


primrec map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []" |
"map f (x # xs) = (f x) # map f xs"

primrec map_tail' :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list ⇒ 'b list" where
"map_tail' f [] acc = rev_tail acc" |
"map_tail' f (x # xs) acc = map_tail' f xs (f x # acc)"

definition map_tail :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map_tail f l = map_tail' f l []"

lemma map_tail'_correct: "∀acc. map_tail' f l acc = (rev_tail acc) @ map f l"
proof (induction l)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  have "map_tail' f (a # l) acc = map_tail' f l (f a # acc)" by simp
  also have "... = rev_tail (f a # acc) @ map f l" using Cons.IH by simp
  also have "... = rev (f a # acc) @ map f l" by (simp add: rev_tail_correct)
  also have "... = rev acc @ [f a] @ map f l" by simp
  also have "... = rev acc @ map f (a # l)" by simp
  also have "... = rev_tail acc @ map f (a # l)" by (simp add: rev_tail_correct)
  finally have "map_tail' f (a # l) acc = rev_tail acc @ map f (a # l)" .
  then show ?case using local.Cons by (simp add: rev_tail_correct)
qed

corollary map_tail_correct: "map_tail f l = map f l"
  by (simp add: rev_tail_def map_tail_def map_tail'_correct)


section ‹Arithmetic expressions›

datatype expr = Const nat
              | Plus expr expr

primrec eval_expr :: "expr ⇒ nat" where
"eval_expr (Const n) = n" |
"eval_expr (Plus e1 e2) = eval_expr e1 + eval_expr e2"

primrec eval_expr_tail' :: "expr ⇒ nat ⇒ nat" where
"eval_expr_tail' (Const n) acc = n + acc" |
"eval_expr_tail' (Plus e1 e2) acc = eval_expr_tail' e2 (eval_expr_tail' e1 acc)"

definition eval_expr_tail :: "expr ⇒ nat" where
"eval_expr_tail e = eval_expr_tail' e 0"

lemma eval_expr_tail_correct: "eval_expr_tail e = eval_expr e"
  sorry


primrec eval_expr_cont' :: "expr ⇒ (nat ⇒ 'a) ⇒ 'a" where
"eval_expr_cont' (Const n) k = k n" |
"eval_expr_cont' (Plus e1 e2) k = eval_expr_cont' e2 (λn2. eval_expr_cont' e1 (λn1. k (n1 + n2)))"

definition eval_expr_cont :: "expr ⇒ nat" where
"eval_expr_cont e = eval_expr_cont' e (λn. n)"

lemma eval_expr_cont_correct: "eval_expr_cont e = eval_expr e"
  sorry


subsection ‹Compiling to a stack language›

datatype instr = Push nat | Add

type_synonym prog = "instr list"

type_synonym stack = "nat list"

primrec run :: "prog ⇒ stack ⇒ stack" where
"run [] s = s" |
"run (i # is) s = (let s' = (case i of
    Push n ⇒ n # s
  | Add    ⇒ (case s of a1 # a2 # s' ⇒ (a1 + a2) # s' | _ ⇒ s))
  in run is s')"

primrec compile :: "expr ⇒ prog" where
"compile (Const n) = [Push n]" |
"compile (Plus e1 e2) = compile e1 @ compile e2 @ [Add]"

lemma compile_correct: "run (compile e) [] = [eval_expr e]"
  sorry


section ‹Fibonacci›

fun fib :: "nat ⇒ nat" where
"fib 0 = 1" |
"fib (Suc n) = (case n of
    0 ⇒ 1
  | Suc n' ⇒ fib n + fib n')"

primrec fib_tail' :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"fib_tail' 0 a b = b" |
"fib_tail' (Suc n) a b = fib_tail' n (a + b) a"

definition fib_tail :: "nat ⇒ nat" where
"fib_tail n = fib_tail' n 1 1"

lemma fib_tail_correct: "fib_tail n = fib n"
  sorry


end