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 \<Rightarrow> 'a list \<Rightarrow> '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 (\<lambda>x. P x) xs = [x \<leftarrow> xs. P x]" by (rule refl)

text {* when termination fails: *}

(* This one will give an error message:
fun nonterm :: "nat \<Rightarrow> 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 \<leftarrow> xs. y \<le> x] @ [x] @ quicksort [y \<leftarrow> xs. x < y]"
*)


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

function  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")
    apply simp
   apply simp
   apply (simp add:less_Suc_eq_le)
  apply simp
  apply (simp add:less_Suc_eq_le)
  (*or: by (relation "measure length", simp_all add: 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"
  (*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 \<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))"


print_theorems
thm gcd2.simps
thm gcd2.induct

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"
  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 \<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)"
print_theorems
(*
text {* 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>"
   apply simp_all
   apply (case_tac x, simp)
   done
termination by lexicographic_order

text {* Isabelle treat the record as datatype *}
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