Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.

--- a/src/HOL/ATP.thy	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/ATP.thy	Wed Jul 30 14:03:13 2014 +0200
@@ -6,7 +6,7 @@
 header {* Automatic Theorem Provers (ATPs) *}
 
 theory ATP
-imports Meson Hilbert_Choice
+imports Meson
 begin
 
 subsection {* ATP problems and proofs *}

--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -90,18 +90,17 @@
 
   val skip_term: string list -> string * string list
   val parse_thf0_formula :string list ->
-      ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
-       'c) ATP_Problem.atp_formula *
-      string list
-  val dummy_atype :  string ATP_Problem.atp_type
-  val role_of_tptp_string:  string -> ATP_Problem.atp_formula_role
+    ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula *
+    string list
+  val dummy_atype : string ATP_Problem.atp_type
+  val role_of_tptp_string: string -> ATP_Problem.atp_formula_role
   val parse_line: string -> ('a * string ATP_Problem.atp_problem_line list) list ->
-              string list -> ((string * string list) * ATP_Problem.atp_formula_role *
-               (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
-                'c) ATP_Problem.atp_formula
-               * string * (string * 'd list) list) list * string list
+    string list -> ((string * string list) * ATP_Problem.atp_formula_role *
+    (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
+      'c) ATP_Problem.atp_formula
+    * string * (string * 'd list) list) list * string list
   val core_inference :   'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
-              ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
+      ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
   val vampire_step_name_ord : (string * 'a) * (string * 'a) -> order
   val core_of_agsyhol_proof :  string -> string list option
 end;
@@ -478,8 +477,8 @@
   [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
    tptp_equal, tptp_app]
 
-fun parse_one_in_list list =
-  foldl1 (op ||) (map Scan.this_string list)
+fun parse_one_in_list xs =
+  foldl1 (op ||) (map Scan.this_string xs)
 
 fun parse_binary_op x =
   (parse_one_in_list tptp_binary_ops

--- a/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -30,7 +30,7 @@
   ((Symbol.scan_ascii_id || ($$ "$" |-- Symbol.scan_ascii_id))
   -- Scan.option ( $$ "(" |-- Scan.option (Symbol.scan_ascii_id --| $$ ",")
   -- ((Scan.option (($$ "[" |-- (Scan.option ((scan_general_id
-         -- Scan.repeat ($$ "," |-- scan_general_id)) >> uncurry cons) --| $$ "]"))
+         -- Scan.repeat ($$ "," |-- scan_general_id)) >> (op ::)) --| $$ "]"))
          || (skip_term >> K "") >> (fn x => SOME [x]))
        >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")"))) x
 
@@ -39,12 +39,12 @@
 
 fun parse_prems x =
   (($$ "[" |-- parse_prem -- Scan.repeat ($$ "," |-- parse_prem) --| $$ "]")
-     >> uncurry cons) x
+     >> (op ::)) x
 
 fun parse_tstp_satallax_extra_arguments x =
   ($$ "," |-- scan_general_id -- (($$ "(" |-- Symbol.scan_ascii_id --| $$ "," )
   -- ($$ "[" |-- Scan.option ((parse_satallax_tstp_information
-  -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> uncurry cons)
+  -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> (op ::))
   --| $$ "]") --
   (Scan.optional ($$ "," |-- parse_prems) [] -- Scan.optional ($$ "," |-- parse_prems) []
     >> (fn (x, []) => x | (_, x) => x))
@@ -58,7 +58,6 @@
   || (Scan.this_string "tab_inh" |-- skip_term --| $$ ".")
      >> K dummy_satallax_step) x
 
-
 datatype satallax_step = Satallax_Step of {
   id: string,
   role: string,
@@ -106,19 +105,23 @@
   end
 
 fun create_grouped_goal_assumption rule new_goals generated_assumptions =
-  if length new_goals = length generated_assumptions then
-    new_goals ~~ (map single generated_assumptions)
-  else if 2 * length new_goals = length generated_assumptions then
-    let
-      fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) =
-          (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions
-        | group_by_pair [] [] = []
-    in
-      group_by_pair new_goals generated_assumptions
-    end
-  else
-    raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.")
-
+  let
+    val number_of_new_goals = length new_goals
+    val number_of_new_assms = length generated_assumptions
+  in
+    if number_of_new_goals = number_of_new_assms then
+      new_goals ~~ (map single generated_assumptions)
+    else if 2 * number_of_new_goals = number_of_new_assms then
+      let
+        fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) =
+            (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions
+          | group_by_pair [] [] = []
+      in
+        group_by_pair new_goals generated_assumptions
+      end
+    else
+      raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.")
+  end
 fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) =
     let
       val (used_assumptions, new_goals, generated_assumptions) = seperate_dependices used_rules
@@ -173,9 +176,9 @@
       | SOME (_, th) =>
         let
           val simplified_ths_with_inlined_assumption =
-              (case List.partition (curry tptp_term_equal th o remove_not_not) ths of
-                ([], ths) => ATerm ((tptp_not, [dummy_atype]), [th]) :: ths
-              | (_, _) => [])
+            (case List.partition (curry tptp_term_equal th o remove_not_not) ths of
+              ([], ths) => ATerm ((tptp_not, [dummy_atype]), [th]) :: ths
+            | (_, _) => [])
         in
           find_assumptions_to_inline simplified_ths_with_inlined_assumption assms to_inline no_inline
         end))
@@ -190,7 +193,6 @@
     | ATerm (("~", _ ), [ATerm (("$true", _), _)]) => a
     | _ => ATerm ((tptp_or, [dummy_atype]), [a, b]))) l)
 
