# HG changeset patch
# User bulwahn
# Date 1285246214 -7200
# Node ID 2a35950ec49523890f33320eb15170b31cee9bad
# Parent  7186d338f2e12e8ab439d3045c4f4b12532c3024
handling equivalences smarter in the predicate compiler

diff -r 7186d338f2e1 -r 2a35950ec495 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Sep 23 14:50:14 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Sep 23 14:50:14 2010 +0200
@@ -14,6 +14,10 @@
 lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
 by (rule eq_reflection) (auto simp add: fun_eq_iff min_def le_bool_def)
 
+lemma [code_pred_inline]: 
+  "((A::bool) ~= (B::bool)) = ((A & ~ B) | (B & ~ A))"
+by fast
+
 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
 
 section {* Pairs *}
diff -r 7186d338f2e1 -r 2a35950ec495 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Thu Sep 23 14:50:14 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Thu Sep 23 14:50:14 2010 +0200
@@ -36,6 +36,21 @@
 quickcheck[generator=predicate_compile_wo_ff]
 oops
 
+section {* Equivalences *}
+
+inductive is_ten :: "nat => bool"
+where
+  "is_ten 10"
+
+inductive is_eleven :: "nat => bool"
+where
+  "is_eleven 11"
+
+lemma
+  "is_ten x = is_eleven x"
+quickcheck[generator = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample]
+oops
+
 section {* Context Free Grammar *}
 
 datatype alphabet = a | b