--- a/src/HOL/Algebra/Group.thy Tue Jul 17 22:18:27 2018 +0100
+++ b/src/HOL/Algebra/Group.thy Thu Jul 19 17:27:44 2018 +0200
@@ -114,10 +114,8 @@
lemma (in monoid) Units_inv_closed [intro, simp]:
"x \<in> Units G ==> inv x \<in> carrier G"
- apply (unfold Units_def m_inv_def, auto)
- apply (rule theI2, fast)
- apply (fast intro: inv_unique, fast)
- done
+ apply (simp add: Units_def m_inv_def)
+ by (metis (mono_tags, lifting) inv_unique the_equality)
lemma (in monoid) Units_l_inv_ex:
"x \<in> Units G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
@@ -129,10 +127,8 @@
lemma (in monoid) Units_l_inv [simp]:
"x \<in> Units G ==> inv x \<otimes> x = \<one>"
- apply (unfold Units_def m_inv_def, auto)
- apply (rule theI2, fast)
- apply (fast intro: inv_unique, fast)
- done
+ apply (unfold Units_def m_inv_def, simp)
+ by (metis (mono_tags, lifting) inv_unique the_equality)
lemma (in monoid) Units_r_inv [simp]:
"x \<in> Units G ==> x \<otimes> inv x = \<one>"
@@ -415,16 +411,15 @@
by (simp add: int_pow_def2)
lemma (in group) int_pow_mult:
- "x \<in> carrier G \<Longrightarrow> x [^] (i + j::int) = x [^] i \<otimes> x [^] j"
+ assumes "x \<in> carrier G" shows "x [^] (i + j::int) = x [^] i \<otimes> x [^] j"
proof -
have [simp]: "-i - j = -j - i" by simp
- assume "x \<in> carrier G" then
show ?thesis
- by (auto simp add: int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
+ by (auto simp add: assms int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
qed
lemma (in group) nat_pow_inv:
- "x \<in> carrier G \<Longrightarrow> (inv x) [^] (i :: nat) = inv (x [^] i)"
+ assumes "x \<in> carrier G" shows "(inv x) [^] (i :: nat) = inv (x [^] i)"
proof (induction i)
case 0 thus ?case by simp
next
@@ -434,9 +429,9 @@
also have " ... = (inv (x [^] i)) \<otimes> inv x"
by (simp add: Suc.IH Suc.prems)
also have " ... = inv (x \<otimes> (x [^] i))"
- using inv_mult_group[OF Suc.prems nat_pow_closed[OF Suc.prems, of i]] by simp
+ by (simp add: assms inv_mult_group)
also have " ... = inv (x [^] (Suc i))"
- using Suc.prems nat_pow_Suc2 by auto
+ using assms nat_pow_Suc2 by auto
finally show ?case .
qed
@@ -475,13 +470,13 @@
lemma (in group) int_pow_diff:
"x \<in> carrier G \<Longrightarrow> x [^] (n - m :: int) = x [^] n \<otimes> inv (x [^] m)"
-by(simp only: diff_conv_add_uminus int_pow_mult int_pow_neg)
+ by(simp only: diff_conv_add_uminus int_pow_mult int_pow_neg)
lemma (in group) inj_on_multc: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. x \<otimes> c) (carrier G)"
-by(simp add: inj_on_def)
+ by(simp add: inj_on_def)
lemma (in group) inj_on_cmult: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. c \<otimes> x) (carrier G)"
-by(simp add: inj_on_def)
+ by(simp add: inj_on_def)
(*Following subsection contributed by Martin Baillon*)
subsection \<open>Submonoids\<close>
@@ -736,20 +731,16 @@
simp add: DirProd_def)
qed
-lemma carrier_DirProd [simp]:
- "carrier (G \<times>\<times> H) = carrier G \<times> carrier H"
+lemma carrier_DirProd [simp]: "carrier (G \<times>\<times> H) = carrier G \<times> carrier H"
by (simp add: DirProd_def)
-lemma one_DirProd [simp]:
- "\<one>\<^bsub>G \<times>\<times> H\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
+lemma one_DirProd [simp]: "\<one>\<^bsub>G \<times>\<times> H\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
by (simp add: DirProd_def)
-lemma mult_DirProd [simp]:
- "(g, h) \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
+lemma mult_DirProd [simp]: "(g, h) \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
by (simp add: DirProd_def)
-lemma DirProd_assoc :
-"(G \<times>\<times> H \<times>\<times> I) = (G \<times>\<times> (H \<times>\<times> I))"
+lemma DirProd_assoc: "(G \<times>\<times> H \<times>\<times> I) = (G \<times>\<times> (H \<times>\<times> I))"
by auto
lemma inv_DirProd [simp]:
@@ -841,8 +832,8 @@
using iso_set_sym unfolding is_iso_def by auto
lemma (in group) iso_set_trans:
- "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
-by (auto simp add: iso_def hom_compose bij_betw_compose)
+ "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
+ by (auto simp add: iso_def hom_compose bij_betw_compose)
corollary (in group) iso_trans: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
using iso_set_trans unfolding is_iso_def by blast
@@ -918,12 +909,11 @@
using iso_set_sym assms unfolding is_iso_def by blast
define \<psi> where psi_def: "\<psi> = inv_into (carrier G) \<phi>"
- from phi
have surj: "\<phi> ` (carrier G) = (carrier H)" "\<psi> ` (carrier H) = (carrier G)"
and inj: "inj_on \<phi> (carrier G)" "inj_on \<psi> (carrier H)"
and phi_hom: "\<And>g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow> \<phi> (g1 \<otimes> g2) = (\<phi> g1) \<otimes>\<^bsub>H\<^esub> (\<phi> g2)"
and psi_hom: "\<And>h1 h2. \<lbrakk> h1 \<in> carrier H; h2 \<in> carrier H \<rbrakk> \<Longrightarrow> \<psi> (h1 \<otimes>\<^bsub>H\<^esub> h2) = (\<psi> h1) \<otimes> (\<psi> h2)"
- using psi_def unfolding iso_def bij_betw_def hom_def by auto
+ using phi psi_def unfolding iso_def bij_betw_def hom_def by auto
have phi_one: "\<phi> \<one> = \<one>\<^bsub>H\<^esub>"
proof -
@@ -1007,8 +997,7 @@
qed
corollary (in group) DirProd_iso_trans :
- assumes "G \<cong> G2"
- and "H \<cong> I"
+ assumes "G \<cong> G2" and "H \<cong> I"
shows "G \<times>\<times> H \<cong> G2 \<times>\<times> I"
using DirProd_iso_set_trans assms unfolding is_iso_def by blast
@@ -1033,12 +1022,10 @@
with homh [unfolded hom_def] show ?thesis by auto
qed
-lemma (in group_hom) one_closed [simp]:
- "h \<one> \<in> carrier H"
+lemma (in group_hom) one_closed [simp]: "h \<one> \<in> carrier H"
by simp
-lemma (in group_hom) hom_one [simp]:
- "h \<one> = \<one>\<^bsub>H\<^esub>"
+lemma (in group_hom) hom_one [simp]: "h \<one> = \<one>\<^bsub>H\<^esub>"
proof -
have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^bsub>H\<^esub> h \<one>"
by (simp add: hom_mult [symmetric] del: hom_mult)
@@ -1050,15 +1037,11 @@
by simp
lemma (in group_hom) hom_inv [simp]:
- "x \<in> carrier G ==> h (inv x) = inv\<^bsub>H\<^esub> (h x)"
+ assumes "x \<in> carrier G" shows "h (inv x) = inv\<^bsub>H\<^esub> (h x)"
proof -
- assume x: "x \<in> carrier G"
- then have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = \<one>\<^bsub>H\<^esub>"
- by (simp add: hom_mult [symmetric] del: hom_mult)
- also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
- by (simp add: hom_mult [symmetric] del: hom_mult)
- finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
- with x show ?thesis by (simp del: H.r_inv H.Units_r_inv)
+ have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
+ using assms by (simp flip: hom_mult)
+ with assms show ?thesis by (simp del: H.r_inv H.Units_r_inv)
qed
(* Contributed by Joachim Breitner *)
@@ -1182,8 +1165,7 @@
locale comm_group = comm_monoid + group
lemma (in group) group_comm_groupI:
- assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
- x \<otimes> y = y \<otimes> x"
+ assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
shows "comm_group G"
by standard (simp_all add: m_comm)
--- a/src/HOL/Real.thy Tue Jul 17 22:18:27 2018 +0100
+++ b/src/HOL/Real.thy Thu Jul 19 17:27:44 2018 +0200
@@ -76,12 +76,16 @@
unfolding vanishes_def by simp
lemma vanishes_const [simp]: "vanishes (\<lambda>n. c) \<longleftrightarrow> c = 0"
- unfolding vanishes_def
- apply (cases "c = 0")
- apply auto
- apply (rule exI [where x = "\<bar>c\<bar>"])
- apply auto
- done
+proof (cases "c = 0")
+ case True
+ then show ?thesis
+ by (simp add: vanishesI)
+next
+ case False
+ then show ?thesis
+ unfolding vanishes_def
+ using zero_less_abs_iff by blast
+qed
lemma vanishes_minus: "vanishes X \<Longrightarrow> vanishes (\<lambda>n. - X n)"
unfolding vanishes_def by simp
@@ -290,12 +294,7 @@
and nz: "\<not> vanishes X"
shows "\<exists>b>0. \<exists>k. \<forall>n\<ge>k. b < \<bar>X n\<bar>"
using cauchy_not_vanishes_cases [OF assms]
- apply clarify
- apply (rule exI)
- apply (erule conjI)
- apply (rule_tac x = k in exI)
- apply auto
- done
+ by (elim ex_forward conj_forward asm_rl) auto
lemma cauchy_inverse [simp]:
assumes X: "cauchy X"
@@ -378,12 +377,7 @@
by (simp add: realrel_def)
lemma symp_realrel: "symp realrel"
- unfolding realrel_def
- apply (rule sympI)
- apply clarify
- apply (drule vanishes_minus)
- apply simp
- done
+ by (simp add: abs_minus_commute realrel_def symp_def vanishes_def)
lemma transp_realrel: "transp realrel"
unfolding realrel_def
@@ -440,10 +434,14 @@
by (simp only: cauchy_minus vanishes_minus simp_thms)
lift_definition times_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n * Y n"
- unfolding realrel_def mult_diff_mult
- apply (subst (4) mult.commute)
- apply (simp only: cauchy_mult vanishes_add vanishes_mult_bounded cauchy_imp_bounded simp_thms)
- done
+proof -
+ fix f1 f2 f3 f4
+ have "\<lbrakk>cauchy f1; cauchy f4; vanishes (\<lambda>n. f1 n - f2 n); vanishes (\<lambda>n. f3 n - f4 n)\<rbrakk>
+ \<Longrightarrow> vanishes (\<lambda>n. f1 n * (f3 n - f4 n) + f4 n * (f1 n - f2 n))"
+ by (simp add: vanishes_add vanishes_mult_bounded cauchy_imp_bounded)
+ then show "\<lbrakk>realrel f1 f2; realrel f3 f4\<rbrakk> \<Longrightarrow> realrel (\<lambda>n. f1 n * f3 n) (\<lambda>n. f2 n * f4 n)"
+ by (simp add: mult.commute realrel_def mult_diff_mult)
+qed
lift_definition inverse_real :: "real \<Rightarrow> real"
is "\<lambda>X. if vanishes X then (\<lambda>n. 0) else (\<lambda>n. inverse (X n))"
@@ -510,17 +508,17 @@
by transfer (simp add: distrib_right realrel_def)
show "(0::real) \<noteq> (1::real)"
by transfer (simp add: realrel_def)
- show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
- apply transfer
- apply (simp add: realrel_def)
- apply (rule vanishesI)
- apply (frule (1) cauchy_not_vanishes)
- apply clarify
- apply (rule_tac x=k in exI)
- apply clarify
- apply (drule_tac x=n in spec)
- apply simp
- done
+ have "vanishes (\<lambda>n. inverse (X n) * X n - 1)" if X: "cauchy X" "\<not> vanishes X" for X
+ proof (rule vanishesI)
+ fix r::rat
+ assume "0 < r"
+ obtain b k where "b>0" "\<forall>n\<ge>k. b < \<bar>X n\<bar>"
+ using X cauchy_not_vanishes by blast
+ then show "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) * X n - 1\<bar> < r"
+ using \<open>0 < r\<close> by force
+ qed
+ then show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
+ by transfer (simp add: realrel_def)
show "a div b = a * inverse b"
by (rule divide_real_def)
show "inverse (0::real) = 0"
@@ -595,9 +593,7 @@
lemma positive_minus: "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
apply transfer
apply (simp add: realrel_def)
- apply (drule (1) cauchy_not_vanishes_cases)
- apply safe
- apply blast+
+ apply (blast intro: dest: cauchy_not_vanishes_cases)
done
instantiation real :: linordered_field
@@ -617,38 +613,18 @@
show "\<bar>a\<bar> = (if a < 0 then - a else a)"
by (rule abs_real_def)
show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
- unfolding less_eq_real_def less_real_def
- apply auto
- apply (drule (1) positive_add)
- apply (simp_all add: positive_zero)
- done
- show "a \<le> a"
- unfolding less_eq_real_def by simp
- show "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
+ "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c" "a \<le> a"
+ "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b"
+ "a \<le> b \<Longrightarrow> c + a \<le> c + b"
unfolding less_eq_real_def less_real_def
- apply auto
- apply (drule (1) positive_add)
- apply (simp add: algebra_simps)
- done
- show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b"
- unfolding less_eq_real_def less_real_def
- apply auto
- apply (drule (1) positive_add)
- apply (simp add: positive_zero)
- done
- show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
- by (auto simp: less_eq_real_def less_real_def)
- (* FIXME: Procedure int_combine_numerals: c + b - (c + a) \<equiv> b + - a *)
- (* Should produce c + b - (c + a) \<equiv> b - a *)
+ by (force simp add: positive_zero dest: positive_add)+
show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
by (rule sgn_real_def)
show "a \<le> b \<or> b \<le> a"
by (auto dest!: positive_minus simp: less_eq_real_def less_real_def)
show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
unfolding less_real_def
- apply (drule (1) positive_mult)
- apply (simp add: algebra_simps)
- done
+ by (force simp add: algebra_simps dest: positive_mult)
qed
end
@@ -672,28 +648,30 @@
by (cases x rule: int_diff_cases) (simp add: of_nat_Real diff_Real)
lemma of_rat_Real: "of_rat x = Real (\<lambda>n. x)"
- apply (induct x)
+proof (induct x)
+ case (Fract a b)
+ then show ?case
apply (simp add: Fract_of_int_quotient of_rat_divide)
- apply (simp add: of_int_Real divide_inverse)
- apply (simp add: inverse_Real mult_Real)
+ apply (simp add: of_int_Real divide_inverse inverse_Real mult_Real)
done
+qed
instance real :: archimedean_field
proof
show "\<exists>z. x \<le> of_int z" for x :: real
- apply (induct x)
- apply (frule cauchy_imp_bounded, clarify)
- apply (rule_tac x="\<lceil>b\<rceil> + 1" in exI)
- apply (rule less_imp_le)
- apply (simp add: of_int_Real less_real_def diff_Real positive_Real)
- apply (rule_tac x=1 in exI)
- apply (simp add: algebra_simps)
- apply (rule_tac x=0 in exI)
- apply clarsimp
- apply (rule le_less_trans [OF abs_ge_self])
- apply (rule less_le_trans [OF _ le_of_int_ceiling])
- apply simp
- done
+ proof (induct x)
+ case (1 X)
+ then obtain b where "0 < b" and b: "\<And>n. \<bar>X n\<bar> < b"
+ by (blast dest: cauchy_imp_bounded)
+ then have "Real X < of_int (\<lceil>b\<rceil> + 1)"
+ using 1
+ apply (simp add: of_int_Real less_real_def diff_Real positive_Real)
+ apply (rule_tac x=1 in exI)
+ apply (simp add: algebra_simps)
+ by (metis abs_ge_self le_less_trans le_of_int_ceiling less_le)
+ then show ?case
+ using less_eq_real_def by blast
+ qed
qed
instantiation real :: floor_ceiling
@@ -712,30 +690,17 @@
subsection \<open>Completeness\<close>
-lemma not_positive_Real: "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)" if "cauchy X"
- apply (simp only: positive_Real [OF that])
+lemma not_positive_Real: "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)" (is "?lhs = ?rhs")
+ if "cauchy X"
+ unfolding positive_Real [OF that]
apply auto
apply (unfold not_less)
apply (erule obtain_pos_sum)
apply (drule_tac x=s in spec)
apply simp
apply (drule_tac r=t in cauchyD [OF that])
- apply clarify
- apply (drule_tac x=k in spec)
- apply clarsimp
- apply (rule_tac x=n in exI)
- apply clarify
- apply (rename_tac m)
- apply (drule_tac x=m in spec)
- apply simp
- apply (drule_tac x=n in spec)
- apply simp
- apply (drule spec)
- apply (drule (1) mp)
- apply clarify
- apply (rename_tac i)
- apply (rule_tac x = "max i k" in exI)
- apply simp
+ apply fastforce
+ apply (meson le_cases)
done
lemma le_Real:
@@ -857,12 +822,7 @@
apply (frule_tac y=y in ex_less_of_nat_mult)
apply clarify
apply (rule_tac x=n in exI)
- apply (erule less_trans)
- apply (rule mult_strict_right_mono)
- apply (rule le_less_trans [OF _ of_nat_less_two_power])
- apply simp
- apply assumption
- done
+ by (metis less_trans mult.commute mult_less_cancel_left_pos of_nat_less_two_power)
have PA: "\<not> P (A n)" for n
by (induct n) (simp_all add: a)
@@ -871,10 +831,7 @@
have ab: "a < b"
using a b unfolding P_def
apply (clarsimp simp add: not_le)
- apply (drule (1) bspec)
- apply (drule (1) less_le_trans)
- apply (simp add: of_rat_less)
- done
+ using less_le_trans of_rat_less by blast
have AB: "A n < B n" for n
by (induct n) (simp_all add: ab C_def avg_def)
have A_mono: "\<And>i j. i \<le> j \<Longrightarrow> A i \<le> A j"