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