--- 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 *}
--- 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