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