theory week07A_demo imports Main begin primrec sep where "sep a [] = []" |"sep a [x] = [x]" |"sep a (x#xs) = x#a#(sep a xs)" -- "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" print_theorems -- "symbolic execution:" lemma "sep a [x,y,z] = blah" apply simp oops -- "with code generation" value "sep a [x,y,z]" -- "tailored induction principle:" lemma "map f (sep x xs) = sep (f x) (map f xs)" apply (induct x xs rule: sep.induct) (* note that both variables are used as induction variables! trying to do induct xs arbitrary: x rule: sep.induct will also work here, but that strategy can sometimes lead you nowhere! *) oops -- "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 "m < ack n m" apply (induct n m rule: ack.induct) apply auto done section "function" -- ----------------------------------------------------------- lemma fancy_syntax: "filter (\x. P x) xs = [x \ xs. P x]" by (rule refl) text {* when termination fails: *} (* This one will give an error message: *) fun nonterm :: "nat \ nat" where "nonterm x = nonterm (x + 1)" (* This one actually works automatically these days, but it's nicer to demonstrate what's going on: fun quicksort where "quicksort [] = []" | "quicksort (x#xs) = quicksort [y \ xs. y \ x] @ [x] @ quicksort [y \ xs. x < y]" *) text {* use the fully tweakable function form instead: *} function quicksort :: "nat list \ nat list" where "quicksort [] = []" | "quicksort (x#xs) = quicksort [y \ xs. y \ x] @ [x] @ quicksort [y \ xs. x < y]" -- "need to prove completeness and distinctness of patterns" 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 simp apply simp apply (simp add:less_Suc_eq_le) apply simp apply (simp add:less_Suc_eq_le) done -- "now have full induction and simp available" print_theorems lemma "All quicksort_dom" apply size_change done lemma "All quicksort_dom" apply lexicographic_order done lemma set_quicksort: "set (quicksort xs) = set xs" (*Note: apply (induct xs) doesn't help*) apply (induct xs rule: quicksort.induct) apply auto done section "More tweaks" -- "see also src/HOL/ex/Fundefs.thy" subsubsection {* Overlapping patterns *} text {* Patterns may overlap if compatible: *} fun gcd2 :: "nat \ nat \ nat" where "gcd2 x 0 = x" | "gcd2 0 y = y" | "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) else gcd2 (x - y) (Suc y))" print_theorems thm gcd2.simps thm gcd2.induct subsubsection {* Guards *} text {* We can reformulate the above example using guarded patterns *} function gcd3 :: "nat \ nat \ nat" where "gcd3 x 0 = x" | "gcd3 0 y = y" | "x < y \ gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" | "\ x < y \ gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" apply simp_all apply (case_tac x, case_tac a, clarsimp) apply (case_tac b, auto) done termination by lexicographic_order thm gcd3.simps thm gcd3.induct text {* General patterns: *} function ev :: "nat \ bool" where "ev (2 * n) = True" | "ev (2 * n + 1) = False" apply (simp_all) apply (subgoal_tac "x = 2 * (x div 2) + (x mod 2)") apply (case_tac "x mod 2 = 0") apply simp apply (subgoal_tac "x mod 2 = 1") apply (subgoal_tac "x = 2 * (x div 2) + 1") apply simp apply simp apply simp apply simp apply arith done termination by lexicographic_order thm ev.simps thm ev.induct thm ev.cases subsection {* Mutual Recursion *} fun evn od :: "nat \ bool" where "evn 0 = True" | "od 0 = False" | "evn (Suc n) = od n" | "od (Suc n) = evn n" print_theorems thm evn.simps thm od.simps thm evn_od.induct text {* Simple Higher-Order Recursion *} datatype 'a tree = Leaf 'a | Branch "'a tree list" fun treemap :: "('a \ 'a) \ 'a tree \ 'a tree" where "treemap fn (Leaf n) = (Leaf (fn n))" | "treemap fn (Branch l) = (Branch (map (treemap fn) l))" fun tinc :: "nat tree \ nat tree" where "tinc (Leaf n) = Leaf (Suc n)" | "tinc (Branch l) = Branch (map tinc l)" print_theorems thm tinc.induct -- ------------------------------------------------------------- text {* congruence rules *} thm if_cong map_cong primrec othermap :: "('a \ 'b) \ 'a list \ 'b list" where "othermap f [] = []" | "othermap f (x#xs) = f x # othermap f xs" fun treemap2 :: "('a \ 'a) \ 'a tree \ 'a tree" where "treemap2 fn (Leaf n) = (Leaf (fn n))" | "treemap2 fn (Branch l) = (Branch (othermap (treemap2 fn) l))" (* fails *) function treemap2 :: "('a \ 'a) \ 'a tree \ 'a tree" where "treemap2 fn (Leaf n) = (Leaf (fn n))" | "treemap2 fn (Branch l) = (Branch (othermap (treemap2 fn) l))" by pat_completeness auto termination apply (relation "R") (* no information about x available *) oops lemma othermap_cong [fundef_cong]: "\ xs = ys; \x. x \ set ys \ f x = g x \ \ othermap f xs = othermap g ys" by (induct xs arbitrary: ys) auto function treemap3 :: "('a \ 'a) \ 'a tree \ 'a tree" where "treemap3 fn (Leaf n) = (Leaf (fn n))" | "treemap3 fn (Branch l) = (Branch (othermap (treemap3 fn) l))" by pat_completeness auto termination apply (relation "R") (*now we have enough information *) sorry fun treemap4 :: "('a \ 'a) \ 'a tree \ 'a tree" where "treemap4 fn (Leaf n) = (Leaf (fn n))" | "treemap4 fn (Branch l) = (Branch (othermap (treemap4 fn) l))" end