Quelle Brother12_Set.thy Sprache: Isabelle

(* Author: Tobias Nipkow, Daniel Stüwe *)

section \<open>1-2 Brother Tree Implementation of Sets\<close>

theory Brother12_Set
  imports
    Cmp
    Set_Specs
    "HOL-Number_Theory.Fib"
begin

subsection \<open>Data Type and Operations\<close>

datatype 'a bro =
  N0 |
  N1 "'a bro" |
  N2 "'a bro" 'a "'a bro" |
  (* auxiliary constructors: *)
  L2 'a |
  N3 "'a bro" 'a "'a bro" 'a "'a bro"

definition empty :: "'a bro" where
  "empty = N0"

fun inorder :: "'a bro \ 'a list" where
  "inorder N0 = []" |
  "inorder (N1 t) = inorder t" |
  "inorder (N2 l a r) = inorder l @ a # inorder r" |
  "inorder (L2 a) = [a]" |
  "inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3"

fun isin :: "'a bro \ 'a::linorder \ bool" where
  "isin N0 x = False" |
  "isin (N1 t) x = isin t x" |
  "isin (N2 l a r) x =
  (case cmp x a of
     LT \<Rightarrow> isin l x |
     EQ \<Rightarrow> True |
     GT \<Rightarrow> isin r x)"

fun n1 :: "'a bro \ 'a bro" where
  "n1 (L2 a) = N2 N0 a N0" |
  "n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
  "n1 t = N1 t"

hide_const (open) insert

locale insert
begin

fun n2 :: "'a bro \ 'a \ 'a bro \ 'a bro" where
  "n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" |
  "n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
  "n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" |
  "n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" |
  "n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
  "n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" |
  "n2 t1 a t2 = N2 t1 a t2"

fun ins :: "'a::linorder \ 'a bro \ 'a bro" where
  "ins x N0 = L2 x" |
  "ins x (N1 t) = n1 (ins x t)" |
  "ins x (N2 l a r) =
  (case cmp x a of
     LT \<Rightarrow> n2 (ins x l) a r |
     EQ \<Rightarrow> N2 l a r |
     GT \<Rightarrow> n2 l a (ins x r))"

fun tree :: "'a bro \ 'a bro" where
  "tree (L2 a) = N2 N0 a N0" |
  "tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
  "tree t = t"

definition insert :: "'a::linorder \ 'a bro \ 'a bro" where
  "insert x t = tree(ins x t)"

end

locale delete
begin

fun n2 :: "'a bro \ 'a \ 'a bro \ 'a bro" where
  "n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" |
  "n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) =
  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
  "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) =
  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
  "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) =
  N2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N2 t4 a4 t5))" |
  "n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) =
  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
  "n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) =
  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
  "n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) =
  N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" |
  "n2 t1 a1 t2 = N2 t1 a1 t2"

fun split_min :: "'a bro \ ('a \ 'a bro) option" where
  "split_min N0 = None" |
  "split_min (N1 t) =
  (case split_min t of
     None \<Rightarrow> None |
     Some (a, t') \ Some (a, N1 t'))" |
  "split_min (N2 t1 a t2) =
  (case split_min t1 of
     None \<Rightarrow> Some (a, N1 t2) |
     Some (b, t1') \ Some (b, n2 t1' a t2))"

fun del :: "'a::linorder \ 'a bro \ 'a bro" where
  "del _ N0 = N0" |
  "del x (N1 t) = N1 (del x t)" |
  "del x (N2 l a r) =
  (case cmp x a of
     LT \<Rightarrow> n2 (del x l) a r |
     GT \<Rightarrow> n2 l a (del x r) |
     EQ \<Rightarrow> (case split_min r of
              None \<Rightarrow> N1 l |
              Some (b, r') \ n2 l b r'))"

fun tree :: "'a bro \ 'a bro" where
  "tree (N1 t) = t" |
  "tree t = t"

definition delete :: "'a::linorder \ 'a bro \ 'a bro" where
  "delete a t = tree (del a t)"

end

subsection \<open>Invariants\<close>

fun B :: "nat \ 'a bro set"
  and U :: "nat \ 'a bro set" where
  "B 0 = {N0}" |
  "B (Suc h) = { N2 t1 a t2 | t1 a t2.
  t1 \<in> B h \<union> U h \<and> t2 \<in> B h \<or> t1 \<in> B h \<and> t2 \<in> B h \<union> U h}" |
  "U 0 = {}" |
  "U (Suc h) = N1 ` B h"

abbreviation "T h \ B h \ U h"

fun Bp :: "nat \ 'a bro set" where
  "Bp 0 = B 0 \ L2 ` UNIV" |
  "Bp (Suc 0) = B (Suc 0) \ {N3 N0 a N0 b N0|a b. True}" |
  "Bp (Suc(Suc h)) = B (Suc(Suc h)) \
  {N3 t1 a t2 b t3 | t1 a t2 b t3. t1 \<in> B (Suc h) \<and> t2 \<in> U (Suc h) \<and> t3 \<in> B (Suc h)}"

fun Um :: "nat \ 'a bro set" where
  "Um 0 = {}" |
  "Um (Suc h) = N1 ` T h"

subsection "Functional Correctness Proofs"

subsubsection "Proofs for isin"

lemma isin_set:
  "t \ T h \ sorted(inorder t) \ isin t x = (x \ set(inorder t))"
  by(induction h arbitrary: t) (fastforce simp: isin_simps split: if_splits)+

subsubsection "Proofs for insertion"

lemma inorder_n1: "inorder(n1 t) = inorder t"
  by(cases t rule: n1.cases) (auto simp: sorted_lems)

context insert
begin

lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
  by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems)

lemma inorder_tree: "inorder(tree t) = inorder t"
  by(cases t) auto

lemma inorder_ins: "t \ T h \
  sorted(inorder t) \<Longrightarrow> inorder(ins a t) = ins_list a (inorder t)"
  by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2)

lemma inorder_insert: "t \ T h \
  sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
  by(simp add: insert_def inorder_ins inorder_tree)

end

subsubsection \<open>Proofs for deletion\<close>

context delete
begin

lemma inorder_tree: "inorder(tree t) = inorder t"
  by(cases t) auto

lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
  by(cases "(l,a,r)" rule: n2.cases) (auto)

lemma inorder_split_min:
  "t \ T h \ (split_min t = None \ inorder t = []) \
  (split_min t = Some(a,t') \ inorder t = a # inorder t')"
  by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)

