Theory Simpl_Heap

(*  Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer
*)

theory Simpl_Heap
imports Main
begin

subsection "References"

definition "ref = (UNIV::nat set)"

typedef ref = ref by (simp add: ref_def)

code_datatype Abs_ref

lemma finite_nat_ex_max:
  assumes fin: "finite (N::nat set)"
  shows "∃m. ∀n∈N. n < m"
using fin
proof (induct)
  case empty
  show ?case by auto
next
  case (insert k N)
  have "∃m. ∀n∈N. n < m" by fact
  then obtain m where m_max: "∀n∈N. n < m"..
  show "∃m. ∀n∈insert k N. n < m"
  proof (rule exI [where x="Suc (max k m)"])
  qed (insert m_max, auto simp add: max_def)
qed

lemma infinite_nat: "¬finite (UNIV::nat set)"
proof
  assume fin: "finite (UNIV::nat set)"
  then obtain m::nat where "∀n∈UNIV. n < m"
    by (rule finite_nat_ex_max [elim_format] ) auto
  moreover have "m∈UNIV"..
  ultimately show False by blast
qed

lemma infinite_ref [simp,intro]: "¬finite (UNIV::ref set)"
proof
  assume "finite (UNIV::ref set)"
  hence "finite (range Rep_ref)"
    by simp
  moreover
  have "range Rep_ref = ref"
  proof
    show "range Rep_ref ⊆ ref"
      by (simp add: ref_def)
  next
    show "ref ⊆ range Rep_ref"
    proof
      fix x
      assume x: "x ∈ ref"
      show "x ∈ range Rep_ref"
        by (rule Rep_ref_induct) (auto simp add: ref_def)
    qed
  qed
  ultimately have "finite ref"
    by simp
  thus False
    by (simp add: ref_def infinite_nat)
qed

consts Null :: ref

definition new :: "ref set ⇒ ref" where
  "new A = (SOME a. a ∉ {Null} ∪ A)"

text ‹
  Constant @{const "Null"} can be defined later on.  Conceptually
  @{const "Null"} and @{const "new"} are ‹fixes› of a locale
  with @{prop "finite A ⟹ new A ∉ A ∪ {Null}"}.  But since definitions
  relative to a locale do not yet work in Isabelle2005 we use this
  workaround to avoid lots of parameters in definitions.
›

lemma new_notin [simp,intro]:
 "finite A ⟹ new (A) ∉ A"
  apply (unfold new_def)
  apply (rule someI2_ex)
  apply (fastforce intro: ex_new_if_finite)
  apply simp
  done

lemma new_not_Null [simp,intro]:
  "finite A ⟹ new (A) ≠ Null"
  apply (unfold new_def)
  apply (rule someI2_ex)
  apply (fastforce intro: ex_new_if_finite)
  apply simp
done

end