src/HOL/Tools/SMT/z3_proof_methods.ML
changeset 45392 828e08541cee
parent 45263 93ac73160d78
child 46497 89ccf66aa73d
     1.1 --- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Nov 07 17:24:57 2011 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Nov 07 17:54:35 2011 +0100
     1.3 @@ -7,6 +7,7 @@
     1.4  signature Z3_PROOF_METHODS =
     1.5  sig
     1.6    val prove_injectivity: Proof.context -> cterm -> thm
     1.7 +  val prove_ite: cterm -> thm
     1.8  end
     1.9  
    1.10  structure Z3_Proof_Methods: Z3_PROOF_METHODS =
    1.11 @@ -20,6 +21,22 @@
    1.12  
    1.13  
    1.14  
    1.15 +(* if-then-else *)
    1.16 +
    1.17 +val pull_ite = mk_meta_eq
    1.18 +  @{lemma "f (if P then x else y) = (if P then f x else f y)" by simp}
    1.19 +
    1.20 +fun pull_ites_conv ct =
    1.21 +  (Conv.rewr_conv pull_ite then_conv
    1.22 +   Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct
    1.23 +
    1.24 +val prove_ite =
    1.25 +  Z3_Proof_Tools.by_tac (
    1.26 +    CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
    1.27 +    THEN' Tactic.rtac @{thm refl})
    1.28 +
    1.29 +
    1.30 +
    1.31  (* injectivity *)
    1.32  
    1.33  local