src/HOL/Data_Structures/RBT_Set.thy
 author nipkow Thu Nov 05 08:27:14 2015 +0100 (2015-11-05) changeset 61581 00d9682e8dd7 parent 61428 5e1938107371 child 61588 1d2907d0ed73 permissions -rw-r--r--
Convertd to 3-way comparisons
 nipkow@61224 1 (* Author: Tobias Nipkow *) nipkow@61224 2 nipkow@61224 3 section \Red-Black Tree Implementation of Sets\ nipkow@61224 4 nipkow@61224 5 theory RBT_Set nipkow@61224 6 imports nipkow@61224 7 RBT nipkow@61581 8 Cmp nipkow@61224 9 Isin2 nipkow@61224 10 begin nipkow@61224 11 nipkow@61581 12 fun insert :: "'a::cmp \ 'a rbt \ 'a rbt" where nipkow@61224 13 "insert x Leaf = R Leaf x Leaf" | nipkow@61581 14 "insert x (B l a r) = (case cmp x a of nipkow@61581 15 LT \ bal (insert x l) a r | nipkow@61581 16 GT \ bal l a (insert x r) | nipkow@61581 17 EQ \ B l a r)" | nipkow@61581 18 "insert x (R l a r) = (case cmp x a of nipkow@61581 19 LT \ R (insert x l) a r | nipkow@61581 20 GT \ R l a (insert x r) | nipkow@61581 21 EQ \ R l a r)" nipkow@61224 22 nipkow@61581 23 fun delete :: "'a::cmp \ 'a rbt \ 'a rbt" nipkow@61581 24 and deleteL :: "'a::cmp \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" nipkow@61581 25 and deleteR :: "'a::cmp \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" nipkow@61224 26 where nipkow@61224 27 "delete x Leaf = Leaf" | nipkow@61581 28 "delete x (Node _ l a r) = (case cmp x a of nipkow@61581 29 LT \ deleteL x l a r | nipkow@61581 30 GT \ deleteR x l a r | nipkow@61581 31 EQ \ combine l r)" | nipkow@61224 32 "deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" | nipkow@61224 33 "deleteL x l a r = R (delete x l) a r" | nipkow@61224 34 "deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" | nipkow@61224 35 "deleteR x l a r = R l a (delete x r)" nipkow@61224 36 nipkow@61224 37 nipkow@61224 38 subsection "Functional Correctness Proofs" nipkow@61224 39 nipkow@61224 40 lemma inorder_bal: nipkow@61224 41 "inorder(bal l a r) = inorder l @ a # inorder r" nipkow@61231 42 by(induction l a r rule: bal.induct) (auto) nipkow@61224 43 nipkow@61224 44 lemma inorder_insert: nipkow@61224 45 "sorted(inorder t) \ inorder(insert a t) = ins_list a (inorder t)" nipkow@61231 46 by(induction a t rule: insert.induct) (auto simp: ins_list_simps inorder_bal) nipkow@61224 47 nipkow@61224 48 lemma inorder_red: "inorder(red t) = inorder t" nipkow@61231 49 by(induction t) (auto) nipkow@61224 50 nipkow@61224 51 lemma inorder_balL: nipkow@61224 52 "inorder(balL l a r) = inorder l @ a # inorder r" nipkow@61231 53 by(induction l a r rule: balL.induct)(auto simp: inorder_bal inorder_red) nipkow@61224 54 nipkow@61224 55 lemma inorder_balR: nipkow@61224 56 "inorder(balR l a r) = inorder l @ a # inorder r" nipkow@61231 57 by(induction l a r rule: balR.induct) (auto simp: inorder_bal inorder_red) nipkow@61224 58 nipkow@61224 59 lemma inorder_combine: nipkow@61224 60 "inorder(combine l r) = inorder l @ inorder r" nipkow@61224 61 by(induction l r rule: combine.induct) nipkow@61231 62 (auto simp: inorder_balL inorder_balR split: tree.split color.split) nipkow@61224 63 nipkow@61224 64 lemma inorder_delete: nipkow@61224 65 "sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)" and nipkow@61224 66 "sorted(inorder l) \ inorder(deleteL x l a r) = nipkow@61224 67 del_list x (inorder l) @ a # inorder r" and nipkow@61224 68 "sorted(inorder r) \ inorder(deleteR x l a r) = nipkow@61224 69 inorder l @ a # del_list x (inorder r)" nipkow@61224 70 by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct) nipkow@61231 71 (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR) nipkow@61224 72 nipkow@61581 73 nipkow@61224 74 interpretation Set_by_Ordered nipkow@61224 75 where empty = Leaf and isin = isin and insert = insert and delete = delete nipkow@61224 76 and inorder = inorder and wf = "\_. True" nipkow@61224 77 proof (standard, goal_cases) nipkow@61224 78 case 1 show ?case by simp nipkow@61224 79 next nipkow@61224 80 case 2 thus ?case by(simp add: isin_set) nipkow@61224 81 next nipkow@61224 82 case 3 thus ?case by(simp add: inorder_insert) nipkow@61224 83 next nipkow@61224 84 case 4 thus ?case by(simp add: inorder_delete) nipkow@61428 85 qed (rule TrueI)+ nipkow@61224 86 nipkow@61224 87 end