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,323 +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 free_in v ct = member (op aconvc) (Misc_Legacy.cterm_frees ct) v +fun free_in v ct = Cterms.defined (Misc_Legacy.cterm_frees 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,234 @@ (* 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 (Misc_Legacy.cterm_frees tm) + val env = Cterms.list_set_rev (Misc_Legacy.cterm_frees tm) + val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons env (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,264 @@ (* 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}) + val mk_env = Cterms.list_set_rev o Misc_Legacy.cterm_frees in fn p => Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons - (Misc_Legacy.cterm_frees p) (K Thm.reflexive) (K Thm.reflexive) + (mk_env 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,1036 +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) + if not (Cterms.defined 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)) + not (Cterms.defined 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 (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg tm))) + (substitutable_monomial (fvs |> Cterms.fold Cterms.add (Misc_Legacy.cterm_frees (Thm.dest_arg tm))) (Thm.dest_arg1 tm) handle Failure _ => - substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg1 tm))) + substitutable_monomial (fvs |> Cterms.fold Cterms.add (Misc_Legacy.cterm_frees (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 (c,v) = substitutable_monomial Cterms.empty (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,75 @@ (* 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 (Misc_Legacy.cterm_frees p) atcv ncv qcv p end + let + val pcv = pcv ctxt + val env = Cterms.list_set_rev (Misc_Legacy.cterm_frees p) + in gen_qelim_conv ctxt pcv pcv pcv cons env 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,985 +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 free_in v t = member op aconvc (Misc_Legacy.cterm_frees t) v; +fun free_in v t = Cterms.defined (Misc_Legacy.cterm_frees 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 = Misc_Legacy.cterm_frees tm - val P' = fold mk_forall avs tm + val P' = fold mk_forall (Cterms.list_set_rev 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 + in specl (Cterms.list_set_rev 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) (Misc_Legacy.cterm_frees m) v)) mons + orelse not(Cterms.defined (Misc_Legacy.cterm_frees 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 (Misc_Legacy.cterm_frees m))) + List.partition (fn m => null (inter (op aconvc) vars (Cterms.list_set_rev (Misc_Legacy.cterm_frees 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/General/table.ML b/src/Pure/General/table.ML --- a/src/Pure/General/table.ML +++ b/src/Pure/General/table.ML @@ -1,479 +1,472 @@ (* Title: Pure/General/table.ML Author: Markus Wenzel and Stefan Berghofer, TU Muenchen Generic tables. Efficient purely functional implementation using balanced 2-3 trees. *) signature KEY = sig type key val ord: key ord end; signature TABLE = sig type key type 'a table exception DUP of key exception SAME exception UNDEF of key val empty: 'a table val build: ('a table -> 'a table) -> 'a table val is_empty: 'a table -> bool val is_single: 'a table -> bool val map: (key -> 'a -> 'b) -> 'a table -> 'b table val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a - val size: 'a table -> int val dest: 'a table -> (key * 'a) list val keys: 'a table -> key list val min: 'a table -> (key * 'a) option val max: 'a table -> (key * 'a) option val exists: (key * 'a -> bool) -> 'a table -> bool val forall: (key * 'a -> bool) -> 'a table -> bool val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option val lookup_key: 'a table -> key -> (key * 'a) option val lookup: 'a table -> key -> 'a option val defined: 'a table -> key -> bool val update: key * 'a -> 'a table -> 'a table val update_new: key * 'a -> 'a table -> 'a table (*exception DUP*) val default: key * 'a -> 'a table -> 'a table val map_entry: key -> ('a -> 'a) (*exception SAME*) -> 'a table -> 'a table val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table val make: (key * 'a) list -> 'a table (*exception DUP*) val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a table * 'a table -> 'a table (*exception DUP*) val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUP*) val delete: key -> 'a table -> 'a table (*exception UNDEF*) val delete_safe: key -> 'a table -> 'a table val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table (*exception DUP*) val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table val lookup_list: 'a list table -> key -> 'a list val cons_list: key * 'a -> 'a list table -> 'a list table val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table val make_list: (key * 'a) list -> 'a list table val dest_list: 'a list table -> (key * 'a) list val merge_list: ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table type set = unit table val insert_set: key -> set -> set val remove_set: key -> set -> set val make_set: key list -> set - val subset: set * set -> bool - val eq_set: set * set -> bool end; functor Table(Key: KEY): TABLE = struct (* datatype table *) type key = Key.key; datatype 'a table = Empty | Branch2 of 'a table * (key * 'a) * 'a table | Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table; exception DUP of key; (* empty and single *) val empty = Empty; fun build (f: 'a table -> 'a table) = f empty; fun is_empty Empty = true | is_empty _ = false; fun is_single (Branch2 (Empty, _, Empty)) = true | is_single _ = false; (* map and fold combinators *) fun map_table f = let fun map Empty = Empty | map (Branch2 (left, (k, x), right)) = Branch2 (map left, (k, f k x), map right) | map (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = Branch3 (map left, (k1, f k1 x1), map mid, (k2, f k2 x2), map right); in map end; fun fold_table f = let fun fold Empty x = x | fold (Branch2 (left, p, right)) x = fold right (f p (fold left x)) | fold (Branch3 (left, p1, mid, p2, right)) x = fold right (f p2 (fold mid (f p1 (fold left x)))); in fold end; fun fold_rev_table f = let fun fold Empty x = x | fold (Branch2 (left, p, right)) x = fold left (f p (fold right x)) | fold (Branch3 (left, p1, mid, p2, right)) x = fold left (f p1 (fold mid (f p2 (fold right x)))); in fold end; -fun size tab = fold_table (fn _ => fn n => n + 1) tab 0; fun dest tab = fold_rev_table cons tab []; fun keys tab = fold_rev_table (cons o #1) tab []; (* min/max entries *) fun min Empty = NONE | min (Branch2 (Empty, p, _)) = SOME p | min (Branch3 (Empty, p, _, _, _)) = SOME p | min (Branch2 (left, _, _)) = min left | min (Branch3 (left, _, _, _, _)) = min left; fun max Empty = NONE | max (Branch2 (_, p, Empty)) = SOME p | max (Branch3 (_, _, _, p, Empty)) = SOME p | max (Branch2 (_, _, right)) = max right | max (Branch3 (_, _, _, _, right)) = max right; (* exists and forall *) fun exists pred = let fun ex Empty = false | ex (Branch2 (left, (k, x), right)) = ex left orelse pred (k, x) orelse ex right | ex (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = ex left orelse pred (k1, x1) orelse ex mid orelse pred (k2, x2) orelse ex right; in ex end; fun forall pred = not o exists (not o pred); (* get_first *) fun get_first f = let fun get Empty = NONE | get (Branch2 (left, (k, x), right)) = (case get left of NONE => (case f (k, x) of NONE => get right | some => some) | some => some) | get (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = (case get left of NONE => (case f (k1, x1) of NONE => (case get mid of NONE => (case f (k2, x2) of NONE => get right | some => some) | some => some) | some => some) | some => some); in get end; (* lookup *) fun lookup tab key = let fun look Empty = NONE | look (Branch2 (left, (k, x), right)) = (case Key.ord (key, k) of LESS => look left | EQUAL => SOME x | GREATER => look right) | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = (case Key.ord (key, k1) of LESS => look left | EQUAL => SOME x1 | GREATER => (case Key.ord (key, k2) of LESS => look mid | EQUAL => SOME x2 | GREATER => look right)); in look tab end; fun lookup_key tab key = let fun look Empty = NONE | look (Branch2 (left, (k, x), right)) = (case Key.ord (key, k) of LESS => look left | EQUAL => SOME (k, x) | GREATER => look right) | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = (case Key.ord (key, k1) of LESS => look left | EQUAL => SOME (k1, x1) | GREATER => (case Key.ord (key, k2) of LESS => look mid | EQUAL => SOME (k2, x2) | GREATER => look right)); in look tab end; fun defined tab key = let fun def Empty = false | def (Branch2 (left, (k, x), right)) = (case Key.ord (key, k) of LESS => def left | EQUAL => true | GREATER => def right) | def (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = (case Key.ord (key, k1) of LESS => def left | EQUAL => true | GREATER => (case Key.ord (key, k2) of LESS => def mid | EQUAL => true | GREATER => def right)); in def tab end; (* modify *) datatype 'a growth = Stay of 'a table | Sprout of 'a table * (key * 'a) * 'a table; exception SAME; fun modify key f tab = let fun modfy Empty = Sprout (Empty, (key, f NONE), Empty) | modfy (Branch2 (left, p as (k, x), right)) = (case Key.ord (key, k) of LESS => (case modfy left of Stay left' => Stay (Branch2 (left', p, right)) | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right))) | EQUAL => Stay (Branch2 (left, (k, f (SOME x)), right)) | GREATER => (case modfy right of Stay right' => Stay (Branch2 (left, p, right')) | Sprout (right1, q, right2) => Stay (Branch3 (left, p, right1, q, right2)))) | modfy (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) = (case Key.ord (key, k1) of LESS => (case modfy left of Stay left' => Stay (Branch3 (left', p1, mid, p2, right)) | Sprout (left1, q, left2) => Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right))) | EQUAL => Stay (Branch3 (left, (k1, f (SOME x1)), mid, p2, right)) | GREATER => (case Key.ord (key, k2) of LESS => (case modfy mid of Stay mid' => Stay (Branch3 (left, p1, mid', p2, right)) | Sprout (mid1, q, mid2) => Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right))) | EQUAL => Stay (Branch3 (left, p1, mid, (k2, f (SOME x2)), right)) | GREATER => (case modfy right of Stay right' => Stay (Branch3 (left, p1, mid, p2, right')) | Sprout (right1, q, right2) => Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2))))); in (case modfy tab of Stay tab' => tab' | Sprout br => Branch2 br) handle SAME => tab end; fun update (key, x) tab = modify key (fn _ => x) tab; fun update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab; fun default (key, x) tab = modify key (fn NONE => x | SOME _ => raise SAME) tab; fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x); fun map_default (key, x) f = modify key (fn NONE => f x | SOME y => f y); (* delete *) exception UNDEF of key; local fun compare NONE (k2, _) = LESS | compare (SOME k1) (k2, _) = Key.ord (k1, k2); fun if_eq EQUAL x y = x | if_eq _ x y = y; fun del (SOME k) Empty = raise UNDEF k | del NONE (Branch2 (Empty, p, Empty)) = (p, (true, Empty)) | del NONE (Branch3 (Empty, p, Empty, q, Empty)) = (p, (false, Branch2 (Empty, q, Empty))) | del k (Branch2 (Empty, p, Empty)) = (case compare k p of EQUAL => (p, (true, Empty)) | _ => raise UNDEF (the k)) | del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare k p of EQUAL => (p, (false, Branch2 (Empty, q, Empty))) | _ => (case compare k q of EQUAL => (q, (false, Branch2 (Empty, p, Empty))) | _ => raise UNDEF (the k))) | del k (Branch2 (l, p, r)) = (case compare k p of LESS => (case del k l of (p', (false, l')) => (p', (false, Branch2 (l', p, r))) | (p', (true, l')) => (p', case r of Branch2 (rl, rp, rr) => (true, Branch3 (l', p, rl, rp, rr)) | Branch3 (rl, rp, rm, rq, rr) => (false, Branch2 (Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr))))) | ord => (case del (if_eq ord NONE k) r of (p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r'))) | (p', (true, r')) => (p', case l of Branch2 (ll, lp, lr) => (true, Branch3 (ll, lp, lr, if_eq ord p' p, r')) | Branch3 (ll, lp, lm, lq, lr) => (false, Branch2 (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r')))))) | del k (Branch3 (l, p, m, q, r)) = (case compare k q of LESS => (case compare k p of LESS => (case del k l of (p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r))) | (p', (true, l')) => (p', (false, case (m, r) of (Branch2 (ml, mp, mr), Branch2 _) => Branch2 (Branch3 (l', p, ml, mp, mr), q, r) | (Branch3 (ml, mp, mm, mq, mr), _) => Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r) | (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) => Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp, Branch2 (rm, rq, rr))))) | ord => (case del (if_eq ord NONE k) m of (p', (false, m')) => (p', (false, Branch3 (l, if_eq ord p' p, m', q, r))) | (p', (true, m')) => (p', (false, case (l, r) of (Branch2 (ll, lp, lr), Branch2 _) => Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r) | (Branch3 (ll, lp, lm, lq, lr), _) => Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, m'), q, r) | (_, Branch3 (rl, rp, rm, rq, rr)) => Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp, Branch2 (rm, rq, rr)))))) | ord => (case del (if_eq ord NONE k) r of (q', (false, r')) => (q', (false, Branch3 (l, p, m, if_eq ord q' q, r'))) | (q', (true, r')) => (q', (false, case (l, m) of (Branch2 _, Branch2 (ml, mp, mr)) => Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r')) | (_, Branch3 (ml, mp, mm, mq, mr)) => Branch3 (l, p, Branch2 (ml, mp, mm), mq, Branch2 (mr, if_eq ord q' q, r')) | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) => Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp, Branch2 (mr, if_eq ord q' q, r')))))); in fun delete key tab = snd (snd (del (SOME key) tab)); fun delete_safe key tab = if defined tab key then delete key tab else tab; end; (* membership operations *) fun member eq tab (key, x) = (case lookup tab key of NONE => false | SOME y => eq (x, y)); fun insert eq (key, x) = modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else raise DUP key); fun remove eq (key, x) tab = (case lookup tab key of NONE => tab | SOME y => if eq (x, y) then delete key tab else tab); (* simultaneous modifications *) fun make entries = build (fold update_new entries); fun join f (table1, table2) = let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab; in if pointer_eq (table1, table2) then table1 else if is_empty table1 then table2 else fold_table add table2 table1 end; fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key); (* list tables *) fun lookup_list tab key = these (lookup tab key); fun cons_list (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab; fun insert_list eq (key, x) = modify key (fn NONE => [x] | SOME xs => if Library.member eq xs x then raise SAME else x :: xs); fun remove_list eq (key, x) tab = map_entry key (fn xs => (case Library.remove eq x xs of [] => raise UNDEF key | ys => ys)) tab handle UNDEF _ => delete key tab; fun update_list eq (key, x) = modify key (fn NONE => [x] | SOME [] => [x] | SOME (xs as y :: _) => if eq (x, y) then raise SAME else Library.update eq x xs); fun make_list args = build (fold_rev cons_list args); fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab); fun merge_list eq = join (fn _ => Library.merge eq); (* set operations *) type set = unit table; fun insert_set x = default (x, ()); fun remove_set x : set -> set = delete_safe x; fun make_set xs = build (fold insert_set xs); -fun subset (A: set, B: set) = forall (defined B o #1) A; -fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B); - (* ML pretty-printing *) val _ = ML_system_pp (fn depth => fn pretty => fn tab => ML_Pretty.to_polyml (ML_Pretty.enum "," "{" "}" (ML_Pretty.pair (ML_Pretty.from_polyml o ML_system_pretty) (ML_Pretty.from_polyml o pretty)) (dest tab, depth))); (*final declarations of this structure!*) val map = map_table; val fold = fold_table; val fold_rev = fold_rev_table; end; structure Inttab = Table(type key = int val ord = int_ord); structure Symtab = Table(type key = string val ord = fast_string_ord); structure Symreltab = Table(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord); diff --git a/src/Pure/Isar/obtain.ML b/src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML +++ b/src/Pure/Isar/obtain.ML @@ -1,425 +1,425 @@ (* Title: Pure/Isar/obtain.ML Author: Markus Wenzel, TU Muenchen Generalized existence and cases rules within Isar proof text. *) signature OBTAIN = sig val obtain_thesis: Proof.context -> ((string * typ) * term) * Proof.context val obtains_attributes: ('typ, 'term) Element.obtain list -> attribute list val obtains_attribs: ('typ, 'term) Element.obtain list -> Token.src list val read_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list val cert_obtains: Proof.context -> term -> Element.obtains_i -> (binding * term) list val parse_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state val obtain: binding -> (binding * typ option * mixfix) list -> (binding * typ option * mixfix) list -> (term * term list) list list -> (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state val obtain_cmd: binding -> (binding * string option * mixfix) list -> (binding * string option * mixfix) list -> (string * string list) list list -> (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state val result: (Proof.context -> tactic) -> thm list -> Proof.context -> ((string * cterm) list * thm list) * Proof.context val guess: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state val guess_cmd: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state end; structure Obtain: OBTAIN = struct (** specification elements **) (* obtain_export *) (* [x, A x] : B -------- B *) fun eliminate_term ctxt xs tm = let val vs = map (dest_Free o Thm.term_of) xs; val bads = Term.fold_aterms (fn t as Free v => if member (op =) vs v then insert (op aconv) t else I | _ => I) tm []; val _ = null bads orelse error ("Result contains obtained parameters: " ^ space_implode " " (map (Syntax.string_of_term ctxt) bads)); in tm end; fun eliminate ctxt rule xs As thm = let val _ = eliminate_term ctxt xs (Thm.full_prop_of thm); val _ = Object_Logic.is_judgment ctxt (Thm.concl_of thm) orelse error "Conclusion in obtained context must be object-logic judgment"; val ((_, [thm']), ctxt') = Variable.import true [thm] ctxt; val prems = Drule.strip_imp_prems (Thm.cprop_of thm'); in ((Drule.implies_elim_list thm' (map Thm.assume prems) |> Drule.implies_intr_list (map (Drule.norm_hhf_cterm ctxt') As) |> Drule.forall_intr_list xs) COMP rule) |> Drule.implies_intr_list prems |> singleton (Variable.export ctxt' ctxt) end; fun obtain_export ctxt rule xs _ As = (eliminate ctxt rule xs As, eliminate_term ctxt xs); (* result declaration *) fun case_names (obtains: ('typ, 'term) Element.obtain list) = obtains |> map_index (fn (i, (b, _)) => if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b); fun obtains_attributes obtains = [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names (case_names obtains)]; fun obtains_attribs obtains = [Attrib.consumes (~ (length obtains)), Attrib.case_names (case_names obtains)]; (* obtain thesis *) fun obtain_thesis ctxt = let val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] ctxt; val t = Object_Logic.fixed_judgment ctxt x; val v = dest_Free (Object_Logic.drop_judgment ctxt t); in ((v, t), ctxt') end; (* obtain clauses *) local val mk_all_external = Logic.all_constraint o Variable.default_type; fun mk_all_internal ctxt (y, z) t = let val frees = Frees.build (t |> Term.fold_aterms (fn Free v => Frees.add_set v | _ => I)); val T = - (case Frees.get_first (fn ((x, T), ()) => if x = z then SOME T else NONE) frees of + (case Frees.get_first (fn ((x, T), _) => if x = z then SOME T else NONE) frees of SOME T => T | NONE => the_default dummyT (Variable.default_type ctxt z)); in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end; fun prepare_clause prep_var parse_prop mk_all ctxt thesis raw_vars raw_props = let val ((xs', vars), ctxt') = ctxt |> fold_map prep_var raw_vars |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars); val xs = map (Variable.check_name o #1) vars; in Logic.list_implies (map (parse_prop ctxt') raw_props, thesis) |> fold_rev (mk_all ctxt') (xs ~~ xs') end; fun prepare_obtains prep_clause check_terms ctxt thesis (raw_obtains: ('typ, 'term) Element.obtain list) = let val clauses = raw_obtains |> map (fn (_, (raw_vars, raw_props)) => prep_clause ctxt thesis raw_vars raw_props) |> check_terms ctxt; in map fst raw_obtains ~~ clauses end; val parse_clause = prepare_clause Proof_Context.read_var Syntax.parse_prop mk_all_external; val cert_clause = prepare_clause Proof_Context.cert_var (K I) mk_all_internal; in val read_obtains = prepare_obtains parse_clause Syntax.check_terms; val cert_obtains = prepare_obtains cert_clause (K I); val parse_obtains = prepare_obtains parse_clause (K I); end; (** consider: generalized elimination and cases rule **) (* consider (a) x where "A x" | (b) y where "B y" | ... \ have thesis if a [intro?]: "\x. A x \ thesis" and b [intro?]: "\y. B y \ thesis" and ... for thesis apply (insert that) *) local fun gen_consider prep_obtains raw_obtains int state = let val _ = Proof.assert_forward_or_chain state; val ctxt = Proof.context_of state; val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt; val obtains = prep_obtains thesis_ctxt thesis raw_obtains; val atts = Rule_Cases.cases_open :: obtains_attributes raw_obtains; in state |> Proof.have true NONE (K I) [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] (map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains) [((Binding.empty, atts), [(thesis, [])])] int |-> Proof.refine_insert end; in val consider = gen_consider cert_obtains; val consider_cmd = gen_consider read_obtains; end; (** obtain: augmented context based on generalized existence rule **) (* obtain (a) x where "A x" \ have thesis if a [intro?]: "\x. A x \ thesis" for thesis apply (insert that) fix x assm <> "A x" *) local fun gen_obtain prep_stmt prep_att that_binding raw_decls raw_fixes raw_prems raw_concls int state = let val _ = Proof.assert_forward_or_chain state; val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state); val ({vars, propss, binds, result_binds, ...}, params_ctxt) = prep_stmt (raw_decls @ raw_fixes) (raw_prems @ map #2 raw_concls) thesis_ctxt; val (decls, fixes) = chop (length raw_decls) vars ||> map #2; val (premss, conclss) = chop (length raw_prems) propss; val propss' = (map o map) (Logic.close_prop fixes (flat premss)) conclss; val that_prop = Logic.list_rename_params (map (#1 o #2) decls) (fold_rev (Logic.all o #2 o #2) decls (Logic.list_implies (flat propss', thesis))); val cparams = map (Thm.cterm_of params_ctxt o #2 o #2) decls; val asms = map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_concls ~~ map (map (rpair [])) propss'; fun after_qed (result_ctxt, results) state' = let val [rule] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in state' |> Proof.fix (map #1 decls) |> Proof.map_context (fold (Variable.bind_term o apsnd (Logic.close_term fixes)) binds) |> Proof.assm (obtain_export params_ctxt rule cparams) [] [] asms end; in state |> Proof.have true NONE after_qed [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] [((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])] [(Binding.empty_atts, [(thesis, [])])] int |-> Proof.refine_insert |> Proof.map_context (fold Variable.bind_term result_binds) end; in val obtain = gen_obtain Proof_Context.cert_stmt (K I); val obtain_cmd = gen_obtain Proof_Context.read_stmt Attrib.attribute_cmd; end; (** tactical result **) fun check_result ctxt thesis th = (case Thm.prems_of th of [prem] => if Thm.concl_of th aconv thesis andalso Logic.strip_assums_concl prem aconv thesis then th else error ("Guessed a different clause:\n" ^ Thm.string_of_thm ctxt th) | [] => error "Goal solved -- nothing guessed" | _ => error ("Guess split into several cases:\n" ^ Thm.string_of_thm ctxt th)); fun result tac facts ctxt = let val ((thesis_var, thesis), thesis_ctxt) = obtain_thesis ctxt; val st = Goal.init (Thm.cterm_of ctxt thesis); val rule = (case SINGLE (Method.insert_tac thesis_ctxt facts 1 THEN tac thesis_ctxt) st of NONE => raise THM ("Obtain.result: tactic failed", 0, facts) | SOME th => check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th))); val closed_rule = Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) rule; val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt; val obtain_rule = Thm.forall_elim (Thm.cterm_of ctxt (Logic.varify_global (Free thesis_var))) rule'; val ((params, stmt), fix_ctxt) = Variable.focus_cterm NONE (Thm.cprem_of obtain_rule 1) ctxt'; val (prems, ctxt'') = Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params)) (Drule.strip_imp_prems stmt) fix_ctxt; in ((params, prems), ctxt'') end; (** guess: obtain based on tactical result **) (* guess x \ { fix thesis have "PROP ?guess" apply magic \ \turn goal into \thesis \ #thesis\\ apply_end magic \ \turn final \(\x. P x \ thesis) \ #thesis\ into\ \ \\#((\x. A x \ thesis) \ thesis)\ which is a finished goal state\ } fix x assm <> "A x" *) local fun unify_params vars thesis_var raw_rule ctxt = let val thy = Proof_Context.theory_of ctxt; val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); fun err msg th = error (msg ^ ":\n" ^ Thm.string_of_thm ctxt th); val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; val rule = Thm.incr_indexes (maxidx + 1) raw_rule; val params = Rule_Cases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); val m = length vars; val n = length params; val _ = m <= n orelse err "More variables than parameters in obtained rule" rule; fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max) handle Type.TUNIFY => err ("Failed to unify variable " ^ string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^ string_of_term (Syntax_Trans.mark_bound_abs (y, Envir.norm_type tyenv U)) ^ " in") rule; val (tyenv, _) = fold unify (map #1 vars ~~ take m params) (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule)); val norm_type = Envir.norm_type tyenv; val xs = map (apsnd norm_type o fst) vars; val ys = map (apsnd norm_type) (drop m params); val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys; val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys'); val instT = TVars.build (params |> fold (#2 #> Term.fold_atyps (fn T => fn instT => (case T of TVar v => if TVars.defined instT v then instT else TVars.add (v, Thm.ctyp_of ctxt (norm_type T)) instT | _ => instT)))); val closed_rule = rule |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) |> Thm.instantiate (TVars.dest instT, []); val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt; val vars' = map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ (map snd vars @ replicate (length ys) NoSyn); val rule'' = Thm.forall_elim (Thm.cterm_of ctxt' (Logic.varify_global (Free thesis_var))) rule'; in ((vars', rule''), ctxt') end; fun inferred_type (binding, _, mx) ctxt = let val x = Variable.check_name binding; val ((_, T), ctxt') = Proof_Context.inferred_param x ctxt in ((x, T, mx), ctxt') end; fun polymorphic ctxt vars = let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars)) in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end; fun gen_guess prep_var raw_vars int state = let val _ = Proof.assert_forward_or_chain state; val ctxt = Proof.context_of state; val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; val (thesis_var, thesis) = #1 (obtain_thesis ctxt); val vars = ctxt |> fold_map prep_var raw_vars |-> fold_map inferred_type |> fst |> polymorphic ctxt; fun guess_context raw_rule state' = let val ((parms, rule), ctxt') = unify_params vars thesis_var raw_rule (Proof.context_of state'); val (xs, _) = Variable.add_fixes (map (#1 o #1) parms) ctxt'; val ps = xs ~~ map (#2 o #1) parms; val ts = map Free ps; val asms = Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) |> map (fn asm => (Term.betapplys (fold_rev Term.abs ps asm, ts), [])); val _ = not (null asms) orelse error "Trivial result -- nothing guessed"; in state' |> Proof.map_context (K ctxt') |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms) |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm (obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts)) [] [] [(Binding.empty_atts, asms)]) |> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts) end; val goal = Var (("guess", 0), propT); val pos = Position.thread_data (); fun print_result ctxt' (k, [(s, [_, th])]) = Proof_Display.print_results int pos ctxt' (k, [(s, [th])]); val before_qed = Method.primitive_text (fn ctxt => Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #> (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))); fun after_qed (result_ctxt, results) state' = let val [_, res] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in state' |> Proof.end_block |> guess_context (check_result ctxt thesis res) end; in state |> Proof.enter_forward |> Proof.begin_block |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] |> Proof.chain_facts chain_facts |> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess" (SOME before_qed) after_qed [] [] [(Binding.empty_atts, [(Logic.mk_term goal, []), (goal, [])])] |> snd |> Proof.refine_singleton (Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis))) end; in val guess = gen_guess Proof_Context.cert_var; val guess_cmd = gen_guess Proof_Context.read_var; end; end; diff --git a/src/Pure/Tools/rule_insts.ML b/src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML +++ b/src/Pure/Tools/rule_insts.ML @@ -1,353 +1,353 @@ (* Title: Pure/Tools/rule_insts.ML Author: Makarius Rule instantiations -- operations within implicit rule / subgoal context. *) signature RULE_INSTS = sig val where_rule: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> thm val of_rule: Proof.context -> string option list * string option list -> (binding * string option * mixfix) list -> thm -> thm val read_instantiate: Proof.context -> ((indexname * Position.T) * string) list -> string list -> thm -> thm val read_term: string -> Proof.context -> term * Proof.context val goal_context: term -> Proof.context -> (string * typ) list * Proof.context val res_inst_tac: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic val eres_inst_tac: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic val cut_inst_tac: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic val forw_inst_tac: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic val dres_inst_tac: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic val thin_tac: Proof.context -> string -> (binding * string option * mixfix) list -> int -> tactic val subgoal_tac: Proof.context -> string -> (binding * string option * mixfix) list -> int -> tactic val make_elim_preserve: Proof.context -> thm -> thm val method: (Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic) -> (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser end; structure Rule_Insts: RULE_INSTS = struct (** read instantiations **) local fun error_var msg (xi, pos) = error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos); fun the_sort tvars (ai, pos) : sort = - (case TVars.get_first (fn ((bi, S), ()) => if ai = bi then SOME S else NONE) tvars of + (case TVars.get_first (fn ((bi, S), _) => if ai = bi then SOME S else NONE) tvars of SOME S => S | NONE => error_var "No such type variable in theorem: " (ai, pos)); fun the_type vars (xi, pos) : typ = (case Vartab.lookup vars xi of SOME T => T | NONE => error_var "No such variable in theorem: " (xi, pos)); fun read_type ctxt tvars ((xi, pos), s) = let val S = the_sort tvars (xi, pos); val T = Syntax.read_typ ctxt s; in if Sign.of_sort (Proof_Context.theory_of ctxt) (T, S) then ((xi, S), T) else error_var "Bad sort for instantiation of type variable: " (xi, pos) end; fun make_instT f (tvars: TVars.set) = let fun add v = let val T = TVar v; val T' = f T; in if T = T' then I else cons (v, T') end; in TVars.fold (add o #1) tvars [] end; fun make_inst f vars = let fun add v = let val t = Var v; val t' = f t; in if t aconv t' then I else cons (v, t') end; in fold add vars [] end; fun read_terms ss Ts ctxt = let fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt; val (ts, ctxt') = fold_map Variable.fix_dummy_patterns (map2 parse Ts ss) ctxt; val ts' = map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts |> Syntax.check_terms ctxt' |> Variable.polymorphic ctxt'; val Ts' = map Term.fastype_of ts'; val tyenv = Vartab.build (fold (Sign.typ_match (Proof_Context.theory_of ctxt)) (Ts ~~ Ts')); val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv []; in ((ts', tyenv'), ctxt') end; in fun read_term s ctxt = let val (t, ctxt') = Variable.fix_dummy_patterns (Syntax.parse_term ctxt s) ctxt; val t' = Syntax.check_term ctxt' t; in (t', ctxt') end; fun read_insts thm raw_insts raw_fixes ctxt = let val (type_insts, term_insts) = List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts; val tvars = TVars.build (Thm.fold_terms {hyps = false} TVars.add_tvars thm); val vars = Vars.build (Thm.fold_terms {hyps = false} Vars.add_vars thm); (*eigen-context*) val (_, ctxt1) = ctxt |> TVars.fold (Variable.declare_internal o Logic.mk_type o TVar o #1) tvars |> Vars.fold (Variable.declare_internal o Var o #1) vars |> Proof_Context.add_fixes_cmd raw_fixes; (*explicit type instantiations*) val instT1 = Term_Subst.instantiateT (TVars.make (map (read_type ctxt1 tvars) type_insts)); val vars1 = - Vartab.build (vars |> Vars.fold (fn ((v, T), ()) => + Vartab.build (vars |> Vars.fold (fn ((v, T), _) => Vartab.insert (K true) (v, instT1 T))); (*term instantiations*) val (xs, ss) = split_list term_insts; val Ts = map (the_type vars1) xs; val ((ts, inferred), ctxt2) = read_terms ss Ts ctxt1; (*implicit type instantiations*) val instT2 = Term_Subst.instantiateT (TVars.make inferred); val vars2 = Vartab.fold (fn (v, T) => cons (v, instT2 T)) vars1 []; val inst2 = Term_Subst.instantiate (TVars.empty, Vars.build (fold2 (fn (xi, _) => fn t => Vars.add ((xi, Term.fastype_of t), t)) xs ts)) #> Envir.beta_norm; val inst_tvars = make_instT (instT2 o instT1) tvars; val inst_vars = make_inst inst2 vars2; in ((inst_tvars, inst_vars), ctxt2) end; end; (** forward rules **) fun where_rule ctxt raw_insts raw_fixes thm = let val ((inst_tvars, inst_vars), ctxt') = read_insts thm raw_insts raw_fixes ctxt; in thm |> Drule.instantiate_normalize (map (apsnd (Thm.ctyp_of ctxt')) inst_tvars, map (apsnd (Thm.cterm_of ctxt')) inst_vars) |> singleton (Variable.export ctxt' ctxt) |> Rule_Cases.save thm end; fun of_rule ctxt (args, concl_args) fixes thm = let fun zip_vars _ [] = [] | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest | zip_vars ((x, _) :: xs) (SOME t :: rest) = ((x, Position.none), t) :: zip_vars xs rest | zip_vars [] _ = error "More instantiations than variables in theorem"; val insts = zip_vars (build_rev (Term.add_vars (Thm.full_prop_of thm))) args @ zip_vars (build_rev (Term.add_vars (Thm.concl_of thm))) concl_args; in where_rule ctxt insts fixes thm end; fun read_instantiate ctxt insts xs = where_rule ctxt insts (map (fn x => (Binding.name x, NONE, NoSyn)) xs); (** attributes **) (* where: named instantiation *) val named_insts = Parse.and_list1 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.embedded_inner_syntax)) -- Parse.for_fixes; val _ = Theory.setup (Attrib.setup \<^binding>\where\ (Scan.lift named_insts >> (fn args => Thm.rule_attribute [] (fn context => uncurry (where_rule (Context.proof_of context)) args))) "named instantiation of theorem"); (* of: positional instantiation (terms only) *) local val inst = Args.maybe Args.embedded_inner_syntax; val concl = Args.$$$ "concl" -- Args.colon; val insts = Scan.repeat (Scan.unless concl inst) -- Scan.optional (concl |-- Scan.repeat inst) []; in val _ = Theory.setup (Attrib.setup \<^binding>\of\ (Scan.lift (insts -- Parse.for_fixes) >> (fn args => Thm.rule_attribute [] (fn context => uncurry (of_rule (Context.proof_of context)) args))) "positional instantiation of theorem"); end; (** tactics **) (* goal context *) fun goal_context goal ctxt = let val ((_, params), ctxt') = ctxt |> Variable.declare_constraints goal |> Variable.improper_fixes |> Variable.focus_params NONE goal ||> Variable.restore_proper_fixes ctxt; in (params, ctxt') end; (* resolution after lifting and instantiation; may refer to parameters of the subgoal *) fun bires_inst_tac bires_flag ctxt raw_insts raw_fixes thm i st = CSUBGOAL (fn (cgoal, _) => let (*goal context*) val (params, goal_ctxt) = goal_context (Thm.term_of cgoal) ctxt; val paramTs = map #2 params; (*instantiation context*) val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm raw_insts raw_fixes goal_ctxt; val fixed = map #1 (fold (Variable.add_newly_fixed inst_ctxt goal_ctxt o #2) inst_vars []); (* lift and instantiate rule *) val inc = Thm.maxidx_of st + 1; val lift_type = Logic.incr_tvar inc; fun lift_var ((a, j), T) = ((a, j + inc), paramTs ---> lift_type T); fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t); val inst_tvars' = inst_tvars |> map (fn (((a, i), S), T) => (((a, i + inc), S), Thm.ctyp_of inst_ctxt (lift_type T))); val inst_vars' = inst_vars |> map (fn (v, t) => (lift_var v, Thm.cterm_of inst_ctxt (lift_term t))); val thm' = Thm.lift_rule cgoal thm |> Drule.instantiate_normalize (inst_tvars', inst_vars') |> singleton (Variable.export inst_ctxt ctxt); in compose_tac ctxt (bires_flag, thm', Thm.nprems_of thm) i end) i st; val res_inst_tac = bires_inst_tac false; val eres_inst_tac = bires_inst_tac true; (* forward resolution *) fun make_elim_preserve ctxt rl = let val maxidx = Thm.maxidx_of rl; fun var x = ((x, 0), propT); fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT)); val revcut_rl' = Drule.instantiate_normalize ([], [(var "V", cvar ("V", maxidx + 1)), (var "W", cvar ("W", maxidx + 1))]) Drule.revcut_rl; in (case Seq.list_of (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} (false, rl, Thm.nprems_of rl) 1 revcut_rl') of [th] => th | _ => raise THM ("make_elim_preserve", 1, [rl])) end; (*instantiate and cut -- for atomic fact*) fun cut_inst_tac ctxt insts fixes rule = res_inst_tac ctxt insts fixes (make_elim_preserve ctxt rule); (*forward tactic applies a rule to an assumption without deleting it*) fun forw_inst_tac ctxt insts fixes rule = cut_inst_tac ctxt insts fixes rule THEN' assume_tac ctxt; (*dresolve tactic applies a rule to replace an assumption*) fun dres_inst_tac ctxt insts fixes rule = eres_inst_tac ctxt insts fixes (make_elim_preserve ctxt rule); (* derived tactics *) (*deletion of an assumption*) fun thin_tac ctxt s fixes = eres_inst_tac ctxt [((("V", 0), Position.none), s)] fixes Drule.thin_rl; (*Introduce the given proposition as lemma and subgoal*) fun subgoal_tac ctxt A fixes = DETERM o res_inst_tac ctxt [((("psi", 0), Position.none), A)] fixes cut_rl; (* method wrapper *) fun method inst_tac tac = Args.goal_spec -- Scan.optional (Scan.lift (named_insts --| Args.$$$ "in")) ([], []) -- Attrib.thms >> (fn ((quant, (insts, fixes)), thms) => fn ctxt => METHOD (fn facts => if null insts andalso null fixes then quant (Method.insert_tac ctxt facts THEN' tac ctxt thms) else (case thms of [thm] => quant (Method.insert_tac ctxt facts THEN' inst_tac ctxt insts fixes thm) | _ => error "Cannot have instantiations with multiple rules"))); (* setup *) (*warning: rule_tac etc. refer to dynamic subgoal context!*) val _ = Theory.setup (Method.setup \<^binding>\rule_tac\ (method res_inst_tac resolve_tac) "apply rule (dynamic instantiation)" #> Method.setup \<^binding>\erule_tac\ (method eres_inst_tac eresolve_tac) "apply rule in elimination manner (dynamic instantiation)" #> Method.setup \<^binding>\drule_tac\ (method dres_inst_tac dresolve_tac) "apply rule in destruct manner (dynamic instantiation)" #> Method.setup \<^binding>\frule_tac\ (method forw_inst_tac forward_tac) "apply rule in forward manner (dynamic instantiation)" #> Method.setup \<^binding>\cut_tac\ (method cut_inst_tac (K cut_rules_tac)) "cut rule (dynamic instantiation)" #> Method.setup \<^binding>\subgoal_tac\ (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.embedded_inner_syntax -- Parse.for_fixes) >> (fn (quant, (props, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (EVERY' (map (fn prop => subgoal_tac ctxt prop fixes) props)))) "insert subgoal (dynamic instantiation)" #> Method.setup \<^binding>\thin_tac\ (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >> (fn (quant, (prop, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop fixes))) "remove premise (dynamic instantiation)"); end; diff --git a/src/Pure/goal.ML b/src/Pure/goal.ML --- a/src/Pure/goal.ML +++ b/src/Pure/goal.ML @@ -1,342 +1,342 @@ (* Title: Pure/goal.ML Author: Makarius Goals in tactical theorem proving, with support for forked proofs. *) signature BASIC_GOAL = sig val quick_and_dirty: bool Config.T val SELECT_GOAL: tactic -> int -> tactic val PREFER_GOAL: tactic -> int -> tactic val CONJUNCTS: tactic -> int -> tactic val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic end; signature GOAL = sig include BASIC_GOAL val init: cterm -> thm val protect: int -> thm -> thm val conclude: thm -> thm val check_finished: Proof.context -> thm -> thm val finish: Proof.context -> thm -> thm val norm_result: Proof.context -> thm -> thm val skip_proofs_enabled: unit -> bool val future_result: Proof.context -> thm future -> term -> thm val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm val is_schematic: term -> bool val prove_common: Proof.context -> int option -> string list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> thm list val prove_future: Proof.context -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm val prove: Proof.context -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm val prove_global_future: theory -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm val prove_global: theory -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm val prove_sorry: Proof.context -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm val prove_sorry_global: theory -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm val restrict: int -> int -> thm -> thm val unrestrict: int -> thm -> thm val conjunction_tac: int -> tactic val precise_conjunction_tac: int -> int -> tactic val recover_conjunction_tac: tactic val norm_hhf_tac: Proof.context -> int -> tactic val assume_rule_tac: Proof.context -> int -> tactic end; structure Goal: GOAL = struct (** goals **) (* -------- (init) C \ #C *) fun init C = Thm.instantiate ([], [((("A", 0), propT), C)]) Drule.protectI; (* A1 \ ... \ An \ C ------------------------ (protect n) A1 \ ... \ An \ #C *) fun protect n th = Drule.comp_no_flatten (th, n) 1 Drule.protectI; (* A \ ... \ #C ---------------- (conclude) A \ ... \ C *) fun conclude th = Drule.comp_no_flatten (th, Thm.nprems_of th) 1 Drule.protectD; (* #C --- (finish) C *) fun check_finished ctxt th = if Thm.no_prems th then th else raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]); fun finish ctxt = check_finished ctxt #> conclude; (** results **) (* normal form *) fun norm_result ctxt = Drule.flexflex_unique (SOME ctxt) #> Raw_Simplifier.norm_hhf_protect ctxt #> Thm.strip_shyps #> Drule.zero_var_indexes; (* scheduling parameters *) fun skip_proofs_enabled () = let val skip = Options.default_bool "skip_proofs" in if Proofterm.proofs_enabled () andalso skip then (warning "Proof terms enabled -- cannot skip proofs"; false) else skip end; (* future_result *) fun future_result ctxt result prop = let val assms = Assumption.all_assms_of ctxt; val As = map Thm.term_of assms; val frees = Frees.build (fold Frees.add_frees (prop :: As)); val xs = Frees.fold_rev (cons o Thm.cterm_of ctxt o Free o #1) frees []; val tfrees = TFrees.build (fold TFrees.add_tfrees (prop :: As)); val Ts = Names.build (TFrees.fold (Names.add_set o #1 o #1) tfrees); val instT = - build (tfrees |> TFrees.fold (fn ((a, S), ()) => + build (tfrees |> TFrees.fold (fn ((a, S), _) => cons (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S))))); val global_prop = Logic.list_implies (As, prop) |> Frees.fold_rev (Logic.all o Free o #1) frees |> Logic.varify_types_global |> Thm.cterm_of ctxt |> Thm.weaken_sorts' ctxt; val global_result = result |> Future.map (Drule.flexflex_unique (SOME ctxt) #> Drule.implies_intr_list assms #> Drule.forall_intr_list xs #> Thm.adjust_maxidx_thm ~1 #> Thm.generalize (Ts, Names.empty) 0 #> Thm.strip_shyps #> Thm.solve_constraints); val local_result = Thm.future global_result global_prop |> Thm.close_derivation \<^here> |> Thm.instantiate (instT, []) |> Drule.forall_elim_list xs |> fold (Thm.elim_implies o Thm.assume) assms |> Thm.solve_constraints; in local_result end; (** tactical theorem proving **) (* prove_internal -- minimal checks, no normalization of result! *) fun prove_internal ctxt casms cprop tac = (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of SOME th => Drule.implies_intr_list casms (finish ctxt th) | NONE => error "Tactic failed"); (* prove variations *) fun is_schematic t = Term.exists_subterm Term.is_Var t orelse Term.exists_type (Term.exists_subtype Term.is_TVar) t; fun prove_common ctxt fork_pri xs asms props tac = let val thy = Proof_Context.theory_of ctxt; val schematic = exists is_schematic props; val immediate = is_none fork_pri; val future = Future.proofs_enabled 1 andalso not (Proofterm.proofs_enabled ()); val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled (); val pos = Position.thread_data (); fun err msg = cat_error msg ("The error(s) above occurred for the goal statement" ^ Position.here pos ^ ":\n" ^ Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props))); fun cert_safe t = Thm.cterm_of ctxt (Envir.beta_norm (Term.no_dummy_patterns t)) handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; val casms = map cert_safe asms; val cprops = map cert_safe props; val (prems, ctxt') = ctxt |> Variable.add_fixes_direct xs |> fold Variable.declare_term (asms @ props) |> Assumption.add_assumes casms ||> Variable.set_body true; val stmt = Thm.weaken_sorts' ctxt' (Conjunction.mk_conjunction_balanced cprops); fun tac' args st = if skip then ALLGOALS (Skip_Proof.cheat_tac ctxt) st before Skip_Proof.report ctxt else tac args st; fun result () = (case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of NONE => err "Tactic failed" | SOME st => let val _ = Context.subthy_id (Thm.theory_id st, Context.theory_id thy) orelse err "Bad background theory of goal state"; val res = (finish ctxt' st |> Drule.flexflex_unique (SOME ctxt') |> Thm.check_shyps ctxt' |> Thm.check_hyps (Context.Proof ctxt')) handle THM (msg, _, _) => err msg | ERROR msg => err msg; in if Unify.matches_list (Context.Proof ctxt') [Thm.term_of stmt] [Thm.prop_of res] then res else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res)) end); val res = if immediate orelse schematic orelse not future orelse skip then result () else future_result ctxt' (Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = the fork_pri} result) (Thm.term_of stmt); in res |> Thm.close_derivation \<^here> |> Conjunction.elim_balanced (length props) |> map (Assumption.export false ctxt' ctxt) |> Variable.export ctxt' ctxt |> map Drule.zero_var_indexes end; fun prove_future_pri ctxt pri xs asms prop tac = hd (prove_common ctxt (SOME pri) xs asms [prop] tac); fun prove_future ctxt = prove_future_pri ctxt ~1; fun prove ctxt xs asms prop tac = hd (prove_common ctxt NONE xs asms [prop] tac); fun prove_global_future thy xs asms prop tac = Drule.export_without_context (prove_future (Proof_Context.init_global thy) xs asms prop tac); fun prove_global thy xs asms prop tac = Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac); (* skip proofs *) val quick_and_dirty = Config.declare_option_bool ("quick_and_dirty", \<^here>); fun prove_sorry ctxt xs asms prop tac = if Config.get ctxt quick_and_dirty then prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)) else (if Future.proofs_enabled 1 then prove_future_pri ctxt ~2 else prove ctxt) xs asms prop tac; fun prove_sorry_global thy xs asms prop tac = Drule.export_without_context (prove_sorry (Proof_Context.init_global thy) xs asms prop tac); (** goal structure **) (* rearrange subgoals *) fun restrict i n st = if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then raise THM ("Goal.restrict", i, [st]) else rotate_prems (i - 1) st |> protect n; fun unrestrict i = conclude #> rotate_prems (1 - i); (*with structural marker*) fun SELECT_GOAL tac i st = if Thm.nprems_of st = 1 andalso i = 1 then tac st else (PRIMITIVE (restrict i 1) THEN tac THEN PRIMITIVE (unrestrict i)) st; (*without structural marker*) fun PREFER_GOAL tac i st = if i < 1 orelse i > Thm.nprems_of st then Seq.empty else (PRIMITIVE (rotate_prems (i - 1)) THEN tac THEN PRIMITIVE (rotate_prems (1 - i))) st; (* multiple goals *) fun precise_conjunction_tac 0 i = eq_assume_tac i | precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i | precise_conjunction_tac n i = PRIMITIVE (Drule.with_subgoal i (Conjunction.curry_balanced n)); val adhoc_conjunction_tac = REPEAT_ALL_NEW (SUBGOAL (fn (goal, i) => if can Logic.dest_conjunction goal then resolve0_tac [Conjunction.conjunctionI] i else no_tac)); val conjunction_tac = SUBGOAL (fn (goal, i) => precise_conjunction_tac (length (Logic.dest_conjunctions goal)) i ORELSE TRY (adhoc_conjunction_tac i)); val recover_conjunction_tac = PRIMITIVE (fn th => Conjunction.uncurry_balanced (Thm.nprems_of th) th); fun PRECISE_CONJUNCTS n tac = SELECT_GOAL (precise_conjunction_tac n 1 THEN tac THEN recover_conjunction_tac); fun CONJUNCTS tac = SELECT_GOAL (conjunction_tac 1 THEN tac THEN recover_conjunction_tac); (* hhf normal form *) fun norm_hhf_tac ctxt = resolve_tac ctxt [Drule.asm_rl] (*cheap approximation -- thanks to builtin Logic.flatten_params*) THEN' SUBGOAL (fn (t, i) => if Drule.is_norm_hhf t then all_tac else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i); (* non-atomic goal assumptions *) fun non_atomic (Const ("Pure.imp", _) $ _ $ _) = true | non_atomic (Const ("Pure.all", _) $ _) = true | non_atomic _ = false; fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) => let val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt; val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); val tacs = Rs |> map (fn R => eresolve_tac ctxt [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac ctxt); in fold_rev (curry op APPEND') tacs (K no_tac) i end); end; structure Basic_Goal: BASIC_GOAL = Goal; open Basic_Goal; 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,783 +1,774 @@ (* 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 Cterms: ITEMS 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 + structure Cterms: ITEMS val eq_ctyp: ctyp * ctyp -> bool val aconvc: cterm * cterm -> bool val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table val add_vars: thm -> cterm Vars.table -> cterm Vars.table 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 forall_intr_vars: 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 {hyps = false} Term.is_TVar (fn cT => fn tab => let val v = Term.dest_TVar (Thm.typ_of cT) in tab |> not (TVars.defined tab v) ? TVars.add (v, cT) end); val add_vars = Thm.fold_atomic_cterms {hyps = false} Term.is_Var (fn ct => fn tab => let val v = Term.dest_Var (Thm.term_of ct) in tab |> not (Vars.defined tab v) ? Vars.add (v, ct) end); (* 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; (* scalable collections *) +structure Cterms = Items(type key = cterm val ord = fast_term_ord); 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 {hyps = false} 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 = Names.build (fold (Names.add_set o #1 o #1) instT); val frees = Names.build (fold (Names.add_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 instT = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_tvars thm)) cTs; val thm' = Thm.instantiate (instT, []) thm; val inst = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_vars thm')) cts; in Thm.instantiate ([], inst) thm' end; (* implicit generalization over variables -- canonical order *) fun forall_intr_vars th = - let - val (_, vars) = - (th, (Vars.empty, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Var - (fn ct => fn (seen, vars) => - let val v = Term.dest_Var (Thm.term_of ct) in - if not (Vars.defined seen v) - then (Vars.add_set v seen, ct :: vars) - else (seen, vars) - end); - in fold Thm.forall_intr vars th end; + let val vars = Cterms.build (Thm.fold_atomic_cterms {hyps = false} Term.is_Var Cterms.add_set th) + in fold_rev Thm.forall_intr (Cterms.list_set vars) th end; fun forall_intr_frees th = let val fixed = Frees.build (fold Frees.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #> fold Frees.add_frees (Thm.hyps_of th)); - val (_, frees) = - (th, (fixed, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Free - (fn ct => fn (seen, frees) => - let val v = Term.dest_Free (Thm.term_of ct) in - if not (Frees.defined seen v) - then (Frees.add_set v seen, ct :: frees) - else (seen, frees) - end); - in fold Thm.forall_intr frees th end; + val is_fixed = Frees.defined fixed o Term.dest_Free o Thm.term_of; + val frees = + Cterms.build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Free + (fn ct => not (is_fixed ct) ? Cterms.add_set ct)); + in fold_rev Thm.forall_intr (Cterms.list_set 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 = TVars.build (prop |> (Term.fold_types o Term.fold_atyps) (fn T => fn instT => (case T of TVar (v as ((a, _), S)) => if TVars.defined instT v then instT else TVars.add (v, TFree (a, S)) instT | _ => instT))); val cinstT = TVars.map (K certT) instT; val cinst = 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 Vars.add (((x, i), T'), cert (Free ((x, T')))) inst end | _ => inst))); in Thm.instantiate (TVars.dest cinstT, 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; diff --git a/src/Pure/term_ord.ML b/src/Pure/term_ord.ML --- a/src/Pure/term_ord.ML +++ b/src/Pure/term_ord.ML @@ -1,370 +1,390 @@ (* Title: Pure/term_ord.ML Author: Tobias Nipkow, TU Muenchen Author: Makarius Term orderings and scalable collections. *) signature ITEMS = sig type key type 'a table val empty: 'a table val build: ('a table -> 'a table) -> 'a table + val size: 'a table -> int val is_empty: 'a table -> bool val map: (key -> 'a -> 'b) -> 'a table -> 'b table val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a - val size: 'a table -> int val dest: 'a table -> (key * 'a) list val keys: 'a table -> key list val exists: (key * 'a -> bool) -> 'a table -> bool val forall: (key * 'a -> bool) -> 'a table -> bool val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option val lookup: 'a table -> key -> 'a option val defined: 'a table -> key -> bool val add: key * 'a -> 'a table -> 'a table val make: (key * 'a) list -> 'a table - type set = unit table + type set = int table val add_set: key -> set -> set val make_set: key list -> set + val list_set: set -> key list + val list_set_rev: set -> key list val subset: set * set -> bool val eq_set: set * set -> bool end; functor Items(Key: KEY): ITEMS = struct +(* table with length *) + structure Table = Table(Key); type key = Table.key; -type 'a table = 'a Table.table; +datatype 'a table = Items of int * 'a Table.table; -val empty = Table.empty; -val build = Table.build; -val is_empty = Table.is_empty; -val size = Table.size; -val dest = Table.dest; -val keys = Table.keys; -val exists = Table.exists; -val forall = Table.forall; -val get_first = Table.get_first; -val lookup = Table.lookup; -val defined = Table.defined; +fun size (Items (n, _)) = n; +fun table (Items (_, tab)) = tab; -fun add entry = Table.insert (K true) entry; -fun make entries = Table.build (fold add entries); +val empty = Items (0, Table.empty); +fun build (f: 'a table -> 'a table) = f empty; +fun is_empty items = size items = 0; -type set = unit table; +fun dest items = Table.dest (table items); +fun keys items = Table.keys (table items); +fun exists pred = Table.exists pred o table; +fun forall pred = Table.forall pred o table; +fun get_first get = Table.get_first get o table; +fun lookup items = Table.lookup (table items); +fun defined items = Table.defined (table items); -fun add_set x = add (x, ()); +fun add (key, x) (items as Items (n, tab)) = + if Table.defined tab key then items + else Items (n + 1, Table.update_new (key, x) tab); + +fun make entries = build (fold add entries); + + +(* set with order of addition *) + +type set = int table; + +fun add_set x (items as Items (n, tab)) = + if Table.defined tab x then items + else Items (n + 1, Table.update_new (x, n) tab); + fun make_set xs = build (fold add_set xs); fun subset (A: set, B: set) = forall (defined B o #1) A; fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B); -val map = Table.map; -val fold = Table.fold; -val fold_rev = Table.fold_rev; +fun list_set_ord ord items = Table.dest (table items) |> sort (ord o apply2 #2) |> map #1 +val list_set = list_set_ord int_ord; +val list_set_rev = list_set_ord (rev_order o int_ord); + +fun map f (Items (n, tab)) = Items (n, Table.map f tab); +fun fold f = Table.fold f o table; +fun fold_rev f = Table.fold_rev f o table; end; signature BASIC_TERM_ORD = sig structure Vartab: TABLE structure Sorttab: TABLE structure Typtab: TABLE structure Termtab: TABLE structure Var_Graph: GRAPH structure Sort_Graph: GRAPH structure Typ_Graph: GRAPH structure Term_Graph: GRAPH structure TFrees: sig include ITEMS val add_tfreesT: typ -> set -> set val add_tfrees: term -> set -> set end structure TVars: sig include ITEMS val add_tvarsT: typ -> set -> set val add_tvars: term -> set -> set end structure Frees: sig include ITEMS val add_frees: term -> set -> set end structure Vars: sig include ITEMS val add_vars: term -> set -> set end structure Names: sig include ITEMS val add_tfree_namesT: typ -> set -> set val add_tfree_names: term -> set -> set val add_free_names: term -> set -> set end end; signature TERM_ORD = sig include BASIC_TERM_ORD val fast_indexname_ord: indexname ord val sort_ord: sort ord val typ_ord: typ ord val fast_term_ord: term ord val syntax_term_ord: term ord val indexname_ord: indexname ord val tvar_ord: (indexname * sort) ord val var_ord: (indexname * typ) ord val term_ord: term ord val hd_ord: term ord val term_lpo: (term -> int) -> term ord val term_cache: (term -> 'a) -> term -> 'a end; structure Term_Ord: TERM_ORD = struct (* fast syntactic ordering -- tuned for inequalities *) val fast_indexname_ord = pointer_eq_ord (int_ord o apply2 snd ||| fast_string_ord o apply2 fst); val sort_ord = pointer_eq_ord (dict_ord fast_string_ord); local fun cons_nr (TVar _) = 0 | cons_nr (TFree _) = 1 | cons_nr (Type _) = 2; in fun typ_ord TU = if pointer_eq TU then EQUAL else (case TU of (Type (a, Ts), Type (b, Us)) => (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord) | (TFree (a, S), TFree (b, S')) => (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord) | (TVar (xi, S), TVar (yj, S')) => (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord) | (T, U) => int_ord (cons_nr T, cons_nr U)); end; local fun cons_nr (Const _) = 0 | cons_nr (Free _) = 1 | cons_nr (Var _) = 2 | cons_nr (Bound _) = 3 | cons_nr (Abs _) = 4 | cons_nr (_ $ _) = 5; fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u) | struct_ord (t1 $ t2, u1 $ u2) = (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord) | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u); fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u) | atoms_ord (t1 $ t2, u1 $ u2) = (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord) | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b) | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y) | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj) | atoms_ord (Bound i, Bound j) = int_ord (i, j) | atoms_ord _ = EQUAL; fun types_ord (Abs (_, T, t), Abs (_, U, u)) = (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord) | types_ord (t1 $ t2, u1 $ u2) = (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord) | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U) | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U) | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U) | types_ord _ = EQUAL; fun comments_ord (Abs (x, _, t), Abs (y, _, u)) = (case fast_string_ord (x, y) of EQUAL => comments_ord (t, u) | ord => ord) | comments_ord (t1 $ t2, u1 $ u2) = (case comments_ord (t1, u1) of EQUAL => comments_ord (t2, u2) | ord => ord) | comments_ord _ = EQUAL; in val fast_term_ord = pointer_eq_ord (struct_ord ||| atoms_ord ||| types_ord); val syntax_term_ord = fast_term_ord ||| comments_ord; end; (* term_ord *) (*a linear well-founded AC-compatible ordering for terms: s < t <=> 1. size(s) < size(t) or 2. size(s) = size(t) and s=f(...) and t=g(...) and f (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord) | (t, u) => (case int_ord (size_of_term t, size_of_term u) of EQUAL => (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of EQUAL => args_ord (t, u) | ord => ord) | ord => ord)) and hd_ord (f, g) = prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g) and args_ord (f $ t, g $ u) = (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord) | args_ord _ = EQUAL; end; (* Lexicographic path order on terms *) (* See Baader & Nipkow, Term rewriting, CUP 1998. Without variables. Const, Var, Bound, Free and Abs are treated all as constants. f_ord maps terms to integers and serves two purposes: - Predicate on constant symbols. Those that are not recognised by f_ord must be mapped to ~1. - Order on the recognised symbols. These must be mapped to distinct integers >= 0. The argument of f_ord is never an application. *) local fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0) | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0) | unrecognized (Var v) = ((1, v), 1) | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2) | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3); fun dest_hd f_ord t = let val ord = f_ord t in if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) end; fun term_lpo f_ord (s, t) = let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in if forall (fn si => term_lpo f_ord (si, t) = LESS) ss then case hd_ord f_ord (f, g) of GREATER => if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts then GREATER else LESS | EQUAL => if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts then list_ord (term_lpo f_ord) (ss, ts) else LESS | LESS => LESS else GREATER end and hd_ord f_ord (f, g) = case (f, g) of (Abs (_, T, t), Abs (_, U, u)) => (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord) | (_, _) => prod_ord (prod_ord int_ord (prod_ord indexname_ord typ_ord)) int_ord (dest_hd f_ord f, dest_hd f_ord g); in val term_lpo = term_lpo end; (* scalable collections *) structure Vartab = Table(type key = indexname val ord = fast_indexname_ord); structure Sorttab = Table(type key = sort val ord = sort_ord); structure Typtab = Table(type key = typ val ord = typ_ord); structure Termtab = Table(type key = term val ord = fast_term_ord); fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f; structure Var_Graph = Graph(type key = indexname val ord = fast_indexname_ord); structure Sort_Graph = Graph(type key = sort val ord = sort_ord); structure Typ_Graph = Graph(type key = typ val ord = typ_ord); structure Term_Graph = Graph(type key = term val ord = fast_term_ord); structure TFrees = struct structure Items = Items(type key = string * sort val ord = pointer_eq_ord (prod_ord fast_string_ord sort_ord)); open Items; val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I); val add_tfrees = fold_types add_tfreesT; end; structure TVars = struct structure Items = Items(type key = indexname * sort val ord = pointer_eq_ord (prod_ord fast_indexname_ord sort_ord)); open Items; val add_tvarsT = fold_atyps (fn TVar v => add_set v | _ => I); val add_tvars = fold_types add_tvarsT; end; structure Frees = struct structure Items = Items(type key = string * typ val ord = pointer_eq_ord (prod_ord fast_string_ord typ_ord)); open Items; val add_frees = fold_aterms (fn Free v => add_set v | _ => I); end; structure Vars = struct structure Items = Items(type key = indexname * typ val ord = pointer_eq_ord (prod_ord fast_indexname_ord typ_ord)); open Items; val add_vars = fold_aterms (fn Var v => add_set v | _ => I); end; structure Names = struct structure Items = Items(type key = string val ord = fast_string_ord); open Items; val add_tfree_namesT = fold_atyps (fn TFree (a, _) => add_set a | _ => I); val add_tfree_names = fold_types add_tfree_namesT; val add_free_names = fold_aterms (fn Free (x, _) => add_set x | _ => I); end; end; structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord; open Basic_Term_Ord; diff --git a/src/Tools/misc_legacy.ML b/src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML +++ b/src/Tools/misc_legacy.ML @@ -1,267 +1,258 @@ (* Title: Tools/misc_legacy.ML Misc legacy stuff -- to be phased out eventually. *) signature MISC_LEGACY = sig - val thm_frees: thm -> cterm list - val cterm_frees: cterm -> cterm list + val thm_frees: thm -> Cterms.set + val cterm_frees: cterm -> Cterms.set val add_term_names: term * string list -> string list val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list val add_term_tfrees: term * (string * sort) list -> (string * sort) list val typ_tvars: typ -> (indexname * sort) list val term_tfrees: term -> (string * sort) list val term_tvars: term -> (indexname * sort) list val add_term_vars: term * term list -> term list val term_vars: term -> term list val add_term_frees: term * term list -> term list val term_frees: term -> term list val mk_defpair: term * term -> string * term val get_def: theory -> xstring -> thm val METAHYPS: Proof.context -> (thm list -> tactic) -> int -> tactic val freeze_thaw_robust: Proof.context -> thm -> thm * (int -> thm -> thm) end; structure Misc_Legacy: MISC_LEGACY = struct -fun thm_frees th = - (th, (Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} Term.is_Free - (fn ct => fn (set, list) => - let val v = Term.dest_Free (Thm.term_of ct) in - if not (Frees.defined set v) - then (Frees.add_set v set, ct :: list) - else (set, list) - end) - |> #2; - +val thm_frees = Cterms.build o Thm.fold_atomic_cterms {hyps = true} Term.is_Free Cterms.add_set; val cterm_frees = thm_frees o Drule.mk_term; (*iterate a function over all types in a term*) fun it_term_types f = let fun iter(Const(_,T), a) = f(T,a) | iter(Free(_,T), a) = f(T,a) | iter(Var(_,T), a) = f(T,a) | iter(Abs(_,T,t), a) = iter(t,f(T,a)) | iter(f$u, a) = iter(f, iter(u, a)) | iter(Bound _, a) = a in iter end (*Accumulates the names in the term, suppressing duplicates. Includes Frees and Consts. For choosing unambiguous bound var names.*) fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs | add_term_names (Free(a,_), bs) = insert (op =) a bs | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) | add_term_names (_, bs) = bs; (*Accumulates the TVars in a type, suppressing duplicates.*) fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts | add_typ_tvars(TFree(_),vs) = vs | add_typ_tvars(TVar(v),vs) = insert (op =) v vs; (*Accumulates the TFrees in a type, suppressing duplicates.*) fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs | add_typ_tfree_names(TVar(_),fs) = fs; fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs | add_typ_tfrees(TVar(_),fs) = fs; (*Accumulates the TVars in a term, suppressing duplicates.*) val add_term_tvars = it_term_types add_typ_tvars; (*Accumulates the TFrees in a term, suppressing duplicates.*) val add_term_tfrees = it_term_types add_typ_tfrees; val add_term_tfree_names = it_term_types add_typ_tfree_names; (*Non-list versions*) fun typ_tfrees T = add_typ_tfrees(T,[]); fun typ_tvars T = add_typ_tvars(T,[]); fun term_tfrees t = add_term_tfrees(t,[]); fun term_tvars t = add_term_tvars(t,[]); (*Accumulates the Vars in the term, suppressing duplicates.*) fun add_term_vars (t, vars: term list) = case t of Var _ => Ord_List.insert Term_Ord.term_ord t vars | Abs (_,_,body) => add_term_vars(body,vars) | f$t => add_term_vars (f, add_term_vars(t, vars)) | _ => vars; fun term_vars t = add_term_vars(t,[]); (*Accumulates the Frees in the term, suppressing duplicates.*) fun add_term_frees (t, frees: term list) = case t of Free _ => Ord_List.insert Term_Ord.term_ord t frees | Abs (_,_,body) => add_term_frees(body,frees) | f$t => add_term_frees (f, add_term_frees(t, frees)) | _ => frees; fun term_frees t = add_term_frees(t,[]); fun mk_defpair (lhs, rhs) = (case Term.head_of lhs of Const (name, _) => (Thm.def_name (Long_Name.base_name name), Logic.mk_equals (lhs, rhs)) | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name; (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions METAHYPS (fn prems => tac prems) i converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new proof state A==>A, supplying A1,...,An as meta-level assumptions (in "prems"). The parameters x1,...,xm become free variables. If the resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An) then it is lifted back into the original context, yielding k subgoals. Replaces unknowns in the context by Frees having the prefix METAHYP_ New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm. DOES NOT HANDLE TYPE UNKNOWNS. NOTE: This version does not observe the proof context, and thus cannot work reliably. See also Subgoal.SUBPROOF and Subgoal.FOCUS for properly localized variants of the same idea. ****) local (*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. Main difference from strip_assums concerns parameters: it replaces the bound variables by free variables. *) fun strip_context_aux (params, Hs, Const (\<^const_name>\Pure.imp\, _) $ H $ B) = strip_context_aux (params, H :: Hs, B) | strip_context_aux (params, Hs, Const (\<^const_name>\Pure.all\,_) $ Abs (a, T, t)) = let val (b, u) = Syntax_Trans.variant_abs (a, T, t) in strip_context_aux ((b, T) :: params, Hs, u) end | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); fun strip_context A = strip_context_aux ([], [], A); (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. Instantiates distinct free variables by terms of same type.*) fun free_instantiate ctpairs = forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); fun free_of s ((a, i), T) = Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T) fun mk_inst v = (Var v, free_of "METAHYP1_" v) fun metahyps_split_prem prem = let (*find all vars in the hyps -- should find tvars also!*) val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) [] val insts = map mk_inst hyps_vars (*replace the hyps_vars by Frees*) val prem' = subst_atomic insts prem val (params,hyps,concl) = strip_context prem' in (insts,params,hyps,concl) end; fun metahyps_aux_tac ctxt tacf (prem,gno) state = let val (insts,params,hyps,concl) = metahyps_split_prem prem val maxidx = Thm.maxidx_of state val chyps = map (Thm.cterm_of ctxt) hyps val hypths = map Thm.assume chyps val subprems = map (Thm.forall_elim_vars 0) hypths val fparams = map Free params val cparams = map (Thm.cterm_of ctxt) fparams fun swap_ctpair (t, u) = apply2 (Thm.cterm_of ctxt) (u, t) (*Subgoal variables: make Free; lift type over params*) fun mk_subgoal_inst concl_vars (v, T) = if member (op =) concl_vars (v, T) then ((v, T), true, free_of "METAHYP2_" (v, T)) else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T)) (*Instantiate subgoal vars by Free applied to params*) fun mk_inst (v, in_concl, u) = if in_concl then (v, Thm.cterm_of ctxt u) else (v, Thm.cterm_of ctxt (list_comb (u, fparams))) (*Restore Vars with higher type and index*) fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) = if in_concl then apply2 (Thm.cterm_of ctxt) (u, Var ((a, i), T)) else apply2 (Thm.cterm_of ctxt) (u, Var ((a, i + maxidx), U)) (*Embed B in the original context of params and hyps*) fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B)) (*Strip the context using elimination rules*) fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths (*A form of lifting that discharges assumptions.*) fun relift st = let val prop = Thm.prop_of st val subgoal_vars = (*Vars introduced in the subgoals*) fold Term.add_vars (Logic.strip_imp_prems prop) [] and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [] val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars val st' = Thm.instantiate ([], map mk_inst subgoal_insts) st val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st') val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs) in (*restore the unknowns to the hypotheses*) free_instantiate (map swap_ctpair insts @ map mk_subgoal_swap_ctpair subgoal_insts) (*discharge assumptions from state in same order*) (implies_intr_list emBs (forall_intr_list cparams (implies_intr_list chyps Cth))) end (*function to replace the current subgoal*) fun next st = Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} (false, relift st, Thm.nprems_of st) gno state in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end; in fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm handle THM ("assume: variables", _, _) => Seq.empty end; (* generating identifiers -- often fresh *) local (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*) fun gensym_char i = if i<26 then chr (ord "A" + i) else if i<52 then chr (ord "a" + i - 26) else chr (ord "0" + i - 52); val char_vec = Vector.tabulate (62, gensym_char); fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n))); val gensym_seed = Synchronized.var "gensym_seed" (0: int); in fun gensym pre = Synchronized.change_result gensym_seed (fn i => (pre ^ newid i, i + 1)); end; (*Convert all Vars in a theorem to Frees. Also return a function for reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*) fun freeze_thaw_robust ctxt th = let val fth = Thm.legacy_freezeT th in case Thm.fold_terms {hyps = false} Term.add_vars fth [] of [] => (fth, fn _ => fn x => x) (*No vars: nothing to do!*) | vars => let fun newName (ix,_) = (ix, gensym (string_of_indexname ix)) val alist = map newName vars fun mk_inst (v,T) = apply2 (Thm.cterm_of ctxt) (Var (v, T), Free (the (AList.lookup (op =) alist v), T)) val insts = map mk_inst vars fun thaw i th' = (*i is non-negative increment for Var indexes*) th' |> forall_intr_list (map #2 insts) |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts) in (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw) end end; end;