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 * (\iii"} or @{text"\"} *} lemma assumes A: "(\n. (\m. m < n \ P m) \ P n)" shows "P (n::nat)" proof (rule A) show "\m. m < n \ 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 \ n" with Suc have "m < n" by arith thus "P m" by(rule Suc) qed qed qed -- --------------------------------------------------------------- -- "arbitrary patterns" fun sep :: "'a \ 'a list \ '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 (\x. P x) xs = [x \ xs. P x]" by (rule refl) -- "when termination fails:" (* fun quicksort where "quicksort [] = []" | "quicksort (x#xs) = quicksort [y \ xs. y \ x] @ [x] @ quicksort [y \ xs. x < y]" *) -- "use the fully tweakable function form instead:" function (sequential) quicksort :: "nat list \ nat list" where "quicksort [] = []" | "quicksort (x#xs) = quicksort [y \ xs. y \ x] @ [x] @ quicksort [y \ 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