src/HOL/Data_Structures/Set_Specs.thy
author nipkow
Wed Jun 13 15:24:20 2018 +0200 (12 months ago)
changeset 68440 6826718f732d
parent 68439 c8101022e52a
child 68492 c7e0a7bcacaf
permissions -rw-r--r--
qualify interpretations to avoid clashes
nipkow@61640
     1
(* Author: Tobias Nipkow *)
nipkow@61640
     2
nipkow@67965
     3
section \<open>Specifications of Set ADT\<close>
nipkow@61640
     4
nipkow@67965
     5
theory Set_Specs
nipkow@61640
     6
imports List_Ins_Del
nipkow@61640
     7
begin
nipkow@61640
     8
nipkow@67965
     9
text \<open>The basic set interface with traditional \<open>set\<close>-based specification:\<close>
nipkow@67964
    10
nipkow@61640
    11
locale Set =
nipkow@61640
    12
fixes empty :: "'s"
nipkow@61640
    13
fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
nipkow@61640
    14
fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
nipkow@61640
    15
fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
nipkow@61640
    16
fixes set :: "'s \<Rightarrow> 'a set"
nipkow@61640
    17
fixes invar :: "'s \<Rightarrow> bool"
nipkow@61640
    18
assumes set_empty:    "set empty = {}"
nipkow@61640
    19
assumes set_isin:     "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
nipkow@61640
    20
assumes set_insert:   "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
nipkow@61640
    21
assumes set_delete:   "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
nipkow@61640
    22
assumes invar_empty:  "invar empty"
nipkow@61640
    23
assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
nipkow@61640
    24
assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
nipkow@61640
    25
nipkow@67964
    26
nipkow@67964
    27
text \<open>The basic set interface with \<open>inorder\<close>-based specification:\<close>
nipkow@67964
    28
nipkow@61640
    29
locale Set_by_Ordered =
nipkow@61640
    30
fixes empty :: "'t"
nipkow@61640
    31
fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
nipkow@61640
    32
fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
nipkow@61640
    33
fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
nipkow@61640
    34
fixes inorder :: "'t \<Rightarrow> 'a list"
nipkow@61640
    35
fixes inv :: "'t \<Rightarrow> bool"
nipkow@68440
    36
assumes inorder_empty: "inorder empty = []"
nipkow@61640
    37
assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
nipkow@67929
    38
  isin t x = (x \<in> set (inorder t))"
nipkow@68440
    39
assumes inorder_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
nipkow@61640
    40
  inorder(insert x t) = ins_list x (inorder t)"
nipkow@68440
    41
assumes inorder_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
nipkow@61640
    42
  inorder(delete x t) = del_list x (inorder t)"
nipkow@68440
    43
assumes inorder_inv_empty:  "inv empty"
nipkow@68440
    44
assumes inorder_inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
nipkow@68440
    45
assumes inorder_inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
nipkow@61640
    46
begin
nipkow@61640
    47
nipkow@67964
    48
text \<open>It implements the traditional specification:\<close>
nipkow@67964
    49
nipkow@68439
    50
definition set :: "'t \<Rightarrow> 'a set" where
nipkow@68439
    51
"set == List.set o inorder"
nipkow@68439
    52
nipkow@68439
    53
definition invar :: "'t \<Rightarrow> bool" where
nipkow@68439
    54
"invar t == inv t \<and> sorted (inorder t)"
nipkow@68439
    55
nipkow@61640
    56
sublocale Set
nipkow@68439
    57
  empty insert delete isin set invar
nipkow@61640
    58
proof(standard, goal_cases)
nipkow@68440
    59
  case 1 show ?case by (auto simp: inorder_empty set_def)
nipkow@61640
    60
next
nipkow@68439
    61
  case 2 thus ?case by(simp add: isin invar_def set_def)
nipkow@61640
    62
next
nipkow@68440
    63
  case 3 thus ?case by(simp add: inorder_insert set_ins_list set_def invar_def)
nipkow@61640
    64
next
nipkow@61640
    65
  case (4 s x) thus ?case
nipkow@68440
    66
    by (auto simp: inorder_delete distinct_if_sorted set_del_list_eq invar_def set_def)
nipkow@61640
    67
next
nipkow@68440
    68
  case 5 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def)
nipkow@61640
    69
next
nipkow@68440
    70
  case 6 thus ?case by(simp add: inorder_insert inorder_inv_insert sorted_ins_list invar_def)
nipkow@61640
    71
next
nipkow@68440
    72
  case 7 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def)
nipkow@61640
    73
qed
nipkow@61640
    74
nipkow@61640
    75
end
nipkow@61640
    76
nipkow@67964
    77
nipkow@67964
    78
text \<open>Set2 = Set with binary operations:\<close>
nipkow@67964
    79
nipkow@67964
    80
locale Set2 = Set
nipkow@67964
    81
  where insert = insert for insert :: "'a \<Rightarrow> 's \<Rightarrow> 's" (*for typing purposes only*) +
nipkow@67964
    82
fixes union :: "'s \<Rightarrow> 's \<Rightarrow> 's"
nipkow@67964
    83
fixes inter :: "'s \<Rightarrow> 's \<Rightarrow> 's"
nipkow@67964
    84
fixes diff  :: "'s \<Rightarrow> 's \<Rightarrow> 's"
nipkow@67964
    85
assumes set_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(union s1 s2) = set s1 \<union> set s2"
nipkow@67964
    86
assumes set_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(inter s1 s2) = set s1 \<inter> set s2"
nipkow@67964
    87
assumes set_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(diff s1 s2) = set s1 - set s2"
nipkow@67964
    88
assumes invar_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(union s1 s2)"
nipkow@67964
    89
assumes invar_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(inter s1 s2)"
nipkow@67964
    90
assumes invar_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(diff s1 s2)"
nipkow@67964
    91
nipkow@61640
    92
end