9 text \<open>Braun Trees were studied by Braun and Rem~\cite{BraunRem} |
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> |
10 and later Hoogerwoord~\cite{Hoogerwoord} who gave them their name.\<close> |
11 |
11 |
12 fun braun :: "'a tree \<Rightarrow> bool" where |
12 fun braun :: "'a tree \<Rightarrow> bool" where |
13 "braun Leaf = True" | |
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)" |
14 "braun (Node l x r) = ((size l = size r \<or> size l = size r + 1) \<and> braun l \<and> braun r)" |
|
15 |
|
16 lemma braun_Node': |
|
17 "braun (Node l x r) = (size r \<le> size l \<and> size l \<le> size r + 1 \<and> braun l \<and> braun r)" |
|
18 by auto |
15 |
19 |
16 text \<open>The shape of a Braun-tree is uniquely determined by its size:\<close> |
20 text \<open>The shape of a Braun-tree is uniquely determined by its size:\<close> |
17 |
21 |
18 lemma braun_unique: "\<lbrakk> braun (t1::unit tree); braun t2; size t1 = size t2 \<rbrakk> \<Longrightarrow> t1 = t2" |
22 lemma braun_unique: "\<lbrakk> braun (t1::unit tree); braun t2; size t1 = size t2 \<rbrakk> \<Longrightarrow> t1 = t2" |
19 proof (induction t1 arbitrary: t2) |
23 proof (induction t1 arbitrary: t2) |
20 case Leaf thus ?case by simp |
24 case Leaf thus ?case by simp |
21 next |
25 next |
22 case (Node l1 _ r1) |
26 case (Node l1 _ r1) |
23 from Node.prems(3) have "t2 \<noteq> Leaf" by auto |
27 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) |
28 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 |
29 with Node.prems have "size l1 = size l2 \<and> size r1 = size r2" by auto |
26 thus ?case using Node.prems(1,2) Node.IH by auto |
30 thus ?case using Node.prems(1,2) Node.IH by auto |
27 qed |
31 qed |
28 |
32 |
29 text \<open>Braun trees are balanced:\<close> |
33 text \<open>Braun trees are balanced:\<close> |
30 |
34 |
32 proof(induction t) |
36 proof(induction t) |
33 case Leaf show ?case by (simp add: balanced_def) |
37 case Leaf show ?case by (simp add: balanced_def) |
34 next |
38 next |
35 case (Node l x r) |
39 case (Node l x r) |
36 have "size l = size r \<or> size l = size r + 1" (is "?A \<or> ?B") |
40 have "size l = size r \<or> size l = size r + 1" (is "?A \<or> ?B") |
37 using Node.prems by auto |
41 using Node.prems by simp |
38 thus ?case |
42 thus ?case |
39 proof |
43 proof |
40 assume "?A" |
44 assume "?A" |
41 thus ?thesis using Node |
45 thus ?thesis using Node |
42 apply(simp add: balanced_def min_def max_def) |
46 apply(simp add: balanced_def min_def max_def) |