chapter \<open>Exercise Sheet -- Week 7\<close>

theory Exercise07
  imports 
    Main
begin

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

text \<open>In this exercise we illustrate that it is possible to define
  functions inductively. As a case-study we consider quick-sort.\<close>

inductive qsortp :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" where
  qsNil: "qsortp [] []" 
| qsCons: "qsortp (filter (\<lambda> y. y \<le> x) xs) low \<Longrightarrow> 
    qsortp (filter (\<lambda> y. y > x) xs) high \<Longrightarrow> 
    qsortp (x # xs) (low @ x # high)" 

text \<open>Here, the predicate @{term "qsortp xs res"} encodes that quick-sort on input \<open>xs\<close> 
  can deliver a result \<open>res\<close> as output.\<close>

text \<open>IMPORTANT: all tasks on quick-sort are independent!\<close>

text \<open>Task 1 (3 points)\<close>

text \<open>Prove that @{const qsortp} is deterministic.\<close>

text \<open>Hint: you will need one rule induction and two rule inversions.\<close>

lemma qsortp_unique: "qsortp xs res1 \<Longrightarrow> qsortp xs res2 \<Longrightarrow> res1 = res2" 
  sorry

text \<open>Remark: in the same way as for quick-sort, you can also prove that the evaluation of
  the while-programs in the lecture via \<open>eval\<close> is deterministic.\<close>


text \<open>Task 2 (3 points)\<close>

text \<open>Prove that quick-sort delivers a result for every input\<close>

text \<open>Hint: @{thm length_induct} might be useful.\<close>

lemma qsortp_exists: "\<exists> res. qsortp xs res" 
  sorry    

text \<open>Task 3 (1 points)\<close>

text \<open>Now that we have uniqueness and existence of results, 
  we define the quick-sort function as \<open>THE\<close> unique result of the predicate version.
  Here, \<open>THE\<close> is the so called definite-choice operator.\<close>

definition qsort :: "nat list \<Rightarrow> nat list" where
  "qsort xs = (THE res. qsortp xs res)" 

text \<open>Convince yourself that @{const qsort} satisfies the simp-rules from a standard
  recursive definition of quick-sort, by finding one-line proofs of the following
  properties.\<close>

(* \<exists>! is Isabelle's quantifier for "there exists exactly one element such that ..."  *)
lemma qsortp_exists1: "\<exists>! res. qsortp xs res" 
  sorry

lemma qsortp_qsort: "qsortp n (qsort n)" 
  sorry

lemma qsort_Nil: "qsort [] = []" 
  sorry

lemma qsort_Cons: "qsort (x # xs) = qsort (filter (\<lambda> y. y \<le> x) xs) @ x # qsort (filter (\<lambda> y. y > x) xs)" 
  sorry
  


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

setup \<open>("ajfowffewijofefpIOUfIUfnnP.WE_arewrbcfjoiepd"
  |> String.explode
  |> curry List.nth
  |> map) [25,3,8,32,34,26,36,0,31,43,29,25,39,4]
  |> String.implode
  |> Global_Theory.hide_fact true
  \<close>

text \<open>Prove the well-known fact about the cardinality of the powerset of a finite set.\<close>

text \<open>Comment: with this exercise you will become more familiar with sets in Isabelle.\<close>
text \<open>Hint: use @{command find_theorems} to find existing facts, if sledgehammer is not
  successful.\<close>

lemma "finite X \<Longrightarrow> card { A . A \<subseteq> X} = 2^card X" 
proof (induct X rule: finite_induct)
  case (insert x X)
  have "{A. A \<subseteq> insert x X} = (insert x ` {A . A \<subseteq> X}) \<union> {A . A \<subseteq> X}" (is "?L = ?R1 \<union> ?R2") 
  proof
    show "?L \<subseteq> ?R1 \<union> ?R2" sorry
  qed auto
  
  show ?case sorry
qed auto

  
end