author | nipkow |
Thu, 12 Nov 2020 12:44:17 +0100 | |
changeset 72586 | e3ba2578ad9d |
parent 72080 | 2030eacf3a72 |
permissions | -rw-r--r-- |
71796 | 1 |
section \<open>Augmented Tree (Tree2)\<close> |
2 |
||
61224 | 3 |
theory Tree2 |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
4 |
imports "HOL-Library.Tree" |
61224 | 5 |
begin |
6 |
||
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
7 |
text \<open>This theory provides the basic infrastructure for the type @{typ \<open>('a * 'b) tree\<close>} |
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
8 |
of augmented trees where @{typ 'a} is the key and @{typ 'b} some additional information.\<close> |
61224 | 9 |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
10 |
text \<open>IMPORTANT: Inductions and cases analyses on augmented trees need to use the following |
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
11 |
two rules explicitly. They generate nodes of the form @{term "Node l (a,b) r"} |
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
12 |
rather than @{term "Node l a r"} for trees of type @{typ "'a tree"}.\<close> |
61224 | 13 |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
14 |
lemmas tree2_induct = tree.induct[where 'a = "'a * 'b", split_format(complete)] |
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
15 |
|
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
16 |
lemmas tree2_cases = tree.exhaust[where 'a = "'a * 'b", split_format(complete)] |
67967 | 17 |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
18 |
fun inorder :: "('a*'b)tree \<Rightarrow> 'a list" where |
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
19 |
"inorder Leaf = []" | |
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
20 |
"inorder (Node l (a,_) r) = inorder l @ a # inorder r" |
62650 | 21 |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
22 |
fun set_tree :: "('a*'b) tree \<Rightarrow> 'a set" where |
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
23 |
"set_tree Leaf = {}" | |
72586 | 24 |
"set_tree (Node l (a,_) r) = {a} \<union> set_tree l \<union> set_tree r" |
70742 | 25 |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
26 |
fun bst :: "('a::linorder*'b) tree \<Rightarrow> bool" where |
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70745
diff
changeset
|
27 |
"bst Leaf = True" | |
72586 | 28 |
"bst (Node l (a, _) r) = ((\<forall>x \<in> set_tree l. x < a) \<and> (\<forall>x \<in> set_tree r. a < x) \<and> bst l \<and> bst r)" |
62650 | 29 |
|
68411 | 30 |
lemma finite_set_tree[simp]: "finite(set_tree t)" |
31 |
by(induction t) auto |
|
32 |
||
70745 | 33 |
lemma eq_set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf" |
70744 | 34 |
by (cases t) auto |
35 |
||
70762 | 36 |
lemma set_inorder[simp]: "set (inorder t) = set_tree t" |
37 |
by (induction t) auto |
|
38 |
||
72080 | 39 |
lemma length_inorder[simp]: "length (inorder t) = size t" |
40 |
by (induction t) auto |
|
41 |
||
62390 | 42 |
end |