author hoelzl Tue Nov 12 19:28:54 2013 +0100 (2013-11-12) changeset 54413 88a036a95967 parent 54412 900c6d724250 child 54414 72949fae4f81
add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Linear_Algebra.thy file | annotate | diff | revisions src/HOL/NthRoot.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Finite_Set.thy	Tue Nov 12 19:28:53 2013 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Tue Nov 12 19:28:54 2013 +0100
1.3 @@ -518,7 +518,6 @@
1.4    then show ?thesis by simp
1.5  qed
1.6
1.7 -
1.8  subsection {* Class @{text finite}  *}
1.9
1.10  class finite =
1.11 @@ -1333,6 +1332,58 @@
1.12  lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
1.13  by (erule psubsetI, blast)
1.14
1.15 +lemma card_le_inj:
1.16 +  assumes fA: "finite A"
1.17 +    and fB: "finite B"
1.18 +    and c: "card A \<le> card B"
1.19 +  shows "\<exists>f. f ` A \<subseteq> B \<and> inj_on f A"
1.20 +  using fA fB c
1.21 +proof (induct arbitrary: B rule: finite_induct)
1.22 +  case empty
1.23 +  then show ?case by simp
1.24 +next
1.25 +  case (insert x s t)
1.26 +  then show ?case
1.27 +  proof (induct rule: finite_induct[OF "insert.prems"(1)])
1.28 +    case 1
1.29 +    then show ?case by simp
1.30 +  next
1.31 +    case (2 y t)
1.32 +    from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t"
1.33 +      by simp
1.34 +    from "2.prems"(3) [OF "2.hyps"(1) cst]
1.35 +    obtain f where "f ` s \<subseteq> t" "inj_on f s"
1.36 +      by blast
1.37 +    with "2.prems"(2) "2.hyps"(2) show ?case
1.38 +      apply -
1.39 +      apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"])
1.40 +      apply (auto simp add: inj_on_def)
1.41 +      done
1.42 +  qed
1.43 +qed
1.44 +
1.45 +lemma card_subset_eq:
1.46 +  assumes fB: "finite B"
1.47 +    and AB: "A \<subseteq> B"
1.48 +    and c: "card A = card B"
1.49 +  shows "A = B"
1.50 +proof -
1.51 +  from fB AB have fA: "finite A"
1.52 +    by (auto intro: finite_subset)
1.53 +  from fA fB have fBA: "finite (B - A)"
1.54 +    by auto
1.55 +  have e: "A \<inter> (B - A) = {}"
1.56 +    by blast
1.57 +  have eq: "A \<union> (B - A) = B"
1.58 +    using AB by blast
1.59 +  from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0"
1.60 +    by arith
1.61 +  then have "B - A = {}"
1.62 +    unfolding card_eq_0_iff using fA fB by simp
1.63 +  with AB show "A = B"
1.64 +    by blast
1.65 +qed
1.66 +
1.67  lemma insert_partition:
1.68    "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
1.69    \<Longrightarrow> x \<inter> \<Union> F = {}"
1.70 @@ -1359,6 +1410,32 @@
1.71    with fin show "P A" using major by blast
1.72  qed
1.73
1.74 +lemma finite_induct_select[consumes 1, case_names empty select]:
1.75 +  assumes "finite S"
1.76 +  assumes "P {}"
1.77 +  assumes select: "\<And>T. T \<subset> S \<Longrightarrow> P T \<Longrightarrow> \<exists>s\<in>S - T. P (insert s T)"
1.78 +  shows "P S"
1.79 +proof -
1.80 +  have "0 \<le> card S" by simp
1.81 +  then have "\<exists>T \<subseteq> S. card T = card S \<and> P T"
1.82 +  proof (induct rule: dec_induct)
1.83 +    case base with `P {}` show ?case
1.84 +      by (intro exI[of _ "{}"]) auto
1.85 +  next
1.86 +    case (step n)
1.87 +    then obtain T where T: "T \<subseteq> S" "card T = n" "P T"
1.88 +      by auto
1.89 +    with `n < card S` have "T \<subset> S" "P T"
1.90 +      by auto
1.91 +    with select[of T] obtain s where "s \<in> S" "s \<notin> T" "P (insert s T)"
1.92 +      by auto
1.93 +    with step(2) T `finite S` show ?case
1.94 +      by (intro exI[of _ "insert s T"]) (auto dest: finite_subset)
1.95 +  qed
1.96 +  with `finite S` show "P S"
1.97 +    by (auto dest: card_subset_eq)
1.98 +qed
1.99 +
1.100  text{* main cardinality theorem *}
1.101  lemma card_partition [rule_format]:
1.102    "finite C ==>
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Nov 12 19:28:53 2013 +0100
2.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Nov 12 19:28:54 2013 +0100
2.3 @@ -36,34 +36,6 @@
2.4    apply auto
2.5    done
2.6
2.7 -lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y"
2.8 -  using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
2.9 -
2.10 -lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y"
2.11 -  using real_sqrt_le_mono[of "x\<^sup>2" y] by simp
2.12 -
2.13 -lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
2.14 -  using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
2.15 -
2.16 -lemma sqrt_even_pow2:
2.17 -  assumes n: "even n"
2.18 -  shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
2.19 -proof -
2.20 -  from n obtain m where m: "n = 2 * m"
2.21 -    unfolding even_mult_two_ex ..
2.22 -  from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
2.23 -    by (simp only: power_mult[symmetric] mult_commute)
2.24 -  then show ?thesis
2.25 -    using m by simp
2.26 -qed
2.27 -
2.28 -lemma real_div_sqrt: "0 \<le> x \<Longrightarrow> x / sqrt x = sqrt x"
2.29 -  apply (cases "x = 0")
2.30 -  apply simp_all
2.31 -  using sqrt_divide_self_eq[of x]
2.32 -  apply (simp add: inverse_eq_divide field_simps)
2.33 -  done
2.34 -
2.35  text{* Hence derive more interesting properties of the norm. *}
2.36
2.37  lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
2.38 @@ -2406,58 +2378,6 @@
2.39
2.40  text {* Can construct an isomorphism between spaces of same dimension. *}
2.41
2.42 -lemma card_le_inj:
2.43 -  assumes fA: "finite A"
2.44 -    and fB: "finite B"
2.45 -    and c: "card A \<le> card B"
2.46 -  shows "\<exists>f. f ` A \<subseteq> B \<and> inj_on f A"
2.47 -  using fA fB c
2.48 -proof (induct arbitrary: B rule: finite_induct)
2.49 -  case empty
2.50 -  then show ?case by simp
2.51 -next
2.52 -  case (insert x s t)
2.53 -  then show ?case
2.54 -  proof (induct rule: finite_induct[OF "insert.prems"(1)])
2.55 -    case 1
2.56 -    then show ?case by simp
2.57 -  next
2.58 -    case (2 y t)
2.59 -    from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t"
2.60 -      by simp
2.61 -    from "2.prems"(3) [OF "2.hyps"(1) cst]
2.62 -    obtain f where "f ` s \<subseteq> t" "inj_on f s"
2.63 -      by blast
2.64 -    with "2.prems"(2) "2.hyps"(2) show ?case
2.65 -      apply -
2.66 -      apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"])
2.67 -      apply (auto simp add: inj_on_def)
2.68 -      done
2.69 -  qed
2.70 -qed
2.71 -
2.72 -lemma card_subset_eq:
2.73 -  assumes fB: "finite B"
2.74 -    and AB: "A \<subseteq> B"
2.75 -    and c: "card A = card B"
2.76 -  shows "A = B"
2.77 -proof -
2.78 -  from fB AB have fA: "finite A"
2.79 -    by (auto intro: finite_subset)
2.80 -  from fA fB have fBA: "finite (B - A)"
2.81 -    by auto
2.82 -  have e: "A \<inter> (B - A) = {}"
2.83 -    by blast
2.84 -  have eq: "A \<union> (B - A) = B"
2.85 -    using AB by blast
2.86 -  from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0"
2.87 -    by arith
2.88 -  then have "B - A = {}"
2.89 -    unfolding card_eq_0_iff using fA fB by simp
2.90 -  with AB show "A = B"
2.91 -    by blast
2.92 -qed
2.93 -
2.94  lemma subspace_isomorphism:
2.95    fixes S :: "'a::euclidean_space set"
2.96      and T :: "'b::euclidean_space set"
```
```     3.1 --- a/src/HOL/NthRoot.thy	Tue Nov 12 19:28:53 2013 +0100
3.2 +++ b/src/HOL/NthRoot.thy	Tue Nov 12 19:28:54 2013 +0100
3.3 @@ -410,6 +410,27 @@
3.4  lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)"
3.5  unfolding sqrt_def by (rule real_root_eq_iff [OF pos2])
3.6
3.7 +lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y"
3.8 +  using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
3.9 +
3.10 +lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y"
3.11 +  using real_sqrt_le_mono[of "x\<^sup>2" y] by simp
3.12 +
3.13 +lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
3.14 +  using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
3.15 +
3.16 +lemma sqrt_even_pow2:
3.17 +  assumes n: "even n"
3.18 +  shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
3.19 +proof -
3.20 +  from n obtain m where m: "n = 2 * m"
3.21 +    unfolding even_mult_two_ex ..
3.22 +  from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
3.23 +    by (simp only: power_mult[symmetric] mult_commute)
3.24 +  then show ?thesis
3.25 +    using m by simp
3.26 +qed
3.27 +
3.28  lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, unfolded real_sqrt_zero]
3.29  lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, unfolded real_sqrt_zero]
3.30  lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, unfolded real_sqrt_zero]
3.31 @@ -490,6 +511,13 @@
3.32    qed
3.33  qed
3.34
3.35 +lemma real_div_sqrt: "0 \<le> x \<Longrightarrow> x / sqrt x = sqrt x"
3.36 +  apply (cases "x = 0")
3.37 +  apply simp_all
3.38 +  using sqrt_divide_self_eq[of x]
3.39 +  apply (simp add: inverse_eq_divide field_simps)
3.40 +  done
3.41 +
3.42  lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"