# HG changeset patch
# User boehmes
# Date 1291070469 -3600
# Node ID 59d96f777da3554cd5e8135968335ec3dbf05a33
# Parent  c8494f89690a5e4d395d0a2ec9e54e2beb4a28cc
also support higher-order rules for Z3 proof reconstruction

diff -r c8494f89690a -r 59d96f777da3 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Nov 29 11:39:00 2010 +0100
+++ b/src/HOL/SMT.thy	Mon Nov 29 23:41:09 2010 +0100
@@ -324,6 +324,7 @@
   "(if P then True else False) = P"
   "(if P then False else True) = (\<not>P)"
   "(if \<not>P then x else y) = (if P then y else x)"
+  "f (if P then x else y) = (if P then f x else f y)"
   by auto
 
 lemma [z3_rule]:
diff -r c8494f89690a -r 59d96f777da3 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 29 11:39:00 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 29 23:41:09 2010 +0100
@@ -73,8 +73,13 @@
   |> Option.map (fn inst => Thm.instantiate inst thm)
 
 fun net_instance' f net ct =
-  let fun first_of f xthms ct = get_first (f (maybe_instantiate ct)) xthms 
-  in first_of f (Net.match_term net (Thm.term_of ct)) ct end
+  let
+    val xthms = Net.match_term net (Thm.term_of ct)
+    fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms 
+    fun first_of' f ct =
+      let val thm = Thm.trivial ct
+      in get_first (f (try (fn rule => rule COMP thm))) xthms end
+  in (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end
 val net_instance = net_instance' I