src/Provers/coherent.ML
changeset 29273 285c00993bc2
parent 28339 6f6fa16543f5
equal deleted inserted replaced
29272:fb3ccf499df5 29273:285c00993bc2
     1 (*  Title:      Provers/coherent.ML
     1 (*  Title:      Provers/coherent.ML
     2     ID:         $Id$
       
     3     Author:     Stefan Berghofer, TU Muenchen
     2     Author:     Stefan Berghofer, TU Muenchen
     4                 Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
     3     Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
     5 
     4 
     6 Prover for coherent logic, see e.g.
     5 Prover for coherent logic, see e.g.
     7 
     6 
     8   Marc Bezem and Thierry Coquand, Automating Coherent Logic, LPAR 2005
     7   Marc Bezem and Thierry Coquand, Automating Coherent Logic, LPAR 2005
     9 
     8 
    37 
    36 
    38 datatype cl_prf =
    37 datatype cl_prf =
    39   ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
    38   ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
    40   int list * (term list * cl_prf) list;
    39   int list * (term list * cl_prf) list;
    41 
    40 
    42 fun is_atomic t = null (term_consts t inter Data.operator_names);
    41 val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
    43 
    42 
    44 local open Conv in
    43 local open Conv in
    45 
    44 
    46 fun rulify_elim_conv ct =
    45 fun rulify_elim_conv ct =
    47   if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
    46   if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct