--- a/src/HOL/Tools/SMT2/z3_new_proof.ML Wed Jun 11 19:15:54 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_proof.ML Wed Jun 11 19:15:55 2014 +0200
@@ -15,6 +15,7 @@
Iff_True | Iff_False | Commutativity | Def_Axiom | Intro_Def | Apply_Def |
Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize |
Modus_Ponens_Oeq | Th_Lemma of string
+ val is_assumption: z3_rule -> bool
val string_of_rule: z3_rule -> string
(*proofs*)
@@ -113,6 +114,13 @@
("sk", Skolemize),
("mp~", Modus_Ponens_Oeq)]
+fun is_assumption Asserted = true
+ | is_assumption Goal = true
+ | is_assumption Hypothesis = true
+ | is_assumption Intro_Def = true
+ | is_assumption Skolemize = true
+ | is_assumption _ = false
+
fun rule_of_string name =
(case Symtab.lookup rule_names name of
SOME rule => rule
--- a/src/HOL/Tools/SMT2/z3_new_replay.ML Wed Jun 11 19:15:54 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Wed Jun 11 19:15:55 2014 +0200
@@ -58,7 +58,7 @@
fun replay_thm ctxt assumed nthms
(Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) =
- if Z3_New_Replay_Methods.is_assumption rule then
+ if Z3_New_Proof.is_assumption rule then
(case Inttab.lookup assumed id of
SOME (_, thm) => thm
| NONE => Thm.assume (SMT2_Util.certify ctxt concl))
@@ -115,7 +115,7 @@
fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...})
(cx as ((iidths, thms), (ctxt, ptab))) =
- if Z3_New_Replay_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
+ if Z3_New_Proof.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
let
val ct = SMT2_Util.certify ctxt concl
val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML Wed Jun 11 19:15:54 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML Wed Jun 11 19:15:55 2014 +0200
@@ -49,7 +49,6 @@
val nnf_neg: z3_method
val mp_oeq: z3_method
val th_lemma: string -> z3_method
- val is_assumption: Z3_New_Proof.z3_rule -> bool
val method_for: Z3_New_Proof.z3_rule -> z3_method
end
@@ -646,13 +645,6 @@
(* mapping of rules to methods *)
-fun is_assumption Z3_New_Proof.Asserted = true
- | is_assumption Z3_New_Proof.Goal = true
- | is_assumption Z3_New_Proof.Hypothesis = true
- | is_assumption Z3_New_Proof.Intro_Def = true
- | is_assumption Z3_New_Proof.Skolemize = true
- | is_assumption _ = false
-
fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
fun assumed rule ctxt = replay_error ctxt "Assumed" rule