-
 fun get_conclusion (Satallax_Step {theorem = AAtom theorem, ...}) = theorem
 
 fun add_assumption new_used_assumptions ((Satallax_Step {id, role, theorem, assumptions,
@@ -208,7 +210,7 @@
     fun inline_in_step (Linear_Part {node as Satallax_Step {generated_goal_assumptions,
           used_assumptions, rule, ...}, succs}) =
         if generated_goal_assumptions = [] then
-            Linear_Part {node = node, succs = []}
+          Linear_Part {node = node, succs = []}
         else
           let
             (*one singel goal is created, two hypothesis can be created, for the "and" rule:
@@ -230,8 +232,8 @@
     fun inline_contradictory_assumptions (Linear_Part {node as Satallax_Step{id, theorem, ...},
        succs}) (to_inline, no_inline) =
       let
-        val (succs, inliner) = fold_map inline_contradictory_assumptions
-                                        succs (to_inline, (id, theorem) :: no_inline)
+        val (succs, inliner) = fold_map inline_contradictory_assumptions succs 
+          (to_inline, (id, theorem) :: no_inline)
       in
         (Linear_Part {node = node, succs = succs}, inliner)
       end
@@ -239,8 +241,8 @@
         theorem = AAtom theorem, assumptions, rule, generated_goal_assumptions,
         used_assumptions, detailed_eigen}, deps}) (to_inline, no_inline) =
       let
-        val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions
-                                                        deps (to_inline, no_inline)
+        val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions deps 
+          (to_inline, no_inline)
         val to_inline'' =
           map (fn s => (s, get_conclusion (find_proof_step hypotheses_step s)))
             (List.filter (fn s => nth_string s 0 = "h")
@@ -292,16 +294,16 @@
   end
 
 val satallax_known_theorems = ["eq_ind", "eq_trans2", "eq_trans3", "eq_neg_neg_id", "eq_true",
-    "eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq",
-    "eq_forall_nexists", "eq_exists_nforall", "eq_leib1", "eq_leib2", "eq_leib3", "eq_leib4",
-    "eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"]
+  "eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq",
+  "eq_forall_nexists", "eq_exists_nforall", "eq_leib1", "eq_leib2", "eq_leib3", "eq_leib4",
+  "eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"]
 val is_special_satallax_rule = member (op =) satallax_known_theorems
 
 fun terms_to_upper_case var (AAbs (((var', ty), b), ts)) =
-     let
-       val bdy = terms_to_upper_case var b
-       val ts' = map (terms_to_upper_case var) ts
-     in
+    let
+      val bdy = terms_to_upper_case var b
+      val ts' = map (terms_to_upper_case var) ts
+    in
       AAbs (((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'), ty),
         bdy), ts')
     end
@@ -364,7 +366,7 @@
 fun remove_unused_dependency steps =
   let
     fun find_all_ids [] = []
-     | find_all_ids (((id, _), _, _, _, _) :: steps) = id :: find_all_ids steps
+      | find_all_ids (((id, _), _, _, _, _) :: steps) = id :: find_all_ids steps
     fun keep_only_used used_ids steps =
       let
         fun remove_unused (((id, ids), role, theorem, rule, deps) :: steps) =
@@ -377,26 +379,25 @@
     keep_only_used (find_all_ids steps) steps
   end
 
-
 fun parse_proof local_name problem =
-    strip_spaces_except_between_idents
-    #> raw_explode
-    #>
-      (if local_name <> satallaxN then
-        (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
-          (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat)))
-           #> fst)
-      else
-        (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
-          (Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line))))
-            #> fst
-            #> rev
-            #> map to_satallax_step
-            #> seperate_assumptions_and_steps
-            #> create_satallax_proof_graph
-            #> add_quantifier_in_tree_part [] []
-            #> transform_to_standard_atp_step []
-            #> remove_unused_dependency))
+  strip_spaces_except_between_idents
+  #> raw_explode
+  #>
+    (if local_name <> satallaxN then
+      (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
+        (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat)))
+         #> fst)
+    else
+      (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
+        (Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line))))
+        #> fst
+        #> rev
+        #> map to_satallax_step
+        #> seperate_assumptions_and_steps
+        #> create_satallax_proof_graph
+        #> add_quantifier_in_tree_part [] []
+        #> transform_to_standard_atp_step []
+        #> remove_unused_dependency))
 
 fun atp_proof_of_tstplike_proof _ _ "" = []
   | atp_proof_of_tstplike_proof local_prover problem tstp =

--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -105,7 +105,7 @@
   smt_options = [],
   default_max_relevant = 120 (* FUDGE *),
   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
-              "warning : proof_done: status is still open"),
+    "warning : proof_done: status is still open"),
   parse_proof = SOME VeriT_Proof_Parse.parse_proof,
   replay = NONE }
 

