--- 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:
--- 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:
--- 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
--- 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