author haftmann Thu Oct 18 09:19:37 2012 +0200 (2012-10-18) changeset 49905 a81f95693c68 parent 49904 2df2786ac7b7 child 49906 06a3570b0f0a child 49913 2e7d0655b176
simp results for simplification results of Inf/Sup expressions on bool;
tuned proofs
 src/HOL/Complete_Lattices.thy file | annotate | diff | revisions src/HOL/Fun.thy file | annotate | diff | revisions
1.1 --- a/src/HOL/Complete_Lattices.thy	Thu Oct 18 09:17:00 2012 +0200
1.2 +++ b/src/HOL/Complete_Lattices.thy	Thu Oct 18 09:19:37 2012 +0200
1.3 @@ -549,23 +549,21 @@
1.5  end
1.7 +lemma not_False_in_image_Ball [simp]:
1.8 +  "False \<notin> P ` A \<longleftrightarrow> Ball A P"
1.9 +  by auto
1.10 +
1.11 +lemma True_in_image_Bex [simp]:
1.12 +  "True \<in> P ` A \<longleftrightarrow> Bex A P"
1.13 +  by auto
1.14 +
1.15  lemma INF_bool_eq [simp]:
1.16    "INFI = Ball"
1.17 -proof (rule ext)+
1.18 -  fix A :: "'a set"
1.19 -  fix P :: "'a \<Rightarrow> bool"
1.20 -  show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
1.21 -    by (auto simp add: INF_def)
1.22 -qed
1.23 +  by (simp add: fun_eq_iff INF_def)
1.25  lemma SUP_bool_eq [simp]:
1.26    "SUPR = Bex"
1.27 -proof (rule ext)+
1.28 -  fix A :: "'a set"
1.29 -  fix P :: "'a \<Rightarrow> bool"
1.30 -  show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)"
1.31 -    by (auto simp add: SUP_def)
1.32 -qed
1.33 +  by (simp add: fun_eq_iff SUP_def)
1.35  instance bool :: complete_boolean_algebra proof
1.36  qed (auto intro: bool_induct)
1.37 @@ -1220,3 +1218,4 @@
1.38    -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
1.40  end
1.41 +
2.1 --- a/src/HOL/Fun.thy	Thu Oct 18 09:17:00 2012 +0200
2.2 +++ b/src/HOL/Fun.thy	Thu Oct 18 09:19:37 2012 +0200
2.3 @@ -188,25 +188,30 @@
2.4    assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
2.5           INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
2.6    shows "inj_on f (\<Union> i \<in> I. A i)"
2.7 -proof(unfold inj_on_def UNION_eq, auto)
2.8 -  fix i j x y
2.9 -  assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
2.10 -         and ***: "f x = f y"
2.11 -  show "x = y"
2.12 -  proof-
2.13 -    {assume "A i \<le> A j"
2.14 -     with ** have "x \<in> A j" by auto
2.15 -     with INJ * ** *** have ?thesis
2.16 -     by(auto simp add: inj_on_def)
2.17 -    }
2.18 -    moreover
2.19 -    {assume "A j \<le> A i"
2.20 -     with ** have "y \<in> A i" by auto
2.21 -     with INJ * ** *** have ?thesis
2.22 -     by(auto simp add: inj_on_def)
2.23 -    }
2.24 -    ultimately show ?thesis using  CH * by blast
2.25 -  qed
2.26 +proof -
2.27 +  {
2.28 +    fix i j x y
2.29 +    assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
2.30 +      and ***: "f x = f y"
2.31 +    have "x = y"
2.32 +    proof -
2.33 +      {
2.34 +        assume "A i \<le> A j"
2.35 +        with ** have "x \<in> A j" by auto
2.36 +        with INJ * ** *** have ?thesis
2.37 +        by(auto simp add: inj_on_def)
2.38 +      }
2.39 +      moreover
2.40 +      {
2.41 +        assume "A j \<le> A i"
2.42 +        with ** have "y \<in> A i" by auto
2.43 +        with INJ * ** *** have ?thesis
2.44 +        by(auto simp add: inj_on_def)
2.45 +      }
2.46 +      ultimately show ?thesis using CH * by blast
2.47 +    qed
2.48 +  }
2.49 +  then show ?thesis by (unfold inj_on_def UNION_eq) auto
2.50  qed
2.52  lemma surj_id: "surj id"
2.53 @@ -416,7 +421,7 @@
2.54    assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
2.55           BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
2.56    shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
2.57 -proof(unfold bij_betw_def, auto simp add: image_def)
2.58 +proof (unfold bij_betw_def, auto)
2.59    have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
2.60    using BIJ bij_betw_def[of f] by auto
2.61    thus "inj_on f (\<Union> i \<in> I. A i)"
2.62 @@ -430,8 +435,9 @@
2.63    fix i x'
2.64    assume *: "i \<in> I" "x' \<in> A' i"
2.65    hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
2.66 -  thus "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
2.67 -  using * by blast
2.68 +  then have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
2.69 +    using * by blast
2.70 +  then show "x' \<in> f ` (\<Union>x\<in>I. A x)" by (simp add: image_def)
2.71  qed
2.73  lemma bij_betw_subset: