# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1584201531 0
# Node ID 66bc4b668d6ed078ffa16c97e5ae987c17588381
# Parent  317e9ebbc3e1ef90c8fb992ec4d488a9f97ea623
tidied up a few little proofs

diff -r 317e9ebbc3e1 -r 66bc4b668d6e src/HOL/Hilbert_Choice.thy
--- 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>.
diff -r 317e9ebbc3e1 -r 66bc4b668d6e src/HOL/Real_Vector_Spaces.thy
--- 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
 
diff -r 317e9ebbc3e1 -r 66bc4b668d6e src/HOL/Wellfounded.thy
--- 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>
 
diff -r 317e9ebbc3e1 -r 66bc4b668d6e src/HOL/Wfrec.thy
--- 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