--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Apr 21 12:10:52 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Apr 21 12:10:52 2010 +0200
@@ -6,6 +6,14 @@
declare HOL.if_bool_eq_disj[code_pred_inline]
+declare bool_diff_def[code_pred_inline]
+declare inf_bool_eq_raw[code_pred_inline]
+declare less_bool_def_raw[code_pred_inline]
+declare le_bool_def_raw[code_pred_inline]
+
+lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
+by (rule eq_reflection) (auto simp add: expand_fun_eq min_def le_bool_def)
+
setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
section {* Pairs *}
@@ -35,6 +43,10 @@
"(A - B) = (%x. A x \<and> \<not> B x)"
by (auto simp add: mem_def)
+lemma subset_eq[code_pred_inline]:
+ "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
+by (rule eq_reflection) (fastsimp simp add: mem_def)
+
lemma set_equality[code_pred_inline]:
"(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
by (fastsimp simp add: mem_def)