theory Demo102 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

-- "tailored induction principle:"
lemma "map f (sep x xs) = sep (f x) (map f xs)"
  apply (induct x xs rule: sep.induct)
  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"
  oops

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

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

-- "when termination fails:"

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


-- "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"
  by pat_completeness auto

(*
     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 (auto simp: less_Suc_eq_le)
  done

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

lemma set_quicksort:
  "set (quicksort xs) = set xs"
  oops


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

subsubsection {* Overlapping patterns *}

text {* Currently, patterns must always be compatible with each other, since
no automatic splitting takes place. But may patterns 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 (case_tac x, case_tac a, auto)
  apply (case_tac ba, auto)
  done
termination by lexicographic_order

thm gcd3.simps
thm gcd3.induct


text {* General patterns allow even strange definitions: *}

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 *} 
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"

thm evn.simps
thm od.simps

thm evn_od.induct



(* Simple Higher-Order Recursion *)
datatype 'a tree = 
  Leaf 'a 
  | Branch "'a tree list"

lemma lem:"x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)"
by (induct l, auto)

function 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))"
by pat_completeness auto
termination by (lexicographic_order simp:lem)

declare lem[simp]

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


(* Pattern matching on records *)
record point =
  Xcoord :: int
  Ycoord :: int

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
termination by rule auto

end