# HG changeset patch
# User nipkow
# Date 1539755446 -7200
# Node ID 5acb1eece41bbc3fb66147a488f9f531ee648be2
# Parent  c5e3212455edda1d1351c1e42ab50f8e564d46d5
more intuitive and simpler (but slower) proofs

diff -r c5e3212455ed -r 5acb1eece41b src/HOL/Data_Structures/Braun_Tree.thy
--- 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"