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! *)
  apply auto
  done


\<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)"

value "ack 2 2"

\<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"

text \<open>when termination fails:\<close>

(* This one will give an error message: *)
fun nonterm :: "nat \<Rightarrow> nat" where
  "nonterm x = nonterm (x + 1)"

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

(* 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 \<open>use the fully tweakable function form instead:\<close>

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




(* -------------------------------------------------------------- *)

(* 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 \<times> 'a list) \<times> 'a list) set" where
  "((a,[]),[]) \<in> my_sep_rel"
| "((a,[x]),[x]) \<in> my_sep_rel"
| "((a,y#l),l') \<in> my_sep_rel \<Longrightarrow> ((a,x#y#l),x#a#l') \<in> my_sep_rel"

(* Prove that the relation is unique and total (\<exists>! means "exists a unique")
 *)
lemma my_sep_rel_unique: "\<exists>!y. ((a, l), y) \<in> 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 \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "my_sep \<equiv> \<lambda>a x. THE y. ((a,x),y) \<in> 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:  "\<And>a. P a []"
      and one:  "\<And>a x. P a [x]"
      and cons: "\<And>a x y l. P a (y#l) \<Longrightarrow> P a(x#y#l)"
    shows "P a l"
proof -
  obtain y where "((a,l), y) \<in> 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


(* ------------------------------------------------------------------ *)

section "More tweaks"
\<comment> \<open> see also src/HOL/ex/Fundefs.thy \<close>

subsubsection \<open>Overlapping patterns\<close>

text \<open>Patterns may overlap if compatible:\<close>

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 \<open>Guards\<close>

text \<open>We can reformulate the above example using guarded patterns\<close>

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

print_theorems

termination by lexicographic_order

thm gcd3.simps
thm gcd3.induct


text \<open>General patterns:\<close>

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 \<open>Mutual Recursion\<close>

fun evn od :: "nat \<Rightarrow> bool"
where
  "evn 0 = True"
| "evn (Suc n) = od n"

| "od 0 = False"
| "od (Suc n) = evn n"

print_theorems

thm evn.simps
thm od.simps

thm evn_od.induct

text \<open>Simple Higher-Order Recursion\<close>
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 \<open>congruence rules\<close>

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 "measure f")
   defer
  apply simp
  (* 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