theory week07B_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 (* An example of how to construct a recursive function from first principles, given an inductive relation that defines the function's graph. We don't recommend this method of introducing functions, but it gives some perspective on the kind of work fun does for us. *) inductive_set my_sep_rel :: "(('a \ 'a list) \ 'a list) set" where "((a,[]),[]) \ my_sep_rel" | "((a,[x]),[x]) \ my_sep_rel" | "((a,y#l),l') \ my_sep_rel \ ((a,x#y#l),x#a#l') \ my_sep_rel" (* Prove that the relation is unique and total (\! means "exists a unique") *) lemma my_sep_rel_unique: "\!y. ((a, l), y) \ my_sep_rel" apply(induct rule: length_induct) apply(case_tac xs) apply(subst my_sep_rel.simps;simp) apply(case_tac list;subst my_sep_rel.simps;simp) apply clarsimp apply(rename_tac p q l) apply(drule_tac x="q#l" in spec) by auto (* Define a function my_sep to Hilbert-choose the RHS from the relevant element of the graph relation my_sep_rel. *) definition my_sep :: "'a \ 'a list \ 'a list" where "my_sep \ \a x. THE y. ((a,x),y) \ my_sep_rel" (* Derive recursive equations as theorems *) lemma my_sep_simps[simp]: "my_sep a [] = []" "my_sep a [x] = [x]" "my_sep a (x#y#l) = (x#a#my_sep a (y#l))" unfolding my_sep_def apply(subst my_sep_rel.simps,simp) apply(rule the1_equality[OF my_sep_rel_unique]) apply(rule my_sep_rel.intros) apply(rule the1_equality[OF my_sep_rel_unique]) apply(rule the1I2[OF my_sep_rel_unique]) by(rule my_sep_rel.intros) (* Derive induction principle from graph relation's induction principle *) lemma my_sep_induct: fixes a::'a and l :: "'a list" assumes nil: "\a. P a []" and one: "\a x. P a [x]" and cons: "\a x y l. P a (y#l) \ P a(x#y#l)" shows "P a l" proof - obtain y where "((a,l), y) \ my_sep_rel" using my_sep_rel_unique by force then show ?thesis by(induct rule: my_sep_rel.induct) (auto intro: assms) qed (* Or we could just let fun do all the work... *) lemma "sep x l = my_sep x l" by(induct x l rule: sep.induct) auto \ \ 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