homework1.thy

theory Homework1
  imports Main
begin

(* https://github.com/nipkow/fds_ss20/blob/master/ex01.pdf *)

fun snoc::"'a list ⇒ 'a ⇒ 'a list" where
"snoc [] x' = [x']" |
"snoc (x#xs) x' = x # (snoc xs x')"

fun reverse :: "'a list ⇒ 'a list" where
"reverse [] = []" | 
"reverse (x#xs) = snoc (reverse xs) x"

fun lmax :: "nat list ⇒ nat" where
"lmax [] = 0" |
"lmax [x] = x" |
"lmax (x # xs) = (if x > lmax xs then x else lmax xs)"

lemma lmax_in_set [simp]: "(x ∈ set xs ⟹ x ≤ lmax xs) ⟹ x ≤ lmax (x # xs)"
  by (induction xs) auto

lemma lmax_generalized [simp]: "x ≤ lmax xs ⟹ x ∈ set xs ⟹ x ≤ lmax (a # xs)"
  by (induction xs) auto

lemma max_greater: "x ∈ set xs ⟹ x ≤ lmax xs"
  by (induction xs) auto

lemma snoc_to_rev: "snoc (reverse xs) a = reverse (a # xs)"
  apply(induction xs)
   apply(auto)
  done

lemma "lmax (reverse xs) = lmax xs"
  apply(induction xs)
   apply(auto) 
  sorry


end