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
  non-deterministic functions inductively. As a case-study we consider 
  a non-determistic version of quick-sort where the pivot element can
  be chosen arbitrary.\<close>

inductive qsortp :: "int list \<Rightarrow> int list \<Rightarrow> bool" where
  qsNil: "qsortp [] []" 
| qsCons: "i < length xs \<comment> \<open>choose position of pivot element\<close>
  \<Longrightarrow> x = xs ! i 
  \<Longrightarrow> ys = take i xs @ drop (Suc i) xs
  \<Longrightarrow> qsortp (filter (\<lambda> y. y \<le> x) ys) low
  \<Longrightarrow> qsortp (filter (\<lambda> y. \<not> y \<le> x) ys) high
  \<Longrightarrow> qsortp 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! 
  Carefully choose a suitable induction principle for each task.\<close>

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

text \<open>Prove that @{const qsortp} preserves the set of elements.\<close>

lemma qsortp_set: "qsortp xs res \<Longrightarrow> set res = set xs" sorry

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

text \<open>Prove that @{const qsortp} produces a sorted list.\<close>

lemma qsortp_sorted: "qsortp xs res \<Longrightarrow> sorted res" sorry

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

fun qsort :: "int list \<Rightarrow> int list" where
  "qsort [] = []" 
| "qsort (x # xs) = qsort (filter (\<lambda> y. y \<le> x) xs) @ x # qsort (filter (\<lambda> y. \<not> y \<le> x) xs)" 

text \<open>Prove that the determistic algorithm @{const qsort} is a refinement of @{const qsortp},
 i.e., it can be simulated by the non-determistic one.\<close>

lemma qsort_qsortp: "qsort xs = res \<Longrightarrow> qsortp xs res" sorry
  
text \<open>As a consequence of the refinement proof, we are able to easily 
  derive that the deterministic quick-sort algorithm has the nice properties.\<close>

lemma set_qsort: "set (qsort xs) = set xs" 
  using qsortp_set[OF qsort_qsortp] by blast

lemma sorted_qsort: "sorted (qsort xs)" 
  using qsortp_sorted[OF qsort_qsortp] by blast


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