src/HOL/Library/Tree.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 58424 cbbba613b6ab child 58438 566117a31cc0 permissions -rw-r--r--
simpler proof
 nipkow@57250 ` 1` ```(* Author: Tobias Nipkow *) ``` nipkow@57250 ` 2` nipkow@57250 ` 3` ```header {* Binary Tree *} ``` nipkow@57250 ` 4` nipkow@57250 ` 5` ```theory Tree ``` nipkow@57250 ` 6` ```imports Main ``` nipkow@57250 ` 7` ```begin ``` nipkow@57250 ` 8` nipkow@58424 ` 9` ```datatype 'a tree = ``` nipkow@58424 ` 10` ``` Leaf ("\\") | ``` nipkow@58424 ` 11` ``` Node (left: "'a tree") (val: 'a) (right: "'a tree") ("\_, _, _\") ``` hoelzl@57449 ` 12` ``` where ``` hoelzl@57449 ` 13` ``` "left Leaf = Leaf" ``` hoelzl@57449 ` 14` ``` | "right Leaf = Leaf" ``` hoelzl@57569 ` 15` ```datatype_compat tree ``` nipkow@57250 ` 16` nipkow@58424 ` 17` ```lemma neq_Leaf_iff: "(t \ \\) = (\l a r. t = \l, a, r\)" ``` nipkow@58424 ` 18` ```by (cases t) auto ``` nipkow@57530 ` 19` nipkow@57687 ` 20` ```lemma finite_set_tree[simp]: "finite(set_tree t)" ``` nipkow@57687 ` 21` ```by(induction t) auto ``` nipkow@57687 ` 22` nipkow@57687 ` 23` nipkow@57687 ` 24` ```subsection "The set of subtrees" ``` nipkow@57687 ` 25` nipkow@57250 ` 26` ```fun subtrees :: "'a tree \ 'a tree set" where ``` nipkow@58424 ` 27` ``` "subtrees \\ = {\\}" | ``` nipkow@58424 ` 28` ``` "subtrees (\l, a, r\) = insert \l, a, r\ (subtrees l \ subtrees r)" ``` nipkow@57250 ` 29` nipkow@58424 ` 30` ```lemma set_treeE: "a \ set_tree t \ \l r. \l, a, r\ \ subtrees t" ``` nipkow@58424 ` 31` ```by (induction t)(auto) ``` hoelzl@57449 ` 32` hoelzl@57450 ` 33` ```lemma Node_notin_subtrees_if[simp]: "a \ set_tree t \ Node l a r \ subtrees t" ``` nipkow@58424 ` 34` ```by (induction t) auto ``` hoelzl@57449 ` 35` nipkow@58424 ` 36` ```lemma in_set_tree_if: "\l, a, r\ \ subtrees t \ a \ set_tree t" ``` nipkow@58424 ` 37` ```by (metis Node_notin_subtrees_if) ``` hoelzl@57449 ` 38` nipkow@57687 ` 39` nipkow@57687 ` 40` ```subsection "Inorder list of entries" ``` nipkow@57687 ` 41` nipkow@57250 ` 42` ```fun inorder :: "'a tree \ 'a list" where ``` nipkow@58424 ` 43` ```"inorder \\ = []" | ``` nipkow@58424 ` 44` ```"inorder \l, x, r\ = inorder l @ [x] @ inorder r" ``` nipkow@57250 ` 45` hoelzl@57449 ` 46` ```lemma set_inorder[simp]: "set (inorder t) = set_tree t" ``` nipkow@58424 ` 47` ```by (induction t) auto ``` nipkow@57250 ` 48` nipkow@57687 ` 49` hoelzl@57449 ` 50` ```subsection {* Binary Search Tree predicate *} ``` nipkow@57250 ` 51` hoelzl@57450 ` 52` ```fun (in linorder) bst :: "'a tree \ bool" where ``` nipkow@58424 ` 53` ```"bst \\ \ True" | ``` nipkow@58424 ` 54` ```"bst \l, a, r\ \ bst l \ bst r \ (\x\set_tree l. x < a) \ (\x\set_tree r. a < x)" ``` nipkow@57250 ` 55` hoelzl@57450 ` 56` ```lemma (in linorder) bst_imp_sorted: "bst t \ sorted (inorder t)" ``` nipkow@58424 ` 57` ```by (induction t) (auto simp: sorted_append sorted_Cons intro: less_imp_le less_trans) ``` nipkow@57250 ` 58` nipkow@57687 ` 59` nipkow@57687 ` 60` ```subsection "Deletion of the rightmost entry" ``` nipkow@57687 ` 61` nipkow@57687 ` 62` ```fun del_rightmost :: "'a tree \ 'a tree * 'a" where ``` nipkow@58424 ` 63` ```"del_rightmost \l, a, \\\ = (l,a)" | ``` nipkow@58424 ` 64` ```"del_rightmost \l, a, r\ = (let (r',x) = del_rightmost r in (\l, a, r'\, x))" ``` nipkow@57687 ` 65` nipkow@57687 ` 66` ```lemma del_rightmost_set_tree_if_bst: ``` nipkow@57687 ` 67` ``` "\ del_rightmost t = (t',x); bst t; t \ Leaf \ ``` nipkow@57687 ` 68` ``` \ x \ set_tree t \ set_tree t' = set_tree t - {x}" ``` nipkow@57687 ` 69` ```apply(induction t arbitrary: t' rule: del_rightmost.induct) ``` nipkow@57687 ` 70` ``` apply (fastforce simp: ball_Un split: prod.splits)+ ``` nipkow@57687 ` 71` ```done ``` nipkow@57687 ` 72` nipkow@57687 ` 73` ```lemma del_rightmost_set_tree: ``` nipkow@58424 ` 74` ``` "\ del_rightmost t = (t',x); t \ \\ \ \ set_tree t = insert x (set_tree t')" ``` nipkow@57687 ` 75` ```apply(induction t arbitrary: t' rule: del_rightmost.induct) ``` nipkow@57687 ` 76` ```by (auto split: prod.splits) auto ``` nipkow@57687 ` 77` nipkow@57687 ` 78` ```lemma del_rightmost_bst: ``` nipkow@58424 ` 79` ``` "\ del_rightmost t = (t',x); bst t; t \ \\ \ \ bst t'" ``` nipkow@57687 ` 80` ```proof(induction t arbitrary: t' rule: del_rightmost.induct) ``` nipkow@57687 ` 81` ``` case (2 l a rl b rr) ``` nipkow@57687 ` 82` ``` let ?r = "Node rl b rr" ``` nipkow@57687 ` 83` ``` from "2.prems"(1) obtain r' where 1: "del_rightmost ?r = (r',x)" and [simp]: "t' = Node l a r'" ``` nipkow@57687 ` 84` ``` by(simp split: prod.splits) ``` nipkow@57687 ` 85` ``` from "2.prems"(2) 1 del_rightmost_set_tree[OF 1] show ?case by(auto)(simp add: "2.IH") ``` nipkow@57687 ` 86` ```qed auto ``` nipkow@57687 ` 87` nipkow@57687 ` 88` nipkow@58424 ` 89` ```lemma del_rightmost_greater: "\ del_rightmost t = (t',x); bst t; t \ \\ \ ``` nipkow@57687 ` 90` ``` \ \a\set_tree t'. a < x" ``` nipkow@57687 ` 91` ```proof(induction t arbitrary: t' rule: del_rightmost.induct) ``` nipkow@57687 ` 92` ``` case (2 l a rl b rr) ``` nipkow@57687 ` 93` ``` from "2.prems"(1) obtain r' ``` nipkow@57687 ` 94` ``` where dm: "del_rightmost (Node rl b rr) = (r',x)" and [simp]: "t' = Node l a r'" ``` nipkow@57687 ` 95` ``` by(simp split: prod.splits) ``` nipkow@57687 ` 96` ``` show ?case using "2.prems"(2) "2.IH"[OF dm] del_rightmost_set_tree_if_bst[OF dm] ``` nipkow@57687 ` 97` ``` by (fastforce simp add: ball_Un) ``` nipkow@57687 ` 98` ```qed simp_all ``` nipkow@57687 ` 99` nipkow@57687 ` 100` ```(* should be moved but metis not available in much of Main *) ``` nipkow@57687 ` 101` ```lemma Max_insert1: "\ finite A; \a\A. a \ x \ \ Max(insert x A) = x" ``` nipkow@57687 ` 102` ```by (metis Max_in Max_insert Max_singleton antisym max_def) ``` nipkow@57687 ` 103` nipkow@57687 ` 104` ```lemma del_rightmost_Max: ``` nipkow@58424 ` 105` ``` "\ del_rightmost t = (t',x); bst t; t \ \\ \ \ x = Max(set_tree t)" ``` nipkow@57687 ` 106` ```by (metis Max_insert1 del_rightmost_greater del_rightmost_set_tree finite_set_tree less_le_not_le) ``` nipkow@57687 ` 107` nipkow@57250 ` 108` ```end ```