# HG changeset patch
# User blanchet
# Date 1335253660 -7200
# Node ID 04400144c6fc1b7a3e29467b54e524794742c373
# Parent  d6683fe037b152b871e1c8829458271faacefc71
handle TPTP definitions as definitions in Nitpick rather than as axioms

diff -r d6683fe037b1 -r 04400144c6fc src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Apr 24 09:47:40 2012 +0200
@@ -189,7 +189,7 @@
     val ctxt = Proof_Context.init_global thy
     val state = Proof.init ctxt
     val (res, _) = Nitpick.pick_nits_in_term state
-      (Nitpick_Isar.default_params thy []) Nitpick.Normal 1 1 1 [] [] t
+      (Nitpick_Isar.default_params thy []) Nitpick.Normal 1 1 1 [] [] [] t
     val _ = Output.urgent_message ("Nitpick: " ^ res)
   in
     (rpair []) (case res of
diff -r d6683fe037b1 -r 04400144c6fc src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Tue Apr 24 09:47:40 2012 +0200
@@ -45,9 +45,12 @@
                      ? Path.append (Path.explode "$PWD"))
     val ((_, _, problem), thy) =
       TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
+    val partitioned_problem =
+      List.partition (fn (_, role, _, _) => role = TPTP_Syntax.Role_Definition)
+                     problem
   in
     (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,
-     map get_tptp_formula problem, thy)
+     pairself (map get_tptp_formula) partitioned_problem, Theory.checkpoint thy)
   end
 
 (** Isabelle (combination of provers) **)
@@ -59,8 +62,9 @@
 
 fun nitpick_tptp_file timeout file_name =
   let
-    val (falsify, ts, thy) = read_tptp_file @{theory} file_name
+    val (falsify, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
     val ctxt = Proof_Context.init_global thy
+    val defs = defs |> map (ATP_Util.extensionalize_term ctxt)
     val state = Proof.init ctxt
     val params =
       [("card", "1\<emdash>100"),
@@ -82,8 +86,8 @@
     val step = 0
     val subst = []
   in
-    Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst ts
-        (if falsify then @{prop False} else @{prop True}); ()
+    Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst
+        defs nondefs (if falsify then @{prop False} else @{prop True}); ()
   end
 
 
@@ -99,13 +103,13 @@
 
 fun refute_tptp_file timeout file_name =
   let
-    val (falsify, ts, thy) = read_tptp_file @{theory} file_name
+    val (falsify, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
     val ctxt = Proof_Context.init_global thy
     val params =
       [("maxtime", string_of_int timeout),
        ("maxvars", "100000")]
   in
-    Refute.refute_term ctxt params ts @{prop False}
+    Refute.refute_term ctxt params (defs @ nondefs) @{prop False}
     |> print_szs_from_outcome falsify
   end
 
diff -r d6683fe037b1 -r 04400144c6fc src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Apr 24 09:47:40 2012 +0200
@@ -1207,19 +1207,6 @@
   else
     t
 
-fun is_fun_equality (@{const_name HOL.eq},
-                     Type (_, [Type (@{type_name fun}, _), _])) = true
-  | is_fun_equality _ = false
-
-fun extensionalize_term ctxt t =
-  if exists_Const is_fun_equality t then
-    let val thy = Proof_Context.theory_of ctxt in
-      t |> cterm_of thy |> Meson.extensionalize_conv ctxt
-        |> prop_of |> Logic.dest_equals |> snd
-    end
-  else
-    t
-
 fun preprocess_abstractions_in_terms trans_lams facts =
   let
     val (facts, lambda_ts) =
diff -r d6683fe037b1 -r 04400144c6fc src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Apr 24 09:47:40 2012 +0200
@@ -35,6 +35,7 @@
   val close_form : term -> term
   val monomorphic_term : Type.tyenv -> term -> term
   val eta_expand : typ list -> term -> int -> term
+  val extensionalize_term : Proof.context -> term -> term
   val transform_elim_prop : term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
   val strip_subgoal :
@@ -286,6 +287,19 @@
              (List.take (binder_types (fastype_of1 (Ts, t)), n))
              (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
 
+fun is_fun_equality (@{const_name HOL.eq},
+                     Type (_, [Type (@{type_name fun}, _), _])) = true
+  | is_fun_equality _ = false
+
+fun extensionalize_term ctxt t =
+  if exists_Const is_fun_equality t then
+    let val thy = Proof_Context.theory_of ctxt in
+      t |> cterm_of thy |> Meson.extensionalize_conv ctxt
+        |> prop_of |> Logic.dest_equals |> snd
+    end
+  else
+    t
+
 (* Converts an elim-rule into an equivalent theorem that does not have the
    predicate variable. Leaves other theorems unchanged. We simply instantiate
    the conclusion variable to "False". (Cf. "transform_elim_theorem" in
diff -r d6683fe037b1 -r 04400144c6fc src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 24 09:47:40 2012 +0200
@@ -72,7 +72,7 @@
   val unregister_term_postprocessor : typ -> theory -> theory
   val pick_nits_in_term :
     Proof.state -> params -> mode -> int -> int -> int -> (term * term) list
-    -> term list -> term -> string * Proof.state
+    -> term list -> term list -> term -> string * Proof.state
   val pick_nits_in_subgoal :
     Proof.state -> params -> mode -> int -> int -> string * Proof.state
 end;
@@ -217,7 +217,7 @@
 fun plazy f = Pretty.blk (0, pstrs (f ()))
 
 fun pick_them_nits_in_term deadline state (params : params) mode i n step
-                           subst assm_ts orig_t =
+                           subst def_assm_ts nondef_assm_ts orig_t =
   let
     val timer = Timer.startRealTimer ()
     val thy = Proof.theory_of state
@@ -259,7 +259,9 @@
     fun check_deadline () =
       if passed_deadline deadline then raise TimeLimit.TimeOut else ()
 
-    val assm_ts = if assms orelse mode <> Normal then assm_ts else []
+    val (def_assm_ts, nondef_assm_ts) =
+      if assms orelse mode <> Normal then (def_assm_ts, nondef_assm_ts)
+      else ([], [])
     val _ =
       if step = 0 then
         print_nt (fn () => "Nitpicking formula...")
@@ -269,26 +271,27 @@
                 (if i <> 1 orelse n <> 1 then
                    "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
                  else
-                   "goal")) [Logic.list_implies (assm_ts, orig_t)]))
+                   "goal")) [Logic.list_implies (nondef_assm_ts, orig_t)]))
     val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S"
                      o Date.fromTimeLocal o Time.now)
     val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
                 else orig_t
