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