# HG changeset patch
# User boehmes
# Date 1320684875 -3600
# Node ID 828e08541cee4b43cd470d72316c50b7d322ba5a
# Parent  30f6617c9986f60313d1cc02187e96df6c8202c6
replace higher-order matching against schematic theorem with dedicated reconstruction method

diff -r 30f6617c9986 -r 828e08541cee src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Nov 07 17:24:57 2011 +0100
+++ b/src/HOL/SMT.thy	Mon Nov 07 17:54:35 2011 +0100
@@ -393,7 +393,6 @@
   "(if P then x = y else x = z) = (x = (if P then y else z))"
   "(if P then x = y else y = z) = (y = (if P then x else z))"
   "(if P then x = y else z = y) = (y = (if P then x else z))"
-  "f (if P then x else y) = (if P then f x else f y)"
   by auto
 
 lemma [z3_rule]:
diff -r 30f6617c9986 -r 828e08541cee src/HOL/Tools/SMT/z3_proof_methods.ML
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Nov 07 17:24:57 2011 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Nov 07 17:54:35 2011 +0100
@@ -7,6 +7,7 @@
 signature Z3_PROOF_METHODS =
 sig
   val prove_injectivity: Proof.context -> cterm -> thm
+  val prove_ite: cterm -> thm
 end
 
 structure Z3_Proof_Methods: Z3_PROOF_METHODS =
@@ -20,6 +21,22 @@
 
 
 
+(* if-then-else *)
+
+val pull_ite = mk_meta_eq
+  @{lemma "f (if P then x else y) = (if P then f x else f y)" by simp}
+
+fun pull_ites_conv ct =
+  (Conv.rewr_conv pull_ite then_conv
+   Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct
+
+val prove_ite =
+  Z3_Proof_Tools.by_tac (
+    CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
+    THEN' Tactic.rtac @{thm refl})
+
+
+
 (* injectivity *)
 
 local
diff -r 30f6617c9986 -r 828e08541cee src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 07 17:24:57 2011 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 07 17:54:35 2011 +0100
@@ -715,6 +715,7 @@
 fun rewrite simpset ths ct ctxt =
   apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [
     named ctxt "conj/disj/distinct" prove_conj_disj_eq,
+    named ctxt "pull-ite" Z3_Proof_Methods.prove_ite,
     Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
       Z3_Proof_Tools.by_tac (
         NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)