author nipkow Sat, 27 Oct 2018 15:30:38 +0200 changeset 69200 9218b7652839 parent 69199 50aa773f62d2 child 69201 f2bb47056d8f child 69202 e5e4de2b93d9
moved lemmas
 src/HOL/Data_Structures/Braun_Tree.thy file | annotate | diff | comparison | revisions src/HOL/Parity.thy file | annotate | diff | comparison | revisions src/HOL/Set_Interval.thy file | annotate | diff | comparison | revisions
--- 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)"
-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"
card_atLeastAtMost_even[of m n, simplified A[symmetric]]
card_atLeastAtMost_odd[of m n, simplified B[symmetric]] split!: if_splits)
by linarith
--- 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)"
+
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"
--- 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}"