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