src/HOL/Decision_Procs/ferrante_rackoff.ML
author wenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 56245 84fc7dfa3cd4
parent 54742 7a86358a3c0b
child 59058 a78612c67ec0
permissions -rw-r--r--
more qualified names;
     1 (* Title:      HOL/Decision_Procs/ferrante_rackoff.ML
     2    Author:     Amine Chaieb, TU Muenchen
     3 
     4 Ferrante and Rackoff's algorithm for quantifier elimination in dense
     5 linear orders.  Proof-synthesis and tactic.
     6 *)
     7 
     8 signature FERRANTE_RACKOFF =
     9 sig
    10   val dlo_conv: Proof.context -> conv
    11   val dlo_tac: Proof.context -> int -> tactic
    12 end;
    13 
    14 structure FerranteRackoff: FERRANTE_RACKOFF =
    15 struct
    16 
    17 open Ferrante_Rackoff_Data;
    18 open Conv;
    19 
    20 type entry = {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list,
    21    ld: thm list, qe: thm, atoms : cterm list} *
    22   {isolate_conv: cterm list -> cterm -> thm,
    23                  whatis : cterm -> cterm -> ord,
    24                  simpset : simpset};
    25 
    26 fun get_p1 th =
    27   funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
    28     (funpow 2 Thm.dest_arg (cprop_of th)) |> Thm.dest_arg
    29 
    30 fun ferrack_conv ctxt
    31    (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi,
    32               ld = ld, qe = qe, atoms = atoms},
    33              {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
    34 let
    35  fun uset (vars as (x::vs)) p = case term_of p of
    36    Const(@{const_name HOL.conj}, _)$ _ $ _ =>
    37      let
    38        val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    39        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    40      in (lS@rS, Drule.binop_cong_rule b lth rth) end
    41  |  Const(@{const_name HOL.disj}, _)$ _ $ _ =>
    42      let
    43        val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    44        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    45      in (lS@rS, Drule.binop_cong_rule b lth rth) end
    46  | _ =>
    47     let
    48       val th = icv vars p
    49       val p' = Thm.rhs_of th
    50       val c = wi x p'
    51       val S = (if member (op =) [Lt, Le, Eq] c then single o Thm.dest_arg
    52                else if member (op =) [Gt, Ge] c then single o Thm.dest_arg1
    53                else if c = NEq then single o Thm.dest_arg o Thm.dest_arg
    54                else K []) p'
    55     in (S,th) end
    56 
    57  val ((p1_v,p2_v),(mp1_v,mp2_v)) =
    58    funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
    59      (funpow 4 Thm.dest_arg (cprop_of (hd minf)))
    60    |> Thm.dest_binop |> pairself Thm.dest_binop |> apfst (pairself Thm.dest_fun)
    61 
    62  fun myfwd (th1, th2, th3, th4, th5) p1 p2
    63       [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] =
    64   let
    65    val (mp1, mp2) = (get_p1 th_1, get_p1 th_1')
    66    val (pp1, pp2) = (get_p1 th_2, get_p1 th_2')
    67    fun fw mi th th' th'' =
    68      let
    69       val th0 = if mi then
    70            Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
    71         else Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
    72      in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
    73   in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
    74       fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
    75   end
    76  val U_v = (Thm.dest_arg o Thm.dest_arg o Thm.dest_arg1) (cprop_of qe)
    77  fun main vs p =
    78   let
    79    val ((xn,ce),(x,fm)) = (case term_of p of
    80                    Const(@{const_name Ex},_)$Abs(xn,xT,_) =>
    81                         Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
    82                  | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    83    val cT = ctyp_of_term x
    84    val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc)
    85    val nthx = Thm.abstract_rule xn x nth
    86    val q = Thm.rhs_of nth
    87    val qx = Thm.rhs_of nthx
    88    val enth = Drule.arg_cong_rule ce nthx
    89    val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
    90    fun ins x th =
    91       Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
    92                                        (Thm.cprop_of th), SOME x] th1) th
    93    val fU = fold ins u th0
    94    val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU)
    95    local
    96      val insI1 = instantiate' [SOME cT] [] @{thm "insertI1"}
    97      val insI2 = instantiate' [SOME cT] [] @{thm "insertI2"}
    98    in
    99     fun provein x S =
   100      case term_of S of
   101         Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S])
   102       | Const(@{const_name insert}, _) $ y $_ =>
   103          let val (cy,S') = Thm.dest_binop S
   104          in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
   105          else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   106                            (provein x S')
   107          end
   108    end
   109    val tabU = fold (fn t => fn tab => Termtab.update (term_of t, provein t cU) tab)
   110                    u Termtab.empty
   111    val U = the o Termtab.lookup tabU o term_of
   112    val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt,
   113         minf_le, minf_gt, minf_ge, minf_P] = minf
   114    val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt,
   115         pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf
   116    val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt,
   117         nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi
   118    val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt,
   119         npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi
   120    val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
   121         ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld
   122 
   123    fun decomp_mpinf fm =
   124      case term_of fm of
   125        Const(@{const_name HOL.conj},_)$_$_ =>
   126         let val (p,q) = Thm.dest_binop fm
   127         in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
   128                          (Thm.lambda x p) (Thm.lambda x q))
   129         end
   130      | Const(@{const_name HOL.disj},_)$_$_ =>
   131         let val (p,q) = Thm.dest_binop fm
   132         in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
   133                          (Thm.lambda x p) (Thm.lambda x q))
   134         end
   135      | _ =>
   136         (let val c = wi x fm
   137              val t = (if c=Nox then I
   138                       else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg
   139                       else if member (op =) [Gt, Ge] c then Thm.dest_arg1
   140                       else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
   141                       else raise Fail "decomp_mpinf: Impossible case!!") fm
   142              val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
   143                if c = Nox then map (instantiate' [] [SOME fm])
   144                                     [minf_P, pinf_P, nmi_P, npi_P, ld_P]
   145                else
   146                 let val [mi_th,pi_th,nmi_th,npi_th,ld_th] =
   147                  map (instantiate' [] [SOME t])
   148                  (case c of Lt => [minf_lt, pinf_lt, nmi_lt, npi_lt, ld_lt]
   149                           | Le => [minf_le, pinf_le, nmi_le, npi_le, ld_le]
   150                           | Gt => [minf_gt, pinf_gt, nmi_gt, npi_gt, ld_gt]
   151                           | Ge => [minf_ge, pinf_ge, nmi_ge, npi_ge, ld_ge]
   152                           | Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq]
   153                           | NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq])
   154                     val tU = U t
   155                     fun Ufw th = Thm.implies_elim th tU
   156                  in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th]
   157                  end
   158          in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end)
   159    val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q
   160    val qe_th = Drule.implies_elim_list
   161                   ((fconv_rule (Thm.beta_conversion true))
   162                    (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
   163                         qe))
   164                   [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
   165     val bex_conv =
   166       Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms bex_simps(1-5)})
   167     val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
   168    in result_th
   169    end
   170 
   171 in main
   172 end;
   173 
   174 val grab_atom_bop =
   175  let
   176   fun h bounds tm =
   177    (case term_of tm of
   178      Const (@{const_name HOL.eq}, T) $ _ $ _ =>
   179        if domain_type T = HOLogic.boolT then find_args bounds tm
   180        else Thm.dest_fun2 tm
   181    | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
   182    | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
   183    | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
   184    | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
   185    | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
   186    | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
   187    | Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm
   188    | Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm
   189    | Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm)
   190    | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
   191    | _ => Thm.dest_fun2 tm)
   192   and find_args bounds tm =
   193            (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
   194  and find_body bounds b =
   195    let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
   196    in h (bounds + 1) b' end;
   197 in h end;
   198 
   199 fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset = ss}) tm =
   200  let
   201    val ss' =
   202      merge_ss (simpset_of
   203       (put_simpset HOL_basic_ss ctxt addsimps
   204         @{thms simp_thms ex_simps all_simps not_all all_not_ex ex_disj_distrib}), ss);
   205    val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
   206    val postcv = Simplifier.rewrite (put_simpset ss ctxt);
   207    val nnf = K (nnf_conv ctxt then_conv postcv)
   208    val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm [])
   209                   (isolate_conv ctxt) nnf
   210                   (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
   211                                                whatis = whatis, simpset = ss}) vs
   212                    then_conv postcv)
   213  in (Simplifier.rewrite (put_simpset ss ctxt) then_conv qe_conv) tm end;
   214 
   215 fun dlo_instance ctxt tm =
   216   Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm);
   217 
   218 fun dlo_conv ctxt tm =
   219   (case dlo_instance ctxt tm of
   220     NONE => raise CTERM ("ferrackqe_conv: no corresponding instance in context!", [tm])
   221   | SOME instance => raw_ferrack_qe_conv ctxt instance tm);
   222 
   223 fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
   224   (case dlo_instance ctxt p of
   225     NONE => no_tac
   226   | SOME instance =>
   227       Object_Logic.full_atomize_tac ctxt i THEN
   228       simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
   229       CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
   230       simp_tac ctxt i));  (* FIXME really? *)
   231 
   232 end;