src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 42348 187354e22c7d
parent 42344 4a58173ffb99
child 42349 721e85fd2db3
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
     1.3 @@ -380,14 +380,16 @@
     1.4  
     1.5  val neg_neg_imp = @{lemma "~ ~ Q ==> Q" by blast}
     1.6  
     1.7 -(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
     1.8 -   double-negations. *)
     1.9 -fun negate_head thy =
    1.10 -  rewrite_rule @{thms atomize_not}
    1.11 -  #> perhaps (try (fn th => resolve_inc_tyvars thy th 1 neg_neg_imp))
    1.12 +val not_atomize =
    1.13 +  @{lemma "(~ A ==> False) == Trueprop A"
    1.14 +    by (cut_tac atomize_not [of "~ A"]) simp}
    1.15 +
    1.16 +(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
    1.17 +   to create double negations. *)
    1.18 +val negate_head = fold (rewrite_rule o single) [not_atomize, atomize_not]
    1.19  
    1.20  (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
    1.21 -fun select_literal thy = negate_head thy oo make_last
    1.22 +val select_literal = negate_head oo make_last
    1.23  
    1.24  fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
    1.25    let
    1.26 @@ -418,8 +420,7 @@
    1.27            handle Empty => raise Fail "Failed to find literal in th2"
    1.28          val _ = trace_msg ctxt (fn () => "  index_th2: " ^ string_of_int index_th2)
    1.29      in
    1.30 -      resolve_inc_tyvars thy (select_literal thy index_th1 i_th1) index_th2
    1.31 -                         i_th2
    1.32 +      resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
    1.33      end
    1.34    end;
    1.35