# HG changeset patch
# User nipkow
# Date 1537103764 -7200
# Node ID 8188985565041f5a1a29244635e3a4c379e61971
# Parent  4278947ba336007da9df7e65aea87bab43215ac4
more traditional formulation

diff -r 4278947ba336 -r 818898556504 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Sat Sep 15 23:35:46 2018 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Sep 16 15:16:04 2018 +0200
@@ -299,7 +299,7 @@
     by (simp add: powr_realpow bheight_size_bound rbt_def)
   finally have "2 powr (height t / 2) \<le> size1 t" .
   hence "height t / 2 \<le> log 2 (size1 t)"
-    by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
+    by (simp add: le_log_iff size1_size del: divide_le_eq_numeral1(1))
   thus ?thesis by simp
 qed
 
diff -r 4278947ba336 -r 818898556504 src/HOL/Data_Structures/Tree2.thy
--- a/src/HOL/Data_Structures/Tree2.thy	Sat Sep 15 23:35:46 2018 +0200
+++ b/src/HOL/Data_Structures/Tree2.thy	Sun Sep 16 15:16:04 2018 +0200
@@ -22,16 +22,15 @@
 "bst Leaf = True" |
 "bst (Node l a _ r) = (bst l \<and> bst r \<and> (\<forall>x \<in> set_tree l. x < a) \<and> (\<forall>x \<in> set_tree r. a < x))"
 
-definition size1 :: "('a,'b) tree \<Rightarrow> nat" where
-"size1 t = size t + 1"
+fun size1 :: "('a,'b) tree \<Rightarrow> nat" where
+"size1 \<langle>\<rangle> = 1" |
+"size1 \<langle>l, _, _, r\<rangle> = size1 l + size1 r"
 
-lemma size1_simps[simp]:
-  "size1 \<langle>\<rangle> = 1"
-  "size1 \<langle>l, x, u, r\<rangle> = size1 l + size1 r"
-by (simp_all add: size1_def)
+lemma size1_size: "size1 t = size t + 1"
+by (induction t) simp_all
 
 lemma size1_ge0[simp]: "0 < size1 t"
-by (simp add: size1_def)
+by (simp add: size1_size)
 
 lemma finite_set_tree[simp]: "finite(set_tree t)"
 by(induction t) auto
diff -r 4278947ba336 -r 818898556504 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Sat Sep 15 23:35:46 2018 +0200
+++ b/src/HOL/Library/Tree.thy	Sun Sep 16 15:16:04 2018 +0200
@@ -12,10 +12,11 @@
   Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
 datatype_compat tree
 
-text\<open>Can be seen as counting the number of leaves rather than nodes:\<close>
+text\<open>Counting the number of leaves rather than nodes:\<close>
 
-definition size1 :: "'a tree \<Rightarrow> nat" where
-"size1 t = size t + 1"
+fun size1 :: "'a tree \<Rightarrow> nat" where
+"size1 \<langle>\<rangle> = 1" |
+"size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
 
 fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where
 "subtrees \<langle>\<rangle> = {\<langle>\<rangle>}" |
@@ -102,13 +103,11 @@
 
 subsection \<open>@{const size}\<close>
 
-lemma size1_simps[simp]:
-  "size1 \<langle>\<rangle> = 1"
-  "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
-by (simp_all add: size1_def)
+lemma size1_size: "size1 t = size t + 1"
+by (induction t) simp_all
 
 lemma size1_ge0[simp]: "0 < size1 t"
-by (simp add: size1_def)
+by (simp add: size1_size)
 
 lemma eq_size_0[simp]: "size t = 0 \<longleftrightarrow> t = Leaf"
 by(cases t) auto
@@ -123,7 +122,7 @@
 by (induction t) auto
 
 lemma size1_map_tree[simp]: "size1 (map_tree f t) = size1 t"
-by (simp add: size1_def)
+by (simp add: size1_size)
 
 
 subsection \<open>@{const set_tree}\<close>
