--- a/src/HOL/Tools/Ferrante_Rackoff/ferrante_rackoff.ML Thu Jun 21 20:48:47 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,263 +0,0 @@
-(* Title: HOL/Tools/ferrante_rackoff.ML
- ID: $Id$
- 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_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 binop_cong b th1 th2 = Thm.combination (Drule.arg_cong_rule b th1) th2;
-val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
-fun C f x y = f y x
-
-fun get_p1 th =
- let
- fun appair f (x,y) = (f x, f y)
- in funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
- (funpow 2 Thm.dest_arg (cprop_of th)) |> Thm.dest_arg
-end;
-
-fun 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, binop_cong b lth rth) end
- | Const("op |", _)$ _ $ _ =>
- let
- val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
- val (lS,lth) = uset vars l val (rS, rth) = uset vars r
- in (lS@rS, binop_cong b lth rth) end
- | _ =>
- let
- val th = icv vars p
- val p' = Thm.rhs_of th
- val c = wi x p'
- val S = (if c mem [Lt, Le, Eq] then single o Thm.dest_arg
- else if c mem [Gt, Ge] then single o Thm.dest_arg1
- else if c = NEq then single o Thm.dest_arg o Thm.dest_arg
- else K []) p'
- in (S,th) end
-
- val ((p1_v,p2_v),(mp1_v,mp2_v)) =
- let
- fun appair f (x,y) = (f x, f y)
- in funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
- (funpow 4 Thm.dest_arg (cprop_of (hd minf)))
- |> Thm.dest_binop |> appair Thm.dest_binop |> apfst (appair Thm.dest_fun)
- end
-
- fun myfwd (th1, th2, th3, th4, th5) p1 p2
- [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] =
- let
- val (mp1, mp2) = (get_p1 th_1, get_p1 th_1')
- val (pp1, pp2) = (get_p1 th_2, get_p1 th_2')
- fun fw mi th th' th'' =
- let
- val th0 = if mi then
- instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
- else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
- in implies_elim (implies_elim th0 th') th'' end
- in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
- fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
- 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
- | _ => error "main QE only trats existential quantifiers!")
- val cT = ctyp_of_term x
- val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc)
- val nthx = Thm.abstract_rule xn x nth
- val q = Thm.rhs_of nth
- val qx = Thm.rhs_of nthx
- val enth = Drule.arg_cong_rule ce nthx
- val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
- fun ins x th =
- implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
- (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("{}",_) => error "provein : not a member!"
- | Const("insert",_)$y$_ =>
- let val (cy,S') = Thm.dest_binop S
- in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
- else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
- (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 = valOf 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 c mem [Lt, Le, Eq] then Thm.dest_arg
- else if c mem [Gt,Ge] then Thm.dest_arg1
- else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
- else error "decomp_mpinf: Impossible case!!") fm
- val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
- if c = Nox then map (instantiate' [] [SOME fm])
- [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 = implies_elim th tU
- in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th]
- end
- in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end)
- val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q
- val qe_th = fold (C implies_elim) [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
- ((fconv_rule (Thm.beta_conversion true))
- (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
- qe))
- val bex_conv =
- Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)}))
- val result_th = fconv_rule (arg_conv bex_conv) (transitive enth qe_th)
- in result_th
- end
-
-in main
-end;
-
-val grab_atom_bop =
- let
- 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 ("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;
-
-local
-fun cterm_frees ct =
- let fun h acc t =
- case (term_of t) of
- _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
- | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
- | Free _ => insert (op aconvc) t acc
- | _ => acc
- in h [] ct end;
-in
-
-fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset}) tm =
- let
- val ss = simpset
- val pcv = Simplifier.rewrite
- (merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
- @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss))
- val postcv = Simplifier.rewrite ss
- val nnf = K (nnf_conv then_conv postcv)
- val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (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 ferrackqe_conv ctxt tm =
- case Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm) of
- NONE => error "ferrackqe_conv : no corresponding instance in context!"
-| SOME res => raw_ferrack_qe_conv ctxt res tm
-end;
-
-fun core_ferrack_tac ctxt res i st =
- let val p = nth (cprems_of st) (i - 1)
- val th = symmetric (arg_conv (raw_ferrack_qe_conv ctxt res) p)
- val p' = Thm.lhs_of th
- val th' = implies_intr p' (equal_elim th (assume p'))
- val _ = print_thm th
- in (rtac th' i) st
- end
-
-fun dlo_tac ctxt i st =
- let
- val instance = (case Ferrante_Rackoff_Data.match ctxt
- (grab_atom_bop 0 (nth (cprems_of st) (i - 1))) of
- NONE => error "ferrackqe_conv : no corresponding instance in context!"
- | SOME r => r)
- val ss = #simpset (snd instance)
- in
- (ObjectLogic.full_atomize_tac i THEN
- simp_tac ss i THEN
- core_ferrack_tac ctxt instance i THEN
- (TRY (simp_tac (Simplifier.local_simpset_of ctxt) i))) st
- end;
-
-end;