more traditional formulation
authornipkow
Sun Sep 16 15:16:04 2018 +0200 (2 months ago)
changeset 68998818898556504
parent 68997 4278947ba336
child 68999 2af022252782
more traditional formulation
src/HOL/Data_Structures/RBT_Set.thy
src/HOL/Data_Structures/Tree2.thy
src/HOL/Library/Tree.thy
src/HOL/Library/Tree_Real.thy
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Sat Sep 15 23:35:46 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Sep 16 15:16:04 2018 +0200
     1.3 @@ -299,7 +299,7 @@
     1.4      by (simp add: powr_realpow bheight_size_bound rbt_def)
     1.5    finally have "2 powr (height t / 2) \<le> size1 t" .
     1.6    hence "height t / 2 \<le> log 2 (size1 t)"
     1.7 -    by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
     1.8 +    by (simp add: le_log_iff size1_size del: divide_le_eq_numeral1(1))
     1.9    thus ?thesis by simp
    1.10  qed
    1.11  
     2.1 --- a/src/HOL/Data_Structures/Tree2.thy	Sat Sep 15 23:35:46 2018 +0200
     2.2 +++ b/src/HOL/Data_Structures/Tree2.thy	Sun Sep 16 15:16:04 2018 +0200
     2.3 @@ -22,16 +22,15 @@
     2.4  "bst Leaf = True" |
     2.5  "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))"
     2.6  
     2.7 -definition size1 :: "('a,'b) tree \<Rightarrow> nat" where
     2.8 -"size1 t = size t + 1"
     2.9 +fun size1 :: "('a,'b) tree \<Rightarrow> nat" where
    2.10 +"size1 \<langle>\<rangle> = 1" |
    2.11 +"size1 \<langle>l, _, _, r\<rangle> = size1 l + size1 r"
    2.12  
    2.13 -lemma size1_simps[simp]:
    2.14 -  "size1 \<langle>\<rangle> = 1"
    2.15 -  "size1 \<langle>l, x, u, r\<rangle> = size1 l + size1 r"
    2.16 -by (simp_all add: size1_def)
    2.17 +lemma size1_size: "size1 t = size t + 1"
    2.18 +by (induction t) simp_all
    2.19  
    2.20  lemma size1_ge0[simp]: "0 < size1 t"
    2.21 -by (simp add: size1_def)
    2.22 +by (simp add: size1_size)
    2.23  
    2.24  lemma finite_set_tree[simp]: "finite(set_tree t)"
    2.25  by(induction t) auto
     3.1 --- a/src/HOL/Library/Tree.thy	Sat Sep 15 23:35:46 2018 +0200
     3.2 +++ b/src/HOL/Library/Tree.thy	Sun Sep 16 15:16:04 2018 +0200
     3.3 @@ -12,10 +12,11 @@
     3.4    Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
     3.5  datatype_compat tree
     3.6  
     3.7 -text\<open>Can be seen as counting the number of leaves rather than nodes:\<close>
     3.8 +text\<open>Counting the number of leaves rather than nodes:\<close>
     3.9  
    3.10 -definition size1 :: "'a tree \<Rightarrow> nat" where
    3.11 -"size1 t = size t + 1"
    3.12 +fun size1 :: "'a tree \<Rightarrow> nat" where
    3.13 +"size1 \<langle>\<rangle> = 1" |
    3.14 +"size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
    3.15  
    3.16  fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where
    3.17  "subtrees \<langle>\<rangle> = {\<langle>\<rangle>}" |
    3.18 @@ -102,13 +103,11 @@
    3.19  
    3.20  subsection \<open>@{const size}\<close>
    3.21  
    3.22 -lemma size1_simps[simp]:
    3.23 -  "size1 \<langle>\<rangle> = 1"
    3.24 -  "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
    3.25 -by (simp_all add: size1_def)
    3.26 +lemma size1_size: "size1 t = size t + 1"
    3.27 +by (induction t) simp_all
    3.28  
    3.29  lemma size1_ge0[simp]: "0 < size1 t"
    3.30 -by (simp add: size1_def)
    3.31 +by (simp add: size1_size)
    3.32  
    3.33  lemma eq_size_0[simp]: "size t = 0 \<longleftrightarrow> t = Leaf"
    3.34  by(cases t) auto
    3.35 @@ -123,7 +122,7 @@
    3.36  by (induction t) auto
    3.37  
    3.38  lemma size1_map_tree[simp]: "size1 (map_tree f t) = size1 t"
    3.39 -by (simp add: size1_def)
    3.40 +by (simp add: size1_size)
    3.41  
    3.42  
    3.43  subsection \<open>@{const set_tree}\<close>
    3.44 @@ -192,7 +191,7 @@
    3.45  qed simp
    3.46  
    3.47  corollary size_height: "size t \<le> 2 ^ height (t::'a tree) - 1"
    3.48 -using size1_height[of t, unfolded size1_def] by(arith)
    3.49 +using size1_height[of t, unfolded size1_size] by(arith)
    3.50  
    3.51  lemma height_subtrees: "s \<in> subtrees t \<Longrightarrow> height s \<le> height t"
    3.52  by (induction t) auto
    3.53 @@ -226,7 +225,7 @@
    3.54  by (induction t) auto
    3.55  
    3.56  lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1"
    3.57 -using size1_if_complete[simplified size1_def] by fastforce
    3.58 +using size1_if_complete[simplified size1_size] by fastforce
    3.59  
    3.60  lemma complete_if_size1_height: "size1 t = 2 ^ height t \<Longrightarrow> complete t"
    3.61  proof (induct "height t" arbitrary: t)
    3.62 @@ -275,7 +274,7 @@
    3.63  
    3.64  lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \<Longrightarrow> complete t"
    3.65  proof (induct "min_height t" arbitrary: t)
    3.66 -  case 0 thus ?case by (simp add: size1_def)
    3.67 +  case 0 thus ?case by (simp add: size1_size)
    3.68  next
    3.69    case (Suc h)
    3.70    hence "t \<noteq> Leaf" by auto
    3.71 @@ -353,7 +352,7 @@
    3.72    proof -
    3.73      have "2 ^ height t = size1 t"
    3.74        using True by (simp add: complete_iff_height size1_if_complete)
    3.75 -    also have "\<dots> \<le> size1 t'" using assms(2) by(simp add: size1_def)
    3.76 +    also have "\<dots> \<le> size1 t'" using assms(2) by(simp add: size1_size)
    3.77      also have "\<dots> \<le> 2 ^ height t'" by (rule size1_height)
    3.78      finally show ?thesis .
    3.79    qed
    3.80 @@ -364,7 +363,7 @@
    3.81    proof -
    3.82      have "(2::nat) ^ min_height t < size1 t"
    3.83        by(rule min_height_size1_if_incomplete[OF False])
    3.84 -    also have "\<dots> \<le> size1 t'" using assms(2) by (simp add: size1_def)
    3.85 +    also have "\<dots> \<le> size1 t'" using assms(2) by (simp add: size1_size)
    3.86      also have "\<dots> \<le> 2 ^ height t'"  by(rule size1_height)
    3.87      finally have "(2::nat) ^ min_height t < (2::nat) ^ height t'" .
    3.88      thus ?thesis .
    3.89 @@ -470,7 +469,7 @@
    3.90  by (induction t) simp_all
    3.91  
    3.92  lemma size1_mirror[simp]: "size1(mirror t) = size1 t"
    3.93 -by (simp add: size1_def)
    3.94 +by (simp add: size1_size)
    3.95  
    3.96  lemma height_mirror[simp]: "height(mirror t) = height t"
    3.97  by (induction t) simp_all
     4.1 --- a/src/HOL/Library/Tree_Real.thy	Sat Sep 15 23:35:46 2018 +0200
     4.2 +++ b/src/HOL/Library/Tree_Real.thy	Sun Sep 16 15:16:04 2018 +0200
     4.3 @@ -67,7 +67,7 @@
     4.4  assumes "balanced l" "balanced r" "size l = size r + 1"
     4.5  shows "balanced \<langle>l, x, r\<rangle>"
     4.6  proof -
     4.7 -  from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_def)
     4.8 +  from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_size)
     4.9    have "nat \<lceil>log 2 (1 + size1 r)\<rceil> \<ge> nat \<lceil>log 2 (size1 r)\<rceil>"
    4.10      by(rule nat_mono[OF ceiling_mono]) simp
    4.11    hence 1: "height(Node l x r) = nat \<lceil>log 2 (1 + size1 r)\<rceil> + 1"
    4.12 @@ -78,7 +78,7 @@
    4.13    hence 2: "min_height(Node l x r) = nat \<lfloor>log 2 (size1 r)\<rfloor> + 1"
    4.14      using min_height_balanced[OF assms(1)] min_height_balanced[OF assms(2)]
    4.15      by (simp)
    4.16 -  have "size1 r \<ge> 1" by(simp add: size1_def)
    4.17 +  have "size1 r \<ge> 1" by(simp add: size1_size)
    4.18    then obtain i where i: "2 ^ i \<le> size1 r" "size1 r < 2 ^ (i + 1)"
    4.19      using ex_power_ivl1[of 2 "size1 r"] by auto
    4.20    hence i1: "2 ^ i < size1 r + 1" "size1 r + 1 \<le> 2 ^ (i + 1)" by auto