# HG changeset patch
# User nipkow
# Date 1540562321 -7200
# Node ID b6434dce1126f968e65dd8759d74a7ab81e894e6
# Parent  6d514e128a8577cc703fee9d9f757e558897fa77
avoid abbreviation that is used only locally

diff -r 6d514e128a85 -r b6434dce1126 src/HOL/Data_Structures/Braun_Tree.thy
--- a/src/HOL/Data_Structures/Braun_Tree.thy	Fri Oct 26 08:20:45 2018 +0000
+++ b/src/HOL/Data_Structures/Braun_Tree.thy	Fri Oct 26 15:58:41 2018 +0200
@@ -56,21 +56,15 @@
 text \<open>We show that a tree is a Braun tree iff a parity-based
 numbering (\<open>braun_indices\<close>) of nodes yields an interval of numbers.\<close>
 
-abbreviation double :: "nat \<Rightarrow> nat" where
-"double \<equiv> (*) 2"
-
-abbreviation double1 :: "nat \<Rightarrow> nat" where
-"double1 \<equiv> \<lambda>n. Suc(2*n)"
-
 fun braun_indices :: "'a tree \<Rightarrow> nat set" where
 "braun_indices Leaf = {}" |
-"braun_indices (Node l _ r) = {1} \<union> double ` braun_indices l \<union> double1 ` braun_indices r"
+"braun_indices (Node l _ r) = {1} \<union> (*) 2 ` braun_indices l \<union> Suc ` (*) 2 ` braun_indices r"
 
 lemma braun_indices_if_braun: "braun t \<Longrightarrow> braun_indices t = {1..size t}"
 proof(induction t)
   case Leaf thus ?case by simp
 next
-  have *: "double ` {a..b} \<union> double1 ` {a..b} = {2*a..2*b+1}" (is "?l = ?r") for a b
+  have *: "(*) 2 ` {a..b} \<union> Suc ` (*) 2 ` {a..b} = {2*a..2*b+1}" (is "?l = ?r") for a b
   proof
     show "?l \<subseteq> ?r" by auto
   next
@@ -205,7 +199,7 @@
 lemma finite_braun_indices: "finite(braun_indices t)"
 by (induction t) auto
 
-lemma evens_odds_disj: "double  ` braun_indices A \<inter> double1 ` B = {}"
+lemma evens_odds_disj: "(*) 2 ` braun_indices A \<inter> Suc ` (*) 2 ` B = {}"
 using double_not_eq_Suc_double by auto
 
 lemma card_braun_indices: "card (braun_indices t) = size t"
@@ -232,14 +226,14 @@
   case (Node t1 x2 t2)
   have 1: "i > 0 \<Longrightarrow> Suc(Suc(2 * (i - Suc 0))) = 2*i" for i::nat by(simp add: algebra_simps)
   have 2: "i > 0 \<Longrightarrow> 2 * (i - Suc 0) + 3 = 2*i + 1" for i::nat by(simp add: algebra_simps)
-  have 3: "double ` braun_indices t1 \<union> double1 ` braun_indices t2 =
+  have 3: "(*) 2 ` braun_indices t1 \<union> Suc ` (*) 2 ` braun_indices t2 =
      {2..size t1 + size t2 + 1}" using Node.prems braun_indices1[of 0 t2]
     apply simp
     apply(drule eq)
      apply auto
     done
   thus ?case using Node.IH even_odd_decomp[OF _ _ 3]
-    by(simp add: card_image inj_on_def card_braun_indices Let_def 1 2 inj_image_eq_iff
+    by(simp add: card_image inj_on_def card_braun_indices Let_def 1 2 inj_image_eq_iff image_comp
            cong: image_cong_strong)
 qed