Quelle Fun.thy Sprache: Isabelle

(*  Title:      HOL/Fun.thy
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
    Author:     Andrei Popescu, TU Muenchen
    Copyright   1994, 2012
*)

section \<open>Notions about functions\<close>

theory Fun
  imports Set
  keywords "functor" :: thy_goal_defn
begin

lemma apply_inverse: "f x = u \ (\x. P x \ g (f x) = x) \ P x \ x = g u"
  by auto

text \<open>Uniqueness, so NOT the axiom of choice.\<close>
lemma uniq_choice: "\x. \!y. Q x y \ \f. \x. Q x (f x)"
  by (force intro: theI')

lemma b_uniq_choice: "\x\S. \!y. Q x y \ \f. \x\S. Q x (f x)"
  by (force intro: theI')

subsection \<open>The Identity Function \<open>id\<close>\<close>

definition id :: "'a \ 'a"
  where "id = (\x. x)"

lemma id_apply [simp]: "id x = x"
  by (simp add: id_def)

lemma image_id [simp]: "image id = id"
  by (simp add: id_def fun_eq_iff)

lemma vimage_id [simp]: "vimage id = id"
  by (simp add: id_def fun_eq_iff)

lemma eq_id_iff: "(\x. f x = x) \ f = id"
  by auto

code_printing
  constant id \<rightharpoonup> (Haskell) "id"

subsection \<open>The Composition Operator \<open>f \<circ> g\<close>\<close>

definition comp :: "('b \ 'c) \ ('a \ 'b) \ 'a \ 'c" (infixl \\\ 55)
  where "f \ g = (\x. f (g x))"

notation (ASCII)
  comp  (infixl \<open>o\<close> 55)

lemma comp_apply [simp]: "(f \ g) x = f (g x)"
  by (simp add: comp_def)

lemma comp_assoc: "(f \ g) \ h = f \ (g \ h)"
  by (simp add: fun_eq_iff)

lemma id_comp [simp]: "id \ g = g"
  by (simp add: fun_eq_iff)

lemma comp_id [simp]: "f \ id = f"
  by (simp add: fun_eq_iff)

lemma comp_eq_dest: "a \ b = c \ d \ a (b v) = c (d v)"
  by (simp add: fun_eq_iff)

lemma comp_eq_elim: "a \ b = c \ d \ ((\v. a (b v) = c (d v)) \ R) \ R"
  by (simp add: fun_eq_iff)

lemma comp_eq_dest_lhs: "a \ b = c \ a (b v) = c v"
  by clarsimp

lemma comp_eq_id_dest: "a \ b = id \ c \ a (b v) = c v"
  by clarsimp

lemma image_comp: "f ` (g ` r) = (f \ g) ` r"
  by auto

lemma vimage_comp: "f -` (g -` x) = (g \ f) -` x"
  by auto

lemma image_eq_imp_comp: "f ` A = g ` B \ (h \ f) ` A = (h \ g) ` B"
  by (auto simp: comp_def elim!: equalityE)

lemma image_bind: "f ` (Set.bind A g) = Set.bind A ((`) f \ g)"
  by (auto simp add: Set.bind_def)

lemma bind_image: "Set.bind (f ` A) g = Set.bind A (g \ f)"
  by (auto simp add: Set.bind_def)

lemma (in group_add) minus_comp_minus [simp]: "uminus \ uminus = id"
  by (simp add: fun_eq_iff)

lemma (in boolean_algebra) minus_comp_minus [simp]: "uminus \ uminus = id"
  by (simp add: fun_eq_iff)

code_printing
  constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."

subsection \<open>The Forward Composition Operator \<open>fcomp\<close>\<close>

definition fcomp :: "('a \ 'b) \ ('b \ 'c) \ 'a \ 'c" (infixl \\>\ 60)
  where "f \> g = (\x. g (f x))"

lemma fcomp_apply [simp]:  "(f \> g) x = g (f x)"
  by (simp add: fcomp_def)

lemma fcomp_assoc: "(f \> g) \> h = f \> (g \> h)"
  by (simp add: fcomp_def)

lemma id_fcomp [simp]: "id \> g = g"
  by (simp add: fcomp_def)

lemma fcomp_id [simp]: "f \> id = f"
  by (simp add: fcomp_def)

lemma fcomp_comp: "fcomp f g = comp g f"
  by (simp add: ext)

code_printing
  constant fcomp \<rightharpoonup> (Eval) infixl 1 "#>"

no_notation fcomp (infixl \<open>\<circ>>\<close> 60)

subsection \<open>Mapping functions\<close>

definition map_fun :: "('c \ 'a) \ ('b \ 'd) \ ('a \ 'b) \ 'c \ 'd"
  where "map_fun f g h = g \ h \ f"

lemma map_fun_apply [simp]: "map_fun f g h x = g (h (f x))"
  by (simp add: map_fun_def)

subsection \<open>Injectivity and Bijectivity\<close>

definition inj_on :: "('a \ 'b) \ 'a set \ bool" \ \injective\
  where "inj_on f A \ (\x\A. \y\A. f x = f y \ x = y)"

definition bij_betw :: "('a \ 'b) \ 'a set \ 'b set \ bool" \ \bijective\
  where "bij_betw f A B \ inj_on f A \ f ` A = B"

text \<open>
  A common special case: functions injective, surjective or bijective over
  the entire domain type.
\<close>

abbreviation inj :: "('a \ 'b) \ bool"
  where "inj f \ inj_on f UNIV"

abbreviation surj :: "('a \ 'b) \ bool"
  where "surj f \ range f = UNIV"

translations \<comment> \<open>The negated case:\<close>
  "\ CONST surj f" \ "CONST range f \ CONST UNIV"

abbreviation bij :: "('a \ 'b) \ bool"
  where "bij f \ bij_betw f UNIV UNIV"

lemma inj_def: "inj f \ (\x y. f x = f y \ x = y)"
  unfolding inj_on_def by blast

lemma injI: "(\x y. f x = f y \ x = y) \ inj f"
  unfolding inj_def by blast

theorem range_ex1_eq: "inj f \ b \ range f \ (\!x. b = f x)"
  unfolding inj_def by blast

lemma injD: "inj f \ f x = f y \ x = y"
  by (simp add: inj_def)

lemma inj_on_eq_iff: "inj_on f A \ x \ A \ y \ A \ f x = f y \ x = y"
  by (auto simp: inj_on_def)

lemma inj_on_cong: "(\a. a \ A \ f a = g a) \ inj_on f A \ inj_on g A"
  by (auto simp: inj_on_def)

lemma image_strict_mono: "inj_on f B \ A \ B \ f ` A \ f ` B"
  unfolding inj_on_def by blast

lemma inj_compose: "inj f \ inj g \ inj (f \ g)"
  by (simp add: inj_def)

lemma inj_fun: "inj f \ inj (\x y. f x)"
  by (simp add: inj_def fun_eq_iff)

lemma inj_eq: "inj f \ f x = f y \ x = y"
  by (simp add: inj_on_eq_iff)

lemma inj_on_iff_Uniq: "inj_on f A \ (\x\A. \\<^sub>\\<^sub>1y. y\A \ f x = f y)"
  by (auto simp: Uniq_def inj_on_def)

lemma inj_on_id[simp]: "inj_on id A"
  by (simp add: inj_on_def)

lemma inj_on_id2[simp]: "inj_on (\x. x) A"
  by (simp add: inj_on_def)

lemma inj_on_Int: "inj_on f A \ inj_on f B \ inj_on f (A \ B)"
  unfolding inj_on_def by blast

lemma surj_id: "surj id"
  by simp

lemma bij_id[simp]: "bij id"
  by (simp add: bij_betw_def)

lemma bij_uminus: "bij (uminus :: 'a \ 'a::group_add)"
  unfolding bij_betw_def inj_on_def
  by (force intro: minus_minus [symmetric])

lemma bij_betwE: "bij_betw f A B \ \a\A. f a \ B"
  unfolding bij_betw_def by auto

lemma inj_onI [intro?]: "(\x y. x \ A \ y \ A \ f x = f y \ x = y) \ inj_on f A"
  by (simp add: inj_on_def)

text \<open>For those frequent proofs by contradiction\<close>
lemma inj_onCI: "(\x y. x \ A \ y \ A \ f x = f y \ x \ y \ False) \ inj_on f A"
  by (force simp: inj_on_def)

lemma inj_on_inverseI: "(\x. x \ A \ g (f x) = x) \ inj_on f A"
  by (auto dest: arg_cong [of concl: g] simp add: inj_on_def)

lemma inj_onD: "inj_on f A \ f x = f y \ x \ A \ y \ A \ x = y"
  unfolding inj_on_def by blast

lemma inj_on_subset:
  "\ inj_on f A; B \ A \ \ inj_on f B"
unfolding inj_on_def by blast

lemma comp_inj_on: "inj_on f A \ inj_on g (f ` A) \ inj_on (g \ f) A"
  by (simp add: comp_def inj_on_def)

lemma inj_on_imageI: "inj_on (g \ f) A \ inj_on g (f ` A)"
  by (auto simp add: inj_on_def)

lemma inj_on_image_iff:
  "\x\A. \y\A. g (f x) = g (f y) \ g x = g y \ inj_on f A \ inj_on g (f ` A) \ inj_on g A"
  unfolding inj_on_def by blast

lemma inj_on_contraD: "inj_on f A \ x \ y \ x \ A \ y \ A \ f x \ f y"
  unfolding inj_on_def by blast

lemma inj_singleton [simp]: "inj_on (\x. {x}) A"
  by (simp add: inj_on_def)

lemma inj_on_empty[iff]: "inj_on f {}"
  by (simp add: inj_on_def)

lemma inj_on_Un: "inj_on f (A \ B) \ inj_on f A \ inj_on f B \ f ` (A - B) \ f ` (B - A) = {}"
  unfolding inj_on_def by (blast intro: sym)

lemma inj_on_insert [iff]: "inj_on f (insert a A) \ inj_on f A \ f a \ f ` (A - {a})"
  unfolding inj_on_def by (blast intro: sym)

lemma inj_on_diff: "inj_on f A \ inj_on f (A - B)"
  unfolding inj_on_def by blast

lemma comp_inj_on_iff: "inj_on f A \ inj_on f' (f ` A) \ inj_on (f' \ f) A"
  by (auto simp: comp_inj_on inj_on_def)

lemma inj_on_imageI2: "inj_on (f' \ f) A \ inj_on f A"
  by (auto simp: comp_inj_on inj_on_def)

lemma inj_img_insertE:
  assumes "inj_on f A"
  assumes "x \ B"
    and "insert x B = f ` A"
  obtains x' A' where "x' \ A'" and "A = insert x' A'" and "x = f x'" and "B = f ` A'"
proof -
  from assms have "x \ f ` A" by auto
  then obtain x' where *: "x' \<in> A" "x = f x'" by auto
  then have A: "A = insert x' (A - {x'})" by auto
  with assms * have B: "B = f ` (A - {x'})" by (auto dest: inj_on_contraD)
  have "x' \ A - {x'}" by simp
  from this A \<open>x = f x'\<close> B show ?thesis ..
qed

lemma linorder_inj_onI:
  fixes A :: "'a::order set"
  assumes ne: "\x y. \x < y; x\A; y\A\ \ f x \ f y" and lin: "\x y. \x\A; y\A\ \ x\y \ y\x"
  shows "inj_on f A"
proof (rule inj_onI)
  fix x y
  assume eq: "f x = f y" and "x\A" "y\A"
  then show "x = y"
    using lin [of x y] ne by (force simp: dual_order.order_iff_strict)
qed

lemma linorder_inj_onI':
  fixes A :: "'a :: linorder set"
  assumes "\i j. i \ A \ j \ A \ i < j \ f i \ f j"
  shows   "inj_on f A"
  by (intro linorder_inj_onI) (auto simp add: assms)

lemma linorder_injI:
  assumes "\x y::'a::linorder. x < y \ f x \ f y"
  shows "inj f"
    \<comment> \<open>Courtesy of Stephan Merz\<close>
using assms by (simp add: linorder_inj_onI')

lemma inj_on_image_Pow: "inj_on f A \inj_on (image f) (Pow A)"
  unfolding Pow_def inj_on_def by blast

lemma inj_on_vimage_image: "inj_on (\b. f -` {b}) (f ` A)"
using inj_on_def by fastforce

lemma bij_betw_image_Pow: "bij_betw f A B \ bij_betw (image f) (Pow A) (Pow B)"
  by (auto simp add: bij_betw_def inj_on_image_Pow image_Pow_surj)

lemma surj_def: "surj f \ (\y. \x. y = f x)"
  by auto

lemma surjI:
  assumes "\x. g (f x) = x"
  shows "surj g"
  using assms [symmetric] by auto

lemma surjD: "surj f \ \x. y = f x"
  by (simp add: surj_def)

lemma surjE: "surj f \ (\x. y = f x \ C) \ C"
  by (simp add: surj_def) blast

lemma comp_surj: "surj f \ surj g \ surj (g \ f)"
  using image_comp [of g f UNIV] by simp

lemma bij_betw_imageI: "inj_on f A \ f ` A = B \ bij_betw f A B"
  unfolding bij_betw_def by clarify

lemma bij_betw_imp_surj_on: "bij_betw f A B \ f ` A = B"
  unfolding bij_betw_def by clarify

lemma bij_betw_imp_surj: "bij_betw f A UNIV \ surj f"
  unfolding bij_betw_def by auto

lemma bij_betw_empty1: "bij_betw f {} A \ A = {}"
  unfolding bij_betw_def by blast

lemma bij_betw_empty2: "bij_betw f A {} \ A = {}"
  unfolding bij_betw_def by blast

lemma inj_on_imp_bij_betw: "inj_on f A \ bij_betw f A (f ` A)"
  unfolding bij_betw_def by simp

lemma bij_betw_DiffI:
  assumes "bij_betw f A B" "bij_betw f C D" "C \ A" "D \ B"
  shows   "bij_betw f (A - C) (B - D)"
  using assms unfolding bij_betw_def inj_on_def by auto

lemma bij_betw_singleton_iff [simp]: "bij_betw f {x} {y} \ f x = y"
  by (auto simp: bij_betw_def)

lemma bij_betw_singletonI [intro]: "f x = y \ bij_betw f {x} {y}"
  by auto

lemma bij_betw_imp_empty_iff: "bij_betw f A B \ A = {} \ B = {}"
  unfolding bij_betw_def by blast

lemma bij_betw_imp_Ex_iff: "bij_betw f {x. P x} {x. Q x} \ (\x. P x) \ (\x. Q x)"
  unfolding bij_betw_def by blast

lemma bij_betw_imp_Bex_iff: "bij_betw f {x\A. P x} {x\B. Q x} \ (\x\A. P x) \ (\x\B. Q x)"
  unfolding bij_betw_def by blast

lemma bij_betw_apply: "\bij_betw f A B; a \ A\ \ f a \ B"
  unfolding bij_betw_def by auto

lemma bij_def: "bij f \ inj f \ surj f"
  by (rule bij_betw_def)

lemma bijI: "inj f \ surj f \ bij f"
  by (rule bij_betw_imageI)

lemma bij_is_inj: "bij f \ inj f"
  by (simp add: bij_def)

lemma bij_is_surj: "bij f \ surj f"
  by (simp add: bij_def)

lemma bij_betw_imp_inj_on: "bij_betw f A B \ inj_on f A"
  by (simp add: bij_betw_def)

lemma bij_betw_trans: "bij_betw f A B \ bij_betw g B C \ bij_betw (g \ f) A C"
  by (auto simp add:bij_betw_def comp_inj_on)

lemma bij_comp: "bij f \ bij g \ bij (g \ f)"
  by (rule bij_betw_trans)

lemma bij_betw_comp_iff: "bij_betw f A A' \ bij_betw f' A' A'' \ bij_betw (f' \ f) A A''"
  by (auto simp add: bij_betw_def inj_on_def)

lemma bij_betw_Collect:
  assumes "bij_betw f A B" "\x. x \ A \ Q (f x) \ P x"
  shows   "bij_betw f {x\A. P x} {y\B. Q y}"
  using assms by (auto simp add: bij_betw_def inj_on_def)

lemma bij_betw_comp_iff2:
  assumes bij: "bij_betw f' A' A''"
    and img: "f ` A \ A'"
  shows "bij_betw f A A' \ bij_betw (f' \ f) A A''" (is "?L \ ?R")
proof
  assume "?L"
  then show "?R"
    using assms by (auto simp add: bij_betw_comp_iff)
  next
    assume *: "?R"
    have "inj_on (f' \ f) A \ inj_on f A"
      using inj_on_imageI2 by blast
    moreover have "A' \ f ` A"
    proof
      fix a'
      assume **: "a' \ A'"
      with bij have "f' a' \ A''"
        unfolding bij_betw_def by auto
      with * obtain a where 1: "a \ A \ f' (f a) = f' a'"
        unfolding bij_betw_def by force
      with img have "f a \ A'" by auto
      with bij ** 1 have "f a = a'"
        unfolding bij_betw_def inj_on_def by auto
      with 1 show "a' \ f ` A" by auto
    qed
    ultimately show "?L"
      using img * by (auto simp add: bij_betw_def)
qed

lemma bij_betw_inv:
  assumes "bij_betw f A B"
  shows "\g. bij_betw g B A"
proof -
  have i: "inj_on f A" and s: "f ` A = B"
    using assms by (auto simp: bij_betw_def)
  let ?P = "\b a. a \ A \ f a = b"
  let ?g = "\b. The (?P b)"
  have g: "?g b = a" if P: "?P b a" for a b
  proof -
    from that s have ex1: "\a. ?P b a" by blast
    then have uex1: "\!a. ?P b a" by (blast dest:inj_onD[OF i])
    then show ?thesis
      using the1_equality[OF uex1, OF P] P by simp
  qed
  have "inj_on ?g B"
  proof (rule inj_onI)
    fix x y
    assume "x \ B" "y \ B" "?g x = ?g y"
    from s \<open>x \<in> B\<close> obtain a1 where a1: "?P x a1" by blast
    from s \<open>y \<in> B\<close> obtain a2 where a2: "?P y a2" by blast
    from g [OF a1] a1 g [OF a2] a2 \<open>?g x = ?g y\<close> show "x = y" by simp
  qed
  moreover have "?g ` B = A"
  proof safe
    fix b
    assume "b \ B"
    with s obtain a where P: "?P b a" by blast
    with g[OF P] show "?g b \ A" by auto
  next
    fix a
    assume "a \ A"
    with s obtain b where P: "?P b a" by blast
    with s have "b \ B" by blast
    with g[OF P] have "\b\B. a = ?g b" by blast
    then show "a \ ?g ` B"
      by auto
  qed
  ultimately show ?thesis
    by (auto simp: bij_betw_def)
qed

lemma bij_betw_cong: "(\a. a \ A \ f a = g a) \ bij_betw f A A' = bij_betw g A A'"
  unfolding bij_betw_def inj_on_def by safe force+  (* somewhat slow *)

lemma bij_betw_id[intro, simp]: "bij_betw id A A"
  unfolding bij_betw_def id_def by auto

lemma bij_betw_id_iff: "bij_betw id A B \ A = B"
  by (auto simp add: bij_betw_def)

lemma bij_betw_combine:
  "bij_betw f A B \ bij_betw f C D \ B \ D = {} \ bij_betw f (A \ C) (B \ D)"
  unfolding bij_betw_def inj_on_Un image_Un by auto

lemma bij_betw_subset: "bij_betw f A A' \ B \ A \ f ` B = B' \ bij_betw f B B'"
  by (auto simp add: bij_betw_def inj_on_def)

lemma bij_betw_ball: "bij_betw f A B \ (\b \ B. phi b) = (\a \ A. phi (f a))"
  unfolding bij_betw_def inj_on_def by blast

lemma bij_pointE:
  assumes "bij f"
  obtains x where "y = f x" and "\x'. y = f x' \ x' = x"
proof -
  from assms have "inj f" by (rule bij_is_inj)
  moreover from assms have "surj f" by (rule bij_is_surj)
  then have "y \ range f" by simp
  ultimately have "\!x. y = f x" by (simp add: range_ex1_eq)
  with that show thesis by blast
qed

lemma bij_iff: \<^marker>\<open>contributor \<open>Amine Chaieb\<close>\<close>
  \<open>bij f \<longleftrightarrow> (\<forall>x. \<exists>!y. f y = x)\<close>  (is \<open>?P \<longleftrightarrow> ?Q\<close>)
proof
  assume ?P
  then have \<open>inj f\<close> \<open>surj f\<close>
    by (simp_all add: bij_def)
  show ?Q
  proof
    fix y
    from \<open>surj f\<close> obtain x where \<open>y = f x\<close>
      by (auto simp add: surj_def)
    with \<open>inj f\<close> show \<open>\<exists>!x. f x = y\<close>
      by (auto simp add: inj_def)
  qed
next
  assume ?Q
  then have \<open>inj f\<close>
    by (auto simp add: inj_def)
  moreover have \<open>\<exists>x. y = f x\<close> for y
  proof -
    from \<open>?Q\<close> obtain x where \<open>f x = y\<close>
      by blast
    then have \<open>y = f x\<close>
      by simp
    then show ?thesis ..
  qed
  then have \<open>surj f\<close>
    by (auto simp add: surj_def)
  ultimately show ?P
    by (rule bijI)
qed

lemma bij_betw_partition:
  \<open>bij_betw f A B\<close>
  if \<open>bij_betw f (A \<union> C) (B \<union> D)\<close> \<open>bij_betw f C D\<close> \<open>A \<inter> C = {}\<close> \<open>B \<inter> D = {}\<close>
proof -
  from that have \<open>inj_on f (A \<union> C)\<close> \<open>inj_on f C\<close> \<open>f ` (A \<union> C) = B \<union> D\<close> \<open>f ` C = D\<close>
    by (simp_all add: bij_betw_def)
  then have \<open>inj_on f A\<close> and \<open>f ` (A - C) \<inter> f ` (C - A) = {}\<close>
    by (simp_all add: inj_on_Un)
  with \<open>A \<inter> C = {}\<close> have \<open>f ` A \<inter> f ` C = {}\<close>
    by auto
  with \<open>f ` (A \<union> C) = B \<union> D\<close> \<open>f ` C = D\<close>  \<open>B \<inter> D = {}\<close>
  have \<open>f ` A = B\<close>
    by blast
  with \<open>inj_on f A\<close> show ?thesis
    by (simp add: bij_betw_def)
qed

lemma surj_image_vimage_eq: "surj f \ f ` (f -` A) = A"
  by simp

lemma surj_vimage_empty:
  assumes "surj f"
  shows "f -` A = {} \ A = {}"
  using surj_image_vimage_eq [OF \<open>surj f\<close>, of A]
  by (intro iffI) fastforce+

lemma inj_vimage_image_eq: "inj f \ f -` (f ` A) = A"
  unfolding inj_def by blast

lemma vimage_subsetD: "surj f \ f -` B \ A \ B \ f ` A"
  by (blast intro: sym)

lemma vimage_subsetI: "inj f \ B \ f ` A \ f -` B \ A"
  unfolding inj_def by blast

lemma vimage_subset_eq: "bij f \ f -` B \ A \ B \ f ` A"
  unfolding bij_def by (blast del: subsetI intro: vimage_subsetI vimage_subsetD)

lemma inj_on_image_eq_iff: "inj_on f C \ A \ C \ B \ C \ f ` A = f ` B \ A = B"
  by (fastforce simp: inj_on_def)

lemma inj_on_Un_image_eq_iff: "inj_on f (A \ B) \ f ` A = f ` B \ A = B"
  by (erule inj_on_image_eq_iff) simp_all

lemma inj_on_image_Int: "inj_on f C \ A \ C \ B \ C \ f ` (A \ B) = f ` A \ f ` B"
  unfolding inj_on_def by blast

lemma inj_on_image_set_diff: "inj_on f C \ A - B \ C \ B \ C \ f ` (A - B) = f ` A - f ` B"
  unfolding inj_on_def by blast

lemma image_Int: "inj f \ f ` (A \ B) = f ` A \ f ` B"
  unfolding inj_def by blast

lemma image_set_diff: "inj f \ f ` (A - B) = f ` A - f ` B"
  unfolding inj_def by blast

lemma inj_on_image_mem_iff: "inj_on f B \ a \ B \ A \ B \ f a \ f ` A \ a \ A"
  by (auto simp: inj_on_def)

lemma inj_image_mem_iff: "inj f \ f a \ f ` A \ a \ A"
  by (blast dest: injD)

lemma inj_image_subset_iff: "inj f \ f ` A \ f ` B \ A \ B"
  by (blast dest: injD)

lemma inj_image_eq_iff: "inj f \ f ` A = f ` B \ A = B"
  by (blast dest: injD)

lemma surj_Compl_image_subset: "surj f \ - (f ` A) \ f ` (- A)"
  by auto

lemma inj_image_Compl_subset: "inj f \ f ` (- A) \ - (f ` A)"
  by (auto simp: inj_def)

lemma bij_image_Compl_eq: "bij f \ f ` (- A) = - (f ` A)"
  by (simp add: bij_def inj_image_Compl_subset surj_Compl_image_subset equalityI)

lemma inj_vimage_singleton: "inj f \ f -` {a} \ {THE x. f x = a}"
  \<comment> \<open>The inverse image of a singleton under an injective function is included in a singleton.\<close>
  by (simp add: inj_def) (blast intro: the_equality [symmetric])

lemma inj_on_vimage_singleton: "inj_on f A \ f -` {a} \ A \ {THE x. x \ A \ f x = a}"
  by (auto simp add: inj_on_def intro: the_equality [symmetric])

lemma bij_betw_byWitness:
  assumes left: "\a \ A. f' (f a) = a"
    and right: "\a' \ A'. f (f' a') = a'"
    and "f ` A \ A'"
    and img2: "f' ` A' \ A"
  shows "bij_betw f A A'"
  using assms
  unfolding bij_betw_def inj_on_def
proof safe
  fix a b
  assume "a \ A" "b \ A"
  with left have "a = f' (f a) \ b = f' (f b)" by simp
  moreover assume "f a = f b"
  ultimately show "a = b" by simp
next
  fix a' assume *: "a' \<in> A'"
  with img2 have "f' a' \ A" by blast
  moreover from * right have "a' = f (f' a')" by simp
  ultimately show "a' \ f ` A" by blast
qed

corollary notIn_Un_bij_betw:
  assumes "b \ A"
    and "f b \ A'"
    and "bij_betw f A A'"
  shows "bij_betw f (A \ {b}) (A' \ {f b})"
proof -
  have "bij_betw f {b} {f b}"
    unfolding bij_betw_def inj_on_def by simp
  with assms show ?thesis
    using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast
qed

lemma notIn_Un_bij_betw3:
  assumes "b \ A"
    and "f b \ A'"
  shows "bij_betw f A A' = bij_betw f (A \ {b}) (A' \ {f b})"
proof
  assume "bij_betw f A A'"
  then show "bij_betw f (A \ {b}) (A' \ {f b})"
    using assms notIn_Un_bij_betw [of b A f A'] by blast
next
  assume *: "bij_betw f (A \ {b}) (A' \ {f b})"
  have "f ` A = A'"
  proof safe
    fix a
    assume **: "a \ A"
    then have "f a \ A' \ {f b}"
      using * unfolding bij_betw_def by blast
    moreover
    have False if "f a = f b"
    proof -
      have "a = b"
        using * ** that unfolding bij_betw_def inj_on_def by blast
      with \<open>b \<notin> A\<close> ** show ?thesis by blast
    qed
    ultimately show "f a \ A'" by blast
  next
    fix a'
    assume **: "a' \ A'"
    then have "a' \ f ` (A \ {b})"
      using * by (auto simp add: bij_betw_def)
    then obtain a where 1: "a \ A \ {b} \ f a = a'" by blast
    moreover
    have False if "a = b" using 1 ** \<open>f b \<notin> A'\<close> that by blast
    ultimately have "a \ A" by blast
    with 1 show "a' \ f ` A" by blast
  qed
  then show "bij_betw f A A'"
    using * bij_betw_subset[of f "A \ {b}" _ A] by blast
qed

lemma inj_on_disjoint_Un:
  assumes "inj_on f A" and "inj_on g B"
  and "f ` A \ g ` B = {}"
  shows "inj_on (\x. if x \ A then f x else g x) (A \ B)"
  using assms by (simp add: inj_on_def disjoint_iff) (blast)

lemma bij_betw_disjoint_Un:
  assumes "bij_betw f A C" and "bij_betw g B D"
  and "A \ B = {}"
  and "C \ D = {}"
  shows "bij_betw (\x. if x \ A then f x else g x) (A \ B) (C \ D)"
  using assms by (auto simp: inj_on_disjoint_Un bij_betw_def)

lemma involuntory_imp_bij:
  \<open>bij f\<close> if \<open>\<And>x. f (f x) = x\<close>
proof (rule bijI)
  from that show \<open>surj f\<close>
    by (rule surjI)
  show \<open>inj f\<close>
  proof (rule injI)
    fix x y
    assume \<open>f x = f y\<close>
    then have \<open>f (f x) = f (f y)\<close>
      by simp
    then show \<open>x = y\<close>
      by (simp add: that)
  qed
qed

subsubsection \<open>Inj/surj/bij of Algebraic Operations\<close>

context cancel_semigroup_add
begin

lemma inj_on_add [simp]:
  "inj_on ((+) a) A"
  by (rule inj_onI) simp

lemma inj_on_add' [simp]:
  "inj_on (\b. b + a) A"
  by (rule inj_onI) simp

lemma bij_betw_add [simp]:
  "bij_betw ((+) a) A B \ (+) a ` A = B"
  by (simp add: bij_betw_def)

end

context group_add
begin

lemma diff_left_imp_eq: "a - b = a - c \ b = c"
unfolding add_uminus_conv_diff[symmetric]
by(drule local.add_left_imp_eq) simp

lemma inj_uminus[simp, intro]: "inj_on uminus A"
  by (auto intro!: inj_onI)

lemma surj_uminus[simp]: "surj uminus"
using surjI minus_minus by blast

lemma surj_plus [simp]:
  "surj ((+) a)"
proof (standard, simp, standard, simp)
  fix x
  have "x = a + (-a + x)" by (simp add: add.assoc)
  thus "x \ range ((+) a)" by blast
qed

lemma surj_plus_right [simp]:
  "surj (\b. b+a)"
proof (standard, simp, standard, simp)
  fix b show "b \ range (\b. b+a)"
    using diff_add_cancel[of b a, symmetric] by blast
qed

lemma inj_on_diff_left [simp]:
  \<open>inj_on ((-) a) A\<close>
by (auto intro: inj_onI dest!: diff_left_imp_eq)

lemma inj_on_diff_right [simp]:
  \<open>inj_on (\<lambda>b. b - a) A\<close>
by (auto intro: inj_onI simp add: algebra_simps)

lemma surj_diff [simp]:
  "surj ((-) a)"
proof (standard, simp, standard, simp)
  fix x
  have "x = a - (- x + a)" by (simp add: algebra_simps)
  thus "x \ range ((-) a)" by blast
qed

lemma surj_diff_right [simp]:
  "surj (\x. x - a)"
proof (standard, simp, standard, simp)
  fix x
  have "x = x + a - a" by simp
  thus "x \ range (\x. x - a)" by fast
qed

lemma shows bij_plus: "bij ((+) a)" and bij_plus_right: "bij (\x. x + a)"
  and bij_uminus: "bij uminus"
  and bij_diff: "bij ((-) a)" and bij_diff_right: "bij (\x. x - a)"
by(simp_all add: bij_def)

lemma translation_subtract_Compl:
  "(\x. x - a) ` (- t) = - ((\x. x - a) ` t)"
by(rule bij_image_Compl_eq)
  (auto simp add: bij_def surj_def inj_def diff_eq_eq intro!: add_diff_cancel[symmetric])

lemma translation_diff:
  "(+) a ` (s - t) = ((+) a ` s) - ((+) a ` t)"
  by auto

lemma translation_subtract_diff:
  "(\x. x - a) ` (s - t) = ((\x. x - a) ` s) - ((\x. x - a) ` t)"
by(rule image_set_diff)(simp add: inj_on_def diff_eq_eq)

lemma translation_Int:
  "(+) a ` (s \ t) = ((+) a ` s) \ ((+) a ` t)"
  by auto

lemma translation_subtract_Int:
  "(\x. x - a) ` (s \ t) = ((\x. x - a) ` s) \ ((\x. x - a) ` t)"
by(rule image_Int)(simp add: inj_on_def diff_eq_eq)

lemma translation_Compl:
  "(+) a ` (- t) = - ((+) a ` t)"
proof (rule set_eqI)
  fix b
  show "b \ (+) a ` (- t) \ b \ - (+) a ` t"
    by (auto simp: image_iff algebra_simps intro!: bexI [of _ "- a + b"])
qed

end

subsection \<open>Function Updating\<close>

definition fun_upd :: "('a \ 'b) \ 'a \ 'b \ ('a \ 'b)"
  where "fun_upd f a b = (\x. if x = a then b else f x)"

nonterminal updbinds and updbind

open_bundle update_syntax
begin

syntax
  "_updbind" :: "'a \ 'a \ updbind" (\(\indent=2 notation=\mixfix update\\_ :=/ _)\)
  ""         :: "updbind \ updbinds" (\_\)
  "_updbinds":: "updbind \ updbinds \ updbinds" (\_,/ _\)
  "_Update"  :: "'a \ updbinds \ 'a"
    (\<open>(\<open>open_block notation=\<open>mixfix function update\<close>\<close>_/'((2_)'))\<close> [1000, 0] 900)
syntax_consts
  "_Update" \<rightleftharpoons> fun_upd
translations
  "_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
  "f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"

end

(* Hint: to define the sum of two functions (or maps), use case_sum.
         A nice infix syntax could be defined by
notation
  case_sum  (infixr "'(+')"80)
*)

lemma fun_upd_idem_iff: "f(x:=y) = f \ f x = y"
  unfolding fun_upd_def
  apply safe
   apply (erule subst)
   apply auto
  done

lemma fun_upd_idem: "f x = y \ f(x := y) = f"
  by (simp only: fun_upd_idem_iff)

lemma fun_upd_triv [iff]: "f(x := f x) = f"
  by (simp only: fun_upd_idem)

lemma fun_upd_apply [simp]: "(f(x := y)) z = (if z = x then y else f z)"
  by (simp add: fun_upd_def)

(* fun_upd_apply supersedes these two, but they are useful
   if fun_upd_apply is intentionally removed from the simpset *)
lemma fun_upd_same: "(f(x := y)) x = y"
  by simp

lemma fun_upd_other: "z \ x \ (f(x := y)) z = f z"
  by simp

lemma fun_upd_upd [simp]: "f(x := y, x := z) = f(x := z)"
  by (simp add: fun_eq_iff)

lemma fun_upd_twist: "a \ c \ (m(a := b))(c := d) = (m(c := d))(a := b)"
  by auto

lemma inj_on_fun_updI: "inj_on f A \ y \ f ` A \ inj_on (f(x := y)) A"
  by (auto simp: inj_on_def)

lemma fun_upd_image: "f(x := y) ` A = (if x \ A then insert y (f ` (A - {x})) else f ` A)"
  by auto

lemma fun_upd_comp: "f \ (g(x := y)) = (f \ g)(x := f y)"
  by auto

lemma fun_upd_eqD: "f(x := y) = g(x := z) \ y = z"
  by (simp add: fun_eq_iff split: if_split_asm)

subsection \<open>\<open>override_on\<close>\<close>

definition override_on :: "('a \ 'b) \ ('a \ 'b) \ 'a set \ 'a \ 'b"
  where "override_on f g A = (\a. if a \ A then g a else f a)"

lemma override_on_emptyset[simp]: "override_on f g {} = f"
  by (simp add: override_on_def)

lemma override_on_apply_notin[simp]: "a \ A \ (override_on f g A) a = f a"
  by (simp add: override_on_def)

lemma override_on_apply_in[simp]: "a \ A \ (override_on f g A) a = g a"
  by (simp add: override_on_def)

lemma override_on_insert: "override_on f g (insert x X) = (override_on f g X)(x:=g x)"
  by (simp add: override_on_def fun_eq_iff)

lemma override_on_insert': "override_on f g (insert x X) = (override_on (f(x:=g x)) g X)"
  by (simp add: override_on_def fun_eq_iff)

subsection \<open>Inversion of injective functions\<close>

definition the_inv_into :: "'a set \ ('a \ 'b) \ ('b \ 'a)"
  where "the_inv_into A f = (\x. THE y. y \ A \ f y = x)"

lemma the_inv_into_f_f: "inj_on f A \ x \ A \ the_inv_into A f (f x) = x"
  unfolding the_inv_into_def inj_on_def by blast

lemma f_the_inv_into_f: "inj_on f A \ y \ f ` A \ f (the_inv_into A f y) = y"
  unfolding the_inv_into_def
  by (rule the1I2; blast dest: inj_onD)

lemma f_the_inv_into_f_bij_betw:
  "bij_betw f A B \ (bij_betw f A B \ x \ B) \ f (the_inv_into A f x) = x"
  unfolding bij_betw_def by (blast intro: f_the_inv_into_f)

lemma the_inv_into_into: "inj_on f A \ x \ f ` A \ A \ B \ the_inv_into A f x \ B"
  unfolding the_inv_into_def
  by (rule the1I2; blast dest: inj_onD)

lemma the_inv_into_onto [simp]: "inj_on f A \ the_inv_into A f ` (f ` A) = A"
  by (fast intro: the_inv_into_into the_inv_into_f_f [symmetric])

lemma the_inv_into_f_eq: "inj_on f A \ f x = y \ x \ A \ the_inv_into A f y = x"
  by (force simp add: the_inv_into_f_f)

lemma the_inv_into_comp:
  "inj_on f (g ` A) \ inj_on g A \ x \ f ` g ` A \
    the_inv_into A (f \<circ> g) x = (the_inv_into A g \<circ> the_inv_into (g ` A) f) x"
  apply (rule the_inv_into_f_eq)
    apply (fast intro: comp_inj_on)
   apply (simp add: f_the_inv_into_f the_inv_into_into)
  apply (simp add: the_inv_into_into)
  done

lemma inj_on_the_inv_into: "inj_on f A \ inj_on (the_inv_into A f) (f ` A)"
  by (auto intro: inj_onI simp: the_inv_into_f_f)

lemma bij_betw_the_inv_into: "bij_betw f A B \ bij_betw (the_inv_into A f) B A"
  by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into)

lemma bij_betw_iff_bijections:
  "bij_betw f A B \ (\g. (\x \ A. f x \ B \ g(f x) = x) \ (\y \ B. g y \ A \ f(g y) = y))"
  (is "?lhs = ?rhs")
proof
  show "?lhs \ ?rhs"
    by (auto simp: bij_betw_def f_the_inv_into_f the_inv_into_f_f the_inv_into_into
        exI[where ?x="the_inv_into A f"])
next
  show "?rhs \ ?lhs"
    by (force intro: bij_betw_byWitness)
qed

abbreviation the_inv :: "('a \ 'b) \ ('b \ 'a)"
  where "the_inv f \ the_inv_into UNIV f"

lemma the_inv_f_f: "the_inv f (f x) = x" if "inj f"
  using that UNIV_I by (rule the_inv_into_f_f)

subsection \<open>Monotonicity\<close>

definition monotone_on :: "'a set \ ('a \ 'a \ bool) \ ('b \ 'b \ bool) \ ('a \ 'b) \ bool"
  where "monotone_on A orda ordb f \ (\x\A. \y\A. orda x y \ ordb (f x) (f y))"

abbreviation monotone :: "('a \ 'a \ bool) \ ('b \ 'b \ bool) \ ('a \ 'b) \ bool"
  where "monotone \ monotone_on UNIV"

lemma monotone_def[no_atp]: "monotone orda ordb f \ (\x y. orda x y \ ordb (f x) (f y))"
  by (simp add: monotone_on_def)

text \<open>Lemma @{thm [source] monotone_def} is provided for backward compatibility.\<close>

lemma monotone_onI:
  "(\x y. x \ A \ y \ A \ orda x y \ ordb (f x) (f y)) \ monotone_on A orda ordb f"
  by (simp add: monotone_on_def)

lemma monotoneI[intro?]: "(\x y. orda x y \ ordb (f x) (f y)) \ monotone orda ordb f"
  by (rule monotone_onI)

lemma monotone_onD:
  "monotone_on A orda ordb f \ x \ A \ y \ A \ orda x y \ ordb (f x) (f y)"
  by (simp add: monotone_on_def)

lemma monotoneD[dest?]: "monotone orda ordb f \ orda x y \ ordb (f x) (f y)"
  by (rule monotone_onD[of UNIV, simplified])

lemma monotone_on_subset: "monotone_on A orda ordb f \ B \ A \ monotone_on B orda ordb f"
  by (auto intro: monotone_onI dest: monotone_onD)

lemma monotone_on_empty[simp]: "monotone_on {} orda ordb f"
  by (auto intro: monotone_onI dest: monotone_onD)

lemma monotone_on_o:
  assumes
    mono_f: "monotone_on A orda ordb f" and
    mono_g: "monotone_on B ordc orda g" and
    "g ` B \ A"
  shows "monotone_on B ordc ordb (f \ g)"
proof (rule monotone_onI)
  fix x y assume "x \ B" and "y \ B" and "ordc x y"
  hence "orda (g x) (g y)"
    by (rule mono_g[THEN monotone_onD])
  moreover from \<open>g ` B \<subseteq> A\<close> \<open>x \<in> B\<close> \<open>y \<in> B\<close> have "g x \<in> A" and "g y \<in> A"
    unfolding image_subset_iff by simp_all
  ultimately show "ordb ((f \ g) x) ((f \ g) y)"
    using mono_f[THEN monotone_onD] by simp
qed

subsubsection \<open>Specializations For @{class ord} Type Class And More\<close>

context ord begin

abbreviation mono_on :: "'a set \ ('a \ 'b :: ord) \ bool"
  where "mono_on A \ monotone_on A (\) (\)"

abbreviation strict_mono_on :: "'a set \ ('a \ 'b :: ord) \ bool"
  where "strict_mono_on A \ monotone_on A (<) (<)"

abbreviation antimono_on :: "'a set \ ('a \ 'b :: ord) \ bool"
  where "antimono_on A \ monotone_on A (\) (\x y. y \ x)"

abbreviation strict_antimono_on :: "'a set \ ('a \ 'b :: ord) \ bool"
  where "strict_antimono_on A \ monotone_on A (<) (\x y. y < x)"

lemma mono_on_def[no_atp]: "mono_on A f \ (\r s. r \ A \ s \ A \ r \ s \ f r \ f s)"
  by (auto simp add: monotone_on_def)

lemma strict_mono_on_def[no_atp]:
  "strict_mono_on A f \ (\r s. r \ A \ s \ A \ r < s \ f r < f s)"
  by (auto simp add: monotone_on_def)

text \<open>Lemmas @{thm [source] mono_on_def} and @{thm [source] strict_mono_on_def} are provided for
backward compatibility.\<close>

lemma mono_onI:
  "(\r s. r \ A \ s \ A \ r \ s \ f r \ f s) \ mono_on A f"
  by (rule monotone_onI)

lemma strict_mono_onI:
  "(\r s. r \ A \ s \ A \ r < s \ f r < f s) \ strict_mono_on A f"
  by (rule monotone_onI)

lemma mono_onD: "\mono_on A f; r \ A; s \ A; r \ s\ \ f r \ f s"
  by (rule monotone_onD)

lemma strict_mono_onD: "\strict_mono_on A f; r \ A; s \ A; r < s\ \ f r < f s"
  by (rule monotone_onD)

lemma mono_on_subset: "mono_on A f \ B \ A \ mono_on B f"
  by (rule monotone_on_subset)

end

context order begin

abbreviation mono :: "('a \ 'b::order) \ bool"
  where "mono \ mono_on UNIV"

abbreviation strict_mono :: "('a \ 'b::order) \ bool"
  where "strict_mono \ strict_mono_on UNIV"

abbreviation antimono :: "('a \ 'b::order) \ bool"
  where "antimono \ monotone (\) (\x y. y \ x)"

lemma mono_def[no_atp]: "mono f \ (\x y. x \ y \ f x \ f y)"
  by (simp add: monotone_on_def)

lemma strict_mono_def[no_atp]: "strict_mono f \ (\x y. x < y \ f x < f y)"
  by (simp add: monotone_on_def)

lemma antimono_def[no_atp]: "antimono f \ (\x y. x \ y \ f x \ f y)"
  by (simp add: monotone_on_def)

text \<open>Lemmas @{thm [source] mono_def}, @{thm [source] strict_mono_def}, and
@{thm [source] antimono_def} are provided for backward compatibility.\<close>

lemma monoI [intro?]: "(\x y. x \ y \ f x \ f y) \ mono f"
  by (rule monotoneI)

lemma strict_monoI [intro?]: "(\x y. x < y \ f x < f y) \ strict_mono f"
  by (rule monotoneI)

lemma antimonoI [intro?]: "(\x y. x \ y \ f x \ f y) \ antimono f"
  by (rule monotoneI)

lemma monoD [dest?]: "mono f \ x \ y \ f x \ f y"
  by (rule monotoneD)

lemma strict_monoD [dest?]: "strict_mono f \ x < y \ f x < f y"
  by (rule monotoneD)

lemma antimonoD [dest?]: "antimono f \ x \ y \ f x \ f y"
  by (rule monotoneD)

lemma monoE:
  assumes "mono f"
  assumes "x \ y"
  obtains "f x \ f y"
proof
  from assms show "f x \ f y" by (simp add: mono_def)
qed

lemma antimonoE:
  fixes f :: "'a \ 'b::order"
  assumes "antimono f"
  assumes "x \ y"
  obtains "f x \ f y"
proof
  from assms show "f x \ f y" by (simp add: antimono_def)
qed

end

lemma mono_imp_mono_on: "mono f \ mono_on A f"
  by (rule monotone_on_subset[OF _ subset_UNIV])

lemma strict_mono_on_imp_mono_on: "strict_mono_on A f \ mono_on A f"
  for f :: "'a::order \ 'b::preorder"
proof (intro mono_onI)
  fix r s :: 'a assume asm: "r \ s" "strict_mono_on A f" "r \ A" "s \ A"
  from this(1) consider "r < s" | "r = s" by fastforce
  then show "f r \ f s"
  proof(cases)
    case 1
    from strict_mono_onD[OF asm(2-4) this] show ?thesis by (fact order.strict_implies_order)
  qed simp
qed

lemma strict_mono_mono [dest?]:
  "strict_mono f \ mono f"
  by (fact strict_mono_on_imp_mono_on)

lemma mono_on_ident: "mono_on S (\x. x)"
  by (intro monotone_onI)

lemma mono_on_id: "mono_on S id"
  unfolding id_def by (fact mono_on_ident)

lemma strict_mono_on_ident: "strict_mono_on S (\x. x)"
  by (intro monotone_onI)

lemma strict_mono_on_id: "strict_mono_on S id"
  unfolding id_def by (fact strict_mono_on_ident)

lemma mono_on_const:
  fixes a :: "'b::preorder" shows "mono_on S (\x. a)"
  by (intro monotone_onI order.refl)

lemma antimono_on_const:
  fixes a :: "'b::preorder" shows "antimono_on S (\x. a)"
  by (intro monotone_onI order.refl)

context linorder begin

lemma mono_on_strict_invE:
  fixes f :: "'a \ 'b::preorder"
  assumes "mono_on S f"
  assumes "x \ S" "y \ S"
  assumes "f x < f y"
  obtains "x < y"
proof
  show "x < y"
  proof (rule ccontr)
    assume "\ x < y"
    then have "y \ x" by simp
    with \<open>mono_on S f\<close> \<open>x \<in> S\<close> \<open>y \<in> S\<close> have "f y \<le> f x" by (simp only: monotone_onD)
    with \<open>f x < f y\<close> show False by (simp add: preorder_class.less_le_not_le)
  qed
qed

corollary mono_on_invE:
  fixes f :: "'a \ 'b::preorder"
  assumes "mono_on S f"
  assumes "x \ S" "y \ S"
  assumes "f x < f y"
  obtains "x \ y"
  using assms mono_on_strict_invE[of S f x y thesis] by simp

lemma strict_mono_on_eq:
  assumes "strict_mono_on S (f::'a \ 'b::preorder)"
  assumes "x \ S" "y \ S"
  shows "f x = f y \ x = y"
proof
  assume "f x = f y"
  show "x = y" proof (cases x y rule: linorder_cases)
    case less with assms have "f x < f y" by (simp add: monotone_onD)
    with \<open>f x = f y\<close> show ?thesis by simp
  next
    case equal then show ?thesis .
  next
    case greater with assms have "f y < f x" by (simp add: monotone_onD)
    with \<open>f x = f y\<close> show ?thesis by simp
  qed
qed simp

lemma strict_mono_on_less_eq:
  assumes "strict_mono_on S (f::'a \ 'b::preorder)"
  assumes "x \ S" "y \ S"
  shows "f x \ f y \ x \ y"
proof
  assume "x \ y"
  then show "f x \ f y"
    using nless_le[of x y] monotone_onD[OF assms] order_less_imp_le[of "f x" "f y"]
    by blast
next
  assume "f x \ f y"
  show "x \ y"
  proof (rule ccontr)
    assume "\ x \ y"
    then have "y < x" by simp
    with assms have "f y < f x" by (simp add: monotone_onD)
    with \<open>f x \<le> f y\<close> show False by (simp add: preorder_class.less_le_not_le)
  qed
qed

lemma strict_mono_on_less:
  assumes "strict_mono_on S (f::'a \ _::preorder)"
  assumes "x \ S" "y \ S"
  shows "f x < f y \ x < y"
  using assms strict_mono_on_eq[of S f x y]
  by (auto simp add: strict_mono_on_less_eq preorder_class.less_le_not_le)

lemmas mono_invE = mono_on_invE[OF _ UNIV_I UNIV_I]
lemmas mono_strict_invE = mono_on_strict_invE[OF _ UNIV_I UNIV_I]
lemmas strict_mono_eq = strict_mono_on_eq[OF _ UNIV_I UNIV_I]
lemmas strict_mono_less_eq = strict_mono_on_less_eq[OF _ UNIV_I UNIV_I]
lemmas strict_mono_less = strict_mono_on_less[OF _ UNIV_I UNIV_I]

end

lemma strict_mono_inv:
  fixes f :: "('a::linorder) \ ('b::linorder)"
  assumes "strict_mono f" and "surj f" and inv: "\x. g (f x) = x"
  shows "strict_mono g"
proof
  fix x y :: 'b assume "x < y"
  from \<open>surj f\<close> obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast
  with \<open>x < y\<close> and \<open>strict_mono f\<close> have "x' < y'" by (simp add: strict_mono_less)
  with inv show "g x < g y" by simp
qed

lemma strict_mono_on_imp_inj_on:
  fixes f :: "'a::linorder \ 'b::preorder"
  assumes "strict_mono_on A f"
  shows "inj_on f A"
proof (rule inj_onI)
  fix x y assume "x \ A" "y \ A" "f x = f y"
  thus "x = y"
    by (cases x y rule: linorder_cases)
       (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x])
qed

lemma strict_mono_on_leD:
  fixes f :: "'a::order \ 'b::preorder"
  assumes "strict_mono_on A f" "x \ A" "y \ A" "x \ y"
  shows "f x \ f y"
proof (cases "x = y")
  case True
  then show ?thesis by simp
next
  case False
  with assms have "f x < f y"
    using strict_mono_onD[OF assms(1)] by simp
  then show ?thesis by (rule less_imp_le)
qed

lemma strict_mono_on_eqD:
  fixes f :: "'c::linorder \ 'd::preorder"
  assumes "strict_mono_on A f" "f x = f y" "x \ A" "y \ A"
  shows "y = x"
  using assms by (cases rule: linorder_cases) (auto dest: strict_mono_onD)

lemma mono_imp_strict_mono:
  fixes f :: "'a::order \ 'b::order"
  shows "\mono_on S f; inj_on f S\ \ strict_mono_on S f"
  by (auto simp add: monotone_on_def order_less_le inj_on_eq_iff)

lemma strict_mono_iff_mono:
  fixes f :: "'a::linorder \ 'b::order"
  shows "strict_mono_on S f \ mono_on S f \ inj_on f S"
proof
  show "strict_mono_on S f \ mono_on S f \ inj_on f S"
    by (simp add: strict_mono_on_imp_inj_on strict_mono_on_imp_mono_on)
qed (auto intro: mono_imp_strict_mono)

lemma antimono_imp_strict_antimono:
  fixes f :: "'a::order \ 'b::order"
  shows "\antimono_on S f; inj_on f S\ \ strict_antimono_on S f"
  by (auto simp add: monotone_on_def order_less_le inj_on_eq_iff)

lemma strict_antimono_iff_antimono:
  fixes f :: "'a::linorder \ 'b::order"
  shows "strict_antimono_on S f \ antimono_on S f \ inj_on f S"
proof
  show "strict_antimono_on S f \ antimono_on S f \ inj_on f S"
    by (force simp add: monotone_on_def intro: linorder_inj_onI)
qed (auto intro: antimono_imp_strict_antimono)

lemma mono_compose: "mono Q \ mono (\i x. Q i (f x))"
  unfolding mono_def le_fun_def by auto

lemma mono_add:
  fixes a :: "'a::ordered_ab_semigroup_add"
  shows "mono ((+) a)"
  by (simp add: add_left_mono monoI)

lemma (in semilattice_inf) mono_inf: "mono f \ f (A \ B) \ f A \ f B"
  for f :: "'a \ 'b::semilattice_inf"
  by (auto simp add: mono_def intro: Lattices.inf_greatest)

lemma (in semilattice_sup) mono_sup: "mono f \ f A \ f B \ f (A \ B)"
  for f :: "'a \ 'b::semilattice_sup"
  by (auto simp add: mono_def intro: Lattices.sup_least)

lemma monotone_on_sup_fun:
  fixes f g :: "_ \ _:: semilattice_sup"
  shows "monotone_on A P (\) f \ monotone_on A P (\) g \ monotone_on A P (\) (f \ g)"
  by (auto intro: monotone_onI sup_mono dest: monotone_onD simp: sup_fun_def)

lemma monotone_on_inf_fun:
  fixes f g :: "_ \ _:: semilattice_inf"
  shows "monotone_on A P (\) f \ monotone_on A P (\) g \ monotone_on A P (\) (f \ g)"
  by (auto intro: monotone_onI inf_mono dest: monotone_onD simp: inf_fun_def)

lemma antimonotone_on_sup_fun:
  fixes f g :: "_ \ _:: semilattice_sup"
  shows "monotone_on A P (\) f \ monotone_on A P (\) g \ monotone_on A P (\) (f \ g)"
  by (auto intro: monotone_onI sup_mono dest: monotone_onD simp: sup_fun_def)

lemma antimonotone_on_inf_fun:
  fixes f g :: "_ \ _:: semilattice_inf"
  shows "monotone_on A P (\) f \ monotone_on A P (\) g \ monotone_on A P (\) (f \ g)"
  by (auto intro: monotone_onI inf_mono dest: monotone_onD simp: inf_fun_def)

lemma (in linorder) min_of_mono: "mono f \ min (f m) (f n) = f (min m n)"
  by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)

lemma (in linorder) max_of_mono: "mono f \ max (f m) (f n) = f (max m n)"
  by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)

lemma (in linorder)
  max_of_antimono: "antimono f \ max (f x) (f y) = f (min x y)" and
  min_of_antimono: "antimono f \ min (f x) (f y) = f (max x y)"
  by (auto simp: antimono_def Orderings.max_def max_def Orderings.min_def min_def intro!: antisym)

lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \ inj_on f A"
  by (auto intro!: inj_onI dest: strict_mono_eq)

lemma mono_Int: "mono f \ f (A \ B) \ f A \ f B"
  by (fact mono_inf)

lemma mono_Un: "mono f \ f A \ f B \ f (A \ B)"
  by (fact mono_sup)

subsubsection \<open>Least value operator\<close>

lemma Least_mono: "mono f \ \x\S. \y\S. x \ y \ (LEAST y. y \ f ` S) = f (LEAST x. x \ S)"
  for f :: "'a::order \ 'b::order"
  \<comment> \<open>Courtesy of Stephan Merz\<close>
  apply clarify
  apply (erule_tac P = "\x. x \ S" in LeastI2_order)
   apply fast
  apply (rule LeastI2_order)
    apply (auto elim: monoD intro!: order_antisym)
  done

subsection \<open>Setup\<close>

subsubsection \<open>Proof tools\<close>

text \<open>Simplify terms of the form \<open>f(\<dots>,x:=y,\<dots>,x:=z,\<dots>)\<close> to \<open>f(\<dots>,x:=z,\<dots>)\<close>\<close>

simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>
  let
    fun gen_fun_upd _ _ _ _ NONE = NONE
      | gen_fun_upd A B x y (SOME f) = SOME \<^Const>\<open>fun_upd A B for f x y\<close>
    fun find_double (t as \<^Const_>\<open>fun_upd A B for f x y\<close>) =
      let
        fun find \<^Const_>\<open>fun_upd _ _ for g v w\<close> =
              if v aconv x then SOME g
              else gen_fun_upd A B v w (find g)
          | find t = NONE
      in gen_fun_upd A B x y (find f) end

    val ss = simpset_of \<^context>
  in
    fn _ => fn ctxt => fn ct =>
      let val t = Thm.term_of ct in
        find_double t |> Option.map (fn rhs =>
          Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
            (fn _ =>
              resolve_tac ctxt [eq_reflection] 1 THEN
              resolve_tac ctxt @{thms ext} 1 THEN
              simp_tac (put_simpset ss ctxt) 1))
      end
  end
\<close>

subsubsection \<open>Functorial structure of types\<close>

ML_file \<open>Tools/functor.ML\<close>

functor map_fun: map_fun
  by (simp_all add: fun_eq_iff)

functor vimage
  by (simp_all add: fun_eq_iff vimage_comp)

text \<open>Legacy theorem names\<close>

lemmas o_def = comp_def
lemmas o_apply = comp_apply
lemmas o_assoc = comp_assoc [symmetric]
lemmas id_o = id_comp
lemmas o_id = comp_id
lemmas o_eq_dest = comp_eq_dest
lemmas o_eq_elim = comp_eq_elim
lemmas o_eq_dest_lhs = comp_eq_dest_lhs
lemmas o_eq_id_dest = comp_eq_id_dest

end

quality99%

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.