simp results for simplification results of Inf/Sup expressions on bool;
authorhaftmann
Thu Oct 18 09:19:37 2012 +0200 (2012-10-18)
changeset 49905a81f95693c68
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
src/HOL/Fun.thy
     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.4  
     1.5  end
     1.6  
     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.24  
    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.34  
    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.39  
    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.51  
    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.72  
    2.73  lemma bij_betw_subset: