equal
deleted
inserted
replaced
21 assumes set_delete: "invar s \<Longrightarrow> set(delete x s) = set s - {x}" |
21 assumes set_delete: "invar s \<Longrightarrow> set(delete x s) = set s - {x}" |
22 assumes invar_empty: "invar empty" |
22 assumes invar_empty: "invar empty" |
23 assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)" |
23 assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)" |
24 assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)" |
24 assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)" |
25 |
25 |
|
26 lemmas (in Set) set_specs = |
|
27 set_empty set_isin set_insert set_delete invar_empty invar_insert invar_delete |
26 |
28 |
27 text \<open>The basic set interface with \<open>inorder\<close>-based specification:\<close> |
29 text \<open>The basic set interface with \<open>inorder\<close>-based specification:\<close> |
28 |
30 |
29 locale Set_by_Ordered = |
31 locale Set_by_Ordered = |
30 fixes empty :: "'t" |
32 fixes empty :: "'t" |
41 assumes inorder_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> |
43 assumes inorder_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> |
42 inorder(delete x t) = del_list x (inorder t)" |
44 inorder(delete x t) = del_list x (inorder t)" |
43 assumes inorder_inv_empty: "inv empty" |
45 assumes inorder_inv_empty: "inv empty" |
44 assumes inorder_inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)" |
46 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)" |
47 assumes inorder_inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)" |
|
48 |
46 begin |
49 begin |
47 |
50 |
48 text \<open>It implements the traditional specification:\<close> |
51 text \<open>It implements the traditional specification:\<close> |
49 |
52 |
50 definition set :: "'t \<Rightarrow> 'a set" where |
53 definition set :: "'t \<Rightarrow> 'a set" where |