--- a/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Mar 13 13:18:14 2014 +0100
@@ -1,17 +1,17 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof_replay.ML
+(* Title: HOL/Tools/SMT2/z3_new_replay.ML
Author: Sascha Boehme, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Z3 proof replay.
*)
-signature Z3_NEW_PROOF_REPLAY =
+signature Z3_NEW_REPLAY =
sig
val replay: Proof.context -> SMT2_Translate.replay_data -> string list ->
(int list * Z3_New_Proof.z3_step list) * thm
end
-structure Z3_New_Proof_Replay: Z3_NEW_PROOF_REPLAY =
+structure Z3_New_Replay: Z3_NEW_REPLAY =
struct
fun params_of t = Term.strip_qnt_vars @{const_name all} t
@@ -21,7 +21,7 @@
val maxidx = Thm.maxidx_of thm + 1
val vs = params_of (Thm.prop_of thm)
val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs
- in Drule.forall_elim_list (map (SMT2_Utils.certify ctxt) vars) thm end
+ in Drule.forall_elim_list (map (SMT2_Util.certify ctxt) vars) thm end
fun add_paramTs names t =
fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (params_of t)
@@ -29,7 +29,7 @@
fun new_fixes ctxt nTs =
let
val (ns, ctxt') = Variable.variant_fixes (replicate (length nTs) "") ctxt
- fun mk (n, T) n' = (n, SMT2_Utils.certify ctxt' (Free (n', T)))
+ fun mk (n, T) n' = (n, SMT2_Util.certify ctxt' (Free (n', T)))
in (ctxt', Symtab.make (map2 mk nTs ns)) end
fun forall_elim_term ct (Const (@{const_name all}, _) $ (a as Abs _)) =
@@ -56,12 +56,12 @@
fun replay_thm ctxt assumed nthms
(Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) =
- if Z3_New_Proof_Methods.is_assumption rule then
+ if Z3_New_Replay_Methods.is_assumption rule then
(case Inttab.lookup assumed id of
SOME (_, thm) => thm
- | NONE => Thm.assume (SMT2_Utils.certify ctxt concl))
+ | NONE => Thm.assume (SMT2_Util.certify ctxt concl))
else
- under_fixes (Z3_New_Proof_Methods.method_for rule) ctxt
+ under_fixes (Z3_New_Replay_Methods.method_for rule) ctxt
(if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl
fun replay_step ctxt assumed (step as Z3_New_Proof.Z3_Step {id, prems, fixes, ...}) proofs =
@@ -77,26 +77,26 @@
| rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
- remove_fun_app, Z3_New_Proof_Literals.rewrite_true]
+ remove_fun_app, Z3_New_Replay_Literals.rewrite_true]
fun rewrite _ [] = I
| rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
fun lookup_assm assms_net ct =
- Z3_New_Proof_Tools.net_instances assms_net ct
+ Z3_New_Replay_Util.net_instances assms_net ct
|> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
in
fun add_asserted outer_ctxt rewrite_rules assms steps ctxt =
let
- val eqs = map (rewrite ctxt [Z3_New_Proof_Literals.rewrite_true]) rewrite_rules
+ val eqs = map (rewrite ctxt [Z3_New_Replay_Literals.rewrite_true]) rewrite_rules
val eqs' = union Thm.eq_thm eqs prep_rules
val assms_net =
assms
|> map (apsnd (rewrite ctxt eqs'))
|> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
- |> Z3_New_Proof_Tools.thm_net_of snd
+ |> Z3_New_Replay_Util.thm_net_of snd
fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
@@ -117,9 +117,9 @@
fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...})
(cx as ((is, thms), (ctxt, ptab))) =
- if Z3_New_Proof_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
+ if Z3_New_Replay_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
let
- val ct = SMT2_Utils.certify ctxt concl
+ val ct = SMT2_Util.certify ctxt concl
val thm1 =
Thm.trivial ct
|> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
@@ -154,7 +154,7 @@
end
fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
- @{thm reflexive}, Z3_New_Proof_Literals.true_thm]
+ @{thm reflexive}, Z3_New_Replay_Literals.true_thm]
val intro_def_rules = @{lemma
"(~ P | P) & (P | ~ P)"
@@ -181,7 +181,7 @@
({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output =
let
val (steps, ctxt1) = Z3_New_Proof.parse typs terms output ctxt
- val ctxt2 = put_simpset (Z3_New_Proof_Tools.make_simpset ctxt1 []) ctxt1
+ val ctxt2 = put_simpset (Z3_New_Replay_Util.make_simpset ctxt1 []) ctxt1
val ((is, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
val proofs = fold (replay_step ctxt3 assumed) steps assumed
val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps