# HG changeset patch
# User haftmann
# Date 1311961675 -7200
# Node ID b5e7594061ce73fbc64621b9a063bb74817c470e
# Parent  a9fcbafdf208f3f6b32a9823abb20d12c8f11b27
tuned proofs

diff -r a9fcbafdf208 -r b5e7594061ce src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Jul 28 16:56:14 2011 +0200
+++ b/src/HOL/Predicate.thy	Fri Jul 29 19:47:55 2011 +0200
@@ -741,11 +741,12 @@
 by simp
 
 lemma closure_of_bool_cases [no_atp]:
-assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
-assumes "f = (%u. True) \<Longrightarrow> P f"
-shows "P f"
+  fixes f :: "unit \<Rightarrow> bool"
+  assumes "f = (\<lambda>u. False) \<Longrightarrow> P f"
+  assumes "f = (\<lambda>u. True) \<Longrightarrow> P f"
+  shows "P f"
 proof -
-  have "f = (%u. False) \<or> f = (%u. True)"
+  have "f = (\<lambda>u. False) \<or> f = (\<lambda>u. True)"
     apply (cases "f ()")
     apply (rule disjI2)
     apply (rule ext)
@@ -758,19 +759,18 @@
 qed
 
 lemma unit_pred_cases:
-assumes "P \<bottom>"
-assumes "P (single ())"
-shows "P Q"
-using assms
-unfolding bot_pred_def Collect_def empty_def single_def
-apply (cases Q)
-apply simp
-apply (rule_tac f="fun" in closure_of_bool_cases)
-apply auto
-apply (subgoal_tac "(%x. () = x) = (%x. True)") 
-apply auto
-done
-
+  assumes "P \<bottom>"
+  assumes "P (single ())"
+  shows "P Q"
+using assms unfolding bot_pred_def Collect_def empty_def single_def proof (cases Q)
+  fix f
+  assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))"
+  then have "P (Pred f)" 
+    by (cases _ f rule: closure_of_bool_cases) simp_all
+  moreover assume "Q = Pred f"
+  ultimately show "P Q" by simp
+qed
+  
 lemma holds_if_pred:
   "holds (if_pred b) = b"
 unfolding if_pred_eq holds_eq