src/HOL/Data_Structures/Set_by_Ordered.thy
author nipkow
Mon Sep 21 14:44:32 2015 +0200 (2015-09-21)
changeset 61203 a8a8eca85801
child 61428 5e1938107371
permissions -rw-r--r--
New subdirectory for functional data structures
nipkow@61203
     1
(* Author: Tobias Nipkow *)
nipkow@61203
     2
nipkow@61203
     3
section {* Implementing Ordered Sets *}
nipkow@61203
     4
nipkow@61203
     5
theory Set_by_Ordered
nipkow@61203
     6
imports List_Ins_Del
nipkow@61203
     7
begin
nipkow@61203
     8
nipkow@61203
     9
locale Set =
nipkow@61203
    10
fixes empty :: "'s"
nipkow@61203
    11
fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
nipkow@61203
    12
fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
nipkow@61203
    13
fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
nipkow@61203
    14
fixes set :: "'s \<Rightarrow> 'a set"
nipkow@61203
    15
fixes invar :: "'s \<Rightarrow> bool"
nipkow@61203
    16
assumes "set empty = {}"
nipkow@61203
    17
assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)"
nipkow@61203
    18
assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)"
nipkow@61203
    19
assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}"
nipkow@61203
    20
assumes "invar s \<Longrightarrow> invar(insert a s)"
nipkow@61203
    21
assumes "invar s \<Longrightarrow> invar(delete a s)"
nipkow@61203
    22
nipkow@61203
    23
locale Set_by_Ordered =
nipkow@61203
    24
fixes empty :: "'t"
nipkow@61203
    25
fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
nipkow@61203
    26
fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
nipkow@61203
    27
fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
nipkow@61203
    28
fixes inorder :: "'t \<Rightarrow> 'a list"
nipkow@61203
    29
fixes wf :: "'t \<Rightarrow> bool"
nipkow@61203
    30
assumes empty: "inorder empty = []"
nipkow@61203
    31
assumes isin: "wf t \<and> sorted(inorder t) \<Longrightarrow>
nipkow@61203
    32
  isin t a = (a \<in> elems (inorder t))"
nipkow@61203
    33
assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow>
nipkow@61203
    34
  inorder(insert a t) = ins_list a (inorder t)"
nipkow@61203
    35
assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow>
nipkow@61203
    36
  inorder(delete a t) = del_list a (inorder t)"
nipkow@61203
    37
assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)"
nipkow@61203
    38
assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)"
nipkow@61203
    39
begin
nipkow@61203
    40
nipkow@61203
    41
sublocale Set
nipkow@61203
    42
  empty insert delete isin "elems o inorder" "\<lambda>t. wf t \<and> sorted(inorder t)"
nipkow@61203
    43
proof(standard, goal_cases)
nipkow@61203
    44
  case 1 show ?case by (auto simp: empty)
nipkow@61203
    45
next
nipkow@61203
    46
  case 2 thus ?case by(simp add: isin)
nipkow@61203
    47
next
nipkow@61203
    48
  case 3 thus ?case by(simp add: insert)
nipkow@61203
    49
next
nipkow@61203
    50
  case (4 s a) show ?case
nipkow@61203
    51
    using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted)
nipkow@61203
    52
next
nipkow@61203
    53
  case 5 thus ?case by(simp add: insert wf_insert sorted_ins_list)
nipkow@61203
    54
next
nipkow@61203
    55
  case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list)
nipkow@61203
    56
qed
nipkow@61203
    57
nipkow@61203
    58
end
nipkow@61203
    59
nipkow@61203
    60
end