theory week07B_demo imports Main begin

-- -------------------------------------------------

-- "More primrec and induction:"

primrec lsum :: "nat list \<Rightarrow> nat"
where
  "lsum [] = 0"
| "lsum (x#xs) = x + lsum xs"

lemma 
  "2 * lsum [0..<Suc n] = n * (n + 1)"
  oops

lemma
  "lsum (replicate n a) = n * a"
  oops

primrec lsumT where
  "lsumT [] s = s"
| "lsumT (x#xs) s = lsumT xs (x+s)"

lemma 
  "lsumT xs 0 = lsum xs"
  oops

-- -------------------------------------------------

-- {* Isar, case distinction *}

declare length_tl[simp del]

lemma "length(tl xs) = length xs - 1"
proof (cases xs)
  case Nil thus ?thesis by simp
next
  case (Cons y ys) thus ?thesis by simp
qed


-- {* structural induction *}

lemma "2 * (\<Sum>i<n+1. i) = n*(n+1::nat)"
  by (induct n, simp_all)


lemma "2 * (\<Sum>i<n+1. i) = n*(n+1::nat)" (is "?P n")
proof (induct n)
  show "?P 0" by simp
next
  fix n assume "?P n"
  thus "?P (Suc n)" by simp
qed


lemma "2 * (\<Sum>i<n+1. i) = n*(n+1::nat)"
proof (induct n)
  case 0 show ?case by simp
next
  case Suc thus ?case by simp
qed


lemma fixes n::nat shows "n < n*n + 1"
proof (induct n)
  case 0 show ?case by simp
next
  case (Suc i) thus "Suc i < Suc i * Suc i + 1" by simp
qed



-- {* induction with @{text"\<And>"} or @{text"\<Longrightarrow>"} *}

lemma 
  assumes A: "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
  shows "P (n::nat)"
proof (rule A)
  show "\<And>m. m < n \<Longrightarrow> P m"
  proof (induct n)
    case 0 thus ?case by simp
  next
    case (Suc n)   
    show ?case    
    proof cases
      assume eq: "m = n"
      from Suc and A have "P n" by blast
      with eq show "P m" by simp
    next
      assume "m \<noteq> n"
      with Suc have "m < n" by arith 
      thus "P m" by(rule Suc)
    qed
  qed
qed


end