author boehmes Mon, 07 Nov 2011 17:54:35 +0100 changeset 45392 828e08541cee parent 45391 30f6617c9986 child 45393 13ab80eafd71
replace higher-order matching against schematic theorem with dedicated reconstruction method
 src/HOL/SMT.thy file | annotate | diff | comparison | revisions src/HOL/Tools/SMT/z3_proof_methods.ML file | annotate | diff | comparison | revisions src/HOL/Tools/SMT/z3_proof_reconstruction.ML file | annotate | diff | comparison | revisions
```--- 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]:```
```--- 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```
```--- 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)```