31 fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't" |
31 fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't" |
32 fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't" |
32 fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't" |
33 fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool" |
33 fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool" |
34 fixes inorder :: "'t \<Rightarrow> 'a list" |
34 fixes inorder :: "'t \<Rightarrow> 'a list" |
35 fixes inv :: "'t \<Rightarrow> bool" |
35 fixes inv :: "'t \<Rightarrow> bool" |
36 assumes empty: "inorder empty = []" |
36 assumes inorder_empty: "inorder empty = []" |
37 assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow> |
37 assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow> |
38 isin t x = (x \<in> set (inorder t))" |
38 isin t x = (x \<in> set (inorder t))" |
39 assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> |
39 assumes inorder_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> |
40 inorder(insert x t) = ins_list x (inorder t)" |
40 inorder(insert x t) = ins_list x (inorder t)" |
41 assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> |
41 assumes inorder_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> |
42 inorder(delete x t) = del_list x (inorder t)" |
42 inorder(delete x t) = del_list x (inorder t)" |
43 assumes inv_empty: "inv empty" |
43 assumes inorder_inv_empty: "inv empty" |
44 assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)" |
44 assumes inorder_inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)" |
45 assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)" |
45 assumes inorder_inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)" |
46 begin |
46 begin |
47 |
47 |
48 text \<open>It implements the traditional specification:\<close> |
48 text \<open>It implements the traditional specification:\<close> |
49 |
49 |
50 definition set :: "'t \<Rightarrow> 'a set" where |
50 definition set :: "'t \<Rightarrow> 'a set" where |
54 "invar t == inv t \<and> sorted (inorder t)" |
54 "invar t == inv t \<and> sorted (inorder t)" |
55 |
55 |
56 sublocale Set |
56 sublocale Set |
57 empty insert delete isin set invar |
57 empty insert delete isin set invar |
58 proof(standard, goal_cases) |
58 proof(standard, goal_cases) |
59 case 1 show ?case by (auto simp: empty set_def) |
59 case 1 show ?case by (auto simp: inorder_empty set_def) |
60 next |
60 next |
61 case 2 thus ?case by(simp add: isin invar_def set_def) |
61 case 2 thus ?case by(simp add: isin invar_def set_def) |
62 next |
62 next |
63 case 3 thus ?case by(simp add: insert set_ins_list set_def invar_def) |
63 case 3 thus ?case by(simp add: inorder_insert set_ins_list set_def invar_def) |
64 next |
64 next |
65 case (4 s x) thus ?case |
65 case (4 s x) thus ?case |
66 by (auto simp: delete distinct_if_sorted set_del_list_eq invar_def set_def) |
66 by (auto simp: inorder_delete distinct_if_sorted set_del_list_eq invar_def set_def) |
67 next |
67 next |
68 case 5 thus ?case by(simp add: empty inv_empty invar_def) |
68 case 5 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def) |
69 next |
69 next |
70 case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list invar_def) |
70 case 6 thus ?case by(simp add: inorder_insert inorder_inv_insert sorted_ins_list invar_def) |
71 next |
71 next |
72 case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list invar_def) |
72 case 7 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def) |
73 qed |
73 qed |
74 |
74 |
75 end |
75 end |
76 |
76 |
77 |
77 |