src/HOL/Lattices_Big.thy

 lemma arg_minI:
   "\<lbrakk> P x;
     \<And>y. P y \<Longrightarrow> \<not> f y < f x;
     \<And>x. \<lbrakk> P x; \<forall>y. P y \<longrightarrow> \<not> f y < f x \<rbrakk> \<Longrightarrow> Q x \<rbrakk>
   \<Longrightarrow> Q (arg_min f P)"
-apply (simp add: arg_min_def is_arg_min_def)
-apply (rule someI2_ex)
- apply blast
-apply blast
-done
+  unfolding arg_min_def is_arg_min_def
+  by (blast intro!: someI2_ex)
 
 lemma arg_min_equality:
   "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f k \<le> f x \<rbrakk> \<Longrightarrow> f (arg_min f P) = f k"
   for f :: "_ \<Rightarrow> 'a::order"
-apply (rule arg_minI)
-  apply assumption
- apply (simp add: less_le_not_le)
-by (metis le_less)
+  by (rule arg_minI; force simp: not_less less_le_not_le)
 
 lemma wf_linord_ex_has_least:
   "\<lbrakk> wf r; \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>*; P k \<rbrakk>
    \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)"
-apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
-apply (drule_tac x = "m ` Collect P" in spec)
-by force
+  by (force dest!:  wf_trancl [THEN wf_eq_minimal [THEN iffD1, THEN spec], where x = "m ` Collect P"])
 
 lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)"
   for m :: "'a \<Rightarrow> nat"
-apply (simp only: pred_nat_trancl_eq_le [symmetric])
-apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
- apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
-by assumption
+  unfolding pred_nat_trancl_eq_le [symmetric]
+  apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
+   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
+  by assumption
 
 lemma arg_min_nat_lemma:
   "P k \<Longrightarrow> P(arg_min m P) \<and> (\<forall>y. P y \<longrightarrow> m (arg_min m P) \<le> m y)"
   for m :: "'a \<Rightarrow> nat"
-apply (simp add: arg_min_def is_arg_min_linorder)
-apply (rule someI_ex)
-apply (erule ex_has_least_nat)
-done
+  unfolding arg_min_def is_arg_min_linorder
+  apply (rule someI_ex)
+  apply (erule ex_has_least_nat)
+  done
 
 lemmas arg_min_natI = arg_min_nat_lemma [THEN conjunct1]
 
 lemma is_arg_min_arg_min_nat: fixes m :: "'a \<Rightarrow> nat"
 shows "P x \<Longrightarrow> is_arg_min m P (arg_min m P)"
 by (metis arg_min_nat_lemma is_arg_min_linorder)
 
 lemma arg_min_nat_le: "P x \<Longrightarrow> m (arg_min m P) \<le> m x"
   for m :: "'a \<Rightarrow> nat"
-by (rule arg_min_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
+  by (rule arg_min_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
 
 lemma ex_min_if_finite:
   "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>m\<in>S. \<not>(\<exists>x\<in>S. x < (m::'a::order))"
-by(induction rule: finite.induct) (auto intro: order.strict_trans)
+  by(induction rule: finite.induct) (auto intro: order.strict_trans)
 
 lemma ex_is_arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order"
-shows "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>x. is_arg_min f (\<lambda>x. x \<in> S) x"
-unfolding is_arg_min_def
-using ex_min_if_finite[of "f ` S"]
-by auto
+  shows "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>x. is_arg_min f (\<lambda>x. x \<in> S) x"
+  unfolding is_arg_min_def
+  using ex_min_if_finite[of "f ` S"]
+  by auto
 
 lemma arg_min_SOME_Min:
   "finite S \<Longrightarrow> arg_min_on f S = (SOME y. y \<in> S \<and> f y = Min(f ` S))"
-unfolding arg_min_on_def arg_min_def is_arg_min_linorder
-apply(rule arg_cong[where f = Eps])
-apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric])
-done
+  unfolding arg_min_on_def arg_min_def is_arg_min_linorder
+  apply(rule arg_cong[where f = Eps])
+  apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric])
+  done
 
 lemma arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order"
-assumes "finite S" "S \<noteq> {}"
-shows  "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>S. f x < f (arg_min_on f S))"
-using ex_is_arg_min_if_finite[OF assms, of f]
-unfolding arg_min_on_def arg_min_def is_arg_min_def
-by(auto dest!: someI_ex)
+  assumes "finite S" "S \<noteq> {}"
+  shows  "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>S. f x < f (arg_min_on f S))"
+  using ex_is_arg_min_if_finite[OF assms, of f]
+  unfolding arg_min_on_def arg_min_def is_arg_min_def
+  by(auto dest!: someI_ex)
 
 lemma arg_min_least: fixes f :: "'a \<Rightarrow> 'b :: linorder"
-shows "\<lbrakk> finite S;  S \<noteq> {};  y \<in> S \<rbrakk> \<Longrightarrow> f(arg_min_on f S) \<le> f y"
-by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f)
+  shows "\<lbrakk> finite S;  S \<noteq> {};  y \<in> S \<rbrakk> \<Longrightarrow> f(arg_min_on f S) \<le> f y"
+  by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f)
 
 lemma arg_min_inj_eq: fixes f :: "'a \<Rightarrow> 'b :: order"
 shows "\<lbrakk> inj_on f {x. P x}; P a; \<forall>y. P y \<longrightarrow> f a \<le> f y \<rbrakk> \<Longrightarrow> arg_min f P = a"
 apply(simp add: arg_min_def is_arg_min_def)
 apply(rule someI2[of _ a])

 lemma arg_maxI:
   "P x \<Longrightarrow>
     (\<And>y. P y \<Longrightarrow> \<not> f y > f x) \<Longrightarrow>
     (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> \<not> f y > f x \<Longrightarrow> Q x) \<Longrightarrow>
     Q (arg_max f P)"
-apply (simp add: arg_max_def is_arg_max_def)
-apply (rule someI2_ex)
- apply blast
-apply blast
-done
+  unfolding arg_max_def is_arg_max_def
+  by (blast intro!: someI2_ex elim: )
 
 lemma arg_max_equality:
   "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f x \<le> f k \<rbrakk> \<Longrightarrow> f (arg_max f P) = f k"
   for f :: "_ \<Rightarrow> 'a::order"
 apply (rule arg_maxI [where f = f])

 
 lemma arg_max_nat_lemma:
   "\<lbrakk> P k;  \<forall>y. P y \<longrightarrow> f y < b \<rbrakk>
   \<Longrightarrow> P (arg_max f P) \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f (arg_max f P))"
   for f :: "'a \<Rightarrow> nat"
-apply (simp add: arg_max_def is_arg_max_linorder)
-apply (rule someI_ex)
-apply (erule (1) ex_has_greatest_nat)
-done
+  unfolding arg_max_def is_arg_max_linorder
+  by (rule someI_ex) (metis ex_has_greatest_nat)
 
 lemmas arg_max_natI = arg_max_nat_lemma [THEN conjunct1]
 
 lemma arg_max_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> f x \<le> f (arg_max f P)"
   for f :: "'a \<Rightarrow> nat"
-by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P])
-
-end
+  using arg_max_nat_lemma by metis
+
+end