@@ -192,7 +191,7 @@
 qed simp
 
 corollary size_height: "size t \<le> 2 ^ height (t::'a tree) - 1"
-using size1_height[of t, unfolded size1_def] by(arith)
+using size1_height[of t, unfolded size1_size] by(arith)
 
 lemma height_subtrees: "s \<in> subtrees t \<Longrightarrow> height s \<le> height t"
 by (induction t) auto
@@ -226,7 +225,7 @@
 by (induction t) auto
 
 lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1"
-using size1_if_complete[simplified size1_def] by fastforce
+using size1_if_complete[simplified size1_size] by fastforce
 
 lemma complete_if_size1_height: "size1 t = 2 ^ height t \<Longrightarrow> complete t"
 proof (induct "height t" arbitrary: t)
@@ -275,7 +274,7 @@
 
 lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \<Longrightarrow> complete t"
 proof (induct "min_height t" arbitrary: t)
-  case 0 thus ?case by (simp add: size1_def)
+  case 0 thus ?case by (simp add: size1_size)
 next
   case (Suc h)
   hence "t \<noteq> Leaf" by auto
@@ -353,7 +352,7 @@
   proof -
     have "2 ^ height t = size1 t"
       using True by (simp add: complete_iff_height size1_if_complete)
-    also have "\<dots> \<le> size1 t'" using assms(2) by(simp add: size1_def)
+    also have "\<dots> \<le> size1 t'" using assms(2) by(simp add: size1_size)
     also have "\<dots> \<le> 2 ^ height t'" by (rule size1_height)
     finally show ?thesis .
   qed
@@ -364,7 +363,7 @@
   proof -
     have "(2::nat) ^ min_height t < size1 t"
       by(rule min_height_size1_if_incomplete[OF False])
-    also have "\<dots> \<le> size1 t'" using assms(2) by (simp add: size1_def)
+    also have "\<dots> \<le> size1 t'" using assms(2) by (simp add: size1_size)
     also have "\<dots> \<le> 2 ^ height t'"  by(rule size1_height)
     finally have "(2::nat) ^ min_height t < (2::nat) ^ height t'" .
     thus ?thesis .
@@ -470,7 +469,7 @@
 by (induction t) simp_all
 
 lemma size1_mirror[simp]: "size1(mirror t) = size1 t"
-by (simp add: size1_def)
+by (simp add: size1_size)
 
 lemma height_mirror[simp]: "height(mirror t) = height t"
 by (induction t) simp_all
diff -r 4278947ba336 -r 818898556504 src/HOL/Library/Tree_Real.thy
--- a/src/HOL/Library/Tree_Real.thy	Sat Sep 15 23:35:46 2018 +0200
+++ b/src/HOL/Library/Tree_Real.thy	Sun Sep 16 15:16:04 2018 +0200
@@ -67,7 +67,7 @@
 assumes "balanced l" "balanced r" "size l = size r + 1"
 shows "balanced \<langle>l, x, r\<rangle>"
 proof -
-  from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_def)
+  from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_size)
   have "nat \<lceil>log 2 (1 + size1 r)\<rceil> \<ge> nat \<lceil>log 2 (size1 r)\<rceil>"
     by(rule nat_mono[OF ceiling_mono]) simp
   hence 1: "height(Node l x r) = nat \<lceil>log 2 (1 + size1 r)\<rceil> + 1"
@@ -78,7 +78,7 @@
   hence 2: "min_height(Node l x r) = nat \<lfloor>log 2 (size1 r)\<rfloor> + 1"
     using min_height_balanced[OF assms(1)] min_height_balanced[OF assms(2)]
     by (simp)
-  have "size1 r \<ge> 1" by(simp add: size1_def)
+  have "size1 r \<ge> 1" by(simp add: size1_size)
   then obtain i where i: "2 ^ i \<le> size1 r" "size1 r < 2 ^ (i + 1)"
     using ex_power_ivl1[of 2 "size1 r"] by auto
   hence i1: "2 ^ i < size1 r + 1" "size1 r + 1 \<le> 2 ^ (i + 1)" by auto