-    val conj_ts = neg_t :: assm_ts @ evals @ these needs
+    val conj_ts = neg_t :: def_assm_ts @ nondef_assm_ts @ evals @ these needs
     val tfree_table =
       if merge_type_vars then merged_type_var_table_for_terms thy conj_ts
       else []
     val merge_tfrees = merge_type_vars_in_term thy merge_type_vars tfree_table
     val neg_t = neg_t |> merge_tfrees
-    val assm_ts = assm_ts |> map merge_tfrees
+    val def_assm_ts = def_assm_ts |> map merge_tfrees
+    val nondef_assm_ts = nondef_assm_ts |> map merge_tfrees
     val evals = evals |> map merge_tfrees
     val needs = needs |> Option.map (map merge_tfrees)
-    val conj_ts = neg_t :: assm_ts @ evals @ these needs
+    val conj_ts = neg_t :: def_assm_ts @ nondef_assm_ts @ evals @ these needs
     val original_max_potential = max_potential
     val original_max_genuine = max_genuine
     val max_bisim_depth = fold Integer.max bisim_depths ~1
     val case_names = case_const_names ctxt stds
-    val defs = all_defs_of thy subst
+    val defs = def_assm_ts @ all_defs_of thy subst
     val nondefs = all_nondefs_of ctxt subst
     val def_tables = const_def_tables ctxt subst defs
     val nondef_table = const_nondef_table nondefs
@@ -321,7 +324,7 @@
             error "Nitpick cannot handle goals with schematic type variables."
     val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms,
          no_poly_user_axioms, binarize) =
-      preprocess_formulas hol_ctxt assm_ts neg_t
+      preprocess_formulas hol_ctxt nondef_assm_ts neg_t
     val got_all_user_axioms =
       got_all_mono_user_axioms andalso no_poly_user_axioms
 
@@ -672,7 +675,8 @@
           got_all_user_axioms andalso none_true wfs andalso
           sound_finitizes andalso total_consts <> SOME true andalso
           codatatypes_ok
-        fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
+        fun assms_prop () =
+          Logic.mk_conjunction_list (neg_t :: def_assm_ts @ nondef_assm_ts)
       in
         (print_t (fn () =>
              "% SZS status " ^
@@ -1047,7 +1051,7 @@
 val timeout_bonus = seconds 1.0
 
 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
-                      step subst assm_ts orig_t =
+                      step subst def_assm_ts nondef_assm_ts orig_t =
   let
     val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
     val print_t = if mode = TPTP then Output.urgent_message else K ()
@@ -1065,7 +1069,7 @@
           time_limit (if debug orelse is_none timeout then NONE
                       else SOME (Time.+ (the timeout, timeout_bonus)))
               (pick_them_nits_in_term deadline state params mode i n step subst
-                                      assm_ts) orig_t
+                                      def_assm_ts nondef_assm_ts) orig_t
           handle TOO_LARGE (_, details) =>
                  (print_t "% SZS status Unknown";
                   print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
@@ -1108,7 +1112,7 @@
         val t = Logic.goal_params t i |> fst
         val assms = map term_of (Assumption.all_assms_of ctxt)
         val (subst, assms, t) = extract_fixed_frees ctxt (assms, t)
-      in pick_nits_in_term state params mode i n step subst assms t end
+      in pick_nits_in_term state params mode i n step subst [] assms t end
   end
 
 end;