# HG changeset patch
# User boehmes
# Date 1273701232 -7200
# Node ID d9b9bec6ff8d24d5847db48965af0986b7dbb1d6
# Parent  3b6a8ecd3c88211aa5b4f09c84131aec97eaeb2d
rewrite bool case expressions as if expression

diff -r 3b6a8ecd3c88 -r d9b9bec6ff8d src/HOL/SMT/Tools/smt_normalize.ML
--- a/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:51 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:52 2010 +0200
@@ -4,6 +4,7 @@
 Normalization steps on theorems required by SMT solvers:
   * unfold trivial let expressions,
   * simplify trivial distincts (those with less than three elements),
+  * rewrite bool case expressions as if expressions,
   * replace negative numerals by negated positive numerals,
   * embed natural numbers into integers,
   * add extra rules specifying types and constants which occur frequently,
@@ -88,6 +89,26 @@
 
 
 
+(* rewrite bool case expressions as if expressions *)
+
+local
+  val is_bool_case = (fn
+      Const (@{const_name "bool.bool_case"}, _) $ _ $ _ $ _ => true
+    | _ => false)
+
+  val thms = @{lemma
+    "(case P of True => x | False => y) == (if P then x else y)"
+    "(case P of False => y | True => x) == (if P then x else y)"
+    by (rule eq_reflection, simp)+}
+  val unfold_conv = if_true_conv is_bool_case (More_Conv.rewrs_conv thms)
+in
+fun rewrite_bool_cases ctxt =
+  map ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
+    Conv.fconv_rule (More_Conv.top_conv (K unfold_conv) ctxt))
+end
+
+
+
 (* rewriting of negative integer numerals into positive numerals *)
 
 local
@@ -506,6 +527,7 @@
   thms
   |> trivial_let ctxt
   |> trivial_distinct ctxt
+  |> rewrite_bool_cases ctxt
   |> positive_numerals ctxt
   |> nat_as_int ctxt
   |> add_rules