theory LiveDemo04
  imports 
    Main
    "HOL-Library.Multiset" 
begin

section \<open>Gauß' Formula: Use Chains of Equality\<close>

fun sum_nats :: "nat \<Rightarrow> nat" where
  "sum_nats 0 = 0" 
| "sum_nats (Suc n) = Suc n + sum_nats n" 

lemma Gauss: "sum_nats n = (n * Suc n) div 2"
proof (induction n)
  case (Suc n)
  have "sum_nats (Suc n) = Suc n + sum_nats n" by simp
  also have "sum_nats n = (n * Suc n) div 2" using Suc by simp
  also have "Suc n + \<dots> = (2 * Suc n + n * Suc n) div 2" by simp
  also have "2 * Suc n + n * Suc n = Suc n * Suc (Suc n)" by simp
  finally show ?case .
qed auto



section \<open>Fast Reversal: Use arbitrary variables\<close>

text \<open>Isabelle has already a defined append function @{const append}
  which usually written in infix notion: @{term "xs @ ys"}.
  (Haskell's ++ = Isabelle's @)\<close>

fun reverse :: "'a list \<Rightarrow> 'a list" where
  "reverse [] = []"  
| "reverse (x # xs) = reverse xs @ [x]"

fun rev_it :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "rev_it [] ys = ys" 
| "rev_it (x # xs) ys = rev_it xs (x # ys)" 

fun fast_rev :: "'a list \<Rightarrow> 'a list" where
  "fast_rev xs = rev_it xs []" 

lemma fast_rev: "fast_rev xs = reverse xs" 
proof -
  have "rev_it xs [] = reverse xs" 
  proof (induction xs)
    case (Cons x xs)
    then show ?case proof simp
      oops

lemma rev_it[simp]: "rev_it xs ys = reverse xs @ ys" 
proof (induction xs arbitrary: ys)
  case (Cons x xs zs)
  have "rev_it (x # xs) zs = rev_it xs (x # zs)" by simp
  also have "\<dots> = reverse xs @ x # zs" unfolding Cons by simp
  also have "\<dots> = reverse (x # xs) @ zs" by simp
  finally show ?case .
qed auto

lemma fast_rev: "fast_rev xs = reverse xs" 
  by simp

text \<open>Since we have proven a faster implementation of reverse, 
  we can now tell the system to use it via a [code] attribute.\<close>


export_code reverse in Haskell 

lemma implement_rev_by_fast_rev[code]: "reverse xs = fast_rev xs" 
  by (auto simp: fast_rev)

export_code reverse in Haskell 

text \<open>Advantage: we can have two versions of an algorithm:
 \<^item> @{const reverse} has a structure which makes it easy to reason about
 \<^item> @{const fast_rev} is better in generated code\<close>



section \<open>Controlled Proof Search\<close>

lemma Gauss_2: "sum_nats n = (n * Suc n) div 2"
proof (induction n)
  case (Suc n)
  show ?case 
    unfolding sum_nats.simps
    unfolding Suc.IH
    by simp
qed auto


text \<open>After successful proof search, one might turn apply-style proof into more
  readable structured proof.\<close>


section \<open>Insertion Sort: Induction with Implications\<close>

fun insert_sorted :: "'a :: linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "insert_sorted x Nil = Cons x Nil" 
| "insert_sorted x (Cons y ys) = (if x \<le> y 
    then Cons x (Cons y ys)
    else Cons y (insert_sorted x ys))" 

fun ins_sort :: "'a :: linorder list \<Rightarrow> 'a list" where
  "ins_sort Nil = Nil" 
| "ins_sort (Cons x xs) = insert_sorted x (ins_sort xs)" 

text \<open>Previous exercise: development of proof that length is preserved.\<close>

text \<open>Now: prove that result is @{const sorted}.\<close>

lemma sorted_insert_sorted: "sorted xs \<Longrightarrow> sorted (insert_sorted x xs)" 
proof (induction xs)
  case (Cons y xs)
  thm Cons.IH (* induction hypthesis via .IH *)
  thm Cons.prems (* premises via .prems *)
  from Cons   (* everything with .IH or .prems *) 
  have IH: "sorted (insert_sorted x xs)" by auto
  show ?case 
  proof (cases "x \<le> y")
    case True
    have "insert_sorted x (y # xs) = x # y # xs" using True by simp
    also have "sorted \<dots>" using Cons.prems True by auto
    finally show "sorted (insert_sorted x (y # xs))" .
  next
    case False
    have "insert_sorted x (y # xs) = y # insert_sorted x xs" using False 
      by simp
    also have "sorted \<dots> = ((\<forall>z\<in>set (insert_sorted x xs). y \<le> z) \<and> sorted (insert_sorted x xs))" by simp
    also have "sorted (insert_sorted x xs) = True" using IH by simp
    also have "set (insert_sorted x xs) = set (x # xs)" 
      by (induction xs) auto
    also have "(\<forall>z\<in>set (x # xs). y \<le> z) = True" 
      using False \<open>sorted (y # xs)\<close> by auto  
    finally show ?thesis by simp
  qed
qed auto


text \<open>Now soundness of insertion sort is easy, using 
  @{thm sorted_insert_sorted} as conditional(!) simp rule.\<close>
declare sorted_insert_sorted[simp]

lemma sorted_ins_sort: "sorted (ins_sort xs)" 
  by (induction xs) auto

text \<open>Conditional simplification rules naturally appear also in
  arithmetic reasoning, e.g. @{thm mult_le_cancel_left_pos}\<close>


text \<open>Just for illustration purposes: soundness of insert_sorted using purely apply-style.\<close>

lemma set_insert_sorted: "set (insert_sorted x xs) = set (x # xs)"
  apply (induction xs)
   apply auto
  done

lemma sorted_insert_sorted_apply_style: "sorted xs \<Longrightarrow> sorted (insert_sorted x xs)"
  apply (induction xs)
  subgoal by simp   (* Nil-Case *)
  subgoal for y xs  (* fix variables for Cons-case *)
    apply (cases "x \<le> y")
    subgoal by auto  (* trivial case: x \<le> y *)
    apply auto (* detect required lemma *)
    apply (subst (asm) set_insert_sorted)
    apply auto 
    done
  done

text \<open>Another illustration: soundness of insert_sorted using mixture of
  apply-style and Isar-style.\<close>
lemma sorted_insert_sorted_mixed_style: "sorted xs \<Longrightarrow> sorted (insert_sorted x xs)"
  apply (induction xs)
  subgoal by simp 
  subgoal for y xs 
    apply (cases "x \<le> y")
    subgoal by auto 
    apply auto (* not to be done! *)
  proof (goal_cases) (* switch to Isar via goal_cases, each subgoal gets a number *)
    case (1 z)
    have eq: "set (insert_sorted x xs) = set (x # xs)" 
      by (induction xs) auto
    show ?case using 1 unfolding eq by auto
  qed
  done

text \<open>Preservation of elements is trivially expressed via multisets.\<close>
lemma mset_insert_sorted[simp]: "mset (insert_sorted x xs) = mset (x # xs)"
  by (induction xs) auto

lemma mset_ins_sort[simp]: "mset (ins_sort xs) = mset xs"
  by (induction xs) auto

text \<open>Insertion sort is the same as Isabelle's @{const sort} function
  (actually every correct sorting algorithm has the same functional
   behavior as @{const sort}.)\<close>
lemma "sort xs = ins_sort xs" 
proof (rule properties_for_sort)
  show "mset (ins_sort xs) = mset xs" by auto
  show "sorted (ins_sort xs)" by (rule sorted_ins_sort)
qed

end