--- a/src/HOL/Tools/SMT2/smtlib2_isar.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -59,7 +59,7 @@
     and un_term t = map_aterms un_free t
   in un_term end
 
-(* It is not entirely clear if this is necessary for abstractions variables. *)
+(* It is not entirely clear why this should be necessary, especially for abstractions variables. *)
 val unskolemize_names =
   Term.map_abs_vars (perhaps (try Name.dest_skolem))
   #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))

--- a/src/HOL/Tools/SMT2/verit_isar.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_isar.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -27,7 +27,6 @@
     conjecture_id fact_helper_ids proof =
   let
     val thy = Proof_Context.theory_of ctxt
-
     fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
       let
         val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs
@@ -45,6 +44,8 @@
             [(name0, role0, concl0, rule, []),
              ((id, []), Plain, concl', veriT_rewrite_rule,
               name0 :: normalizing_prems ctxt concl0)] end
+        else if rule = veriT_tmp_ite_elim_rule then
+          [standard_step Lemma]
         else
           [standard_step Plain]
       end

--- a/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -22,6 +22,8 @@
   val veriT_step_prefix : string
   val veriT_input_rule: string
   val veriT_rewrite_rule : string
+  val veriT_tmp_skolemize_rule : string
+  val veriT_tmp_ite_elim_rule : string
 end;
 
 structure VeriT_Proof: VERIT_PROOF =
