# HG changeset patch
# User nipkow
# Date 1540580850 -7200
# Node ID 930dbc6610d089085b3cff73125c8f794280e727
# Parent  b6434dce1126f968e65dd8759d74a7ab81e894e6
tuned and added lemmas

diff -r b6434dce1126 -r 930dbc6610d0 src/HOL/Data_Structures/Braun_Tree.thy
--- a/src/HOL/Data_Structures/Braun_Tree.thy	Fri Oct 26 15:58:41 2018 +0200
+++ b/src/HOL/Data_Structures/Braun_Tree.thy	Fri Oct 26 21:07:30 2018 +0200
@@ -6,6 +6,12 @@
 imports "HOL-Library.Tree_Real"
 begin
 
+(* FIXME mv *)
+lemma mod2_iff: "x mod 2 = (if even x then 0 else 1)"
+by (simp add: odd_iff_mod_2_eq_one)
+lemma Icc_eq_insert_lb_nat: "m \<le> n \<Longrightarrow> {m..n} = insert m {Suc m..n}"
+by auto
+
 text \<open>Braun Trees were studied by Braun and Rem~\cite{BraunRem}
 and later Hoogerwoord~\cite{Hoogerwoord}.\<close>
 
@@ -60,6 +66,12 @@
 "braun_indices Leaf = {}" |
 "braun_indices (Node l _ r) = {1} \<union> (*) 2 ` braun_indices l \<union> Suc ` (*) 2 ` braun_indices r"
 
+lemma braun_indices1: "0 \<notin> braun_indices t"
+by (induction t) auto
+
+lemma finite_braun_indices: "finite(braun_indices t)"
+by (induction t) auto
+
 lemma braun_indices_if_braun: "braun t \<Longrightarrow> braun_indices t = {1..size t}"
 proof(induction t)
   case Leaf thus ?case by simp
@@ -88,6 +100,30 @@
   qed
 qed
 
+lemma disj_evens_odds: "(*) 2 ` A \<inter> Suc ` (*) 2 ` B = {}"
+using double_not_eq_Suc_double by auto
+
+lemma Suc0_notin_double: "Suc 0 \<notin> (*) 2 ` A"
+by(auto)
+
+lemma zero_in_double_iff: "(0::nat) \<in> (*) 2 ` A \<longleftrightarrow> 0 \<in> A"
+by(auto)
+
+lemma Suc_in_Suc_image_iff: "Suc n \<in> Suc ` A \<longleftrightarrow> n \<in> A"
+by(auto)
+
+lemmas nat_in_image = Suc0_notin_double zero_in_double_iff Suc_in_Suc_image_iff
+
+lemma card_braun_indices: "card (braun_indices t) = size t"
+proof (induction t)
+  case Leaf thus ?case by simp
+next
+  case Node
+  thus ?case
+    by(auto simp: UNION_singleton_eq_range finite_braun_indices card_Un_disjoint
+                  card_insert_if disj_evens_odds card_image inj_on_def braun_indices1)
+qed
+
 text \<open>How many even/odd natural numbers are there between m and n?\<close>
 
 lemma card_atLeastAtMost_even:
@@ -129,9 +165,6 @@
   finally show ?thesis .
 qed
 
-lemma mod2_iff: "x mod 2 = (if even x then 0 else 1)"
-by (simp add: odd_iff_mod_2_eq_one)
-
 lemma compact_ivl_even: assumes "A = {i \<in> {m..n}. even i}"
 shows "A = (\<lambda>j. 2*(j-1) + m + m mod 2) ` {1..card A}" (is "_ = ?A")
 proof
@@ -193,31 +226,6 @@
   with ab A' B' show ?thesis by simp
 qed
 
-lemma braun_indices1: "i \<in> braun_indices t \<Longrightarrow> i \<ge> 1"
-by (induction t arbitrary: i) auto
-
-lemma finite_braun_indices: "finite(braun_indices t)"
-by (induction t) auto
-
-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"
-proof (induction t)
-  case Leaf thus ?case by simp
-next
-  case Node
-  thus ?case
-    by(auto simp: UNION_singleton_eq_range finite_braun_indices card_Un_disjoint
-                  card_insert_if evens_odds_disj card_image inj_on_def dest: braun_indices1)
-qed
-
-lemma eq: "insert (Suc 0) M = {Suc 0..n} \<Longrightarrow> Suc 0 \<notin> M \<Longrightarrow> M = {2..n}"
-by (metis Suc_n_not_le_n atLeastAtMost_iff atLeastAtMost_insertL insertI1 insert_ident numeral_2_eq_2)
-
-lemma inj_on_Suc: "inj_on f N \<Longrightarrow> inj_on (\<lambda>n. Suc(f n)) N"
-by (simp add: inj_on_def)
-
 lemma braun_if_braun_indices: "braun_indices t = {1..size t} \<Longrightarrow> braun t"
 proof(induction t)
 case Leaf
@@ -227,11 +235,8 @@
   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: "(*) 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
+     {2..size t1 + size t2 + 1}" using Node.prems
+    by (simp add: insert_ident Icc_eq_insert_lb_nat nat_in_image braun_indices1)
   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 image_comp
            cong: image_cong_strong)