equal
deleted
inserted
replaced
15 fixes invar :: "'s \<Rightarrow> bool" |
15 fixes invar :: "'s \<Rightarrow> bool" |
16 assumes "set empty = {}" |
16 assumes "set empty = {}" |
17 assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)" |
17 assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)" |
18 assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)" |
18 assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)" |
19 assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}" |
19 assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}" |
|
20 assumes "invar empty" |
20 assumes "invar s \<Longrightarrow> invar(insert a s)" |
21 assumes "invar s \<Longrightarrow> invar(insert a s)" |
21 assumes "invar s \<Longrightarrow> invar(delete a s)" |
22 assumes "invar s \<Longrightarrow> invar(delete a s)" |
22 |
23 |
23 locale Set_by_Ordered = |
24 locale Set_by_Ordered = |
24 fixes empty :: "'t" |
25 fixes empty :: "'t" |
32 isin t a = (a \<in> elems (inorder t))" |
33 isin t a = (a \<in> elems (inorder t))" |
33 assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> |
34 assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> |
34 inorder(insert a t) = ins_list a (inorder t)" |
35 inorder(insert a t) = ins_list a (inorder t)" |
35 assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> |
36 assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> |
36 inorder(delete a t) = del_list a (inorder t)" |
37 inorder(delete a t) = del_list a (inorder t)" |
|
38 assumes wf_empty: "wf empty" |
37 assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)" |
39 assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)" |
38 assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)" |
40 assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)" |
39 begin |
41 begin |
40 |
42 |
41 sublocale Set |
43 sublocale Set |
48 case 3 thus ?case by(simp add: insert) |
50 case 3 thus ?case by(simp add: insert) |
49 next |
51 next |
50 case (4 s a) show ?case |
52 case (4 s a) show ?case |
51 using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted) |
53 using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted) |
52 next |
54 next |
53 case 5 thus ?case by(simp add: insert wf_insert sorted_ins_list) |
55 case 5 thus ?case by(simp add: empty wf_empty) |
54 next |
56 next |
55 case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list) |
57 case 6 thus ?case by(simp add: insert wf_insert sorted_ins_list) |
|
58 next |
|
59 case 7 thus ?case by (auto simp: delete wf_delete sorted_del_list) |
56 qed |
60 qed |
57 |
61 |
58 end |
62 end |
59 |
63 |
60 end |
64 end |