theory week07B_demo imports Main begin

primrec sep
where
  "sep a [] = []"
 |"sep a [x] = [x]"
 |"sep a (x#xs) = x#a#(sep a xs)"

\<comment> \<open>arbitrary patterns\<close>
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

\<comment> \<open>symbolic execution\<close>
lemma "sep a [x,y,z] = blah"
  apply simp
  oops

\<comment> \<open>with code generation\<close>
  value "sep a [x,y,z]"

\<comment> \<open>tailored induction principle:\<close>
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 for A where
  "([],[]) \<in> my_sep_rel A"
| "([x],[x]) \<in> my_sep_rel A"
| "(y#l,l') \<in> my_sep_rel A \<Longrightarrow> (x#y#l,x#A#l') \<in> my_sep_rel A"

(* Prove that the relation is unique and total (\<exists>! means "exists a unique")
 *)
lemma my_sep_rel_unique: "\<exists>!y. (l, y) \<in> my_sep_rel A"
  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

(* Declare a new constant my_sep, about which we initially know nothing
   except its type. Note that at the lowest level, declaring a new constant
   is decoupled from giving it a definition.
 *)
consts
 my_sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"

(* Give my_sep a definition by specification; that is, let 
   my_sep be a function that satisfies the predicates
   my_sep1 and my_sep2, given a proof that such a function
   exists.

   The witness to this function's existence Hilbert-chooses the
   RHS from the relevant element of the graph relation my_sep_rel.
 *)
specification(my_sep)
 my_sep_simp1[simp]:
   "my_sep a [] = []"
 my_sep_simp2[simp]:
   "my_sep a [x] = [x]"
 my_sep_simp3[simp]:
   "my_sep a (x#y#l) = (x#a#my_sep a (y#l))"
  apply(rule exI[where x="\<lambda>a x. THE y. (x,y) \<in> my_sep_rel a"])
  apply(subst my_sep_rel.simps,simp)
  apply(rule conjI)
   apply(rule allI)+
   apply(rule the1_equality[OF my_sep_rel_unique])
   apply(rule my_sep_rel.intros)
  apply(rule allI)+
  apply(rule the1_equality[OF my_sep_rel_unique])
  apply(rule the1I2[OF my_sep_rel_unique])
  by(rule my_sep_rel.intros)

print_theorems

(* 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

\<comment> \<open> can leave type to be inferred:\<close>
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)"

\<comment> \<open> nested recursion -> induction principle that mentions ack again:\<close>
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]"
  \<comment> \<open> need to prove completeness and distinctness of patterns \<close>
     apply pat_completeness
    apply simp
   apply simp
  apply simp
  done

\<comment> \<open> get only partial simp and induction rules \<close>

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


\<comment> \<open> now have full induction and simp available \<close>
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"
\<comment> \<open> see also src/HOL/ex/Fundefs.thy \<close>

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
thm tinc.induct

text {* congruence rules *}

thm if_cong map_cong

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

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

termination
  apply (relation "R") (*now we have enough information *)
  sorry

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

end