theory week07A_demo imports Main begin

-- "arbitrary patterns"
fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> '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

-- "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"
  sorry (* prove *)

section "function"
-- -----------------------------------------------------------

lemma fancy_syntax:
  "filter (\<lambda>x. P x) xs = [x \<leftarrow> xs. P x]" by (rule refl)

text {* when termination fails: *}

(*
fun nonterm :: "nat \<Rightarrow> nat" where
  "nonterm x = nonterm (x + 1)"

fun quicksort where
  "quicksort [] = []"
| "quicksort (x#xs) =
     quicksort [y \<leftarrow> xs. y \<le> x] @ [x] @ quicksort [y \<leftarrow> xs. x < y]"
*)


text {* use the fully tweakable function form instead: *}

function (sequential) quicksort :: "nat list \<Rightarrow> nat list"
where
  "quicksort [] = []"
| "quicksort (x#xs) =
     quicksort [y \<leftarrow> xs. y \<le> x] @ [x] @ quicksort [y \<leftarrow> xs. x < y]"

  -- "need to prove distinctness and completeness 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")
    thm less_Suc_eq_le
    apply (auto simp: less_Suc_eq_le)
  done

-- "now have full induction and simp available"
print_theorems

lemma "All quicksort_dom"
  apply size_change
(* can try different orders (ms = Multiset, needs Multiset Library thy
  apply (size_change min)
  apply (size_change max)
  apply (size_change ms)
*)
  done

lemma "All quicksort_dom"
  apply lexicographic_order
  done

lemma set_quicksort:
  "set (quicksort xs) = set xs"
  sorry (* prove *)


section "More tweaks"
-- "see also src/HOL/ex/Fundefs.thy"

subsubsection {* Overlapping patterns *}

text {* Patterns may overlap if compatible: *}

fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> 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))"

thm gcd2.simps

subsubsection {* Guards *}

text {* We can reformulate the above example using guarded patterns *}

function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
  "gcd3 x 0 = x"
| "gcd3 0 y = y"
| "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
| "\<not> x < y \<Longrightarrow> 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 \<Rightarrow> bool"
where
  "ev (2 * n) = True"
| "ev (2 * n + 1) = False"
proof -  -- {* completeness is more difficult here *}
  fix P :: bool
    and x :: nat
  assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
    and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
  have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto
  show "P"
  proof cases
    assume "x mod 2 = 0"
    with divmod have "x = 2 * (x div 2)" by simp
    with c1 show "P" .
  next
    assume "x mod 2 \<noteq> 0"
    hence "x mod 2 = 1" by simp
    with divmod have "x = 2 * (x div 2) + 1" by simp
    with c2 show "P" .
  qed
qed presburger+ -- {* solve compatibility with presburger (arith also works) *}
termination by lexicographic_order

thm ev.simps
thm ev.induct
thm ev.cases


subsection {* Mutual Recursion *}

fun evn od :: "nat \<Rightarrow> 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 \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
where
  "treemap fn (Leaf n) = (Leaf (fn n))"
| "treemap fn (Branch l) = (Branch (map (treemap fn) l))"

fun tinc :: "nat tree \<Rightarrow> nat tree"
where
  "tinc (Leaf n) = Leaf (Suc n)"
| "tinc (Branch l) = Branch (map tinc l)"


text {* Pattern matching on records *}
record point =
  Xcoord :: int
  Ycoord :: int

text {* the manual way *}
function
  swp :: "point \<Rightarrow> point"
where
  "swp \<lparr> Xcoord = x, Ycoord = y \<rparr> = \<lparr> Xcoord = y, Ycoord = x \<rparr>"
proof -
  fix P x
  assume "\<And>xa y. x = \<lparr>Xcoord = xa, Ycoord = y\<rparr> \<Longrightarrow> P"
  thus "P" by (cases x)
qed auto
(* alternatively prove whole thing by (auto split: point.splits) *)
termination by lexicographic_order

text {* make Isabelle treat the record as datatype first: *}
rep_datatype point_ext
  by (auto intro: point.ext_induct point.ext_inject)

text {* then automatic: *}
fun swp2 where
  "swp2 \<lparr> Xcoord = x, Ycoord = y \<rparr> = (y,x)"

print_theorems

-- -------------------------------------------------------------

text {* partial functions, with tail recursion *}

partial_function (tailrec) fixp where
  "fixp f x = (if f x = x then x else fixp f (f x))"

print_theorems

declare fixp.simps [code]
value "fixp (\<lambda>x. x - 1) (7::nat)"


-- -------------------------------------------------------------

text {* congruence rules *}

thm if_cong map_cong

function foo :: "nat \<Rightarrow> nat" where
  "foo x = (if x = 0 then 0 else foo (x - 1))"
  by pat_completeness auto

termination
  apply (relation "measure size")
  (* knows that for recursive call x \<noteq> 0 *)
  apply auto
  done

primrec
  othermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
  "othermap f [] = []" |
  "othermap f (x#xs) = f x # othermap f xs"

(* fun treemap2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
where
  "treemap2 fn (Leaf n) = (Leaf (fn n))"
| "treemap2 fn (Branch l) = (Branch (othermap (treemap2 fn) l))"
(* fails *) *)

function treemap2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> '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]:
  "\<lbrakk> xs = ys; \<And>x. x \<in> set ys \<Longrightarrow> f x = g x \<rbrakk>
  \<Longrightarrow> othermap f xs = othermap g ys"
  by (induct xs arbitrary: ys) auto

fun treemap3 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
where
  "treemap3 fn (Leaf n) = (Leaf (fn n))"
| "treemap3 fn (Branch l) = (Branch (othermap (treemap3 fn) l))"

end