author boehmes Wed, 12 May 2010 23:53:52 +0200 changeset 36888 d9b9bec6ff8d parent 36887 3b6a8ecd3c88 child 36889 1355523fb07d
rewrite bool case expressions as if expression
```--- 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