src/HOL/Decision_Procs/ferrante_rackoff.ML
changeset 38549 d0385f2764d8
parent 37744 3daaf23b9ab4
child 38558 32ad17fe2b9c
     1.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 19 10:27:12 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 19 11:02:14 2010 +0200
     1.3 @@ -33,12 +33,12 @@
     1.4               {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
     1.5  let
     1.6   fun uset (vars as (x::vs)) p = case term_of p of
     1.7 -   Const("op &", _)$ _ $ _ =>
     1.8 +   Const(@{const_name "op &"}, _)$ _ $ _ =>
     1.9       let
    1.10         val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    1.11         val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    1.12       in (lS@rS, Drule.binop_cong_rule b lth rth) end
    1.13 - |  Const("op |", _)$ _ $ _ =>
    1.14 + |  Const(@{const_name "op |"}, _)$ _ $ _ =>
    1.15       let
    1.16         val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    1.17         val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    1.18 @@ -77,7 +77,7 @@
    1.19   fun main vs p =
    1.20    let
    1.21     val ((xn,ce),(x,fm)) = (case term_of p of
    1.22 -                   Const("Ex",_)$Abs(xn,xT,_) =>
    1.23 +                   Const(@{const_name "Ex"},_)$Abs(xn,xT,_) =>
    1.24                          Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
    1.25                   | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    1.26     val cT = ctyp_of_term x
    1.27 @@ -122,12 +122,12 @@
    1.28  
    1.29     fun decomp_mpinf fm =
    1.30       case term_of fm of
    1.31 -       Const("op &",_)$_$_ =>
    1.32 +       Const(@{const_name "op &"},_)$_$_ =>
    1.33          let val (p,q) = Thm.dest_binop fm
    1.34          in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
    1.35                           (Thm.cabs x p) (Thm.cabs x q))
    1.36          end
    1.37 -     | Const("op |",_)$_$_ =>
    1.38 +     | Const(@{const_name "op |"},_)$_$_ =>
    1.39          let val (p,q) = Thm.dest_binop fm
    1.40          in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
    1.41                           (Thm.cabs x p) (Thm.cabs x q))
    1.42 @@ -175,19 +175,19 @@
    1.43   let
    1.44    fun h bounds tm =
    1.45     (case term_of tm of
    1.46 -     Const ("op =", T) $ _ $ _ =>
    1.47 +     Const (@{const_name "op ="}, T) $ _ $ _ =>
    1.48         if domain_type T = HOLogic.boolT then find_args bounds tm
    1.49         else Thm.dest_fun2 tm
    1.50 -   | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
    1.51 -   | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.52 -   | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.53 -   | Const ("op &", _) $ _ $ _ => find_args bounds tm
    1.54 -   | Const ("op |", _) $ _ $ _ => find_args bounds tm
    1.55 -   | Const ("op -->", _) $ _ $ _ => find_args bounds tm
    1.56 +   | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
    1.57 +   | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.58 +   | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.59 +   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    1.60 +   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    1.61 +   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
    1.62     | Const ("==>", _) $ _ $ _ => find_args bounds tm
    1.63     | Const ("==", _) $ _ $ _ => find_args bounds tm
    1.64     | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.65 -   | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
    1.66 +   | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
    1.67     | _ => Thm.dest_fun2 tm)
    1.68    and find_args bounds tm =
    1.69             (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)