# HG changeset patch # User huffman # Date 1291132850 28800 # Node ID 86dff9dfd8069b84dcaf7f974dd4cb06126d1672 # Parent 63276d22ea6028649c7975dfb2ced64f3c2cef89# Parent eeaa59fb5ad82346bdb9e9f88223b52e40080920 merged diff -r 63276d22ea60 -r 86dff9dfd806 src/HOL/SMT.thy --- a/src/HOL/SMT.thy Mon Nov 29 14:37:40 2010 -0800 +++ b/src/HOL/SMT.thy Tue Nov 30 08:00:50 2010 -0800 @@ -324,6 +324,7 @@ "(if P then True else False) = P" "(if P then False else True) = (\P)" "(if \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 63276d22ea60 -r 86dff9dfd806 src/HOL/Tools/SMT/z3_proof_tools.ML --- a/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Nov 29 14:37:40 2010 -0800 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Tue Nov 30 08:00:50 2010 -0800 @@ -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