src/HOL/Data_Structures/Tree_Map.thy
 author nipkow Wed Sep 23 09:14:22 2015 +0200 (2015-09-23) changeset 61231 cc6969542f8d parent 61224 759b5299a9f2 child 61534 a88e07c8d0d5 permissions -rw-r--r--
tuned
 nipkow@61203 ` 1` ```(* Author: Tobias Nipkow *) ``` nipkow@61203 ` 2` nipkow@61203 ` 3` ```section {* Unbalanced Tree as Map *} ``` nipkow@61203 ` 4` nipkow@61203 ` 5` ```theory Tree_Map ``` nipkow@61203 ` 6` ```imports ``` nipkow@61231 ` 7` ``` Tree_Set ``` nipkow@61203 ` 8` ``` Map_by_Ordered ``` nipkow@61203 ` 9` ```begin ``` nipkow@61203 ` 10` nipkow@61203 ` 11` ```fun lookup :: "('a::linorder*'b) tree \ 'a \ 'b option" where ``` nipkow@61203 ` 12` ```"lookup Leaf x = None" | ``` nipkow@61203 ` 13` ```"lookup (Node l (a,b) r) x = (if x < a then lookup l x else ``` nipkow@61203 ` 14` ``` if x > a then lookup r x else Some b)" ``` nipkow@61203 ` 15` nipkow@61203 ` 16` ```fun update :: "'a::linorder \ 'b \ ('a*'b) tree \ ('a*'b) tree" where ``` nipkow@61203 ` 17` ```"update a b Leaf = Node Leaf (a,b) Leaf" | ``` nipkow@61203 ` 18` ```"update a b (Node l (x,y) r) = ``` nipkow@61203 ` 19` ``` (if a < x then Node (update a b l) (x,y) r ``` nipkow@61203 ` 20` ``` else if a=x then Node l (a,b) r ``` nipkow@61203 ` 21` ``` else Node l (x,y) (update a b r))" ``` nipkow@61203 ` 22` nipkow@61203 ` 23` ```fun delete :: "'a::linorder \ ('a*'b) tree \ ('a*'b) tree" where ``` nipkow@61203 ` 24` ```"delete k Leaf = Leaf" | ``` nipkow@61203 ` 25` ```"delete k (Node l (a,b) r) = (if k a then Node l (a,b) (delete k r) else ``` nipkow@61203 ` 27` ``` if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')" ``` nipkow@61203 ` 28` nipkow@61203 ` 29` nipkow@61203 ` 30` ```subsection "Functional Correctness Proofs" ``` nipkow@61203 ` 31` nipkow@61224 ` 32` ```lemma lookup_eq: ``` nipkow@61224 ` 33` ``` "sorted1(inorder t) \ lookup t x = map_of (inorder t) x" ``` nipkow@61231 ` 34` ```by (induction t) (auto simp: map_of_simps split: option.split) ``` nipkow@61203 ` 35` nipkow@61203 ` 36` nipkow@61203 ` 37` ```lemma inorder_update: ``` nipkow@61203 ` 38` ``` "sorted1(inorder t) \ inorder(update a b t) = upd_list a b (inorder t)" ``` nipkow@61224 ` 39` ```by(induction t) (auto simp: upd_list_simps) ``` nipkow@61203 ` 40` nipkow@61203 ` 41` nipkow@61203 ` 42` ```lemma del_minD: ``` nipkow@61203 ` 43` ``` "del_min t = (x,t') \ t \ Leaf \ sorted1(inorder t) \ ``` nipkow@61203 ` 44` ``` x # inorder t' = inorder t" ``` nipkow@61203 ` 45` ```by(induction t arbitrary: t' rule: del_min.induct) ``` nipkow@61231 ` 46` ``` (auto simp: del_list_simps split: prod.splits) ``` nipkow@61203 ` 47` nipkow@61203 ` 48` ```lemma inorder_delete: ``` nipkow@61203 ` 49` ``` "sorted1(inorder t) \ inorder(delete x t) = del_list x (inorder t)" ``` nipkow@61231 ` 50` ```by(induction t) (auto simp: del_list_simps del_minD split: prod.splits) ``` nipkow@61203 ` 51` nipkow@61203 ` 52` nipkow@61203 ` 53` ```interpretation Map_by_Ordered ``` nipkow@61203 ` 54` ```where empty = Leaf and lookup = lookup and update = update and delete = delete ``` nipkow@61203 ` 55` ```and inorder = inorder and wf = "\_. True" ``` nipkow@61203 ` 56` ```proof (standard, goal_cases) ``` nipkow@61203 ` 57` ``` case 1 show ?case by simp ``` nipkow@61203 ` 58` ```next ``` nipkow@61203 ` 59` ``` case 2 thus ?case by(simp add: lookup_eq) ``` nipkow@61203 ` 60` ```next ``` nipkow@61203 ` 61` ``` case 3 thus ?case by(simp add: inorder_update) ``` nipkow@61203 ` 62` ```next ``` nipkow@61203 ` 63` ``` case 4 thus ?case by(simp add: inorder_delete) ``` nipkow@61203 ` 64` ```qed (rule TrueI)+ ``` nipkow@61203 ` 65` nipkow@61203 ` 66` ```end ```