moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
authornipkow
Thu Feb 21 17:33:58 2008 +0100 (2008-02-21)
changeset 26105ae06618225ec
parent 26104 200b4e401e65
child 26106 be52145f482d
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
added some
src/HOL/Fun.thy
src/HOL/Hilbert_Choice.thy
src/HOL/SetInterval.thy
src/HOL/Wellfounded_Recursion.thy
     1.1 --- a/src/HOL/Fun.thy	Wed Feb 20 23:24:38 2008 +0100
     1.2 +++ b/src/HOL/Fun.thy	Thu Feb 21 17:33:58 2008 +0100
     1.3 @@ -59,9 +59,14 @@
     1.4  lemmas o_def = comp_def
     1.5  
     1.6  constdefs
     1.7 -  inj_on :: "['a => 'b, 'a set] => bool"         (*injective*)
     1.8 +  inj_on :: "['a => 'b, 'a set] => bool"  -- "injective"
     1.9    "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.10  
    1.11 +definition
    1.12 +  bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
    1.13 +  "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
    1.14 +
    1.15 +
    1.16  text{*A common special case: functions injective over the entire domain type.*}
    1.17  
    1.18  abbreviation
    1.19 @@ -237,8 +242,7 @@
    1.20  done
    1.21  
    1.22  
    1.23 -
    1.24 -subsection{*The Predicate @{term bij}: Bijectivity*}
    1.25 +subsection{*The Predicate @{const bij}: Bijectivity*}
    1.26  
    1.27  lemma bijI: "[| inj f; surj f |] ==> bij f"
    1.28  by (simp add: bij_def)
    1.29 @@ -250,6 +254,43 @@
    1.30  by (simp add: bij_def)
    1.31  
    1.32  
    1.33 +subsection{*The Predicate @{const bij_betw}: Bijectivity*}
    1.34 +
    1.35 +lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
    1.36 +by (simp add: bij_betw_def)
    1.37 +
    1.38 +lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
    1.39 +proof -
    1.40 +  have i: "inj_on f A" and s: "f ` A = B"
    1.41 +    using assms by(auto simp:bij_betw_def)
    1.42 +  let ?P = "%b a. a:A \<and> f a = b" let ?g = "%b. The (?P b)"
    1.43 +  { fix a b assume P: "?P b a"
    1.44 +    hence ex1: "\<exists>a. ?P b a" using s unfolding image_def by blast
    1.45 +    hence uex1: "\<exists>!a. ?P b a" by(blast dest:inj_onD[OF i])
    1.46 +    hence " ?g b = a" using the1_equality[OF uex1, OF P] P by simp
    1.47 +  } note g = this
    1.48 +  have "inj_on ?g B"
    1.49 +  proof(rule inj_onI)
    1.50 +    fix x y assume "x:B" "y:B" "?g x = ?g y"
    1.51 +    from s `x:B` obtain a1 where a1: "?P x a1" unfolding image_def by blast
    1.52 +    from s `y:B` obtain a2 where a2: "?P y a2" unfolding image_def by blast
    1.53 +    from g[OF a1] a1 g[OF a2] a2 `?g x = ?g y` show "x=y" by simp
    1.54 +  qed
    1.55 +  moreover have "?g ` B = A"
    1.56 +  proof(auto simp:image_def)
    1.57 +    fix b assume "b:B"
    1.58 +    with s obtain a where P: "?P b a" unfolding image_def by blast
    1.59 +    thus "?g b \<in> A" using g[OF P] by auto
    1.60 +  next
    1.61 +    fix a assume "a:A"
    1.62 +    then obtain b where P: "?P b a" using s unfolding image_def by blast
    1.63 +    then have "b:B" using s unfolding image_def by blast
    1.64 +    with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
    1.65 +  qed
    1.66 +  ultimately show ?thesis by(auto simp:bij_betw_def)
    1.67 +qed
    1.68 +
    1.69 +
    1.70  subsection{*Facts About the Identity Function*}
    1.71  
    1.72  text{*We seem to need both the @{term id} forms and the @{term "\<lambda>x. x"}
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Feb 20 23:24:38 2008 +0100
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Feb 21 17:33:58 2008 +0100
     2.3 @@ -268,6 +268,11 @@
     2.4    apply (simp add: Inv_mem)
     2.5    done
     2.6  
     2.7 +lemma bij_betw_Inv: "bij_betw f A B \<Longrightarrow> bij_betw (Inv A f) B A"
     2.8 +  apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
     2.9 +  apply (simp add: image_compose [symmetric] o_def)
    2.10 +  apply (simp add: image_def Inv_f_f)
    2.11 +  done
    2.12  
    2.13  subsection {*Other Consequences of Hilbert's Epsilon*}
    2.14  
     3.1 --- a/src/HOL/SetInterval.thy	Wed Feb 20 23:24:38 2008 +0100
     3.2 +++ b/src/HOL/SetInterval.thy	Thu Feb 21 17:33:58 2008 +0100
     3.3 @@ -469,6 +469,18 @@
     3.4  lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
     3.5    by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
     3.6  
     3.7 +
     3.8 +lemma ex_bij_betw_nat_finite:
     3.9 +  "finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
    3.10 +apply(drule finite_imp_nat_seg_image_inj_on)
    3.11 +apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def)
    3.12 +done
    3.13 +
    3.14 +lemma ex_bij_betw_finite_nat:
    3.15 +  "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
    3.16 +by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
    3.17 +
    3.18 +
    3.19  subsection {* Intervals of integers *}
    3.20  
    3.21  lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
     4.1 --- a/src/HOL/Wellfounded_Recursion.thy	Wed Feb 20 23:24:38 2008 +0100
     4.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Thu Feb 21 17:33:58 2008 +0100
     4.3 @@ -633,6 +633,22 @@
     4.4     "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
     4.5  by (erule (1) Least_Suc [THEN ssubst], simp)
     4.6  
     4.7 +lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)"
     4.8 +apply(cases n) apply blast
     4.9 +apply(rule_tac x="LEAST k. P(k)" in exI)
    4.10 +apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
    4.11 +done
    4.12 +
    4.13 +lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
    4.14 +apply(cases n) apply blast
    4.15 +apply(frule (1) ex_least_nat_le)
    4.16 +apply(erule exE)
    4.17 +apply(case_tac k) apply simp
    4.18 +apply(rename_tac k1)
    4.19 +apply(rule_tac x=k1 in exI)
    4.20 +apply fastsimp
    4.21 +done
    4.22 +
    4.23  
    4.24  subsection {* size of a datatype value *}
    4.25