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