src/HOL/Tools/Qelim/ferrante_rackoff.ML

 
 Ferrante and Rackoff's algorithm for quantifier elimination in dense
 linear orders.  Proof-synthesis and tactic.
 *)
 
-signature FERRANTE_RACKOFF = 
+signature FERRANTE_RACKOFF =
 sig
+  val dlo_conv: Proof.context -> conv
   val dlo_tac: Proof.context -> int -> tactic
 end;
 
 structure FerranteRackoff: FERRANTE_RACKOFF =
 struct
 
 open Ferrante_Rackoff_Data;
 open Conv;
 
-type entry = {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list,  
+type entry = {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list,
    ld: thm list, qe: thm, atoms : cterm list} *
-  {isolate_conv: cterm list -> cterm -> thm, 
+  {isolate_conv: cterm list -> cterm -> thm,
                  whatis : cterm -> cterm -> ord,
                  simpset : simpset};
 
-fun binop_cong b th1 th2 = Thm.combination (Drule.arg_cong_rule b th1) th2;
-val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
-fun C f x y = f y x
-
-fun get_p1 th = 
- let 
-    fun appair f (x,y) = (f x, f y)
-  in funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) 
-     (funpow 2 Thm.dest_arg (cprop_of th)) |> Thm.dest_arg 
-end;
+fun get_p1 th =
+  funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
+    (funpow 2 Thm.dest_arg (cprop_of th)) |> Thm.dest_arg
 
 fun ferrack_conv
-   (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, 
+   (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi,
               ld = ld, qe = qe, atoms = atoms},
-             {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) = 
-let 
+             {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
+let
  fun uset (vars as (x::vs)) p = case term_of p of
-   Const("op &", _)$ _ $ _ => 
-     let 
-       val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb 
+   Const("op &", _)$ _ $ _ =>
+     let
+       val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
-     in (lS@rS, binop_cong b lth rth) end
- |  Const("op |", _)$ _ $ _ => 
-     let 
-       val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb 
+     in (lS@rS, Drule.binop_cong_rule b lth rth) end
+ |  Const("op |", _)$ _ $ _ =>
+     let
+       val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
-     in (lS@rS, binop_cong b lth rth) end
- | _ => 
-    let 
-      val th = icv vars p 
+     in (lS@rS, Drule.binop_cong_rule b lth rth) end
+ | _ =>
+    let
+      val th = icv vars p
       val p' = Thm.rhs_of th
       val c = wi x p'
-      val S = (if c mem [Lt, Le, Eq] then single o Thm.dest_arg
-               else if c mem [Gt, Ge] then single o Thm.dest_arg1
-               else if c = NEq then single o Thm.dest_arg o Thm.dest_arg 
+      val S = (if member (op =) [Lt, Le, Eq] c then single o Thm.dest_arg
+               else if member (op =) [Gt, Ge] c then single o Thm.dest_arg1
+               else if c = NEq then single o Thm.dest_arg o Thm.dest_arg
                else K []) p'
     in (S,th) end
 
- val ((p1_v,p2_v),(mp1_v,mp2_v)) = 
+ val ((p1_v,p2_v),(mp1_v,mp2_v)) =
+   funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
+     (funpow 4 Thm.dest_arg (cprop_of (hd minf)))
+   |> Thm.dest_binop |> pairself Thm.dest_binop |> apfst (pairself Thm.dest_fun)
+
+ fun myfwd (th1, th2, th3, th4, th5) p1 p2
+      [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] =
   let
-   fun appair f (x,y) = (f x, f y)
-  in funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) 
-       (funpow 4 Thm.dest_arg (cprop_of (hd minf))) 
-     |> Thm.dest_binop |> appair Thm.dest_binop |> apfst (appair Thm.dest_fun)  
-  end
-
- fun myfwd (th1, th2, th3, th4, th5) p1 p2 
-      [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] = 
-  let  
    val (mp1, mp2) = (get_p1 th_1, get_p1 th_1')
    val (pp1, pp2) = (get_p1 th_2, get_p1 th_2')
-   fun fw mi th th' th'' = 
-     let 
-      val th0 = if mi then 
+   fun fw mi th th' th'' =
+     let
+      val th0 = if mi then
            instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
         else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
      in implies_elim (implies_elim th0 th') th'' end
-  in (fw true th1 th_1 th_1', fw false th2 th_2 th_2', 
-      fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5') 
+  in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
+      fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
   end
  val U_v = (Thm.dest_arg o Thm.dest_arg o Thm.dest_arg1) (cprop_of qe)
- fun main vs p = 
-  let 
-   val ((xn,ce),(x,fm)) = (case term_of p of 
-                   Const("Ex",_)$Abs(xn,xT,_) =>  
+ fun main vs p =
+  let
+   val ((xn,ce),(x,fm)) = (case term_of p of
+                   Const("Ex",_)$Abs(xn,xT,_) =>
                         Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
-                 | _ => error "main QE only trats existential quantifiers!")
+                 | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    val cT = ctyp_of_term x
    val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc)
    val nthx = Thm.abstract_rule xn x nth
    val q = Thm.rhs_of nth
    val qx = Thm.rhs_of nthx
    val enth = Drule.arg_cong_rule ce nthx
    val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
-   fun ins x th = 
-      implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) 
+   fun ins x th =
+      implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
                                        (Thm.cprop_of th), SOME x] th1) th
    val fU = fold ins u th0
    val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU)
-   local 
+   local
      val insI1 = instantiate' [SOME cT] [] @{thm "insertI1"}
      val insI2 = instantiate' [SOME cT] [] @{thm "insertI2"}
    in
-    fun provein x S = 
+    fun provein x S =
      case term_of S of
-        Const("{}",_) => error "provein : not a member!"
-      | Const("insert",_)$y$_ => 
+        Const("{}",_) => raise CTERM ("provein : not a member!", [S])
+      | Const("insert",_)$y$_ =>
          let val (cy,S') = Thm.dest_binop S
          in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
-         else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) 
+         else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
                            (provein x S')
          end
    end
-   val tabU = fold (fn t => fn tab => Termtab.update (term_of t, provein t cU) tab) 
+   val tabU = fold (fn t => fn tab => Termtab.update (term_of t, provein t cU) tab)
                    u Termtab.empty
-   val U = valOf o Termtab.lookup tabU o term_of
-   val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt, 
+   val U = the o Termtab.lookup tabU o term_of
+   val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt,
         minf_le, minf_gt, minf_ge, minf_P] = minf
-   val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt, 
+   val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt,
         pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf
-   val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt, 
+   val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt,
         nmi_le, nmi_gt, nmi_ge, nmi_P] = map (instantiate ([],[(U_v,cU)])) nmi
-   val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt, 
+   val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt,
         npi_le, npi_gt, npi_ge, npi_P] = map (instantiate ([],[(U_v,cU)])) npi
-   val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt, 
+   val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
         ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld
-  
-   fun decomp_mpinf fm = 
+
+   fun decomp_mpinf fm =
      case term_of fm of
-       Const("op &",_)$_$_ => 
-        let val (p,q) = Thm.dest_binop fm 
-        in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj) 
+       Const("op &",_)$_$_ =>
+        let val (p,q) = Thm.dest_binop fm
+        in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
                          (Thm.cabs x p) (Thm.cabs x q))
         end
-     | Const("op |",_)$_$_ => 
-        let val (p,q) = Thm.dest_binop fm 
+     | Const("op |",_)$_$_ =>
+        let val (p,q) = Thm.dest_binop fm
         in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
                          (Thm.cabs x p) (Thm.cabs x q))
         end
-     | _ => 
+     | _ =>
         (let val c = wi x fm
-             val t = (if c=Nox then I 
-                      else if c mem [Lt, Le, Eq] then Thm.dest_arg
-                      else if c mem [Gt,Ge] then Thm.dest_arg1
-                      else if c = NEq then (Thm.dest_arg o Thm.dest_arg) 
-                      else error "decomp_mpinf: Impossible case!!") fm
-             val [mi_th, pi_th, nmi_th, npi_th, ld_th] = 
-               if c = Nox then map (instantiate' [] [SOME fm]) 
+             val t = (if c=Nox then I
+                      else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg
+                      else if member (op =) [Gt, Ge] c then Thm.dest_arg1
+                      else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
+                      else sys_error "decomp_mpinf: Impossible case!!") fm
+             val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
+               if c = Nox then map (instantiate' [] [SOME fm])
                                     [minf_P, pinf_P, nmi_P, npi_P, ld_P]
-               else 
-                let val [mi_th,pi_th,nmi_th,npi_th,ld_th] = 
+               else
+                let val [mi_th,pi_th,nmi_th,npi_th,ld_th] =
                  map (instantiate' [] [SOME t])
                  (case c of Lt => [minf_lt, pinf_lt, nmi_lt, npi_lt, ld_lt]
                           | Le => [minf_le, pinf_le, nmi_le, npi_le, ld_le]
                           | Gt => [minf_gt, pinf_gt, nmi_gt, npi_gt, ld_gt]
                           | Ge => [minf_ge, pinf_ge, nmi_ge, npi_ge, ld_ge]

                     fun Ufw th = implies_elim th tU
                  in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th]
                  end
          in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end)
    val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q
-   val qe_th = fold (C implies_elim)  [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th] 
-                  ((fconv_rule (Thm.beta_conversion true)) 
-                   (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th]) 
+   val qe_th = Drule.implies_elim_list
+                  ((fconv_rule (Thm.beta_conversion true))
+                   (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
                         qe))
-    val bex_conv = 
+                  [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
+    val bex_conv =
       Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)}))
     val result_th = fconv_rule (arg_conv bex_conv) (transitive enth qe_th)
    in result_th
    end
 
 in main
 end;
 
