1.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri May 13 16:03:03 2011 +0200
1.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri May 13 22:55:00 2011 +0200
1.3 @@ -97,9 +97,14 @@
1.4 val rewr_if =
1.5 @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}
1.6 in
1.7 -val simp_fast_tac =
1.8 +
1.9 +fun HOL_fast_tac ctxt =
1.10 + Classical.fast_tac (put_claset HOL_cs ctxt)
1.11 +
1.12 +fun simp_fast_tac ctxt =
1.13 Simplifier.simp_tac (HOL_ss addsimps [rewr_if])
1.14 - THEN_ALL_NEW Classical.fast_tac HOL_cs
1.15 + THEN_ALL_NEW HOL_fast_tac ctxt
1.16 +
1.17 end
1.18
1.19
1.20 @@ -300,7 +305,7 @@
1.21
1.22 (* distributivity of | over & *)
1.23 fun distributivity ctxt = Thm o try_apply ctxt [] [
1.24 - named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
1.25 + named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
1.26 (* FIXME: not very well tested *)
1.27
1.28
1.29 @@ -356,7 +361,7 @@
1.30 fun def_axiom ctxt = Thm o try_apply ctxt [] [
1.31 named ctxt "conj/disj/distinct" prove_def_axiom,
1.32 Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
1.33 - named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
1.34 + named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
1.35 end
1.36
1.37
1.38 @@ -417,7 +422,7 @@
1.39 fun prove_nnf ctxt = try_apply ctxt [] [
1.40 named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
1.41 Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
1.42 - named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
1.43 + named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
1.44 in
1.45 fun nnf ctxt vars ps ct =
1.46 (case SMT_Utils.term_of ct of
1.47 @@ -552,13 +557,13 @@
1.48
1.49 (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
1.50 fun pull_quant ctxt = Thm o try_apply ctxt [] [
1.51 - named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
1.52 + named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
1.53 (* FIXME: not very well tested *)
1.54
1.55
1.56 (* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
1.57 fun push_quant ctxt = Thm o try_apply ctxt [] [
1.58 - named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
1.59 + named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
1.60 (* FIXME: not very well tested *)
1.61
1.62
1.63 @@ -582,7 +587,7 @@
1.64
1.65 (* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
1.66 fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
1.67 - named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
1.68 + named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
1.69 (* FIXME: not very well tested *)
1.70
1.71
1.72 @@ -694,18 +699,18 @@
1.73 Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
1.74 Z3_Proof_Tools.by_tac (
1.75 NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
1.76 - THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
1.77 + THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
1.78 Z3_Proof_Tools.by_abstraction (false, true) ctxt [] (fn ctxt' =>
1.79 Z3_Proof_Tools.by_tac (
1.80 NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
1.81 THEN_ALL_NEW (
1.82 - NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
1.83 + NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
1.84 ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
1.85 Z3_Proof_Tools.by_abstraction (true, true) ctxt [] (fn ctxt' =>
1.86 Z3_Proof_Tools.by_tac (
1.87 NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
1.88 THEN_ALL_NEW (
1.89 - NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
1.90 + NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
1.91 ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
1.92 named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt)]) ct))
1.93