src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 40221 d10b68c6e6d4
parent 40158 a88d6073b190
child 40258 2c0d8fe36c21
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Oct 27 09:22:40 2010 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Oct 27 16:32:13 2010 +0200
     1.3 @@ -336,8 +336,10 @@
     1.4             | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
     1.5    end
     1.6  
     1.7 -fun mk_not (Const (@{const_name Not}, _) $ b) = b
     1.8 -  | mk_not b = HOLogic.mk_not b
     1.9 +fun s_not (@{const Not} $ t) = t
    1.10 +  | s_not t = HOLogic.mk_not t
    1.11 +fun simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
    1.12 +  | simp_not_not t = t
    1.13  
    1.14  (* Match untyped terms. *)
    1.15  fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
    1.16 @@ -351,16 +353,12 @@
    1.17    | untyped_aconv _ _ = false
    1.18  
    1.19  (* Finding the relative location of an untyped term within a list of terms *)
    1.20 -fun literal_index lit =
    1.21 +fun index_of_literal lit haystack =
    1.22    let
    1.23 -    val lit = Envir.eta_contract lit
    1.24 -    fun get _ [] = raise Empty
    1.25 -      | get n (x :: xs) =
    1.26 -        if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then
    1.27 -          n
    1.28 -        else
    1.29 -          get (n+1) xs
    1.30 -  in get 1 end
    1.31 +    val normalize = simp_not_not o Envir.eta_contract
    1.32 +    val match_lit =
    1.33 +      HOLogic.dest_Trueprop #> normalize #> untyped_aconv (lit |> normalize)
    1.34 +  in case find_index match_lit haystack of ~1 => raise Empty | n => n + 1 end
    1.35  
    1.36  (* Permute a rule's premises to move the i-th premise to the last position. *)
    1.37  fun make_last i th =
    1.38 @@ -391,16 +389,19 @@
    1.39        i_th1
    1.40      else
    1.41        let
    1.42 -        val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems)
    1.43 -                              (Metis_Term.Fn atm)
    1.44 +        val i_atm =
    1.45 +          singleton (hol_terms_from_fol ctxt mode old_skolems)
    1.46 +                    (Metis_Term.Fn atm)
    1.47          val _ = trace_msg ctxt (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
    1.48          val prems_th1 = prems_of i_th1
    1.49          val prems_th2 = prems_of i_th2
    1.50 -        val index_th1 = literal_index (mk_not i_atm) prems_th1
    1.51 -              handle Empty => raise Fail "Failed to find literal in th1"
    1.52 +        val index_th1 =
    1.53 +          index_of_literal (s_not i_atm) prems_th1
    1.54 +          handle Empty => raise Fail "Failed to find literal in th1"
    1.55          val _ = trace_msg ctxt (fn () => "  index_th1: " ^ Int.toString index_th1)
    1.56 -        val index_th2 = literal_index i_atm prems_th2
    1.57 -              handle Empty => raise Fail "Failed to find literal in th2"
    1.58 +        val index_th2 =
    1.59 +          index_of_literal i_atm prems_th2
    1.60 +          handle Empty => raise Fail "Failed to find literal in th2"
    1.61          val _ = trace_msg ctxt (fn () => "  index_th2: " ^ Int.toString index_th2)
    1.62      in
    1.63        resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2