# 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 \ unit pred" where if_pred_eq: "if_pred b = (if b then single () else \)" +definition holds :: "unit pred \ bool" where + holds_eq: "holds P = eval P ()" + definition not_pred :: "unit pred \ unit pred" where not_pred_eq: "not_pred P = (if eval P () then \ else single ())" @@ -592,7 +595,54 @@ lemma not_predE': "eval (not_pred P) x \ (\ eval P x \ thesis) \ thesis" unfolding not_pred_eq by (auto split: split_if_asm elim: botE) +lemma "f () = False \ f () = True" +by simp +lemma closure_of_bool_cases: +assumes "(f :: unit \ bool) = (%u. False) \ P f" +assumes "f = (%u. True) \ P f" +shows "P f" +proof - + have "f = (%u. False) \ 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 \" +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 \ \ 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 "\=" 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])