--- 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)
--- /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;
--- /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;
--- /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
--- /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;
--- 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
--- 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;
--- 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;
--- 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
--- 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;