simp results for simplification results of Inf/Sup expressions on bool;
tuned proofs
--- a/src/HOL/Complete_Lattices.thy Thu Oct 18 09:17:00 2012 +0200
+++ b/src/HOL/Complete_Lattices.thy Thu Oct 18 09:19:37 2012 +0200
@@ -549,23 +549,21 @@
end
+lemma not_False_in_image_Ball [simp]:
+ "False \<notin> P ` A \<longleftrightarrow> Ball A P"
+ by auto
+
+lemma True_in_image_Bex [simp]:
+ "True \<in> P ` A \<longleftrightarrow> Bex A P"
+ by auto
+
lemma INF_bool_eq [simp]:
"INFI = Ball"
-proof (rule ext)+
- fix A :: "'a set"
- fix P :: "'a \<Rightarrow> bool"
- show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
- by (auto simp add: INF_def)
-qed
+ by (simp add: fun_eq_iff INF_def)
lemma SUP_bool_eq [simp]:
"SUPR = Bex"
-proof (rule ext)+
- fix A :: "'a set"
- fix P :: "'a \<Rightarrow> bool"
- show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)"
- by (auto simp add: SUP_def)
-qed
+ by (simp add: fun_eq_iff SUP_def)
instance bool :: complete_boolean_algebra proof
qed (auto intro: bool_induct)
@@ -1220,3 +1218,4 @@
-- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
end
+
--- a/src/HOL/Fun.thy Thu Oct 18 09:17:00 2012 +0200
+++ b/src/HOL/Fun.thy Thu Oct 18 09:19:37 2012 +0200
@@ -188,25 +188,30 @@
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
INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
shows "inj_on f (\<Union> i \<in> I. A i)"
-proof(unfold inj_on_def UNION_eq, auto)
- fix i j x y
- assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
- and ***: "f x = f y"
- show "x = y"
- proof-
- {assume "A i \<le> A j"
- with ** have "x \<in> A j" by auto
- with INJ * ** *** have ?thesis
- by(auto simp add: inj_on_def)
- }
- moreover
- {assume "A j \<le> A i"
- with ** have "y \<in> A i" by auto
- with INJ * ** *** have ?thesis
- by(auto simp add: inj_on_def)
- }
- ultimately show ?thesis using CH * by blast
- qed
+proof -
+ {
+ fix i j x y
+ assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
+ and ***: "f x = f y"
+ have "x = y"
+ proof -
+ {
+ assume "A i \<le> A j"
+ with ** have "x \<in> A j" by auto
+ with INJ * ** *** have ?thesis
+ by(auto simp add: inj_on_def)
+ }
+ moreover
+ {
+ assume "A j \<le> A i"
+ with ** have "y \<in> A i" by auto
+ with INJ * ** *** have ?thesis
+ by(auto simp add: inj_on_def)
+ }
+ ultimately show ?thesis using CH * by blast
+ qed
+ }
+ then show ?thesis by (unfold inj_on_def UNION_eq) auto
qed
lemma surj_id: "surj id"
@@ -416,7 +421,7 @@
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
BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
-proof(unfold bij_betw_def, auto simp add: image_def)
+proof (unfold bij_betw_def, auto)
have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
using BIJ bij_betw_def[of f] by auto
thus "inj_on f (\<Union> i \<in> I. A i)"
@@ -430,8 +435,9 @@
fix i x'
assume *: "i \<in> I" "x' \<in> A' i"
hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
- thus "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
- using * by blast
+ then have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
+ using * by blast
+ then show "x' \<in> f ` (\<Union>x\<in>I. A x)" by (simp add: image_def)
qed
lemma bij_betw_subset: