theory Exercise05
  imports Main
begin

text \<open>On this exercise sheet we will define and prove soundness of bubble-sort.\<close>

fun bubble :: "'a :: linorder list \<Rightarrow> 'a list" where 
  "bubble (x # y # ys) = (case bubble (y # ys) of z # zs \<Rightarrow> 
      if x < z then x # z # zs else z # x # zs)" 
 | "bubble xs = xs" 

function (sequential) bsort where
  "bsort [] = []" 
| "bsort xs = (case bubble xs of y # ys \<Rightarrow> y # bsort ys)" 
  by pat_completeness auto

section \<open>Exercise 1 -- 3 points\<close>

text \<open>Complete the termination of @{const bsort}. 
  To this end, you also need to prove a suitable property about @{const bubble}.\<close>

termination 
proof (relation "measure length")
  fix x y :: 'a and xs ys
  assume "bubble (x # xs) = y # ys"   
  show "(ys, x # xs) \<in> measure length" sorry
qed auto

section \<open>Exercise 2 -- 2 points\<close>

text \<open>Prove that @{const bsort} preserves the set of elements. 
  We already provide a similar lemma for @{const bubble}.\<close>
lemma set_bubble[simp]: "set (bubble xs) = set xs"
proof (induction xs rule: bubble.induct)
  case (1 x y ys)
  thus ?case by (cases "bubble (y # ys)") auto
qed auto

lemma set_bsort[simp]: "set (bsort xs) = set xs"
  sorry

section \<open>Exercise 3 -- 3 points\<close>

text \<open>Prove that @{const bubble} moves the smallest element to the front. 
  This is the most difficult proof on this exercise sheet.

  Important: you most likely will have to manually instantiate @{thm set_bubble} for 
  exercises 3 and 4.\<close>

lemma bubble_first_least: "bubble xs = y # zs \<Longrightarrow> \<forall> e \<in> set zs. y \<le> e" 
proof (induct xs arbitrary: y zs rule: bubble.induct)
  case (1 x y ys z zs)
  obtain u us where bubble: "bubble (y # ys) = u # us" sorry
  from 1(2) bubble 
  have result: "z # zs = (if x < u then x # u # us else u # x # us)" by auto
  show ?case sorry (* using some intermediate facts by (cases "x < u") auto *)
qed auto

section \<open>Exercise 4 -- 2 points\<close>

text \<open>Prove that bsort sorts a list. You can use all previously stated lemmas,
  even if you did not prove them.\<close>

lemma bsort: "sorted (bsort xs)" 
  sorry
end