theory Demo10 imports Main begin


-- {* 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 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


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

-- "arbitrary patterns"
fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  "sep a (x # y # zs) = x # a # sep a (y # zs)"
| "sep a xs = xs"

-- "symbolic execution:"
lemma "sep a [x,y,z] = blah" 
  apply simp
  oops

-- "tailored induction principle:"
lemma "map f (sep x xs) = sep (f x) (map f xs)"
  apply (induct x xs rule: sep.induct)
  apply auto
  done


-- "can leave type to be inferred:"
fun ack where
  "ack 0 n = Suc n"
| "ack (Suc m) 0 = ack m 1"
| "ack (Suc m) (Suc n) = ack m (ack (m+1) n)"

-- "nested recursion -> induction principle that mentions ack again:"
thm ack.induct



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

lemma fancy_syntax:
  "filter (\<lambda>x. P x) xs = [x \<leftarrow> xs. P x]" by (rule refl)

-- "when termination fails:"

(*
fun quicksort where
  "quicksort [] = []"
| "quicksort (x#xs) = quicksort [y \<leftarrow> xs. y \<le> x] @ [x] @ quicksort [y \<leftarrow> xs. x < y]"
*)


-- "use the fully tweakable function form instead:"

function (sequential) quicksort :: "nat list \<Rightarrow> nat list" 
where
  "quicksort [] = []"
| "quicksort (x#xs) = quicksort [y \<leftarrow> xs. y \<le> x] @ [x] @ quicksort [y \<leftarrow> xs. x < y]"

-- "need to prove distinctness and completeness of patterns"
  by pat_completeness auto

(*
     apply pat_completeness
    apply simp
   apply simp
  apply simp
  done
*)

-- "get only partial simp and induction rules"
thm quicksort.psimps
thm quicksort.pinduct

termination quicksort
  apply (relation "measure length")
    apply (auto simp: less_Suc_eq_le)
  done

-- "now have full induction and simp available"
print_theorems

thm sorted.simps

lemma sorted_quicksort:
  "set (quicksort xs) = set xs"
  oops

end
