--- 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>
--- a/src/HOL/Conditionally_Complete_Lattices.thy Tue Jul 10 09:52:22 2018 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Wed Jul 11 01:04:23 2018 +0200
@@ -526,6 +526,13 @@
end
+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)
+
+
instantiation int :: conditionally_complete_linorder
begin
--- a/src/HOL/Hilbert_Choice.thy Tue Jul 10 09:52:22 2018 +0100
+++ b/src/HOL/Hilbert_Choice.thy Wed Jul 11 01:04:23 2018 +0200
@@ -268,6 +268,92 @@
apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
done
+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 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 bij_inv_eq_iff[OF assms] by auto
+ 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, THEN fun_cong] by (simp)
+ 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"
+ from \<open>bij f\<close> obtain a b where x: "x = f a" and y: "y = f b" by(fastforce simp: bij_def surj_def)
+ show "inv f x \<le> inv f y"
+ proof (rule le_cases)
+ assume "a \<le> b"
+ thus ?thesis using \<open>bij f\<close> x y by(simp add: bij_def inv_f_f)
+ next
+ assume "b \<le> a"
+ hence "f b \<le> f a" by(rule monoD[OF \<open>mono f\<close>])
+ hence "y \<le> x" using x y by simp
+ hence "x = y" using \<open>x \<le> y\<close> by auto
+ thus ?thesis by simp
+ qed
+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 "surj f" using \<open>bij f\<close> by (auto simp: bij_betw_def)
+ 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
+ have "Inf (f`A) \<le> f (Inf ((inv f)`(f`A)))"
+ using monoD[OF \<open>mono f\<close> *] by(simp add: surj_f_inv_f[OF \<open>surj f\<close>])
+ 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 finite_fun_UNIVD1:
assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
--- a/src/HOL/Nat.thy Tue Jul 10 09:52:22 2018 +0100
+++ b/src/HOL/Nat.thy Wed Jul 11 01:04:23 2018 +0200
@@ -1582,6 +1582,28 @@
qed
qed
+lemma inj_fn[simp]:
+ fixes f::"'a \<Rightarrow> 'a"
+ assumes "inj f"
+ shows "inj (f^^n)"
+proof (induction n)
+ case Suc thus ?case using inj_comp[OF assms Suc.IH] by (simp del: comp_apply)
+qed simp
+
+lemma surj_fn[simp]:
+ fixes f::"'a \<Rightarrow> 'a"
+ assumes "surj f"
+ shows "surj (f^^n)"
+proof (induction n)
+ case Suc thus ?case by (simp add: comp_surj[OF Suc.IH assms] del: comp_apply)
+qed simp
+
+lemma bij_fn[simp]:
+ 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]]])
+
subsection \<open>Kleene iteration\<close>