diff -r b65692d4adcd -r 28c6a0118818 src/HOL/Tools/Qelim/ferrante_rackoff.ML --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML Wed Jul 04 16:49:34 2007 +0200 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Wed Jul 04 16:49:35 2007 +0200 @@ -6,8 +6,9 @@ linear orders. Proof-synthesis and tactic. *) -signature FERRANTE_RACKOFF = +signature FERRANTE_RACKOFF = sig + val dlo_conv: Proof.context -> conv val dlo_tac: Proof.context -> int -> tactic end; @@ -17,79 +18,69 @@ open Ferrante_Rackoff_Data; open Conv; -type entry = {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list, +type entry = {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list, ld: thm list, qe: thm, atoms : cterm list} * - {isolate_conv: cterm list -> cterm -> thm, + {isolate_conv: cterm list -> cterm -> thm, whatis : cterm -> cterm -> ord, simpset : simpset}; -fun binop_cong b th1 th2 = Thm.combination (Drule.arg_cong_rule b th1) th2; -val is_refl = op aconv o Logic.dest_equals o Thm.prop_of; -fun C f x y = f y x - -fun get_p1 th = - let - fun appair f (x,y) = (f x, f y) - in funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) - (funpow 2 Thm.dest_arg (cprop_of th)) |> Thm.dest_arg -end; +fun get_p1 th = + funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) + (funpow 2 Thm.dest_arg (cprop_of th)) |> Thm.dest_arg fun ferrack_conv - (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, + (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = ld, qe = qe, atoms = atoms}, - {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) = -let + {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) = +let fun uset (vars as (x::vs)) p = case term_of p of - Const("op &", _)$ _ $ _ => - let - val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb + Const("op &", _)$ _ $ _ => + let + val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb val (lS,lth) = uset vars l val (rS, rth) = uset vars r - in (lS@rS, binop_cong b lth rth) end - | Const("op |", _)$ _ $ _ => - let - val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb + in (lS@rS, Drule.binop_cong_rule b lth rth) end + | Const("op |", _)$ _ $ _ => + let + val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb val (lS,lth) = uset vars l val (rS, rth) = uset vars r - in (lS@rS, binop_cong b lth rth) end - | _ => - let - val th = icv vars p + in (lS@rS, Drule.binop_cong_rule b lth rth) end + | _ => + let + val th = icv vars p val p' = Thm.rhs_of th val c = wi x p' - val S = (if c mem [Lt, Le, Eq] then single o Thm.dest_arg - else if c mem [Gt, Ge] then single o Thm.dest_arg1 - else if c = NEq then single o Thm.dest_arg o Thm.dest_arg + val S = (if member (op =) [Lt, Le, Eq] c then single o Thm.dest_arg + else if member (op =) [Gt, Ge] c then single o Thm.dest_arg1 + else if c = NEq then single o Thm.dest_arg o Thm.dest_arg else K []) p' in (S,th) end - val ((p1_v,p2_v),(mp1_v,mp2_v)) = + val ((p1_v,p2_v),(mp1_v,mp2_v)) = + funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) + (funpow 4 Thm.dest_arg (cprop_of (hd minf))) + |> Thm.dest_binop |> pairself Thm.dest_binop |> apfst (pairself Thm.dest_fun) + + fun myfwd (th1, th2, th3, th4, th5) p1 p2 + [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] = let - fun appair f (x,y) = (f x, f y) - in funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) - (funpow 4 Thm.dest_arg (cprop_of (hd minf))) - |> Thm.dest_binop |> appair Thm.dest_binop |> apfst (appair Thm.dest_fun) - end - - fun myfwd (th1, th2, th3, th4, th5) p1 p2 - [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] = - let val (mp1, mp2) = (get_p1 th_1, get_p1 th_1') val (pp1, pp2) = (get_p1 th_2, get_p1 th_2') - fun fw mi th th' th'' = - let - val th0 = if mi then + fun fw mi th th' th'' = + let + val th0 = if mi then instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th in implies_elim (implies_elim th0 th') th'' end - in (fw true th1 th_1 th_1', fw false th2 th_2 th_2', - fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5') + in (fw true th1 th_1 th_1', fw false th2 th_2 th_2', + fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5') end val U_v = (Thm.dest_arg o Thm.dest_arg o Thm.dest_arg1) (cprop_of qe) - fun main vs p = - let - val ((xn,ce),(x,fm)) = (case term_of p of - Const("Ex",_)$Abs(xn,xT,_) => + fun main vs p = + let + val ((xn,ce),(x,fm)) = (case term_of p of + Const("Ex",_)$Abs(xn,xT,_) => Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn - | _ => error "main QE only trats existential quantifiers!") + | _ => raise CTERM ("main QE only treats existential quantifiers!", [p])) val cT = ctyp_of_term x val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc) val nthx = Thm.abstract_rule xn x nth @@ -97,63 +88,63 @@ val qx = Thm.rhs_of nthx val enth = Drule.arg_cong_rule ce nthx val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"} - fun ins x th = - implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) + fun ins x th = + implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th val fU = fold ins u th0 val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU) - local + local val insI1 = instantiate' [SOME cT] [] @{thm "insertI1"} val insI2 = instantiate' [SOME cT] [] @{thm "insertI2"} in - fun provein x S = + fun provein x S = case term_of S of - Const("{}",_) => error "provein : not a member!" - | Const("insert",_)$y$_ => + Const("{}",_) => raise CTERM ("provein : not a member!", [S]) + | Const("insert",_)$y$_ => let val (cy,S') = Thm.dest_binop S in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1 - else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) + else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) (provein x S') end end - val tabU = fold (fn t => fn tab => Termtab.update (term_of t, provein t cU) tab) + val tabU = fold (fn t => fn tab => Termtab.update (term_of t, provein t cU) tab) u Termtab.empty - val U = valOf o Termtab.lookup tabU o term_of - val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt, + val U = the o Termtab.lookup tabU o term_of + val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt, minf_le, minf_gt, minf_ge, minf_P] = minf - val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt, + val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt, pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf - val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt, + val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt, nmi_le, nmi_gt, nmi_ge, nmi_P] = map (instantiate ([],[(U_v,cU)])) nmi - val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt, + val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt, npi_le, npi_gt, npi_ge, npi_P] = map (instantiate ([],[(U_v,cU)])) npi - val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt, + val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt, ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld - - fun decomp_mpinf fm = + + fun decomp_mpinf fm = case term_of fm of - Const("op &",_)$_$_ => - let val (p,q) = Thm.dest_binop fm - in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj) + Const("op &",_)$_$_ => + let val (p,q) = Thm.dest_binop fm + in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj) (Thm.cabs x p) (Thm.cabs x q)) end - | Const("op |",_)$_$_ => - let val (p,q) = Thm.dest_binop fm + | Const("op |",_)$_$_ => + let val (p,q) = Thm.dest_binop fm in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj) (Thm.cabs x p) (Thm.cabs x q)) end - | _ => + | _ => (let val c = wi x fm - val t = (if c=Nox then I - else if c mem [Lt, Le, Eq] then Thm.dest_arg - else if c mem [Gt,Ge] then Thm.dest_arg1 - else if c = NEq then (Thm.dest_arg o Thm.dest_arg) - else error "decomp_mpinf: Impossible case!!") fm - val [mi_th, pi_th, nmi_th, npi_th, ld_th] = - if c = Nox then map (instantiate' [] [SOME fm]) + val t = (if c=Nox then I + else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg + else if member (op =) [Gt, Ge] c then Thm.dest_arg1 + else if c = NEq then (Thm.dest_arg o Thm.dest_arg) + else sys_error "decomp_mpinf: Impossible case!!") fm + val [mi_th, pi_th, nmi_th, npi_th, ld_th] = + if c = Nox then map (instantiate' [] [SOME fm]) [minf_P, pinf_P, nmi_P, npi_P, ld_P] - else - let val [mi_th,pi_th,nmi_th,npi_th,ld_th] = + else + let val [mi_th,pi_th,nmi_th,npi_th,ld_th] = map (instantiate' [] [SOME t]) (case c of Lt => [minf_lt, pinf_lt, nmi_lt, npi_lt, ld_lt] | Le => [minf_le, pinf_le, nmi_le, npi_le, ld_le] @@ -167,11 +158,12 @@ end in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end) val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q - val qe_th = fold (C implies_elim) [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th] - ((fconv_rule (Thm.beta_conversion true)) - (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th]) + val qe_th = Drule.implies_elim_list + ((fconv_rule (Thm.beta_conversion true)) + (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th]) qe)) - val bex_conv = + [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th] + val bex_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)})) val result_th = fconv_rule (arg_conv bex_conv) (transitive enth qe_th) in result_th @@ -180,12 +172,12 @@ in main end; -val grab_atom_bop = - let +val grab_atom_bop = + let fun h bounds tm = (case term_of tm of Const ("op =", T) $ _ $ _ => - if domain_type T = HOLogic.boolT then find_args bounds tm + if domain_type T = HOLogic.boolT then find_args bounds tm else Thm.dest_fun2 tm | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm) | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm) @@ -197,55 +189,45 @@ | Const ("==", _) $ _ $ _ => find_args bounds tm | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm) | _ => Thm.dest_fun2 tm) - and find_args bounds tm = + and find_args bounds tm = (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm) and find_body bounds b = let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b in h (bounds + 1) b' end; in h end; -fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset}) tm = - let +fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset}) tm = + let val ss = simpset - val pcv = Simplifier.rewrite - (merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps) - @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss)) - val postcv = Simplifier.rewrite ss - val nnf = K (nnf_conv then_conv postcv) - val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm []) + val ss' = + merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps) + @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss) + |> Simplifier.inherit_context ss + val pcv = Simplifier.rewrite ss' + val postcv = Simplifier.rewrite ss + val nnf = K (nnf_conv then_conv postcv) + val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm []) (isolate_conv ctxt) nnf - (fn vs => ferrack_conv (thy,{isolate_conv = isolate_conv ctxt, + (fn vs => ferrack_conv (thy,{isolate_conv = isolate_conv ctxt, whatis = whatis, simpset = simpset}) vs then_conv postcv) in (Simplifier.rewrite ss then_conv qe_conv) tm end; -fun ferrackqe_conv ctxt tm = - case Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm) of - NONE => error "ferrackqe_conv : no corresponding instance in context!" -| SOME res => raw_ferrack_qe_conv ctxt res tm +fun 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 core_ferrack_tac ctxt res i st = - let val p = nth (cprems_of st) (i - 1) - val th = symmetric (arg_conv (raw_ferrack_qe_conv ctxt res) p) - val p' = Thm.lhs_of th - val th' = implies_intr p' (equal_elim th (assume p')) - val _ = print_thm th - in (rtac th' i) st - end - -fun dlo_tac ctxt i st = - let - val instance = (case Ferrante_Rackoff_Data.match ctxt - (grab_atom_bop 0 (nth (cprems_of st) (i - 1))) of - NONE => error "ferrackqe_conv : no corresponding instance in context!" - | SOME r => r) - val ss = #simpset (snd instance) - in - (ObjectLogic.full_atomize_tac i THEN - simp_tac ss i THEN - core_ferrack_tac ctxt instance i THEN - (TRY (simp_tac (Simplifier.local_simpset_of ctxt) i))) st - end; +fun dlo_tac ctxt = CSUBGOAL (fn (p, i) => + (case dlo_instance ctxt p of + NONE => no_tac + | SOME instance => + ObjectLogic.full_atomize_tac i THEN + simp_tac (#simpset (snd instance)) i THEN (* FIXME already part of raw_ferrack_qe_conv? *) + CONVERSION (ObjectLogic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN + simp_tac (Simplifier.local_simpset_of ctxt) i)); (* FIXME really? *) end;