--- a/src/HOL/Analysis/Extended_Real_Limits.thy Tue Jul 10 09:52:22 2018 +0100
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy Wed Jul 11 01:04:23 2018 +0200
@@ -358,123 +358,6 @@
apply (metis INF_absorb centre_in_ball)
done
-subsection \<open>Fun.thy\<close>
-
-lemma inj_fn:
- fixes f::"'a \<Rightarrow> 'a"
- assumes "inj f"
- shows "inj (f^^n)"
-proof (induction n)
- case (Suc n)
- have "inj (f o (f^^n))"
- using inj_comp[OF assms Suc.IH] by simp
- then show "inj (f^^(Suc n))"
- by auto
-qed (auto)
-
-lemma surj_fn:
- fixes f::"'a \<Rightarrow> 'a"
- assumes "surj f"
- shows "surj (f^^n)"
-proof (induction n)
- case (Suc n)
- have "surj (f o (f^^n))"
- using assms Suc.IH by (simp add: comp_surj)
- then show "surj (f^^(Suc n))"
- by auto
-qed (auto)
-
-lemma bij_fn:
- fixes f::"'a \<Rightarrow> 'a"
- assumes "bij f"
- shows "bij (f^^n)"
-by (rule bijI[OF inj_fn[OF bij_is_inj[OF assms]] surj_fn[OF bij_is_surj[OF assms]]])
-
-lemma inv_fn_o_fn_is_id:
- fixes f::"'a \<Rightarrow> 'a"
- assumes "bij f"
- shows "((inv f)^^n) o (f^^n) = (\<lambda>x. x)"
-proof -
- have "((inv f)^^n)((f^^n) x) = x" for x n
- proof (induction n)
- case (Suc n)
- have *: "(inv f) (f y) = y" for y
- by (simp add: assms bij_is_inj)
- have "(inv f ^^ Suc n) ((f ^^ Suc n) x) = (inv f^^n) (inv f (f ((f^^n) x)))"
- by (simp add: funpow_swap1)
- also have "... = (inv f^^n) ((f^^n) x)"
- using * by auto
- also have "... = x" using Suc.IH by auto
- finally show ?case by simp
- qed (auto)
- then show ?thesis unfolding o_def by blast
-qed
-
-lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y" (* COPIED FROM Permutations *)
- using surj_f_inv_f[of p] by (auto simp add: bij_def)
-
-lemma fn_o_inv_fn_is_id:
- fixes f::"'a \<Rightarrow> 'a"
- assumes "bij f"
- shows "(f^^n) o ((inv f)^^n) = (\<lambda>x. x)"
-proof -
- have "(f^^n) (((inv f)^^n) x) = x" for x n
- proof (induction n)
- case (Suc n)
- have *: "f(inv f y) = y" for y
- using assms by (meson bij_inv_eq_iff)
- have "(f ^^ Suc n) ((inv f ^^ Suc n) x) = (f^^n) (f (inv f ((inv f^^n) x)))"
- by (simp add: funpow_swap1)
- also have "... = (f^^n) ((inv f^^n) x)"
- using * by auto
- also have "... = x" using Suc.IH by auto
- finally show ?case by simp
- qed (auto)
- then show ?thesis unfolding o_def by blast
-qed
-
-lemma inv_fn:
- fixes f::"'a \<Rightarrow> 'a"
- assumes "bij f"
- shows "inv (f^^n) = ((inv f)^^n)"
-proof -
- have "inv (f^^n) x = ((inv f)^^n) x" for x
- apply (rule inv_into_f_eq, auto simp add: inj_fn[OF bij_is_inj[OF assms]])
- using fn_o_inv_fn_is_id[OF assms, of n] by (metis comp_apply)
- then show ?thesis by auto
-qed
-
-lemma mono_inv:
- fixes f::"'a::linorder \<Rightarrow> 'b::linorder"
- assumes "mono f" "bij f"
- shows "mono (inv f)"
-proof
- fix x y::'b assume "x \<le> y"
- then show "inv f x \<le> inv f y"
- by (metis (no_types, lifting) assms bij_is_surj eq_iff le_cases mono_def surj_f_inv_f)
-qed
-
-lemma mono_bij_Inf:
- fixes f :: "'a::complete_linorder \<Rightarrow> 'b::complete_linorder"
- assumes "mono f" "bij f"
- shows "f (Inf A) = Inf (f`A)"
-proof -
- have "(inv f) (Inf (f`A)) \<le> Inf ((inv f)`(f`A))"
- using mono_Inf[OF mono_inv[OF assms], of "f`A"] by simp
- then have "Inf (f`A) \<le> f (Inf ((inv f)`(f`A)))"
- by (metis (no_types, lifting) assms mono_def bij_inv_eq_iff)
- also have "... = f(Inf A)"
- using assms by (simp add: bij_is_inj)
- finally show ?thesis using mono_Inf[OF assms(1), of A] by auto
-qed
-
-
-lemma Inf_nat_def1:
- fixes K::"nat set"
- assumes "K \<noteq> {}"
- shows "Inf K \<in> K"
-by (auto simp add: Min_def Inf_nat_def) (meson LeastI assms bot.extremum_unique subsetI)
-
subsection \<open>Extended-Real.thy\<close>