theory Exercise10
  imports Main
begin

text \<open>Many of the types and algorithms exist already in the
  standard Isabelle library. We hide existing constants and develop
  everything from scratch.\<close>

hide_const plus times set Nil Cons append insort sort length

(* this is a comment *)

text \<open>Proofs from the lecture\<close>

datatype Nat = Zero | Succ Nat

fun plus :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat" where
  "plus Zero y = y" 
| "plus (Succ x) y = Succ (plus x y)" 


fun times :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat" where
  "times Zero y = Zero" 
| "times (Succ x) y = plus y (times x y)" 

(* we prove the lemma and via [simp] tell Isabelle to always use it for simplification *)
lemma Zero_right_neutral[simp]: "plus x Zero = x" 
  by (induction x) simp_all

(* the next property we do not add for global simplifications, i.e., no [simp] attribute *)
lemma plus_right_Succ: "plus x (Succ y) = Succ (plus x y)" 
  by (induction x arbitrary: y) simp_all

(* the next lemma is in a style where we locally step through the proof by 
   a sequence of apply-commands, finalized with "done" *)
lemma plus_comm: "plus x y = plus y x" 
proof (induction x arbitrary: y)
  (* click in the output window in the blue part to get an outline after the induction method *)
  case Zero
  then show ?case by simp
next
  case (Succ x y)
  (* IH is made available via "then show", "using Succ.IH" or "simp add: Succ.IH" *)
  (* one can inspect it via thm *)
  thm Succ.IH
  show ?case 
    apply simp
    apply (simp add: Succ.IH) (* locally use IH *)
    apply (simp add: plus_right_Succ) (* locally use lemma in this proof-step *)
    done (* close proof via done *)
qed 

(* we now perform a proof by a sequence of equalities with explicit intermediate terms;
   such a proof might be necessary, if unrestricted simplification does too much *)
lemma plus_comm2: "plus x y = plus y x" 
proof (induction x arbitrary: y)
  case (Succ x y)
  have "plus (Succ x) y = Succ (plus x y)" by simp (* initial equation *)
  also have "\<dots> = Succ (plus y x)" using Succ.IH by simp (* further equation with "also have" *)
  also have "\<dots> = plus y (Succ x)" by (simp add: plus_right_Succ)
  finally show ?case by simp (* "finally" combines all equations by transitivity *)
qed simp_all (* remaining cases (here: Zero) are solved by simp_all *)




section \<open>Exercise 1\<close>

text \<open>Consider the insertion sort algorithm from the lecture, where now we use Isabelle's built-in 
  Boolean's and built-in if-then-else.\<close>

datatype List = Nil | Cons Nat List

fun le :: "Nat \<Rightarrow> Nat \<Rightarrow> bool" where
  "le Zero y = True" 
| "le (Succ x) Zero = False" 
| "le (Succ x) (Succ y) = le x y" 

fun insort :: "Nat \<Rightarrow> List \<Rightarrow> List" where
  "insort x Nil = Cons x Nil" 
| "insort x (Cons y ys) = (if le x y then Cons x (Cons y ys) else Cons y (insort x ys))"

fun sort :: "List \<Rightarrow> List" where
  "sort Nil = Nil" 
| "sort (Cons x xs) = insort x (sort xs)" 

subsection \<open>Task 1.1 - 2 points\<close>

text \<open>Specify and prove that @{const sort} preserves the length of the input list\<close>





subsection \<open>Task 1.2 - 2 points\<close>

text \<open>Specify and prove that @{const sort} preserves the set of elements of a list\<close>

text \<open>Hint 1: The primitives @{term "insert :: 'a \<Rightarrow> 'a set \<Rightarrow> 'a set"} and
  @{term "{} :: 'a set"} might be useful.\<close>

text \<open>Hint 2: Have a look at Demo05.thy for the syntax of a case-analysis, cf. lemma sorted_insort.
  Perform explicit equational reasoning steps if you get stuck, and prove them by "sorry" as in 

  have "a = b" by simp
  also have "... = c" by (simp add: IH some_lemma)
  also have "... = d" sorry (* this step was not possible for some reason *)
  also have "... = e" by simp
  finally show "a = e" by simp
\<close>




subsection \<open>Task 1.3 - 2 points\<close>

text \<open>Consider Quicksort\<close>

fun low :: "Nat \<Rightarrow> List \<Rightarrow> List" where
  "low p (Cons x xs) = (if le x p then Cons x (low p xs) else low p xs)" 
| "low p Nil = Nil" 

fun high :: "Nat \<Rightarrow> List \<Rightarrow> List" where
  "high p (Cons x xs) = (if le x p then high p xs else Cons x (high p xs))" 
| "high p Nil = Nil" 

fun app :: "List \<Rightarrow> List \<Rightarrow> List" where
  "app (Cons x xs) ys = Cons x (app xs ys)" 
| "app Nil ys = ys"

function quick_sort :: "List \<Rightarrow> List" where
  "quick_sort Nil = Nil"
| "quick_sort (Cons x xs) = app (quick_sort (low x xs)) (Cons x (quick_sort (high x xs)))" 
  by pat_completeness auto

termination sorry (* ignore this sorry, we here just assume termination *)

text \<open>Specify and prove that @{const quick_sort} preserves the length of a list.\<close>

text \<open>Hint: You might want to start your main proof by something similar to: 

  proof (induction xs rule: quick_sort.induct)

\<close>

end