qsort.thy

theory qsort
imports Main
begin

fun qsort :: "nat list ⇒ nat list" where
  "qsort [] = []"
| "qsort (x#xs) = qsort [y←xs. y < x] @ [x] @ qsort [y←xs. x ≤ y]"

inductive inc :: "nat list ⇒ bool" where
  inc_nil: "inc []"
| inc_singleton: "inc [x]"
| inc_cons: "⟦ x ≤ y; inc (y#ys) ⟧ ⟹ inc (x#y#ys)"

lemma inc_cons_inv: "inc (x#y#ys) ⟹ x ≤ y ∧ inc (y#ys)"
by (cases rule: inc.cases, simp, simp, simp, simp)

lemma inc_uncons:
  fixes x :: nat and xs :: "nat list"
  assumes "inc (x#xs)"
  shows "⋀y. y ∈ set xs ⟹ x ≤ y" and "inc xs"
using assms
apply (induct xs, simp)
apply (rule, auto)
using inc_cons_inv apply blast
proof -
  fix a :: nat and xsa :: "nat list" and y :: nat
  assume a1: "⋀y. ⟦y ∈ set xsa; inc (x # xsa)⟧ ⟹ x ≤ y"
  assume a2: "inc (x # a # xsa)"
  assume a3: "y ∈ set xsa"
  have "∀n ns. (n::nat) ∉ set ns ∨ (∃nsa. ns = n # nsa) ∨ (∃na nsa. ns = na # nsa ∧ n ∈ set nsa)"
    by (meson list.set_cases)
  then obtain nns :: "nat ⇒ nat list ⇒ nat list" and nn :: "nat ⇒ nat list ⇒ nat" and nnsa :: "nat ⇒ nat list ⇒ nat list" where
    "nn y xsa # nnsa y xsa = xsa ∨ y # nns y xsa = xsa"
    using a3 by (metis (no_types))
  then have "y # nns y xsa = xsa ∨ inc (x # xsa)"
    using a2 by (metis inc_cons inc_cons_inv le_trans)
  then show "x ≤ y"
    using a3 a2 a1 by (metis inc_cons_inv le_trans)
next
  fix a xs
  show "(⋀y. y ∈ set xs ⟹ inc (x # xs) ⟹ x ≤ y) ⟹
  (inc (x # xs) ⟹ inc xs) ⟹ inc (x # a # xs) ⟹ inc (a # xs)"
    using inc_cons_inv by blast
qed    

lemma inc_append_l: "⟦ inc xs; (⋀x. x ∈ set xs ⟹ y ≤ x) ⟧ ⟹ inc (y # xs)"
by (induct xs, rule, rule, simp, simp)

lemma inc_append_r: "⟦ inc xs; (⋀x. x ∈ set xs ⟹ x ≤ y) ⟧ ⟹ inc (xs @ [y])"
proof (induct xs, simp, rule)
  fix a xs
  assume hyp: "inc xs ⟹ (⋀x. x ∈ set xs ⟹ x ≤ y) ⟹ inc (xs @ [y])" "inc (a # xs)" "⋀x. x ∈ set (a # xs) ⟹ x ≤ y"
  have "⟦ inc (a # xs); ⋀x. x ∈ set (a # xs) ⟹ x ≤ y; inc xs ⟹ (⋀x. x ∈ set xs ⟹ x ≤ y) ⟹ inc (xs @ [y]) ⟧ ⟹ inc ((a # xs) @ [y])"
    apply (induct xs, simp, rule, simp, rule)
    apply (simp, rule)
    using inc_cons_inv apply auto[1]
    using inc_cons_inv apply blast
    done
  thus "inc ((a # xs) @ [y])"
    using hyp by simp
qed

lemma inc_append_lr: "⟦ inc (xs @ [z]); inc (z # ys) ⟧ ⟹ inc (xs @ z # ys)"
apply (induct xs, simp)
apply (simp, rule inc_append_l)
using inc_uncons(2) apply blast
apply (metis Un_iff in_set_conv_decomp inc_cons inc_uncons(1) set_append)
done

primrec count :: "'a list ⇒ 'a ⇒ nat" where
  "count [] a = 0"
| "count (x#xs) a = (if x = a then 1 else 0) + count xs a"

lemma append_count: "count (xs @ ys) a = count xs a + count ys a"
by (induct xs, simp, simp)

lemma count_split_filter:
  fixes xs :: "nat list"
  shows "count xs a = count [x←xs. x < y] a + count [x←xs. y ≤ x] a"
by (induct xs, simp, auto)

definition perm :: "'a list ⇒ 'a list ⇒ bool" where
  "perm xs ys == (∀a. count xs a = count ys a)"

lemma pm_refl: "perm xs xs"
apply (induct xs, unfold perm_def, simp)
apply (auto)
done

lemma pm_cons:
  assumes "perm xs ys"
  shows "perm (z#xs) (z#ys)"
using assms unfolding perm_def
apply auto
done

theorem well_sorted:
  fixes xs :: "nat list"
  shows "inc (qsort xs) ∧ perm xs (qsort xs)"
proof-
  { fix m
    have "⋀(xs :: nat list). length xs = m ⟹ inc (qsort xs) ∧ set (qsort xs) = set xs"
      proof (induct m rule: nat_less_induct)
        fix n and xs :: "nat list"
        assume hyp: "∀m<n. ∀x. length x = m ⟶ inc (qsort x) ∧ set (qsort x) = set x"
        show "length xs = n ⟹ inc (qsort xs) ∧ set (qsort xs) = set xs"
          apply (cases xs, simp, rule, simp, rule)
          apply (rule inc_append_lr)
            apply (rule inc_append_r)
            using hyp apply (metis le_imp_less_Suc length_filter_le)
            using hyp apply (metis filter_set le_imp_less_Suc length_filter_le less_imp_le_nat member_filter)
            apply (rule inc_append_l)
            using hyp apply (metis le_imp_less_Suc length_filter_le)
            using hyp apply (metis filter_set le_imp_less_Suc length_filter_le member_filter)
          apply (rule, simp, rule)
            using hyp apply (metis filter_is_subset le_imp_less_Suc length_filter_le subset_insertI2)
            using hyp apply (metis filter_is_subset le_imp_less_Suc length_filter_le subset_insertI2)
            apply rule
            apply (metis UnI1 UnI2 filter_set hyp insert_iff leI le_imp_less_Suc length_filter_le member_filter)
          done
      qed
  }
  hence "inc (qsort xs)"
    by auto
    
  moreover have "perm xs (qsort xs)"
    proof-
      { fix m
        have "⋀(xs :: nat list). length xs = m ⟹ perm xs (qsort xs)"
          proof (induct m rule: nat_less_induct)
            fix n and xs :: "nat list"
            assume hyp: "∀m<n. ∀x. length x = m ⟶ perm x (qsort x)"
            show "length xs = n ⟹ perm xs (qsort xs)"
              apply (cases xs, simp, rule pm_refl, simp)
              apply (unfold perm_def, auto)
              apply (simp add: append_count)
                apply (subst count_split_filter)
                using hyp apply (metis count_split_filter le_imp_less_Suc length_filter_le perm_def)
              apply (simp add: append_count)
              apply (subst count_split_filter)
              using hyp apply (metis count_split_filter le_imp_less_Suc length_filter_le perm_def) 
              done
          qed
      }
      thus "perm xs (qsort xs)" by simp
    qed
  
  ultimately show ?thesis by simp
qed

end