author  nipkow 
Thu, 25 Sep 2014 11:38:56 +0200  
changeset 58438  566117a31cc0 
parent 58424  cbbba613b6ab 
child 58467  6a3da58f7233 
permissions  rwrr 
57250  1 
(* Author: Tobias Nipkow *) 
2 

3 
header {* Binary Tree *} 

4 

5 
theory Tree 

6 
imports Main 

7 
begin 

8 

58424  9 
datatype 'a tree = 
10 
Leaf ("\<langle>\<rangle>")  

11 
Node (left: "'a tree") (val: 'a) (right: "'a tree") ("\<langle>_, _, _\<rangle>") 

57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

12 
where 
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

13 
"left Leaf = Leaf" 
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

14 
 "right Leaf = Leaf" 
57569
e20a999f7161
register tree with datatype_compat ot support QuickCheck
hoelzl
parents:
57530
diff
changeset

15 
datatype_compat tree 
57250  16 

58438  17 
text{* Can be seen as counting the number of leaves rather than nodes: *} 
18 

19 
definition size1 :: "'a tree \<Rightarrow> nat" where 

20 
"size1 t = size t + 1" 

21 

22 
lemma size1_simps[simp]: 

23 
"size1 \<langle>\<rangle> = 1" 

24 
"size1 \<langle>l, x, r\<rangle> = size1 l + size1 r" 

25 
by (simp_all add: size1_def) 

26 

58424  27 
lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)" 
28 
by (cases t) auto 

57530  29 

57687  30 
lemma finite_set_tree[simp]: "finite(set_tree t)" 
31 
by(induction t) auto 

32 

33 

34 
subsection "The set of subtrees" 

35 

57250  36 
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where 
58424  37 
"subtrees \<langle>\<rangle> = {\<langle>\<rangle>}"  
38 
"subtrees (\<langle>l, a, r\<rangle>) = insert \<langle>l, a, r\<rangle> (subtrees l \<union> subtrees r)" 

57250  39 

58424  40 
lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. \<langle>l, a, r\<rangle> \<in> subtrees t" 
41 
by (induction t)(auto) 

57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

42 

57450  43 
lemma Node_notin_subtrees_if[simp]: "a \<notin> set_tree t \<Longrightarrow> Node l a r \<notin> subtrees t" 
58424  44 
by (induction t) auto 
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

45 

58424  46 
lemma in_set_tree_if: "\<langle>l, a, r\<rangle> \<in> subtrees t \<Longrightarrow> a \<in> set_tree t" 
47 
by (metis Node_notin_subtrees_if) 

57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

48 

57687  49 

50 
subsection "Inorder list of entries" 

51 

57250  52 
fun inorder :: "'a tree \<Rightarrow> 'a list" where 
58424  53 
"inorder \<langle>\<rangle> = []"  
54 
"inorder \<langle>l, x, r\<rangle> = inorder l @ [x] @ inorder r" 

57250  55 

57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

56 
lemma set_inorder[simp]: "set (inorder t) = set_tree t" 
58424  57 
by (induction t) auto 
57250  58 

57687  59 

57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

60 
subsection {* Binary Search Tree predicate *} 
57250  61 

57450  62 
fun (in linorder) bst :: "'a tree \<Rightarrow> bool" where 
58424  63 
"bst \<langle>\<rangle> \<longleftrightarrow> True"  
64 
"bst \<langle>l, a, r\<rangle> \<longleftrightarrow> bst l \<and> bst r \<and> (\<forall>x\<in>set_tree l. x < a) \<and> (\<forall>x\<in>set_tree r. a < x)" 

57250  65 

57450  66 
lemma (in linorder) bst_imp_sorted: "bst t \<Longrightarrow> sorted (inorder t)" 
58424  67 
by (induction t) (auto simp: sorted_append sorted_Cons intro: less_imp_le less_trans) 
57250  68 

57687  69 

70 
subsection "Deletion of the rightmost entry" 

71 

72 
fun del_rightmost :: "'a tree \<Rightarrow> 'a tree * 'a" where 

58424  73 
"del_rightmost \<langle>l, a, \<langle>\<rangle>\<rangle> = (l,a)"  
74 
"del_rightmost \<langle>l, a, r\<rangle> = (let (r',x) = del_rightmost r in (\<langle>l, a, r'\<rangle>, x))" 

57687  75 

76 
lemma del_rightmost_set_tree_if_bst: 

77 
"\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> Leaf \<rbrakk> 

78 
\<Longrightarrow> x \<in> set_tree t \<and> set_tree t' = set_tree t  {x}" 

79 
apply(induction t arbitrary: t' rule: del_rightmost.induct) 

80 
apply (fastforce simp: ball_Un split: prod.splits)+ 

81 
done 

82 

83 
lemma del_rightmost_set_tree: 

58424  84 
"\<lbrakk> del_rightmost t = (t',x); t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> set_tree t = insert x (set_tree t')" 
57687  85 
apply(induction t arbitrary: t' rule: del_rightmost.induct) 
86 
by (auto split: prod.splits) auto 

87 

88 
lemma del_rightmost_bst: 

58424  89 
"\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> bst t'" 
57687  90 
proof(induction t arbitrary: t' rule: del_rightmost.induct) 
91 
case (2 l a rl b rr) 

92 
let ?r = "Node rl b rr" 

93 
from "2.prems"(1) obtain r' where 1: "del_rightmost ?r = (r',x)" and [simp]: "t' = Node l a r'" 

94 
by(simp split: prod.splits) 

95 
from "2.prems"(2) 1 del_rightmost_set_tree[OF 1] show ?case by(auto)(simp add: "2.IH") 

96 
qed auto 

97 

98 

58424  99 
lemma del_rightmost_greater: "\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> \<langle>\<rangle> \<rbrakk> 
57687  100 
\<Longrightarrow> \<forall>a\<in>set_tree t'. a < x" 
101 
proof(induction t arbitrary: t' rule: del_rightmost.induct) 

102 
case (2 l a rl b rr) 

103 
from "2.prems"(1) obtain r' 

104 
where dm: "del_rightmost (Node rl b rr) = (r',x)" and [simp]: "t' = Node l a r'" 

105 
by(simp split: prod.splits) 

106 
show ?case using "2.prems"(2) "2.IH"[OF dm] del_rightmost_set_tree_if_bst[OF dm] 

107 
by (fastforce simp add: ball_Un) 

108 
qed simp_all 

109 

110 
(* should be moved but metis not available in much of Main *) 

111 
lemma Max_insert1: "\<lbrakk> finite A; \<forall>a\<in>A. a \<le> x \<rbrakk> \<Longrightarrow> Max(insert x A) = x" 

112 
by (metis Max_in Max_insert Max_singleton antisym max_def) 

113 

114 
lemma del_rightmost_Max: 

58424  115 
"\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> x = Max(set_tree t)" 
57687  116 
by (metis Max_insert1 del_rightmost_greater del_rightmost_set_tree finite_set_tree less_le_not_le) 
117 

57250  118 
end 