a few new lemmas about functions
authorpaulson <lp15@cam.ac.uk>
Sat May 23 21:24:33 2020 +0100 (8 days ago)
changeset 71857d73955442df5
parent 71856 e9df7895e331
child 71859 059d2cf529d4
a few new lemmas about functions
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Starlike.thy
src/HOL/BNF_Wellorder_Embedding.thy
src/HOL/Fun.thy
src/HOL/Library/Equipollence.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Fri May 22 19:21:16 2020 +0200
     1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Sat May 23 21:24:33 2020 +0100
     1.3 @@ -2673,7 +2673,8 @@
     1.4      then have "False"
     1.5        using homeomorphic_map_closure_of [OF hom] hom
     1.6        unfolding homeomorphic_eq_everything_map
     1.7 -      by (metis (no_types, lifting) Diff_subset S closure_of_subset_topspace inj_on_image_mem_iff_alt inj_on_image_set_diff) }
     1.8 +      by (metis Diff_subset S closure_of_subset_topspace inj_on_image_mem_iff inj_on_image_set_diff)
     1.9 +  }
    1.10    ultimately  show ?thesis
    1.11      by (auto simp: interior_of_closure_of)
    1.12  qed
    1.13 @@ -2700,7 +2701,7 @@
    1.14    then have "y \<in> topspace X"
    1.15      by (simp add: in_closure_of)
    1.16    then have "f y \<notin> f ` (X interior_of S)"
    1.17 -    by (meson hom homeomorphic_eq_everything_map inj_on_image_mem_iff_alt interior_of_subset_topspace y(3))
    1.18 +    by (meson hom homeomorphic_map_def inj_on_image_mem_iff interior_of_subset_topspace y(3))
    1.19    then show "x \<notin> Y interior_of f ` S"
    1.20      using S hom homeomorphic_map_interior_of y(1) by blast
    1.21  qed
     2.1 --- a/src/HOL/Analysis/Starlike.thy	Fri May 22 19:21:16 2020 +0200
     2.2 +++ b/src/HOL/Analysis/Starlike.thy	Sat May 23 21:24:33 2020 +0100
     2.3 @@ -3519,7 +3519,7 @@
     2.4        ultimately have "f a \<in> f ` closed_segment c b"
     2.5          by blast
     2.6        then have a: "a \<in> closed_segment c b"
     2.7 -        by (meson ends_in_segment inj_on_image_mem_iff_alt injf subset_closed_segment that)
     2.8 +        by (meson ends_in_segment inj_on_image_mem_iff injf subset_closed_segment that)
     2.9        have cb: "closed_segment c b \<subseteq> closed_segment a b"
    2.10          by (simp add: closed_segment_subset that)
    2.11        show "f a = f c"
    2.12 @@ -3539,7 +3539,7 @@
    2.13        ultimately have "f b \<in> f ` closed_segment a c"
    2.14          by blast
    2.15        then have b: "b \<in> closed_segment a c"
    2.16 -        by (meson ends_in_segment inj_on_image_mem_iff_alt injf subset_closed_segment that)
    2.17 +        by (meson ends_in_segment inj_on_image_mem_iff injf subset_closed_segment that)
    2.18        have ca: "closed_segment a c \<subseteq> closed_segment a b"
    2.19          by (simp add: closed_segment_subset that)
    2.20        show "f b = f c"
     3.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri May 22 19:21:16 2020 +0200
     3.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Sat May 23 21:24:33 2020 +0100
     3.3 @@ -1003,55 +1003,29 @@
     3.4    with * show "iso r r' f" unfolding iso_def by auto
     3.5  qed
     3.6  
     3.7 -lemma iso_iff2:
     3.8 -assumes "Well_order r"
     3.9 -shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and>
    3.10 -                     (\<forall>a \<in> Field r. \<forall>b \<in> Field r.
    3.11 -                         (((a,b) \<in> r) = ((f a, f b) \<in> r'))))"
    3.12 -using assms
    3.13 -proof(auto simp add: iso_def)
    3.14 -  fix a b
    3.15 -  assume "embed r r' f"
    3.16 -  hence "compat r r' f" using embed_compat[of r] by auto
    3.17 -  moreover assume "(a,b) \<in> r"
    3.18 -  ultimately show "(f a, f b) \<in> r'" using compat_def[of r] by auto
    3.19 -next
    3.20 -  let ?f' = "inv_into (Field r) f"
    3.21 -  assume "embed r r' f" and 1: "bij_betw f (Field r) (Field r')"
    3.22 -  hence "embed r' r ?f'" using assms
    3.23 -  by (auto simp add: inv_into_Field_embed_bij_betw)
    3.24 -  hence 2: "compat r' r ?f'" using embed_compat[of r'] by auto
    3.25 -  fix a b assume *: "a \<in> Field r" "b \<in> Field r" and **: "(f a,f b) \<in> r'"
    3.26 -  hence "?f'(f a) = a \<and> ?f'(f b) = b" using 1
    3.27 -  by (auto simp add: bij_betw_inv_into_left)
    3.28 -  thus "(a,b) \<in> r" using ** 2 compat_def[of r' r ?f'] by fastforce
    3.29 +lemma iso_iff2: "iso r r' f \<longleftrightarrow>
    3.30 +                 bij_betw f (Field r) (Field r') \<and> 
    3.31 +                 (\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a, b) \<in> r \<longleftrightarrow> (f a, f b) \<in> r')"
    3.32 +    (is "?lhs = ?rhs")
    3.33 +proof
    3.34 +  assume L: ?lhs
    3.35 +  then have "bij_betw f (Field r) (Field r')" and emb: "embed r r' f"
    3.36 +    by (auto simp: bij_betw_def iso_def)
    3.37 +  then obtain g where g: "\<And>x. x \<in> Field r \<Longrightarrow> g (f x) = x"
    3.38 +    by (auto simp: bij_betw_iff_bijections)
    3.39 +  moreover
    3.40 +  have "(a, b) \<in> r" if "a \<in> Field r" "b \<in> Field r" "(f a, f b) \<in> r'" for a b 
    3.41 +    using that emb g g [OF FieldI1] \<comment>\<open>yes it's weird\<close>
    3.42 +    by (force simp add: embed_def under_def bij_betw_iff_bijections)
    3.43 +  ultimately show ?rhs
    3.44 +    using L by (auto simp: compat_def iso_def dest: embed_compat)
    3.45  next
    3.46 -  assume *: "bij_betw f (Field r) (Field r')" and
    3.47 -         **: "\<forall>a\<in>Field r. \<forall>b\<in>Field r. ((a, b) \<in> r) = ((f a, f b) \<in> r')"
    3.48 -  have 1: "\<And> a. under r a \<le> Field r \<and> under r' (f a) \<le> Field r'"
    3.49 -  by (auto simp add: under_Field)
    3.50 -  have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def)
    3.51 -  {fix a assume ***: "a \<in> Field r"
    3.52 -   have "bij_betw f (under r a) (under r' (f a))"
    3.53 -   proof(unfold bij_betw_def, auto)
    3.54 -     show "inj_on f (under r a)" using 1 2 subset_inj_on by blast
    3.55 -   next
    3.56 -     fix b assume "b \<in> under r a"
    3.57 -     hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"
    3.58 -     unfolding under_def by (auto simp add: Field_def Range_def Domain_def)
    3.59 -     with 1 ** show "f b \<in> under r' (f a)"
    3.60 -     unfolding under_def by auto
    3.61 -   next
    3.62 -     fix b' assume "b' \<in> under r' (f a)"
    3.63 -     hence 3: "(b',f a) \<in> r'" unfolding under_def by simp
    3.64 -     hence "b' \<in> Field r'" unfolding Field_def by auto
    3.65 -     with * obtain b where "b \<in> Field r \<and> f b = b'"
    3.66 -     unfolding bij_betw_def by force
    3.67 -     with 3 ** ***
    3.68 -     show "b' \<in> f ` (under r a)" unfolding under_def by blast
    3.69 -   qed
    3.70 -  }
    3.71 -  thus "embed r r' f" unfolding embed_def using * by auto
    3.72 +  assume R: ?rhs
    3.73 +  then show ?lhs
    3.74 +    apply (clarsimp simp add: iso_def embed_def under_def bij_betw_iff_bijections)
    3.75 +    apply (rule_tac x="g" in exI)
    3.76 +    apply (fastforce simp add: intro: FieldI1)+
    3.77 +    done
    3.78  qed
    3.79  
    3.80  lemma iso_iff3:
     4.1 --- a/src/HOL/Fun.thy	Fri May 22 19:21:16 2020 +0200
     4.2 +++ b/src/HOL/Fun.thy	Sat May 23 21:24:33 2020 +0100
     4.3 @@ -507,10 +507,6 @@
     4.4  lemma inj_on_image_mem_iff: "inj_on f B \<Longrightarrow> a \<in> B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f a \<in> f ` A \<longleftrightarrow> a \<in> A"
     4.5    by (auto simp: inj_on_def)
     4.6  
     4.7 -(*FIXME DELETE*)
     4.8 -lemma inj_on_image_mem_iff_alt: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f a \<in> f ` A \<Longrightarrow> a \<in> B \<Longrightarrow> a \<in> A"
     4.9 -  by (blast dest: inj_onD)
    4.10 -
    4.11  lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f ` A \<longleftrightarrow> a \<in> A"
    4.12    by (blast dest: injD)
    4.13  
    4.14 @@ -614,7 +610,20 @@
    4.15      using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast
    4.16  qed
    4.17  
    4.18 -text \<open>Important examples\<close>
    4.19 +lemma inj_on_disjoint_Un:
    4.20 +  assumes "inj_on f A" and "inj_on g B" 
    4.21 +  and "f ` A \<inter> g ` B = {}"
    4.22 +  shows "inj_on (\<lambda>x. if x \<in> A then f x else g x) (A \<union> B)"
    4.23 +  using assms by (simp add: inj_on_def disjoint_iff) (blast)
    4.24 +
    4.25 +lemma bij_betw_disjoint_Un:
    4.26 +  assumes "bij_betw f A C" and "bij_betw g B D" 
    4.27 +  and "A \<inter> B = {}"
    4.28 +  and "C \<inter> D = {}"
    4.29 +  shows "bij_betw (\<lambda>x. if x \<in> A then f x else g x) (A \<union> B) (C \<union> D)"
    4.30 +  using assms by (auto simp: inj_on_disjoint_Un bij_betw_def)
    4.31 +
    4.32 +subsubsection \<open>Important examples\<close>
    4.33  
    4.34  context cancel_semigroup_add
    4.35  begin
    4.36 @@ -859,27 +868,18 @@
    4.37    unfolding the_inv_into_def inj_on_def by blast
    4.38  
    4.39  lemma f_the_inv_into_f: "inj_on f A \<Longrightarrow> y \<in> f ` A  \<Longrightarrow> f (the_inv_into A f y) = y"
    4.40 -  apply (simp add: the_inv_into_def)
    4.41 -  apply (rule the1I2)
    4.42 -   apply (blast dest: inj_onD)
    4.43 -  apply blast
    4.44 -  done
    4.45 +  unfolding the_inv_into_def
    4.46 +  by (rule the1I2; blast dest: inj_onD)
    4.47  
    4.48  lemma the_inv_into_into: "inj_on f A \<Longrightarrow> x \<in> f ` A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> the_inv_into A f x \<in> B"
    4.49 -  apply (simp add: the_inv_into_def)
    4.50 -  apply (rule the1I2)
    4.51 -   apply (blast dest: inj_onD)
    4.52 -  apply blast
    4.53 -  done
    4.54 +  unfolding the_inv_into_def
    4.55 +  by (rule the1I2; blast dest: inj_onD)
    4.56  
    4.57  lemma the_inv_into_onto [simp]: "inj_on f A \<Longrightarrow> the_inv_into A f ` (f ` A) = A"
    4.58    by (fast intro: the_inv_into_into the_inv_into_f_f [symmetric])
    4.59  
    4.60  lemma the_inv_into_f_eq: "inj_on f A \<Longrightarrow> f x = y \<Longrightarrow> x \<in> A \<Longrightarrow> the_inv_into A f y = x"
    4.61 -  apply (erule subst)
    4.62 -  apply (erule the_inv_into_f_f)
    4.63 -  apply assumption
    4.64 -  done
    4.65 +  by (force simp add: the_inv_into_f_f)
    4.66  
    4.67  lemma the_inv_into_comp:
    4.68    "inj_on f (g ` A) \<Longrightarrow> inj_on g A \<Longrightarrow> x \<in> f ` g ` A \<Longrightarrow>
    4.69 @@ -896,6 +896,17 @@
    4.70  lemma bij_betw_the_inv_into: "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
    4.71    by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into)
    4.72  
    4.73 +lemma bij_betw_iff_bijections:
    4.74 +  "bij_betw f A B \<longleftrightarrow> (\<exists>g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
    4.75 +  (is "?lhs = ?rhs")
    4.76 +proof
    4.77 +  assume L: ?lhs
    4.78 +  then show ?rhs
    4.79 +    apply (rule_tac x="the_inv_into A f" in exI)
    4.80 +    apply (auto simp: bij_betw_def f_the_inv_into_f the_inv_into_f_f the_inv_into_into)
    4.81 +    done
    4.82 +qed (force intro: bij_betw_byWitness)
    4.83 +
    4.84  abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
    4.85    where "the_inv f \<equiv> the_inv_into UNIV f"
    4.86  
     5.1 --- a/src/HOL/Library/Equipollence.thy	Fri May 22 19:21:16 2020 +0200
     5.2 +++ b/src/HOL/Library/Equipollence.thy	Sat May 23 21:24:33 2020 +0100
     5.3 @@ -98,21 +98,6 @@
     5.4        by (auto simp: inj_on_def)
     5.5  qed auto
     5.6  
     5.7 -lemma bij_betw_iff_bijections:
     5.8 -  "bij_betw f A B \<longleftrightarrow> (\<exists>g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
     5.9 -  (is "?lhs = ?rhs")
    5.10 -proof
    5.11 -  assume L: ?lhs
    5.12 -  then show ?rhs
    5.13 -    apply (rule_tac x="the_inv_into A f" in exI)
    5.14 -    apply (auto simp: bij_betw_def f_the_inv_into_f the_inv_into_f_f the_inv_into_into)
    5.15 -    done
    5.16 -next
    5.17 -  assume ?rhs
    5.18 -  then show ?lhs
    5.19 -    by (auto simp: bij_betw_def inj_on_def image_def; metis)
    5.20 -qed
    5.21 -
    5.22  lemma eqpoll_iff_bijections:
    5.23     "A \<approx> B \<longleftrightarrow> (\<exists>f g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
    5.24      by (auto simp: eqpoll_def bij_betw_iff_bijections)
     6.1 --- a/src/HOL/List.thy	Fri May 22 19:21:16 2020 +0200
     6.2 +++ b/src/HOL/List.thy	Sat May 23 21:24:33 2020 +0100
     6.3 @@ -6117,6 +6117,67 @@
     6.4    by (simp add: Uniq_def strict_sorted_equal)
     6.5  
     6.6  
     6.7 +lemma length_sorted_list_of_set [simp]:
     6.8 +  fixes A :: "'a::linorder set" 
     6.9 +  shows "length (sorted_list_of_set A) = card A"
    6.10 +proof (cases "finite A")
    6.11 +  case True
    6.12 +  then show ?thesis 
    6.13 +    by(metis distinct_card distinct_sorted_list_of_set set_sorted_list_of_set)
    6.14 +qed auto
    6.15 +
    6.16 +lemma sorted_list_of_set_inject:
    6.17 +  fixes A :: "'a::linorder set" 
    6.18 +  assumes "sorted_list_of_set A = sorted_list_of_set B" "finite A" "finite B" 
    6.19 +  shows "A = B"
    6.20 +  using assms set_sorted_list_of_set by fastforce
    6.21 +
    6.22 +lemma sorted_list_of_set_unique:
    6.23 +  fixes A :: "'a::linorder set" 
    6.24 +  assumes "finite A"
    6.25 +  shows "strict_sorted l \<and> List.set l = A \<and> length l = card A \<longleftrightarrow> sorted_list_of_set A = l"
    6.26 +  using assms strict_sorted_equal by force
    6.27 +
    6.28 +
    6.29 +lemma sorted_list_of_set_lessThan_Suc [simp]: 
    6.30 +  "sorted_list_of_set {..<Suc k} = sorted_list_of_set {..<k} @ [k]"
    6.31 +proof -
    6.32 +  have "sorted_wrt (<) (sorted_list_of_set {..<k} @ [k])"
    6.33 +    unfolding sorted_wrt_append  by (auto simp flip: strict_sorted_sorted_wrt)
    6.34 +  then show ?thesis
    6.35 +    by (simp add: lessThan_atLeast0)
    6.36 +qed
    6.37 +
    6.38 +lemma sorted_list_of_set_atMost_Suc [simp]:
    6.39 +  "sorted_list_of_set {..Suc k} = sorted_list_of_set {..k} @ [Suc k]"
    6.40 +  using lessThan_Suc_atMost sorted_list_of_set_lessThan_Suc by fastforce
    6.41 +
    6.42 +lemma sorted_list_of_set_greaterThanLessThan:
    6.43 +  assumes "Suc i < j" 
    6.44 +    shows "sorted_list_of_set {i<..<j} = Suc i # sorted_list_of_set {Suc i<..<j}"
    6.45 +proof -
    6.46 +  have "{i<..<j} = insert (Suc i) {Suc i<..<j}"
    6.47 +    using assms by auto
    6.48 +  then show ?thesis
    6.49 +    by (metis assms atLeastSucLessThan_greaterThanLessThan sorted_list_of_set_range upt_conv_Cons)
    6.50 +qed
    6.51 +
    6.52 +lemma sorted_list_of_set_greaterThanAtMost:
    6.53 +  assumes "Suc i \<le> j" 
    6.54 +    shows "sorted_list_of_set {i<..j} = Suc i # sorted_list_of_set {Suc i<..j}"
    6.55 +  using sorted_list_of_set_greaterThanLessThan [of i "Suc j"]
    6.56 +  by (metis assms greaterThanAtMost_def greaterThanLessThan_eq le_imp_less_Suc lessThan_Suc_atMost)
    6.57 +
    6.58 +lemma nth_sorted_list_of_set_greaterThanLessThan: 
    6.59 +  "n < j - Suc i \<Longrightarrow> sorted_list_of_set {i<..<j} ! n = Suc (i+n)"
    6.60 +  by (induction n arbitrary: i) (auto simp: sorted_list_of_set_greaterThanLessThan)
    6.61 +
    6.62 +lemma nth_sorted_list_of_set_greaterThanAtMost: 
    6.63 +  "n < j - i \<Longrightarrow> sorted_list_of_set {i<..j} ! n = Suc (i+n)"
    6.64 +  using nth_sorted_list_of_set_greaterThanLessThan [of n "Suc j" i]
    6.65 +  by (simp add: greaterThanAtMost_def greaterThanLessThan_eq lessThan_Suc_atMost)
    6.66 +
    6.67 +
    6.68  subsubsection \<open>\<open>lists\<close>: the list-forming operator over sets\<close>
    6.69  
    6.70  inductive_set