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