author  hoelzl 
Thu, 17 Jul 2014 14:55:56 +0200  
changeset 57569  e20a999f7161 
parent 57530  439f881c8744 
child 57687  cca7e8788481 
permissions  rwrr 
57250  1 
(* Author: Tobias Nipkow *) 
2 

3 
header {* Binary Tree *} 

4 

5 
theory Tree 

6 
imports Main 

7 
begin 

8 

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

9 
datatype_new 'a tree = Leaf  Node (left: "'a tree") (val: 'a) (right: "'a tree") 
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

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

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

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

13 
datatype_compat tree 
57250  14 

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

15 
lemma neq_Leaf_iff: "(t \<noteq> Leaf) = (\<exists>l a r. t = Node l a r)" 
57450  16 
by (cases t) auto 
57250  17 

57530  18 
lemma set_tree_Node2: "set_tree(Node l x r) = insert x (set_tree l \<union> set_tree r)" 
19 
by auto 

20 

57250  21 
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where 
57450  22 
"subtrees Leaf = {Leaf}"  
23 
"subtrees (Node l a r) = insert (Node l a r) (subtrees l \<union> subtrees r)" 

57250  24 

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

25 
lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. Node l a r \<in> subtrees t" 
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

26 
by (induction t)(auto) 
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

27 

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

29 
by (induction t) auto 
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

30 

57450  31 
lemma in_set_tree_if: "Node l a r \<in> subtrees t \<Longrightarrow> a \<in> set_tree t" 
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

32 
by (metis Node_notin_subtrees_if) 
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

33 

57250  34 
fun inorder :: "'a tree \<Rightarrow> 'a list" where 
57450  35 
"inorder Leaf = []"  
36 
"inorder (Node l x r) = inorder l @ [x] @ inorder r" 

57250  37 

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

38 
lemma set_inorder[simp]: "set (inorder t) = set_tree t" 
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

39 
by (induction t) auto 
57250  40 

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

41 
subsection {* Binary Search Tree predicate *} 
57250  42 

57450  43 
fun (in linorder) bst :: "'a tree \<Rightarrow> bool" where 
44 
"bst Leaf \<longleftrightarrow> True"  

45 
"bst (Node l a r) \<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  46 

57450  47 
lemma (in linorder) bst_imp_sorted: "bst t \<Longrightarrow> sorted (inorder t)" 
48 
by (induction t) (auto simp: sorted_append sorted_Cons intro: less_imp_le less_trans) 

57250  49 

50 
end 