# HG changeset patch
# User nipkow
# Date 1540647038 -7200
# Node ID 9218b7652839f2d1038de3088606ea18e2a84423
# Parent  50aa773f62d2a0a0dd2d4f17340d87468596fe47
moved lemmas

diff -r 50aa773f62d2 -r 9218b7652839 src/HOL/Data_Structures/Braun_Tree.thy
--- a/src/HOL/Data_Structures/Braun_Tree.thy	Fri Oct 26 21:19:07 2018 +0200
+++ b/src/HOL/Data_Structures/Braun_Tree.thy	Sat Oct 27 15:30:38 2018 +0200
@@ -6,12 +6,6 @@
 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>
 
@@ -191,7 +185,7 @@
   have "\<exists>j \<in> {1..?a}. i = 2*(j-1) + m + m mod 2" if *: "i \<in> {m..n}" "even i" for i
   proof -
     let ?j = "(i - (m + m mod 2)) div 2 + 1"
-    have "?j \<in> {1..?a} \<and> i = 2*(?j-1) + m + m mod 2" using * by(auto simp: mod2_iff) presburger+
+    have "?j \<in> {1..?a} \<and> i = 2*(?j-1) + m + m mod 2" using * by(auto simp: mod2_eq_if) presburger+
     thus ?thesis by blast
   qed
   thus "A \<subseteq> ?A" using assms
@@ -199,7 +193,7 @@
 next
   let ?a = "(n+1-m + (m+1) mod 2) div 2"
   have 1: "2 * (j - 1) + m + m mod 2 \<in> {m..n}" if *: "j \<in> {1..?a}" for j
-    using * by(auto simp: mod2_iff)
+    using * by(auto simp: mod2_eq_if)
   have 2: "even (2 * (j - 1) + m + m mod 2)" for j by presburger
   show "?A \<subseteq> A"
     apply(simp add: assms card_atLeastAtMost_even del: atLeastAtMost_iff One_nat_def)
@@ -238,7 +232,7 @@
   have B: "B = {i \<in> {m..n}. odd i}" using assms by auto
   hence B': "B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..?b}" by(rule compact_ivl_odd)
   have "?a = ?b \<or> ?a = ?b+1 \<and> even m \<or> ?a+1 = ?b \<and> odd m"
-    apply(simp add: Let_def mod2_iff
+    apply(simp add: Let_def mod2_eq_if
       card_atLeastAtMost_even[of m n, simplified A[symmetric]]
       card_atLeastAtMost_odd[of m n, simplified B[symmetric]] split!: if_splits)
     by linarith
diff -r 50aa773f62d2 -r 9218b7652839 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Fri Oct 26 21:19:07 2018 +0200
+++ b/src/HOL/Parity.thy	Sat Oct 27 15:30:38 2018 +0200
@@ -154,6 +154,9 @@
     by (auto intro: division_segment_eq_iff simp add: division_segment_mod)
 qed
 
+lemma mod2_eq_if: "x mod 2 = (if even x then 0 else 1)"
+by (simp add: odd_iff_mod_2_eq_one)
+
 lemma parity_cases [case_names even odd]:
   assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
   assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P"
diff -r 50aa773f62d2 -r 9218b7652839 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Oct 26 21:19:07 2018 +0200
+++ b/src/HOL/Set_Interval.thy	Sat Oct 27 15:30:38 2018 +0200
@@ -770,6 +770,9 @@
 
 subsubsection \<open>The Constant @{term atLeastAtMost}\<close>
 
+lemma Icc_eq_insert_lb_nat: "m \<le> n \<Longrightarrow> {m..n} = insert m {Suc m..n}"
+by auto
+
 lemma atLeast0_atMost_Suc:
   "{0..Suc n} = insert (Suc n) {0..n}"
   by (simp add: atLeast0AtMost atMost_Suc)