# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID d39815cdb7ba6230f97316e6091d5d4bc5f3b0d1
# Parent  2df9ed24114fe06139f3a8bbd0a27a0032d53dd4
remove lambda-lifting related assumptions from generated Isar proofs

diff -r 2df9ed24114f -r d39815cdb7ba src/HOL/Tools/SMT2/smtlib2_isar.ML
--- 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;
diff -r 2df9ed24114f -r d39815cdb7ba src/HOL/Tools/SMT2/verit_isar.ML
--- 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
diff -r 2df9ed24114f -r d39815cdb7ba src/HOL/Tools/SMT2/z3_new_isar.ML
--- 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]