replace higher-order matching against schematic theorem with dedicated reconstruction method
authorboehmes
Mon Nov 07 17:54:35 2011 +0100 (2011-11-07)
changeset 45392828e08541cee
parent 45391 30f6617c9986
child 45393 13ab80eafd71
replace higher-order matching against schematic theorem with dedicated reconstruction method
src/HOL/SMT.thy
src/HOL/Tools/SMT/z3_proof_methods.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
     1.1 --- a/src/HOL/SMT.thy	Mon Nov 07 17:24:57 2011 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Nov 07 17:54:35 2011 +0100
     1.3 @@ -393,7 +393,6 @@
     1.4    "(if P then x = y else x = z) = (x = (if P then y else z))"
     1.5    "(if P then x = y else y = z) = (y = (if P then x else z))"
     1.6    "(if P then x = y else z = y) = (y = (if P then x else z))"
     1.7 -  "f (if P then x else y) = (if P then f x else f y)"
     1.8    by auto
     1.9  
    1.10  lemma [z3_rule]:
     2.1 --- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Nov 07 17:24:57 2011 +0100
     2.2 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Nov 07 17:54:35 2011 +0100
     2.3 @@ -7,6 +7,7 @@
     2.4  signature Z3_PROOF_METHODS =
     2.5  sig
     2.6    val prove_injectivity: Proof.context -> cterm -> thm
     2.7 +  val prove_ite: cterm -> thm
     2.8  end
     2.9  
    2.10  structure Z3_Proof_Methods: Z3_PROOF_METHODS =
    2.11 @@ -20,6 +21,22 @@
    2.12  
    2.13  
    2.14  
    2.15 +(* if-then-else *)
    2.16 +
    2.17 +val pull_ite = mk_meta_eq
    2.18 +  @{lemma "f (if P then x else y) = (if P then f x else f y)" by simp}
    2.19 +
    2.20 +fun pull_ites_conv ct =
    2.21 +  (Conv.rewr_conv pull_ite then_conv
    2.22 +   Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct
    2.23 +
    2.24 +val prove_ite =
    2.25 +  Z3_Proof_Tools.by_tac (
    2.26 +    CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
    2.27 +    THEN' Tactic.rtac @{thm refl})
    2.28 +
    2.29 +
    2.30 +
    2.31  (* injectivity *)
    2.32  
    2.33  local
     3.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 07 17:24:57 2011 +0100
     3.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 07 17:54:35 2011 +0100
     3.3 @@ -715,6 +715,7 @@
     3.4  fun rewrite simpset ths ct ctxt =
     3.5    apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [
     3.6      named ctxt "conj/disj/distinct" prove_conj_disj_eq,
     3.7 +    named ctxt "pull-ite" Z3_Proof_Methods.prove_ite,
     3.8      Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
     3.9        Z3_Proof_Tools.by_tac (
    3.10          NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)