author nipkow Wed, 17 Oct 2018 07:50:46 +0200 changeset 69143 5acb1eece41b parent 69142 c5e3212455ed child 69144 f13b82281715 child 69146 0b0680016187
more intuitive and simpler (but slower) proofs
```--- a/src/HOL/Data_Structures/Braun_Tree.thy	Tue Oct 16 18:34:44 2018 +0200
+++ b/src/HOL/Data_Structures/Braun_Tree.thy	Wed Oct 17 07:50:46 2018 +0200
@@ -11,7 +11,11 @@

fun braun :: "'a tree \<Rightarrow> bool" where
"braun Leaf = True" |
-"braun (Node l x r) = (size r \<le> size l \<and> size l \<le> size r + 1 \<and> braun l \<and> braun r)"
+"braun (Node l x r) = ((size l = size r \<or> size l = size r + 1) \<and> braun l \<and> braun r)"
+
+lemma braun_Node':
+  "braun (Node l x r) = (size r \<le> size l \<and> size l \<le> size r + 1 \<and> braun l \<and> braun r)"
+by auto

text \<open>The shape of a Braun-tree is uniquely determined by its size:\<close>

@@ -22,7 +26,7 @@
case (Node l1 _ r1)
from Node.prems(3) have "t2 \<noteq> Leaf" by auto
then obtain l2 x2 r2 where [simp]: "t2 = Node l2 x2 r2" by (meson neq_Leaf_iff)
-  with Node.prems have "size l1 = size l2 \<and> size r1 = size r2" by simp
+  with Node.prems have "size l1 = size l2 \<and> size r1 = size r2" by auto
thus ?case using Node.prems(1,2) Node.IH by auto
qed

@@ -34,7 +38,7 @@
next
case (Node l x r)
have "size l = size r \<or> size l = size r + 1" (is "?A \<or> ?B")
-    using Node.prems by auto
+    using Node.prems by simp
thus ?case
proof
assume "?A"```