# HG changeset patch
# User bulwahn
# Date 1271844652 -7200
# Node ID 6e969ce3dfcc5f508a7b20e34e797f4feb244474
# Parent  beba03215d8fe8c1e1e16098e967f360f19e6eb3
added further inlining of boolean constants to the predicate compiler

diff -r beba03215d8f -r 6e969ce3dfcc src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- 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)
diff -r beba03215d8f -r 6e969ce3dfcc src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 21 12:10:52 2010 +0200
@@ -1392,6 +1392,20 @@
 values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
 values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}"
 
+subsection {* minus on bool *}
+
+inductive All :: "nat => bool"
+where
+  "All x"
+
+inductive None :: "nat => bool"
+
+definition "test_minus_bool x = (None x - All x)"
+
+code_pred [inductify] test_minus_bool .
+thm test_minus_bool.equation
+
+values "{x. test_minus_bool x}"