@@ -85,6 +87,14 @@
      replace_bound_var_by_free_var v free_vars
   | replace_bound_var_by_free_var u _ = u
 
+fun replace_bound_all_by_ex ((q as Const (_, typ)) $ Abs (var, ty, u)) free_var =
+    (case List.find (fn v => String.isPrefix v var) free_var of
+      NONE => q $ Abs (var, ty, replace_bound_all_by_ex u free_var)
+    | SOME _ => Const (@{const_name "HOL.Ex"}, typ) $ Abs (var, ty, replace_bound_all_by_ex u free_var))
+  | replace_bound_all_by_ex (u $ v) free_vars = replace_bound_all_by_ex u free_vars $
+     replace_bound_all_by_ex v free_vars
+  | replace_bound_all_by_ex u _ = u
+
 fun find_type_in_formula (Abs(v, ty, u)) var_name =
     if String.isPrefix var_name v then SOME ty else find_type_in_formula u var_name
   | find_type_in_formula (u $ v) var_name =
@@ -195,7 +205,7 @@
     #> fix_subproof_steps
     ##> to_node
     #> (fn (subproof, (step, cx)) => (subproof @ [step], cx))
-    #> (fn (steps, cx) => fold_map update_step_and_cx steps cx)
+    #> uncurry (fold_map update_step_and_cx)
   end
 
 
@@ -236,8 +246,8 @@
 
 (*Yes every case is possible: the introduced var is not on a special size of the equality sign.*)
 fun find_ite_var_in_term (Const ("HOL.If", _) $ _ $
-      (Const ("HOL.eq", _) $ Free (var1, _) $ Free (var2, _) ) $
-      (Const ("HOL.eq", _) $ Free (var3, _) $ Free (var4, _) )) =
+      (Const (@{const_name "HOL.eq"}, _) $ Free (var1, _) $ Free (var2, _) ) $
+      (Const (@{const_name "HOL.eq"}, _) $ Free (var3, _) $ Free (var4, _) )) =
     let
       fun get_number_of_ite_transformed_var var =
         perhaps (try (unprefix "ite")) var
@@ -278,7 +288,7 @@
 
 
 fun correct_veriT_step steps (st as VeriT_Node {id, rule, prems, concl, bounds}) =
-  if rule = "tmp_ite_elim" then
+  if rule = veriT_tmp_ite_elim_rule then
     if bounds = [] then
       (*if the introduced var has already been defined,
         adding the definition as a dependency*)
@@ -325,7 +335,7 @@
     val smtlib2_lines_without_at =
       remove_all_at (map SMTLIB2.parse (seperate_into_steps lines))
     val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l)
-                             smtlib2_lines_without_at (empty_context ctxt typs funs))
+      smtlib2_lines_without_at (empty_context ctxt typs funs))
     val t = correct_veriT_steps u
     fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) =
       mk_step id rule prems concl bounds

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -66,7 +66,7 @@
     zipperposition_cnf_rule]
 
 val is_skolemize_rule = member (op =) skolemize_rules
-val is_arith_rule = (String.isPrefix z3_th_lemma_rule) orf (member (op =) veriT_arith_rules)
+val is_arith_rule = String.isPrefix z3_th_lemma_rule orf member (op =) veriT_arith_rules
 val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule
 
 fun raw_label_of_num num = (num, 0)
@@ -84,8 +84,7 @@
       line :: lines
     else if t aconv @{prop True} then
       map (replace_dependencies_in_line (name, [])) lines
-    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule
-        orelse is_skolemize_rule rule then
+    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then
       line :: lines
     else if role = Axiom then
       lines (* axioms (facts) need no proof lines *)