# HG changeset patch
# User haftmann
# Date 1350544777 -7200
# Node ID a81f95693c684a7b3c4d83409f8695f93c15549e
# Parent  2df2786ac7b70f5ed940abed00de2dfd8740ac60
simp results for simplification results of Inf/Sup expressions on bool;
tuned proofs

diff -r 2df2786ac7b7 -r a81f95693c68 src/HOL/Complete_Lattices.thy
--- 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
+
diff -r 2df2786ac7b7 -r a81f95693c68 src/HOL/Fun.thy
--- 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: