moved ML files where they are actually used;
authorwenzelm
Tue May 25 22:21:31 2010 +0200 (2010-05-25)
changeset 371205df087c6ce94
parent 37119 b36a5512c5fb
child 37121 8e51fc35d59f
moved ML files where they are actually used;
more precise dependencies;
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/ferrante_rackoff_data.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/Decision_Procs/langford_data.ML
src/HOL/IsaMakefile
src/HOL/Tools/Qelim/ferrante_rackoff.ML
src/HOL/Tools/Qelim/ferrante_rackoff_data.ML
src/HOL/Tools/Qelim/langford.ML
src/HOL/Tools/Qelim/langford_data.ML
     1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 25 22:12:26 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 25 22:21:31 2010 +0200
     1.3 @@ -8,10 +8,10 @@
     1.4  theory Dense_Linear_Order
     1.5  imports Main
     1.6  uses
     1.7 -  "~~/src/HOL/Tools/Qelim/langford_data.ML"
     1.8 -  "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"
     1.9 -  ("~~/src/HOL/Tools/Qelim/langford.ML")
    1.10 -  ("~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML")
    1.11 +  "langford_data.ML"
    1.12 +  "ferrante_rackoff_data.ML"
    1.13 +  ("langford.ML")
    1.14 +  ("ferrante_rackoff.ML")
    1.15  begin
    1.16  
    1.17  setup {* Langford_Data.setup #> Ferrante_Rackoff_Data.setup *}
    1.18 @@ -293,7 +293,7 @@
    1.19  
    1.20  lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
    1.21  
    1.22 -use "~~/src/HOL/Tools/Qelim/langford.ML"
    1.23 +use "langford.ML"
    1.24  method_setup dlo = {*
    1.25    Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac)
    1.26  *} "Langford's algorithm for quantifier elimination in dense linear orders"
    1.27 @@ -543,7 +543,7 @@
    1.28  
    1.29  end
    1.30  
    1.31 -use "~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML"
    1.32 +use "ferrante_rackoff.ML"
    1.33  
    1.34  method_setup ferrack = {*
    1.35    Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Tue May 25 22:21:31 2010 +0200
     2.3 @@ -0,0 +1,233 @@
     2.4 +(* Title:      HOL/Tools/Qelim/ferrante_rackoff.ML
     2.5 +   Author:     Amine Chaieb, TU Muenchen
     2.6 +
     2.7 +Ferrante and Rackoff's algorithm for quantifier elimination in dense
     2.8 +linear orders.  Proof-synthesis and tactic.
     2.9 +*)
    2.10 +
    2.11 +signature FERRANTE_RACKOFF =
    2.12 +sig
    2.13 +  val dlo_conv: Proof.context -> conv
    2.14 +  val dlo_tac: Proof.context -> int -> tactic
    2.15 +end;
    2.16 +
    2.17 +structure FerranteRackoff: FERRANTE_RACKOFF =
    2.18 +struct
    2.19 +
    2.20 +open Ferrante_Rackoff_Data;
    2.21 +open Conv;
    2.22 +
    2.23 +type entry = {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list,
    2.24 +   ld: thm list, qe: thm, atoms : cterm list} *
    2.25 +  {isolate_conv: cterm list -> cterm -> thm,
    2.26 +                 whatis : cterm -> cterm -> ord,
    2.27 +                 simpset : simpset};
    2.28 +
    2.29 +fun get_p1 th =
    2.30 +  funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
    2.31 +    (funpow 2 Thm.dest_arg (cprop_of th)) |> Thm.dest_arg
    2.32 +
    2.33 +fun ferrack_conv
    2.34 +   (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi,
    2.35 +              ld = ld, qe = qe, atoms = atoms},
    2.36 +             {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
    2.37 +let
    2.38 + fun uset (vars as (x::vs)) p = case term_of p of
    2.39 +   Const("op &", _)$ _ $ _ =>
    2.40 +     let
    2.41 +       val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    2.42 +       val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    2.43 +     in (lS@rS, Drule.binop_cong_rule b lth rth) end
    2.44 + |  Const("op |", _)$ _ $ _ =>
    2.45 +     let
    2.46 +       val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    2.47 +       val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    2.48 +     in (lS@rS, Drule.binop_cong_rule b lth rth) end
    2.49 + | _ =>
    2.50 +    let
    2.51 +      val th = icv vars p
    2.52 +      val p' = Thm.rhs_of th
    2.53 +      val c = wi x p'
    2.54 +      val S = (if member (op =) [Lt, Le, Eq] c then single o Thm.dest_arg
    2.55 +               else if member (op =) [Gt, Ge] c then single o Thm.dest_arg1
    2.56 +               else if c = NEq then single o Thm.dest_arg o Thm.dest_arg
    2.57 +               else K []) p'
    2.58 +    in (S,th) end
    2.59 +
    2.60 + val ((p1_v,p2_v),(mp1_v,mp2_v)) =
    2.61 +   funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
    2.62 +     (funpow 4 Thm.dest_arg (cprop_of (hd minf)))
    2.63 +   |> Thm.dest_binop |> pairself Thm.dest_binop |> apfst (pairself Thm.dest_fun)
    2.64 +
    2.65 + fun myfwd (th1, th2, th3, th4, th5) p1 p2
    2.66 +      [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] =
    2.67 +  let
    2.68 +   val (mp1, mp2) = (get_p1 th_1, get_p1 th_1')
    2.69 +   val (pp1, pp2) = (get_p1 th_2, get_p1 th_2')
    2.70 +   fun fw mi th th' th'' =
    2.71 +     let
    2.72 +      val th0 = if mi then
    2.73 +           instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
    2.74 +        else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
    2.75 +     in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
    2.76 +  in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
    2.77 +      fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
    2.78 +  end
    2.79 + val U_v = (Thm.dest_arg o Thm.dest_arg o Thm.dest_arg1) (cprop_of qe)
    2.80 + fun main vs p =
    2.81 +  let
    2.82 +   val ((xn,ce),(x,fm)) = (case term_of p of
    2.83 +                   Const("Ex",_)$Abs(xn,xT,_) =>
    2.84 +                        Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
    2.85 +                 | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    2.86 +   val cT = ctyp_of_term x
    2.87 +   val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc)
    2.88 +   val nthx = Thm.abstract_rule xn x nth
    2.89 +   val q = Thm.rhs_of nth
    2.90 +   val qx = Thm.rhs_of nthx
    2.91 +   val enth = Drule.arg_cong_rule ce nthx
    2.92 +   val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
    2.93 +   fun ins x th =
    2.94 +      Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
    2.95 +                                       (Thm.cprop_of th), SOME x] th1) th
    2.96 +   val fU = fold ins u th0
    2.97 +   val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU)
    2.98 +   local
    2.99 +     val insI1 = instantiate' [SOME cT] [] @{thm "insertI1"}
   2.100 +     val insI2 = instantiate' [SOME cT] [] @{thm "insertI2"}
   2.101 +   in
   2.102 +    fun provein x S =
   2.103 +     case term_of S of
   2.104 +        Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S])
   2.105 +      | Const(@{const_name insert}, _) $ y $_ =>
   2.106 +         let val (cy,S') = Thm.dest_binop S
   2.107 +         in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
   2.108 +         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   2.109 +                           (provein x S')
   2.110 +         end
   2.111 +   end
   2.112 +   val tabU = fold (fn t => fn tab => Termtab.update (term_of t, provein t cU) tab)
   2.113 +                   u Termtab.empty
   2.114 +   val U = the o Termtab.lookup tabU o term_of
   2.115 +   val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt,
   2.116 +        minf_le, minf_gt, minf_ge, minf_P] = minf
   2.117 +   val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt,
   2.118 +        pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf
   2.119 +   val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt,
   2.120 +        nmi_le, nmi_gt, nmi_ge, nmi_P] = map (instantiate ([],[(U_v,cU)])) nmi
   2.121 +   val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt,
   2.122 +        npi_le, npi_gt, npi_ge, npi_P] = map (instantiate ([],[(U_v,cU)])) npi
   2.123 +   val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
   2.124 +        ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld
   2.125 +
   2.126 +   fun decomp_mpinf fm =
   2.127 +     case term_of fm of
   2.128 +       Const("op &",_)$_$_ =>
   2.129 +        let val (p,q) = Thm.dest_binop fm
   2.130 +        in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
   2.131 +                         (Thm.cabs x p) (Thm.cabs x q))
   2.132 +        end
   2.133 +     | Const("op |",_)$_$_ =>
   2.134 +        let val (p,q) = Thm.dest_binop fm
   2.135 +        in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
   2.136 +                         (Thm.cabs x p) (Thm.cabs x q))
   2.137 +        end
   2.138 +     | _ =>
   2.139 +        (let val c = wi x fm
   2.140 +             val t = (if c=Nox then I
   2.141 +                      else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg
   2.142 +                      else if member (op =) [Gt, Ge] c then Thm.dest_arg1
   2.143 +                      else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
   2.144 +                      else sys_error "decomp_mpinf: Impossible case!!") fm
   2.145 +             val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
   2.146 +               if c = Nox then map (instantiate' [] [SOME fm])
   2.147 +                                    [minf_P, pinf_P, nmi_P, npi_P, ld_P]
   2.148 +               else
   2.149 +                let val [mi_th,pi_th,nmi_th,npi_th,ld_th] =
   2.150 +                 map (instantiate' [] [SOME t])
   2.151 +                 (case c of Lt => [minf_lt, pinf_lt, nmi_lt, npi_lt, ld_lt]
   2.152 +                          | Le => [minf_le, pinf_le, nmi_le, npi_le, ld_le]
   2.153 +                          | Gt => [minf_gt, pinf_gt, nmi_gt, npi_gt, ld_gt]
   2.154 +                          | Ge => [minf_ge, pinf_ge, nmi_ge, npi_ge, ld_ge]
   2.155 +                          | Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq]
   2.156 +                          | NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq])
   2.157 +                    val tU = U t
   2.158 +                    fun Ufw th = Thm.implies_elim th tU
   2.159 +                 in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th]
   2.160 +                 end
   2.161 +         in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end)
   2.162 +   val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q
   2.163 +   val qe_th = Drule.implies_elim_list
   2.164 +                  ((fconv_rule (Thm.beta_conversion true))
   2.165 +                   (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
   2.166 +                        qe))
   2.167 +                  [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
   2.168 +    val bex_conv =
   2.169 +      Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)}))
   2.170 +    val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
   2.171 +   in result_th
   2.172 +   end
   2.173 +
   2.174 +in main
   2.175 +end;
   2.176 +
   2.177 +val grab_atom_bop =
   2.178 + let
   2.179 +  fun h bounds tm =
   2.180 +   (case term_of tm of
   2.181 +     Const ("op =", T) $ _ $ _ =>
   2.182 +       if domain_type T = HOLogic.boolT then find_args bounds tm
   2.183 +       else Thm.dest_fun2 tm
   2.184 +   | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
   2.185 +   | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
   2.186 +   | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
   2.187 +   | Const ("op &", _) $ _ $ _ => find_args bounds tm
   2.188 +   | Const ("op |", _) $ _ $ _ => find_args bounds tm
   2.189 +   | Const ("op -->", _) $ _ $ _ => find_args bounds tm
   2.190 +   | Const ("==>", _) $ _ $ _ => find_args bounds tm
   2.191 +   | Const ("==", _) $ _ $ _ => find_args bounds tm
   2.192 +   | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
   2.193 +   | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
   2.194 +   | _ => Thm.dest_fun2 tm)
   2.195 +  and find_args bounds tm =
   2.196 +           (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
   2.197 + and find_body bounds b =
   2.198 +   let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
   2.199 +   in h (bounds + 1) b' end;
   2.200 +in h end;
   2.201 +
   2.202 +fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset}) tm =
   2.203 + let
   2.204 +   val ss = simpset
   2.205 +   val ss' =
   2.206 +     merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
   2.207 +              @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss)
   2.208 +     |> Simplifier.inherit_context ss
   2.209 +   val pcv = Simplifier.rewrite ss'     
   2.210 +   val postcv = Simplifier.rewrite ss
   2.211 +   val nnf = K (nnf_conv then_conv postcv)
   2.212 +   val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm [])
   2.213 +                  (isolate_conv ctxt) nnf
   2.214 +                  (fn vs => ferrack_conv (thy,{isolate_conv = isolate_conv ctxt,
   2.215 +                                               whatis = whatis, simpset = simpset}) vs
   2.216 +                   then_conv postcv)
   2.217 + in (Simplifier.rewrite ss then_conv qe_conv) tm end;
   2.218 +
   2.219 +fun dlo_instance ctxt tm =
   2.220 +  Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm);
   2.221 +
   2.222 +fun dlo_conv ctxt tm =
   2.223 +  (case dlo_instance ctxt tm of
   2.224 +    NONE => raise CTERM ("ferrackqe_conv: no corresponding instance in context!", [tm])
   2.225 +  | SOME instance => raw_ferrack_qe_conv ctxt instance tm);
   2.226 +
   2.227 +fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
   2.228 +  (case dlo_instance ctxt p of
   2.229 +    NONE => no_tac
   2.230 +  | SOME instance =>
   2.231 +      Object_Logic.full_atomize_tac i THEN
   2.232 +      simp_tac (#simpset (snd instance)) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
   2.233 +      CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
   2.234 +      simp_tac (simpset_of ctxt) i));  (* FIXME really? *)
   2.235 +
   2.236 +end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Tue May 25 22:21:31 2010 +0200
     3.3 @@ -0,0 +1,146 @@
     3.4 +(* Title:      HOL/Tools/Qelim/ferrante_rackoff_data.ML
     3.5 +   Author:     Amine Chaieb, TU Muenchen
     3.6 +
     3.7 +Context data for Ferrante and Rackoff's algorithm for quantifier
     3.8 +elimination in dense linear orders.
     3.9 +*)
    3.10 +
    3.11 +signature FERRANTE_RACKOF_DATA =
    3.12 +sig
    3.13 +  datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox
    3.14 +  type entry
    3.15 +  val get: Proof.context -> (thm * entry) list
    3.16 +  val del: attribute
    3.17 +  val add: entry -> attribute 
    3.18 +  val funs: thm -> 
    3.19 +    {isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm,
    3.20 +     whatis: morphism -> cterm -> cterm -> ord,
    3.21 +     simpset: morphism -> simpset} -> declaration
    3.22 +  val match: Proof.context -> cterm -> entry option
    3.23 +  val setup: theory -> theory
    3.24 +end;
    3.25 +
    3.26 +structure Ferrante_Rackoff_Data: FERRANTE_RACKOF_DATA = 
    3.27 +struct
    3.28 +
    3.29 +(* data *)
    3.30 +
    3.31 +datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox
    3.32 +
    3.33 +type entry = 
    3.34 +  {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list,  
    3.35 +   ld: thm list, qe: thm, atoms : cterm list} *
    3.36 +   {isolate_conv: Proof.context -> cterm list -> cterm -> thm, 
    3.37 +    whatis : cterm -> cterm -> ord, 
    3.38 +    simpset : simpset};
    3.39 +
    3.40 +val eq_key = Thm.eq_thm;
    3.41 +fun eq_data arg = eq_fst eq_key arg;
    3.42 +
    3.43 +structure Data = Generic_Data
    3.44 +(
    3.45 +  type T = (thm * entry) list;
    3.46 +  val empty = [];
    3.47 +  val extend = I;
    3.48 +  fun merge data : T = AList.merge eq_key (K true) data;
    3.49 +);
    3.50 +
    3.51 +val get = Data.get o Context.Proof;
    3.52 +
    3.53 +fun del_data key = remove eq_data (key, []);
    3.54 +
    3.55 +val del = Thm.declaration_attribute (Data.map o del_data);
    3.56 +
    3.57 +fun add entry = 
    3.58 +    Thm.declaration_attribute (fn key => fn context => context |> Data.map 
    3.59 +      (del_data key #> cons (key, entry)));
    3.60 +
    3.61 +
    3.62 +(* extra-logical functions *)
    3.63 +
    3.64 +fun funs raw_key {isolate_conv = icv, whatis = wi, simpset = ss} phi = Data.map (fn data =>
    3.65 +  let
    3.66 +    val key = Morphism.thm phi raw_key;
    3.67 +    val _ = AList.defined eq_key data key orelse
    3.68 +      raise THM ("No data entry for structure key", 0, [key]);
    3.69 +    val fns = {isolate_conv = icv phi, whatis = wi phi, simpset = ss phi};
    3.70 +  in AList.map_entry eq_key key (apsnd (K fns)) data end);
    3.71 +
    3.72 +fun match ctxt tm =
    3.73 +  let
    3.74 +    fun match_inst
    3.75 +        ({minf, pinf, nmi, npi, ld, qe, atoms},
    3.76 +         fns as {isolate_conv, whatis, simpset}) pat =
    3.77 +       let
    3.78 +        fun h instT =
    3.79 +          let
    3.80 +            val substT = Thm.instantiate (instT, []);
    3.81 +            val substT_cterm = Drule.cterm_rule substT;
    3.82 +
    3.83 +            val minf' = map substT minf
    3.84 +            val pinf' = map substT pinf
    3.85 +            val nmi' = map substT nmi
    3.86 +            val npi' = map substT npi
    3.87 +            val ld' = map substT ld
    3.88 +            val qe' = substT qe
    3.89 +            val atoms' = map substT_cterm atoms
    3.90 +            val result = ({minf = minf', pinf = pinf', nmi = nmi', npi = npi', 
    3.91 +                           ld = ld', qe = qe', atoms = atoms'}, fns)
    3.92 +          in SOME result end
    3.93 +      in (case try Thm.match (pat, tm) of
    3.94 +           NONE => NONE
    3.95 +         | SOME (instT, _) => h instT)
    3.96 +      end;
    3.97 +
    3.98 +    fun match_struct (_,
    3.99 +        entry as ({atoms = atoms, ...}, _): entry) =
   3.100 +      get_first (match_inst entry) atoms;
   3.101 +  in get_first match_struct (get ctxt) end;
   3.102 +
   3.103 +
   3.104 +(* concrete syntax *)
   3.105 +
   3.106 +local
   3.107 +val minfN = "minf";
   3.108 +val pinfN = "pinf";
   3.109 +val nmiN = "nmi";
   3.110 +val npiN = "npi";
   3.111 +val lin_denseN = "lindense";
   3.112 +val qeN = "qe"
   3.113 +val atomsN = "atoms"
   3.114 +val simpsN = "simps"
   3.115 +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   3.116 +val any_keyword =
   3.117 +  keyword minfN || keyword pinfN || keyword nmiN 
   3.118 +|| keyword npiN || keyword lin_denseN || keyword qeN 
   3.119 +|| keyword atomsN || keyword simpsN;
   3.120 +
   3.121 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   3.122 +val terms = thms >> map Drule.dest_term;
   3.123 +in
   3.124 +
   3.125 +val ferrak_setup =
   3.126 +  Attrib.setup @{binding ferrack}
   3.127 +    ((keyword minfN |-- thms)
   3.128 +     -- (keyword pinfN |-- thms)
   3.129 +     -- (keyword nmiN |-- thms)
   3.130 +     -- (keyword npiN |-- thms)
   3.131 +     -- (keyword lin_denseN |-- thms)
   3.132 +     -- (keyword qeN |-- thms)
   3.133 +     -- (keyword atomsN |-- terms) >>
   3.134 +       (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> 
   3.135 +       if length qe = 1 then
   3.136 +         add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
   3.137 +              qe = hd qe, atoms = atoms},
   3.138 +             {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
   3.139 +       else error "only one theorem for qe!"))
   3.140 +    "Ferrante Rackoff data";
   3.141 +
   3.142 +end;
   3.143 +
   3.144 +
   3.145 +(* theory setup *)
   3.146 +
   3.147 +val setup = ferrak_setup;
   3.148 +
   3.149 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Decision_Procs/langford.ML	Tue May 25 22:21:31 2010 +0200
     4.3 @@ -0,0 +1,244 @@
     4.4 +(*  Title:      HOL/Tools/Qelim/langford.ML
     4.5 +    Author:     Amine Chaieb, TU Muenchen
     4.6 +*)
     4.7 +
     4.8 +signature LANGFORD_QE = 
     4.9 +sig
    4.10 +  val dlo_tac : Proof.context -> int -> tactic
    4.11 +  val dlo_conv : Proof.context -> cterm -> thm
    4.12 +end
    4.13 +
    4.14 +structure LangfordQE :LANGFORD_QE = 
    4.15 +struct
    4.16 +
    4.17 +val dest_set =
    4.18 + let 
    4.19 +  fun h acc ct = 
    4.20 +   case term_of ct of
    4.21 +     Const (@{const_name Orderings.bot}, _) => acc
    4.22 +   | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
    4.23 +in h [] end;
    4.24 +
    4.25 +fun prove_finite cT u = 
    4.26 +let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
    4.27 +    fun ins x th =
    4.28 +     Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
    4.29 +                                     (Thm.cprop_of th), SOME x] th1) th
    4.30 +in fold ins u th0 end;
    4.31 +
    4.32 +val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms))));
    4.33 +
    4.34 +fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = 
    4.35 + case term_of ep of 
    4.36 +  Const("Ex",_)$_ => 
    4.37 +   let 
    4.38 +     val p = Thm.dest_arg ep
    4.39 +     val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid)
    4.40 +     val (L,U) = 
    4.41 +       let 
    4.42 +         val (x,q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
    4.43 +       in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1)
    4.44 +       end
    4.45 +     fun proveneF S =         
    4.46 +       let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg
    4.47 +           val cT = ctyp_of_term a
    4.48 +           val ne = instantiate' [SOME cT] [SOME a, SOME A] 
    4.49 +                    @{thm insert_not_empty}
    4.50 +           val f = prove_finite cT (dest_set S)
    4.51 +       in (ne, f) end
    4.52 +
    4.53 +     val qe = case (term_of L, term_of U) of 
    4.54 +      (Const (@{const_name Orderings.bot}, _),_) =>  
    4.55 +        let
    4.56 +          val (neU,fU) = proveneF U 
    4.57 +        in simp_rule (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
    4.58 +    | (_,Const (@{const_name Orderings.bot}, _)) =>  
    4.59 +        let
    4.60 +          val (neL,fL) = proveneF L
    4.61 +        in simp_rule (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
    4.62 +
    4.63 +    | (_,_) =>  
    4.64 +      let 
    4.65 +       val (neL,fL) = proveneF L
    4.66 +       val (neU,fU) = proveneF U
    4.67 +      in simp_rule (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) 
    4.68 +      end
    4.69 +   in qe end 
    4.70 + | _ => error "dlo_qe : Not an existential formula";
    4.71 +
    4.72 +val all_conjuncts = 
    4.73 + let fun h acc ct = 
    4.74 +  case term_of ct of
    4.75 +   @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
    4.76 +  | _ => ct::acc
    4.77 +in h [] end;
    4.78 +
    4.79 +fun conjuncts ct =
    4.80 + case term_of ct of
    4.81 +  @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
    4.82 +| _ => [ct];
    4.83 +
    4.84 +fun fold1 f = foldr1 (uncurry f);
    4.85 +
    4.86 +val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
    4.87 +
    4.88 +fun mk_conj_tab th = 
    4.89 + let fun h acc th = 
    4.90 +   case prop_of th of
    4.91 +   @{term "Trueprop"}$(@{term "op &"}$p$q) => 
    4.92 +     h (h acc (th RS conjunct2)) (th RS conjunct1)
    4.93 +  | @{term "Trueprop"}$p => (p,th)::acc
    4.94 +in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
    4.95 +
    4.96 +fun is_conj (@{term "op &"}$_$_) = true
    4.97 +  | is_conj _ = false;
    4.98 +
    4.99 +fun prove_conj tab cjs = 
   4.100 + case cjs of 
   4.101 +   [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c
   4.102 + | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs];
   4.103 +
   4.104 +fun conj_aci_rule eq = 
   4.105 + let 
   4.106 +  val (l,r) = Thm.dest_equals eq
   4.107 +  fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
   4.108 +  fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
   4.109 +  val ll = Thm.dest_arg l
   4.110 +  val rr = Thm.dest_arg r
   4.111 +  
   4.112 +  val thl  = prove_conj tabl (conjuncts rr) 
   4.113 +                |> Drule.implies_intr_hyps
   4.114 +  val thr  = prove_conj tabr (conjuncts ll) 
   4.115 +                |> Drule.implies_intr_hyps
   4.116 +  val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
   4.117 + in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
   4.118 +
   4.119 +fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
   4.120 +
   4.121 +fun is_eqx x eq = case term_of eq of
   4.122 +   Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x
   4.123 + | _ => false ;
   4.124 +
   4.125 +local 
   4.126 +fun proc ct = 
   4.127 + case term_of ct of
   4.128 +  Const("Ex",_)$Abs (xn,_,_) => 
   4.129 +   let 
   4.130 +    val e = Thm.dest_fun ct
   4.131 +    val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
   4.132 +    val Pp = Thm.capply @{cterm "Trueprop"} p 
   4.133 +    val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
   4.134 +   in case eqs of
   4.135 +      [] => 
   4.136 +        let 
   4.137 +         val (dx,ndx) = List.partition (contains x) neqs
   4.138 +         in case ndx of [] => NONE
   4.139 +                      | _ =>
   4.140 +            conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
   4.141 +                 (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx))))
   4.142 +           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
   4.143 +           |> Conv.fconv_rule (Conv.arg_conv 
   4.144 +                   (Simplifier.rewrite 
   4.145 +                      (HOL_basic_ss addsimps (simp_thms @ ex_simps))))
   4.146 +           |> SOME
   4.147 +          end
   4.148 +    | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
   4.149 +                 (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs))))
   4.150 +           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
   4.151 +           |> Conv.fconv_rule (Conv.arg_conv 
   4.152 +                   (Simplifier.rewrite 
   4.153 +                (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) 
   4.154 +           |> SOME
   4.155 +   end
   4.156 + | _ => NONE;
   4.157 +in val reduce_ex_simproc = 
   4.158 +  Simplifier.make_simproc 
   4.159 +  {lhss = [@{cpat "EX x. ?P x"}] , name = "reduce_ex_simproc",
   4.160 +   proc = K (K proc) , identifier = []}
   4.161 +end;
   4.162 +
   4.163 +fun raw_dlo_conv dlo_ss 
   4.164 +          ({qe_bnds, qe_nolb, qe_noub, gst, gs, atoms}:Langford_Data.entry) = 
   4.165 + let 
   4.166 +  val ss = dlo_ss addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc]
   4.167 +  val dnfex_conv = Simplifier.rewrite ss
   4.168 +   val pcv = Simplifier.rewrite
   4.169 +               (dlo_ss addsimps (simp_thms @ ex_simps @ all_simps)
   4.170 +                @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib])
   4.171 + in fn p => 
   4.172 +   Qelim.gen_qelim_conv pcv pcv dnfex_conv cons 
   4.173 +                  (Thm.add_cterm_frees p [])  (K Thm.reflexive) (K Thm.reflexive)
   4.174 +                  (K (basic_dloqe () gst qe_bnds qe_nolb qe_noub gs)) p
   4.175 + end;
   4.176 +
   4.177 +
   4.178 +val grab_atom_bop =
   4.179 + let
   4.180 +  fun h bounds tm =
   4.181 +   (case term_of tm of
   4.182 +     Const ("op =", T) $ _ $ _ =>
   4.183 +       if domain_type T = HOLogic.boolT then find_args bounds tm
   4.184 +       else Thm.dest_fun2 tm
   4.185 +   | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
   4.186 +   | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
   4.187 +   | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
   4.188 +   | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
   4.189 +   | Const ("op &", _) $ _ $ _ => find_args bounds tm
   4.190 +   | Const ("op |", _) $ _ $ _ => find_args bounds tm
   4.191 +   | Const ("op -->", _) $ _ $ _ => find_args bounds tm
   4.192 +   | Const ("==>", _) $ _ $ _ => find_args bounds tm
   4.193 +   | Const ("==", _) $ _ $ _ => find_args bounds tm
   4.194 +   | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
   4.195 +   | _ => Thm.dest_fun2 tm)
   4.196 +  and find_args bounds tm =
   4.197 +    (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
   4.198 + and find_body bounds b =
   4.199 +   let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
   4.200 +   in h (bounds + 1) b' end;
   4.201 +in h end;
   4.202 +
   4.203 +fun dlo_instance ctxt tm =
   4.204 +  (fst (Langford_Data.get ctxt), 
   4.205 +   Langford_Data.match ctxt (grab_atom_bop 0 tm));
   4.206 +
   4.207 +fun dlo_conv ctxt tm =
   4.208 +  (case dlo_instance ctxt tm of
   4.209 +    (_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm])
   4.210 +  | (ss, SOME instance) => raw_dlo_conv ss instance tm);
   4.211 +
   4.212 +fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
   4.213 + let 
   4.214 +   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
   4.215 +   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
   4.216 +   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
   4.217 +   val p' = fold_rev gen ts p
   4.218 + in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
   4.219 +
   4.220 +
   4.221 +fun cfrees ats ct =
   4.222 + let 
   4.223 +  val ins = insert (op aconvc)
   4.224 +  fun h acc t = 
   4.225 +   case (term_of t) of
   4.226 +    b$_$_ => if member (op aconvc) ats (Thm.dest_fun2 t) 
   4.227 +                then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc) 
   4.228 +                else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
   4.229 +  | _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
   4.230 +  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
   4.231 +  | Free _ => if member (op aconvc) ats t then acc else ins t acc
   4.232 +  | Var _ => if member (op aconvc) ats t then acc else ins t acc
   4.233 +  | _ => acc
   4.234 + in h [] ct end
   4.235 +
   4.236 +fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
   4.237 +  (case dlo_instance ctxt p of
   4.238 +    (ss, NONE) => simp_tac ss i
   4.239 +  | (ss,  SOME instance) =>
   4.240 +      Object_Logic.full_atomize_tac i THEN
   4.241 +      simp_tac ss i
   4.242 +      THEN (CONVERSION Thm.eta_long_conversion) i
   4.243 +      THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
   4.244 +      THEN Object_Logic.full_atomize_tac i
   4.245 +      THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ss instance)) i
   4.246 +      THEN (simp_tac ss i)));  
   4.247 +end;
   4.248 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Decision_Procs/langford_data.ML	Tue May 25 22:21:31 2010 +0200
     5.3 @@ -0,0 +1,113 @@
     5.4 +signature LANGFORD_DATA =
     5.5 +sig
     5.6 +  type entry
     5.7 +  val get: Proof.context -> simpset * (thm * entry) list
     5.8 +  val add: entry -> attribute 
     5.9 +  val del: attribute
    5.10 +  val setup: theory -> theory
    5.11 +  val match: Proof.context -> cterm -> entry option
    5.12 +end;
    5.13 +
    5.14 +structure Langford_Data: LANGFORD_DATA = 
    5.15 +struct
    5.16 +
    5.17 +(* data *)
    5.18 +type entry = {qe_bnds: thm, qe_nolb : thm , qe_noub: thm, 
    5.19 +              gs : thm list, gst : thm, atoms: cterm list};
    5.20 +val eq_key = Thm.eq_thm;
    5.21 +fun eq_data arg = eq_fst eq_key arg;
    5.22 +
    5.23 +structure Data = Generic_Data
    5.24 +(
    5.25 +  type T = simpset * (thm * entry) list;
    5.26 +  val empty = (HOL_basic_ss, []);
    5.27 +  val extend = I;
    5.28 +  fun merge ((ss1, es1), (ss2, es2)) : T =
    5.29 +    (merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2));
    5.30 +);
    5.31 +
    5.32 +val get = Data.get o Context.Proof;
    5.33 +
    5.34 +fun del_data key = apsnd (remove eq_data (key, []));
    5.35 +
    5.36 +val del = Thm.declaration_attribute (Data.map o del_data);
    5.37 +
    5.38 +fun add entry = 
    5.39 +    Thm.declaration_attribute (fn key => fn context => context |> Data.map 
    5.40 +      (del_data key #> apsnd (cons (key, entry))));
    5.41 +
    5.42 +val add_simp = Thm.declaration_attribute (fn th => fn context => 
    5.43 +  context |> Data.map (fn (ss,ts') => (ss addsimps [th], ts'))) 
    5.44 +
    5.45 +val del_simp = Thm.declaration_attribute (fn th => fn context => 
    5.46 +  context |> Data.map (fn (ss,ts') => (ss delsimps [th], ts'))) 
    5.47 +
    5.48 +fun match ctxt tm =
    5.49 +  let
    5.50 +    fun match_inst
    5.51 +        {qe_bnds, qe_nolb, qe_noub, gs, gst, atoms} pat =
    5.52 +       let
    5.53 +        fun h instT =
    5.54 +          let
    5.55 +            val substT = Thm.instantiate (instT, []);
    5.56 +            val substT_cterm = Drule.cterm_rule substT;
    5.57 +
    5.58 +            val qe_bnds' = substT qe_bnds
    5.59 +            val qe_nolb' = substT qe_nolb
    5.60 +            val qe_noub' = substT qe_noub
    5.61 +            val gs' = map substT gs
    5.62 +            val gst' = substT gst
    5.63 +            val atoms' = map substT_cterm atoms
    5.64 +            val result = {qe_bnds = qe_bnds', qe_nolb = qe_nolb', 
    5.65 +                          qe_noub = qe_noub', gs = gs', gst = gst', 
    5.66 +                          atoms = atoms'}
    5.67 +          in SOME result end
    5.68 +      in (case try Thm.match (pat, tm) of
    5.69 +           NONE => NONE
    5.70 +         | SOME (instT, _) => h instT)
    5.71 +      end;
    5.72 +
    5.73 +    fun match_struct (_,
    5.74 +        entry as ({atoms = atoms, ...}): entry) =
    5.75 +      get_first (match_inst entry) atoms;
    5.76 +  in get_first match_struct (snd (get ctxt)) end;
    5.77 +
    5.78 +(* concrete syntax *)
    5.79 +
    5.80 +local
    5.81 +val qeN = "qe";
    5.82 +val gatherN = "gather";
    5.83 +val atomsN = "atoms"
    5.84 +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
    5.85 +val any_keyword =
    5.86 +  keyword qeN || keyword gatherN || keyword atomsN;
    5.87 +
    5.88 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    5.89 +val terms = thms >> map Drule.dest_term;
    5.90 +in
    5.91 +
    5.92 +val langford_setup =
    5.93 +  Attrib.setup @{binding langford}
    5.94 +    ((keyword qeN |-- thms)
    5.95 +     -- (keyword gatherN |-- thms)
    5.96 +     -- (keyword atomsN |-- terms) >>
    5.97 +       (fn ((qes,gs), atoms) => 
    5.98 +       if length qes = 3 andalso length gs > 1 then
    5.99 +         let 
   5.100 +           val [q1,q2,q3] = qes
   5.101 +           val gst::gss = gs
   5.102 +           val entry = {qe_bnds = q1, qe_nolb = q2,
   5.103 +                        qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
   5.104 +         in add entry end
   5.105 +       else error "Need 3 theorems for qe and at least one for gs"))
   5.106 +    "Langford data";
   5.107 +
   5.108 +end;
   5.109 +
   5.110 +(* theory setup *)
   5.111 +
   5.112 +val setup =
   5.113 +  langford_setup #>
   5.114 +  Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset";
   5.115 +
   5.116 +end;
     6.1 --- a/src/HOL/IsaMakefile	Tue May 25 22:12:26 2010 +0200
     6.2 +++ b/src/HOL/IsaMakefile	Tue May 25 22:21:31 2010 +0200
     6.3 @@ -378,10 +378,6 @@
     6.4    Taylor.thy \
     6.5    Transcendental.thy \
     6.6    Tools/float_syntax.ML \
     6.7 -  Tools/Qelim/ferrante_rackoff_data.ML \
     6.8 -  Tools/Qelim/ferrante_rackoff.ML \
     6.9 -  Tools/Qelim/langford_data.ML \
    6.10 -  Tools/Qelim/langford.ML \
    6.11    Tools/SMT/smt_real.ML
    6.12  
    6.13  $(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
    6.14 @@ -826,6 +822,7 @@
    6.15    Decision_Procs/MIR.thy \
    6.16    Decision_Procs/Parametric_Ferrante_Rackoff.thy \
    6.17    Decision_Procs/Polynomial_List.thy \
    6.18 +  Decision_Procs/ROOT.ML \
    6.19    Decision_Procs/Reflected_Multivariate_Polynomial.thy \
    6.20    Decision_Procs/commutative_ring_tac.ML \
    6.21    Decision_Procs/cooper_tac.ML \
    6.22 @@ -833,8 +830,11 @@
    6.23    Decision_Procs/ex/Commutative_Ring_Ex.thy \
    6.24    Decision_Procs/ex/Dense_Linear_Order_Ex.thy \
    6.25    Decision_Procs/ferrack_tac.ML \
    6.26 -  Decision_Procs/mir_tac.ML \
    6.27 -  Decision_Procs/ROOT.ML
    6.28 +  Decision_Procs/ferrante_rackoff.ML \
    6.29 +  Decision_Procs/ferrante_rackoff_data.ML \
    6.30 +  Decision_Procs/langford.ML \
    6.31 +  Decision_Procs/langford_data.ML \
    6.32 +  Decision_Procs/mir_tac.ML
    6.33  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
    6.34  
    6.35  
     7.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Tue May 25 22:12:26 2010 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,233 +0,0 @@
     7.4 -(* Title:      HOL/Tools/Qelim/ferrante_rackoff.ML
     7.5 -   Author:     Amine Chaieb, TU Muenchen
     7.6 -
     7.7 -Ferrante and Rackoff's algorithm for quantifier elimination in dense
     7.8 -linear orders.  Proof-synthesis and tactic.
     7.9 -*)
    7.10 -
    7.11 -signature FERRANTE_RACKOFF =
    7.12 -sig
    7.13 -  val dlo_conv: Proof.context -> conv
    7.14 -  val dlo_tac: Proof.context -> int -> tactic
    7.15 -end;
    7.16 -
    7.17 -structure FerranteRackoff: FERRANTE_RACKOFF =
    7.18 -struct
    7.19 -
    7.20 -open Ferrante_Rackoff_Data;
    7.21 -open Conv;
    7.22 -
    7.23 -type entry = {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list,
    7.24 -   ld: thm list, qe: thm, atoms : cterm list} *
    7.25 -  {isolate_conv: cterm list -> cterm -> thm,
    7.26 -                 whatis : cterm -> cterm -> ord,
    7.27 -                 simpset : simpset};
    7.28 -
    7.29 -fun get_p1 th =
    7.30 -  funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
    7.31 -    (funpow 2 Thm.dest_arg (cprop_of th)) |> Thm.dest_arg
    7.32 -
    7.33 -fun ferrack_conv
    7.34 -   (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi,
    7.35 -              ld = ld, qe = qe, atoms = atoms},
    7.36 -             {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
    7.37 -let
    7.38 - fun uset (vars as (x::vs)) p = case term_of p of
    7.39 -   Const("op &", _)$ _ $ _ =>
    7.40 -     let
    7.41 -       val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    7.42 -       val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    7.43 -     in (lS@rS, Drule.binop_cong_rule b lth rth) end
    7.44 - |  Const("op |", _)$ _ $ _ =>
    7.45 -     let
    7.46 -       val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    7.47 -       val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    7.48 -     in (lS@rS, Drule.binop_cong_rule b lth rth) end
    7.49 - | _ =>
    7.50 -    let
    7.51 -      val th = icv vars p
    7.52 -      val p' = Thm.rhs_of th
    7.53 -      val c = wi x p'
    7.54 -      val S = (if member (op =) [Lt, Le, Eq] c then single o Thm.dest_arg
    7.55 -               else if member (op =) [Gt, Ge] c then single o Thm.dest_arg1
    7.56 -               else if c = NEq then single o Thm.dest_arg o Thm.dest_arg
    7.57 -               else K []) p'
    7.58 -    in (S,th) end
    7.59 -
    7.60 - val ((p1_v,p2_v),(mp1_v,mp2_v)) =
    7.61 -   funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
    7.62 -     (funpow 4 Thm.dest_arg (cprop_of (hd minf)))
    7.63 -   |> Thm.dest_binop |> pairself Thm.dest_binop |> apfst (pairself Thm.dest_fun)
    7.64 -
    7.65 - fun myfwd (th1, th2, th3, th4, th5) p1 p2
    7.66 -      [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] =
    7.67 -  let
    7.68 -   val (mp1, mp2) = (get_p1 th_1, get_p1 th_1')
    7.69 -   val (pp1, pp2) = (get_p1 th_2, get_p1 th_2')
    7.70 -   fun fw mi th th' th'' =
    7.71 -     let
    7.72 -      val th0 = if mi then
    7.73 -           instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
    7.74 -        else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
    7.75 -     in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
    7.76 -  in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
    7.77 -      fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
    7.78 -  end
    7.79 - val U_v = (Thm.dest_arg o Thm.dest_arg o Thm.dest_arg1) (cprop_of qe)
    7.80 - fun main vs p =
    7.81 -  let
    7.82 -   val ((xn,ce),(x,fm)) = (case term_of p of
    7.83 -                   Const("Ex",_)$Abs(xn,xT,_) =>
    7.84 -                        Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
    7.85 -                 | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    7.86 -   val cT = ctyp_of_term x
    7.87 -   val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc)
    7.88 -   val nthx = Thm.abstract_rule xn x nth
    7.89 -   val q = Thm.rhs_of nth
    7.90 -   val qx = Thm.rhs_of nthx
    7.91 -   val enth = Drule.arg_cong_rule ce nthx
    7.92 -   val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
    7.93 -   fun ins x th =
    7.94 -      Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
    7.95 -                                       (Thm.cprop_of th), SOME x] th1) th
    7.96 -   val fU = fold ins u th0
    7.97 -   val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU)
    7.98 -   local
    7.99 -     val insI1 = instantiate' [SOME cT] [] @{thm "insertI1"}
   7.100 -     val insI2 = instantiate' [SOME cT] [] @{thm "insertI2"}
   7.101 -   in
   7.102 -    fun provein x S =
   7.103 -     case term_of S of
   7.104 -        Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S])
   7.105 -      | Const(@{const_name insert}, _) $ y $_ =>
   7.106 -         let val (cy,S') = Thm.dest_binop S
   7.107 -         in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
   7.108 -         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   7.109 -                           (provein x S')
   7.110 -         end
   7.111 -   end
   7.112 -   val tabU = fold (fn t => fn tab => Termtab.update (term_of t, provein t cU) tab)
   7.113 -                   u Termtab.empty
   7.114 -   val U = the o Termtab.lookup tabU o term_of
   7.115 -   val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt,
   7.116 -        minf_le, minf_gt, minf_ge, minf_P] = minf
   7.117 -   val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt,
   7.118 -        pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf
   7.119 -   val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt,
   7.120 -        nmi_le, nmi_gt, nmi_ge, nmi_P] = map (instantiate ([],[(U_v,cU)])) nmi
   7.121 -   val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt,
   7.122 -        npi_le, npi_gt, npi_ge, npi_P] = map (instantiate ([],[(U_v,cU)])) npi
   7.123 -   val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
   7.124 -        ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld
   7.125 -
   7.126 -   fun decomp_mpinf fm =
   7.127 -     case term_of fm of
   7.128 -       Const("op &",_)$_$_ =>
   7.129 -        let val (p,q) = Thm.dest_binop fm
   7.130 -        in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
   7.131 -                         (Thm.cabs x p) (Thm.cabs x q))
   7.132 -        end
   7.133 -     | Const("op |",_)$_$_ =>
   7.134 -        let val (p,q) = Thm.dest_binop fm
   7.135 -        in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
   7.136 -                         (Thm.cabs x p) (Thm.cabs x q))
   7.137 -        end
   7.138 -     | _ =>
   7.139 -        (let val c = wi x fm
   7.140 -             val t = (if c=Nox then I
   7.141 -                      else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg
   7.142 -                      else if member (op =) [Gt, Ge] c then Thm.dest_arg1
   7.143 -                      else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
   7.144 -                      else sys_error "decomp_mpinf: Impossible case!!") fm
   7.145 -             val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
   7.146 -               if c = Nox then map (instantiate' [] [SOME fm])
   7.147 -                                    [minf_P, pinf_P, nmi_P, npi_P, ld_P]
   7.148 -               else
   7.149 -                let val [mi_th,pi_th,nmi_th,npi_th,ld_th] =
   7.150 -                 map (instantiate' [] [SOME t])
   7.151 -                 (case c of Lt => [minf_lt, pinf_lt, nmi_lt, npi_lt, ld_lt]
   7.152 -                          | Le => [minf_le, pinf_le, nmi_le, npi_le, ld_le]
   7.153 -                          | Gt => [minf_gt, pinf_gt, nmi_gt, npi_gt, ld_gt]
   7.154 -                          | Ge => [minf_ge, pinf_ge, nmi_ge, npi_ge, ld_ge]
   7.155 -                          | Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq]
   7.156 -                          | NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq])
   7.157 -                    val tU = U t
   7.158 -                    fun Ufw th = Thm.implies_elim th tU
   7.159 -                 in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th]
   7.160 -                 end
   7.161 -         in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end)
   7.162 -   val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q
   7.163 -   val qe_th = Drule.implies_elim_list
   7.164 -                  ((fconv_rule (Thm.beta_conversion true))
   7.165 -                   (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
   7.166 -                        qe))
   7.167 -                  [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
   7.168 -    val bex_conv =
   7.169 -      Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)}))
   7.170 -    val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
   7.171 -   in result_th
   7.172 -   end
   7.173 -
   7.174 -in main
   7.175 -end;
   7.176 -
   7.177 -val grab_atom_bop =
   7.178 - let
   7.179 -  fun h bounds tm =
   7.180 -   (case term_of tm of
   7.181 -     Const ("op =", T) $ _ $ _ =>
   7.182 -       if domain_type T = HOLogic.boolT then find_args bounds tm
   7.183 -       else Thm.dest_fun2 tm
   7.184 -   | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
   7.185 -   | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
   7.186 -   | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
   7.187 -   | Const ("op &", _) $ _ $ _ => find_args bounds tm
   7.188 -   | Const ("op |", _) $ _ $ _ => find_args bounds tm
   7.189 -   | Const ("op -->", _) $ _ $ _ => find_args bounds tm
   7.190 -   | Const ("==>", _) $ _ $ _ => find_args bounds tm
   7.191 -   | Const ("==", _) $ _ $ _ => find_args bounds tm
   7.192 -   | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
   7.193 -   | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
   7.194 -   | _ => Thm.dest_fun2 tm)
   7.195 -  and find_args bounds tm =
   7.196 -           (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
   7.197 - and find_body bounds b =
   7.198 -   let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
   7.199 -   in h (bounds + 1) b' end;
   7.200 -in h end;
   7.201 -
   7.202 -fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset}) tm =
   7.203 - let
   7.204 -   val ss = simpset
   7.205 -   val ss' =
   7.206 -     merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
   7.207 -              @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss)
   7.208 -     |> Simplifier.inherit_context ss
   7.209 -   val pcv = Simplifier.rewrite ss'     
   7.210 -   val postcv = Simplifier.rewrite ss
   7.211 -   val nnf = K (nnf_conv then_conv postcv)
   7.212 -   val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm [])
   7.213 -                  (isolate_conv ctxt) nnf
   7.214 -                  (fn vs => ferrack_conv (thy,{isolate_conv = isolate_conv ctxt,
   7.215 -                                               whatis = whatis, simpset = simpset}) vs
   7.216 -                   then_conv postcv)
   7.217 - in (Simplifier.rewrite ss then_conv qe_conv) tm end;
   7.218 -
   7.219 -fun dlo_instance ctxt tm =
   7.220 -  Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm);
   7.221 -
   7.222 -fun dlo_conv ctxt tm =
   7.223 -  (case dlo_instance ctxt tm of
   7.224 -    NONE => raise CTERM ("ferrackqe_conv: no corresponding instance in context!", [tm])
   7.225 -  | SOME instance => raw_ferrack_qe_conv ctxt instance tm);
   7.226 -
   7.227 -fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
   7.228 -  (case dlo_instance ctxt p of
   7.229 -    NONE => no_tac
   7.230 -  | SOME instance =>
   7.231 -      Object_Logic.full_atomize_tac i THEN
   7.232 -      simp_tac (#simpset (snd instance)) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
   7.233 -      CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
   7.234 -      simp_tac (simpset_of ctxt) i));  (* FIXME really? *)
   7.235 -
   7.236 -end;
     8.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Tue May 25 22:12:26 2010 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,146 +0,0 @@
     8.4 -(* Title:      HOL/Tools/Qelim/ferrante_rackoff_data.ML
     8.5 -   Author:     Amine Chaieb, TU Muenchen
     8.6 -
     8.7 -Context data for Ferrante and Rackoff's algorithm for quantifier
     8.8 -elimination in dense linear orders.
     8.9 -*)
    8.10 -
    8.11 -signature FERRANTE_RACKOF_DATA =
    8.12 -sig
    8.13 -  datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox
    8.14 -  type entry
    8.15 -  val get: Proof.context -> (thm * entry) list
    8.16 -  val del: attribute
    8.17 -  val add: entry -> attribute 
    8.18 -  val funs: thm -> 
    8.19 -    {isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm,
    8.20 -     whatis: morphism -> cterm -> cterm -> ord,
    8.21 -     simpset: morphism -> simpset} -> declaration
    8.22 -  val match: Proof.context -> cterm -> entry option
    8.23 -  val setup: theory -> theory
    8.24 -end;
    8.25 -
    8.26 -structure Ferrante_Rackoff_Data: FERRANTE_RACKOF_DATA = 
    8.27 -struct
    8.28 -
    8.29 -(* data *)
    8.30 -
    8.31 -datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox
    8.32 -
    8.33 -type entry = 
    8.34 -  {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list,  
    8.35 -   ld: thm list, qe: thm, atoms : cterm list} *
    8.36 -   {isolate_conv: Proof.context -> cterm list -> cterm -> thm, 
    8.37 -    whatis : cterm -> cterm -> ord, 
    8.38 -    simpset : simpset};
    8.39 -
    8.40 -val eq_key = Thm.eq_thm;
    8.41 -fun eq_data arg = eq_fst eq_key arg;
    8.42 -
    8.43 -structure Data = Generic_Data
    8.44 -(
    8.45 -  type T = (thm * entry) list;
    8.46 -  val empty = [];
    8.47 -  val extend = I;
    8.48 -  fun merge data : T = AList.merge eq_key (K true) data;
    8.49 -);
    8.50 -
    8.51 -val get = Data.get o Context.Proof;
    8.52 -
    8.53 -fun del_data key = remove eq_data (key, []);
    8.54 -
    8.55 -val del = Thm.declaration_attribute (Data.map o del_data);
    8.56 -
    8.57 -fun add entry = 
    8.58 -    Thm.declaration_attribute (fn key => fn context => context |> Data.map 
    8.59 -      (del_data key #> cons (key, entry)));
    8.60 -
    8.61 -
    8.62 -(* extra-logical functions *)
    8.63 -
    8.64 -fun funs raw_key {isolate_conv = icv, whatis = wi, simpset = ss} phi = Data.map (fn data =>
    8.65 -  let
    8.66 -    val key = Morphism.thm phi raw_key;
    8.67 -    val _ = AList.defined eq_key data key orelse
    8.68 -      raise THM ("No data entry for structure key", 0, [key]);
    8.69 -    val fns = {isolate_conv = icv phi, whatis = wi phi, simpset = ss phi};
    8.70 -  in AList.map_entry eq_key key (apsnd (K fns)) data end);
    8.71 -
    8.72 -fun match ctxt tm =
    8.73 -  let
    8.74 -    fun match_inst
    8.75 -        ({minf, pinf, nmi, npi, ld, qe, atoms},
    8.76 -         fns as {isolate_conv, whatis, simpset}) pat =
    8.77 -       let
    8.78 -        fun h instT =
    8.79 -          let
    8.80 -            val substT = Thm.instantiate (instT, []);
    8.81 -            val substT_cterm = Drule.cterm_rule substT;
    8.82 -
    8.83 -            val minf' = map substT minf
    8.84 -            val pinf' = map substT pinf
    8.85 -            val nmi' = map substT nmi
    8.86 -            val npi' = map substT npi
    8.87 -            val ld' = map substT ld
    8.88 -            val qe' = substT qe
    8.89 -            val atoms' = map substT_cterm atoms
    8.90 -            val result = ({minf = minf', pinf = pinf', nmi = nmi', npi = npi', 
    8.91 -                           ld = ld', qe = qe', atoms = atoms'}, fns)
    8.92 -          in SOME result end
    8.93 -      in (case try Thm.match (pat, tm) of
    8.94 -           NONE => NONE
    8.95 -         | SOME (instT, _) => h instT)
    8.96 -      end;
    8.97 -
    8.98 -    fun match_struct (_,
    8.99 -        entry as ({atoms = atoms, ...}, _): entry) =
   8.100 -      get_first (match_inst entry) atoms;
   8.101 -  in get_first match_struct (get ctxt) end;
   8.102 -
   8.103 -
   8.104 -(* concrete syntax *)
   8.105 -
   8.106 -local
   8.107 -val minfN = "minf";
   8.108 -val pinfN = "pinf";
   8.109 -val nmiN = "nmi";
   8.110 -val npiN = "npi";
   8.111 -val lin_denseN = "lindense";
   8.112 -val qeN = "qe"
   8.113 -val atomsN = "atoms"
   8.114 -val simpsN = "simps"
   8.115 -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   8.116 -val any_keyword =
   8.117 -  keyword minfN || keyword pinfN || keyword nmiN 
   8.118 -|| keyword npiN || keyword lin_denseN || keyword qeN 
   8.119 -|| keyword atomsN || keyword simpsN;
   8.120 -
   8.121 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   8.122 -val terms = thms >> map Drule.dest_term;
   8.123 -in
   8.124 -
   8.125 -val ferrak_setup =
   8.126 -  Attrib.setup @{binding ferrack}
   8.127 -    ((keyword minfN |-- thms)
   8.128 -     -- (keyword pinfN |-- thms)
   8.129 -     -- (keyword nmiN |-- thms)
   8.130 -     -- (keyword npiN |-- thms)
   8.131 -     -- (keyword lin_denseN |-- thms)
   8.132 -     -- (keyword qeN |-- thms)
   8.133 -     -- (keyword atomsN |-- terms) >>
   8.134 -       (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> 
   8.135 -       if length qe = 1 then
   8.136 -         add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
   8.137 -              qe = hd qe, atoms = atoms},
   8.138 -             {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
   8.139 -       else error "only one theorem for qe!"))
   8.140 -    "Ferrante Rackoff data";
   8.141 -
   8.142 -end;
   8.143 -
   8.144 -
   8.145 -(* theory setup *)
   8.146 -
   8.147 -val setup = ferrak_setup;
   8.148 -
   8.149 -end;
     9.1 --- a/src/HOL/Tools/Qelim/langford.ML	Tue May 25 22:12:26 2010 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,244 +0,0 @@
     9.4 -(*  Title:      HOL/Tools/Qelim/langford.ML
     9.5 -    Author:     Amine Chaieb, TU Muenchen
     9.6 -*)
     9.7 -
     9.8 -signature LANGFORD_QE = 
     9.9 -sig
    9.10 -  val dlo_tac : Proof.context -> int -> tactic
    9.11 -  val dlo_conv : Proof.context -> cterm -> thm
    9.12 -end
    9.13 -
    9.14 -structure LangfordQE :LANGFORD_QE = 
    9.15 -struct
    9.16 -
    9.17 -val dest_set =
    9.18 - let 
    9.19 -  fun h acc ct = 
    9.20 -   case term_of ct of
    9.21 -     Const (@{const_name Orderings.bot}, _) => acc
    9.22 -   | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
    9.23 -in h [] end;
    9.24 -
    9.25 -fun prove_finite cT u = 
    9.26 -let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
    9.27 -    fun ins x th =
    9.28 -     Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
    9.29 -                                     (Thm.cprop_of th), SOME x] th1) th
    9.30 -in fold ins u th0 end;
    9.31 -
    9.32 -val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms))));
    9.33 -
    9.34 -fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = 
    9.35 - case term_of ep of 
    9.36 -  Const("Ex",_)$_ => 
    9.37 -   let 
    9.38 -     val p = Thm.dest_arg ep
    9.39 -     val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid)
    9.40 -     val (L,U) = 
    9.41 -       let 
    9.42 -         val (x,q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
    9.43 -       in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1)
    9.44 -       end
    9.45 -     fun proveneF S =         
    9.46 -       let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg
    9.47 -           val cT = ctyp_of_term a
    9.48 -           val ne = instantiate' [SOME cT] [SOME a, SOME A] 
    9.49 -                    @{thm insert_not_empty}
    9.50 -           val f = prove_finite cT (dest_set S)
    9.51 -       in (ne, f) end
    9.52 -
    9.53 -     val qe = case (term_of L, term_of U) of 
    9.54 -      (Const (@{const_name Orderings.bot}, _),_) =>  
    9.55 -        let
    9.56 -          val (neU,fU) = proveneF U 
    9.57 -        in simp_rule (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
    9.58 -    | (_,Const (@{const_name Orderings.bot}, _)) =>  
    9.59 -        let
    9.60 -          val (neL,fL) = proveneF L
    9.61 -        in simp_rule (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
    9.62 -
    9.63 -    | (_,_) =>  
    9.64 -      let 
    9.65 -       val (neL,fL) = proveneF L
    9.66 -       val (neU,fU) = proveneF U
    9.67 -      in simp_rule (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) 
    9.68 -      end
    9.69 -   in qe end 
    9.70 - | _ => error "dlo_qe : Not an existential formula";
    9.71 -
    9.72 -val all_conjuncts = 
    9.73 - let fun h acc ct = 
    9.74 -  case term_of ct of
    9.75 -   @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
    9.76 -  | _ => ct::acc
    9.77 -in h [] end;
    9.78 -
    9.79 -fun conjuncts ct =
    9.80 - case term_of ct of
    9.81 -  @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
    9.82 -| _ => [ct];
    9.83 -
    9.84 -fun fold1 f = foldr1 (uncurry f);
    9.85 -
    9.86 -val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
    9.87 -
    9.88 -fun mk_conj_tab th = 
    9.89 - let fun h acc th = 
    9.90 -   case prop_of th of
    9.91 -   @{term "Trueprop"}$(@{term "op &"}$p$q) => 
    9.92 -     h (h acc (th RS conjunct2)) (th RS conjunct1)
    9.93 -  | @{term "Trueprop"}$p => (p,th)::acc
    9.94 -in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
    9.95 -
    9.96 -fun is_conj (@{term "op &"}$_$_) = true
    9.97 -  | is_conj _ = false;
    9.98 -
    9.99 -fun prove_conj tab cjs = 
   9.100 - case cjs of 
   9.101 -   [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c
   9.102 - | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs];
   9.103 -
   9.104 -fun conj_aci_rule eq = 
   9.105 - let 
   9.106 -  val (l,r) = Thm.dest_equals eq
   9.107 -  fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
   9.108 -  fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
   9.109 -  val ll = Thm.dest_arg l
   9.110 -  val rr = Thm.dest_arg r
   9.111 -  
   9.112 -  val thl  = prove_conj tabl (conjuncts rr) 
   9.113 -                |> Drule.implies_intr_hyps
   9.114 -  val thr  = prove_conj tabr (conjuncts ll) 
   9.115 -                |> Drule.implies_intr_hyps
   9.116 -  val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
   9.117 - in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
   9.118 -
   9.119 -fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
   9.120 -
   9.121 -fun is_eqx x eq = case term_of eq of
   9.122 -   Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x
   9.123 - | _ => false ;
   9.124 -
   9.125 -local 
   9.126 -fun proc ct = 
   9.127 - case term_of ct of
   9.128 -  Const("Ex",_)$Abs (xn,_,_) => 
   9.129 -   let 
   9.130 -    val e = Thm.dest_fun ct
   9.131 -    val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
   9.132 -    val Pp = Thm.capply @{cterm "Trueprop"} p 
   9.133 -    val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
   9.134 -   in case eqs of
   9.135 -      [] => 
   9.136 -        let 
   9.137 -         val (dx,ndx) = List.partition (contains x) neqs
   9.138 -         in case ndx of [] => NONE
   9.139 -                      | _ =>
   9.140 -            conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
   9.141 -                 (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx))))
   9.142 -           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
   9.143 -           |> Conv.fconv_rule (Conv.arg_conv 
   9.144 -                   (Simplifier.rewrite 
   9.145 -                      (HOL_basic_ss addsimps (simp_thms @ ex_simps))))
   9.146 -           |> SOME
   9.147 -          end
   9.148 -    | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
   9.149 -                 (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs))))
   9.150 -           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
   9.151 -           |> Conv.fconv_rule (Conv.arg_conv 
   9.152 -                   (Simplifier.rewrite 
   9.153 -                (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) 
   9.154 -           |> SOME
   9.155 -   end
   9.156 - | _ => NONE;
   9.157 -in val reduce_ex_simproc = 
   9.158 -  Simplifier.make_simproc 
   9.159 -  {lhss = [@{cpat "EX x. ?P x"}] , name = "reduce_ex_simproc",
   9.160 -   proc = K (K proc) , identifier = []}
   9.161 -end;
   9.162 -
   9.163 -fun raw_dlo_conv dlo_ss 
   9.164 -          ({qe_bnds, qe_nolb, qe_noub, gst, gs, atoms}:Langford_Data.entry) = 
   9.165 - let 
   9.166 -  val ss = dlo_ss addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc]
   9.167 -  val dnfex_conv = Simplifier.rewrite ss
   9.168 -   val pcv = Simplifier.rewrite
   9.169 -               (dlo_ss addsimps (simp_thms @ ex_simps @ all_simps)
   9.170 -                @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib])
   9.171 - in fn p => 
   9.172 -   Qelim.gen_qelim_conv pcv pcv dnfex_conv cons 
   9.173 -                  (Thm.add_cterm_frees p [])  (K Thm.reflexive) (K Thm.reflexive)
   9.174 -                  (K (basic_dloqe () gst qe_bnds qe_nolb qe_noub gs)) p
   9.175 - end;
   9.176 -
   9.177 -
   9.178 -val grab_atom_bop =
   9.179 - let
   9.180 -  fun h bounds tm =
   9.181 -   (case term_of tm of
   9.182 -     Const ("op =", T) $ _ $ _ =>
   9.183 -       if domain_type T = HOLogic.boolT then find_args bounds tm
   9.184 -       else Thm.dest_fun2 tm
   9.185 -   | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
   9.186 -   | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
   9.187 -   | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
   9.188 -   | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
   9.189 -   | Const ("op &", _) $ _ $ _ => find_args bounds tm
   9.190 -   | Const ("op |", _) $ _ $ _ => find_args bounds tm
   9.191 -   | Const ("op -->", _) $ _ $ _ => find_args bounds tm
   9.192 -   | Const ("==>", _) $ _ $ _ => find_args bounds tm
   9.193 -   | Const ("==", _) $ _ $ _ => find_args bounds tm
   9.194 -   | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
   9.195 -   | _ => Thm.dest_fun2 tm)
   9.196 -  and find_args bounds tm =
   9.197 -    (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
   9.198 - and find_body bounds b =
   9.199 -   let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
   9.200 -   in h (bounds + 1) b' end;
   9.201 -in h end;
   9.202 -
   9.203 -fun dlo_instance ctxt tm =
   9.204 -  (fst (Langford_Data.get ctxt), 
   9.205 -   Langford_Data.match ctxt (grab_atom_bop 0 tm));
   9.206 -
   9.207 -fun dlo_conv ctxt tm =
   9.208 -  (case dlo_instance ctxt tm of
   9.209 -    (_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm])
   9.210 -  | (ss, SOME instance) => raw_dlo_conv ss instance tm);
   9.211 -
   9.212 -fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
   9.213 - let 
   9.214 -   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
   9.215 -   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
   9.216 -   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
   9.217 -   val p' = fold_rev gen ts p
   9.218 - in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
   9.219 -
   9.220 -
   9.221 -fun cfrees ats ct =
   9.222 - let 
   9.223 -  val ins = insert (op aconvc)
   9.224 -  fun h acc t = 
   9.225 -   case (term_of t) of
   9.226 -    b$_$_ => if member (op aconvc) ats (Thm.dest_fun2 t) 
   9.227 -                then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc) 
   9.228 -                else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
   9.229 -  | _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
   9.230 -  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
   9.231 -  | Free _ => if member (op aconvc) ats t then acc else ins t acc
   9.232 -  | Var _ => if member (op aconvc) ats t then acc else ins t acc
   9.233 -  | _ => acc
   9.234 - in h [] ct end
   9.235 -
   9.236 -fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
   9.237 -  (case dlo_instance ctxt p of
   9.238 -    (ss, NONE) => simp_tac ss i
   9.239 -  | (ss,  SOME instance) =>
   9.240 -      Object_Logic.full_atomize_tac i THEN
   9.241 -      simp_tac ss i
   9.242 -      THEN (CONVERSION Thm.eta_long_conversion) i
   9.243 -      THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
   9.244 -      THEN Object_Logic.full_atomize_tac i
   9.245 -      THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ss instance)) i
   9.246 -      THEN (simp_tac ss i)));  
   9.247 -end;
   9.248 \ No newline at end of file
    10.1 --- a/src/HOL/Tools/Qelim/langford_data.ML	Tue May 25 22:12:26 2010 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,113 +0,0 @@
    10.4 -signature LANGFORD_DATA =
    10.5 -sig
    10.6 -  type entry
    10.7 -  val get: Proof.context -> simpset * (thm * entry) list
    10.8 -  val add: entry -> attribute 
    10.9 -  val del: attribute
   10.10 -  val setup: theory -> theory
   10.11 -  val match: Proof.context -> cterm -> entry option
   10.12 -end;
   10.13 -
   10.14 -structure Langford_Data: LANGFORD_DATA = 
   10.15 -struct
   10.16 -
   10.17 -(* data *)
   10.18 -type entry = {qe_bnds: thm, qe_nolb : thm , qe_noub: thm, 
   10.19 -              gs : thm list, gst : thm, atoms: cterm list};
   10.20 -val eq_key = Thm.eq_thm;
   10.21 -fun eq_data arg = eq_fst eq_key arg;
   10.22 -
   10.23 -structure Data = Generic_Data
   10.24 -(
   10.25 -  type T = simpset * (thm * entry) list;
   10.26 -  val empty = (HOL_basic_ss, []);
   10.27 -  val extend = I;
   10.28 -  fun merge ((ss1, es1), (ss2, es2)) : T =
   10.29 -    (merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2));
   10.30 -);
   10.31 -
   10.32 -val get = Data.get o Context.Proof;
   10.33 -
   10.34 -fun del_data key = apsnd (remove eq_data (key, []));
   10.35 -
   10.36 -val del = Thm.declaration_attribute (Data.map o del_data);
   10.37 -
   10.38 -fun add entry = 
   10.39 -    Thm.declaration_attribute (fn key => fn context => context |> Data.map 
   10.40 -      (del_data key #> apsnd (cons (key, entry))));
   10.41 -
   10.42 -val add_simp = Thm.declaration_attribute (fn th => fn context => 
   10.43 -  context |> Data.map (fn (ss,ts') => (ss addsimps [th], ts'))) 
   10.44 -
   10.45 -val del_simp = Thm.declaration_attribute (fn th => fn context => 
   10.46 -  context |> Data.map (fn (ss,ts') => (ss delsimps [th], ts'))) 
   10.47 -
   10.48 -fun match ctxt tm =
   10.49 -  let
   10.50 -    fun match_inst
   10.51 -        {qe_bnds, qe_nolb, qe_noub, gs, gst, atoms} pat =
   10.52 -       let
   10.53 -        fun h instT =
   10.54 -          let
   10.55 -            val substT = Thm.instantiate (instT, []);
   10.56 -            val substT_cterm = Drule.cterm_rule substT;
   10.57 -
   10.58 -            val qe_bnds' = substT qe_bnds
   10.59 -            val qe_nolb' = substT qe_nolb
   10.60 -            val qe_noub' = substT qe_noub
   10.61 -            val gs' = map substT gs
   10.62 -            val gst' = substT gst
   10.63 -            val atoms' = map substT_cterm atoms
   10.64 -            val result = {qe_bnds = qe_bnds', qe_nolb = qe_nolb', 
   10.65 -                          qe_noub = qe_noub', gs = gs', gst = gst', 
   10.66 -                          atoms = atoms'}
   10.67 -          in SOME result end
   10.68 -      in (case try Thm.match (pat, tm) of
   10.69 -           NONE => NONE
   10.70 -         | SOME (instT, _) => h instT)
   10.71 -      end;
   10.72 -
   10.73 -    fun match_struct (_,
   10.74 -        entry as ({atoms = atoms, ...}): entry) =
   10.75 -      get_first (match_inst entry) atoms;
   10.76 -  in get_first match_struct (snd (get ctxt)) end;
   10.77 -
   10.78 -(* concrete syntax *)
   10.79 -
   10.80 -local
   10.81 -val qeN = "qe";
   10.82 -val gatherN = "gather";
   10.83 -val atomsN = "atoms"
   10.84 -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   10.85 -val any_keyword =
   10.86 -  keyword qeN || keyword gatherN || keyword atomsN;
   10.87 -
   10.88 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   10.89 -val terms = thms >> map Drule.dest_term;
   10.90 -in
   10.91 -
   10.92 -val langford_setup =
   10.93 -  Attrib.setup @{binding langford}
   10.94 -    ((keyword qeN |-- thms)
   10.95 -     -- (keyword gatherN |-- thms)
   10.96 -     -- (keyword atomsN |-- terms) >>
   10.97 -       (fn ((qes,gs), atoms) => 
   10.98 -       if length qes = 3 andalso length gs > 1 then
   10.99 -         let 
  10.100 -           val [q1,q2,q3] = qes
  10.101 -           val gst::gss = gs
  10.102 -           val entry = {qe_bnds = q1, qe_nolb = q2,
  10.103 -                        qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
  10.104 -         in add entry end
  10.105 -       else error "Need 3 theorems for qe and at least one for gs"))
  10.106 -    "Langford data";
  10.107 -
  10.108 -end;
  10.109 -
  10.110 -(* theory setup *)
  10.111 -
  10.112 -val setup =
  10.113 -  langford_setup #>
  10.114 -  Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset";
  10.115 -
  10.116 -end;