lemma inorder_del:
  "t \ T h \ sorted(inorder t) \ inorder(del x t) = del_list x (inorder t)"
  apply (induction h arbitrary: t)
  apply (auto simp: del_list_simps inorder_n2 split: option.splits)
  apply (auto simp: del_list_simps inorder_n2
      inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
  done

lemma inorder_delete:
  "t \ T h \ sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)"
  by(simp add: delete_def inorder_del inorder_tree)

end

subsection \<open>Invariant Proofs\<close>

subsubsection \<open>Proofs for insertion\<close>

lemma n1_type: "t \ Bp h \ n1 t \ T (Suc h)"
  by(cases h rule: Bp.cases) auto

context insert
begin

lemma tree_type: "t \ Bp h \ tree t \ B h \ B (Suc h)"
  by(cases h rule: Bp.cases) auto

lemma n2_type:
  "(t1 \ Bp h \ t2 \ T h \ n2 t1 a t2 \ Bp (Suc h)) \
   (t1 \<in> T h \<and> t2 \<in> Bp h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h))"
  apply(cases h rule: Bp.cases)
    apply (auto)[2]
  apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+
  done

lemma Bp_if_B: "t \ B h \ t \ Bp h"
  by (cases h rule: Bp.cases) simp_all

text\<open>An automatic proof:\<close>

lemma
  "(t \ B h \ ins x t \ Bp h) \ (t \ U h \ ins x t \ T h)"
proof (induction h arbitrary: t)
  case 0
  then show ?case by simp
next
  case (Suc h)
  then show ?case by (fastforce simp: Bp_if_B n2_type dest: n1_type)
qed

text\<open>A detailed proof:\<close>

lemma ins_type:
  shows "t \ B h \ ins x t \ Bp h" and "t \ U h \ ins x t \ T h"
proof(induction h arbitrary: t)
  case 0
  { case 1 thus ?case by simp
  next
    case 2 thus ?case by simp }
next
  case (Suc h)
  { case 1
    then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
      t1: "t1 \ T h" and t2: "t2 \ T h" and t12: "t1 \ B h \ t2 \ B h"
      by auto
    have ?case if "x < a"
    proof -
      have "n2 (ins x t1) a t2 \ Bp (Suc h)"
      proof cases
        assume "t1 \ B h"
        with t2 show ?thesis by (simp add: Suc.IH(1) n2_type)
      next
        assume "t1 \ B h"
        hence 1: "t1 \ U h" and 2: "t2 \ B h" using t1 t12 by auto
        show ?thesis by (metis Suc.IH(2)[OF 1] Bp_if_B[OF 2] n2_type)
      qed
      with \<open>x < a\<close> show ?case by simp
    qed
    moreover
    have ?case if "a < x"
    proof -
      have "n2 t1 a (ins x t2) \ Bp (Suc h)"
      proof cases
        assume "t2 \ B h"
        with t1 show ?thesis by (simp add: Suc.IH(1) n2_type)
      next
        assume "t2 \ B h"
        hence 1: "t1 \ B h" and 2: "t2 \ U h" using t2 t12 by auto
        show ?thesis by (metis Bp_if_B[OF 1] Suc.IH(2)[OF 2] n2_type)
      qed
      with \<open>a < x\<close> show ?case by simp
    qed
    moreover
    have ?case if "x = a"
    proof -
      from 1 have "t \ Bp (Suc h)" by(rule Bp_if_B)
      thus "?case" using \<open>x = a\<close> by simp
    qed
    ultimately show ?case by auto
  next
    case 2 thus ?case using Suc(1) n1_type by fastforce }
qed

lemma insert_type:
  "t \ B h \ insert x t \ B h \ B (Suc h)"
  unfolding insert_def by (metis ins_type(1) tree_type)

end

subsubsection "Proofs for deletion"

lemma B_simps[simp]:
  "N1 t \ B h = False"
  "L2 y \ B h = False"
  "(N3 t1 a1 t2 a2 t3) \ B h = False"
  "N0 \ B h \ h = 0"
  by (cases h, auto)+

context delete
begin

lemma n2_type1:
  "\t1 \ Um h; t2 \ B h\ \ n2 t1 a t2 \ T (Suc h)"
  apply(cases h rule: Bp.cases)
    apply auto[2]
  apply(erule exE bexE conjE imageE | simp | erule disjE)+
  done

lemma n2_type2:
  "\t1 \ B h ; t2 \ Um h \ \ n2 t1 a t2 \ T (Suc h)"
  apply(cases h rule: Bp.cases)
  using Um.simps(1) apply blast
   apply force
  apply(erule exE bexE conjE imageE | simp | erule disjE)+
  done

lemma n2_type3:
  "\t1 \ T h ; t2 \ T h \ \ n2 t1 a t2 \ T (Suc h)"
  apply(cases h rule: Bp.cases)
    apply auto[2]
  apply(erule exE bexE conjE imageE | simp | erule disjE)+
  done

lemma split_minNoneN0: "\t \ B h; split_min t = None\ \ t = N0"
  by (cases t) (auto split: option.splits)

lemma split_minNoneN1 : "\t \ U h; split_min t = None\ \ t = N1 N0"
  by (cases h) (auto simp: split_minNoneN0  split: option.splits)

lemma split_min_type:
  "t \ B h \ split_min t = Some (a, t') \ t' \ T h"
  "t \ U h \ split_min t = Some (a, t') \ t' \ Um h"
proof (induction h arbitrary: t a t')
  case (Suc h)
  { case 1
    then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
      t12: "t1 \ T h" "t2 \ T h" "t1 \ B h \ t2 \ B h"
      by auto
    show ?case
    proof (cases "split_min t1")
      case None
      show ?thesis
      proof cases
        assume "t1 \ B h"
        with split_minNoneN0[OF this None] 1 show ?thesis by(auto)
      next
        assume "t1 \ B h"
        thus ?thesis using 1 None by (auto)
      qed
    next
      case [simp]: (Some bt')
      obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
      show ?thesis
      proof cases
        assume "t1 \ B h"
        from Suc.IH(1)[OF this] 1 have "t1' \ T h" by simp
        from n2_type3[OF this t12(2)] 1 show ?thesis by auto
      next
        assume "t1 \ B h"
        hence t1: "t1 \ U h" and t2: "t2 \ B h" using t12 by auto
        from Suc.IH(2)[OF t1] have "t1' \ Um h" by simp
        from n2_type1[OF this t2] 1 show ?thesis by auto
      qed
    qed
  }
  { case 2
    then obtain t1 where [simp]: "t = N1 t1" and t1: "t1 \ B h" by auto
    show ?case
    proof (cases "split_min t1")
      case None
      with split_minNoneN0[OF t1 None] 2 show ?thesis by(auto)
    next
      case [simp]: (Some bt')
      obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
      from Suc.IH(1)[OF t1] have "t1' \ T h" by simp
      thus ?thesis using 2 by auto
    qed
  }
qed auto

lemma del_type:
  "t \ B h \ del x t \ T h"
  "t \ U h \ del x t \ Um h"
proof (induction h arbitrary: x t)
  case (Suc h)
  { case 1
    then obtain l a r where [simp]: "t = N2 l a r" and
      lr: "l \ T h" "r \ T h" "l \ B h \ r \ B h" by auto
    have ?case if "x < a"
    proof cases
      assume "l \ B h"
      from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
      show ?thesis using \<open>x<a\<close> by(simp)
    next
      assume "l \ B h"
      hence "l \ U h" "r \ B h" using lr by auto
      from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
      show ?thesis using \<open>x<a\<close> by(simp)
    qed
    moreover
    have ?case if "x > a"
    proof cases
      assume "r \ B h"
      from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
      show ?thesis using \<open>x>a\<close> by(simp)
    next
      assume "r \ B h"
      hence "l \ B h" "r \ U h" using lr by auto
      from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
      show ?thesis using \<open>x>a\<close> by(simp)
    qed
    moreover
    have ?case if [simp]: "x=a"
    proof (cases "split_min r")
      case None
      show ?thesis
      proof cases
        assume "r \ B h"
        with split_minNoneN0[OF this None] lr show ?thesis by(simp)
      next
        assume "r \ B h"
        hence "r \ U h" using lr by auto
        with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
      qed
    next
      case [simp]: (Some br')
      obtain b r' where [simp]: "br' = (b,r')" by fastforce
      show ?thesis
      proof cases
        assume "r \ B h"
        from split_min_type(1)[OF this] n2_type3[OF lr(1)]
        show ?thesis by simp
      next
        assume "r \ B h"
        hence "l \ B h" and "r \ U h" using lr by auto
        from split_min_type(2)[OF this(2)] n2_type2[OF this(1)]
        show ?thesis by simp
      qed
    qed
    ultimately show ?case by auto
  }
  { case 2 with Suc.IH(1) show ?case by auto }
qed auto

lemma tree_type: "t \ T (h+1) \ tree t \ B (h+1) \ B h"
  by(auto)

lemma delete_type: "t \ B h \ delete x t \ B h \ B(h-1)"
  unfolding delete_def
  by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)

end

subsection "Overall correctness"

interpretation Set_by_Ordered
  where empty = empty and isin = isin and insert = insert.insert
    and delete = delete.delete and inorder = inorder and inv = "\t. \h. t \ B h"
proof (standard, goal_cases)
  case 2 thus ?case by(auto intro!: isin_set)
next
  case 3 thus ?case by(auto intro!: insert.inorder_insert)
next
  case 4 thus ?case by(auto intro!: delete.inorder_delete)
next
  case 6 thus ?case using insert.insert_type by blast
next
  case 7 thus ?case using delete.delete_type by blast
qed (auto simp: empty_def)

subsection \<open>Height-Size Relation\<close>

text \<open>By Daniel Stüwe\<close>

fun fib_tree :: "nat \ unit bro" where
  "fib_tree 0 = N0"
| "fib_tree (Suc 0) = N2 N0 () N0"
| "fib_tree (Suc(Suc h)) = N2 (fib_tree (h+1)) () (N1 (fib_tree h))"

fun fib' :: "nat \ nat" where
  "fib' 0 = 0"
| "fib' (Suc 0) = 1"
| "fib' (Suc(Suc h)) = 1 + fib' (Suc h) + fib' h"

fun size :: "'a bro \ nat" where
  "size N0 = 0"
| "size (N1 t) = size t"
| "size (N2 t1 _ t2) = 1 + size t1 + size t2"

lemma fib_tree_B: "fib_tree h \ B h"
  by (induction h rule: fib_tree.induct) auto

declare [[names_short]]

lemma size_fib': "size (fib_tree h) = fib' h"
  by (induction h rule: fib_tree.induct) auto

lemma fibfib: "fib' h + 1 = fib (Suc(Suc h))"
  by (induction h rule: fib_tree.induct) auto

lemma B_N2_cases[consumes 1]:
  assumes "N2 t1 a t2 \ B (Suc n)"
  obtains
    (BB) "t1 \ B n" and "t2 \ B n" |
    (UB) "t1 \ U n" and "t2 \ B n" |
    (BU) "t1 \ B n" and "t2 \ U n"
  using assms by auto

lemma size_bounded: "t \ B h \ size t \ size (fib_tree h)"
  unfolding size_fib' proof (induction h arbitrary: t rule: fib'.induct)
  case (3 h t')
  note main = 3
  then obtain t1 a t2 where t': "t' = N2 t1 a t2" by auto
  with main have "N2 t1 a t2 \ B (Suc (Suc h))" by auto
  thus ?case proof (cases rule: B_N2_cases)
    case BB
    then obtain x y z where t2: "t2 = N2 x y z \ t2 = N2 z y x" "x \ B h" by auto
    show ?thesis unfolding t' using main(1)[OF BB(1)] main(2)[OF t2(2)] t2(1) by auto
  next
    case UB
    then obtain t11 where t1: "t1 = N1 t11" "t11 \ B h" by auto
    show ?thesis unfolding t' t1(1) using main(2)[OF t1(2)] main(1)[OF UB(2)] by simp
  next
    case BU
    then obtain t22 where t2: "t2 = N1 t22" "t22 \ B h" by auto
    show ?thesis unfolding t' t2(1) using main(2)[OF t2(2)] main(1)[OF BU(1)] by simp
  qed
qed auto

theorem "t \ B h \ fib (h + 2) \ size t + 1"
  using size_bounded
  by (simp add: size_fib' fibfib[symmetric] del: fib.simps)

end

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.