# HG changeset patch # User nipkow # Date 1531263863 -7200 # Node ID 4fdc9f6814791bf50fcf1afd0c9ac227ce9054b8 # Parent 9963bb965a0ec0da9c8c47a25cfe66a16e04f627 moved lemmas diff -r 9963bb965a0e -r 4fdc9f681479 src/HOL/Analysis/Extended_Real_Limits.thy --- 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 \Fun.thy\ - -lemma inj_fn: - fixes f::"'a \ '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 \ '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 \ '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 \ 'a" - assumes "bij f" - shows "((inv f)^^n) o (f^^n) = (\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 \ x = inv p y \ 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 \ 'a" - assumes "bij f" - shows "(f^^n) o ((inv f)^^n) = (\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 \ '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 \ 'b::linorder" - assumes "mono f" "bij f" - shows "mono (inv f)" -proof - fix x y::'b assume "x \ y" - then show "inv f x \ 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 \ 'b::complete_linorder" - assumes "mono f" "bij f" - shows "f (Inf A) = Inf (f`A)" -proof - - have "(inv f) (Inf (f`A)) \ Inf ((inv f)`(f`A))" - using mono_Inf[OF mono_inv[OF assms], of "f`A"] by simp - then have "Inf (f`A) \ 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 \ {}" - shows "Inf K \ K" -by (auto simp add: Min_def Inf_nat_def) (meson LeastI assms bot.extremum_unique subsetI) - subsection \Extended-Real.thy\ diff -r 9963bb965a0e -r 4fdc9f681479 src/HOL/Conditionally_Complete_Lattices.thy --- 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 \ {}" + shows "Inf K \ K" +by (auto simp add: Min_def Inf_nat_def) (meson LeastI assms bot.extremum_unique subsetI) + + instantiation int :: conditionally_complete_linorder begin diff -r 9963bb965a0e -r 4fdc9f681479 src/HOL/Hilbert_Choice.thy --- 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 \ 'a" + assumes "bij f" + shows "((inv f)^^n) o (f^^n) = (\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 \ 'a" + assumes "bij f" + shows "(f^^n) o ((inv f)^^n) = (\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 \ '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 \ 'b::linorder" + assumes "mono f" "bij f" + shows "mono (inv f)" +proof + fix x y::'b assume "x \ y" + from \bij f\ obtain a b where x: "x = f a" and y: "y = f b" by(fastforce simp: bij_def surj_def) + show "inv f x \ inv f y" + proof (rule le_cases) + assume "a \ b" + thus ?thesis using \bij f\ x y by(simp add: bij_def inv_f_f) + next + assume "b \ a" + hence "f b \ f a" by(rule monoD[OF \mono f\]) + hence "y \ x" using x y by simp + hence "x = y" using \x \ y\ by auto + thus ?thesis by simp + qed +qed + +lemma mono_bij_Inf: + fixes f :: "'a::complete_linorder \ 'b::complete_linorder" + assumes "mono f" "bij f" + shows "f (Inf A) = Inf (f`A)" +proof - + have "surj f" using \bij f\ by (auto simp: bij_betw_def) + have *: "(inv f) (Inf (f`A)) \ Inf ((inv f)`(f`A))" + using mono_Inf[OF mono_inv[OF assms], of "f`A"] by simp + have "Inf (f`A) \ f (Inf ((inv f)`(f`A)))" + using monoD[OF \mono f\ *] by(simp add: surj_f_inv_f[OF \surj f\]) + 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 \ 'b) set)" and card: "card (UNIV :: 'b set) \ Suc 0" diff -r 9963bb965a0e -r 4fdc9f681479 src/HOL/Nat.thy --- 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 \ '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 \ '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 \ '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 \Kleene iteration\