author boehmes Mon Nov 07 17:54:35 2011 +0100 (2011-11-07) 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 | revisions src/HOL/Tools/SMT/z3_proof_methods.ML file | annotate | diff | revisions src/HOL/Tools/SMT/z3_proof_reconstruction.ML file | annotate | diff | revisions
```     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)
```