--- a/src/HOL/Tools/SMT2/smtlib2_isar.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML Fri Aug 01 14:43:57 2014 +0200
@@ -12,7 +12,7 @@
val postprocess_step_conclusion: term -> theory -> thm list -> term list -> term
val normalizing_prems : Proof.context -> term -> (string * string list) list
val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list ->
- (''a * 'c) list -> 'c list -> 'c -> 'c -> ATP_Problem.atp_formula_role * 'c
+ (''a * 'c) list -> 'c list -> 'c -> 'c -> (ATP_Problem.atp_formula_role * 'c) option
val unskolemize_names: term -> term
end;
@@ -87,14 +87,13 @@
fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts concl_t
t =
(case ss of
- [s] => (Axiom, the (AList.lookup (op =) fact_helper_ts s))
+ [s] => SOME (Axiom, the (AList.lookup (op =) fact_helper_ts s))
| _ =>
if id = conjecture_id then
- (Conjecture, concl_t)
+ SOME (Conjecture, concl_t)
else
- (Hypothesis,
- (case find_index (curry (op =) id) prem_ids of
- ~1 => t
- | i => nth hyp_ts i)))
+ (case find_index (curry (op =) id) prem_ids of
+ ~1 => NONE (* lambda-lifting definition *)
+ | i => SOME (Hypothesis, nth hyp_ts i)))
end;
--- a/src/HOL/Tools/SMT2/verit_isar.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_isar.ML Fri Aug 01 14:43:57 2014 +0200
@@ -30,20 +30,23 @@
fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
let
val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs
- fun standard_step role =
- ((id, []), role, concl', rule,
- map (fn id => (id, [])) prems)
+ fun standard_step role = ((id, []), role, concl', rule, map (fn id => (id, [])) prems)
in
if rule = veriT_input_rule then
- let
- val ss = the_list (AList.lookup (op =) fact_helper_ids (the (Int.fromString id)))
- val name0 = (id ^ "a", ss)
- val (role0, concl0) = distinguish_conjecture_and_hypothesis ss (the (Int.fromString id))
- conjecture_id prem_ids fact_helper_ts hyp_ts concl_t concl ||> unskolemize_names
- in
- [(name0, role0, concl0, rule, []),
- ((id, []), Plain, concl', veriT_rewrite_rule,
- name0 :: normalizing_prems ctxt concl0)] end
+ let val ss = the_list (AList.lookup (op =) fact_helper_ids (the (Int.fromString id))) in
+ (case distinguish_conjecture_and_hypothesis ss (the (Int.fromString id))
+ conjecture_id prem_ids fact_helper_ts hyp_ts concl_t concl of
+ NONE => []
+ | SOME (role0, concl00) =>
+ let
+ val name0 = (id ^ "a", ss)
+ val concl0 = unskolemize_names concl00
+ in
+ [(name0, role0, unskolemize_names concl0, rule, []),
+ ((id, []), Plain, concl', veriT_rewrite_rule,
+ name0 :: normalizing_prems ctxt concl0)]
+ end)
+ end
else if rule = veriT_tmp_ite_elim_rule then
[standard_step Lemma]
else
--- a/src/HOL/Tools/SMT2/z3_new_isar.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Fri Aug 01 14:43:57 2014 +0200
@@ -79,19 +79,17 @@
in
(case rule of
Z3_New_Proof.Asserted =>
- let
- val ss = the_list (AList.lookup (op =) fact_helper_ids id)
- val name0 = (sid ^ "a", ss)
-
- val (role0, concl0) =
- distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts
- hyp_ts concl_t concl
-
- in
- (if role0 = Axiom then []
- else [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]) @
- [((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
- name0 :: normalizing_prems ctxt concl0)]
+ let val ss = the_list (AList.lookup (op =) fact_helper_ids id) in
+ (case distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts
+ hyp_ts concl_t concl of
+ NONE => []
+ | SOME (role0, concl0) =>
+ let val name0 = (sid ^ "a", ss) in
+ (if role0 = Axiom then []
+ else [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]) @
+ [((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
+ name0 :: normalizing_prems ctxt concl0)]
+ end)
end
| Z3_New_Proof.Rewrite => [standard_step Lemma]
| Z3_New_Proof.Rewrite_Star => [standard_step Lemma]