1.1 --- a/src/HOL/Predicate.thy	Thu Jul 28 16:56:14 2011 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Fri Jul 29 19:47:55 2011 +0200
     1.3 @@ -741,11 +741,12 @@
     1.4  by simp
     1.5  
     1.6  lemma closure_of_bool_cases [no_atp]:
     1.7 -assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
     1.8 -assumes "f = (%u. True) \<Longrightarrow> P f"
     1.9 -shows "P f"
    1.10 +  fixes f :: "unit \<Rightarrow> bool"
    1.11 +  assumes "f = (\<lambda>u. False) \<Longrightarrow> P f"
    1.12 +  assumes "f = (\<lambda>u. True) \<Longrightarrow> P f"
    1.13 +  shows "P f"
    1.14  proof -
    1.15 -  have "f = (%u. False) \<or> f = (%u. True)"
    1.16 +  have "f = (\<lambda>u. False) \<or> f = (\<lambda>u. True)"
    1.17      apply (cases "f ()")
    1.18      apply (rule disjI2)
    1.19      apply (rule ext)
    1.20 @@ -758,19 +759,18 @@
    1.21  qed
    1.22  
    1.23  lemma unit_pred_cases:
    1.24 -assumes "P \<bottom>"
    1.25 -assumes "P (single ())"
    1.26 -shows "P Q"
    1.27 -using assms
    1.28 -unfolding bot_pred_def Collect_def empty_def single_def
    1.29 -apply (cases Q)
    1.30 -apply simp
    1.31 -apply (rule_tac f="fun" in closure_of_bool_cases)
    1.32 -apply auto
    1.33 -apply (subgoal_tac "(%x. () = x) = (%x. True)") 
    1.34 -apply auto
    1.35 -done
    1.36 -
    1.37 +  assumes "P \<bottom>"
    1.38 +  assumes "P (single ())"
    1.39 +  shows "P Q"
    1.40 +using assms unfolding bot_pred_def Collect_def empty_def single_def proof (cases Q)
    1.41 +  fix f
    1.42 +  assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))"
    1.43 +  then have "P (Pred f)" 
    1.44 +    by (cases _ f rule: closure_of_bool_cases) simp_all
    1.45 +  moreover assume "Q = Pred f"
    1.46 +  ultimately show "P Q" by simp
    1.47 +qed
    1.48 +  
    1.49  lemma holds_if_pred:
    1.50    "holds (if_pred b) = b"
    1.51  unfolding if_pred_eq holds_eq