1.1 --- a/src/HOL/Predicate.thy	Thu Nov 19 08:25:51 2009 +0100
     1.2 +++ b/src/HOL/Predicate.thy	Thu Nov 19 08:25:53 2009 +0100
     1.3 @@ -570,6 +570,9 @@
     1.4  definition if_pred :: "bool \<Rightarrow> unit pred" where
     1.5    if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
     1.6  
     1.7 +definition holds :: "unit pred \<Rightarrow> bool" where
     1.8 +  holds_eq: "holds P = eval P ()"
     1.9 +
    1.10  definition not_pred :: "unit pred \<Rightarrow> unit pred" where
    1.11    not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())"
    1.12  
    1.13 @@ -592,7 +595,54 @@
    1.14  lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis"
    1.15    unfolding not_pred_eq
    1.16    by (auto split: split_if_asm elim: botE)
    1.17 +lemma "f () = False \<or> f () = True"
    1.18 +by simp
    1.19  
    1.20 +lemma closure_of_bool_cases:
    1.21 +assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
    1.22 +assumes "f = (%u. True) \<Longrightarrow> P f"
    1.23 +shows "P f"
    1.24 +proof -
    1.25 +  have "f = (%u. False) \<or> f = (%u. True)"
    1.26 +    apply (cases "f ()")
    1.27 +    apply (rule disjI2)
    1.28 +    apply (rule ext)
    1.29 +    apply (simp add: unit_eq)
    1.30 +    apply (rule disjI1)
    1.31 +    apply (rule ext)
    1.32 +    apply (simp add: unit_eq)
    1.33 +    done
    1.34 +  from this prems show ?thesis by blast
    1.35 +qed
    1.36 +
    1.37 +lemma unit_pred_cases:
    1.38 +assumes "P \<bottom>"
    1.39 +assumes "P (single ())"
    1.40 +shows "P Q"
    1.41 +using assms
    1.42 +unfolding bot_pred_def Collect_def empty_def single_def
    1.43 +apply (cases Q)
    1.44 +apply simp
    1.45 +apply (rule_tac f="fun" in closure_of_bool_cases)
    1.46 +apply auto
    1.47 +apply (subgoal_tac "(%x. () = x) = (%x. True)") 
    1.48 +apply auto
    1.49 +done
    1.50 +
    1.51 +lemma holds_if_pred:
    1.52 +  "holds (if_pred b) = b"
    1.53 +unfolding if_pred_eq holds_eq
    1.54 +by (cases b) (auto intro: singleI elim: botE)
    1.55 +
    1.56 +lemma if_pred_holds:
    1.57 +  "if_pred (holds P) = P"
    1.58 +unfolding if_pred_eq holds_eq
    1.59 +by (rule unit_pred_cases) (auto intro: singleI elim: botE)
    1.60 +
    1.61 +lemma is_empty_holds:
    1.62 +  "is_empty P \<longleftrightarrow> \<not> holds P"
    1.63 +unfolding is_empty_def holds_eq
    1.64 +by (rule unit_pred_cases) (auto elim: botE intro: singleI)
    1.65  
    1.66  subsubsection {* Implementation *}
    1.67  
    1.68 @@ -838,7 +888,7 @@
    1.69    bind (infixl "\<guillemotright>=" 70)
    1.70  
    1.71  hide (open) type pred seq
    1.72 -hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
    1.73 +hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds
    1.74    Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
    1.75  
    1.76  end

     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 19 08:25:51 2009 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 19 08:25:53 2009 +0100
     2.3 @@ -2226,12 +2226,12 @@
     2.4              val args = map2 (curry Free) arg_names Ts
     2.5              val predfun = Const (predfun_name_of thy predname full_mode,
     2.6                Ts ---> PredicateCompFuns.mk_predT @{typ unit})
     2.7 -            val rhs = PredicateCompFuns.mk_Eval (list_comb (predfun, args), @{term "Unity"})
     2.8 +            val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
     2.9              val eq_term = HOLogic.mk_Trueprop
    2.10                (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
    2.11              val def = predfun_definition_of thy predname full_mode
    2.12              val tac = fn _ => Simplifier.simp_tac
    2.13 -              (HOL_basic_ss addsimps [def, @{thm eval_pred}]) 1
    2.14 +              (HOL_basic_ss addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1
    2.15              val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac
    2.16            in
    2.17              (pred, result_thms @ [eq])