equal
deleted
inserted
replaced
|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 section \<open>Braun Trees\<close> |
|
4 |
|
5 theory Braun_Tree |
|
6 imports "HOL-Library.Tree_Real" |
|
7 begin |
|
8 |
|
9 text \<open>Braun Trees were studied by Braun and Rem~\cite{BraunRem} |
|
10 and later Hoogerwoord~\cite{Hoogerwoord} who gave them their name.\<close> |
|
11 |
|
12 fun braun :: "'a tree \<Rightarrow> bool" where |
|
13 "braun Leaf = True" | |
|
14 "braun (Node l x r) = (size r \<le> size l \<and> size l \<le> size r + 1 \<and> braun l \<and> braun r)" |
|
15 |
|
16 text \<open>The shape of a Braun-tree is uniquely determined by its size:\<close> |
|
17 |
|
18 lemma braun_unique: "\<lbrakk> braun (t1::unit tree); braun t2; size t1 = size t2 \<rbrakk> \<Longrightarrow> t1 = t2" |
|
19 proof (induction t1 arbitrary: t2) |
|
20 case Leaf thus ?case by simp |
|
21 next |
|
22 case (Node l1 _ r1) |
|
23 from Node.prems(3) have "t2 \<noteq> Leaf" by auto |
|
24 then obtain l2 x2 r2 where [simp]: "t2 = Node l2 x2 r2" by (meson neq_Leaf_iff) |
|
25 with Node.prems have "size l1 = size l2 \<and> size r1 = size r2" by simp |
|
26 thus ?case using Node.prems(1,2) Node.IH by auto |
|
27 qed |
|
28 |
|
29 text \<open>Braun trees are balanced:\<close> |
|
30 |
|
31 lemma balanced_if_braun: "braun t \<Longrightarrow> balanced t" |
|
32 proof(induction t) |
|
33 case Leaf show ?case by (simp add: balanced_def) |
|
34 next |
|
35 case (Node l x r) |
|
36 have "size l = size r \<or> size l = size r + 1" (is "?A \<or> ?B") |
|
37 using Node.prems by auto |
|
38 thus ?case |
|
39 proof |
|
40 assume "?A" |
|
41 thus ?thesis using Node |
|
42 apply(simp add: balanced_def min_def max_def) |
|
43 by (metis Node.IH balanced_optimal le_antisym le_refl) |
|
44 next |
|
45 assume "?B" |
|
46 thus ?thesis using Node by(intro balanced_Node_if_wbal1) auto |
|
47 qed |
|
48 qed |
|
49 |
|
50 end |