# HG changeset patch # User wenzelm # Date 1274818891 -7200 # Node ID 5df087c6ce94962144b0a34e6df4a7c765cfe30f # Parent b36a5512c5fbe277af10bf6b3dcbc7885eaacab5 moved ML files where they are actually used; more precise dependencies; diff -r b36a5512c5fb -r 5df087c6ce94 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue May 25 22:12:26 2010 +0200 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue May 25 22:21:31 2010 +0200 @@ -8,10 +8,10 @@ theory Dense_Linear_Order imports Main uses - "~~/src/HOL/Tools/Qelim/langford_data.ML" - "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML" - ("~~/src/HOL/Tools/Qelim/langford.ML") - ("~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML") + "langford_data.ML" + "ferrante_rackoff_data.ML" + ("langford.ML") + ("ferrante_rackoff.ML") begin setup {* Langford_Data.setup #> Ferrante_Rackoff_Data.setup *} @@ -293,7 +293,7 @@ lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib -use "~~/src/HOL/Tools/Qelim/langford.ML" +use "langford.ML" method_setup dlo = {* Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac) *} "Langford's algorithm for quantifier elimination in dense linear orders" @@ -543,7 +543,7 @@ end -use "~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML" +use "ferrante_rackoff.ML" method_setup ferrack = {* Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac) diff -r b36a5512c5fb -r 5df087c6ce94 src/HOL/Decision_Procs/ferrante_rackoff.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Tue May 25 22:21:31 2010 +0200 @@ -0,0 +1,233 @@ +(* Title: HOL/Tools/Qelim/ferrante_rackoff.ML + Author: Amine Chaieb, TU Muenchen + +Ferrante and Rackoff's algorithm for quantifier elimination in dense +linear orders. Proof-synthesis and tactic. +*) + +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, + ld: thm list, qe: thm, atoms : cterm list} * + {isolate_conv: cterm list -> cterm -> thm, + whatis : cterm -> cterm -> ord, + simpset : simpset}; + +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, + ld = ld, qe = qe, atoms = atoms}, + {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 + val (lS,lth) = uset vars l val (rS, rth) = uset vars r + 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, 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 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)) = + 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 + 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 + 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 Thm.implies_elim (Thm.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') + 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,_) => + Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn + | _ => 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 = + Thm.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 + val insI1 = instantiate' [SOME cT] [] @{thm "insertI1"} + val insI2 = instantiate' [SOME cT] [] @{thm "insertI2"} + in + fun provein x S = + case term_of S of + Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S]) + | Const(@{const_name 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 Thm.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) + u Termtab.empty + 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, + pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf + 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, + 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, + ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld + + 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) + (Thm.cabs x p) (Thm.cabs x q)) + end + | 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 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] = + 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] + | Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq] + | NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq]) + val tU = U t + fun Ufw th = Thm.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 = Drule.implies_elim_list + ((fconv_rule (Thm.beta_conversion true)) + (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th]) + qe)) + [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) (Thm.transitive enth qe_th) + in result_th + end + +in main +end; + +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 + 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 ("op -->", _) $ _ $ _ => find_args bounds tm + | Const ("==>", _) $ _ $ _ => find_args bounds tm + | Const ("==", _) $ _ $ _ => find_args bounds tm + | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm) + | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm) + | _ => Thm.dest_fun2 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 + val ss = simpset + 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, + whatis = whatis, simpset = simpset}) vs + then_conv postcv) + in (Simplifier.rewrite ss then_conv qe_conv) tm 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 => + Object_Logic.full_atomize_tac i THEN + simp_tac (#simpset (snd instance)) i THEN (* FIXME already part of raw_ferrack_qe_conv? *) + CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN + simp_tac (simpset_of ctxt) i)); (* FIXME really? *) + +end; diff -r b36a5512c5fb -r 5df087c6ce94 src/HOL/Decision_Procs/ferrante_rackoff_data.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Tue May 25 22:21:31 2010 +0200 @@ -0,0 +1,146 @@ +(* Title: HOL/Tools/Qelim/ferrante_rackoff_data.ML + Author: Amine Chaieb, TU Muenchen + +Context data for Ferrante and Rackoff's algorithm for quantifier +elimination in dense linear orders. +*) + +signature FERRANTE_RACKOF_DATA = +sig + datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox + type entry + val get: Proof.context -> (thm * entry) list + val del: attribute + val add: entry -> attribute + val funs: thm -> + {isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm, + whatis: morphism -> cterm -> cterm -> ord, + simpset: morphism -> simpset} -> declaration + val match: Proof.context -> cterm -> entry option + val setup: theory -> theory +end; + +structure Ferrante_Rackoff_Data: FERRANTE_RACKOF_DATA = +struct + +(* data *) + +datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox + +type entry = + {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list, + ld: thm list, qe: thm, atoms : cterm list} * + {isolate_conv: Proof.context -> cterm list -> cterm -> thm, + whatis : cterm -> cterm -> ord, + simpset : simpset}; + +val eq_key = Thm.eq_thm; +fun eq_data arg = eq_fst eq_key arg; + +structure Data = Generic_Data +( + type T = (thm * entry) list; + val empty = []; + val extend = I; + fun merge data : T = AList.merge eq_key (K true) data; +); + +val get = Data.get o Context.Proof; + +fun del_data key = remove eq_data (key, []); + +val del = Thm.declaration_attribute (Data.map o del_data); + +fun add entry = + Thm.declaration_attribute (fn key => fn context => context |> Data.map + (del_data key #> cons (key, entry))); + + +(* extra-logical functions *) + +fun funs raw_key {isolate_conv = icv, whatis = wi, simpset = ss} phi = Data.map (fn data => + let + val key = Morphism.thm phi raw_key; + val _ = AList.defined eq_key data key orelse + raise THM ("No data entry for structure key", 0, [key]); + val fns = {isolate_conv = icv phi, whatis = wi phi, simpset = ss phi}; + in AList.map_entry eq_key key (apsnd (K fns)) data end); + +fun match ctxt tm = + let + fun match_inst + ({minf, pinf, nmi, npi, ld, qe, atoms}, + fns as {isolate_conv, whatis, simpset}) pat = + let + fun h instT = + let + val substT = Thm.instantiate (instT, []); + val substT_cterm = Drule.cterm_rule substT; + + val minf' = map substT minf + val pinf' = map substT pinf + val nmi' = map substT nmi + val npi' = map substT npi + val ld' = map substT ld + val qe' = substT qe + val atoms' = map substT_cterm atoms + val result = ({minf = minf', pinf = pinf', nmi = nmi', npi = npi', + ld = ld', qe = qe', atoms = atoms'}, fns) + in SOME result end + in (case try Thm.match (pat, tm) of + NONE => NONE + | SOME (instT, _) => h instT) + end; + + fun match_struct (_, + entry as ({atoms = atoms, ...}, _): entry) = + get_first (match_inst entry) atoms; + in get_first match_struct (get ctxt) end; + + +(* concrete syntax *) + +local +val minfN = "minf"; +val pinfN = "pinf"; +val nmiN = "nmi"; +val npiN = "npi"; +val lin_denseN = "lindense"; +val qeN = "qe" +val atomsN = "atoms" +val simpsN = "simps" +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); +val any_keyword = + keyword minfN || keyword pinfN || keyword nmiN +|| keyword npiN || keyword lin_denseN || keyword qeN +|| keyword atomsN || keyword simpsN; + +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; +val terms = thms >> map Drule.dest_term; +in + +val ferrak_setup = + Attrib.setup @{binding ferrack} + ((keyword minfN |-- thms) + -- (keyword pinfN |-- thms) + -- (keyword nmiN |-- thms) + -- (keyword npiN |-- thms) + -- (keyword lin_denseN |-- thms) + -- (keyword qeN |-- thms) + -- (keyword atomsN |-- terms) >> + (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> + if length qe = 1 then + add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, + qe = hd qe, atoms = atoms}, + {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss}) + else error "only one theorem for qe!")) + "Ferrante Rackoff data"; + +end; + + +(* theory setup *) + +val setup = ferrak_setup; + +end; diff -r b36a5512c5fb -r 5df087c6ce94 src/HOL/Decision_Procs/langford.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Decision_Procs/langford.ML Tue May 25 22:21:31 2010 +0200 @@ -0,0 +1,244 @@ +(* Title: HOL/Tools/Qelim/langford.ML + Author: Amine Chaieb, TU Muenchen +*) + +signature LANGFORD_QE = +sig + val dlo_tac : Proof.context -> int -> tactic + val dlo_conv : Proof.context -> cterm -> thm +end + +structure LangfordQE :LANGFORD_QE = +struct + +val dest_set = + let + fun h acc ct = + case term_of ct of + Const (@{const_name Orderings.bot}, _) => acc + | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct) +in h [] end; + +fun prove_finite cT u = +let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"} + fun ins x th = + Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) + (Thm.cprop_of th), SOME x] th1) th +in fold ins u th0 end; + +val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms)))); + +fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = + case term_of ep of + Const("Ex",_)$_ => + let + val p = Thm.dest_arg ep + val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid) + val (L,U) = + let + val (x,q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths)) + in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) + end + fun proveneF S = + let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg + val cT = ctyp_of_term a + val ne = instantiate' [SOME cT] [SOME a, SOME A] + @{thm insert_not_empty} + val f = prove_finite cT (dest_set S) + in (ne, f) end + + val qe = case (term_of L, term_of U) of + (Const (@{const_name Orderings.bot}, _),_) => + let + val (neU,fU) = proveneF U + in simp_rule (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end + | (_,Const (@{const_name Orderings.bot}, _)) => + let + val (neL,fL) = proveneF L + in simp_rule (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end + + | (_,_) => + let + val (neL,fL) = proveneF L + val (neU,fU) = proveneF U + in simp_rule (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) + end + in qe end + | _ => error "dlo_qe : Not an existential formula"; + +val all_conjuncts = + let fun h acc ct = + case term_of ct of + @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct) + | _ => ct::acc +in h [] end; + +fun conjuncts ct = + case term_of ct of + @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct)) +| _ => [ct]; + +fun fold1 f = foldr1 (uncurry f); + +val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ; + +fun mk_conj_tab th = + let fun h acc th = + case prop_of th of + @{term "Trueprop"}$(@{term "op &"}$p$q) => + h (h acc (th RS conjunct2)) (th RS conjunct1) + | @{term "Trueprop"}$p => (p,th)::acc +in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end; + +fun is_conj (@{term "op &"}$_$_) = true + | is_conj _ = false; + +fun prove_conj tab cjs = + case cjs of + [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c + | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs]; + +fun conj_aci_rule eq = + let + val (l,r) = Thm.dest_equals eq + fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c)) + fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c)) + val ll = Thm.dest_arg l + val rr = Thm.dest_arg r + + val thl = prove_conj tabl (conjuncts rr) + |> Drule.implies_intr_hyps + val thr = prove_conj tabr (conjuncts ll) + |> Drule.implies_intr_hyps + val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI} + in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end; + +fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x); + +fun is_eqx x eq = case term_of eq of + Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x + | _ => false ; + +local +fun proc ct = + case term_of ct of + Const("Ex",_)$Abs (xn,_,_) => + let + val e = Thm.dest_fun ct + val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct) + val Pp = Thm.capply @{cterm "Trueprop"} p + val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p) + in case eqs of + [] => + let + val (dx,ndx) = List.partition (contains x) neqs + in case ndx of [] => NONE + | _ => + conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp + (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx)))) + |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e + |> Conv.fconv_rule (Conv.arg_conv + (Simplifier.rewrite + (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) + |> SOME + end + | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp + (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs)))) + |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e + |> Conv.fconv_rule (Conv.arg_conv + (Simplifier.rewrite + (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) + |> SOME + end + | _ => NONE; +in val reduce_ex_simproc = + Simplifier.make_simproc + {lhss = [@{cpat "EX x. ?P x"}] , name = "reduce_ex_simproc", + proc = K (K proc) , identifier = []} +end; + +fun raw_dlo_conv dlo_ss + ({qe_bnds, qe_nolb, qe_noub, gst, gs, atoms}:Langford_Data.entry) = + let + val ss = dlo_ss addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc] + val dnfex_conv = Simplifier.rewrite ss + val pcv = Simplifier.rewrite + (dlo_ss addsimps (simp_thms @ ex_simps @ all_simps) + @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]) + in fn p => + Qelim.gen_qelim_conv pcv pcv dnfex_conv cons + (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive) + (K (basic_dloqe () gst qe_bnds qe_nolb qe_noub gs)) p + end; + + +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 + else Thm.dest_fun2 tm + | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm) + | Const ("All", _) $ _ => find_body 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 ("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 = + (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (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 dlo_instance ctxt tm = + (fst (Langford_Data.get ctxt), + Langford_Data.match ctxt (grab_atom_bop 0 tm)); + +fun dlo_conv ctxt tm = + (case dlo_instance ctxt tm of + (_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm]) + | (ss, SOME instance) => raw_dlo_conv ss instance tm); + +fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st => + let + fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} + fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) + val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p) + val p' = fold_rev gen ts p + in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end)); + + +fun cfrees ats ct = + let + val ins = insert (op aconvc) + fun h acc t = + case (term_of t) of + b$_$_ => if member (op aconvc) ats (Thm.dest_fun2 t) + then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc) + else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) + | _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) + | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc)) + | Free _ => if member (op aconvc) ats t then acc else ins t acc + | Var _ => if member (op aconvc) ats t then acc else ins t acc + | _ => acc + in h [] ct end + +fun dlo_tac ctxt = CSUBGOAL (fn (p, i) => + (case dlo_instance ctxt p of + (ss, NONE) => simp_tac ss i + | (ss, SOME instance) => + Object_Logic.full_atomize_tac i THEN + simp_tac ss i + THEN (CONVERSION Thm.eta_long_conversion) i + THEN (TRY o generalize_tac (cfrees (#atoms instance))) i + THEN Object_Logic.full_atomize_tac i + THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ss instance)) i + THEN (simp_tac ss i))); +end; \ No newline at end of file diff -r b36a5512c5fb -r 5df087c6ce94 src/HOL/Decision_Procs/langford_data.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Decision_Procs/langford_data.ML Tue May 25 22:21:31 2010 +0200 @@ -0,0 +1,113 @@ +signature LANGFORD_DATA = +sig + type entry + val get: Proof.context -> simpset * (thm * entry) list + val add: entry -> attribute + val del: attribute + val setup: theory -> theory + val match: Proof.context -> cterm -> entry option +end; + +structure Langford_Data: LANGFORD_DATA = +struct + +(* data *) +type entry = {qe_bnds: thm, qe_nolb : thm , qe_noub: thm, + gs : thm list, gst : thm, atoms: cterm list}; +val eq_key = Thm.eq_thm; +fun eq_data arg = eq_fst eq_key arg; + +structure Data = Generic_Data +( + type T = simpset * (thm * entry) list; + val empty = (HOL_basic_ss, []); + val extend = I; + fun merge ((ss1, es1), (ss2, es2)) : T = + (merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2)); +); + +val get = Data.get o Context.Proof; + +fun del_data key = apsnd (remove eq_data (key, [])); + +val del = Thm.declaration_attribute (Data.map o del_data); + +fun add entry = + Thm.declaration_attribute (fn key => fn context => context |> Data.map + (del_data key #> apsnd (cons (key, entry)))); + +val add_simp = Thm.declaration_attribute (fn th => fn context => + context |> Data.map (fn (ss,ts') => (ss addsimps [th], ts'))) + +val del_simp = Thm.declaration_attribute (fn th => fn context => + context |> Data.map (fn (ss,ts') => (ss delsimps [th], ts'))) + +fun match ctxt tm = + let + fun match_inst + {qe_bnds, qe_nolb, qe_noub, gs, gst, atoms} pat = + let + fun h instT = + let + val substT = Thm.instantiate (instT, []); + val substT_cterm = Drule.cterm_rule substT; + + val qe_bnds' = substT qe_bnds + val qe_nolb' = substT qe_nolb + val qe_noub' = substT qe_noub + val gs' = map substT gs + val gst' = substT gst + val atoms' = map substT_cterm atoms + val result = {qe_bnds = qe_bnds', qe_nolb = qe_nolb', + qe_noub = qe_noub', gs = gs', gst = gst', + atoms = atoms'} + in SOME result end + in (case try Thm.match (pat, tm) of + NONE => NONE + | SOME (instT, _) => h instT) + end; + + fun match_struct (_, + entry as ({atoms = atoms, ...}): entry) = + get_first (match_inst entry) atoms; + in get_first match_struct (snd (get ctxt)) end; + +(* concrete syntax *) + +local +val qeN = "qe"; +val gatherN = "gather"; +val atomsN = "atoms" +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); +val any_keyword = + keyword qeN || keyword gatherN || keyword atomsN; + +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; +val terms = thms >> map Drule.dest_term; +in + +val langford_setup = + Attrib.setup @{binding langford} + ((keyword qeN |-- thms) + -- (keyword gatherN |-- thms) + -- (keyword atomsN |-- terms) >> + (fn ((qes,gs), atoms) => + if length qes = 3 andalso length gs > 1 then + let + val [q1,q2,q3] = qes + val gst::gss = gs + val entry = {qe_bnds = q1, qe_nolb = q2, + qe_noub = q3, gs = gss, gst = gst, atoms = atoms} + in add entry end + else error "Need 3 theorems for qe and at least one for gs")) + "Langford data"; + +end; + +(* theory setup *) + +val setup = + langford_setup #> + Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset"; + +end; diff -r b36a5512c5fb -r 5df087c6ce94 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue May 25 22:12:26 2010 +0200 +++ b/src/HOL/IsaMakefile Tue May 25 22:21:31 2010 +0200 @@ -378,10 +378,6 @@ Taylor.thy \ Transcendental.thy \ Tools/float_syntax.ML \ - Tools/Qelim/ferrante_rackoff_data.ML \ - Tools/Qelim/ferrante_rackoff.ML \ - Tools/Qelim/langford_data.ML \ - Tools/Qelim/langford.ML \ Tools/SMT/smt_real.ML $(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES) @@ -826,6 +822,7 @@ Decision_Procs/MIR.thy \ Decision_Procs/Parametric_Ferrante_Rackoff.thy \ Decision_Procs/Polynomial_List.thy \ + Decision_Procs/ROOT.ML \ Decision_Procs/Reflected_Multivariate_Polynomial.thy \ Decision_Procs/commutative_ring_tac.ML \ Decision_Procs/cooper_tac.ML \ @@ -833,8 +830,11 @@ Decision_Procs/ex/Commutative_Ring_Ex.thy \ Decision_Procs/ex/Dense_Linear_Order_Ex.thy \ Decision_Procs/ferrack_tac.ML \ - Decision_Procs/mir_tac.ML \ - Decision_Procs/ROOT.ML + Decision_Procs/ferrante_rackoff.ML \ + Decision_Procs/ferrante_rackoff_data.ML \ + Decision_Procs/langford.ML \ + Decision_Procs/langford_data.ML \ + Decision_Procs/mir_tac.ML @$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs diff -r b36a5512c5fb -r 5df087c6ce94 src/HOL/Tools/Qelim/ferrante_rackoff.ML --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML Tue May 25 22:12:26 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,233 +0,0 @@ -(* Title: HOL/Tools/Qelim/ferrante_rackoff.ML - Author: Amine Chaieb, TU Muenchen - -Ferrante and Rackoff's algorithm for quantifier elimination in dense -linear orders. Proof-synthesis and tactic. -*) - -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, - ld: thm list, qe: thm, atoms : cterm list} * - {isolate_conv: cterm list -> cterm -> thm, - whatis : cterm -> cterm -> ord, - simpset : simpset}; - -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, - ld = ld, qe = qe, atoms = atoms}, - {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 - val (lS,lth) = uset vars l val (rS, rth) = uset vars r - 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, 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 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)) = - 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 - 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 - 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 Thm.implies_elim (Thm.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') - 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,_) => - Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn - | _ => 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 = - Thm.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 - val insI1 = instantiate' [SOME cT] [] @{thm "insertI1"} - val insI2 = instantiate' [SOME cT] [] @{thm "insertI2"} - in - fun provein x S = - case term_of S of - Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S]) - | Const(@{const_name 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 Thm.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) - u Termtab.empty - 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, - pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf - 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, - 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, - ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld - - 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) - (Thm.cabs x p) (Thm.cabs x q)) - end - | 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 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] = - 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] - | Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq] - | NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq]) - val tU = U t - fun Ufw th = Thm.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 = Drule.implies_elim_list - ((fconv_rule (Thm.beta_conversion true)) - (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th]) - qe)) - [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) (Thm.transitive enth qe_th) - in result_th - end - -in main -end; - -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 - 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 ("op -->", _) $ _ $ _ => find_args bounds tm - | Const ("==>", _) $ _ $ _ => find_args bounds tm - | Const ("==", _) $ _ $ _ => find_args bounds tm - | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm) - | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm) - | _ => Thm.dest_fun2 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 - val ss = simpset - 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, - whatis = whatis, simpset = simpset}) vs - then_conv postcv) - in (Simplifier.rewrite ss then_conv qe_conv) tm 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 => - Object_Logic.full_atomize_tac i THEN - simp_tac (#simpset (snd instance)) i THEN (* FIXME already part of raw_ferrack_qe_conv? *) - CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN - simp_tac (simpset_of ctxt) i)); (* FIXME really? *) - -end; diff -r b36a5512c5fb -r 5df087c6ce94 src/HOL/Tools/Qelim/ferrante_rackoff_data.ML --- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Tue May 25 22:12:26 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,146 +0,0 @@ -(* Title: HOL/Tools/Qelim/ferrante_rackoff_data.ML - Author: Amine Chaieb, TU Muenchen - -Context data for Ferrante and Rackoff's algorithm for quantifier -elimination in dense linear orders. -*) - -signature FERRANTE_RACKOF_DATA = -sig - datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox - type entry - val get: Proof.context -> (thm * entry) list - val del: attribute - val add: entry -> attribute - val funs: thm -> - {isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm, - whatis: morphism -> cterm -> cterm -> ord, - simpset: morphism -> simpset} -> declaration - val match: Proof.context -> cterm -> entry option - val setup: theory -> theory -end; - -structure Ferrante_Rackoff_Data: FERRANTE_RACKOF_DATA = -struct - -(* data *) - -datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox - -type entry = - {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list, - ld: thm list, qe: thm, atoms : cterm list} * - {isolate_conv: Proof.context -> cterm list -> cterm -> thm, - whatis : cterm -> cterm -> ord, - simpset : simpset}; - -val eq_key = Thm.eq_thm; -fun eq_data arg = eq_fst eq_key arg; - -structure Data = Generic_Data -( - type T = (thm * entry) list; - val empty = []; - val extend = I; - fun merge data : T = AList.merge eq_key (K true) data; -); - -val get = Data.get o Context.Proof; - -fun del_data key = remove eq_data (key, []); - -val del = Thm.declaration_attribute (Data.map o del_data); - -fun add entry = - Thm.declaration_attribute (fn key => fn context => context |> Data.map - (del_data key #> cons (key, entry))); - - -(* extra-logical functions *) - -fun funs raw_key {isolate_conv = icv, whatis = wi, simpset = ss} phi = Data.map (fn data => - let - val key = Morphism.thm phi raw_key; - val _ = AList.defined eq_key data key orelse - raise THM ("No data entry for structure key", 0, [key]); - val fns = {isolate_conv = icv phi, whatis = wi phi, simpset = ss phi}; - in AList.map_entry eq_key key (apsnd (K fns)) data end); - -fun match ctxt tm = - let - fun match_inst - ({minf, pinf, nmi, npi, ld, qe, atoms}, - fns as {isolate_conv, whatis, simpset}) pat = - let - fun h instT = - let - val substT = Thm.instantiate (instT, []); - val substT_cterm = Drule.cterm_rule substT; - - val minf' = map substT minf - val pinf' = map substT pinf - val nmi' = map substT nmi - val npi' = map substT npi - val ld' = map substT ld - val qe' = substT qe - val atoms' = map substT_cterm atoms - val result = ({minf = minf', pinf = pinf', nmi = nmi', npi = npi', - ld = ld', qe = qe', atoms = atoms'}, fns) - in SOME result end - in (case try Thm.match (pat, tm) of - NONE => NONE - | SOME (instT, _) => h instT) - end; - - fun match_struct (_, - entry as ({atoms = atoms, ...}, _): entry) = - get_first (match_inst entry) atoms; - in get_first match_struct (get ctxt) end; - - -(* concrete syntax *) - -local -val minfN = "minf"; -val pinfN = "pinf"; -val nmiN = "nmi"; -val npiN = "npi"; -val lin_denseN = "lindense"; -val qeN = "qe" -val atomsN = "atoms" -val simpsN = "simps" -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); -val any_keyword = - keyword minfN || keyword pinfN || keyword nmiN -|| keyword npiN || keyword lin_denseN || keyword qeN -|| keyword atomsN || keyword simpsN; - -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; -val terms = thms >> map Drule.dest_term; -in - -val ferrak_setup = - Attrib.setup @{binding ferrack} - ((keyword minfN |-- thms) - -- (keyword pinfN |-- thms) - -- (keyword nmiN |-- thms) - -- (keyword npiN |-- thms) - -- (keyword lin_denseN |-- thms) - -- (keyword qeN |-- thms) - -- (keyword atomsN |-- terms) >> - (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> - if length qe = 1 then - add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, - qe = hd qe, atoms = atoms}, - {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss}) - else error "only one theorem for qe!")) - "Ferrante Rackoff data"; - -end; - - -(* theory setup *) - -val setup = ferrak_setup; - -end; diff -r b36a5512c5fb -r 5df087c6ce94 src/HOL/Tools/Qelim/langford.ML --- a/src/HOL/Tools/Qelim/langford.ML Tue May 25 22:12:26 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,244 +0,0 @@ -(* Title: HOL/Tools/Qelim/langford.ML - Author: Amine Chaieb, TU Muenchen -*) - -signature LANGFORD_QE = -sig - val dlo_tac : Proof.context -> int -> tactic - val dlo_conv : Proof.context -> cterm -> thm -end - -structure LangfordQE :LANGFORD_QE = -struct - -val dest_set = - let - fun h acc ct = - case term_of ct of - Const (@{const_name Orderings.bot}, _) => acc - | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct) -in h [] end; - -fun prove_finite cT u = -let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"} - fun ins x th = - Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) - (Thm.cprop_of th), SOME x] th1) th -in fold ins u th0 end; - -val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms)))); - -fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = - case term_of ep of - Const("Ex",_)$_ => - let - val p = Thm.dest_arg ep - val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid) - val (L,U) = - let - val (x,q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths)) - in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) - end - fun proveneF S = - let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg - val cT = ctyp_of_term a - val ne = instantiate' [SOME cT] [SOME a, SOME A] - @{thm insert_not_empty} - val f = prove_finite cT (dest_set S) - in (ne, f) end - - val qe = case (term_of L, term_of U) of - (Const (@{const_name Orderings.bot}, _),_) => - let - val (neU,fU) = proveneF U - in simp_rule (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end - | (_,Const (@{const_name Orderings.bot}, _)) => - let - val (neL,fL) = proveneF L - in simp_rule (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end - - | (_,_) => - let - val (neL,fL) = proveneF L - val (neU,fU) = proveneF U - in simp_rule (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) - end - in qe end - | _ => error "dlo_qe : Not an existential formula"; - -val all_conjuncts = - let fun h acc ct = - case term_of ct of - @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct) - | _ => ct::acc -in h [] end; - -fun conjuncts ct = - case term_of ct of - @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct)) -| _ => [ct]; - -fun fold1 f = foldr1 (uncurry f); - -val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ; - -fun mk_conj_tab th = - let fun h acc th = - case prop_of th of - @{term "Trueprop"}$(@{term "op &"}$p$q) => - h (h acc (th RS conjunct2)) (th RS conjunct1) - | @{term "Trueprop"}$p => (p,th)::acc -in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end; - -fun is_conj (@{term "op &"}$_$_) = true - | is_conj _ = false; - -fun prove_conj tab cjs = - case cjs of - [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c - | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs]; - -fun conj_aci_rule eq = - let - val (l,r) = Thm.dest_equals eq - fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c)) - fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c)) - val ll = Thm.dest_arg l - val rr = Thm.dest_arg r - - val thl = prove_conj tabl (conjuncts rr) - |> Drule.implies_intr_hyps - val thr = prove_conj tabr (conjuncts ll) - |> Drule.implies_intr_hyps - val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI} - in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end; - -fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x); - -fun is_eqx x eq = case term_of eq of - Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x - | _ => false ; - -local -fun proc ct = - case term_of ct of - Const("Ex",_)$Abs (xn,_,_) => - let - val e = Thm.dest_fun ct - val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct) - val Pp = Thm.capply @{cterm "Trueprop"} p - val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p) - in case eqs of - [] => - let - val (dx,ndx) = List.partition (contains x) neqs - in case ndx of [] => NONE - | _ => - conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp - (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx)))) - |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e - |> Conv.fconv_rule (Conv.arg_conv - (Simplifier.rewrite - (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) - |> SOME - end - | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp - (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs)))) - |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e - |> Conv.fconv_rule (Conv.arg_conv - (Simplifier.rewrite - (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) - |> SOME - end - | _ => NONE; -in val reduce_ex_simproc = - Simplifier.make_simproc - {lhss = [@{cpat "EX x. ?P x"}] , name = "reduce_ex_simproc", - proc = K (K proc) , identifier = []} -end; - -fun raw_dlo_conv dlo_ss - ({qe_bnds, qe_nolb, qe_noub, gst, gs, atoms}:Langford_Data.entry) = - let - val ss = dlo_ss addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc] - val dnfex_conv = Simplifier.rewrite ss - val pcv = Simplifier.rewrite - (dlo_ss addsimps (simp_thms @ ex_simps @ all_simps) - @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]) - in fn p => - Qelim.gen_qelim_conv pcv pcv dnfex_conv cons - (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive) - (K (basic_dloqe () gst qe_bnds qe_nolb qe_noub gs)) p - end; - - -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 - else Thm.dest_fun2 tm - | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm) - | Const ("All", _) $ _ => find_body 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 ("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 = - (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (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 dlo_instance ctxt tm = - (fst (Langford_Data.get ctxt), - Langford_Data.match ctxt (grab_atom_bop 0 tm)); - -fun dlo_conv ctxt tm = - (case dlo_instance ctxt tm of - (_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm]) - | (ss, SOME instance) => raw_dlo_conv ss instance tm); - -fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st => - let - fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} - fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) - val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p) - val p' = fold_rev gen ts p - in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end)); - - -fun cfrees ats ct = - let - val ins = insert (op aconvc) - fun h acc t = - case (term_of t) of - b$_$_ => if member (op aconvc) ats (Thm.dest_fun2 t) - then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc) - else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) - | _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) - | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc)) - | Free _ => if member (op aconvc) ats t then acc else ins t acc - | Var _ => if member (op aconvc) ats t then acc else ins t acc - | _ => acc - in h [] ct end - -fun dlo_tac ctxt = CSUBGOAL (fn (p, i) => - (case dlo_instance ctxt p of - (ss, NONE) => simp_tac ss i - | (ss, SOME instance) => - Object_Logic.full_atomize_tac i THEN - simp_tac ss i - THEN (CONVERSION Thm.eta_long_conversion) i - THEN (TRY o generalize_tac (cfrees (#atoms instance))) i - THEN Object_Logic.full_atomize_tac i - THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ss instance)) i - THEN (simp_tac ss i))); -end; \ No newline at end of file diff -r b36a5512c5fb -r 5df087c6ce94 src/HOL/Tools/Qelim/langford_data.ML --- a/src/HOL/Tools/Qelim/langford_data.ML Tue May 25 22:12:26 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,113 +0,0 @@ -signature LANGFORD_DATA = -sig - type entry - val get: Proof.context -> simpset * (thm * entry) list - val add: entry -> attribute - val del: attribute - val setup: theory -> theory - val match: Proof.context -> cterm -> entry option -end; - -structure Langford_Data: LANGFORD_DATA = -struct - -(* data *) -type entry = {qe_bnds: thm, qe_nolb : thm , qe_noub: thm, - gs : thm list, gst : thm, atoms: cterm list}; -val eq_key = Thm.eq_thm; -fun eq_data arg = eq_fst eq_key arg; - -structure Data = Generic_Data -( - type T = simpset * (thm * entry) list; - val empty = (HOL_basic_ss, []); - val extend = I; - fun merge ((ss1, es1), (ss2, es2)) : T = - (merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2)); -); - -val get = Data.get o Context.Proof; - -fun del_data key = apsnd (remove eq_data (key, [])); - -val del = Thm.declaration_attribute (Data.map o del_data); - -fun add entry = - Thm.declaration_attribute (fn key => fn context => context |> Data.map - (del_data key #> apsnd (cons (key, entry)))); - -val add_simp = Thm.declaration_attribute (fn th => fn context => - context |> Data.map (fn (ss,ts') => (ss addsimps [th], ts'))) - -val del_simp = Thm.declaration_attribute (fn th => fn context => - context |> Data.map (fn (ss,ts') => (ss delsimps [th], ts'))) - -fun match ctxt tm = - let - fun match_inst - {qe_bnds, qe_nolb, qe_noub, gs, gst, atoms} pat = - let - fun h instT = - let - val substT = Thm.instantiate (instT, []); - val substT_cterm = Drule.cterm_rule substT; - - val qe_bnds' = substT qe_bnds - val qe_nolb' = substT qe_nolb - val qe_noub' = substT qe_noub - val gs' = map substT gs - val gst' = substT gst - val atoms' = map substT_cterm atoms - val result = {qe_bnds = qe_bnds', qe_nolb = qe_nolb', - qe_noub = qe_noub', gs = gs', gst = gst', - atoms = atoms'} - in SOME result end - in (case try Thm.match (pat, tm) of - NONE => NONE - | SOME (instT, _) => h instT) - end; - - fun match_struct (_, - entry as ({atoms = atoms, ...}): entry) = - get_first (match_inst entry) atoms; - in get_first match_struct (snd (get ctxt)) end; - -(* concrete syntax *) - -local -val qeN = "qe"; -val gatherN = "gather"; -val atomsN = "atoms" -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); -val any_keyword = - keyword qeN || keyword gatherN || keyword atomsN; - -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; -val terms = thms >> map Drule.dest_term; -in - -val langford_setup = - Attrib.setup @{binding langford} - ((keyword qeN |-- thms) - -- (keyword gatherN |-- thms) - -- (keyword atomsN |-- terms) >> - (fn ((qes,gs), atoms) => - if length qes = 3 andalso length gs > 1 then - let - val [q1,q2,q3] = qes - val gst::gss = gs - val entry = {qe_bnds = q1, qe_nolb = q2, - qe_noub = q3, gs = gss, gst = gst, atoms = atoms} - in add entry end - else error "Need 3 theorems for qe and at least one for gs")) - "Langford data"; - -end; - -(* theory setup *) - -val setup = - langford_setup #> - Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset"; - -end;