diff --git a/src/HOL/Tools/Metis/metis_reconstruct.ML b/src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML @@ -1,758 +1,757 @@ (* Title: HOL/Tools/Metis/metis_reconstruct.ML Author: Kong W. Susanto, Cambridge University Computer Laboratory Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Copyright Cambridge University 2007 Proof reconstruction for Metis. *) signature METIS_RECONSTRUCT = sig type type_enc = ATP_Problem_Generate.type_enc exception METIS_RECONSTRUCT of string * string val hol_clause_of_metis : Proof.context -> type_enc -> int Symtab.table -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a val replay_one_inference : Proof.context -> type_enc -> (string * term) list * (string * term) list -> int Symtab.table -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list -> (Metis_Thm.thm * thm) list val discharge_skolem_premises : Proof.context -> (thm * term) option list -> thm -> thm end; structure Metis_Reconstruct : METIS_RECONSTRUCT = struct open ATP_Problem open ATP_Problem_Generate open ATP_Proof_Reconstruct open Metis_Generate exception METIS_RECONSTRUCT of string * string val meta_not_not = @{thms not_not[THEN eq_reflection]} fun atp_name_of_metis type_enc s = (case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of SOME ((s, _), (_, swap)) => (s, swap) | _ => (s, false)) fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) = let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev) end | atp_term_of_metis _ (Metis_Term.Var s) = ATerm ((Metis_Name.toString s, []), []) fun hol_term_of_metis ctxt type_enc sym_tab = atp_term_of_metis type_enc #> term_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab NONE fun atp_literal_of_metis type_enc (pos, atom) = atom |> Metis_Term.Fn |> atp_term_of_metis type_enc |> AAtom |> not pos ? mk_anot fun atp_clause_of_metis _ [] = AAtom (ATerm ((tptp_false, []), [])) | atp_clause_of_metis type_enc lits = lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr fun polish_hol_terms ctxt (lifted, old_skolems) = map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems) #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) fun hol_clause_of_metis ctxt type_enc sym_tab concealed = Metis_Thm.clause #> Metis_LiteralSet.toList #> atp_clause_of_metis type_enc #> prop_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab #> singleton (polish_hol_terms ctxt concealed) fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms = let val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms val _ = trace_msg ctxt (fn () => " calling type inference:") val _ = List.app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts val ts' = ts |> polish_hol_terms ctxt concealed val _ = List.app (fn t => trace_msg ctxt (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ " of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts' in ts' end (** FOL step Inference Rules **) fun lookth th_pairs fol_th = (case AList.lookup (uncurry Metis_Thm.equal) th_pairs fol_th of SOME th => th | NONE => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fol_th)) fun cterm_incr_types ctxt idx = Thm.cterm_of ctxt o map_types (Logic.incr_tvar idx) (* INFERENCE RULE: AXIOM *) (*This causes variables to have an index of 1 by default. See also "term_of_atp" in "ATP_Proof_Reconstruct".*) val axiom_inference = Thm.incr_indexes 1 oo lookth (* INFERENCE RULE: ASSUME *) -fun inst_excluded_middle i_atom = - @{lemma "P \ \ P \ False" by (rule notE)} - |> instantiate_normalize (TVars.empty, Vars.make [(\<^var>\?P::bool\, i_atom)]) +fun excluded_middle P = + \<^instantiate>\P in lemma (open) \P \ \ P \ False\ by (rule notE)\ fun assume_inference ctxt type_enc concealed sym_tab atom = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom) - |> Thm.cterm_of ctxt |> inst_excluded_middle + |> Thm.cterm_of ctxt |> excluded_middle (* INFERENCE RULE: INSTANTIATE (SUBST). *) (*Type instantiations are ignored. Trying to reconstruct them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange hat new TVars are distinct and that types can be inferred from terms.*) fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th = let val i_th = lookth th_pairs th val i_th_vars = Term.add_vars (Thm.prop_of i_th) [] fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) fun subst_translation (x,y) = let val v = find_var x (*We call "polish_hol_terms" below.*) val t = hol_term_of_metis ctxt type_enc sym_tab y in SOME (Thm.cterm_of ctxt (Var v), t) end handle Option.Option => (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th); NONE) | TYPE _ => (trace_msg ctxt (fn () => "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th); NONE) fun remove_typeinst (a, t) = let val a = Metis_Name.toString a in (case unprefix_and_unascii schematic_var_prefix a of SOME b => SOME (b, t) | NONE => (case unprefix_and_unascii tvar_prefix a of SOME _ => NONE (*type instantiations are forbidden*) | NONE => SOME (a, t) (*internal Metis var?*))) end val _ = trace_msg ctxt (fn () => " isa th: " ^ Thm.string_of_thm ctxt i_th) val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) val (vars, tms) = ListPair.unzip (map_filter subst_translation substs) ||> polish_hol_terms ctxt concealed val ctm_of = cterm_incr_types ctxt (Thm.maxidx_of i_th + 1) val substs' = ListPair.zip (vars, map ctm_of tms) val _ = trace_msg ctxt (fn () => cat_lines ("subst_translations:" :: (substs' |> map (fn (x, y) => Syntax.string_of_term ctxt (Thm.term_of x) ^ " |-> " ^ Syntax.string_of_term ctxt (Thm.term_of y))))) in infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) substs') i_th end handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg) | ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg) (* INFERENCE RULE: RESOLVE *) (*Increment the indexes of only the type variables*) fun incr_type_indexes ctxt inc th = let val tvs = Term.add_tvars (Thm.full_prop_of th) [] fun inc_tvar ((a, i), s) = (((a, i), s), Thm.ctyp_of ctxt (TVar ((a, i + inc), s))) in Thm.instantiate (TVars.make (map inc_tvar tvs), Vars.empty) th end (*Like RSN, but we rename apart only the type variables. Vars here typically have an index of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars could then fail.*) fun resolve_inc_tyvars ctxt th1 i th2 = let val th1' = incr_type_indexes ctxt (Thm.maxidx_of th2 + 1) th1 fun res (tha, thb) = (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true} (false, Thm.close_derivation \<^here> tha, Thm.nprems_of tha) i thb |> Seq.list_of |> distinct Thm.eq_thm of [th] => th | _ => let val thaa'bb' as [(tha', _), (thb', _)] = map (`(Local_Defs.unfold0 ctxt meta_not_not)) [tha, thb] in if forall Thm.eq_thm_prop thaa'bb' then raise THM ("resolve_inc_tyvars: unique result expected", i, [tha, thb]) else res (tha', thb') end) in res (th1', th2) handle TERM z => let val ps = [] |> fold (Term.add_vars o Thm.prop_of) [th1', th2] |> AList.group (op =) |> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts) |> rpair Envir.init |-> fold (Pattern.unify (Context.Proof ctxt)) |> Envir.type_env |> Vartab.dest |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T)) in (*The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as first argument). We then perform unification of the types of variables by hand and try again. We could do this the first time around but this error occurs seldom and we don't want to break existing proofs in subtle ways or slow them down.*) if null ps then raise TERM z else res (apply2 (Drule.instantiate_normalize (TVars.make ps, Vars.empty)) (th1', th2)) end end fun s_not \<^Const_>\Not for t\ = t | s_not t = HOLogic.mk_not t fun simp_not_not \<^Const_>\Trueprop for t\ = \<^Const>\Trueprop for \simp_not_not t\\ | simp_not_not \<^Const_>\Not for t\ = s_not (simp_not_not t) | simp_not_not t = t val normalize_literal = simp_not_not o Envir.eta_contract (*Find the relative location of an untyped term within a list of terms as a 1-based index. Returns 0 in case of failure.*) fun index_of_literal lit haystack = let fun match_lit normalize = HOLogic.dest_Trueprop #> normalize #> curry Term.aconv_untyped (lit |> normalize) in (case find_index (match_lit I) haystack of ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack | j => j) + 1 end (*Permute a rule's premises to move the i-th premise to the last position.*) fun make_last i th = let val n = Thm.nprems_of th in if i >= 1 andalso i <= n then Thm.permute_prems (i - 1) 1 th else raise THM ("select_literal", i, [th]) end (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding to create double negations. The "select" wrapper is a trick to ensure that "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We don't use this trick in general because it makes the proof object uglier than necessary. FIXME.*) fun negate_head ctxt th = if exists (fn t => t aconv \<^prop>\\ False\) (Thm.prems_of th) then (th RS @{thm select_FalseI}) |> fold (rewrite_rule ctxt o single) @{thms not_atomize_select atomize_not_select} else th |> fold (rewrite_rule ctxt o single) @{thms not_atomize atomize_not} (* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) fun select_literal ctxt = negate_head ctxt oo make_last fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 = let val (i_th1, i_th2) = apply2 (lookth th_pairs) (th1, th2) val _ = trace_msg ctxt (fn () => " isa th1 (pos): " ^ Thm.string_of_thm ctxt i_th1 ^ "\n\ \ isa th2 (neg): " ^ Thm.string_of_thm ctxt i_th2) in (* Trivial cases where one operand is type info *) if Thm.eq_thm (TrueI, i_th1) then i_th2 else if Thm.eq_thm (TrueI, i_th2) then i_th1 else let val i_atom = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom) val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atom) in (case index_of_literal (s_not i_atom) (Thm.prems_of i_th1) of 0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th1\""); i_th1) | j1 => (trace_msg ctxt (fn () => " index th1: " ^ string_of_int j1); (case index_of_literal i_atom (Thm.prems_of i_th2) of 0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th2\""); i_th2) | j2 => (trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2); resolve_inc_tyvars ctxt (select_literal ctxt j1 i_th1) j2 i_th2 handle TERM (s, _) => raise METIS_RECONSTRUCT ("resolve_inference", s))))) end end (* INFERENCE RULE: REFL *) val REFL_THM = Thm.incr_indexes 2 @{lemma "x \ x \ False" by (drule notE) (rule refl)} val [refl_x] = Term.add_vars (Thm.prop_of REFL_THM) []; fun refl_inference ctxt type_enc concealed sym_tab t = let val i_t = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) val c_t = cterm_incr_types ctxt (Thm.maxidx_of REFL_THM + 1) i_t in infer_instantiate_types ctxt [(refl_x, c_t)] REFL_THM end (* INFERENCE RULE: EQUALITY *) val subst_em = @{lemma "s = t \ P s \ \ P t \ False" by (erule notE) (erule subst)} val ssubst_em = @{lemma "s = t \ P t \ \ P s \ False" by (erule notE) (erule ssubst)} fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr = let val m_tm = Metis_Term.Fn atom val [i_atom, i_tm] = hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr] val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos) fun replace_item_list lx 0 (_::ls) = lx::ls | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls fun path_finder_fail tm ps t = raise METIS_RECONSTRUCT ("equality_inference (path_finder)", "path = " ^ space_implode " " (map string_of_int ps) ^ " isa-term: " ^ Syntax.string_of_term ctxt tm ^ (case t of SOME t => " fol-term: " ^ Metis_Term.toString t | NONE => "")) fun path_finder tm [] _ = (tm, Bound 0) | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) = let val s = s |> Metis_Name.toString |> perhaps (try (unprefix_and_unascii const_prefix #> the #> unmangled_const_name #> hd)) in if s = metis_predicator orelse s = predicator_name orelse s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag orelse s = type_tag_name then path_finder tm ps (nth ts p) else if s = metis_app_op orelse s = app_op_name then let val (tm1, tm2) = dest_comb tm val p' = p - (length ts - 2) in if p' = 0 then path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2) else path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y) end else let val (tm1, args) = strip_comb tm val adjustment = length ts - length args val p' = if adjustment > p then p else p - adjustment val tm_p = nth args p' handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t) val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^ " " ^ Syntax.string_of_term ctxt tm_p) val (r, t) = path_finder tm_p ps (nth ts p) in (r, list_comb (tm1, replace_item_list t p' args)) end end | path_finder tm ps t = path_finder_fail tm ps (SOME t) val (tm_subst, body) = path_finder i_atom fp m_tm val tm_abs = Abs ("x", type_of tm_subst, body) val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) val maxidx = fold Term.maxidx_term [i_tm, tm_abs, tm_subst] ~1 val subst' = Thm.incr_indexes (maxidx + 1) (if pos then subst_em else ssubst_em) val _ = trace_msg ctxt (fn () => "subst' " ^ Thm.string_of_thm ctxt subst') val eq_terms = map (apply2 (Thm.cterm_of ctxt)) (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm])) in infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) eq_terms) subst' end val factor = Seq.hd o distinct_subgoals_tac fun one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inference) = (case inference of Metis_Proof.Axiom _ => axiom_inference th_pairs fol_th |> factor | Metis_Proof.Assume atom => assume_inference ctxt type_enc concealed sym_tab atom | Metis_Proof.Metis_Subst (subst, th1) => inst_inference ctxt type_enc concealed sym_tab th_pairs subst th1 |> factor | Metis_Proof.Resolve (atom, th1, th2) => resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 |> factor | Metis_Proof.Refl tm => refl_inference ctxt type_enc concealed sym_tab tm | Metis_Proof.Equality (lit, p, r) => equality_inference ctxt type_enc concealed sym_tab lit p r) fun flexflex_first_order ctxt th = (case Thm.tpairs_of th of [] => th | pairs => let val thy = Proof_Context.theory_of ctxt val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) fun mkT (v, (S, T)) = ((v, S), Thm.ctyp_of ctxt T) fun mk (v, (T, t)) = ((v, Envir.subst_type tyenv T), Thm.cterm_of ctxt t) val instsT = Vartab.fold (cons o mkT) tyenv [] val insts = Vartab.fold (cons o mk) tenv [] in Thm.instantiate (TVars.make instsT, Vars.make insts) th end handle THM _ => th) fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix (Metis_Name.toString s)) fun is_isabelle_literal_genuine t = (case t of _ $ \<^Const_>\Meson.skolem _ for _\ => false | _ => true) fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0 (*Seldomly needed hack. A Metis clause is represented as a set, so duplicate disjuncts are impossible. In the Isabelle proof, in spite of efforts to eliminate them, duplicates sometimes appear with slightly different (but unifiable) types.*) fun resynchronize ctxt fol_th th = let val num_metis_lits = count is_metis_literal_genuine (Metis_LiteralSet.toList (Metis_Thm.clause fol_th)) val num_isabelle_lits = count is_isabelle_literal_genuine (Thm.prems_of th) in if num_metis_lits >= num_isabelle_lits then th else let val (prems0, concl) = th |> Thm.prop_of |> Logic.strip_horn val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped val goal = Logic.list_implies (prems, concl) val ctxt' = fold Thm.declare_hyps (Thm.chyps_of th) ctxt val tac = cut_tac th 1 THEN rewrite_goals_tac ctxt' meta_not_not THEN ALLGOALS (assume_tac ctxt') in if length prems = length prems0 then raise METIS_RECONSTRUCT ("resynchronize", "Out of sync") else Goal.prove ctxt' [] [] goal (K tac) |> resynchronize ctxt' fol_th end end fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf) th_pairs = if not (null th_pairs) andalso Thm.prop_of (snd (hd th_pairs)) aconv \<^prop>\False\ then (*Isabelle sometimes identifies literals (premises) that are distinct in Metis (e.g., because of type variables). We give the Isabelle proof the benefice of the doubt.*) th_pairs else let val _ = trace_msg ctxt (fn () => "=============================================") val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf) |> flexflex_first_order ctxt |> resynchronize ctxt fol_th val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Thm.string_of_thm ctxt th) val _ = trace_msg ctxt (fn () => "=============================================") in (fol_th, th) :: th_pairs end (*It is normally sufficient to apply "assume_tac" to unify the conclusion with one of the premises. Unfortunately, this sometimes yields "Variable has two distinct types" errors. To avoid this, we instantiate the variables before applying "assume_tac". Typical constraints are of the form ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z \\<^sup>? SK_a_b_c_x, where the nonvariables are goal parameters.*) fun unify_first_prem_with_concl ctxt i th = let val goal = Logic.get_goal (Thm.prop_of th) i |> Envir.beta_eta_contract val prem = goal |> Logic.strip_assums_hyp |> hd val concl = goal |> Logic.strip_assums_concl fun pair_untyped_aconv (t1, t2) (u1, u2) = Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2) fun add_terms tp inst = if exists (pair_untyped_aconv tp) inst then inst else tp :: map (apsnd (subst_atomic [tp])) inst fun is_flex t = (case strip_comb t of (Var _, args) => forall is_Bound args | _ => false) fun unify_flex flex rigid = (case strip_comb flex of (Var (z as (_, T)), args) => add_terms (Var z, fold_rev absdummy (take (length args) (binder_types T)) rigid) | _ => I) fun unify_potential_flex comb atom = if is_flex comb then unify_flex comb atom else if is_Var atom then add_terms (atom, comb) else I fun unify_terms (t, u) = (case (t, u) of (t1 $ t2, u1 $ u2) => if is_flex t then unify_flex t u else if is_flex u then unify_flex u t else fold unify_terms [(t1, u1), (t2, u2)] | (_ $ _, _) => unify_potential_flex t u | (_, _ $ _) => unify_potential_flex u t | (Var _, _) => add_terms (t, u) | (_, Var _) => add_terms (u, t) | _ => I) val t_inst = [] |> try (unify_terms (prem, concl) #> map (apply2 (Thm.cterm_of ctxt))) |> the_default [] (* FIXME *) in infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) t_inst) th end val copy_prem = @{lemma "P \ (P \ P \ Q) \ Q" by assumption} fun copy_prems_tac ctxt [] ns i = if forall (curry (op =) 1) ns then all_tac else copy_prems_tac ctxt (rev ns) [] i | copy_prems_tac ctxt (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ctxt ms (1 :: ns) i | copy_prems_tac ctxt (m :: ms) ns i = eresolve_tac ctxt [copy_prem] i THEN copy_prems_tac ctxt ms (m div 2 :: (m + 1) div 2 :: ns) i (*Metis generates variables of the form _nnn.*) val is_metis_fresh_variable = String.isPrefix "_" fun instantiate_forall_tac ctxt t i st = let val params = Logic.strip_params (Logic.get_goal (Thm.prop_of st) i) |> rev fun repair (t as (Var ((s, _), _))) = (case find_index (fn (s', _) => s' = s) params of ~1 => t | j => Bound j) | repair (t $ u) = (case (repair t, repair u) of (t as Bound j, u as Bound k) => (*This is a trick to repair the discrepancy between the fully skolemized term that MESON gives us (where existentials were pulled out) and the reality.*) if k > j then t else t $ u | (t, u) => t $ u) | repair t = t val t' = t |> repair |> fold (absdummy o snd) params fun do_instantiate th = (case Term.add_vars (Thm.prop_of th) [] |> filter_out ((Meson_Clausify.is_zapped_var_name orf is_metis_fresh_variable) o fst o fst) of [] => th | [var as (_, T)] => let val var_binder_Ts = T |> binder_types |> take (length params) |> rev val var_body_T = T |> funpow (length params) range_type val tyenv = Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params, var_body_T :: var_binder_Ts) val env = Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0, tenv = Vartab.empty, tyenv = tyenv} val ty_inst = Vartab.fold (fn (x, (S, T)) => cons (((x, S), Thm.ctyp_of ctxt T))) tyenv [] val t_inst = [apply2 (Thm.cterm_of ctxt o Envir.norm_term env) (Var var, t')] in Drule.instantiate_normalize (TVars.make ty_inst, Vars.make (map (apfst (dest_Var o Thm.term_of)) t_inst)) th end | _ => raise Fail "expected a single non-zapped, non-Metis Var") in (DETERM (eresolve_tac ctxt @{thms allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st end fun fix_exists_tac ctxt t = eresolve_tac ctxt [exE] THEN' rename_tac [t |> dest_Var |> fst |> fst] fun release_quantifier_tac ctxt (skolem, t) = (if skolem then fix_exists_tac ctxt else instantiate_forall_tac ctxt) t fun release_clusters_tac _ _ _ [] = K all_tac | release_clusters_tac ctxt ax_counts substs ((ax_no, cluster_no) :: clusters) = let val cluster_of_var = Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no val cluster_substs = substs |> map_filter (fn (ax_no', (_, (_, tsubst))) => if ax_no' = ax_no then tsubst |> map (apfst cluster_of_var) |> filter (in_right_cluster o fst) |> map (apfst snd) |> SOME else NONE) fun do_cluster_subst cluster_subst = map (release_quantifier_tac ctxt) cluster_subst @ [rotate_tac 1] val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs in rotate_tac first_prem THEN' (EVERY' (maps do_cluster_subst cluster_substs)) THEN' rotate_tac (~ first_prem - length cluster_substs) THEN' release_clusters_tac ctxt ax_counts substs clusters end fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) = (ax_no, (cluster_no, (skolem, index_no))) fun cluster_ord p = prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord)) (apply2 cluster_key p) val tysubst_ord = list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord)) structure Int_Tysubst_Table = Table ( type key = int * (indexname * (sort * typ)) list val ord = prod_ord int_ord tysubst_ord ) structure Int_Pair_Graph = Graph( type key = int * int val ord = prod_ord int_ord int_ord ) fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no) fun shuffle_ord p = prod_ord int_ord int_ord (apply2 shuffle_key p) (*Attempts to derive the theorem "False" from a theorem of the form "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the specified axioms. The axioms have leading "All" and "Ex" quantifiers, which must be eliminated first.*) fun discharge_skolem_premises ctxt axioms prems_imp_false = if Thm.prop_of prems_imp_false aconv \<^prop>\False\ then prems_imp_false else let val thy = Proof_Context.theory_of ctxt fun match_term p = let val (tyenv, tenv) = Pattern.first_order_match thy p (Vartab.empty, Vartab.empty) val tsubst = tenv |> Vartab.dest |> filter (Meson_Clausify.is_zapped_var_name o fst o fst) |> sort (cluster_ord o apply2 (Meson_Clausify.cluster_of_zapped_var_name o fst o fst)) |> map (fn (xi, (T, t)) => apply2 (Envir.subst_term_types tyenv) (Var (xi, T), t)) val tysubst = tyenv |> Vartab.dest in (tysubst, tsubst) end fun subst_info_of_prem subgoal_no prem = (case prem of _ $ \<^Const_>\Meson.skolem _ for \_ $ t $ num\\ => let val ax_no = HOLogic.dest_nat num in (ax_no, (subgoal_no, match_term (nth axioms ax_no |> the |> snd, t))) end | _ => raise TERM ("discharge_skolem_premises: Malformed premise", [prem])) fun cluster_of_var_name skolem s = (case try Meson_Clausify.cluster_of_zapped_var_name s of NONE => NONE | SOME ((ax_no, (cluster_no, _)), skolem') => if skolem' = skolem andalso cluster_no > 0 then SOME (ax_no, cluster_no) else NONE) fun clusters_in_term skolem t = Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst) fun deps_of_term_subst (var, t) = (case clusters_in_term false var of [] => NONE | [(ax_no, cluster_no)] => SOME ((ax_no, cluster_no), clusters_in_term true t |> cluster_no > 1 ? cons (ax_no, cluster_no - 1)) | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])) val prems = Logic.strip_imp_prems (Thm.prop_of prems_imp_false) val substs = prems |> map2 subst_info_of_prem (1 upto length prems) |> sort (int_ord o apply2 fst) val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs val clusters = maps (op ::) depss val ordered_clusters = Int_Pair_Graph.empty |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters) |> fold Int_Pair_Graph.add_deps_acyclic depss |> Int_Pair_Graph.topological_order handle Int_Pair_Graph.CYCLES _ => error "Cannot replay Metis proof in Isabelle without \"Hilbert_Choice\"" val ax_counts = Int_Tysubst_Table.empty |> fold (fn (ax_no, (_, (tysubst, _))) => Int_Tysubst_Table.map_default ((ax_no, tysubst), 0) (Integer.add 1)) substs |> Int_Tysubst_Table.dest val needed_axiom_props = 0 upto length axioms - 1 ~~ axioms |> map_filter (fn (_, NONE) => NONE | (ax_no, SOME (_, t)) => if exists (fn ((ax_no', _), n) => ax_no' = ax_no andalso n > 0) ax_counts then SOME t else NONE) val outer_param_names = [] |> fold Term.add_var_names needed_axiom_props |> filter (Meson_Clausify.is_zapped_var_name o fst) |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst)) |> filter (fn (((_, (cluster_no, _)), skolem), _) => cluster_no = 0 andalso skolem) |> sort shuffle_ord |> map (fst o snd) (* for debugging only: fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^ commas (map ((fn (s, t) => s ^ " |-> " ^ t) o apply2 (Syntax.string_of_term ctxt)) tsubst) ^ "}" val _ = tracing ("ORDERED CLUSTERS: " ^ @{make_string} ordered_clusters) val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts) val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names) val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ cat_lines (map string_of_subst_info substs)) *) val ctxt' = fold Thm.declare_hyps (Thm.chyps_of prems_imp_false) ctxt fun cut_and_ex_tac axiom = cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac ctxt' @{thms exE}) 1) fun rotation_of_subgoal i = find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs in Goal.prove ctxt' [] [] \<^prop>\False\ (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst o fst) ax_counts) THEN rename_tac outer_param_names 1 THEN copy_prems_tac ctxt' (map snd ax_counts) [] 1) THEN release_clusters_tac ctxt' ax_counts substs ordered_clusters 1 THEN match_tac ctxt' [prems_imp_false] 1 THEN ALLGOALS (fn i => resolve_tac ctxt' @{thms Meson.skolem_COMBK_I} i THEN rotate_tac (rotation_of_subgoal i) i THEN PRIMITIVE (unify_first_prem_with_concl ctxt' i) THEN assume_tac ctxt' i THEN flexflex_tac ctxt'))) handle ERROR msg => cat_error msg "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions" end end; diff --git a/src/HOL/Tools/lin_arith.ML b/src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML +++ b/src/HOL/Tools/lin_arith.ML @@ -1,975 +1,975 @@ (* Title: HOL/Tools/lin_arith.ML Author: Tjark Weber and Tobias Nipkow, TU Muenchen HOL setup for linear arithmetic (see Provers/Arith/fast_lin_arith.ML). *) signature LIN_ARITH = sig val pre_tac: Proof.context -> int -> tactic val simple_tac: Proof.context -> int -> tactic val tac: Proof.context -> int -> tactic val simproc: Proof.context -> cterm -> thm option val add_inj_thms: thm list -> Context.generic -> Context.generic val add_lessD: thm -> Context.generic -> Context.generic val add_simps: thm list -> Context.generic -> Context.generic val add_simprocs: simproc list -> Context.generic -> Context.generic val add_inj_const: string * typ -> Context.generic -> Context.generic val add_discrete_type: string -> Context.generic -> Context.generic val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic val global_setup: theory -> theory val init_arith_data: Context.generic -> Context.generic val split_limit: int Config.T val neq_limit: int Config.T val trace: bool Config.T end; structure Lin_Arith: LIN_ARITH = struct (* Parameters data for general linear arithmetic functor *) structure LA_Logic: LIN_ARITH_LOGIC = struct val ccontr = @{thm ccontr}; val conjI = conjI; val notI = notI; val sym = sym; val trueI = TrueI; val not_lessD = @{thm linorder_not_less} RS iffD1; val not_leD = @{thm linorder_not_le} RS iffD1; fun mk_Eq thm = thm RS @{thm Eq_FalseI} handle THM _ => thm RS @{thm Eq_TrueI}; val mk_Trueprop = HOLogic.mk_Trueprop; fun atomize thm = case Thm.prop_of thm of Const (\<^const_name>\Trueprop\, _) $ (Const (\<^const_name>\HOL.conj\, _) $ _ $ _) => atomize (thm RS conjunct1) @ atomize (thm RS conjunct2) | _ => [thm]; fun neg_prop ((TP as Const(\<^const_name>\Trueprop\, _)) $ (Const (\<^const_name>\Not\, _) $ t)) = TP $ t | neg_prop ((TP as Const(\<^const_name>\Trueprop\, _)) $ t) = TP $ (HOLogic.Not $t) | neg_prop t = raise TERM ("neg_prop", [t]); fun is_False thm = let val _ $ t = Thm.prop_of thm in t = \<^term>\False\ end; fun is_nat t = (fastype_of1 t = HOLogic.natT); fun mk_nat_thm thy t = - let val ct = Thm.global_cterm_of thy t - in Drule.instantiate_normalize (TVars.empty, Vars.make [(\<^var>\?n::nat\, ct)]) @{thm le0} end; + \<^instantiate>\n = \Thm.global_cterm_of thy t\ in + lemma (open) \0 \ n\ for n :: nat by (rule le0)\; end; (* arith context data *) structure Lin_Arith_Data = Generic_Data ( type T = {splits: thm list, inj_consts: (string * typ) list, discrete: string list}; val empty = {splits = [], inj_consts = [], discrete = []}; fun merge ({splits = splits1, inj_consts = inj_consts1, discrete = discrete1}, {splits = splits2, inj_consts = inj_consts2, discrete = discrete2}) : T = {splits = Thm.merge_thms (splits1, splits2), inj_consts = Library.merge (op =) (inj_consts1, inj_consts2), discrete = Library.merge (op =) (discrete1, discrete2)}; ); val get_arith_data = Lin_Arith_Data.get o Context.Proof; fun get_splits ctxt = #splits (get_arith_data ctxt) |> map (Thm.transfer' ctxt); fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} => {splits = update Thm.eq_thm_prop (Thm.trim_context thm) splits, inj_consts = inj_consts, discrete = discrete}); fun add_discrete_type d = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} => {splits = splits, inj_consts = inj_consts, discrete = update (op =) d discrete}); fun add_inj_const c = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} => {splits = splits, inj_consts = update (op =) c inj_consts, discrete = discrete}); val split_limit = Attrib.setup_config_int \<^binding>\linarith_split_limit\ (K 9); val neq_limit = Attrib.setup_config_int \<^binding>\linarith_neq_limit\ (K 9); val trace = Attrib.setup_config_bool \<^binding>\linarith_trace\ (K false); structure LA_Data: LIN_ARITH_DATA = struct val neq_limit = neq_limit; val trace = trace; (* Decomposition of terms *) (*internal representation of linear (in-)equations*) type decomp = ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool); fun nT (Type ("fun", [N, _])) = (N = HOLogic.natT) | nT _ = false; fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) : (term * Rat.rat) list * Rat.rat = case AList.lookup Envir.aeconv p t of NONE => ((t, m) :: p, i) | SOME n => (AList.update Envir.aeconv (t, Rat.add n m) p, i); (* decompose nested multiplications, bracketing them to the right and combining all their coefficients inj_consts: list of constants to be ignored when encountered (e.g. arithmetic type conversions that preserve value) m: multiplicity associated with the entire product returns either (SOME term, associated multiplicity) or (NONE, constant) *) fun of_field_sort thy U = Sign.of_sort thy (U, \<^sort>\inverse\); fun demult thy (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat = let fun demult ((mC as Const (\<^const_name>\Groups.times\, _)) $ s $ t, m) = (case s of Const (\<^const_name>\Groups.times\, _) $ s1 $ s2 => (* bracketing to the right: '(s1 * s2) * t' becomes 's1 * (s2 * t)' *) demult (mC $ s1 $ (mC $ s2 $ t), m) | _ => (* product 's * t', where either factor can be 'NONE' *) (case demult (s, m) of (SOME s', m') => (case demult (t, m') of (SOME t', m'') => (SOME (mC $ s' $ t'), m'') | (NONE, m'') => (SOME s', m'')) | (NONE, m') => demult (t, m'))) | demult (atom as (mC as Const (\<^const_name>\Rings.divide\, T)) $ s $ t, m) = (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ? Note that if we choose to do so here, the simpset used by arith must be able to perform the same simplifications. *) (* quotient 's / t', where the denominator t can be NONE *) (* Note: will raise Div iff m' is @0 *) if of_field_sort thy (domain_type T) then let val (os',m') = demult (s, m); val (ot',p) = demult (t, @1) in (case (os',ot') of (SOME s', SOME t') => SOME (mC $ s' $ t') | (SOME s', NONE) => SOME s' | (NONE, SOME t') => SOME (mC $ Const (\<^const_name>\Groups.one\, domain_type (snd (dest_Const mC))) $ t') | (NONE, NONE) => NONE, Rat.mult m' (Rat.inv p)) end else (SOME atom, m) (* terms that evaluate to numeric constants *) | demult (Const (\<^const_name>\Groups.uminus\, _) $ t, m) = demult (t, ~ m) | demult (Const (\<^const_name>\Groups.zero\, _), _) = (NONE, @0) | demult (Const (\<^const_name>\Groups.one\, _), m) = (NONE, m) (*Warning: in rare cases (neg_)numeral encloses a non-numeral, in which case dest_numeral raises TERM; hence all the handles below. Same for Suc-terms that turn out not to be numerals - although the simplifier should eliminate those anyway ...*) | demult (t as Const ("Num.numeral_class.numeral", _) (*DYNAMIC BINDING!*) $ n, m) = ((NONE, Rat.mult m (Rat.of_int (HOLogic.dest_numeral n))) handle TERM _ => (SOME t, m)) | demult (t as Const (\<^const_name>\Suc\, _) $ _, m) = ((NONE, Rat.mult m (Rat.of_int (HOLogic.dest_nat t))) handle TERM _ => (SOME t, m)) (* injection constants are ignored *) | demult (t as Const f $ x, m) = if member (op =) inj_consts f then demult (x, m) else (SOME t, m) (* everything else is considered atomic *) | demult (atom, m) = (SOME atom, m) in demult end; fun decomp0 thy (inj_consts : (string * typ) list) (rel : string, lhs : term, rhs : term) : ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat) option = let (* Turns a term 'all' and associated multiplicity 'm' into a list 'p' of summands and associated multiplicities, plus a constant 'i' (with implicit multiplicity 1) *) fun poly (Const (\<^const_name>\Groups.plus\, _) $ s $ t, m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi)) | poly (all as Const (\<^const_name>\Groups.minus\, T) $ s $ t, m, pi) = if nT T then add_atom all m pi else poly (s, m, poly (t, ~ m, pi)) | poly (all as Const (\<^const_name>\Groups.uminus\, T) $ t, m, pi) = if nT T then add_atom all m pi else poly (t, ~ m, pi) | poly (Const (\<^const_name>\Groups.zero\, _), _, pi) = pi | poly (Const (\<^const_name>\Groups.one\, _), m, (p, i)) = (p, Rat.add i m) | poly (all as Const ("Num.numeral_class.numeral", _) (*DYNAMIC BINDING!*) $ t, m, pi as (p, i)) = (let val k = HOLogic.dest_numeral t in (p, Rat.add i (Rat.mult m (Rat.of_int k))) end handle TERM _ => add_atom all m pi) | poly (Const (\<^const_name>\Suc\, _) $ t, m, (p, i)) = poly (t, m, (p, Rat.add i m)) | poly (all as Const (\<^const_name>\Groups.times\, _) $ _ $ _, m, pi as (p, i)) = (case demult thy inj_consts (all, m) of (NONE, m') => (p, Rat.add i m') | (SOME u, m') => add_atom u m' pi) | poly (all as Const (\<^const_name>\Rings.divide\, T) $ _ $ _, m, pi as (p, i)) = if of_field_sort thy (domain_type T) then (case demult thy inj_consts (all, m) of (NONE, m') => (p, Rat.add i m') | (SOME u, m') => add_atom u m' pi) else add_atom all m pi | poly (all as Const f $ x, m, pi) = if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi | poly (all, m, pi) = add_atom all m pi val (p, i) = poly (lhs, @1, ([], @0)) val (q, j) = poly (rhs, @1, ([], @0)) in case rel of \<^const_name>\Orderings.less\ => SOME (p, i, "<", q, j) | \<^const_name>\Orderings.less_eq\ => SOME (p, i, "<=", q, j) | \<^const_name>\HOL.eq\ => SOME (p, i, "=", q, j) | _ => NONE end handle General.Div => NONE; fun of_lin_arith_sort thy U = Sign.of_sort thy (U, \<^sort>\Rings.linordered_idom\); fun allows_lin_arith thy (discrete : string list) (U as Type (D, [])) : bool * bool = if of_lin_arith_sort thy U then (true, member (op =) discrete D) else if member (op =) discrete D then (true, true) else (false, false) | allows_lin_arith sg _ U = (of_lin_arith_sort sg U, false); fun decomp_typecheck thy (discrete, inj_consts) (T : typ, xxx) : decomp option = case T of Type ("fun", [U, _]) => (case allows_lin_arith thy discrete U of (true, d) => (case decomp0 thy inj_consts xxx of NONE => NONE | SOME (p, i, rel, q, j) => SOME (p, i, rel, q, j, d)) | (false, _) => NONE) | _ => NONE; fun negate (SOME (x, i, rel, y, j, d)) = SOME (x, i, "~" ^ rel, y, j, d) | negate NONE = NONE; fun decomp_negation thy data ((Const (\<^const_name>\Trueprop\, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option = decomp_typecheck thy data (T, (rel, lhs, rhs)) | decomp_negation thy data ((Const (\<^const_name>\Trueprop\, _)) $ (Const (\<^const_name>\Not\, _) $ (Const (rel, T) $ lhs $ rhs))) = negate (decomp_typecheck thy data (T, (rel, lhs, rhs))) | decomp_negation _ _ _ = NONE; fun decomp ctxt : term -> decomp option = let val thy = Proof_Context.theory_of ctxt val {discrete, inj_consts, ...} = get_arith_data ctxt in decomp_negation thy (discrete, inj_consts) end; fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T | domain_is_nat (_ $ (Const (\<^const_name>\Not\, _) $ (Const (_, T) $ _ $ _))) = nT T | domain_is_nat _ = false; (* Abstraction of terms *) (* Abstract terms contain only arithmetic operators and relations. When constructing an abstract term for an arbitrary term, non-arithmetic sub-terms are replaced by fresh variables which are declared in the context. Constructing an abstract term from an arbitrary term follows the strategy of decomp. *) fun apply t u = t $ u fun with2 f c t u cx = f t cx ||>> f u |>> (fn (t, u) => c $ t $ u) fun abstract_atom (t as Free _) cx = (t, cx) | abstract_atom (t as Const _) cx = (t, cx) | abstract_atom t (cx as (terms, ctxt)) = (case AList.lookup Envir.aeconv terms t of SOME u => (u, cx) | NONE => let val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt val u = Free (n, fastype_of t) in (u, ((t, u) :: terms, ctxt')) end) fun abstract_num t cx = if can HOLogic.dest_number t then (t, cx) else abstract_atom t cx fun is_field_sort (_, ctxt) T = of_field_sort (Proof_Context.theory_of ctxt) (domain_type T) fun is_inj_const (_, ctxt) f = let val {inj_consts, ...} = get_arith_data ctxt in member (op =) inj_consts f end fun abstract_arith ((c as Const (\<^const_name>\Groups.plus\, _)) $ u1 $ u2) cx = with2 abstract_arith c u1 u2 cx | abstract_arith (t as (c as Const (\<^const_name>\Groups.minus\, T)) $ u1 $ u2) cx = if nT T then abstract_atom t cx else with2 abstract_arith c u1 u2 cx | abstract_arith (t as (c as Const (\<^const_name>\Groups.uminus\, T)) $ u) cx = if nT T then abstract_atom t cx else abstract_arith u cx |>> apply c | abstract_arith ((c as Const (\<^const_name>\Suc\, _)) $ u) cx = abstract_arith u cx |>> apply c | abstract_arith ((c as Const (\<^const_name>\Groups.times\, _)) $ u1 $ u2) cx = with2 abstract_arith c u1 u2 cx | abstract_arith (t as (c as Const (\<^const_name>\Rings.divide\, T)) $ u1 $ u2) cx = if is_field_sort cx T then with2 abstract_arith c u1 u2 cx else abstract_atom t cx | abstract_arith (t as (c as Const f) $ u) cx = if is_inj_const cx f then abstract_arith u cx |>> apply c else abstract_num t cx | abstract_arith t cx = abstract_num t cx fun is_lin_arith_rel \<^const_name>\Orderings.less\ = true | is_lin_arith_rel \<^const_name>\Orderings.less_eq\ = true | is_lin_arith_rel \<^const_name>\HOL.eq\ = true | is_lin_arith_rel _ = false fun is_lin_arith_type (_, ctxt) T = let val {discrete, ...} = get_arith_data ctxt in fst (allows_lin_arith (Proof_Context.theory_of ctxt) discrete T) end fun abstract_rel (t as (r as Const (rel, Type ("fun", [U, _]))) $ lhs $ rhs) cx = if is_lin_arith_rel rel andalso is_lin_arith_type cx U then with2 abstract_arith r lhs rhs cx else abstract_atom t cx | abstract_rel t cx = abstract_atom t cx fun abstract_neg ((c as Const (\<^const_name>\Not\, _)) $ t) cx = abstract_rel t cx |>> apply c | abstract_neg t cx = abstract_rel t cx fun abstract ((c as Const (\<^const_name>\Trueprop\, _)) $ t) cx = abstract_neg t cx |>> apply c | abstract t cx = abstract_atom t cx (*---------------------------------------------------------------------------*) (* the following code performs splitting of certain constants (e.g., min, *) (* max) in a linear arithmetic problem; similar to what split_tac later does *) (* to the proof state *) (*---------------------------------------------------------------------------*) (* checks if splitting with 'thm' is implemented *) fun is_split_thm ctxt thm = (case Thm.concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *) (case head_of lhs of Const (a, _) => member (op =) [\<^const_name>\Orderings.max\, \<^const_name>\Orderings.min\, \<^const_name>\Groups.abs\, \<^const_name>\Groups.minus\, "Int.nat" (*DYNAMIC BINDING!*), \<^const_name>\Rings.modulo\, \<^const_name>\Rings.divide\] a | _ => (if Context_Position.is_visible ctxt then warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm) else (); false)) | _ => (if Context_Position.is_visible ctxt then warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm) else (); false)); (* substitute new for occurrences of old in a term, incrementing bound *) (* variables as needed when substituting inside an abstraction *) fun subst_term ([] : (term * term) list) (t : term) = t | subst_term pairs t = (case AList.lookup Envir.aeconv pairs t of SOME new => new | NONE => (case t of Abs (a, T, body) => let val pairs' = map (apply2 (incr_boundvars 1)) pairs in Abs (a, T, subst_term pairs' body) end | t1 $ t2 => subst_term pairs t1 $ subst_term pairs t2 | _ => t)); (* approximates the effect of one application of split_tac (followed by NNF *) (* normalization) on the subgoal represented by '(Ts, terms)'; returns a *) (* list of new subgoals (each again represented by a typ list for bound *) (* variables and a term list for premises), or NONE if split_tac would fail *) (* on the subgoal *) (* FIXME: currently only the effect of certain split theorems is reproduced *) (* (which is why we need 'is_split_thm'). A more canonical *) (* implementation should analyze the right-hand side of the split *) (* theorem that can be applied, and modify the subgoal accordingly. *) (* Or even better, the splitter should be extended to provide *) (* splitting on terms as well as splitting on theorems (where the *) (* former can have a faster implementation as it does not need to be *) (* proof-producing). *) fun split_once_items ctxt (Ts : typ list, terms : term list) : (typ list * term list) list option = let val thy = Proof_Context.theory_of ctxt (* takes a list [t1, ..., tn] to the term *) (* tn' --> ... --> t1' --> False , *) (* where ti' = HOLogic.dest_Trueprop ti *) fun REPEAT_DETERM_etac_rev_mp tms = fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms) \<^term>\False\ val split_thms = filter (is_split_thm ctxt) (get_splits ctxt) val cmap = Splitter.cmap_of_split_thms split_thms val goal_tm = REPEAT_DETERM_etac_rev_mp terms val splits = Splitter.split_posns cmap thy Ts goal_tm val split_limit = Config.get ctxt split_limit in if length splits > split_limit then ( tracing ("linarith_split_limit exceeded (current value is " ^ string_of_int split_limit ^ ")"); NONE ) else case splits of [] => (* split_tac would fail: no possible split *) NONE | (_, _::_, _, _, _) :: _ => (* disallow a split that involves non-locally bound variables (except *) (* when bound by outermost meta-quantifiers) *) NONE | (_, [], _, split_type, split_term) :: _ => (* ignore all but the first possible split *) (case strip_comb split_term of (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *) (Const (\<^const_name>\Orderings.max\, _), [t1, t2]) => let val rev_terms = rev terms val terms1 = map (subst_term [(split_term, t1)]) rev_terms val terms2 = map (subst_term [(split_term, t2)]) rev_terms val t1_leq_t2 = Const (\<^const_name>\Orderings.less_eq\, split_type --> split_type --> HOLogic.boolT) $ t1 $ t2 val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ \<^term>\False\) val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false] val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false] in SOME [(Ts, subgoal1), (Ts, subgoal2)] end (* ?P (min ?i ?j) = ((?i <= ?j --> ?P ?i) & (~ ?i <= ?j --> ?P ?j)) *) | (Const (\<^const_name>\Orderings.min\, _), [t1, t2]) => let val rev_terms = rev terms val terms1 = map (subst_term [(split_term, t1)]) rev_terms val terms2 = map (subst_term [(split_term, t2)]) rev_terms val t1_leq_t2 = Const (\<^const_name>\Orderings.less_eq\, split_type --> split_type --> HOLogic.boolT) $ t1 $ t2 val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ \<^term>\False\) val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false] val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false] in SOME [(Ts, subgoal1), (Ts, subgoal2)] end (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *) | (Const (\<^const_name>\Groups.abs\, _), [t1]) => let val rev_terms = rev terms val terms1 = map (subst_term [(split_term, t1)]) rev_terms val terms2 = map (subst_term [(split_term, Const (\<^const_name>\Groups.uminus\, split_type --> split_type) $ t1)]) rev_terms val zero = Const (\<^const_name>\Groups.zero\, split_type) val zero_leq_t1 = Const (\<^const_name>\Orderings.less_eq\, split_type --> split_type --> HOLogic.boolT) $ zero $ t1 val t1_lt_zero = Const (\<^const_name>\Orderings.less\, split_type --> split_type --> HOLogic.boolT) $ t1 $ zero val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ \<^term>\False\) val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false] val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false] in SOME [(Ts, subgoal1), (Ts, subgoal2)] end (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *) | (Const (\<^const_name>\Groups.minus\, _), [t1, t2]) => let (* "d" in the above theorem becomes a new bound variable after NNF *) (* transformation, therefore some adjustment of indices is necessary *) val rev_terms = rev terms val zero = Const (\<^const_name>\Groups.zero\, split_type) val d = Bound 0 val terms1 = map (subst_term [(split_term, zero)]) rev_terms val terms2 = map (subst_term [(incr_boundvars 1 split_term, d)]) (map (incr_boundvars 1) rev_terms) val t1' = incr_boundvars 1 t1 val t2' = incr_boundvars 1 t2 val t1_lt_t2 = Const (\<^const_name>\Orderings.less\, split_type --> split_type --> HOLogic.boolT) $ t1 $ t2 val t1_eq_t2_plus_d = Const (\<^const_name>\HOL.eq\, split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const (\<^const_name>\Groups.plus\, split_type --> split_type --> split_type) $ t2' $ d) val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ \<^term>\False\) val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false] val subgoal2 = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false] in SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)] end (* ?P (nat ?i) = ((ALL n. ?i = of_nat n --> ?P n) & (?i < 0 --> ?P 0)) *) | (Const ("Int.nat", _), (*DYNAMIC BINDING!*) [t1]) => let val rev_terms = rev terms val zero_int = Const (\<^const_name>\Groups.zero\, HOLogic.intT) val zero_nat = Const (\<^const_name>\Groups.zero\, HOLogic.natT) val n = Bound 0 val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)]) (map (incr_boundvars 1) rev_terms) val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms val t1' = incr_boundvars 1 t1 val t1_eq_nat_n = Const (\<^const_name>\HOL.eq\, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $ (Const (\<^const_name>\of_nat\, HOLogic.natT --> HOLogic.intT) $ n) val t1_lt_zero = Const (\<^const_name>\Orderings.less\, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ \<^term>\False\) val subgoal1 = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false] val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false] in SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)] end (* ?P ((?n::nat) mod (numeral ?k)) = ((numeral ?k = 0 --> ?P ?n) & (~ (numeral ?k = 0) --> (ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P j))) *) | (Const (\<^const_name>\Rings.modulo\, Type ("fun", [\<^typ>\nat\, _])), [t1, t2]) => let val rev_terms = rev terms val zero = Const (\<^const_name>\Groups.zero\, split_type) val i = Bound 1 val j = Bound 0 val terms1 = map (subst_term [(split_term, t1)]) rev_terms val terms2 = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms) val t1' = incr_boundvars 2 t1 val t2' = incr_boundvars 2 t2 val t2_eq_zero = Const (\<^const_name>\HOL.eq\, split_type --> split_type --> HOLogic.boolT) $ t2 $ zero val t2_neq_zero = HOLogic.mk_not (Const (\<^const_name>\HOL.eq\, split_type --> split_type --> HOLogic.boolT) $ t2' $ zero) val j_lt_t2 = Const (\<^const_name>\Orderings.less\, split_type --> split_type--> HOLogic.boolT) $ j $ t2' val t1_eq_t2_times_i_plus_j = Const (\<^const_name>\HOL.eq\, split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const (\<^const_name>\Groups.plus\, split_type --> split_type --> split_type) $ (Const (\<^const_name>\Groups.times\, split_type --> split_type --> split_type) $ t2' $ i) $ j) val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ \<^term>\False\) val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] val subgoal2 = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false] in SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)] end (* ?P ((?n::nat) div (numeral ?k)) = ((numeral ?k = 0 --> ?P 0) & (~ (numeral ?k = 0) --> (ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P i))) *) | (Const (\<^const_name>\Rings.divide\, Type ("fun", [\<^typ>\nat\, _])), [t1, t2]) => let val rev_terms = rev terms val zero = Const (\<^const_name>\Groups.zero\, split_type) val i = Bound 1 val j = Bound 0 val terms1 = map (subst_term [(split_term, zero)]) rev_terms val terms2 = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms) val t1' = incr_boundvars 2 t1 val t2' = incr_boundvars 2 t2 val t2_eq_zero = Const (\<^const_name>\HOL.eq\, split_type --> split_type --> HOLogic.boolT) $ t2 $ zero val t2_neq_zero = HOLogic.mk_not (Const (\<^const_name>\HOL.eq\, split_type --> split_type --> HOLogic.boolT) $ t2' $ zero) val j_lt_t2 = Const (\<^const_name>\Orderings.less\, split_type --> split_type--> HOLogic.boolT) $ j $ t2' val t1_eq_t2_times_i_plus_j = Const (\<^const_name>\HOL.eq\, split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const (\<^const_name>\Groups.plus\, split_type --> split_type --> split_type) $ (Const (\<^const_name>\Groups.times\, split_type --> split_type --> split_type) $ t2' $ i) $ j) val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ \<^term>\False\) val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] val subgoal2 = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false] in SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)] end (* ?P ((?n::int) mod (numeral ?k)) = ((numeral ?k = 0 --> ?P ?n) & (0 < numeral ?k --> (ALL i j. 0 <= j & j < numeral ?k & ?n = numeral ?k * i + j --> ?P j)) & (numeral ?k < 0 --> (ALL i j. numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P j))) *) | (Const (\<^const_name>\Rings.modulo\, Type ("fun", [Type ("Int.int", []), _])), (*DYNAMIC BINDING!*) [t1, t2]) => let val rev_terms = rev terms val zero = Const (\<^const_name>\Groups.zero\, split_type) val i = Bound 1 val j = Bound 0 val terms1 = map (subst_term [(split_term, t1)]) rev_terms val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms) val t1' = incr_boundvars 2 t1 val t2' = incr_boundvars 2 t2 val t2_eq_zero = Const (\<^const_name>\HOL.eq\, split_type --> split_type --> HOLogic.boolT) $ t2 $ zero val zero_lt_t2 = Const (\<^const_name>\Orderings.less\, split_type --> split_type --> HOLogic.boolT) $ zero $ t2' val t2_lt_zero = Const (\<^const_name>\Orderings.less\, split_type --> split_type --> HOLogic.boolT) $ t2' $ zero val zero_leq_j = Const (\<^const_name>\Orderings.less_eq\, split_type --> split_type --> HOLogic.boolT) $ zero $ j val j_leq_zero = Const (\<^const_name>\Orderings.less_eq\, split_type --> split_type --> HOLogic.boolT) $ j $ zero val j_lt_t2 = Const (\<^const_name>\Orderings.less\, split_type --> split_type--> HOLogic.boolT) $ j $ t2' val t2_lt_j = Const (\<^const_name>\Orderings.less\, split_type --> split_type--> HOLogic.boolT) $ t2' $ j val t1_eq_t2_times_i_plus_j = Const (\<^const_name>\HOL.eq\, split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const (\<^const_name>\Groups.plus\, split_type --> split_type --> split_type) $ (Const (\<^const_name>\Groups.times\, split_type --> split_type --> split_type) $ t2' $ i) $ j) val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ \<^term>\False\) val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] val subgoal2 = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j]) @ hd terms2_3 :: (if tl terms2_3 = [] then [not_false] else []) @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j]) @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false]) val subgoal3 = (map HOLogic.mk_Trueprop [t2_lt_zero, t2_lt_j]) @ hd terms2_3 :: (if tl terms2_3 = [] then [not_false] else []) @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j]) @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false]) val Ts' = split_type :: split_type :: Ts in SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)] end (* ?P ((?n::int) div (numeral ?k)) = ((numeral ?k = 0 --> ?P 0) & (0 < numeral ?k --> (ALL i j. 0 <= j & j < numeral ?k & ?n = numeral ?k * i + j --> ?P i)) & (numeral ?k < 0 --> (ALL i j. numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P i))) *) | (Const (\<^const_name>\Rings.divide\, Type ("fun", [Type ("Int.int", []), _])), (*DYNAMIC BINDING!*) [t1, t2]) => let val rev_terms = rev terms val zero = Const (\<^const_name>\Groups.zero\, split_type) val i = Bound 1 val j = Bound 0 val terms1 = map (subst_term [(split_term, zero)]) rev_terms val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms) val t1' = incr_boundvars 2 t1 val t2' = incr_boundvars 2 t2 val t2_eq_zero = Const (\<^const_name>\HOL.eq\, split_type --> split_type --> HOLogic.boolT) $ t2 $ zero val zero_lt_t2 = Const (\<^const_name>\Orderings.less\, split_type --> split_type --> HOLogic.boolT) $ zero $ t2' val t2_lt_zero = Const (\<^const_name>\Orderings.less\, split_type --> split_type --> HOLogic.boolT) $ t2' $ zero val zero_leq_j = Const (\<^const_name>\Orderings.less_eq\, split_type --> split_type --> HOLogic.boolT) $ zero $ j val j_leq_zero = Const (\<^const_name>\Orderings.less_eq\, split_type --> split_type --> HOLogic.boolT) $ j $ zero val j_lt_t2 = Const (\<^const_name>\Orderings.less\, split_type --> split_type--> HOLogic.boolT) $ j $ t2' val t2_lt_j = Const (\<^const_name>\Orderings.less\, split_type --> split_type--> HOLogic.boolT) $ t2' $ j val t1_eq_t2_times_i_plus_j = Const (\<^const_name>\HOL.eq\, split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const (\<^const_name>\Groups.plus\, split_type --> split_type --> split_type) $ (Const (\<^const_name>\Groups.times\, split_type --> split_type --> split_type) $ t2' $ i) $ j) val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ \<^term>\False\) val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] val subgoal2 = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j]) @ hd terms2_3 :: (if tl terms2_3 = [] then [not_false] else []) @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j]) @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false]) val subgoal3 = (map HOLogic.mk_Trueprop [t2_lt_zero, t2_lt_j]) @ hd terms2_3 :: (if tl terms2_3 = [] then [not_false] else []) @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j]) @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false]) val Ts' = split_type :: split_type :: Ts in SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)] end (* this will only happen if a split theorem can be applied for which no *) (* code exists above -- in which case either the split theorem should be *) (* implemented above, or 'is_split_thm' should be modified to filter it *) (* out *) | (t, ts) => (if Context_Position.is_visible ctxt then warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^ " (with " ^ string_of_int (length ts) ^ " argument(s)) not implemented; proof reconstruction is likely to fail") else (); NONE)) end; (* split_once_items *) (* remove terms that do not satisfy 'p'; change the order of the remaining *) (* terms in the same way as filter_prems_tac does *) fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list = let fun filter_prems t (left, right) = if p t then (left, right @ [t]) else (left @ right, []) val (left, right) = fold filter_prems terms ([], []) in right @ left end; (* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a *) (* subgoal that has 'terms' as premises *) fun negated_term_occurs_positively (terms : term list) : bool = exists (fn (Trueprop $ (Const (\<^const_name>\Not\, _) $ t)) => member Envir.aeconv terms (Trueprop $ t) | _ => false) terms; fun pre_decomp ctxt (Ts : typ list, terms : term list) : (typ list * term list) list = let (* repeatedly split (including newly emerging subgoals) until no further *) (* splitting is possible *) fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list) | split_loop (subgoal::subgoals) = (case split_once_items ctxt subgoal of SOME new_subgoals => split_loop (new_subgoals @ subgoals) | NONE => subgoal :: split_loop subgoals) fun is_relevant t = is_some (decomp ctxt t) (* filter_prems_tac is_relevant: *) val relevant_terms = filter_prems_tac_items is_relevant terms (* split_tac, NNF normalization: *) val split_goals = split_loop [(Ts, relevant_terms)] (* necessary because split_once_tac may normalize terms: *) val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals (* TRY (etac notE) THEN eq_assume_tac: *) val result = filter_out (negated_term_occurs_positively o snd) beta_eta_norm in result end; (* takes the i-th subgoal [| A1; ...; An |] ==> B to *) (* An --> ... --> A1 --> B, performs splitting with the given 'split_thms' *) (* (resulting in a different subgoal P), takes P to ~P ==> False, *) (* performs NNF-normalization of ~P, and eliminates conjunctions, *) (* disjunctions and existential quantifiers from the premises, possibly (in *) (* the case of disjunctions) resulting in several new subgoals, each of the *) (* general form [| Q1; ...; Qm |] ==> False. Fails if more than *) (* !split_limit splits are possible. *) local fun nnf_simpset ctxt = (empty_simpset ctxt |> Simplifier.set_mkeqTrue mk_eq_True |> Simplifier.set_mksimps (mksimps mksimps_pairs)) addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj}, @{thm de_Morgan_conj}, not_all, not_ex, not_not] fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt) in fun split_once_tac ctxt split_thms = let val thy = Proof_Context.theory_of ctxt val cond_split_tac = SUBGOAL (fn (subgoal, i) => let val Ts = rev (map snd (Logic.strip_params subgoal)) val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal) val cmap = Splitter.cmap_of_split_thms split_thms val splits = Splitter.split_posns cmap thy Ts concl in if null splits orelse length splits > Config.get ctxt split_limit then no_tac else if null (#2 (hd splits)) then split_tac ctxt split_thms i else (* disallow a split that involves non-locally bound variables *) (* (except when bound by outermost meta-quantifiers) *) no_tac end) in EVERY' [ REPEAT_DETERM o eresolve_tac ctxt [rev_mp], cond_split_tac, resolve_tac ctxt @{thms ccontr}, prem_nnf_tac ctxt, TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac ctxt [conjE, exE] ORELSE' eresolve_tac ctxt [disjE])) ] end; end; (* local *) (* remove irrelevant premises, then split the i-th subgoal (and all new *) (* subgoals) by using 'split_once_tac' repeatedly. Beta-eta-normalize new *) (* subgoals and finally attempt to solve them by finding an immediate *) (* contradiction (i.e., a term and its negation) in their premises. *) fun pre_tac ctxt i = let val split_thms = filter (is_split_thm ctxt) (get_splits ctxt) fun is_relevant t = is_some (decomp ctxt t) in DETERM ( TRY (filter_prems_tac ctxt is_relevant i) THEN ( (TRY o REPEAT_ALL_NEW (split_once_tac ctxt split_thms)) THEN_ALL_NEW (CONVERSION Drule.beta_eta_conversion THEN' (TRY o (eresolve_tac ctxt [notE] THEN' eq_assume_tac))) ) i ) end; end; (* LA_Data *) val pre_tac = LA_Data.pre_tac; structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data); val add_inj_thms = Fast_Arith.add_inj_thms; val add_lessD = Fast_Arith.add_lessD; val add_simps = Fast_Arith.add_simps; val add_simprocs = Fast_Arith.add_simprocs; val set_number_of = Fast_Arith.set_number_of; val simple_tac = Fast_Arith.lin_arith_tac; (* reduce contradictory <= to False. Most of the work is done by the cancel tactics. *) val init_arith_data = Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, number_of, ...} => {add_mono_thms = map Thm.trim_context @{thms add_mono_thms_linordered_semiring add_mono_thms_linordered_field} @ add_mono_thms, mult_mono_thms = map Thm.trim_context (@{thms mult_strict_left_mono mult_left_mono} @ [@{lemma "a = b ==> c * a = c * b" by (rule arg_cong)}]) @ mult_mono_thms, inj_thms = inj_thms, lessD = lessD, neqE = map Thm.trim_context @{thms linorder_neqE_nat linorder_neqE_linordered_idom} @ neqE, simpset = put_simpset HOL_basic_ss \<^context> |> Simplifier.add_cong @{thm if_weak_cong} |> simpset_of, number_of = number_of}); (* FIXME !?? *) fun add_arith_facts ctxt = Simplifier.add_prems (rev (Named_Theorems.get ctxt \<^named_theorems>\arith\)) ctxt; val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc; (* generic refutation procedure *) (* parameters: test: term -> bool tests if a term is at all relevant to the refutation proof; if not, then it can be discarded. Can improve performance, esp. if disjunctions can be discarded (no case distinction needed!). prep_tac: int -> tactic A preparation tactic to be applied to the goal once all relevant premises have been moved to the conclusion. ref_tac: int -> tactic the actual refutation tactic. Should be able to deal with goals [| A1; ...; An |] ==> False where the Ai are atomic, i.e. no top-level &, | or EX *) local fun nnf_simpset ctxt = (empty_simpset ctxt |> Simplifier.set_mkeqTrue mk_eq_True |> Simplifier.set_mksimps (mksimps mksimps_pairs)) addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj}, @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}]; fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt); in fun refute_tac ctxt test prep_tac ref_tac = let val refute_prems_tac = REPEAT_DETERM (eresolve_tac ctxt [@{thm conjE}, @{thm exE}] 1 ORELSE filter_prems_tac ctxt test 1 ORELSE eresolve_tac ctxt @{thms disjE} 1) THEN (DETERM (eresolve_tac ctxt @{thms notE} 1 THEN eq_assume_tac 1) ORELSE ref_tac 1); in EVERY'[TRY o filter_prems_tac ctxt test, REPEAT_DETERM o eresolve_tac ctxt @{thms rev_mp}, prep_tac, resolve_tac ctxt @{thms ccontr}, prem_nnf_tac ctxt, SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] end; end; (* arith proof method *) local fun raw_tac ctxt = (* FIXME: K true should be replaced by a sensible test (perhaps "is_some o decomp sg"? -- but note that the test is applied to terms already before they are split/normalized) to speed things up in case there are lots of irrelevant terms involved; elimination of min/max can be optimized: (max m n + k <= r) = (m+k <= r & n+k <= r) (l <= min m n + k) = (l <= m+k & l <= n+k) *) refute_tac ctxt (K true) (* Splitting is also done inside simple_tac, but not completely -- *) (* split_tac may use split theorems that have not been implemented in *) (* simple_tac (cf. pre_decomp and split_once_items above), and *) (* split_limit may trigger. *) (* Therefore splitting outside of simple_tac may allow us to prove *) (* some goals that simple_tac alone would fail on. *) (REPEAT_DETERM o split_tac ctxt (get_splits ctxt)) (Fast_Arith.lin_arith_tac ctxt); in fun tac ctxt = FIRST' [simple_tac ctxt, Object_Logic.full_atomize_tac ctxt THEN' (REPEAT_DETERM o resolve_tac ctxt [impI]) THEN' raw_tac ctxt]; end; (* context setup *) val global_setup = map_theory_simpset (fn ctxt => ctxt addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac))) #> Attrib.setup \<^binding>\arith_split\ (Scan.succeed (Thm.declaration_attribute add_split)) "declaration of split rules for arithmetic procedure" #> Method.setup \<^binding>\linarith\ (Scan.succeed (fn ctxt => METHOD (fn facts => HEADGOAL (Method.insert_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\arith\) @ facts) THEN' tac ctxt)))) "linear arithmetic" #> Arith_Data.add_tactic "linear arithmetic" tac; end;