PFAD, Chapter 1-1

PFAD.thy

theory PFAD
imports Main
begin

fun maximum where
  "maximum xs = foldr max xs 0"

lemma maximum_larger: "xs ≠ [] ⟹ (⋀x :: nat. x ∈ set xs ⟹ x ≤ maximum xs)"
proof (induct xs, simp, auto)
  fix a :: nat and xs :: "nat list" and x
  assume a: "⋀x. xs ≠ [] ⟹ x ∈ set xs ⟹ x ≤ foldr max xs 0" "x ∈ set xs"
  from a(2) have 1: "xs ≠ []" by auto
  have "x ≤ maximum xs" using a(1) by (simp add: 1 a(2))
  thus "x ≤ max a (foldr max xs 0)" by simp
qed

lemma maximum_suc_notin: "xs ≠ [] ⟹ (maximum xs + (1 :: nat) ∉ set xs)"
proof-
  assume a: "xs ≠ []"
  have 1: "⋀x. x ∈ set xs ⟹ x ≠ maximum xs + (1 :: nat)"
    apply (rule less_imp_neq)
    using maximum_larger [OF a] by fastforce
  show "maximum xs + (1 :: nat) ∉ set xs"
    using 1 by auto
qed

primrec remove where
  "remove [] ys = []"
  | "remove (x # xs) ys = (if x ∈ set ys then remove xs ys else x # remove xs ys)"

lemma after_removing: "⋀x. x ∈ set (remove xs ys) ⟹ x ∉ set ys"
proof (induct xs, simp, simp)
  fix a xs x
  assume a: "⋀x. x ∈ set (remove xs ys) ⟹ x ∉ set ys"
            "x ∈ set (if a ∈ set ys then remove xs ys else a # remove xs ys)"
  show "x ∉ set ys"
    apply (cases "a ∈ set ys")
      using a(2) apply (simp add: a(1))
      using a(2) apply (simp, auto simp add: a(1))
    done
qed

lemma remove_stable: "⋀x. ⟦ x ∈ set xs; x ∉ set ys ⟧ ⟹ x ∈ set (remove xs ys)"
by (induct xs, auto)

lemma remove_subset: "set (remove xs ys) ⊆ set xs"
by (induct xs, auto)

lemma remove_preserve_sorted: "sorted xs ⟹ sorted (remove xs ys)"
proof (induct xs, simp, rule sorted.cases, simp, simp, simp, rule)
  fix a xs xsa x
  assume a: "sorted (remove xsa ys)" "sorted (x # xsa)" "a = x ∧ xs = xsa"
  and b: "∀y∈set xsa. x ≤ y" "sorted xsa" "x ∉ set ys"
  show "sorted (x # remove xsa ys)"
    apply rule using b remove_subset [of xsa ys] apply auto
    apply (rule a) done
qed

lemma sorted_minimum_hd: "⟦ sorted xs; xs ≠ [] ⟧ ⟹ (⋀x. x ∈ set xs ⟹ hd xs ≤ x)"
by (rule sorted.cases, auto)

fun minfree :: "nat list ⇒ nat" where
  "minfree xs = hd (remove [0..<(maximum xs+2)] xs)"

definition problem1 where
  "problem1 f xs ≡ (f xs ∉ set xs ∧ (∀x. x ∉ set xs ⟶ f xs ≤ x))"

lemma minfree_problem1: "xs ≠ [] ⟹ problem1 minfree xs"
proof-
  assume a: "xs ≠ []"
                     
  have removed_nonempty: "remove [0..<(maximum xs+2)] xs ≠ []"
    proof-
      have "maximum xs + 1 ∈ set (remove [0..<(maximum xs+2)] xs)"
        apply (rule remove_stable, simp)
        apply (rule maximum_suc_notin, rule a) done
      thus ?thesis by auto
    qed

  have minfree_in: "minfree xs ∈ set (remove [0..<(maximum xs+2)] xs)"
    using removed_nonempty by auto

  have "minfree xs ∉ set xs"
    proof-
      have 1: "⋀x. x ∈ set (remove [0..<(maximum xs+2)] xs) ⟹ x ∉ set xs"
        by (rule after_removing, simp)
      show ?thesis by (rule 1 [OF minfree_in])
    qed
  moreover have "⋀x. x ∉ set xs ⟹ minfree xs ≤ x"
    proof-
      fix x
      assume a: "x ∉ set xs"
      have 1: "x ∈ set [0..<maximum xs + 2] ⟹ hd (remove [0..<(maximum xs+2)] xs) ≤ x"
        apply (rule sorted_minimum_hd, rule remove_preserve_sorted)
        apply (rule sorted_upt, rule removed_nonempty)
        apply (rule remove_stable, simp, rule a)
        done
      have 2: "x ∈ set [0..<maximum xs + 2] ⟹ minfree xs ≤ x"
        using 1 by auto
      have 3: "x ∉ set [0..<maximum xs + 2] ⟹ maximum xs + 2 ≤ x"
        by (induct xs, auto)
      have 4: "minfree xs < maximum xs + 2"
        proof-
          have "minfree xs ∈ set [0..<maximum xs + 2]"
            using minfree_in remove_subset [of "[0..<maximum xs + 2]" xs] by auto
          thus ?thesis by auto
        qed
      have 5: "x ∉ set [0..<maximum xs + 2] ⟹ minfree xs ≤ x"
        using 3 4 by auto
      show "minfree xs ≤ x"
        apply (cases "x ∈ set [0..<maximum xs + 2]")
          by (rule 2, simp, rule 5, simp)
    qed
  ultimately
    show ?thesis
      by (unfold problem1_def, auto)
qed

end