--- a/src/HOL/Hilbert_Choice.thy Thu Mar 12 23:05:11 2020 +0100
+++ b/src/HOL/Hilbert_Choice.thy Sat Mar 14 15:58:51 2020 +0000
@@ -57,6 +57,10 @@
apply (erule someI)
done
+lemma some_eq_imp:
+ assumes "Eps P = a" "P b" shows "P a"
+ using assms someI_ex by force
+
text \<open>
Easier to apply than \<open>someI\<close> because the conclusion has only one
occurrence of \<^term>\<open>P\<close>.
--- a/src/HOL/Real_Vector_Spaces.thy Thu Mar 12 23:05:11 2020 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Sat Mar 14 15:58:51 2020 +0000
@@ -277,7 +277,7 @@
by (simp add: of_real_def scaleR_left_diff_distrib)
lemma of_real_mult [simp]: "of_real (x * y) = of_real x * of_real y"
- by (simp add: of_real_def mult.commute)
+ by (simp add: of_real_def)
lemma of_real_sum[simp]: "of_real (sum f s) = (\<Sum>x\<in>s. of_real (f x))"
by (induct s rule: infinite_finite_induct) auto
@@ -1365,7 +1365,7 @@
lemma sgn_mult: "sgn (x * y) = sgn x * sgn y"
for x y :: "'a::real_normed_div_algebra"
- by (simp add: sgn_div_norm norm_mult mult.commute)
+ by (simp add: sgn_div_norm norm_mult)
hide_fact (open) sgn_mult
--- a/src/HOL/Wellfounded.thy Thu Mar 12 23:05:11 2020 +0100
+++ b/src/HOL/Wellfounded.thy Sat Mar 14 15:58:51 2020 +0000
@@ -724,17 +724,20 @@
text \<open>Inverse Image\<close>
-lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)"
- for f :: "'a \<Rightarrow> 'b"
- apply (simp add: inv_image_def wf_eq_minimal)
- apply clarify
- apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}")
- prefer 2
- apply (blast del: allE)
- apply (erule allE)
- apply (erule (1) notE impE)
- apply blast
- done
+lemma wf_inv_image [simp,intro!]:
+ fixes f :: "'a \<Rightarrow> 'b"
+ assumes "wf r"
+ shows "wf (inv_image r f)"
+proof (clarsimp simp: inv_image_def wf_eq_minimal)
+ fix P and x::'a
+ assume "x \<in> P"
+ then obtain w where w: "w \<in> {w. \<exists>x::'a. x \<in> P \<and> f x = w}"
+ by auto
+ have *: "\<And>Q u. u \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
+ using assms by (auto simp add: wf_eq_minimal)
+ show "\<exists>z\<in>P. \<forall>y. (f y, f z) \<in> r \<longrightarrow> y \<notin> P"
+ using * [OF w] by auto
+qed
text \<open>Measure functions into \<^typ>\<open>nat\<close>\<close>
--- a/src/HOL/Wfrec.thy Thu Mar 12 23:05:11 2020 +0100
+++ b/src/HOL/Wfrec.thy Sat Mar 14 15:58:51 2020 +0000
@@ -96,15 +96,17 @@
by (simp add: same_fst_def)
lemma wf_same_fst:
- assumes prem: "\<And>x. P x \<Longrightarrow> wf (R x)"
+ assumes "\<And>x. P x \<Longrightarrow> wf (R x)"
shows "wf (same_fst P R)"
- apply (simp cong del: imp_cong add: wf_def same_fst_def)
- apply (intro strip)
- apply (rename_tac a b)
- apply (case_tac "wf (R a)")
- apply (erule_tac a = b in wf_induct)
- apply blast
- apply (blast intro: prem)
- done
+proof (clarsimp simp add: wf_def same_fst_def)
+ fix Q a b
+ assume *: "\<forall>a b. (\<forall>x. P a \<and> (x,b) \<in> R a \<longrightarrow> Q (a,x)) \<longrightarrow> Q (a,b)"
+ show "Q(a,b)"
+ proof (cases "wf (R a)")
+ case True
+ then show ?thesis
+ by (induction b rule: wf_induct_rule) (use * in blast)
+ qed (use * assms in blast)
+qed
end