# HG changeset patch
# User bulwahn
# Date 1258615553 -3600
# Node ID f2957bd46fafee16e07b0b406ddaeb6561987a03
# Parent  1344e9bb611e67c5235860017cead2f5d04ea848
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler

diff -r 1344e9bb611e -r f2957bd46faf src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Nov 19 08:25:51 2009 +0100
+++ b/src/HOL/Predicate.thy	Thu Nov 19 08:25:53 2009 +0100
@@ -570,6 +570,9 @@
 definition if_pred :: "bool \<Rightarrow> unit pred" where
   if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
 
+definition holds :: "unit pred \<Rightarrow> bool" where
+  holds_eq: "holds P = eval P ()"
+
 definition not_pred :: "unit pred \<Rightarrow> unit pred" where
   not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())"
 
@@ -592,7 +595,54 @@
 lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   unfolding not_pred_eq
   by (auto split: split_if_asm elim: botE)
+lemma "f () = False \<or> f () = True"
+by simp
 
+lemma closure_of_bool_cases:
+assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
+assumes "f = (%u. True) \<Longrightarrow> P f"
+shows "P f"
+proof -
+  have "f = (%u. False) \<or> f = (%u. True)"
+    apply (cases "f ()")
+    apply (rule disjI2)
+    apply (rule ext)
+    apply (simp add: unit_eq)
+    apply (rule disjI1)
+    apply (rule ext)
+    apply (simp add: unit_eq)
+    done
+  from this prems show ?thesis by blast
+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
+
+lemma holds_if_pred:
+  "holds (if_pred b) = b"
+unfolding if_pred_eq holds_eq
+by (cases b) (auto intro: singleI elim: botE)
+
+lemma if_pred_holds:
+  "if_pred (holds P) = P"
+unfolding if_pred_eq holds_eq
+by (rule unit_pred_cases) (auto intro: singleI elim: botE)
+
+lemma is_empty_holds:
+  "is_empty P \<longleftrightarrow> \<not> holds P"
+unfolding is_empty_def holds_eq
+by (rule unit_pred_cases) (auto elim: botE intro: singleI)
 
 subsubsection {* Implementation *}
 
@@ -838,7 +888,7 @@
   bind (infixl "\<guillemotright>=" 70)
 
 hide (open) type pred seq
-hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
+hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds
   Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
 
 end
diff -r 1344e9bb611e -r f2957bd46faf src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 19 08:25:51 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 19 08:25:53 2009 +0100
@@ -2226,12 +2226,12 @@
             val args = map2 (curry Free) arg_names Ts
             val predfun = Const (predfun_name_of thy predname full_mode,
               Ts ---> PredicateCompFuns.mk_predT @{typ unit})
-            val rhs = PredicateCompFuns.mk_Eval (list_comb (predfun, args), @{term "Unity"})
+            val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
             val eq_term = HOLogic.mk_Trueprop
               (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
             val def = predfun_definition_of thy predname full_mode
             val tac = fn _ => Simplifier.simp_tac
-              (HOL_basic_ss addsimps [def, @{thm eval_pred}]) 1
+              (HOL_basic_ss addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1
             val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac
           in
             (pred, result_thms @ [eq])