839 apply blast |
839 apply blast |
840 apply blast |
840 apply blast |
841 done |
841 done |
842 |
842 |
843 lemma arg_min_equality: |
843 lemma arg_min_equality: |
844 "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> f k \<le> f x) \<Longrightarrow> f (arg_min f P) = f k" |
844 "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f k \<le> f x \<rbrakk> \<Longrightarrow> f (arg_min f P) = f k" |
845 for f :: "_ \<Rightarrow> 'a::order" |
845 for f :: "_ \<Rightarrow> 'a::order" |
846 apply (rule arg_minI) |
846 apply (rule arg_minI) |
847 apply assumption |
847 apply assumption |
848 apply (simp add: less_le_not_le) |
848 apply (simp add: less_le_not_le) |
849 by (metis le_less) |
849 by (metis le_less) |
|
850 |
|
851 lemma wf_linord_ex_has_least: |
|
852 "\<lbrakk> wf r; \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>*; P k \<rbrakk> |
|
853 \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)" |
|
854 apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]]) |
|
855 apply (drule_tac x = "m ` Collect P" in spec) |
|
856 by force |
|
857 |
|
858 lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)" |
|
859 for m :: "'a \<Rightarrow> nat" |
|
860 apply (simp only: pred_nat_trancl_eq_le [symmetric]) |
|
861 apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) |
|
862 apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le) |
|
863 by assumption |
850 |
864 |
851 lemma arg_min_nat_lemma: |
865 lemma arg_min_nat_lemma: |
852 "P k \<Longrightarrow> P(arg_min m P) \<and> (\<forall>y. P y \<longrightarrow> m (arg_min m P) \<le> m y)" |
866 "P k \<Longrightarrow> P(arg_min m P) \<and> (\<forall>y. P y \<longrightarrow> m (arg_min m P) \<le> m y)" |
853 for m :: "'a \<Rightarrow> nat" |
867 for m :: "'a \<Rightarrow> nat" |
854 apply (simp add: arg_min_def is_arg_min_linorder) |
868 apply (simp add: arg_min_def is_arg_min_linorder) |