-val grab_atom_bop = 
- let 
+val grab_atom_bop =
+ let
   fun h bounds tm =
    (case term_of tm of
      Const ("op =", T) $ _ $ _ =>
-       if domain_type T = HOLogic.boolT then find_args bounds tm 
+       if domain_type T = HOLogic.boolT then find_args bounds tm
        else Thm.dest_fun2 tm
    | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
    | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const ("op &", _) $ _ $ _ => find_args bounds tm

    | Const ("op -->", _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
    | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
    | _ => Thm.dest_fun2 tm)
-  and find_args bounds tm = 
+  and find_args bounds tm =
            (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
  and find_body bounds b =
    let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
    in h (bounds + 1) b' end;
 in h end;
 
-fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset}) tm = 
- let 
+fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset}) tm =
+ let
    val ss = simpset
-   val pcv = Simplifier.rewrite 
-     (merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
-              @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss))
-    val postcv = Simplifier.rewrite ss
-    val nnf = K (nnf_conv then_conv postcv)
-    val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm []) 
+   val ss' =
+     merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
+              @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss)
+     |> Simplifier.inherit_context ss
+   val pcv = Simplifier.rewrite ss'     
+   val postcv = Simplifier.rewrite ss
+   val nnf = K (nnf_conv then_conv postcv)
+   val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm [])
                   (isolate_conv ctxt) nnf
-                  (fn vs => ferrack_conv (thy,{isolate_conv = isolate_conv ctxt, 
+                  (fn vs => ferrack_conv (thy,{isolate_conv = isolate_conv ctxt,
                                                whatis = whatis, simpset = simpset}) vs
                    then_conv postcv)
  in (Simplifier.rewrite ss then_conv qe_conv) tm end;
 
-fun ferrackqe_conv ctxt tm = 
- case Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm) of
-  NONE => error "ferrackqe_conv : no corresponding instance in context!"
-| SOME res => raw_ferrack_qe_conv ctxt res tm
-
-
-fun core_ferrack_tac ctxt res i st =
- let val p = nth (cprems_of st) (i - 1)
-     val th = symmetric (arg_conv (raw_ferrack_qe_conv ctxt res) p)
-     val p' = Thm.lhs_of th
-     val th' = implies_intr p' (equal_elim th (assume p')) 
-     val _ = print_thm th
-  in (rtac th' i) st 
-  end
-
-fun dlo_tac ctxt i st = 
- let 
-   val instance = (case Ferrante_Rackoff_Data.match ctxt 
-                           (grab_atom_bop 0 (nth (cprems_of st) (i - 1))) of 
-                    NONE => error "ferrackqe_conv : no corresponding instance in context!"
-                  | SOME r => r)
-   val ss = #simpset (snd instance)
-   in
-   (ObjectLogic.full_atomize_tac i THEN 
-    simp_tac ss i THEN
-    core_ferrack_tac ctxt instance i THEN 
-    (TRY (simp_tac (Simplifier.local_simpset_of ctxt) i))) st
-  end;
+fun dlo_instance ctxt tm =
+  Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm);
+
+fun dlo_conv ctxt tm =
+  (case dlo_instance ctxt tm of
+    NONE => raise CTERM ("ferrackqe_conv: no corresponding instance in context!", [tm])
+  | SOME instance => raw_ferrack_qe_conv ctxt instance tm);
+
+fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
+  (case dlo_instance ctxt p of
+    NONE => no_tac
+  | SOME instance =>
+      ObjectLogic.full_atomize_tac i THEN
+      simp_tac (#simpset (snd instance)) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
+      CONVERSION (ObjectLogic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
+      simp_tac (Simplifier.local_simpset_of ctxt) i));  (* FIXME really? *)
 
 end;