# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 6dc58b3b73b5bb8222c6462a038108986de29b69
# Parent  ef3ff88562451f606f3256c360b2399cbd5c4854
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)

diff -r ef3ff8856245 -r 6dc58b3b73b5 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -387,7 +387,8 @@
 
 fun s_not (@{const Not} $ t) = t
   | s_not t = HOLogic.mk_not t
-fun simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
+fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
+  | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
   | simp_not_not t = t
 
 (* Match untyped terms. *)
@@ -400,15 +401,20 @@
     untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
   | untyped_aconv _ = false
 
+val normalize_literal = simp_not_not o Envir.eta_contract
+
 (* Find the relative location of an untyped term within a list of terms as a
    1-based index. Returns 0 in case of failure. *)
 fun index_of_literal lit haystack =
   let
-    val normalize = simp_not_not o Envir.eta_contract
-    val match_lit =
+    fun match_lit normalize =
       HOLogic.dest_Trueprop #> normalize
       #> curry untyped_aconv (lit |> normalize)
-  in find_index match_lit haystack + 1 end
+  in
+    (case find_index (match_lit I) haystack of
+       ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
+     | j => j) + 1
+  end
 
 (* Permute a rule's premises to move the i-th premise to the last position. *)
 fun make_last i th =
@@ -599,11 +605,7 @@
              (*if not equality, ignore head to skip the hBOOL predicate*)
         | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
         | path_finder MX tm ps t = path_finder_MX tm ps t
-      fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
-            let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
-            in (tm, nt $ tm_rslt) end
-        | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
-      val (tm_subst, body) = path_finder_lit i_atom fp
+      val (tm_subst, body) = path_finder mode i_atom fp m_tm
       val tm_abs = Abs ("x", type_of tm_subst, body)
       val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
       val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
@@ -667,14 +669,17 @@
     else
       let
         val (prems0, concl) = th |> prop_of |> Logic.strip_horn
-        val prems = prems0 |> distinct untyped_aconv
+        val prems = prems0 |> map normalize_literal
+                           |> distinct untyped_aconv
         val goal = Logic.list_implies (prems, concl)
+        val tac = cut_rules_tac [th] 1
+                  THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
+                  THEN ALLGOALS assume_tac
       in
         if length prems = length prems0 then
           raise METIS ("resynchronize", "Out of sync")
         else
-          Goal.prove ctxt [] [] goal (K (cut_rules_tac [th] 1
-                                         THEN ALLGOALS assume_tac))
+          Goal.prove ctxt [] [] goal (K tac)
           |> resynchronize ctxt fol_th
       end
   end