# HG changeset patch
# User blanchet
# Date 1337876514 -7200
# Node ID 3eb598b044ade1aa8a6389e6a69f08abd3a9f21a
# Parent  7a642e5c272c501aec8188d3ec640be55fdeafd7
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)

diff -r 7a642e5c272c -r 3eb598b044ad src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Thu May 24 17:46:35 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Thu May 24 18:21:54 2012 +0200
@@ -75,8 +75,13 @@
   let
     val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
     val thy = Proof_Context.theory_of ctxt
-    val defs = defs |> map (ATP_Util.abs_extensionalize_term ctxt
-                            #> aptrueprop (open_form I))
+    val (defs, pseudo_defs) =
+      defs |> map (ATP_Util.abs_extensionalize_term ctxt
+                   #> aptrueprop (open_form I))
+           |> List.partition (ATP_Util.is_legitimate_tptp_def
+                              o perhaps (try HOLogic.dest_Trueprop)
+                              o ATP_Util.unextensionalize_def)
+    val nondefs = pseudo_defs @ nondefs
     val state = Proof.init ctxt
     val params =
       [("card", "1\<emdash>100"),
diff -r 7a642e5c272c -r 3eb598b044ad src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 24 17:46:35 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 24 18:21:54 2012 +0200
@@ -1247,20 +1247,6 @@
       | freeze t = t
   in t |> exists_subterm is_Var t ? freeze end
 
-fun unextensionalize_def t =
-  case t of
-    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
-    (case strip_comb lhs of
-       (c as Const (_, T), args) =>
-       if forall is_Var args andalso not (has_duplicates (op =) args) then
-         @{const Trueprop}
-         $ (Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
-            $ c $ fold_rev lambda args rhs)
-       else
-         t
-     | _ => t)
-  | _ => t
-
 fun presimp_prop ctxt type_enc t =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -1296,17 +1282,12 @@
      atomic_types = atomic_Ts}
   end
 
-fun is_legitimate_thf_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
-    (is_Const t orelse is_Free t) andalso
-    not (exists_subterm (curry (op =) t) u)
-  | is_legitimate_thf_def _ = false
-
 fun make_fact ctxt format type_enc iff_for_eq
               ((name, stature as (_, status)), t) =
   let
     val role =
       if is_type_enc_higher_order type_enc andalso status = Def andalso
-         is_legitimate_thf_def t then
+         is_legitimate_tptp_def t then
         Definition
       else
         Axiom
@@ -1329,7 +1310,7 @@
           let
             val role =
               if is_type_enc_higher_order type_enc andalso
-                 role <> Conjecture andalso is_legitimate_thf_def t then
+                 role <> Conjecture andalso is_legitimate_tptp_def t then
                 Definition
               else
                 role
diff -r 7a642e5c272c -r 3eb598b044ad src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Thu May 24 17:46:35 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu May 24 18:21:54 2012 +0200
@@ -38,6 +38,8 @@
   val eta_expand : typ list -> term -> int -> term
   val cong_extensionalize_term : theory -> term -> term
   val abs_extensionalize_term : Proof.context -> term -> term
+  val unextensionalize_def : term -> term
+  val is_legitimate_tptp_def : term -> bool
   val transform_elim_prop : term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
   val strip_subgoal :
@@ -320,6 +322,26 @@
   else
     t
 
+fun unextensionalize_def t =
+  case t of
+    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
+    (case strip_comb lhs of
+       (c as Const (_, T), args) =>
+       if forall is_Var args andalso not (has_duplicates (op =) args) then
+         @{const Trueprop}
+         $ (Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
+            $ c $ fold_rev lambda args rhs)
+       else
+         t
+     | _ => t)
+  | _ => t
+
+fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t
+  | is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+    (is_Const t orelse is_Free t) andalso
+    not (exists_subterm (curry (op =) t) u)
+  | is_legitimate_tptp_def _ = false
+
 (* 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