diff --git a/src/HOL/Analysis/metric_arith.ML b/src/HOL/Analysis/metric_arith.ML --- a/src/HOL/Analysis/metric_arith.ML +++ b/src/HOL/Analysis/metric_arith.ML @@ -1,324 +1,323 @@ signature METRIC_ARITH = sig val metric_arith_tac : Proof.context -> int -> tactic val trace: bool Config.T end structure MetricArith : METRIC_ARITH = struct fun default d x = case x of SOME y => SOME y | NONE => d (* apply f to both cterms in ct_pair, merge results *) fun app_union_ct_pair f ct_pair = uncurry (union (op aconvc)) (apply2 f ct_pair) val trace = Attrib.setup_config_bool \<^binding>\metric_trace\ (K false) fun trace_tac ctxt msg = if Config.get ctxt trace then print_tac ctxt msg else all_tac fun argo_trace_ctxt ctxt = if Config.get ctxt trace then Config.map (Argo_Tactic.trace) (K "basic") ctxt else ctxt fun IF_UNSOLVED' tac i = IF_UNSOLVED (tac i) fun REPEAT' tac i = REPEAT (tac i) -fun frees ct = Drule.cterm_add_frees ct [] -fun free_in v ct = member (op aconvc) (frees ct) v +fun free_in v ct = member (op aconvc) (Drule.cterm_frees_of ct) v (* build a cterm set with elements cts of type ty *) fun mk_ct_set ctxt ty = map Thm.term_of #> HOLogic.mk_set ty #> Thm.cterm_of ctxt fun prenex_tac ctxt = let val prenex_simps = Proof_Context.get_thms ctxt @{named_theorems metric_prenex} val prenex_ctxt = put_simpset HOL_basic_ss ctxt addsimps prenex_simps in simp_tac prenex_ctxt THEN' K (trace_tac ctxt "Prenex form") end fun nnf_tac ctxt = let val nnf_simps = Proof_Context.get_thms ctxt @{named_theorems metric_nnf} val nnf_ctxt = put_simpset HOL_basic_ss ctxt addsimps nnf_simps in simp_tac nnf_ctxt THEN' K (trace_tac ctxt "NNF form") end fun unfold_tac ctxt = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ( Proof_Context.get_thms ctxt @{named_theorems metric_unfold})) fun pre_arith_tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps ( Proof_Context.get_thms ctxt @{named_theorems metric_pre_arith})) THEN' K (trace_tac ctxt "Prepared for decision procedure") fun dist_refl_sym_tac ctxt = let val refl_sym_simps = @{thms dist_self dist_commute add_0_right add_0_left simp_thms} val refl_sym_ctxt = put_simpset HOL_basic_ss ctxt addsimps refl_sym_simps in simp_tac refl_sym_ctxt THEN' K (trace_tac ctxt ("Simplified using " ^ @{make_string} refl_sym_simps)) end fun is_exists ct = case Thm.term_of ct of Const (\<^const_name>\HOL.Ex\,_)$_ => true | Const (\<^const_name>\Trueprop\,_)$_ => is_exists (Thm.dest_arg ct) | _ => false fun is_forall ct = case Thm.term_of ct of Const (\<^const_name>\HOL.All\,_)$_ => true | Const (\<^const_name>\Trueprop\,_)$_ => is_forall (Thm.dest_arg ct) | _ => false fun dist_ty mty = mty --> mty --> \<^typ>\real\ (* find all free points in ct of type metric_ty *) fun find_points ctxt metric_ty ct = let fun find ct = (if Thm.typ_of_cterm ct = metric_ty then [ct] else []) @ ( case Thm.term_of ct of _ $ _ => app_union_ct_pair find (Thm.dest_comb ct) | Abs (_, _, _) => (* ensure the point doesn't contain the bound variable *) let val (var, bod) = Thm.dest_abs NONE ct in filter (free_in var #> not) (find bod) end | _ => []) val points = find ct in case points of [] => (* if no point can be found, invent one *) let val free_name = Term.variant_frees (Thm.term_of ct) [("x", metric_ty)] in map (Free #> Thm.cterm_of ctxt) free_name end | _ => points end (* find all cterms "dist x y" in ct, where x and y have type metric_ty *) fun find_dist metric_ty ct = let val dty = dist_ty metric_ty fun find ct = case Thm.term_of ct of Const (\<^const_name>\dist\, ty) $ _ $ _ => if ty = dty then [ct] else [] | _ $ _ => app_union_ct_pair find (Thm.dest_comb ct) | Abs (_, _, _) => let val (var, bod) = Thm.dest_abs NONE ct in filter (free_in var #> not) (find bod) end | _ => [] in find ct end (* find all "x=y", where x has type metric_ty *) fun find_eq metric_ty ct = let fun find ct = case Thm.term_of ct of Const (\<^const_name>\HOL.eq\, ty) $ _ $ _ => if fst (dest_funT ty) = metric_ty then [ct] else app_union_ct_pair find (Thm.dest_binop ct) | _ $ _ => app_union_ct_pair find (Thm.dest_comb ct) | Abs (_, _, _) => let val (var, bod) = Thm.dest_abs NONE ct in filter (free_in var #> not) (find bod) end | _ => [] in find ct end (* rewrite ct of the form "dist x y" using maxdist_thm *) fun maxdist_conv ctxt fset_ct ct = let val (xct, yct) = Thm.dest_binop ct val solve_prems = rule_by_tactic ctxt (ALLGOALS (simp_tac (put_simpset HOL_ss ctxt addsimps @{thms finite.emptyI finite_insert empty_iff insert_iff}))) val image_simp = Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms image_empty image_insert}) val dist_refl_sym_simp = Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self}) val algebra_simp = Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms diff_self diff_0_right diff_0 abs_zero abs_minus_cancel abs_minus_commute}) val insert_simp = Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms insert_absorb2 insert_commute}) val sup_simp = Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms cSup_singleton Sup_insert_insert}) val real_abs_dist_simp = Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms real_abs_dist}) val maxdist_thm = @{thm maxdist_thm} |> infer_instantiate' ctxt [SOME fset_ct, SOME xct, SOME yct] |> solve_prems in ((Conv.rewr_conv maxdist_thm) then_conv (* SUP to Sup *) image_simp then_conv dist_refl_sym_simp then_conv algebra_simp then_conv (* eliminate duplicate terms in set *) insert_simp then_conv (* Sup to max *) sup_simp then_conv real_abs_dist_simp) ct end (* rewrite ct of the form "x=y" using metric_eq_thm *) fun metric_eq_conv ctxt fset_ct ct = let val (xct, yct) = Thm.dest_binop ct val solve_prems = rule_by_tactic ctxt (ALLGOALS (simp_tac (put_simpset HOL_ss ctxt addsimps @{thms empty_iff insert_iff}))) val ball_simp = Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms Set.ball_empty ball_insert}) val dist_refl_sym_simp = Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self}) val metric_eq_thm = @{thm metric_eq_thm} |> infer_instantiate' ctxt [SOME xct, SOME fset_ct, SOME yct] |> solve_prems in ((Conv.rewr_conv metric_eq_thm) then_conv (* convert \x\{x\<^sub>1,...,x\<^sub>n}. P x to P x\<^sub>1 \ ... \ P x\<^sub>n *) ball_simp then_conv dist_refl_sym_simp) ct end (* build list of theorems "0 \ dist x y" for all dist terms in ct *) fun augment_dist_pos ctxt metric_ty ct = let fun inst dist_ct = let val (xct, yct) = Thm.dest_binop dist_ct in infer_instantiate' ctxt [SOME xct, SOME yct] @{thm zero_le_dist} end in map inst (find_dist metric_ty ct) end fun top_sweep_rewrs_tac ctxt thms = CONVERSION (Conv.top_sweep_conv (K (Conv.rewrs_conv thms)) ctxt) (* apply maxdist_conv and metric_eq_conv to the goal, thereby embedding the goal in (\\<^sup>n,dist\<^sub>\) *) fun embedding_tac ctxt metric_ty i goal = let val ct = (Thm.cprem_of goal 1) val points = find_points ctxt metric_ty ct val fset_ct = mk_ct_set ctxt metric_ty points (* embed all subterms of the form "dist x y" in (\\<^sup>n,dist\<^sub>\) *) val eq1 = map (maxdist_conv ctxt fset_ct) (find_dist metric_ty ct) (* replace point equality by equality of components in \\<^sup>n *) val eq2 = map (metric_eq_conv ctxt fset_ct) (find_eq metric_ty ct) in ( K (trace_tac ctxt "Embedding into \\<^sup>n") THEN' top_sweep_rewrs_tac ctxt (eq1 @ eq2))i goal end (* decision procedure for linear real arithmetic *) fun lin_real_arith_tac ctxt metric_ty i goal = let val dist_thms = augment_dist_pos ctxt metric_ty (Thm.cprem_of goal 1) val ctxt' = argo_trace_ctxt ctxt in (Argo_Tactic.argo_tac ctxt' dist_thms) i goal end fun basic_metric_arith_tac ctxt metric_ty = HEADGOAL (dist_refl_sym_tac ctxt THEN' IF_UNSOLVED' (embedding_tac ctxt metric_ty) THEN' IF_UNSOLVED' (pre_arith_tac ctxt) THEN' IF_UNSOLVED' (lin_real_arith_tac ctxt metric_ty)) (* tries to infer the metric space from ct from dist terms, if no dist terms are present, equality terms will be used *) fun guess_metric ctxt ct = let fun find_dist ct = case Thm.term_of ct of Const (\<^const_name>\dist\, ty) $ _ $ _ => SOME (fst (dest_funT ty)) | _ $ _ => let val (s, t) = Thm.dest_comb ct in default (find_dist t) (find_dist s) end | Abs (_, _, _) => find_dist (snd (Thm.dest_abs NONE ct)) | _ => NONE fun find_eq ct = case Thm.term_of ct of Const (\<^const_name>\HOL.eq\, ty) $ x $ _ => let val (l, r) = Thm.dest_binop ct in if Sign.of_sort (Proof_Context.theory_of ctxt) (type_of x, \<^sort>\metric_space\) then SOME (fst (dest_funT ty)) else default (find_dist r) (find_eq l) end | _ $ _ => let val (s, t) = Thm.dest_comb ct in default (find_eq t) (find_eq s) end | Abs (_, _, _) => find_eq (snd (Thm.dest_abs NONE ct)) | _ => NONE in case default (find_eq ct) (find_dist ct) of SOME ty => ty | NONE => error "No Metric Space was found" end (* eliminate \ by proving the goal for a single witness from the metric space *) fun elim_exists ctxt goal = let val ct = Thm.cprem_of goal 1 val metric_ty = guess_metric ctxt ct val points = find_points ctxt metric_ty ct fun try_point ctxt pt = let val ex_rule = infer_instantiate' ctxt [NONE, SOME pt] @{thm exI} in HEADGOAL (resolve_tac ctxt [ex_rule] ORELSE' (* variable doesn't occur in body *) resolve_tac ctxt @{thms exI}) THEN trace_tac ctxt ("Removed existential quantifier, try " ^ @{make_string} pt) THEN try_points ctxt end and try_points ctxt goal = ( if is_exists (Thm.cprem_of goal 1) then FIRST (map (try_point ctxt) points) else if is_forall (Thm.cprem_of goal 1) then HEADGOAL (resolve_tac ctxt @{thms HOL.allI} THEN' Subgoal.FOCUS (fn {context = ctxt', ...} => trace_tac ctxt "Removed universal quantifier" THEN try_points ctxt') ctxt) else basic_metric_arith_tac ctxt metric_ty) goal in try_points ctxt goal end fun metric_arith_tac ctxt = (* unfold common definitions to get rid of sets *) unfold_tac ctxt THEN' (* remove all meta-level connectives *) IF_UNSOLVED' (Object_Logic.full_atomize_tac ctxt) THEN' (* convert goal to prenex form *) IF_UNSOLVED' (prenex_tac ctxt) THEN' (* and NNF to ? *) IF_UNSOLVED' (nnf_tac ctxt) THEN' (* turn all universally quantified variables into free variables, by focusing the subgoal *) REPEAT' (resolve_tac ctxt @{thms HOL.allI}) THEN' IF_UNSOLVED' (SUBPROOF (fn {context=ctxt', ...} => trace_tac ctxt' "Focused on subgoal" THEN elim_exists ctxt') ctxt) end diff --git a/src/HOL/Decision_Procs/ferrante_rackoff.ML b/src/HOL/Decision_Procs/ferrante_rackoff.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML @@ -1,233 +1,233 @@ (* Title: HOL/Decision_Procs/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 (Thm.cprop_of th)) |> Thm.dest_arg fun ferrack_conv ctxt (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 Thm.term_of p of Const(\<^const_name>\HOL.conj\, _)$ _ $ _ => 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(\<^const_name>\HOL.disj\, _)$ _ $ _ => 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 (Thm.cprop_of (hd minf))) |> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun) |> apply2 (apply2 (dest_Var o Thm.term_of)) 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 Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th else Drule.instantiate_normalize ([],[(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 = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 (Thm.cprop_of qe))))) fun main vs p = let val ((xn,ce),(x,fm)) = (case Thm.term_of p of Const(\<^const_name>\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 = Thm.ctyp_of_cterm 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 (Thm.instantiate' [SOME cT] []) @{thms "finite.intros"} fun ins x th = Thm.implies_elim (Thm.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 = Thm.instantiate' [SOME cT] [] @{thm "insertI1"} val insI2 = Thm.instantiate' [SOME cT] [] @{thm "insertI2"} in fun provein x S = case Thm.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 Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1 else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2) (provein x S') end end val tabU = fold (fn t => fn tab => Termtab.update (Thm.term_of t, provein t cU) tab) u Termtab.empty val U = the o Termtab.lookup tabU o Thm.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 (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt, npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt, ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld fun decomp_mpinf fm = case Thm.term_of fm of Const(\<^const_name>\HOL.conj\,_)$_$_ => let val (p,q) = Thm.dest_binop fm in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj) (Thm.lambda x p) (Thm.lambda x q)) end | Const(\<^const_name>\HOL.disj\,_)$_$_ => let val (p,q) = Thm.dest_binop fm in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj) (Thm.lambda x p) (Thm.lambda 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 raise Fail "decomp_mpinf: Impossible case!!") fm val [mi_th, pi_th, nmi_th, npi_th, ld_th] = if c = Nox then map (Thm.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 (Thm.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)) (Thm.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 (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_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 Thm.term_of tm of Const (\<^const_name>\HOL.eq\, T) $ _ $ _ => if domain_type T = HOLogic.boolT then find_args bounds tm else Thm.dest_fun2 tm | Const (\<^const_name>\Not\, _) $ _ => h bounds (Thm.dest_arg tm) | Const (\<^const_name>\All\, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (\<^const_name>\Ex\, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (\<^const_name>\HOL.conj\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\HOL.disj\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\HOL.implies\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\Pure.imp\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\Pure.eq\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\Pure.all\, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (\<^const_name>\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 = ss}) tm = let val ss' = merge_ss (simpset_of (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps all_simps not_all all_not_ex ex_disj_distrib}), ss); val pcv = Simplifier.rewrite (put_simpset ss' ctxt); val postcv = Simplifier.rewrite (put_simpset ss ctxt); val nnf = K (nnf_conv ctxt then_conv postcv) - val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_add_frees tm []) + val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_frees_of tm) (isolate_conv ctxt) nnf (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt, whatis = whatis, simpset = ss}) vs then_conv postcv) in (Simplifier.rewrite (put_simpset ss ctxt) 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 ctxt i THEN simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN (* FIXME already part of raw_ferrack_qe_conv? *) CONVERSION (Object_Logic.judgment_conv ctxt (raw_ferrack_qe_conv ctxt instance)) i THEN simp_tac ctxt i)); (* FIXME really? *) end; diff --git a/src/HOL/Decision_Procs/langford.ML b/src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML +++ b/src/HOL/Decision_Procs/langford.ML @@ -1,263 +1,263 @@ (* Title: HOL/Decision_Procs/langford.ML Author: Amine Chaieb, TU Muenchen *) signature LANGFORD = sig val dlo_tac : Proof.context -> int -> tactic val dlo_conv : Proof.context -> cterm -> thm end structure Langford: LANGFORD = struct val dest_set = let fun h acc ct = (case Thm.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 (Thm.instantiate' [SOME cT] []) @{thms finite.intros} fun ins x th = Thm.implies_elim (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th in fold ins u th0 end; fun simp_rule ctxt = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms ball_simps simp_thms}))); fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = (case Thm.term_of ep of Const (\<^const_name>\Ex\, _) $ _ => let val p = Thm.dest_arg ep val ths = simplify (put_simpset HOL_basic_ss ctxt addsimps gather) (Thm.instantiate' [] [SOME p] stupid) val (L, U) = let val (_, 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 = Thm.ctyp_of_cterm a val ne = Thm.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 (Thm.term_of L, Thm.term_of U) of (Const (\<^const_name>\Orderings.bot\, _),_) => let val (neU, fU) = proveneF U in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end | (_, Const (\<^const_name>\Orderings.bot\, _)) => let val (neL,fL) = proveneF L in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end | _ => let val (neL, fL) = proveneF L val (neU, fU) = proveneF U in simp_rule ctxt (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 Thm.term_of ct of \<^term>\HOL.conj\ $ _ $ _ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct) | _ => ct :: acc) in h [] end; fun conjuncts ct = (case Thm.term_of ct of \<^term>\HOL.conj\ $ _ $ _ => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct) | _ => [ct]); fun fold1 f = foldr1 (uncurry f); (* FIXME !? *) val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply \<^cterm>\HOL.conj\ c) c'); fun mk_conj_tab th = let fun h acc th = (case Thm.prop_of th of \<^term>\Trueprop\ $ (\<^term>\HOL.conj\ $ 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>\HOL.conj\$_$_) = true | is_conj _ = false; fun prove_conj tab cjs = (case cjs of [c] => if is_conj (Thm.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)) (Thm.term_of c)) fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (Thm.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 = Thm.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) (Misc_Legacy.term_frees (Thm.term_of ct)) (Thm.term_of x); fun is_eqx x eq = (case Thm.term_of eq of Const (\<^const_name>\HOL.eq\, _) $ l $ r => l aconv Thm.term_of x orelse r aconv Thm.term_of x | _ => false); local fun proc ctxt ct = (case Thm.term_of ct of Const (\<^const_name>\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.apply \<^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>\(\) :: prop => _\ Pp (Thm.apply \<^cterm>\Trueprop\ (list_conj (ndx @ dx)))) |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |> Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps}))) |> SOME end | _ => conj_aci_rule (Thm.mk_binop \<^cterm>\(\) :: prop => _\ Pp (Thm.apply \<^cterm>\Trueprop\ (list_conj (eqs @ neqs)))) |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |> Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps}))) |> SOME) end | _ => NONE); in val reduce_ex_simproc = Simplifier.make_simproc \<^context> "reduce_ex_simproc" {lhss = [\<^term>\\x. P x\], proc = K proc}; end; fun raw_dlo_conv ctxt dlo_ss ({qe_bnds, qe_nolb, qe_noub, gst, gs, ...}: Langford_Data.entry) = let val ctxt' = Context_Position.set_visible false (put_simpset dlo_ss ctxt) addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc] val dnfex_conv = Simplifier.rewrite ctxt' val pcv = Simplifier.rewrite (put_simpset dlo_ss ctxt addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib}) in fn p => Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons - (Drule.cterm_add_frees p []) (K Thm.reflexive) (K Thm.reflexive) + (Drule.cterm_frees_of p) (K Thm.reflexive) (K Thm.reflexive) (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p end; val grab_atom_bop = let fun h bounds tm = (case Thm.term_of tm of Const (\<^const_name>\HOL.eq\, T) $ _ $ _ => if domain_type T = HOLogic.boolT then find_args bounds tm else Thm.dest_fun2 tm | Const (\<^const_name>\Not\, _) $ _ => h bounds (Thm.dest_arg tm) | Const (\<^const_name>\All\, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (\<^const_name>\Pure.all\, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (\<^const_name>\Ex\, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (\<^const_name>\HOL.conj\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\HOL.disj\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\HOL.implies\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\Pure.imp\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\Pure.eq\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\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 ctxt ss instance tm); fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st => let fun all x t = Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t) val ts = sort Thm.fast_term_ord (f p) val p' = fold_rev all 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 Thm.term_of t of _ $ _ $ _ => 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 (put_simpset ss ctxt) i | (ss, SOME instance) => Object_Logic.full_atomize_tac ctxt i THEN simp_tac (put_simpset ss ctxt) i THEN (CONVERSION Thm.eta_long_conversion) i THEN (TRY o generalize_tac ctxt (cfrees (#atoms instance))) i THEN Object_Logic.full_atomize_tac ctxt i THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i THEN (simp_tac (put_simpset ss ctxt) i))); end; diff --git a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML @@ -1,1034 +1,1036 @@ (* Title: HOL/Library/Sum_of_Squares/sum_of_squares.ML Author: Amine Chaieb, University of Cambridge Author: Philipp Meyer, TU Muenchen A tactic for proving nonlinear inequalities. *) signature SUM_OF_SQUARES = sig datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic val trace: bool Config.T val debug: bool Config.T val trace_message: Proof.context -> (unit -> string) -> unit val debug_message: Proof.context -> (unit -> string) -> unit exception Failure of string; end structure Sum_of_Squares: SUM_OF_SQUARES = struct val max = Integer.max; val denominator_rat = Rat.dest #> snd #> Rat.of_int; fun int_of_rat a = (case Rat.dest a of (i, 1) => i | _ => error "int_of_rat: not an int"); fun lcm_rat x y = Rat.of_int (Integer.lcm (int_of_rat x) (int_of_rat y)); fun rat_pow r i = let fun pow r i = if i = 0 then @1 else let val d = pow r (i div 2) in d * d * (if i mod 2 = 0 then @1 else r) end in if i < 0 then pow (Rat.inv r) (~ i) else pow r i end; fun round_rat r = let val (a,b) = Rat.dest (abs r) val d = a div b val s = if r < @0 then ~ o Rat.of_int else Rat.of_int val x2 = 2 * (a - (b * d)) in s (if x2 >= b then d + 1 else d) end val trace = Attrib.setup_config_bool \<^binding>\sos_trace\ (K false); val debug = Attrib.setup_config_bool \<^binding>\sos_debug\ (K false); fun trace_message ctxt msg = if Config.get ctxt trace orelse Config.get ctxt debug then tracing (msg ()) else (); fun debug_message ctxt msg = if Config.get ctxt debug then tracing (msg ()) else (); exception Sanity; exception Unsolvable; exception Failure of string; datatype proof_method = Certificate of RealArith.pss_tree | Prover of (string -> string) (* Turn a rational into a decimal string with d sig digits. *) local fun normalize y = if abs y < @1/10 then normalize (@10 * y) - 1 else if abs y >= @1 then normalize (y / @10) + 1 else 0 in fun decimalize d x = if x = @0 then "0.0" else let val y = abs x val e = normalize y val z = rat_pow @10 (~ e) * y + @1 val k = int_of_rat (round_rat (rat_pow @10 d * z)) in (if x < @0 then "-0." else "0.") ^ implode (tl (raw_explode(string_of_int k))) ^ (if e = 0 then "" else "e" ^ string_of_int e) end end; (* Iterations over numbers, and lists indexed by numbers. *) fun itern k l f a = (case l of [] => a | h::t => itern (k + 1) t f (f h k a)); fun iter (m,n) f a = if n < m then a else iter (m + 1, n) f (f m a); (* The main types. *) type vector = int * Rat.rat FuncUtil.Intfunc.table; type matrix = (int * int) * Rat.rat FuncUtil.Intpairfunc.table; fun iszero (_, r) = r = @0; (* Vectors. Conventionally indexed 1..n. *) fun vector_0 n = (n, FuncUtil.Intfunc.empty): vector; fun dim (v: vector) = fst v; fun vector_cmul c (v: vector) = let val n = dim v in if c = @0 then vector_0 n else (n,FuncUtil.Intfunc.map (fn _ => fn x => c * x) (snd v)) end; fun vector_of_list l = let val n = length l in (n, fold_rev FuncUtil.Intfunc.update (1 upto n ~~ l) FuncUtil.Intfunc.empty): vector end; (* Matrices; again rows and columns indexed from 1. *) fun dimensions (m: matrix) = fst m; fun row k (m: matrix) : vector = let val (_, j) = dimensions m in (j, FuncUtil.Intpairfunc.fold (fn ((i, j), c) => fn a => if i = k then FuncUtil.Intfunc.update (j, c) a else a) (snd m) FuncUtil.Intfunc.empty) end; (* Monomials. *) fun monomial_eval assig m = FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a * rat_pow (FuncUtil.Ctermfunc.apply assig x) k) m @1; val monomial_1 = FuncUtil.Ctermfunc.empty; fun monomial_var x = FuncUtil.Ctermfunc.onefunc (x, 1); val monomial_mul = FuncUtil.Ctermfunc.combine Integer.add (K false); fun monomial_multidegree m = FuncUtil.Ctermfunc.fold (fn (_, k) => fn a => k + a) m 0; fun monomial_variables m = FuncUtil.Ctermfunc.dom m; (* Polynomials. *) fun eval assig p = FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a + c * monomial_eval assig m) p @0; val poly_0 = FuncUtil.Monomialfunc.empty; fun poly_isconst p = FuncUtil.Monomialfunc.fold (fn (m, _) => fn a => FuncUtil.Ctermfunc.is_empty m andalso a) p true; fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x, @1); fun poly_const c = if c = @0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c); fun poly_cmul c p = if c = @0 then poly_0 else FuncUtil.Monomialfunc.map (fn _ => fn x => c * x) p; fun poly_neg p = FuncUtil.Monomialfunc.map (K ~) p; fun poly_add p1 p2 = FuncUtil.Monomialfunc.combine (curry op +) (fn x => x = @0) p1 p2; fun poly_sub p1 p2 = poly_add p1 (poly_neg p2); fun poly_cmmul (c,m) p = if c = @0 then poly_0 else if FuncUtil.Ctermfunc.is_empty m then FuncUtil.Monomialfunc.map (fn _ => fn d => c * d) p else FuncUtil.Monomialfunc.fold (fn (m', d) => fn a => (FuncUtil.Monomialfunc.update (monomial_mul m m', c * d) a)) p poly_0; fun poly_mul p1 p2 = FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => poly_add (poly_cmmul (c,m) p2) a) p1 poly_0; fun poly_square p = poly_mul p p; fun poly_pow p k = if k = 0 then poly_const @1 else if k = 1 then p else let val q = poly_square(poly_pow p (k div 2)) in if k mod 2 = 1 then poly_mul p q else q end; fun multidegree p = FuncUtil.Monomialfunc.fold (fn (m, _) => fn a => max (monomial_multidegree m) a) p 0; fun poly_variables p = sort Thm.fast_term_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, _) => union (is_equal o Thm.fast_term_ord) (monomial_variables m)) p []); (* Conversion from HOL term. *) local val neg_tm = \<^cterm>\uminus :: real \ _\ val add_tm = \<^cterm>\(+) :: real \ _\ val sub_tm = \<^cterm>\(-) :: real \ _\ val mul_tm = \<^cterm>\(*) :: real \ _\ val inv_tm = \<^cterm>\inverse :: real \ _\ val div_tm = \<^cterm>\(/) :: real \ _\ val pow_tm = \<^cterm>\(^) :: real \ _\ val zero_tm = \<^cterm>\0:: real\ val is_numeral = can (HOLogic.dest_number o Thm.term_of) fun poly_of_term tm = if tm aconvc zero_tm then poly_0 else if RealArith.is_ratconst tm then poly_const(RealArith.dest_ratconst tm) else (let val (lop, r) = Thm.dest_comb tm in if lop aconvc neg_tm then poly_neg(poly_of_term r) else if lop aconvc inv_tm then let val p = poly_of_term r in if poly_isconst p then poly_const(Rat.inv (eval FuncUtil.Ctermfunc.empty p)) else error "poly_of_term: inverse of non-constant polyomial" end else (let val (opr,l) = Thm.dest_comb lop in if opr aconvc pow_tm andalso is_numeral r then poly_pow (poly_of_term l) ((snd o HOLogic.dest_number o Thm.term_of) r) else if opr aconvc add_tm then poly_add (poly_of_term l) (poly_of_term r) else if opr aconvc sub_tm then poly_sub (poly_of_term l) (poly_of_term r) else if opr aconvc mul_tm then poly_mul (poly_of_term l) (poly_of_term r) else if opr aconvc div_tm then let val p = poly_of_term l val q = poly_of_term r in if poly_isconst q then poly_cmul (Rat.inv (eval FuncUtil.Ctermfunc.empty q)) p else error "poly_of_term: division by non-constant polynomial" end else poly_var tm end handle CTERM ("dest_comb",_) => poly_var tm) end handle CTERM ("dest_comb",_) => poly_var tm) in val poly_of_term = fn tm => if type_of (Thm.term_of tm) = \<^typ>\real\ then poly_of_term tm else error "poly_of_term: term does not have real type" end; (* String of vector (just a list of space-separated numbers). *) fun sdpa_of_vector (v: vector) = let val n = dim v val strs = map (decimalize 20 o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i @0)) (1 upto n) in space_implode " " strs ^ "\n" end; fun triple_int_ord ((a, b, c), (a', b', c')) = prod_ord int_ord (prod_ord int_ord int_ord) ((a, (b, c)), (a', (b', c'))); structure Inttriplefunc = FuncFun(type key = int * int * int val ord = triple_int_ord); (* Parse back csdp output. *) local val decimal_digits = Scan.many1 Symbol.is_ascii_digit val decimal_nat = decimal_digits >> (#1 o Library.read_int); val decimal_int = decimal_nat >> Rat.of_int; val decimal_sig = decimal_int -- Scan.option (Scan.$$ "." |-- decimal_digits) >> (fn (a, NONE) => a | (a, SOME bs) => a + Rat.of_int (#1 (Library.read_int bs)) / rat_pow @10 (length bs)); fun signed neg parse = $$ "-" |-- parse >> neg || $$ "+" |-- parse || parse; val exponent = ($$ "e" || $$ "E") |-- signed ~ decimal_nat; val decimal = signed ~ decimal_sig -- Scan.optional exponent 0 >> (fn (a, b) => a * rat_pow @10 b); val csdp_output = decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) --| Scan.many Symbol.not_eof >> (fn (a, bs) => vector_of_list (a :: map_filter I bs)); in fun parse_csdpoutput s = Symbol.scanner "Malformed CSDP output" csdp_output (raw_explode s); end; (* Try some apparently sensible scaling first. Note that this is purely to *) (* get a cleaner translation to floating-point, and doesn't affect any of *) (* the results, in principle. In practice it seems a lot better when there *) (* are extreme numbers in the original problem. *) (* Version for (int*int*int) keys *) local fun max_rat x y = if x < y then y else x fun common_denominator fld amat acc = fld (fn (_,c) => fn a => lcm_rat (denominator_rat c) a) amat acc fun maximal_element fld amat acc = fld (fn (_,c) => fn maxa => max_rat maxa (abs c)) amat acc fun float_of_rat x = let val (a,b) = Rat.dest x in Real.fromInt a / Real.fromInt b end; fun int_of_float x = (trunc x handle Overflow => 0 | Domain => 0) in fun tri_scale_then solver (obj:vector) mats = let val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats @1 val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj) @1 val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 * x)) mats val obj' = vector_cmul cd2 obj val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' @0 val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') @0 val scal1 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0)) val scal2 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0)) val mats'' = map (Inttriplefunc.map (fn _ => fn x => x * scal1)) mats' val obj'' = vector_cmul scal2 obj' in solver obj'' mats'' end end; (* Round a vector to "nice" rationals. *) fun nice_rational n x = round_rat (n * x) / n; fun nice_vector n ((d,v) : vector) = (d, FuncUtil.Intfunc.fold (fn (i,c) => fn a => let val y = nice_rational n c in if c = @0 then a else FuncUtil.Intfunc.update (i,y) a end) v FuncUtil.Intfunc.empty): vector fun dest_ord f x = is_equal (f x); (* Stuff for "equations" ((int*int*int)->num functions). *) fun tri_equation_cmul c eq = if c = @0 then Inttriplefunc.empty else Inttriplefunc.map (fn _ => fn d => c * d) eq; fun tri_equation_add eq1 eq2 = Inttriplefunc.combine (curry op +) (fn x => x = @0) eq1 eq2; fun tri_equation_eval assig eq = let fun value v = Inttriplefunc.apply assig v in Inttriplefunc.fold (fn (v, c) => fn a => a + value v * c) eq @0 end; (* Eliminate all variables, in an essentially arbitrary order. *) fun tri_eliminate_all_equations one = let fun choose_variable eq = let val (v,_) = Inttriplefunc.choose eq in if is_equal (triple_int_ord(v,one)) then let val eq' = Inttriplefunc.delete_safe v eq in if Inttriplefunc.is_empty eq' then error "choose_variable" else fst (Inttriplefunc.choose eq') end else v end fun eliminate dun eqs = (case eqs of [] => dun | eq :: oeqs => if Inttriplefunc.is_empty eq then eliminate dun oeqs else let val v = choose_variable eq val a = Inttriplefunc.apply eq v val eq' = tri_equation_cmul ((Rat.of_int ~1) / a) (Inttriplefunc.delete_safe v eq) fun elim e = let val b = Inttriplefunc.tryapplyd e v @0 in if b = @0 then e else tri_equation_add e (tri_equation_cmul (~ b / a) eq) end in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun)) (map elim oeqs) end) in fn eqs => let val assig = eliminate Inttriplefunc.empty eqs val vs = Inttriplefunc.fold (fn (_, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig [] in (distinct (dest_ord triple_int_ord) vs,assig) end end; (* Multiply equation-parametrized poly by regular poly and add accumulator. *) fun tri_epoly_pmul p q acc = FuncUtil.Monomialfunc.fold (fn (m1, c) => fn a => FuncUtil.Monomialfunc.fold (fn (m2, e) => fn b => let val m = monomial_mul m1 m2 val es = FuncUtil.Monomialfunc.tryapplyd b m Inttriplefunc.empty in FuncUtil.Monomialfunc.update (m,tri_equation_add (tri_equation_cmul c e) es) b end) q a) p acc; (* Hence produce the "relevant" monomials: those whose squares lie in the *) (* Newton polytope of the monomials in the input. (This is enough according *) (* to Reznik: "Extremal PSD forms with few terms", Duke Math. Journal, *) (* vol 45, pp. 363--374, 1978. *) (* *) (* These are ordered in sort of decreasing degree. In particular the *) (* constant monomial is last; this gives an order in diagonalization of the *) (* quadratic form that will tend to display constants. *) (* Diagonalize (Cholesky/LDU) the matrix corresponding to a quadratic form. *) local fun diagonalize n i m = if FuncUtil.Intpairfunc.is_empty (snd m) then [] else let val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) @0 in if a11 < @0 then raise Failure "diagonalize: not PSD" else if a11 = @0 then if FuncUtil.Intfunc.is_empty (snd (row i m)) then diagonalize n (i + 1) m else raise Failure "diagonalize: not PSD ___ " else let val v = row i m val v' = (fst v, FuncUtil.Intfunc.fold (fn (i, c) => fn a => let val y = c / a11 in if y = @0 then a else FuncUtil.Intfunc.update (i,y) a end) (snd v) FuncUtil.Intfunc.empty) fun upt0 x y a = if y = @0 then a else FuncUtil.Intpairfunc.update (x,y) a val m' = ((n, n), iter (i + 1, n) (fn j => iter (i + 1, n) (fn k => (upt0 (j, k) (FuncUtil.Intpairfunc.tryapplyd (snd m) (j, k) @0 - FuncUtil.Intfunc.tryapplyd (snd v) j @0 * FuncUtil.Intfunc.tryapplyd (snd v') k @0)))) FuncUtil.Intpairfunc.empty) in (a11, v') :: diagonalize n (i + 1) m' end end in fun diag m = let val nn = dimensions m val n = fst nn in if snd nn <> n then error "diagonalize: non-square matrix" else diagonalize n 1 m end end; (* Enumeration of monomials with given multidegree bound. *) fun enumerate_monomials d vars = if d < 0 then [] else if d = 0 then [FuncUtil.Ctermfunc.empty] else if null vars then [monomial_1] else let val alts = map_range (fn k => let val oths = enumerate_monomials (d - k) (tl vars) in map (fn ks => if k = 0 then ks else FuncUtil.Ctermfunc.update (hd vars, k) ks) oths end) (d + 1) in flat alts end; (* Enumerate products of distinct input polys with degree <= d. *) (* We ignore any constant input polynomials. *) (* Give the output polynomial and a record of how it was derived. *) fun enumerate_products d pols = if d = 0 then [(poly_const @1, RealArith.Rational_lt @1)] else if d < 0 then [] else (case pols of [] => [(poly_const @1, RealArith.Rational_lt @1)] | (p, b) :: ps => let val e = multidegree p in if e = 0 then enumerate_products d ps else enumerate_products d ps @ map (fn (q, c) => (poly_mul p q, RealArith.Product (b, c))) (enumerate_products (d - e) ps) end) (* Convert regular polynomial. Note that we treat (0,0,0) as -1. *) fun epoly_of_poly p = FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0, 0, 0), ~ c)) a) p FuncUtil.Monomialfunc.empty; (* String for block diagonal matrix numbered k. *) fun sdpa_of_blockdiagonal k m = let val pfx = string_of_int k ^" " val ents = Inttriplefunc.fold (fn ((b, i, j), c) => fn a => if i > j then a else ((b, i, j), c) :: a) m [] val entss = sort (triple_int_ord o apply2 fst) ents in fold_rev (fn ((b,i,j),c) => fn a => pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ " " ^ decimalize 20 c ^ "\n" ^ a) entss "" end; (* SDPA for problem using block diagonal (i.e. multiple SDPs) *) fun sdpa_of_blockproblem nblocks blocksizes obj mats = let val m = length mats - 1 in string_of_int m ^ "\n" ^ string_of_int nblocks ^ "\n" ^ (space_implode " " (map string_of_int blocksizes)) ^ "\n" ^ sdpa_of_vector obj ^ fold_rev (fn (k, m) => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a) (1 upto length mats ~~ mats) "" end; (* Run prover on a problem in block diagonal form. *) fun run_blockproblem prover nblocks blocksizes obj mats = parse_csdpoutput (prover (sdpa_of_blockproblem nblocks blocksizes obj mats)) (* 3D versions of matrix operations to consider blocks separately. *) val bmatrix_add = Inttriplefunc.combine (curry op +) (fn x => x = @0); fun bmatrix_cmul c bm = if c = @0 then Inttriplefunc.empty else Inttriplefunc.map (fn _ => fn x => c * x) bm; val bmatrix_neg = bmatrix_cmul (Rat.of_int ~1); (* Smash a block matrix into components. *) fun blocks blocksizes bm = map (fn (bs, b0) => let val m = Inttriplefunc.fold (fn ((b, i, j), c) => fn a => if b = b0 then FuncUtil.Intpairfunc.update ((i, j), c) a else a) bm FuncUtil.Intpairfunc.empty val _ = FuncUtil.Intpairfunc.fold (fn ((i, j), _) => fn a => max a (max i j)) m 0 in (((bs, bs), m): matrix) end) (blocksizes ~~ (1 upto length blocksizes)); (* FIXME : Get rid of this !!!*) local fun tryfind_with msg _ [] = raise Failure msg | tryfind_with _ f (x::xs) = (f x handle Failure s => tryfind_with s f xs); in fun tryfind f = tryfind_with "tryfind" f end (* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *) fun real_positivnullstellensatz_general ctxt prover linf d eqs leqs pol = let val vars = fold_rev (union (op aconvc) o poly_variables) (pol :: eqs @ map fst leqs) [] val monoid = if linf then (poly_const @1, RealArith.Rational_lt @1):: (filter (fn (p,_) => multidegree p <= d) leqs) else enumerate_products d leqs val nblocks = length monoid fun mk_idmultiplier k p = let val e = d - multidegree p val mons = enumerate_monomials e vars val nons = mons ~~ (1 upto length mons) in (mons, fold_rev (fn (m, n) => FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((~k, ~n, n), @1))) nons FuncUtil.Monomialfunc.empty) end fun mk_sqmultiplier k (p,_) = let val e = (d - multidegree p) div 2 val mons = enumerate_monomials e vars val nons = mons ~~ (1 upto length mons) in (mons, fold_rev (fn (m1, n1) => fold_rev (fn (m2, n2) => fn a => let val m = monomial_mul m1 m2 in if n1 > n2 then a else let val c = if n1 = n2 then @1 else @2 val e = FuncUtil.Monomialfunc.tryapplyd a m Inttriplefunc.empty in FuncUtil.Monomialfunc.update (m, tri_equation_add (Inttriplefunc.onefunc ((k, n1, n2), c)) e) a end end) nons) nons FuncUtil.Monomialfunc.empty) end val (sqmonlist,sqs) = split_list (map2 mk_sqmultiplier (1 upto length monoid) monoid) val (_(*idmonlist*),ids) = split_list (map2 mk_idmultiplier (1 upto length eqs) eqs) val blocksizes = map length sqmonlist val bigsum = fold_rev (fn (p, q) => fn a => tri_epoly_pmul p q a) (eqs ~~ ids) (fold_rev (fn ((p, _), s) => fn a => tri_epoly_pmul p s a) (monoid ~~ sqs) (epoly_of_poly (poly_neg pol))) val eqns = FuncUtil.Monomialfunc.fold (fn (_, e) => fn a => e :: a) bigsum [] val (pvs, assig) = tri_eliminate_all_equations (0, 0, 0) eqns val qvars = (0, 0, 0) :: pvs val allassig = fold_rev (fn v => Inttriplefunc.update (v, (Inttriplefunc.onefunc (v, @1)))) pvs assig fun mk_matrix v = Inttriplefunc.fold (fn ((b, i, j), ass) => fn m => if b < 0 then m else let val c = Inttriplefunc.tryapplyd ass v @0 in if c = @0 then m else Inttriplefunc.update ((b, j, i), c) (Inttriplefunc.update ((b, i, j), c) m) end) allassig Inttriplefunc.empty val diagents = Inttriplefunc.fold (fn ((b, i, j), e) => fn a => if b > 0 andalso i = j then tri_equation_add e a else a) allassig Inttriplefunc.empty val mats = map mk_matrix qvars val obj = (length pvs, itern 1 pvs (fn v => fn i => FuncUtil.Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v @0)) FuncUtil.Intfunc.empty) val raw_vec = if null pvs then vector_0 0 else tri_scale_then (run_blockproblem prover nblocks blocksizes) obj mats fun int_element (_, v) i = FuncUtil.Intfunc.tryapplyd v i @0 fun find_rounding d = let val _ = debug_message ctxt (fn () => "Trying rounding with limit "^Rat.string_of_rat d ^ "\n") val vec = nice_vector d raw_vec val blockmat = iter (1, dim vec) (fn i => fn a => bmatrix_add (bmatrix_cmul (int_element vec i) (nth mats i)) a) (bmatrix_neg (nth mats 0)) val allmats = blocks blocksizes blockmat in (vec, map diag allmats) end val (vec, ratdias) = if null pvs then find_rounding @1 else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map (rat_pow @2) (5 upto 66)) val newassigs = fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k)) (1 upto dim vec) (Inttriplefunc.onefunc ((0, 0, 0), Rat.of_int ~1)) val finalassigs = Inttriplefunc.fold (fn (v, e) => fn a => Inttriplefunc.update (v, tri_equation_eval newassigs e) a) allassig newassigs fun poly_of_epoly p = FuncUtil.Monomialfunc.fold (fn (v, e) => fn a => FuncUtil.Monomialfunc.updatep iszero (v, tri_equation_eval finalassigs e) a) p FuncUtil.Monomialfunc.empty fun mk_sos mons = let fun mk_sq (c, m) = (c, fold_rev (fn k => fn a => FuncUtil.Monomialfunc.updatep iszero (nth mons (k - 1), int_element m k) a) (1 upto length mons) FuncUtil.Monomialfunc.empty) in map mk_sq end val sqs = map2 mk_sos sqmonlist ratdias val cfs = map poly_of_epoly ids val msq = filter (fn (_, b) => not (null b)) (map2 pair monoid sqs) fun eval_sq sqs = fold_rev (fn (c, q) => poly_add (poly_cmul c (poly_mul q q))) sqs poly_0 val sanity = fold_rev (fn ((p, _), s) => poly_add (poly_mul p (eval_sq s))) msq (fold_rev (fn (p, q) => poly_add (poly_mul p q)) (cfs ~~ eqs) (poly_neg pol)) in if not(FuncUtil.Monomialfunc.is_empty sanity) then raise Sanity else (cfs, map (fn (a, b) => (snd a, b)) msq) end (* Iterative deepening. *) fun deepen ctxt f n = (trace_message ctxt (fn () => "Searching with depth limit " ^ string_of_int n); (f n handle Failure s => (trace_message ctxt (fn () => "failed with message: " ^ s); deepen ctxt f (n + 1)))); (* Map back polynomials and their composites to a positivstellensatz. *) fun cterm_of_sqterm (c, p) = RealArith.Product (RealArith.Rational_lt c, RealArith.Square p); fun cterm_of_sos (pr,sqs) = if null sqs then pr else RealArith.Product (pr, foldr1 RealArith.Sum (map cterm_of_sqterm sqs)); (* Interface to HOL. *) local open Conv val concl = Thm.dest_arg o Thm.cprop_of in (* FIXME: Replace tryfind by get_first !! *) fun real_nonlinear_prover proof_method ctxt = let val {add = _, mul = _, neg = _, pow = _, sub = _, main = real_poly_conv} = Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt (the (Semiring_Normalizer.match ctxt \<^cterm>\(0::real) + 1\)) Thm.term_ord fun mainf cert_choice translator (eqs, les, lts) = let val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs val le0 = map (poly_of_term o Thm.dest_arg o concl) les val lt0 = map (poly_of_term o Thm.dest_arg o concl) lts val eqp0 = map_index (fn (i, t) => (t,RealArith.Axiom_eq i)) eq0 val lep0 = map_index (fn (i, t) => (t,RealArith.Axiom_le i)) le0 val ltp0 = map_index (fn (i, t) => (t,RealArith.Axiom_lt i)) lt0 val (keq,eq) = List.partition (fn (p, _) => multidegree p = 0) eqp0 val (klep,lep) = List.partition (fn (p, _) => multidegree p = 0) lep0 val (kltp,ltp) = List.partition (fn (p, _) => multidegree p = 0) ltp0 fun trivial_axiom (p, ax) = (case ax of RealArith.Axiom_eq n => if eval FuncUtil.Ctermfunc.empty p <> @0 then nth eqs n else raise Failure "trivial_axiom: Not a trivial axiom" | RealArith.Axiom_le n => if eval FuncUtil.Ctermfunc.empty p < @0 then nth les n else raise Failure "trivial_axiom: Not a trivial axiom" | RealArith.Axiom_lt n => if eval FuncUtil.Ctermfunc.empty p <= @0 then nth lts n else raise Failure "trivial_axiom: Not a trivial axiom" | _ => error "trivial_axiom: Not a trivial axiom") in let val th = tryfind trivial_axiom (keq @ klep @ kltp) in (fconv_rule (arg_conv (arg1_conv (real_poly_conv ctxt)) then_conv Numeral_Simprocs.field_comp_conv ctxt) th, RealArith.Trivial) end handle Failure _ => let val proof = (case proof_method of Certificate certs => (* choose certificate *) let fun chose_cert [] (RealArith.Cert c) = c | chose_cert (RealArith.Left::s) (RealArith.Branch (l, _)) = chose_cert s l | chose_cert (RealArith.Right::s) (RealArith.Branch (_, r)) = chose_cert s r | chose_cert _ _ = error "certificate tree in invalid form" in chose_cert cert_choice certs end | Prover prover => (* call prover *) let val pol = fold_rev poly_mul (map fst ltp) (poly_const @1) val leq = lep @ ltp fun tryall d = let val e = multidegree pol val k = if e = 0 then 0 else d div e val eq' = map fst eq in tryfind (fn i => (d, i, real_positivnullstellensatz_general ctxt prover false d eq' leq (poly_neg(poly_pow pol i)))) (0 upto k) end val (_,i,(cert_ideal,cert_cone)) = deepen ctxt tryall 0 val proofs_ideal = map2 (fn q => fn (_,ax) => RealArith.Eqmul(q,ax)) cert_ideal eq val proofs_cone = map cterm_of_sos cert_cone val proof_ne = if null ltp then RealArith.Rational_lt @1 else let val p = foldr1 RealArith.Product (map snd ltp) in funpow i (fn q => RealArith.Product (p, q)) (RealArith.Rational_lt @1) end in foldr1 RealArith.Sum (proof_ne :: proofs_ideal @ proofs_cone) end) in (translator (eqs,les,lts) proof, RealArith.Cert proof) end end in mainf end end (* FIXME : This is very bad!!!*) fun subst_conv eqs t = let val t' = fold (Thm.lambda o Thm.lhs_of) eqs t in Conv.fconv_rule (Thm.beta_conversion true) (fold (fn a => fn b => Thm.combination b a) eqs (Thm.reflexive t')) end (* A wrapper that tries to substitute away variables first. *) local open Conv val concl = Thm.dest_arg o Thm.cprop_of val shuffle1 = fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" by (atomize (full)) (simp add: field_simps)}) val shuffle2 = fconv_rule (rewr_conv @{lemma "(x + a == y) == (x == y - (a::real))" by (atomize (full)) (simp add: field_simps)}) fun substitutable_monomial fvs tm = (case Thm.term_of tm of Free (_, \<^typ>\real\) => if not (member (op aconvc) fvs tm) then (@1, tm) else raise Failure "substitutable_monomial" | \<^term>\(*) :: real \ _\ $ _ $ (Free _) => if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso not (member (op aconvc) fvs (Thm.dest_arg tm)) then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm) else raise Failure "substitutable_monomial" | \<^term>\(+) :: real \ _\$_$_ => - (substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm) + (substitutable_monomial (merge (op aconvc) (fvs, Drule.cterm_frees_of (Thm.dest_arg tm))) + (Thm.dest_arg1 tm) handle Failure _ => - substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm)) + substitutable_monomial (merge (op aconvc) (fvs, Drule.cterm_frees_of (Thm.dest_arg1 tm))) + (Thm.dest_arg tm)) | _ => raise Failure "substitutable_monomial") fun isolate_variable v th = let val w = Thm.dest_arg1 (Thm.cprop_of th) in if v aconvc w then th else (case Thm.term_of w of \<^term>\(+) :: real \ _\ $ _ $ _ => if Thm.dest_arg1 w aconvc v then shuffle2 th else isolate_variable v (shuffle1 th) | _ => error "isolate variable : This should not happen?") end in fun real_nonlinear_subst_prover prover ctxt = let val {add = _, mul = real_poly_mul_conv, neg = _, pow = _, sub = _, main = real_poly_conv} = Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt (the (Semiring_Normalizer.match ctxt \<^cterm>\(0::real) + 1\)) Thm.term_ord fun make_substitution th = let val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th)) val th1 = Drule.arg_cong_rule (Thm.apply \<^cterm>\(*) :: real \ _\ (RealArith.cterm_of_rat (Rat.inv c))) (mk_meta_eq th) val th2 = fconv_rule (binop_conv (real_poly_mul_conv ctxt)) th1 in fconv_rule (arg_conv (real_poly_conv ctxt)) (isolate_variable v th2) end fun oprconv cv ct = let val g = Thm.dest_fun2 ct in if g aconvc \<^cterm>\(\) :: real \ _\ orelse g aconvc \<^cterm>\(<) :: real \ _\ then arg_conv cv ct else arg1_conv cv ct end fun mainf cert_choice translator = let fun substfirst (eqs, les, lts) = (let val eth = tryfind make_substitution eqs val modify = fconv_rule (arg_conv (oprconv(subst_conv [eth] then_conv (real_poly_conv ctxt)))) in substfirst (filter_out (fn t => (Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of) t aconvc \<^cterm>\0::real\) (map modify eqs), map modify les, map modify lts) end handle Failure _ => real_nonlinear_prover prover ctxt cert_choice translator (rev eqs, rev les, rev lts)) in substfirst end in mainf end (* Overall function. *) fun real_sos prover ctxt = RealArith.gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt) end; val known_sos_constants = [\<^term>\(\)\, \<^term>\Trueprop\, \<^term>\HOL.False\, \<^term>\HOL.implies\, \<^term>\HOL.conj\, \<^term>\HOL.disj\, \<^term>\Not\, \<^term>\(=) :: bool \ _\, \<^term>\All :: (real \ _) \ _\, \<^term>\Ex :: (real \ _) \ _\, \<^term>\(=) :: real \ _\, \<^term>\(<) :: real \ _\, \<^term>\(\) :: real \ _\, \<^term>\(+) :: real \ _\, \<^term>\(-) :: real \ _\, \<^term>\(*) :: real \ _\, \<^term>\uminus :: real \ _\, \<^term>\(/) :: real \ _\, \<^term>\inverse :: real \ _\, \<^term>\(^) :: real \ _\, \<^term>\abs :: real \ _\, \<^term>\min :: real \ _\, \<^term>\max :: real \ _\, \<^term>\0::real\, \<^term>\1::real\, \<^term>\numeral :: num \ nat\, \<^term>\numeral :: num \ real\, \<^term>\Num.Bit0\, \<^term>\Num.Bit1\, \<^term>\Num.One\]; fun check_sos kcts ct = let val t = Thm.term_of ct val _ = if not (null (Term.add_tfrees t []) andalso null (Term.add_tvars t [])) then error "SOS: not sos. Additional type varables" else () val fs = Term.add_frees t [] val _ = if exists (fn ((_,T)) => not (T = \<^typ>\real\)) fs then error "SOS: not sos. Variables with type not real" else () val vs = Term.add_vars t [] val _ = if exists (fn ((_,T)) => not (T = \<^typ>\real\)) vs then error "SOS: not sos. Variables with type not real" else () val ukcs = subtract (fn (t,p) => Const p aconv t) kcts (Term.add_consts t []) val _ = if null ukcs then () else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs)) in () end fun core_sos_tac print_cert prover = SUBPROOF (fn {concl, context = ctxt, ...} => let val _ = check_sos known_sos_constants concl val (th, certificates) = real_sos prover ctxt (Thm.dest_arg concl) val _ = print_cert certificates in resolve_tac ctxt [th] 1 end); fun default_SOME _ NONE v = SOME v | default_SOME _ (SOME v) _ = SOME v; fun lift_SOME f NONE a = f a | lift_SOME _ (SOME a) _ = SOME a; local val is_numeral = can (HOLogic.dest_number o Thm.term_of) in fun get_denom b ct = (case Thm.term_of ct of \<^term>\(/) :: real \ _\ $ _ $ _ => if is_numeral (Thm.dest_arg ct) then get_denom b (Thm.dest_arg1 ct) else default_SOME (get_denom b) (get_denom b (Thm.dest_arg ct)) (Thm.dest_arg ct, b) | \<^term>\(<) :: real \ _\ $ _ $ _ => lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct) | \<^term>\(\) :: real \ _\ $ _ $ _ => lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct) | _ $ _ => lift_SOME (get_denom b) (get_denom b (Thm.dest_fun ct)) (Thm.dest_arg ct) | _ => NONE) end; val sos_ss = @{context} |> fold Simplifier.add_simp @{thms field_simps} |> Simplifier.del_simp @{thm mult_nonneg_nonneg} |> Simplifier.simpset_of; fun elim_one_denom_tac ctxt = CSUBGOAL (fn (P, i) => (case get_denom false P of NONE => no_tac | SOME (d, ord) => let val simp_ctxt = ctxt |> Simplifier.put_simpset sos_ss val th = Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)] (if ord then @{lemma "(d=0 \ P) \ (d>0 \ P) \ (d<(0::real) \ P) \ P" by auto} else @{lemma "(d=0 \ P) \ (d \ (0::real) \ P) \ P" by blast}) in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end)); fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i); fun sos_tac print_cert prover ctxt = Object_Logic.full_atomize_tac ctxt THEN' elim_denom_tac ctxt THEN' core_sos_tac print_cert prover ctxt; end; diff --git a/src/HOL/Tools/Qelim/qelim.ML b/src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML +++ b/src/HOL/Tools/Qelim/qelim.ML @@ -1,73 +1,73 @@ (* Title: HOL/Tools/Qelim/qelim.ML Author: Amine Chaieb, TU Muenchen Generic quantifier elimination conversions for HOL formulae. *) signature QELIM = sig val gen_qelim_conv: Proof.context -> conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a -> ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv val standard_qelim_conv: Proof.context -> (cterm list -> conv) -> (cterm list -> conv) -> (cterm list -> conv) -> conv end; structure Qelim: QELIM = struct val all_not_ex = mk_meta_eq @{thm "all_not_ex"}; fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv = let fun conv env p = case Thm.term_of p of Const(s,T)$_$_ => if domain_type T = HOLogic.boolT andalso member (op =) [\<^const_name>\HOL.conj\, \<^const_name>\HOL.disj\, \<^const_name>\HOL.implies\, \<^const_name>\HOL.eq\] s then Conv.binop_conv (conv env) p else atcv env p | Const(\<^const_name>\Not\,_)$_ => Conv.arg_conv (conv env) p | Const(\<^const_name>\Ex\,_)$Abs(s,_,_) => let val (e,p0) = Thm.dest_comb p val (x,p') = Thm.dest_abs (SOME s) p0 val env' = ins x env val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p') |> Drule.arg_cong_rule e val th' = simpex_conv (Thm.rhs_of th) val (_, r) = Thm.dest_equals (Thm.cprop_of th') in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th)) else Thm.transitive (Thm.transitive th th') (conv env r) end | Const(\<^const_name>\Ex\,_)$ _ => (Thm.eta_long_conversion then_conv conv env) p | Const(\<^const_name>\All\, _)$_ => let val allT = Thm.ctyp_of_cterm (Thm.dest_fun p) val T = Thm.dest_ctyp0 (Thm.dest_ctyp0 allT) val p = Thm.dest_arg p val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex in Thm.transitive th (conv env (Thm.rhs_of th)) end | _ => atcv env p in precv then_conv (conv env) then_conv postcv end (* Instantiation of some parameter for most common cases *) local val ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib}); fun pcv ctxt = Simplifier.rewrite (put_simpset ss ctxt) in fun standard_qelim_conv ctxt atcv ncv qcv p = let val pcv = pcv ctxt - in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end + in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_frees_of p) atcv ncv qcv p end end; end; diff --git a/src/HOL/Tools/groebner.ML b/src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML +++ b/src/HOL/Tools/groebner.ML @@ -1,986 +1,985 @@ (* Title: HOL/Tools/groebner.ML Author: Amine Chaieb, TU Muenchen *) signature GROEBNER = sig val ring_and_ideal_conv: {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list, vars: cterm list, semiring: cterm list * thm list, ideal : thm list} -> (cterm -> Rat.rat) -> (Rat.rat -> cterm) -> conv -> conv -> {ring_conv: Proof.context -> conv, simple_ideal: cterm list -> cterm -> cterm ord -> cterm list, multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list, poly_eq_ss: simpset, unwind_conv: Proof.context -> conv} val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic end structure Groebner : GROEBNER = struct val concl = Thm.cprop_of #> Thm.dest_arg; fun is_binop ct ct' = (case Thm.term_of ct' of c $ _ $ _ => Thm.term_of ct aconv c | _ => false); fun dest_binary ct ct' = if is_binop ct ct' then Thm.dest_binop ct' else raise CTERM ("dest_binary: bad binop", [ct, ct']) val denominator_rat = Rat.dest #> snd #> Rat.of_int; fun int_of_rat a = case Rat.dest a of (i,1) => i | _ => error "int_of_rat: not an int"; val lcm_rat = fn x => fn y => Rat.of_int (Integer.lcm (int_of_rat x) (int_of_rat y)); val (eqF_intr, eqF_elim) = let val [th1,th2] = @{thms PFalse} in (fn th => th COMP th2, fn th => th COMP th1) end; val (PFalse, PFalse') = let val PFalse_eq = nth @{thms simp_thms} 13 in (PFalse_eq RS iffD1, PFalse_eq RS iffD2) end; (* Type for recording history, i.e. how a polynomial was obtained. *) datatype history = Start of int | Mmul of (Rat.rat * int list) * history | Add of history * history; (* Monomial ordering. *) fun morder_lt m1 m2= let fun lexorder l1 l2 = case (l1,l2) of ([],[]) => false | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2 | _ => error "morder: inconsistent monomial lengths" val n1 = Integer.sum m1 val n2 = Integer.sum m2 in n1 < n2 orelse n1 = n2 andalso lexorder m1 m2 end; (* Arithmetic on canonical polynomials. *) fun grob_neg l = map (fn (c,m) => (Rat.neg c,m)) l; fun grob_add l1 l2 = case (l1,l2) of ([],l2) => l2 | (l1,[]) => l1 | ((c1,m1)::o1,(c2,m2)::o2) => if m1 = m2 then let val c = c1 + c2 val rest = grob_add o1 o2 in if c = @0 then rest else (c,m1)::rest end else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2) else (c2,m2)::(grob_add l1 o2); fun grob_sub l1 l2 = grob_add l1 (grob_neg l2); fun grob_mmul (c1,m1) (c2,m2) = (c1 * c2, ListPair.map (op +) (m1, m2)); fun grob_cmul cm pol = map (grob_mmul cm) pol; fun grob_mul l1 l2 = case l1 of [] => [] | (h1::t1) => grob_add (grob_cmul h1 l2) (grob_mul t1 l2); fun grob_inv l = case l of [(c,vs)] => if (forall (fn x => x = 0) vs) then if c = @0 then error "grob_inv: division by zero" else [(@1 / c,vs)] else error "grob_inv: non-constant divisor polynomial" | _ => error "grob_inv: non-constant divisor polynomial"; fun grob_div l1 l2 = case l2 of [(c,l)] => if (forall (fn x => x = 0) l) then if c = @0 then error "grob_div: division by zero" else grob_cmul (@1 / c,l) l1 else error "grob_div: non-constant divisor polynomial" | _ => error "grob_div: non-constant divisor polynomial"; fun grob_pow vars l n = if n < 0 then error "grob_pow: negative power" else if n = 0 then [(@1,map (K 0) vars)] else grob_mul l (grob_pow vars l (n - 1)); (* Monomial division operation. *) fun mdiv (c1,m1) (c2,m2) = (c1 / c2, map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2); (* Lowest common multiple of two monomials. *) fun mlcm (_,m1) (_,m2) = (@1, ListPair.map Int.max (m1, m2)); (* Reduce monomial cm by polynomial pol, returning replacement for cm. *) fun reduce1 cm (pol,hpol) = case pol of [] => error "reduce1" | cm1::cms => ((let val (c,m) = mdiv cm cm1 in (grob_cmul (~ c, m) cms, Mmul ((~ c,m),hpol)) end) handle ERROR _ => error "reduce1"); (* Try this for all polynomials in a basis. *) fun tryfind f l = case l of [] => error "tryfind" | (h::t) => ((f h) handle ERROR _ => tryfind f t); fun reduceb cm basis = tryfind (fn p => reduce1 cm p) basis; (* Reduction of a polynomial (always picking largest monomial possible). *) fun reduce basis (pol,hist) = case pol of [] => (pol,hist) | cm::ptl => ((let val (q,hnew) = reduceb cm basis in reduce basis (grob_add q ptl,Add(hnew,hist)) end) handle (ERROR _) => (let val (q,hist') = reduce basis (ptl,hist) in (cm::q,hist') end)); (* Check for orthogonality w.r.t. LCM. *) fun orthogonal l p1 p2 = snd l = snd(grob_mmul (hd p1) (hd p2)); (* Compute S-polynomial of two polynomials. *) fun spoly cm ph1 ph2 = case (ph1,ph2) of (([],h),_) => ([],h) | (_,([],h)) => ([],h) | ((cm1::ptl1,his1),(cm2::ptl2,his2)) => (grob_sub (grob_cmul (mdiv cm cm1) ptl1) (grob_cmul (mdiv cm cm2) ptl2), Add(Mmul(mdiv cm cm1,his1), Mmul(mdiv (~ (fst cm),snd cm) cm2,his2))); (* Make a polynomial monic. *) fun monic (pol,hist) = if null pol then (pol,hist) else let val (c',m') = hd pol in (map (fn (c,m) => (c / c',m)) pol, Mmul((@1 / c',map (K 0) m'),hist)) end; (* The most popular heuristic is to order critical pairs by LCM monomial. *) fun forder ((_,m1),_) ((_,m2),_) = morder_lt m1 m2; fun poly_lt p q = case (p,q) of (_,[]) => false | ([],_) => true | ((c1,m1)::o1,(c2,m2)::o2) => c1 < c2 orelse c1 = c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2); fun align ((p,hp),(q,hq)) = if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp)); fun poly_eq p1 p2 = eq_list (fn ((c1, m1), (c2, m2)) => c1 = c2 andalso (m1: int list) = m2) (p1, p2); fun memx ((p1,_),(p2,_)) ppairs = not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs); (* Buchberger's second criterion. *) fun criterion2 basis (lcm,((p1,h1),(p2,h2))) opairs = exists (fn g => not(poly_eq (fst g) p1) andalso not(poly_eq (fst g) p2) andalso can (mdiv lcm) (hd(fst g)) andalso not(memx (align (g,(p1,h1))) (map snd opairs)) andalso not(memx (align (g,(p2,h2))) (map snd opairs))) basis; (* Test for hitting constant polynomial. *) fun constant_poly p = length p = 1 andalso forall (fn x => x = 0) (snd(hd p)); (* Grobner basis algorithm. *) (* FIXME: try to get rid of mergesort? *) fun merge ord l1 l2 = case l1 of [] => l2 | h1::t1 => case l2 of [] => l1 | h2::t2 => if ord h1 h2 then h1::(merge ord t1 l2) else h2::(merge ord l1 t2); fun mergesort ord l = let fun mergepairs l1 l2 = case (l1,l2) of ([s],[]) => s | (l,[]) => mergepairs [] l | (l,[s1]) => mergepairs (s1::l) [] | (l,(s1::s2::ss)) => mergepairs ((merge ord s1 s2)::l) ss in if null l then [] else mergepairs [] (map (fn x => [x]) l) end; fun grobner_basis basis pairs = case pairs of [] => basis | (l,(p1,p2))::opairs => let val (sph as (sp,_)) = monic (reduce basis (spoly l p1 p2)) in if null sp orelse criterion2 basis (l,(p1,p2)) opairs then grobner_basis basis opairs else if constant_poly sp then grobner_basis (sph::basis) [] else let val rawcps = map (fn p => (mlcm (hd(fst p)) (hd sp),align(p,sph))) basis val newcps = filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) rawcps in grobner_basis (sph::basis) (merge forder opairs (mergesort forder newcps)) end end; (* Interreduce initial polynomials. *) fun grobner_interreduce rpols ipols = case ipols of [] => map monic (rev rpols) | p::ps => let val p' = reduce (rpols @ ps) p in if null (fst p') then grobner_interreduce rpols ps else grobner_interreduce (p'::rpols) ps end; (* Overall function. *) fun grobner pols = let val npols = map_index (fn (n, p) => (p, Start n)) pols val phists = filter (fn (p,_) => not (null p)) npols val bas = grobner_interreduce [] (map monic phists) val prs0 = map_product pair bas bas val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0 val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1 val prs3 = filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) prs2 in grobner_basis bas (mergesort forder prs3) end; (* Get proof of contradiction from Grobner basis. *) fun find p l = case l of [] => error "find" | (h::t) => if p(h) then h else find p t; fun grobner_refute pols = let val gb = grobner pols in snd(find (fn (p,_) => length p = 1 andalso forall (fn x=> x=0) (snd(hd p))) gb) end; (* Turn proof into a certificate as sum of multipliers. *) (* In principle this is very inefficient: in a heavily shared proof it may *) (* make the same calculation many times. Could put in a cache or something. *) fun resolve_proof vars prf = case prf of Start(~1) => [] | Start m => [(m,[(@1,map (K 0) vars)])] | Mmul(pol,lin) => let val lis = resolve_proof vars lin in map (fn (n,p) => (n,grob_cmul pol p)) lis end | Add(lin1,lin2) => let val lis1 = resolve_proof vars lin1 val lis2 = resolve_proof vars lin2 val dom = distinct (op =) (union (op =) (map fst lis1) (map fst lis2)) in map (fn n => let val a = these (AList.lookup (op =) lis1 n) val b = these (AList.lookup (op =) lis2 n) in (n,grob_add a b) end) dom end; (* Run the procedure and produce Weak Nullstellensatz certificate. *) fun grobner_weak vars pols = let val cert = resolve_proof vars (grobner_refute pols) val l = fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert @1 in (l,map (fn (i,p) => (i,map (fn (d,m) => (l * d,m)) p)) cert) end; (* Prove a polynomial is in ideal generated by others, using Grobner basis. *) fun grobner_ideal vars pols pol = let val (pol',h) = reduce (grobner pols) (grob_neg pol,Start(~1)) in if not (null pol') then error "grobner_ideal: not in the ideal" else resolve_proof vars h end; (* Produce Strong Nullstellensatz certificate for a power of pol. *) fun grobner_strong vars pols pol = let val vars' = \<^cterm>\True\::vars val grob_z = [(@1, 1::(map (K 0) vars))] val grob_1 = [(@1, (map (K 0) vars'))] fun augment p= map (fn (c,m) => (c,0::m)) p val pols' = map augment pols val pol' = augment pol val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols' val (l,cert) = grobner_weak vars' allpols val d = fold (fold (Integer.max o hd o snd) o snd) cert 0 fun transform_monomial (c,m) = grob_cmul (c,tl m) (grob_pow vars pol (d - hd m)) fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q [] val cert' = map (fn (c,q) => (c-1,transform_polynomial q)) (filter (fn (k,_) => k <> 0) cert) in (d,l,cert') end; (* Overall parametrized universal procedure for (semi)rings. *) (* We return an ideal_conv and the actual ring prover. *) fun refute_disj rfn tm = case Thm.term_of tm of Const(\<^const_name>\HOL.disj\,_)$_$_ => Drule.compose (refute_disj rfn (Thm.dest_arg tm), 2, Drule.compose (refute_disj rfn (Thm.dest_arg1 tm), 2, disjE)) | _ => rfn tm ; val notnotD = @{thm notnotD}; fun mk_binop ct x y = Thm.apply (Thm.apply ct x) y fun is_neg t = case Thm.term_of t of (Const(\<^const_name>\Not\,_)$_) => true | _ => false; fun is_eq t = case Thm.term_of t of (Const(\<^const_name>\HOL.eq\,_)$_$_) => true | _ => false; fun end_itlist f l = case l of [] => error "end_itlist" | [x] => x | (h::t) => f h (end_itlist f t); val list_mk_binop = fn b => end_itlist (mk_binop b); val list_dest_binop = fn b => let fun h acc t = ((let val (l,r) = dest_binary b t in h (h acc r) l end) handle CTERM _ => (t::acc)) (* Why had I handle _ => ? *) in h [] end; val strip_exists = let fun h (acc, t) = case Thm.term_of t of Const (\<^const_name>\Ex\, _) $ Abs _ => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc)) | _ => (acc,t) in fn t => h ([],t) end; fun is_forall t = case Thm.term_of t of (Const(\<^const_name>\All\,_)$Abs(_,_,_)) => true | _ => false; val nnf_simps = @{thms nnf_simps}; fun weak_dnf_conv ctxt = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms weak_dnf_simps}); val initial_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps nnf_simps addsimps [not_all, not_ex] addsimps map (fn th => th RS sym) (@{thms ex_simps} @ @{thms all_simps})); fun initial_conv ctxt = Simplifier.rewrite (put_simpset initial_ss ctxt); val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec)); val cTrp = \<^cterm>\Trueprop\; val cConj = \<^cterm>\HOL.conj\; val (cNot,false_tm) = (\<^cterm>\Not\, \<^cterm>\False\); val assume_Trueprop = Thm.apply cTrp #> Thm.assume; val list_mk_conj = list_mk_binop cConj; val conjs = list_dest_binop cConj; val mk_neg = Thm.apply cNot; fun striplist dest = let fun h acc x = case try dest x of SOME (a,b) => h (h acc b) a | NONE => x::acc in h [] end; fun list_mk_binop b = foldr1 (fn (s,t) => Thm.apply (Thm.apply b s) t); val eq_commute = mk_meta_eq @{thm eq_commute}; fun sym_conv eq = let val (l,r) = Thm.dest_binop eq in Thm.instantiate' [SOME (Thm.ctyp_of_cterm l)] [SOME l, SOME r] eq_commute end; (* FIXME : copied from cqe.ML -- complex QE*) fun conjuncts ct = case Thm.term_of ct of \<^term>\HOL.conj\$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct)) | _ => [ct]; fun fold1 f = foldr1 (uncurry f); fun mk_conj_tab th = let fun h acc th = case Thm.prop_of th of \<^term>\Trueprop\$(\<^term>\HOL.conj\$_$_) => 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>\HOL.conj\$_$_) = true | is_conj _ = false; fun prove_conj tab cjs = case cjs of [c] => if is_conj (Thm.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_ac_rule eq = let val (l,r) = Thm.dest_equals eq val ctabl = mk_conj_tab (Thm.assume (Thm.apply \<^cterm>\Trueprop\ l)) val ctabr = mk_conj_tab (Thm.assume (Thm.apply \<^cterm>\Trueprop\ r)) fun tabl c = the (Termtab.lookup ctabl (Thm.term_of c)) fun tabr c = the (Termtab.lookup ctabr (Thm.term_of c)) val thl = prove_conj tabl (conjuncts r) |> implies_intr_hyps val thr = prove_conj tabr (conjuncts l) |> implies_intr_hyps val eqI = Thm.instantiate' [] [SOME l, SOME r] @{thm iffI} in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end; (* END FIXME.*) (* Conversion for the equivalence of existential statements where EX quantifiers are rearranged differently *) fun ext ctxt T = Thm.cterm_of ctxt (Const (\<^const_name>\Ex\, (T --> \<^typ>\bool\) --> \<^typ>\bool\)) fun mk_ex ctxt v t = Thm.apply (ext ctxt (Thm.typ_of_cterm v)) (Thm.lambda v t) fun choose v th th' = case Thm.concl_of th of \<^term>\Trueprop\ $ (Const(\<^const_name>\Ex\,_)$_) => let val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th val T = Thm.dest_ctyp0 (Thm.ctyp_of_cterm p) val th0 = Conv.fconv_rule (Thm.beta_conversion true) (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE) val pv = (Thm.rhs_of o Thm.beta_conversion true) (Thm.apply \<^cterm>\Trueprop\ (Thm.apply p v)) val th1 = Thm.forall_intr v (Thm.implies_intr pv th') in Thm.implies_elim (Thm.implies_elim th0 th) th1 end | _ => error "" (* FIXME ? *) fun simple_choose ctxt v th = choose v (Thm.assume ((Thm.apply \<^cterm>\Trueprop\ o mk_ex ctxt v) (Thm.dest_arg (hd (Thm.chyps_of th))))) th fun mkexi v th = let val p = Thm.lambda v (Thm.dest_arg (Thm.cprop_of th)) in Thm.implies_elim (Conv.fconv_rule (Thm.beta_conversion true) (Thm.instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI})) th end fun ex_eq_conv ctxt t = let val (p0,q0) = Thm.dest_binop t val (vs',P) = strip_exists p0 val (vs,_) = strip_exists q0 val th = Thm.assume (Thm.apply \<^cterm>\Trueprop\ P) val th1 = implies_intr_hyps (fold (simple_choose ctxt) vs' (fold mkexi vs th)) val th2 = implies_intr_hyps (fold (simple_choose ctxt) vs (fold mkexi vs' th)) val p = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) th1 val q = (Thm.dest_arg o Thm.dest_arg o Thm.cprop_of) th1 in Thm.implies_elim (Thm.implies_elim (Thm.instantiate' [] [SOME p, SOME q] iffI) th1) th2 |> mk_meta_eq end; fun getname v = case Thm.term_of v of Free(s,_) => s | Var ((s,_),_) => s | _ => "x" fun mk_eq s t = Thm.apply (Thm.apply \<^cterm>\(\) :: bool \ _\ s) t fun mk_exists ctxt v th = Drule.arg_cong_rule (ext ctxt (Thm.typ_of_cterm v)) (Thm.abstract_rule (getname v) v th) fun simp_ex_conv ctxt = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)}) -fun frees t = Drule.cterm_add_frees t []; -fun free_in v t = member op aconvc (frees t) v; +fun free_in v t = member op aconvc (Drule.cterm_frees_of t) v; val vsubst = let fun vsubst (t,v) tm = (Thm.rhs_of o Thm.beta_conversion false) (Thm.apply (Thm.lambda v tm) t) in fold vsubst end; (** main **) fun ring_and_ideal_conv {vars = _, semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), idom, ideal} dest_const mk_const ring_eq_conv ring_normalize_conv = let val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops; val [ring_add_tm, ring_mul_tm, ring_pow_tm] = map Thm.dest_fun2 [add_pat, mul_pat, pow_pat]; val (ring_sub_tm, ring_neg_tm) = (case r_ops of [sub_pat, neg_pat] => (Thm.dest_fun2 sub_pat, Thm.dest_fun neg_pat) |_ => (\<^cterm>\True\, \<^cterm>\True\)); val (field_div_tm, field_inv_tm) = (case f_ops of [div_pat, inv_pat] => (Thm.dest_fun2 div_pat, Thm.dest_fun inv_pat) | _ => (\<^cterm>\True\, \<^cterm>\True\)); val [idom_thm, neq_thm] = idom; val [idl_sub, idl_add0] = if length ideal = 2 then ideal else [eq_commute, eq_commute] fun ring_dest_neg t = let val (l,r) = Thm.dest_comb t in if Term.could_unify(Thm.term_of l, Thm.term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t]) end fun field_dest_inv t = let val (l,r) = Thm.dest_comb t in if Term.could_unify (Thm.term_of l, Thm.term_of field_inv_tm) then r else raise CTERM ("field_dest_inv", [t]) end val ring_dest_add = dest_binary ring_add_tm; val ring_mk_add = mk_binop ring_add_tm; val ring_dest_sub = dest_binary ring_sub_tm; val ring_dest_mul = dest_binary ring_mul_tm; val ring_mk_mul = mk_binop ring_mul_tm; val field_dest_div = dest_binary field_div_tm; val ring_dest_pow = dest_binary ring_pow_tm; val ring_mk_pow = mk_binop ring_pow_tm ; fun grobvars tm acc = if can dest_const tm then acc else if can ring_dest_neg tm then grobvars (Thm.dest_arg tm) acc else if can ring_dest_pow tm then grobvars (Thm.dest_arg1 tm) acc else if can ring_dest_add tm orelse can ring_dest_sub tm orelse can ring_dest_mul tm then grobvars (Thm.dest_arg1 tm) (grobvars (Thm.dest_arg tm) acc) else if can field_dest_inv tm then let val gvs = grobvars (Thm.dest_arg tm) [] in if null gvs then acc else tm::acc end else if can field_dest_div tm then let val lvs = grobvars (Thm.dest_arg1 tm) acc val gvs = grobvars (Thm.dest_arg tm) [] in if null gvs then lvs else tm::acc end else tm::acc ; fun grobify_term vars tm = ((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else [(@1, map (fn i => if i aconvc tm then 1 else 0) vars)]) handle CTERM _ => ((let val x = dest_const tm in if x = @0 then [] else [(x,map (K 0) vars)] end) handle ERROR _ => ((grob_neg(grobify_term vars (ring_dest_neg tm))) handle CTERM _ => ( (grob_inv(grobify_term vars (field_dest_inv tm))) handle CTERM _ => ((let val (l,r) = ring_dest_add tm in grob_add (grobify_term vars l) (grobify_term vars r) end) handle CTERM _ => ((let val (l,r) = ring_dest_sub tm in grob_sub (grobify_term vars l) (grobify_term vars r) end) handle CTERM _ => ((let val (l,r) = ring_dest_mul tm in grob_mul (grobify_term vars l) (grobify_term vars r) end) handle CTERM _ => ( (let val (l,r) = field_dest_div tm in grob_div (grobify_term vars l) (grobify_term vars r) end) handle CTERM _ => ((let val (l,r) = ring_dest_pow tm in grob_pow vars (grobify_term vars l) ((Thm.term_of #> HOLogic.dest_number #> snd) r) end) handle CTERM _ => error "grobify_term: unknown or invalid term"))))))))); val eq_tm = idom_thm |> concl |> Thm.dest_arg |> Thm.dest_arg |> Thm.dest_fun2; val dest_eq = dest_binary eq_tm; fun grobify_equation vars tm = let val (l,r) = dest_binary eq_tm tm in grob_sub (grobify_term vars l) (grobify_term vars r) end; fun grobify_equations tm = let val cjs = conjs tm val rawvars = fold_rev (fn eq => fn a => grobvars (Thm.dest_arg1 eq) (grobvars (Thm.dest_arg eq) a)) cjs [] val vars = sort Thm.term_ord (distinct (op aconvc) rawvars) in (vars,map (grobify_equation vars) cjs) end; val holify_polynomial = let fun holify_varpow (v,n) = if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber \<^ctyp>\nat\ n) (* FIXME *) fun holify_monomial vars (c,m) = let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m)) in end_itlist ring_mk_mul (mk_const c :: xps) end fun holify_polynomial vars p = if null p then mk_const @0 else end_itlist ring_mk_add (map (holify_monomial vars) p) in holify_polynomial end ; fun idom_rule ctxt = simplify (put_simpset HOL_basic_ss ctxt addsimps [idom_thm]); fun prove_nz n = eqF_elim (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const @0))); val neq_01 = prove_nz @1; fun neq_rule n th = [prove_nz n, th] MRS neq_thm; fun mk_add th1 = Thm.combination (Drule.arg_cong_rule ring_add_tm th1); fun refute ctxt tm = if tm aconvc false_tm then assume_Trueprop tm else ((let val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims ctxt (assume_Trueprop tm)) val nths = filter (is_eq o Thm.dest_arg o concl) nths0 val eths = filter (is_eq o concl) eths0 in if null eths then let val th1 = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths val th2 = Conv.fconv_rule ((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1 val conc = th2 |> concl |> Thm.dest_arg val (l,_) = conc |> dest_eq in Thm.implies_intr (Thm.apply cTrp tm) (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2)) (HOLogic.mk_obj_eq (Thm.reflexive l))) end else let val (vars,l,cert,noteqth) =( if null nths then let val (vars,pols) = grobify_equations(list_mk_conj(map concl eths)) val (l,cert) = grobner_weak vars pols in (vars,l,cert,neq_01) end else let val nth = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths val (vars,pol::pols) = grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths)) val (deg,l,cert) = grobner_strong vars pols pol val th1 = Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) nth val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01 in (vars,l,cert,th2) end) val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > @0) p)) cert val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (~ c,m)) (filter (fn (c,_) => c < @0) p))) cert val herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos val herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg fun thm_fn pols = if null pols then Thm.reflexive(mk_const @0) else end_itlist mk_add (map (fn (i,p) => Drule.arg_cong_rule (Thm.apply ring_mul_tm p) (nth eths i |> mk_meta_eq)) pols) val th1 = thm_fn herts_pos val th2 = thm_fn herts_neg val th3 = HOLogic.conj_intr ctxt (HOLogic.mk_obj_eq (mk_add (Thm.symmetric th1) th2)) noteqth val th4 = Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv) (neq_rule l th3) val (l, _) = dest_eq(Thm.dest_arg(concl th4)) in Thm.implies_intr (Thm.apply cTrp tm) (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4)) (HOLogic.mk_obj_eq (Thm.reflexive l))) end end) handle ERROR _ => raise CTERM ("Groebner-refute: unable to refute",[tm])) fun ring ctxt tm = let fun mk_forall x p = let val T = Thm.typ_of_cterm x; val all = Thm.cterm_of ctxt (Const (\<^const_name>\All\, (T --> \<^typ>\bool\) --> \<^typ>\bool\)) in Thm.apply all (Thm.lambda x p) end - val avs = Drule.cterm_add_frees tm [] + val avs = Drule.cterm_frees_of tm val P' = fold mk_forall avs tm val th1 = initial_conv ctxt (mk_neg P') val (evs,bod) = strip_exists(concl th1) in if is_forall bod then raise CTERM("ring: non-universal formula",[tm]) else let val th1a = weak_dnf_conv ctxt bod val boda = concl th1a val th2a = refute_disj (refute ctxt) boda val th2b = [HOLogic.mk_obj_eq th1a, (th2a COMP notI) COMP PFalse'] MRS trans val th2 = fold (fn v => fn th => (Thm.forall_intr v th) COMP allI) evs (th2b RS PFalse) val th3 = Thm.equal_elim (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [not_ex RS sym]) (th2 |> Thm.cprop_of)) th2 in specl avs ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD) end end fun ideal tms tm ord = let val rawvars = fold_rev grobvars (tm::tms) [] val vars = sort ord (distinct (fn (x,y) => (Thm.term_of x) aconv (Thm.term_of y)) rawvars) val pols = map (grobify_term vars) tms val pol = grobify_term vars tm val cert = grobner_ideal vars pols pol in map_range (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars) (length pols) end fun poly_eq_conv t = let val (a,b) = Thm.dest_binop t in Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv ring_normalize_conv)) (Thm.instantiate' [] [SOME a, SOME b] idl_sub) end val poly_eq_simproc = let fun proc ct = let val th = poly_eq_conv ct in if Thm.is_reflexive th then NONE else SOME th end in Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc" {lhss = [Thm.term_of (Thm.lhs_of idl_sub)], proc = fn _ => fn _ => proc} end; val poly_eq_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms} addsimprocs [poly_eq_simproc]) local fun is_defined v t = let val mons = striplist(dest_binary ring_add_tm) t in member (op aconvc) mons v andalso forall (fn m => v aconvc m - orelse not(member (op aconvc) (Drule.cterm_add_frees m []) v)) mons + orelse not(member (op aconvc) (Drule.cterm_frees_of m) v)) mons end fun isolate_variable vars tm = let val th = poly_eq_conv tm val th' = (sym_conv then_conv poly_eq_conv) tm val (v,th1) = case find_first(fn v=> is_defined v (Thm.dest_arg1 (Thm.rhs_of th))) vars of SOME v => (v,th') | NONE => (the (find_first (fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th) val th2 = Thm.transitive th1 (Thm.instantiate' [] [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v] idl_add0) in Conv.fconv_rule(funpow 2 Conv.arg_conv ring_normalize_conv) th2 end in fun unwind_polys_conv ctxt tm = let val (vars,bod) = strip_exists tm val cjs = striplist (dest_binary \<^cterm>\HOL.conj\) bod val th1 = (the (get_first (try (isolate_variable vars)) cjs) handle Option.Option => raise CTERM ("unwind_polys_conv",[tm])) val eq = Thm.lhs_of th1 val bod' = list_mk_binop \<^cterm>\HOL.conj\ (eq::(remove (op aconvc) eq cjs)) val th2 = conj_ac_rule (mk_eq bod bod') val th3 = Thm.transitive th2 (Drule.binop_cong_rule \<^cterm>\HOL.conj\ th1 (Thm.reflexive (Thm.dest_arg (Thm.rhs_of th2)))) val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3)) val th4 = Conv.fconv_rule (Conv.arg_conv (simp_ex_conv ctxt)) (mk_exists ctxt v th3) val th5 = ex_eq_conv ctxt (mk_eq tm (fold (mk_ex ctxt) (remove op aconvc v vars) (Thm.lhs_of th4))) in Thm.transitive th5 (fold (mk_exists ctxt) (remove op aconvc v vars) th4) end; end local fun scrub_var v m = let val ps = striplist ring_dest_mul m val ps' = remove op aconvc v ps in if null ps' then one_tm else fold1 ring_mk_mul ps' end fun find_multipliers v mons = let val mons1 = filter (fn m => free_in v m) mons val mons2 = map (scrub_var v) mons1 in if null mons2 then zero_tm else fold1 ring_mk_add mons2 end fun isolate_monomials vars tm = let val (cmons,vmons) = - List.partition (fn m => null (inter (op aconvc) vars (frees m))) + List.partition (fn m => null (inter (op aconvc) vars (Drule.cterm_frees_of m))) (striplist ring_dest_add tm) val cofactors = map (fn v => find_multipliers v vmons) vars val cnc = if null cmons then zero_tm else Thm.apply ring_neg_tm (list_mk_binop ring_add_tm cmons) in (cofactors,cnc) end; fun isolate_variables evs ps eq = let val vars = filter (fn v => free_in v eq) evs val (qs,p) = isolate_monomials vars eq val rs = ideal (qs @ ps) p Thm.term_ord in (eq, take (length qs) rs ~~ vars) end; fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p)); in fun solve_idealism evs ps eqs = if null evs then [] else let val (eq,cfs) = get_first (try (isolate_variables evs ps)) eqs |> the val evs' = subtract op aconvc evs (map snd cfs) val eqs' = map (subst_in_poly cfs) (remove op aconvc eq eqs) in cfs @ solve_idealism evs' ps eqs' end; end; in {ring_conv = ring, simple_ideal = ideal, multi_ideal = solve_idealism, poly_eq_ss = poly_eq_ss, unwind_conv = unwind_polys_conv} end; fun find_term bounds tm = (case Thm.term_of tm of Const (\<^const_name>\HOL.eq\, T) $ _ $ _ => if domain_type T = HOLogic.boolT then find_args bounds tm else Thm.dest_arg tm | Const (\<^const_name>\Not\, _) $ _ => find_term bounds (Thm.dest_arg tm) | Const (\<^const_name>\All\, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (\<^const_name>\Ex\, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (\<^const_name>\HOL.conj\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\HOL.disj\, _) $ _ $ _ => find_args bounds tm | Const (\<^const_name>\HOL.implies\, _) $ _ $ _ => find_args bounds tm | \<^term>\Pure.imp\ $_$_ => find_args bounds tm | Const("(==)",_)$_$_ => find_args bounds tm (* FIXME proper const name *) | \<^term>\Trueprop\$_ => find_term bounds (Thm.dest_arg tm) | _ => raise TERM ("find_term", [])) and find_args bounds tm = let val (t, u) = Thm.dest_binop tm in (find_term bounds t handle TERM _ => find_term bounds u) end and find_body bounds b = let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b in find_term (bounds + 1) b' end; fun get_ring_ideal_convs ctxt form = case try (find_term 0) form of NONE => NONE | SOME tm => (case Semiring_Normalizer.match ctxt tm of NONE => NONE | SOME (res as (theory, {is_const = _, dest_const, mk_const, conv = ring_eq_conv})) => SOME (ring_and_ideal_conv theory dest_const (mk_const (Thm.ctyp_of_cterm tm)) (ring_eq_conv ctxt) (Semiring_Normalizer.semiring_normalize_wrapper ctxt res))) fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (Named_Theorems.get ctxt \<^named_theorems>\algebra\) delsimps del_thms addsimps add_thms); fun ring_tac add_ths del_ths ctxt = Object_Logic.full_atomize_tac ctxt THEN' presimplify ctxt add_ths del_ths THEN' CSUBGOAL (fn (p, i) => resolve_tac ctxt [let val form = Object_Logic.dest_judgment ctxt p in case get_ring_ideal_convs ctxt form of NONE => Thm.reflexive form | SOME thy => #ring_conv thy ctxt form end] i handle TERM _ => no_tac | CTERM _ => no_tac | THM _ => no_tac); local fun lhs t = case Thm.term_of t of Const(\<^const_name>\HOL.eq\,_)$_$_ => Thm.dest_arg1 t | _=> raise CTERM ("ideal_tac - lhs",[t]) fun exitac _ NONE = no_tac | exitac ctxt (SOME y) = resolve_tac ctxt [Thm.instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1 val claset = claset_of \<^context> in fun ideal_tac add_ths del_ths ctxt = presimplify ctxt add_ths del_ths THEN' CSUBGOAL (fn (p, i) => case get_ring_ideal_convs ctxt p of NONE => no_tac | SOME thy => let fun poly_exists_tac {asms = asms, concl = concl, prems = prems, params = _, context = ctxt, schematics = _} = let val (evs,bod) = strip_exists (Thm.dest_arg concl) val ps = map_filter (try (lhs o Thm.dest_arg)) asms val cfs = (map swap o #multi_ideal thy evs ps) (map Thm.dest_arg1 (conjuncts bod)) val ws = map (exitac ctxt o AList.lookup op aconvc cfs) evs in EVERY (rev ws) THEN Method.insert_tac ctxt prems 1 THEN ring_tac add_ths del_ths ctxt 1 end in clarify_tac (put_claset claset ctxt) i THEN Object_Logic.full_atomize_tac ctxt i THEN asm_full_simp_tac (put_simpset (#poly_eq_ss thy) ctxt) i THEN clarify_tac (put_claset claset ctxt) i THEN (REPEAT (CONVERSION (#unwind_conv thy ctxt) i)) THEN SUBPROOF poly_exists_tac ctxt i end handle TERM _ => no_tac | CTERM _ => no_tac | THM _ => no_tac); end; fun algebra_tac add_ths del_ths ctxt i = ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i end; diff --git a/src/Pure/drule.ML b/src/Pure/drule.ML --- a/src/Pure/drule.ML +++ b/src/Pure/drule.ML @@ -1,840 +1,840 @@ (* Title: Pure/drule.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Derived rules and other operations on theorems. *) infix 0 RL RLN MRS OF COMP INCR_COMP COMP_INCR; signature BASIC_DRULE = sig val mk_implies: cterm * cterm -> cterm val list_implies: cterm list * cterm -> cterm val strip_imp_prems: cterm -> cterm list val strip_imp_concl: cterm -> cterm val cprems_of: thm -> cterm list val forall_intr_list: cterm list -> thm -> thm val forall_intr_vars: thm -> thm val forall_elim_list: cterm list -> thm -> thm val lift_all: Proof.context -> cterm -> thm -> thm val implies_elim_list: thm -> thm list -> thm val implies_intr_list: cterm list -> thm -> thm val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm val instantiate'_normalize: ctyp option list -> cterm option list -> thm -> thm val infer_instantiate_types: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm val infer_instantiate': Proof.context -> cterm option list -> thm -> thm val zero_var_indexes_list: thm list -> thm list val zero_var_indexes: thm -> thm val implies_intr_hyps: thm -> thm val rotate_prems: int -> thm -> thm val rearrange_prems: int list -> thm -> thm val RLN: thm list * (int * thm list) -> thm list val RL: thm list * thm list -> thm list val MRS: thm list * thm -> thm val OF: thm * thm list -> thm val COMP: thm * thm -> thm val INCR_COMP: thm * thm -> thm val COMP_INCR: thm * thm -> thm val size_of_thm: thm -> int val reflexive_thm: thm val symmetric_thm: thm val transitive_thm: thm val extensional: thm -> thm val asm_rl: thm val cut_rl: thm val revcut_rl: thm val thin_rl: thm end; signature DRULE = sig include BASIC_DRULE val outer_params: term -> (string * typ) list val generalize: Symtab.set * Symtab.set -> thm -> thm val list_comb: cterm * cterm list -> cterm val strip_comb: cterm -> cterm * cterm list val beta_conv: cterm -> cterm -> cterm val flexflex_unique: Proof.context option -> thm -> thm val export_without_context: thm -> thm val export_without_context_open: thm -> thm val store_thm: binding -> thm -> thm val store_standard_thm: binding -> thm -> thm val store_thm_open: binding -> thm -> thm val store_standard_thm_open: binding -> thm -> thm val multi_resolve: Proof.context option -> thm list -> thm -> thm Seq.seq val multi_resolves: Proof.context option -> thm list -> thm list -> thm Seq.seq val compose: thm * int * thm -> thm val equals_cong: thm val imp_cong: thm val swap_prems_eq: thm val imp_cong_rule: thm -> thm -> thm val arg_cong_rule: cterm -> thm -> thm val binop_cong_rule: cterm -> thm -> thm -> thm val fun_cong_rule: thm -> cterm -> thm val beta_eta_conversion: cterm -> thm val eta_contraction_rule: thm -> thm val norm_hhf_eq: thm val norm_hhf_eqs: thm list val is_norm_hhf: term -> bool val norm_hhf: theory -> term -> term val norm_hhf_cterm: Proof.context -> cterm -> cterm val protect: cterm -> cterm val protectI: thm val protectD: thm val protect_cong: thm val implies_intr_protected: cterm list -> thm -> thm val termI: thm val mk_term: cterm -> thm val dest_term: thm -> cterm val cterm_rule: (thm -> thm) -> cterm -> cterm - val cterm_add_frees: cterm -> cterm list -> cterm list + val cterm_frees_of: cterm -> cterm list val dummy_thm: thm val free_dummy_thm: thm val is_sort_constraint: term -> bool val sort_constraintI: thm val sort_constraint_eq: thm val with_subgoal: int -> (thm -> thm) -> thm -> thm val comp_no_flatten: thm * int -> int -> thm -> thm val rename_bvars: (string * string) list -> thm -> thm val rename_bvars': string option list -> thm -> thm val incr_indexes: thm -> thm -> thm val incr_indexes2: thm -> thm -> thm -> thm val triv_forall_equality: thm val distinct_prems_rl: thm val equal_intr_rule: thm val equal_elim_rule1: thm val equal_elim_rule2: thm val remdups_rl: thm val abs_def: thm -> thm end; structure Drule: DRULE = struct (** some cterm->cterm operations: faster than calling cterm_of! **) (* A1\...An\B goes to [A1,...,An], where B is not an implication *) fun strip_imp_prems ct = let val (cA, cB) = Thm.dest_implies ct in cA :: strip_imp_prems cB end handle TERM _ => []; (* A1\...An\B goes to B, where B is not an implication *) fun strip_imp_concl ct = (case Thm.term_of ct of Const ("Pure.imp", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct) | _ => ct); (*The premises of a theorem, as a cterm list*) val cprems_of = strip_imp_prems o Thm.cprop_of; fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t; val implies = certify Logic.implies; fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B; (*cterm version of list_implies: [A1,...,An], B goes to \A1;...;An\\B *) fun list_implies([], B) = B | list_implies(A::As, B) = mk_implies (A, list_implies(As,B)); (*cterm version of list_comb: maps (f, [t1,...,tn]) to f(t1,...,tn) *) fun list_comb (f, []) = f | list_comb (f, t::ts) = list_comb (Thm.apply f t, ts); (*cterm version of strip_comb: maps f(t1,...,tn) to (f, [t1,...,tn]) *) fun strip_comb ct = let fun stripc (p as (ct, cts)) = let val (ct1, ct2) = Thm.dest_comb ct in stripc (ct1, ct2 :: cts) end handle CTERM _ => p in stripc (ct, []) end; (*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs of the meta-equality returned by the beta_conversion rule.*) fun beta_conv x y = Thm.dest_arg (Thm.cprop_of (Thm.beta_conversion false (Thm.apply x y))); (** Standardization of rules **) (*Generalization over a list of variables*) val forall_intr_list = fold_rev Thm.forall_intr; (*Generalization over Vars -- canonical order*) fun forall_intr_vars th = fold Thm.forall_intr (Thm.add_vars th []) th; fun outer_params t = let val vs = Term.strip_all_vars t in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end; (*lift vars wrt. outermost goal parameters -- reverses the effect of gen_all modulo higher-order unification*) fun lift_all ctxt raw_goal raw_th = let val thy = Proof_Context.theory_of ctxt; val goal = Thm.transfer_cterm thy raw_goal; val th = Thm.transfer thy raw_th; val maxidx = Thm.maxidx_of th; val ps = outer_params (Thm.term_of goal) |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T)); val Ts = map Term.fastype_of ps; val inst = Term_Subst.Vars.build (th |> (Thm.fold_terms o Term.fold_aterms) (fn t => fn inst => (case t of Var (xi, T) => if Term_Subst.Vars.defined inst (xi, T) then inst else let val ct = Thm.cterm_of ctxt (Term.list_comb (Var (xi, Ts ---> T), ps)) in Term_Subst.Vars.update ((xi, T), ct) inst end | _ => inst))); in th |> Thm.instantiate ([], Term_Subst.Vars.dest inst) |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps end; (*direct generalization*) fun generalize names th = Thm.generalize names (Thm.maxidx_of th + 1) th; (*specialization over a list of cterms*) val forall_elim_list = fold Thm.forall_elim; (*maps A1,...,An |- B to \A1;...;An\ \ B*) val implies_intr_list = fold_rev Thm.implies_intr; (*maps \A1;...;An\ \ B and [A1,...,An] to B*) fun implies_elim_list impth ths = fold Thm.elim_implies ths impth; (*Reset Var indexes to zero, renaming to preserve distinctness*) fun zero_var_indexes_list [] = [] | zero_var_indexes_list ths = let val (instT, inst) = Term_Subst.zero_var_indexes_inst Name.context (map Thm.full_prop_of ths); val tvars = fold Thm.add_tvars ths []; fun the_tvar v = the (find_first (fn cT => v = dest_TVar (Thm.typ_of cT)) tvars); val instT' = build (instT |> Term_Subst.TVars.fold (fn (v, TVar (b, _)) => cons (v, Thm.rename_tvar b (the_tvar v)))); val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths []; fun the_var v = the (find_first (fn ct => v = dest_Var (Thm.term_of ct)) vars); val inst' = build (inst |> Term_Subst.Vars.fold (fn (v, Var (b, _)) => cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v))))); in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (instT', inst')) ths end; val zero_var_indexes = singleton zero_var_indexes_list; (** Standard form of object-rule: no hypotheses, flexflex constraints, Frees, or outer quantifiers; all generality expressed by Vars of index 0.**) (*Discharge all hypotheses.*) fun implies_intr_hyps th = fold Thm.implies_intr (Thm.chyps_of th) th; (*Squash a theorem's flexflex constraints provided it can be done uniquely. This step can lose information.*) fun flexflex_unique opt_ctxt th = if null (Thm.tpairs_of th) then th else (case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule opt_ctxt th)) of [th] => th | [] => raise THM ("flexflex_unique: impossible constraints", 0, [th]) | _ => raise THM ("flexflex_unique: multiple unifiers", 0, [th])); (* old-style export without context *) val export_without_context_open = implies_intr_hyps #> Thm.forall_intr_frees #> `Thm.maxidx_of #-> (fn maxidx => Thm.forall_elim_vars (maxidx + 1) #> Thm.strip_shyps #> zero_var_indexes #> Thm.varifyT_global); val export_without_context = flexflex_unique NONE #> export_without_context_open #> Thm.close_derivation \<^here>; (*Rotates a rule's premises to the left by k*) fun rotate_prems 0 = I | rotate_prems k = Thm.permute_prems 0 k; fun with_subgoal i f = rotate_prems (i - 1) #> f #> rotate_prems (1 - i); (*Permute prems, where the i-th position in the argument list (counting from 0) gives the position within the original thm to be transferred to position i. Any remaining trailing positions are left unchanged.*) val rearrange_prems = let fun rearr new [] thm = thm | rearr new (p :: ps) thm = rearr (new + 1) (map (fn q => if new <= q andalso q < p then q + 1 else q) ps) (Thm.permute_prems (new + 1) (new - p) (Thm.permute_prems new (p - new) thm)) in rearr 0 end; (*Resolution: multiple arguments, multiple results*) local fun res opt_ctxt th i rule = (Thm.biresolution opt_ctxt false [(false, th)] i rule handle THM _ => Seq.empty) |> Seq.map Thm.solve_constraints; fun multi_res _ _ [] rule = Seq.single rule | multi_res opt_ctxt i (th :: ths) rule = Seq.maps (res opt_ctxt th i) (multi_res opt_ctxt (i + 1) ths rule); in fun multi_resolve opt_ctxt = multi_res opt_ctxt 1; fun multi_resolves opt_ctxt facts rules = Seq.maps (multi_resolve opt_ctxt facts) (Seq.of_list rules); end; (*For joining lists of rules*) fun thas RLN (i, thbs) = let val resolve = Thm.biresolution NONE false (map (pair false) thas) i fun resb thb = Seq.list_of (resolve thb) handle THM _ => [] in maps resb thbs |> map Thm.solve_constraints end; fun thas RL thbs = thas RLN (1, thbs); (*Isar-style multi-resolution*) fun bottom_rl OF rls = (case Seq.chop 2 (multi_resolve NONE rls bottom_rl) of ([th], _) => Thm.solve_constraints th | ([], _) => raise THM ("OF: no unifiers", 0, bottom_rl :: rls) | _ => raise THM ("OF: multiple unifiers", 0, bottom_rl :: rls)); (*Resolve a list of rules against bottom_rl from right to left; makes proof trees*) fun rls MRS bottom_rl = bottom_rl OF rls; (*compose Q and \...,Qi,Q(i+1),...\ \ R to \...,Q(i+1),...\ \ R with no lifting or renaming! Q may contain \ or meta-quantifiers ALWAYS deletes premise i *) fun compose (tha, i, thb) = Thm.bicompose NONE {flatten = true, match = false, incremented = false} (false, tha, 0) i thb |> Seq.list_of |> distinct Thm.eq_thm |> (fn [th] => Thm.solve_constraints th | _ => raise THM ("compose: unique result expected", i, [tha, thb])); (** theorem equality **) (*Useful "distance" function for BEST_FIRST*) val size_of_thm = size_of_term o Thm.full_prop_of; (*** Meta-Rewriting Rules ***) val read_prop = certify o Simple_Syntax.read_prop; fun store_thm name th = Context.>>> (Context.map_theory_result (Global_Theory.store_thm (name, th))); fun store_thm_open name th = Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th))); fun store_standard_thm name th = store_thm name (export_without_context th); fun store_standard_thm_open name th = store_thm_open name (export_without_context_open th); val reflexive_thm = let val cx = certify (Var(("x",0),TVar(("'a",0),[]))) in store_standard_thm_open (Binding.make ("reflexive", \<^here>)) (Thm.reflexive cx) end; val symmetric_thm = let val xy = read_prop "x::'a \ y::'a"; val thm = Thm.implies_intr xy (Thm.symmetric (Thm.assume xy)); in store_standard_thm_open (Binding.make ("symmetric", \<^here>)) thm end; val transitive_thm = let val xy = read_prop "x::'a \ y::'a"; val yz = read_prop "y::'a \ z::'a"; val xythm = Thm.assume xy; val yzthm = Thm.assume yz; val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm); in store_standard_thm_open (Binding.make ("transitive", \<^here>)) thm end; fun extensional eq = let val eq' = Thm.abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (Thm.cprop_of eq)))) eq in Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of eq')) eq' end; val equals_cong = store_standard_thm_open (Binding.make ("equals_cong", \<^here>)) (Thm.reflexive (read_prop "x::'a \ y::'a")); val imp_cong = let val ABC = read_prop "A \ B::prop \ C::prop" val AB = read_prop "A \ B" val AC = read_prop "A \ C" val A = read_prop "A" in store_standard_thm_open (Binding.make ("imp_cong", \<^here>)) (Thm.implies_intr ABC (Thm.equal_intr (Thm.implies_intr AB (Thm.implies_intr A (Thm.equal_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)) (Thm.implies_elim (Thm.assume AB) (Thm.assume A))))) (Thm.implies_intr AC (Thm.implies_intr A (Thm.equal_elim (Thm.symmetric (Thm.implies_elim (Thm.assume ABC) (Thm.assume A))) (Thm.implies_elim (Thm.assume AC) (Thm.assume A))))))) end; val swap_prems_eq = let val ABC = read_prop "A \ B \ C" val BAC = read_prop "B \ A \ C" val A = read_prop "A" val B = read_prop "B" in store_standard_thm_open (Binding.make ("swap_prems_eq", \<^here>)) (Thm.equal_intr (Thm.implies_intr ABC (Thm.implies_intr B (Thm.implies_intr A (Thm.implies_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)) (Thm.assume B))))) (Thm.implies_intr BAC (Thm.implies_intr A (Thm.implies_intr B (Thm.implies_elim (Thm.implies_elim (Thm.assume BAC) (Thm.assume B)) (Thm.assume A)))))) end; val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies); fun arg_cong_rule ct th = Thm.combination (Thm.reflexive ct) th; (*AP_TERM in LCF/HOL*) fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct); (*AP_THM in LCF/HOL*) fun binop_cong_rule ct th1 th2 = Thm.combination (arg_cong_rule ct th1) th2; fun beta_eta_conversion ct = let val thm = Thm.beta_conversion true ct in Thm.transitive thm (Thm.eta_conversion (Thm.rhs_of thm)) end; (*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*) fun eta_contraction_rule th = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of th)) th; (* abs_def *) (* f ?x1 ... ?xn \ u -------------------- f \ \x1 ... xn. u *) local fun contract_lhs th = Thm.transitive (Thm.symmetric (beta_eta_conversion (#1 (Thm.dest_equals (Thm.cprop_of th))))) th; fun var_args ct = (case try Thm.dest_comb ct of SOME (f, arg) => (case Thm.term_of arg of Var ((x, _), _) => update (eq_snd (op aconvc)) (x, arg) (var_args f) | _ => []) | NONE => []); in fun abs_def th = let val th' = contract_lhs th; val args = var_args (Thm.lhs_of th'); in contract_lhs (fold (uncurry Thm.abstract_rule) args th') end; end; (*** Some useful meta-theorems ***) (*The rule V/V, obtains assumption solving for eresolve_tac*) val asm_rl = store_standard_thm_open (Binding.make ("asm_rl", \<^here>)) (Thm.trivial (read_prop "?psi")); (*Meta-level cut rule: \V \ W; V\ \ W *) val cut_rl = store_standard_thm_open (Binding.make ("cut_rl", \<^here>)) (Thm.trivial (read_prop "?psi \ ?theta")); (*Generalized elim rule for one conclusion; cut_rl with reversed premises: \PROP V; PROP V \ PROP W\ \ PROP W *) val revcut_rl = let val V = read_prop "V"; val VW = read_prop "V \ W"; in store_standard_thm_open (Binding.make ("revcut_rl", \<^here>)) (Thm.implies_intr V (Thm.implies_intr VW (Thm.implies_elim (Thm.assume VW) (Thm.assume V)))) end; (*for deleting an unwanted assumption*) val thin_rl = let val V = read_prop "V"; val W = read_prop "W"; val thm = Thm.implies_intr V (Thm.implies_intr W (Thm.assume W)); in store_standard_thm_open (Binding.make ("thin_rl", \<^here>)) thm end; (* (\x. PROP ?V) \ PROP ?V Allows removal of redundant parameters*) val triv_forall_equality = let val V = read_prop "V"; val QV = read_prop "\x::'a. V"; val x = certify (Free ("x", Term.aT [])); in store_standard_thm_open (Binding.make ("triv_forall_equality", \<^here>)) (Thm.equal_intr (Thm.implies_intr QV (Thm.forall_elim x (Thm.assume QV))) (Thm.implies_intr V (Thm.forall_intr x (Thm.assume V)))) end; (* (PROP ?Phi \ PROP ?Phi \ PROP ?Psi) \ (PROP ?Phi \ PROP ?Psi) *) val distinct_prems_rl = let val AAB = read_prop "Phi \ Phi \ Psi"; val A = read_prop "Phi"; in store_standard_thm_open (Binding.make ("distinct_prems_rl", \<^here>)) (implies_intr_list [AAB, A] (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A])) end; (* \PROP ?phi \ PROP ?psi; PROP ?psi \ PROP ?phi\ \ PROP ?phi \ PROP ?psi Introduction rule for \ as a meta-theorem. *) val equal_intr_rule = let val PQ = read_prop "phi \ psi"; val QP = read_prop "psi \ phi"; in store_standard_thm_open (Binding.make ("equal_intr_rule", \<^here>)) (Thm.implies_intr PQ (Thm.implies_intr QP (Thm.equal_intr (Thm.assume PQ) (Thm.assume QP)))) end; (* PROP ?phi \ PROP ?psi \ PROP ?phi \ PROP ?psi *) val equal_elim_rule1 = let val eq = read_prop "phi::prop \ psi::prop"; val P = read_prop "phi"; in store_standard_thm_open (Binding.make ("equal_elim_rule1", \<^here>)) (Thm.equal_elim (Thm.assume eq) (Thm.assume P) |> implies_intr_list [eq, P]) end; (* PROP ?psi \ PROP ?phi \ PROP ?phi \ PROP ?psi *) val equal_elim_rule2 = store_standard_thm_open (Binding.make ("equal_elim_rule2", \<^here>)) (symmetric_thm RS equal_elim_rule1); (* PROP ?phi \ PROP ?phi \ PROP ?psi \ PROP ?psi *) val remdups_rl = let val P = read_prop "phi"; val Q = read_prop "psi"; val thm = implies_intr_list [P, P, Q] (Thm.assume Q); in store_standard_thm_open (Binding.make ("remdups_rl", \<^here>)) thm end; (** embedded terms and types **) local val A = certify (Free ("A", propT)); val axiom = Thm.unvarify_axiom (Context.the_global_context ()); val prop_def = axiom "Pure.prop_def"; val term_def = axiom "Pure.term_def"; val sort_constraint_def = axiom "Pure.sort_constraint_def"; val C = Thm.lhs_of sort_constraint_def; val T = Thm.dest_arg C; val CA = mk_implies (C, A); in (* protect *) val protect = Thm.apply (certify Logic.protectC); val protectI = store_standard_thm (Binding.concealed (Binding.make ("protectI", \<^here>))) (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)); val protectD = store_standard_thm (Binding.concealed (Binding.make ("protectD", \<^here>))) (Thm.equal_elim prop_def (Thm.assume (protect A))); val protect_cong = store_standard_thm_open (Binding.make ("protect_cong", \<^here>)) (Thm.reflexive (protect A)); fun implies_intr_protected asms th = let val asms' = map protect asms in implies_elim_list (implies_intr_list asms th) (map (fn asm' => Thm.assume asm' RS protectD) asms') |> implies_intr_list asms' end; (* term *) val termI = store_standard_thm (Binding.concealed (Binding.make ("termI", \<^here>))) (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))); fun mk_term ct = let val cT = Thm.ctyp_of_cterm ct; val T = Thm.typ_of cT; in Thm.instantiate ([((("'a", 0), []), cT)], [((("x", 0), T), ct)]) termI end; fun dest_term th = let val cprop = strip_imp_concl (Thm.cprop_of th) in if can Logic.dest_term (Thm.term_of cprop) then Thm.dest_arg cprop else raise THM ("dest_term", 0, [th]) end; fun cterm_rule f = dest_term o f o mk_term; -val cterm_add_frees = Thm.add_frees o mk_term; +val cterm_frees_of = Thm.frees_of o mk_term; val dummy_thm = mk_term (certify Term.dummy_prop); val free_dummy_thm = Thm.tag_free_dummy dummy_thm; (* sort_constraint *) fun is_sort_constraint (Const ("Pure.sort_constraint", _) $ Const ("Pure.type", _)) = true | is_sort_constraint _ = false; val sort_constraintI = store_standard_thm (Binding.concealed (Binding.make ("sort_constraintI", \<^here>))) (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T)); val sort_constraint_eq = store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", \<^here>))) (Thm.equal_intr (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI))) (implies_intr_list [A, C] (Thm.assume A))); end; (* HHF normalization *) (* (PROP ?phi \ (\x. PROP ?psi x)) \ (\x. PROP ?phi \ PROP ?psi x) *) val norm_hhf_eq = let val aT = TFree ("'a", []); val x = Free ("x", aT); val phi = Free ("phi", propT); val psi = Free ("psi", aT --> propT); val cx = certify x; val cphi = certify phi; val lhs = certify (Logic.mk_implies (phi, Logic.all x (psi $ x))); val rhs = certify (Logic.all x (Logic.mk_implies (phi, psi $ x))); in Thm.equal_intr (Thm.implies_elim (Thm.assume lhs) (Thm.assume cphi) |> Thm.forall_elim cx |> Thm.implies_intr cphi |> Thm.forall_intr cx |> Thm.implies_intr lhs) (Thm.implies_elim (Thm.assume rhs |> Thm.forall_elim cx) (Thm.assume cphi) |> Thm.forall_intr cx |> Thm.implies_intr cphi |> Thm.implies_intr rhs) |> store_standard_thm_open (Binding.make ("norm_hhf_eq", \<^here>)) end; val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq); val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq]; fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false | is_norm_hhf (Const ("Pure.imp", _) $ _ $ (Const ("Pure.all", _) $ _)) = false | is_norm_hhf (Abs _ $ _) = false | is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u | is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t | is_norm_hhf _ = true; fun norm_hhf thy t = if is_norm_hhf t then t else Pattern.rewrite_term thy [norm_hhf_prop] [] t; fun norm_hhf_cterm ctxt raw_ct = let val thy = Proof_Context.theory_of ctxt; val ct = Thm.transfer_cterm thy raw_ct; val t = Thm.term_of ct; in if is_norm_hhf t then ct else Thm.cterm_of ctxt (norm_hhf thy t) end; (* var indexes *) fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1); fun incr_indexes2 th1 th2 = Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1); local (*compose Q and \Q1,Q2,...,Qk\ \ R to \Q2,...,Qk\ \ R getting unique result*) fun comp incremented th1 th2 = Thm.bicompose NONE {flatten = true, match = false, incremented = incremented} (false, th1, 0) 1 th2 |> Seq.list_of |> distinct Thm.eq_thm |> (fn [th] => Thm.solve_constraints th | _ => raise THM ("COMP", 1, [th1, th2])); in fun th1 COMP th2 = comp false th1 th2; fun th1 INCR_COMP th2 = comp true (incr_indexes th2 th1) th2; fun th1 COMP_INCR th2 = comp true th1 (incr_indexes th1 th2); end; fun comp_no_flatten (th, n) i rule = (case distinct Thm.eq_thm (Seq.list_of (Thm.bicompose NONE {flatten = false, match = false, incremented = true} (false, th, n) i (incr_indexes th rule))) of [th'] => Thm.solve_constraints th' | [] => raise THM ("comp_no_flatten", i, [th, rule]) | _ => raise THM ("comp_no_flatten: unique result expected", i, [th, rule])); (** variations on Thm.instantiate **) fun instantiate_normalize instpair th = Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl); fun instantiate'_normalize Ts ts th = Thm.adjust_maxidx_thm ~1 (Thm.instantiate' Ts ts th COMP_INCR asm_rl); (*instantiation with type-inference for variables*) fun infer_instantiate_types _ [] th = th | infer_instantiate_types ctxt args raw_th = let val thy = Proof_Context.theory_of ctxt; val th = Thm.transfer thy raw_th; fun infer ((xi, T), cu) (tyenv, maxidx) = let val _ = Thm.ctyp_of ctxt T; val _ = Thm.transfer_cterm thy cu; val U = Thm.typ_of_cterm cu; val maxidx' = maxidx |> Integer.max (#2 xi) |> Term.maxidx_typ T |> Integer.max (Thm.maxidx_of_cterm cu); val (tyenv', maxidx'') = Sign.typ_unify thy (T, U) (tyenv, maxidx') handle Type.TUNIFY => let val t = Var (xi, T); val u = Thm.term_of cu; in raise THM ("infer_instantiate_types: type " ^ Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^ Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^ "\ncannot be unified with type " ^ Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ " of term " ^ Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u), 0, [th]) end; in (tyenv', maxidx'') end; val (tyenv, _) = fold infer args (Vartab.empty, 0); val instT = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv []; val inst = args |> map (fn ((xi, T), cu) => ((xi, Envir.norm_type tyenv T), Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu))); in instantiate_normalize (instT, inst) th end handle CTERM (msg, _) => raise THM (msg, 0, [raw_th]) | TERM (msg, _) => raise THM (msg, 0, [raw_th]) | TYPE (msg, _, _) => raise THM (msg, 0, [raw_th]); fun infer_instantiate _ [] th = th | infer_instantiate ctxt args th = let val vars = Term.add_vars (Thm.full_prop_of th) []; val dups = duplicates (eq_fst op =) vars; val _ = null dups orelse raise THM ("infer_instantiate: inconsistent types for variables " ^ commas_quote (map (Syntax.string_of_term (Config.put show_types true ctxt) o Var) dups), 0, [th]); val args' = args |> map_filter (fn (xi, cu) => AList.lookup (op =) vars xi |> Option.map (fn T => ((xi, T), cu))); in infer_instantiate_types ctxt args' th end; fun infer_instantiate' ctxt args th = let val vars = build_rev (Term.add_vars (Thm.full_prop_of th)); val args' = zip_options vars args handle ListPair.UnequalLengths => raise THM ("infer_instantiate': more instantiations than variables in thm", 0, [th]); in infer_instantiate_types ctxt args' th end; (** renaming of bound variables **) (* replace bound variables x_i in thm by y_i *) (* where vs = [(x_1, y_1), ..., (x_n, y_n)] *) fun rename_bvars [] thm = thm | rename_bvars vs thm = let fun rename (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, rename t) | rename (t $ u) = rename t $ rename u | rename a = a; in Thm.renamed_prop (rename (Thm.prop_of thm)) thm end; (* renaming in left-to-right order *) fun rename_bvars' xs thm = let fun rename [] t = ([], t) | rename (x' :: xs) (Abs (x, T, t)) = let val (xs', t') = rename xs t in (xs', Abs (the_default x x', T, t')) end | rename xs (t $ u) = let val (xs', t') = rename xs t; val (xs'', u') = rename xs' u; in (xs'', t' $ u') end | rename xs a = (xs, a); in (case rename xs (Thm.prop_of thm) of ([], prop') => Thm.renamed_prop prop' thm | _ => error "More names than abstractions in theorem") end; end; structure Basic_Drule: BASIC_DRULE = Drule; open Basic_Drule; diff --git a/src/Pure/more_thm.ML b/src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML +++ b/src/Pure/more_thm.ML @@ -1,766 +1,778 @@ (* Title: Pure/more_thm.ML Author: Makarius Further operations on type ctyp/cterm/thm, outside the inference kernel. *) infix aconvc; signature BASIC_THM = sig include BASIC_THM val show_consts: bool Config.T val show_hyps: bool Config.T val show_tags: bool Config.T structure Ctermtab: TABLE structure Thmtab: TABLE val aconvc: cterm * cterm -> bool type attribute = Context.generic * thm -> Context.generic option * thm option end; signature THM = sig include THM structure Ctermtab: TABLE structure Thmtab: TABLE val eq_ctyp: ctyp * ctyp -> bool val aconvc: cterm * cterm -> bool val add_tvars: thm -> ctyp list -> ctyp list val add_frees: thm -> cterm list -> cterm list val add_vars: thm -> cterm list -> cterm list + val frees_of: thm -> cterm list val dest_funT: ctyp -> ctyp * ctyp val strip_type: ctyp -> ctyp list * ctyp val all_name: Proof.context -> string * cterm -> cterm -> cterm val all: Proof.context -> cterm -> cterm -> cterm val mk_binop: cterm -> cterm -> cterm -> cterm val dest_binop: cterm -> cterm * cterm val dest_implies: cterm -> cterm * cterm val dest_equals: cterm -> cterm * cterm val dest_equals_lhs: cterm -> cterm val dest_equals_rhs: cterm -> cterm val lhs_of: thm -> cterm val rhs_of: thm -> cterm val fast_term_ord: cterm ord val term_ord: cterm ord val thm_ord: thm ord val cterm_cache: (cterm -> 'a) -> cterm -> 'a val thm_cache: (thm -> 'a) -> thm -> 'a val is_reflexive: thm -> bool val eq_thm: thm * thm -> bool val eq_thm_prop: thm * thm -> bool val eq_thm_strict: thm * thm -> bool val equiv_thm: theory -> thm * thm -> bool val class_triv: theory -> class -> thm val of_sort: ctyp * sort -> thm list val is_dummy: thm -> bool val add_thm: thm -> thm list -> thm list val del_thm: thm -> thm list -> thm list val merge_thms: thm list * thm list -> thm list val item_net: thm Item_Net.T val item_net_intro: thm Item_Net.T val item_net_elim: thm Item_Net.T val declare_hyps: cterm -> Proof.context -> Proof.context val assume_hyps: cterm -> Proof.context -> thm * Proof.context val unchecked_hyps: Proof.context -> Proof.context val restore_hyps: Proof.context -> Proof.context -> Proof.context val undeclared_hyps: Context.generic -> thm -> term list val check_hyps: Context.generic -> thm -> thm val declare_term_sorts: term -> Proof.context -> Proof.context val extra_shyps': Proof.context -> thm -> sort list val check_shyps: Proof.context -> thm -> thm val weaken_sorts': Proof.context -> cterm -> cterm val elim_implies: thm -> thm -> thm val forall_intr_name: string * cterm -> thm -> thm val forall_elim_var: int -> thm -> thm val forall_elim_vars: int -> thm -> thm val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm val instantiate': ctyp option list -> cterm option list -> thm -> thm val forall_intr_frees: thm -> thm val unvarify_global: theory -> thm -> thm val unvarify_axiom: theory -> string -> thm val rename_params_rule: string list * int -> thm -> thm val rename_boundvars: term -> term -> thm -> thm val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory val add_axiom_global: binding * term -> theory -> (string * thm) * theory val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory type attribute = Context.generic * thm -> Context.generic option * thm option type binding = binding * attribute list val tag_rule: string * string -> thm -> thm val untag_rule: string -> thm -> thm val is_free_dummy: thm -> bool val tag_free_dummy: thm -> thm val def_name: string -> string val def_name_optional: string -> string -> string val def_binding: Binding.binding -> Binding.binding val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding val make_def_binding: bool -> Binding.binding -> Binding.binding val has_name_hint: thm -> bool val get_name_hint: thm -> string val put_name_hint: string -> thm -> thm val theoremK: string val legacy_get_kind: thm -> string val kind_rule: string -> thm -> thm val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic val theory_attributes: attribute list -> thm -> theory -> thm * theory val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context val no_attributes: 'a -> 'a * 'b list val simple_fact: 'a -> ('a * 'b list) list val tag: string * string -> attribute val untag: string -> attribute val kind: string -> attribute val register_proofs: thm list lazy -> theory -> theory val consolidate_theory: theory -> unit val expose_theory: theory -> unit val show_consts: bool Config.T val show_hyps: bool Config.T val show_tags: bool Config.T val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val pretty_thm_item: Proof.context -> thm -> Pretty.T val pretty_thm_global: theory -> thm -> Pretty.T val string_of_thm: Proof.context -> thm -> string val string_of_thm_global: theory -> thm -> string end; structure Thm: THM = struct (** basic operations **) (* collecting ctyps and cterms *) val eq_ctyp = op = o apply2 Thm.typ_of; val op aconvc = op aconv o apply2 Thm.term_of; val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a); val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a); val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); +fun frees_of th = + (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms + (fn a => fn (set, list) => + (case Thm.term_of a of + Free v => + if not (Term_Subst.Frees.defined set v) + then (Term_Subst.Frees.add (v, ()) set, a :: list) + else (set, list) + | _ => (set, list))) + |> #2; + (* ctyp operations *) fun dest_funT cT = (case Thm.typ_of cT of Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end | T => raise TYPE ("dest_funT", [T], [])); (* ctyp version of strip_type: maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *) fun strip_type cT = (case Thm.typ_of cT of Type ("fun", _) => let val (cT1, cT2) = dest_funT cT; val (cTs, cT') = strip_type cT2 in (cT1 :: cTs, cT') end | _ => ([], cT)); (* cterm operations *) fun all_name ctxt (x, t) A = let val T = Thm.typ_of_cterm t; val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T --> propT) --> propT)); in Thm.apply all_const (Thm.lambda_name (x, t) A) end; fun all ctxt t A = all_name ctxt ("", t) A; fun mk_binop c a b = Thm.apply (Thm.apply c a) b; fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct); fun dest_implies ct = (case Thm.term_of ct of Const ("Pure.imp", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_implies", [Thm.term_of ct])); fun dest_equals ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_equals", [Thm.term_of ct])); fun dest_equals_lhs ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct])); fun dest_equals_rhs ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct])); val lhs_of = dest_equals_lhs o Thm.cprop_of; val rhs_of = dest_equals_rhs o Thm.cprop_of; (* certified term order *) val fast_term_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of; val term_ord = Term_Ord.term_ord o apply2 Thm.term_of; (* thm order: ignores theory context! *) val thm_ord = Term_Ord.fast_term_ord o apply2 Thm.prop_of ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 Thm.tpairs_of ||| list_ord Term_Ord.fast_term_ord o apply2 Thm.hyps_of ||| list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of; (* tables and caches *) structure Ctermtab = Table(type key = cterm val ord = fast_term_ord); structure Thmtab = Table(type key = thm val ord = thm_ord); fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f; fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f; (* equality *) fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) handle TERM _ => false; val eq_thm = is_equal o thm_ord; val eq_thm_prop = op aconv o apply2 Thm.full_prop_of; fun eq_thm_strict ths = eq_thm ths andalso Context.eq_thy_id (apply2 Thm.theory_id ths) andalso op = (apply2 Thm.maxidx_of ths) andalso op = (apply2 Thm.get_tags ths); (* pattern equivalence *) fun equiv_thm thy ths = Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths); (* type classes and sorts *) fun class_triv thy c = Thm.of_class (Thm.global_ctyp_of thy (TVar ((Name.aT, 0), [c])), c); fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S; (* misc operations *) fun is_dummy thm = (case try Logic.dest_term (Thm.concl_of thm) of NONE => false | SOME t => Term.is_dummy_pattern (Term.head_of t)); (* collections of theorems in canonical order *) val add_thm = update eq_thm_prop; val del_thm = remove eq_thm_prop; val merge_thms = merge eq_thm_prop; val item_net = Item_Net.init eq_thm_prop (single o Thm.full_prop_of); val item_net_intro = Item_Net.init eq_thm_prop (single o Thm.concl_of); val item_net_elim = Item_Net.init eq_thm_prop (single o Thm.major_prem_of); (** declared hyps and sort hyps **) structure Hyps = Proof_Data ( type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T}; fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []}; ); fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} => let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps) in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end); (* hyps *) fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) => let val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct; val hyps' = Termtab.update (Thm.term_of ct, ()) hyps; in (checked_hyps, hyps', shyps) end); fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt); val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps)); fun restore_hyps ctxt = map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps)); fun undeclared_hyps context th = Thm.hyps_of th |> filter_out (case context of Context.Theory _ => K false | Context.Proof ctxt => (case Hyps.get ctxt of {checked_hyps = false, ...} => K true | {hyps, ...} => Termtab.defined hyps)); fun check_hyps context th = (case undeclared_hyps context th of [] => th | undeclared => error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared)))); (* shyps *) fun declare_term_sorts t = map_hyps (fn (checked_hyps, hyps, shyps) => (checked_hyps, hyps, Sorts.insert_term t shyps)); fun extra_shyps' ctxt th = Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th); fun check_shyps ctxt raw_th = let val th = Thm.strip_shyps raw_th; val extra_shyps = extra_shyps' ctxt th; in if null extra_shyps then th else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" :: Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps)))) end; val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get; (** basic derived rules **) (*Elimination of implication A A \ B ------------ B *) fun elim_implies thA thAB = Thm.implies_elim thAB thA; (* forall_intr_name *) fun forall_intr_name (a, x) th = let val th' = Thm.forall_intr x th; val prop' = (case Thm.prop_of th' of all $ Abs (_, T, b) => all $ Abs (a, T, b)); in Thm.renamed_prop prop' th' end; (* forall_elim_var(s) *) local fun dest_all ct = (case Thm.term_of ct of Const ("Pure.all", _) $ Abs (a, _, _) => let val (x, ct') = Thm.dest_abs NONE (Thm.dest_arg ct) in SOME ((a, Thm.ctyp_of_cterm x), ct') end | _ => NONE); fun dest_all_list ct = (case dest_all ct of NONE => [] | SOME (v, ct') => v :: dest_all_list ct'); fun forall_elim_vars_list vars i th = let val used = (Thm.fold_terms o Term.fold_aterms) (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th []; val vars' = (Name.variant_list used (map #1 vars), vars) |> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T)); in fold Thm.forall_elim vars' th end; in fun forall_elim_vars i th = forall_elim_vars_list (dest_all_list (Thm.cprop_of th)) i th; fun forall_elim_var i th = let val vars = (case dest_all (Thm.cprop_of th) of SOME (v, _) => [v] | NONE => raise THM ("forall_elim_var", i, [th])); in forall_elim_vars_list vars i th end; end; (* instantiate frees *) fun instantiate_frees ([], []) th = th | instantiate_frees (instT, inst) th = let val idx = Thm.maxidx_of th + 1; fun index ((a, A), b) = (((a, idx), A), b); val insts = (map index instT, map index inst); val tfrees = Symtab.build (fold (Symtab.insert_set o #1 o #1) instT); val frees = Symtab.build (fold (Symtab.insert_set o #1 o #1) inst); val hyps = Thm.chyps_of th; val inst_cterm = Thm.generalize_cterm (tfrees, frees) idx #> Thm.instantiate_cterm insts; in th |> fold_rev Thm.implies_intr hyps |> Thm.generalize (tfrees, frees) idx |> Thm.instantiate insts |> fold (elim_implies o Thm.assume o inst_cterm) hyps end; (* instantiate by left-to-right occurrence of variables *) fun instantiate' cTs cts thm = let fun err msg = raise TYPE ("instantiate': " ^ msg, map_filter (Option.map Thm.typ_of) cTs, map_filter (Option.map Thm.term_of) cts); fun zip_vars xs ys = zip_options xs ys handle ListPair.UnequalLengths => err "more instantiations than variables in thm"; val thm' = Thm.instantiate ((zip_vars (build_rev (Thm.fold_terms Term.add_tvars thm)) cTs), []) thm; val thm'' = Thm.instantiate ([], zip_vars (build_rev (Thm.fold_terms Term.add_vars thm')) cts) thm'; in thm'' end; (* forall_intr_frees: generalization over all suitable Free variables *) fun forall_intr_frees th = let val fixed0 = Term_Subst.Frees.build (fold Term_Subst.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #> fold Term_Subst.add_frees (Thm.hyps_of th)); val (_, frees) = (th, (fixed0, [])) |-> Thm.fold_atomic_cterms (fn a => fn (fixed, frees) => (case Thm.term_of a of Free v => if not (Term_Subst.Frees.defined fixed v) then (Term_Subst.Frees.add (v, ()) fixed, a :: frees) else (fixed, frees) | _ => (fixed, frees))); in fold Thm.forall_intr frees th end; (* unvarify_global: global schematic variables *) fun unvarify_global thy th = let val prop = Thm.full_prop_of th; val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) handle TERM (msg, _) => raise THM (msg, 0, [th]); val cert = Thm.global_cterm_of thy; val certT = Thm.global_ctyp_of thy; val instT = Term_Subst.TVars.build (prop |> (Term.fold_types o Term.fold_atyps) (fn T => fn instT => (case T of TVar (v as ((a, _), S)) => if Term_Subst.TVars.defined instT v then instT else Term_Subst.TVars.update (v, TFree (a, S)) instT | _ => instT))); val cinstT = Term_Subst.TVars.map (K certT) instT; val cinst = Term_Subst.Vars.build (prop |> Term.fold_aterms (fn t => fn inst => (case t of Var ((x, i), T) => let val T' = Term_Subst.instantiateT instT T in Term_Subst.Vars.update (((x, i), T'), cert (Free ((x, T')))) inst end | _ => inst))); in Thm.instantiate (Term_Subst.TVars.dest cinstT, Term_Subst.Vars.dest cinst) th end; fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy; (* user renaming of parameters in a subgoal *) (*The names, if distinct, are used for the innermost parameters of subgoal i; preceding parameters may be renamed to make all parameters distinct.*) fun rename_params_rule (names, i) st = let val (_, Bs, Bi, C) = Thm.dest_state (st, i); val params = map #1 (Logic.strip_params Bi); val short = length params - length names; val names' = if short < 0 then error "More names than parameters in subgoal!" else Name.variant_list names (take short params) @ names; val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi []; val Bi' = Logic.list_rename_params names' Bi; in (case duplicates (op =) names of a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); st) | [] => (case inter (op =) names free_names of a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); st) | [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st)) end; (* preservation of bound variable names *) fun rename_boundvars pat obj th = (case Term.rename_abs pat obj (Thm.prop_of th) of NONE => th | SOME prop' => Thm.renamed_prop prop' th); (** specification primitives **) (* rules *) fun stripped_sorts thy t = let val tfrees = build_rev (Term.add_tfrees t); val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees)); val recover = map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) tfrees' tfrees; val strip = map (apply2 TFree) (tfrees ~~ tfrees'); val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; in (strip, recover, t') end; fun add_axiom ctxt (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val (strip, recover, prop') = stripped_sorts thy prop; val constraints = map (fn (TFree (_, S), T) => (T, S)) strip; val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip; val thy' = thy |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop')); val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = Thm.instantiate (recover, []) axm' |> unvarify_global thy' |> fold elim_implies of_sorts; in ((axm_name, thm), thy') end; fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop); val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop); val thy' = Theory.add_def context unchecked overloaded (b, concl') thy; val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = Thm.instantiate (recover, []) axm' |> unvarify_global thy' |> fold_rev Thm.implies_intr prems; in ((axm_name, thm), thy') end; fun add_def_global unchecked overloaded arg thy = add_def (Defs.global_context thy) unchecked overloaded arg thy; (** theorem tags **) (* add / delete tags *) fun tag_rule tg = Thm.map_tags (insert (op =) tg); fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); (* free dummy thm -- for abstract closure *) val free_dummyN = "free_dummy"; fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; val tag_free_dummy = tag_rule (free_dummyN, ""); (* def_name *) fun def_name c = c ^ "_def"; fun def_name_optional c "" = def_name c | def_name_optional _ name = name; val def_binding = Binding.map_name def_name #> Binding.reset_pos; fun def_binding_optional b name = if Binding.is_empty name then def_binding b else name; fun make_def_binding cond b = if cond then def_binding b else Binding.empty; (* unofficial theorem names *) fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN; fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown"; fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); (* theorem kinds *) val theoremK = "theorem"; fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; (** attributes **) (*attributes subsume any kind of rules or context modifiers*) type attribute = Context.generic * thm -> Context.generic option * thm option; type binding = binding * attribute list; fun rule_attribute ths f (x, th) = (NONE, (case find_first is_free_dummy (th :: ths) of SOME th' => SOME th' | NONE => SOME (f x th))); fun declaration_attribute f (x, th) = (if is_free_dummy th then NONE else SOME (f th x), NONE); fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end; fun apply_attribute (att: attribute) th x = let val (x', th') = att (x, check_hyps x (Thm.transfer'' x th)) in (the_default th th', the_default x x') end; fun attribute_declaration att th x = #2 (apply_attribute att th x); fun apply_attributes mk dest = let fun app [] th x = (th, x) | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts; in app end; val theory_attributes = apply_attributes Context.Theory Context.the_theory; val proof_attributes = apply_attributes Context.Proof Context.the_proof; fun no_attributes x = (x, []); fun simple_fact x = [(x, [])]; fun tag tg = rule_attribute [] (K (tag_rule tg)); fun untag s = rule_attribute [] (K (untag_rule s)); fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k)); (** forked proofs **) structure Proofs = Theory_Data ( type T = thm list lazy Inttab.table; val empty = Inttab.empty; val extend = I; val merge = Inttab.merge (K true); ); fun reset_proofs thy = if Inttab.is_empty (Proofs.get thy) then NONE else SOME (Proofs.put Inttab.empty thy); val _ = Theory.setup (Theory.at_begin reset_proofs); fun register_proofs ths thy = let val entry = (serial (), Lazy.map_finished (map Thm.trim_context) ths) in (Proofs.map o Inttab.update) entry thy end; fun force_proofs thy = Proofs.get thy |> Inttab.dest |> maps (map (Thm.transfer thy) o Lazy.force o #2); val consolidate_theory = Thm.consolidate o force_proofs; fun expose_theory thy = if Proofterm.export_enabled () then Thm.expose_proofs thy (force_proofs thy) else (); (** print theorems **) (* options *) val show_consts = Config.declare_option_bool ("show_consts", \<^here>); val show_hyps = Config.declare_bool ("show_hyps", \<^here>) (K false); val show_tags = Config.declare_bool ("show_tags", \<^here>) (K false); (* pretty_thm etc. *) fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; val pretty_tags = Pretty.list "[" "]" o map pretty_tag; fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = let val show_tags = Config.get ctxt show_tags; val show_hyps = Config.get ctxt show_hyps; val th = raw_th |> perhaps (try (Thm.transfer' ctxt)) |> perhaps (try Thm.strip_shyps); val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; val extra_shyps = extra_shyps' ctxt th; val tags = Thm.get_tags th; val tpairs = Thm.tpairs_of th; val q = if quote then Pretty.quote else I; val prt_term = q o Syntax.pretty_term ctxt; val hlen = length extra_shyps + length hyps + length tpairs; val hsymbs = if hlen = 0 then [] else if show_hyps orelse show_hyps' then [Pretty.brk 2, Pretty.list "[" "]" (map (q o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ map (Syntax.pretty_sort ctxt) extra_shyps)] else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; val tsymbs = if null tags orelse not show_tags then [] else [Pretty.brk 1, pretty_tags tags]; in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; fun pretty_thm_global thy = pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; val string_of_thm = Pretty.string_of oo pretty_thm; val string_of_thm_global = Pretty.string_of oo pretty_thm_global; open Thm; end; structure Basic_Thm: BASIC_THM = Thm; open Basic_Thm;