src/HOL/Data_Structures/Set_by_Ordered.thy
author haftmann
Sat, 11 Nov 2017 18:41:08 +0000
changeset 67051 e7e54a0b9197
parent 61640 44c9198f210c
child 67406 23307fd33906
permissions -rw-r--r--
dedicated definition for coprimality
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61640
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
     1
(* Author: Tobias Nipkow *)
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
     2
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
     3
section {* Implementing Ordered Sets *}
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
     4
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
     5
theory Set_by_Ordered
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
     6
imports List_Ins_Del
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
     7
begin
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
     8
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
     9
locale Set =
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    10
fixes empty :: "'s"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    11
fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    12
fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    13
fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    14
fixes set :: "'s \<Rightarrow> 'a set"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    15
fixes invar :: "'s \<Rightarrow> bool"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    16
assumes set_empty:    "set empty = {}"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    17
assumes set_isin:     "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    18
assumes set_insert:   "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    19
assumes set_delete:   "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    20
assumes invar_empty:  "invar empty"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    21
assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    22
assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    23
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    24
locale Set_by_Ordered =
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    25
fixes empty :: "'t"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    26
fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    27
fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    28
fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    29
fixes inorder :: "'t \<Rightarrow> 'a list"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    30
fixes inv :: "'t \<Rightarrow> bool"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    31
assumes empty: "inorder empty = []"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    32
assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    33
  isin t x = (x \<in> elems (inorder t))"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    34
assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    35
  inorder(insert x t) = ins_list x (inorder t)"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    36
assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    37
  inorder(delete x t) = del_list x (inorder t)"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    38
assumes inv_empty:  "inv empty"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    39
assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    40
assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    41
begin
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    42
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    43
sublocale Set
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    44
  empty insert delete isin "elems o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    45
proof(standard, goal_cases)
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    46
  case 1 show ?case by (auto simp: empty)
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    47
next
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    48
  case 2 thus ?case by(simp add: isin)
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    49
next
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    50
  case 3 thus ?case by(simp add: insert set_ins_list)
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    51
next
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    52
  case (4 s x) thus ?case
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    53
    using delete[OF 4, of x] by (auto simp: distinct_if_sorted elems_del_list_eq)
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    54
next
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    55
  case 5 thus ?case by(simp add: empty inv_empty)
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    56
next
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    57
  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    58
next
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    59
  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    60
qed
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    61
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    62
end
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    63
44c9198f210c no CRLF
nipkow
parents: 61589
diff changeset
    64
end