# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1727358277 -3600
# Node ID 572970d15ab06a2c7cf7a5038e8ddf6565221745
# Parent  1ba97eb5e5e2fa7a448c3e66522597f93890bdb8
To tiny but maybe useful lemmas (moved in from the AFP, Word_Lib)

diff -r 1ba97eb5e5e2 -r 572970d15ab0 src/HOL/Complex_Analysis/Laurent_Convergence.thy
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Tue Sep 24 21:41:01 2024 +0200
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Thu Sep 26 14:44:37 2024 +0100
@@ -598,7 +598,7 @@
     by (rule asymp_equiv_symI, rule has_laurent_expansion_imp_asymp_equiv_0) fact
   show "(\<lambda>z. fls_nth F (fls_subdegree F) * z powi fls_subdegree F) \<midarrow>0\<rightarrow> fls_nth F 0"
     by (rule tendsto_eq_intros refl | use assms(2) in simp)+
-       (use assms(2) in \<open>auto simp: power_int_0_left_If\<close>)
+       (use assms(2) in \<open>auto simp: power_int_0_left_if\<close>)
 qed
 
 lemma has_laurent_expansion_imp_tendsto:
diff -r 1ba97eb5e5e2 -r 572970d15ab0 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Sep 24 21:41:01 2024 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 26 14:44:37 2024 +0100
@@ -633,6 +633,11 @@
   shows R
   using assms by (elim impCE)
 
+text \<open>The analogous introduction rule for conjunction, above, is even constructive\<close>
+lemma context_disjE:
+  assumes major: "P \<or> Q" and minor: "P \<Longrightarrow> R" "\<not>P \<Longrightarrow> Q \<Longrightarrow> R"
+  shows R
+  by (iprover intro: disjE [OF major] disjE [OF excluded_middle] assms)
 
 text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close>
 lemma iffCE:
diff -r 1ba97eb5e5e2 -r 572970d15ab0 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Sep 24 21:41:01 2024 +0200
+++ b/src/HOL/Int.thy	Thu Sep 26 14:44:37 2024 +0100
@@ -1790,11 +1790,11 @@
 lemma power_int_eq_0_iff [simp]: "power_int (x::'a) n = 0 \<longleftrightarrow> x = 0 \<and> n \<noteq> 0"
   by (auto simp: power_int_def)
 
-lemma power_int_0_left_If: "power_int (0 :: 'a) m = (if m = 0 then 1 else 0)"
+lemma power_int_0_left_if: "power_int (0 :: 'a) m = (if m = 0 then 1 else 0)"
   by (auto simp: power_int_def)
 
 lemma power_int_0_left [simp]: "m \<noteq> 0 \<Longrightarrow> power_int (0 :: 'a) m = 0"
-  by (simp add: power_int_0_left_If)
+  by (simp add: power_int_0_left_if)
 
 lemma power_int_1_left [simp]: "power_int 1 n = (1 :: 'a :: division_ring)"
   by (auto simp: power_int_def) 
@@ -1836,7 +1836,7 @@
   shows   "power_int (x::'a) (m + n) = power_int x m * power_int x n"
 proof (cases "x = 0")
   case True
-  thus ?thesis using assms by (auto simp: power_int_0_left_If)
+  thus ?thesis using assms by (auto simp: power_int_0_left_if)
 next
   case [simp]: False
   show ?thesis
@@ -2050,7 +2050,7 @@
   also have "\<dots> \<le> power_int a n * 1"
     using assms * by (intro mult_left_mono) (auto simp: power_int_def)
   finally show ?thesis by simp
-qed (use assms in \<open>auto simp: power_int_0_left_If\<close>)
+qed (use assms in \<open>auto simp: power_int_0_left_if\<close>)
 
 lemma one_less_power_int: "1 < (a :: 'a) \<Longrightarrow> 0 < n \<Longrightarrow> 1 < power_int a n"
   using power_int_strict_increasing[of 0 n a] by simp
diff -r 1ba97eb5e5e2 -r 572970d15ab0 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Sep 24 21:41:01 2024 +0200
+++ b/src/HOL/Power.thy	Thu Sep 26 14:44:37 2024 +0100
@@ -348,6 +348,10 @@
     by (simp add: power_add)
 qed
 
+lemma power_diff_if:
+  "a ^ (m - n) = (if n \<le> m then (a ^ m) div (a ^ n) else 1)" if "a \<noteq> 0"
+  by (simp add: power_diff that) 
+
 end
 
 context algebraic_semidom