diff --git a/src/HOL/Numeral_Simprocs.thy b/src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy +++ b/src/HOL/Numeral_Simprocs.thy @@ -1,302 +1,302 @@ (* Author: Various *) section \Combination and Cancellation Simprocs for Numeral Expressions\ theory Numeral_Simprocs imports Divides begin ML_file \~~/src/Provers/Arith/assoc_fold.ML\ ML_file \~~/src/Provers/Arith/cancel_numerals.ML\ ML_file \~~/src/Provers/Arith/combine_numerals.ML\ ML_file \~~/src/Provers/Arith/cancel_numeral_factor.ML\ ML_file \~~/src/Provers/Arith/extract_common_term.ML\ lemmas semiring_norm = Let_def arith_simps diff_nat_numeral rel_simps if_False if_True - add_0 add_Suc add_numeral_left + add_Suc add_numeral_left add_neg_numeral_left mult_numeral_left numeral_One [symmetric] uminus_numeral_One [symmetric] Suc_eq_plus1 eq_numeral_iff_iszero not_iszero_Numeral1 declare split_div [of _ _ "numeral k", linarith_split] for k declare split_mod [of _ _ "numeral k", linarith_split] for k text \For \combine_numerals\\ lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)" by (simp add: add_mult_distrib) text \For \cancel_numerals\\ lemma nat_diff_add_eq1: "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)" by (simp split: nat_diff_split add: add_mult_distrib) lemma nat_diff_add_eq2: "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))" by (simp split: nat_diff_split add: add_mult_distrib) lemma nat_eq_add_iff1: "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)" by (auto split: nat_diff_split simp add: add_mult_distrib) lemma nat_eq_add_iff2: "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)" by (auto split: nat_diff_split simp add: add_mult_distrib) lemma nat_less_add_iff1: "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)" by (auto split: nat_diff_split simp add: add_mult_distrib) lemma nat_less_add_iff2: "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)" by (auto split: nat_diff_split simp add: add_mult_distrib) lemma nat_le_add_iff1: "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)" by (auto split: nat_diff_split simp add: add_mult_distrib) lemma nat_le_add_iff2: "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)" by (auto split: nat_diff_split simp add: add_mult_distrib) text \For \cancel_numeral_factors\\ lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)" by auto lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m (k*m = k*n) = (m=n)" by auto lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)" by auto lemma nat_mult_dvd_cancel_disj[simp]: "(k*m) dvd (k*n) = (k=0 \ m dvd (n::nat))" by (auto simp: dvd_eq_mod_eq_0 mod_mult_mult1) lemma nat_mult_dvd_cancel1: "0 < k \ (k*m) dvd (k*n::nat) = (m dvd n)" by(auto) text \For \cancel_factor\\ lemmas nat_mult_le_cancel_disj = mult_le_cancel1 lemmas nat_mult_less_cancel_disj = mult_less_cancel1 lemma nat_mult_eq_cancel_disj: fixes k m n :: nat shows "k * m = k * n \ k = 0 \ m = n" - by auto + by (fact mult_cancel_left) -lemma nat_mult_div_cancel_disj [simp]: +lemma nat_mult_div_cancel_disj: fixes k m n :: nat shows "(k * m) div (k * n) = (if k = 0 then 0 else m div n)" by (fact div_mult_mult1_if) lemma numeral_times_minus_swap: fixes x:: "'a::comm_ring_1" shows "numeral w * -x = x * - numeral w" - by (simp add: mult.commute) + by (simp add: ac_simps) ML_file \Tools/numeral_simprocs.ML\ simproc_setup semiring_assoc_fold ("(a::'a::comm_semiring_1_cancel) * b") = \fn phi => Numeral_Simprocs.assoc_fold\ (* TODO: see whether the type class can be generalized further *) simproc_setup int_combine_numerals ("(i::'a::comm_ring_1) + j" | "(i::'a::comm_ring_1) - j") = \fn phi => Numeral_Simprocs.combine_numerals\ simproc_setup field_combine_numerals ("(i::'a::{field,ring_char_0}) + j" |"(i::'a::{field,ring_char_0}) - j") = \fn phi => Numeral_Simprocs.field_combine_numerals\ simproc_setup inteq_cancel_numerals ("(l::'a::comm_ring_1) + m = n" |"(l::'a::comm_ring_1) = m + n" |"(l::'a::comm_ring_1) - m = n" |"(l::'a::comm_ring_1) = m - n" |"(l::'a::comm_ring_1) * m = n" |"(l::'a::comm_ring_1) = m * n" |"- (l::'a::comm_ring_1) = m" |"(l::'a::comm_ring_1) = - m") = \fn phi => Numeral_Simprocs.eq_cancel_numerals\ simproc_setup intless_cancel_numerals ("(l::'a::linordered_idom) + m < n" |"(l::'a::linordered_idom) < m + n" |"(l::'a::linordered_idom) - m < n" |"(l::'a::linordered_idom) < m - n" |"(l::'a::linordered_idom) * m < n" |"(l::'a::linordered_idom) < m * n" |"- (l::'a::linordered_idom) < m" |"(l::'a::linordered_idom) < - m") = \fn phi => Numeral_Simprocs.less_cancel_numerals\ simproc_setup intle_cancel_numerals ("(l::'a::linordered_idom) + m \ n" |"(l::'a::linordered_idom) \ m + n" |"(l::'a::linordered_idom) - m \ n" |"(l::'a::linordered_idom) \ m - n" |"(l::'a::linordered_idom) * m \ n" |"(l::'a::linordered_idom) \ m * n" |"- (l::'a::linordered_idom) \ m" |"(l::'a::linordered_idom) \ - m") = \fn phi => Numeral_Simprocs.le_cancel_numerals\ simproc_setup ring_eq_cancel_numeral_factor ("(l::'a::{idom,ring_char_0}) * m = n" |"(l::'a::{idom,ring_char_0}) = m * n") = \fn phi => Numeral_Simprocs.eq_cancel_numeral_factor\ simproc_setup ring_less_cancel_numeral_factor ("(l::'a::linordered_idom) * m < n" |"(l::'a::linordered_idom) < m * n") = \fn phi => Numeral_Simprocs.less_cancel_numeral_factor\ simproc_setup ring_le_cancel_numeral_factor ("(l::'a::linordered_idom) * m <= n" |"(l::'a::linordered_idom) <= m * n") = \fn phi => Numeral_Simprocs.le_cancel_numeral_factor\ (* TODO: remove comm_ring_1 constraint if possible *) simproc_setup int_div_cancel_numeral_factors ("((l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) * m) div n" |"(l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) div (m * n)") = \fn phi => Numeral_Simprocs.div_cancel_numeral_factor\ simproc_setup divide_cancel_numeral_factor ("((l::'a::{field,ring_char_0}) * m) / n" |"(l::'a::{field,ring_char_0}) / (m * n)" |"((numeral v)::'a::{field,ring_char_0}) / (numeral w)") = \fn phi => Numeral_Simprocs.divide_cancel_numeral_factor\ simproc_setup ring_eq_cancel_factor ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") = \fn phi => Numeral_Simprocs.eq_cancel_factor\ simproc_setup linordered_ring_le_cancel_factor ("(l::'a::linordered_idom) * m <= n" |"(l::'a::linordered_idom) <= m * n") = \fn phi => Numeral_Simprocs.le_cancel_factor\ simproc_setup linordered_ring_less_cancel_factor ("(l::'a::linordered_idom) * m < n" |"(l::'a::linordered_idom) < m * n") = \fn phi => Numeral_Simprocs.less_cancel_factor\ simproc_setup int_div_cancel_factor ("((l::'a::euclidean_semiring_cancel) * m) div n" |"(l::'a::euclidean_semiring_cancel) div (m * n)") = \fn phi => Numeral_Simprocs.div_cancel_factor\ simproc_setup int_mod_cancel_factor ("((l::'a::euclidean_semiring_cancel) * m) mod n" |"(l::'a::euclidean_semiring_cancel) mod (m * n)") = \fn phi => Numeral_Simprocs.mod_cancel_factor\ simproc_setup dvd_cancel_factor ("((l::'a::idom) * m) dvd n" |"(l::'a::idom) dvd (m * n)") = \fn phi => Numeral_Simprocs.dvd_cancel_factor\ simproc_setup divide_cancel_factor ("((l::'a::field) * m) / n" |"(l::'a::field) / (m * n)") = \fn phi => Numeral_Simprocs.divide_cancel_factor\ ML_file \Tools/nat_numeral_simprocs.ML\ simproc_setup nat_combine_numerals ("(i::nat) + j" | "Suc (i + j)") = \fn phi => Nat_Numeral_Simprocs.combine_numerals\ simproc_setup nateq_cancel_numerals ("(l::nat) + m = n" | "(l::nat) = m + n" | "(l::nat) * m = n" | "(l::nat) = m * n" | "Suc m = n" | "m = Suc n") = \fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals\ simproc_setup natless_cancel_numerals ("(l::nat) + m < n" | "(l::nat) < m + n" | "(l::nat) * m < n" | "(l::nat) < m * n" | "Suc m < n" | "m < Suc n") = \fn phi => Nat_Numeral_Simprocs.less_cancel_numerals\ simproc_setup natle_cancel_numerals ("(l::nat) + m \ n" | "(l::nat) \ m + n" | "(l::nat) * m \ n" | "(l::nat) \ m * n" | "Suc m \ n" | "m \ Suc n") = \fn phi => Nat_Numeral_Simprocs.le_cancel_numerals\ simproc_setup natdiff_cancel_numerals ("((l::nat) + m) - n" | "(l::nat) - (m + n)" | "(l::nat) * m - n" | "(l::nat) - m * n" | "Suc m - n" | "m - Suc n") = \fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals\ simproc_setup nat_eq_cancel_numeral_factor ("(l::nat) * m = n" | "(l::nat) = m * n") = \fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor\ simproc_setup nat_less_cancel_numeral_factor ("(l::nat) * m < n" | "(l::nat) < m * n") = \fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor\ simproc_setup nat_le_cancel_numeral_factor ("(l::nat) * m <= n" | "(l::nat) <= m * n") = \fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor\ simproc_setup nat_div_cancel_numeral_factor ("((l::nat) * m) div n" | "(l::nat) div (m * n)") = \fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor\ simproc_setup nat_dvd_cancel_numeral_factor ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = \fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor\ simproc_setup nat_eq_cancel_factor ("(l::nat) * m = n" | "(l::nat) = m * n") = \fn phi => Nat_Numeral_Simprocs.eq_cancel_factor\ simproc_setup nat_less_cancel_factor ("(l::nat) * m < n" | "(l::nat) < m * n") = \fn phi => Nat_Numeral_Simprocs.less_cancel_factor\ simproc_setup nat_le_cancel_factor ("(l::nat) * m <= n" | "(l::nat) <= m * n") = \fn phi => Nat_Numeral_Simprocs.le_cancel_factor\ simproc_setup nat_div_cancel_factor ("((l::nat) * m) div n" | "(l::nat) div (m * n)") = \fn phi => Nat_Numeral_Simprocs.div_cancel_factor\ simproc_setup nat_dvd_cancel_factor ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = \fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor\ declaration \ K (Lin_Arith.add_simprocs [\<^simproc>\semiring_assoc_fold\, \<^simproc>\int_combine_numerals\, \<^simproc>\inteq_cancel_numerals\, \<^simproc>\intless_cancel_numerals\, \<^simproc>\intle_cancel_numerals\, \<^simproc>\field_combine_numerals\, \<^simproc>\nat_combine_numerals\, \<^simproc>\nateq_cancel_numerals\, \<^simproc>\natless_cancel_numerals\, \<^simproc>\natle_cancel_numerals\, \<^simproc>\natdiff_cancel_numerals\, Numeral_Simprocs.field_divide_cancel_numeral_factor]) \ 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,961 @@ (* 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 = \<^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); +fun nnf_simpset ctxt = + (empty_simpset ctxt + |> Simplifier.set_mkeqTrue mk_eq_True + |> Simplifier.set_mksimps (mksimps mksimps_pairs)) + addsimps @{thms imp_conv_disj iff_conv_conj_imp de_Morgan_disj + de_Morgan_conj not_all not_ex not_not} + +fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt) + 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>\linarith_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; diff --git a/src/HOL/Tools/numeral_simprocs.ML b/src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML +++ b/src/HOL/Tools/numeral_simprocs.ML @@ -1,741 +1,740 @@ (* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 2000 University of Cambridge Simprocs for the (integer) numerals. *) (*To quote from Provers/Arith/cancel_numeral_factor.ML: Cancels common coefficients in balanced expressions: u*#m ~~ u'*#m' == #n*u ~~ #n'*u' where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) and d = gcd(m,m') and n=m/d and n'=m'/d. *) signature NUMERAL_SIMPROCS = sig val trans_tac: Proof.context -> thm option -> tactic val assoc_fold: Proof.context -> cterm -> thm option val combine_numerals: Proof.context -> cterm -> thm option val eq_cancel_numerals: Proof.context -> cterm -> thm option val less_cancel_numerals: Proof.context -> cterm -> thm option val le_cancel_numerals: Proof.context -> cterm -> thm option val eq_cancel_factor: Proof.context -> cterm -> thm option val le_cancel_factor: Proof.context -> cterm -> thm option val less_cancel_factor: Proof.context -> cterm -> thm option val div_cancel_factor: Proof.context -> cterm -> thm option val mod_cancel_factor: Proof.context -> cterm -> thm option val dvd_cancel_factor: Proof.context -> cterm -> thm option val divide_cancel_factor: Proof.context -> cterm -> thm option val eq_cancel_numeral_factor: Proof.context -> cterm -> thm option val less_cancel_numeral_factor: Proof.context -> cterm -> thm option val le_cancel_numeral_factor: Proof.context -> cterm -> thm option val div_cancel_numeral_factor: Proof.context -> cterm -> thm option val divide_cancel_numeral_factor: Proof.context -> cterm -> thm option val field_combine_numerals: Proof.context -> cterm -> thm option val field_divide_cancel_numeral_factor: simproc val num_ss: simpset val field_comp_conv: Proof.context -> conv end; structure Numeral_Simprocs : NUMERAL_SIMPROCS = struct fun trans_tac _ NONE = all_tac | trans_tac ctxt (SOME th) = ALLGOALS (resolve_tac ctxt [th RS trans]); val mk_number = Arith_Data.mk_number; val mk_sum = Arith_Data.mk_sum; val long_mk_sum = Arith_Data.long_mk_sum; val dest_sum = Arith_Data.dest_sum; val mk_times = HOLogic.mk_binop \<^const_name>\Groups.times\; fun one_of T = Const(\<^const_name>\Groups.one\, T); (* build product with trailing 1 rather than Numeral 1 in order to avoid the unnecessary restriction to type class number_ring which is not required for cancellation of common factors in divisions. UPDATE: this reasoning no longer applies (number_ring is gone) *) fun mk_prod T = let val one = one_of T fun mk [] = one | mk [t] = t | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts) in mk end; (*This version ALWAYS includes a trailing one*) fun long_mk_prod T [] = one_of T | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); val dest_times = HOLogic.dest_bin \<^const_name>\Groups.times\ dummyT; fun dest_prod t = let val (t,u) = dest_times t in dest_prod t @ dest_prod u end handle TERM _ => [t]; fun find_first_numeral past (t::terms) = ((snd (HOLogic.dest_number t), rev past @ terms) handle TERM _ => find_first_numeral (t::past) terms) | find_first_numeral past [] = raise TERM("find_first_numeral", []); (*DON'T do the obvious simplifications; that would create special cases*) fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); (*Express t as a product of (possibly) a numeral with other sorted terms*) fun dest_coeff sign (Const (\<^const_name>\Groups.uminus\, _) $ t) = dest_coeff (~sign) t | dest_coeff sign t = let val ts = sort Term_Ord.term_ord (dest_prod t) val (n, ts') = find_first_numeral [] ts handle TERM _ => (1, ts) in (sign*n, mk_prod (Term.fastype_of t) ts') end; (*Find first coefficient-term THAT MATCHES u*) fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) | find_first_coeff past u (t::terms) = let val (n,u') = dest_coeff 1 t in if u aconv u' then (n, rev past @ terms) else find_first_coeff (t::past) u terms end handle TERM _ => find_first_coeff (t::past) u terms; (*Fractions as pairs of ints. Can't use Rat.rat because the representation needs to preserve negative values in the denominator.*) fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); (*Don't reduce fractions; sums must be proved by rule add_frac_eq. Fractions are reduced later by the cancel_numeral_factor simproc.*) fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); val mk_divide = HOLogic.mk_binop \<^const_name>\Rings.divide\; (*Build term (p / q) * t*) fun mk_fcoeff ((p, q), t) = let val T = Term.fastype_of t in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; (*Express t as a product of a fraction with other sorted terms*) fun dest_fcoeff sign (Const (\<^const_name>\Groups.uminus\, _) $ t) = dest_fcoeff (~sign) t | dest_fcoeff sign (Const (\<^const_name>\Rings.divide\, _) $ t $ u) = let val (p, t') = dest_coeff sign t val (q, u') = dest_coeff 1 u in (mk_frac (p, q), mk_divide (t', u')) end | dest_fcoeff sign t = let val (p, t') = dest_coeff sign t val T = Term.fastype_of t in (mk_frac (p, 1), mk_divide (t', one_of T)) end; (** New term ordering so that AC-rewriting brings numerals to the front **) (*Order integers by absolute value and then by sign. The standard integer ordering is not well-founded.*) fun num_ord (i,j) = (case int_ord (abs i, abs j) of EQUAL => int_ord (Int.sign i, Int.sign j) | ord => ord); (*This resembles Term_Ord.term_ord, but it puts binary numerals before other non-atomic terms.*) local open Term in fun numterm_ord (t, u) = case (try HOLogic.dest_number t, try HOLogic.dest_number u) of (SOME (_, i), SOME (_, j)) => num_ord (i, j) | (SOME _, NONE) => LESS | (NONE, SOME _) => GREATER | _ => ( case (t, u) of (Abs (_, T, t), Abs(_, U, u)) => (prod_ord numterm_ord Term_Ord.typ_ord ((t, T), (u, U))) | _ => ( case int_ord (size_of_term t, size_of_term u) of EQUAL => let val (f, ts) = strip_comb t and (g, us) = strip_comb u in (prod_ord Term_Ord.hd_ord numterms_ord ((f, ts), (g, us))) end | ord => ord)) and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) end; val num_ss = simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.set_term_ord numterm_ord); (*Maps 1 to Numeral1 so that arithmetic isn't complicated by the abstract 1.*) -val numeral_syms = [@{thm numeral_One} RS sym]; +val numeral_syms = @{thms numeral_One [symmetric]}; (*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) val add_0s = @{thms add_0_left add_0_right}; val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right div_by_1}; (* For post-simplification of the rhs of simproc-generated rules *) val post_simps = - [@{thm numeral_One}, - @{thm add_0_left}, @{thm add_0_right}, - @{thm mult_zero_left}, @{thm mult_zero_right}, - @{thm mult_1_left}, @{thm mult_1_right}, - @{thm mult_minus1}, @{thm mult_minus1_right}] + @{thms numeral_One + add_0_left add_0_right + mult_zero_left mult_zero_right + mult_1_left mult_1_right + mult_minus1 mult_minus1_right} val field_post_simps = - post_simps @ [@{thm div_0}, @{thm div_by_1}] + post_simps @ @{thms div_0 div_by_1} (*Simplify inverse Numeral1*) -val inverse_1s = [@{thm inverse_numeral_1}]; +val inverse_1s = @{thms inverse_numeral_1} (*To perform binary arithmetic. The "left" rewriting handles patterns created by the Numeral_Simprocs, such as 3 * (5 * x). *) val simps = - [@{thm numeral_One} RS sym] @ - @{thms add_numeral_left} @ - @{thms add_neg_numeral_left} @ - @{thms mult_numeral_left} @ - @{thms arith_simps} @ @{thms rel_simps}; + @{thms numeral_One [symmetric] + add_numeral_left + add_neg_numeral_left + mult_numeral_left + arith_simps rel_simps} (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms during re-arrangement*) val non_add_simps = subtract Thm.eq_thm - (@{thms add_numeral_left} @ - @{thms add_neg_numeral_left} @ - @{thms numeral_plus_numeral} @ - @{thms add_neg_numeral_simps}) simps; - -(*To evaluate binary negations of coefficients*) -val minus_simps = [@{thm minus_zero}, @{thm minus_minus}]; + @{thms add_numeral_left + add_neg_numeral_left + numeral_plus_numeral + add_neg_numeral_simps} simps; (*To let us treat subtraction as addition*) -val diff_simps = [@{thm diff_conv_add_uminus}, @{thm minus_add_distrib}, @{thm minus_minus}]; +val diff_simps = @{thms diff_conv_add_uminus minus_add_distrib minus_minus}; (*To let us treat division as multiplication*) -val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; +val divide_simps = @{thms divide_inverse inverse_mult_distrib inverse_inverse_eq}; (*to extract again any uncancelled minuses*) val minus_from_mult_simps = - [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}]; + @{thms minus_minus mult_minus_left mult_minus_right}; (*combine unary minus with numeric literals, however nested within a product*) val mult_minus_simps = - [@{thm mult.assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}, @{thm numeral_times_minus_swap}]; + @{thms mult.assoc minus_mult_right minus_mult_commute numeral_times_minus_swap}; val norm_ss1 = simpset_of (put_simpset num_ss \<^context> addsimps numeral_syms @ add_0s @ mult_1s @ - diff_simps @ minus_simps @ @{thms ac_simps}) + diff_simps @ @{thms minus_zero ac_simps}) val norm_ss2 = simpset_of (put_simpset num_ss \<^context> addsimps non_add_simps @ mult_minus_simps) val norm_ss3 = simpset_of (put_simpset num_ss \<^context> - addsimps minus_from_mult_simps @ @{thms ac_simps} @ @{thms ac_simps minus_mult_commute}) + addsimps minus_from_mult_simps @ @{thms ac_simps minus_mult_commute}) structure CancelNumeralsCommon = struct val mk_sum = mk_sum val dest_sum = dest_sum val mk_coeff = mk_coeff val dest_coeff = dest_coeff 1 val find_first_coeff = find_first_coeff [] val trans_tac = trans_tac fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) val numeral_simp_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps add_0s @ simps) + simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps val prove_conv = Arith_Data.prove_conv end; structure EqCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin \<^const_name>\HOL.eq\ dummyT val bal_add1 = @{thm eq_add_iff1} RS trans val bal_add2 = @{thm eq_add_iff2} RS trans ); structure LessCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val mk_bal = HOLogic.mk_binrel \<^const_name>\Orderings.less\ val dest_bal = HOLogic.dest_bin \<^const_name>\Orderings.less\ dummyT val bal_add1 = @{thm less_add_iff1} RS trans val bal_add2 = @{thm less_add_iff2} RS trans ); structure LeCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val mk_bal = HOLogic.mk_binrel \<^const_name>\Orderings.less_eq\ val dest_bal = HOLogic.dest_bin \<^const_name>\Orderings.less_eq\ dummyT val bal_add1 = @{thm le_add_iff1} RS trans val bal_add2 = @{thm le_add_iff2} RS trans ); val eq_cancel_numerals = EqCancelNumerals.proc val less_cancel_numerals = LessCancelNumerals.proc val le_cancel_numerals = LeCancelNumerals.proc structure CombineNumeralsData = struct type coeff = int val iszero = (fn x => x = 0) val add = op + val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) val dest_sum = dest_sum val mk_coeff = mk_coeff val dest_coeff = dest_coeff 1 val left_distrib = @{thm combine_common_factor} RS trans val prove_conv = Arith_Data.prove_conv_nohyps val trans_tac = trans_tac fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) val numeral_simp_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps add_0s @ simps) + simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps end; structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); (*Version for fields, where coefficients can be fractions*) structure FieldCombineNumeralsData = struct type coeff = int * int val iszero = (fn (p, _) => p = 0) val add = add_frac val mk_sum = long_mk_sum val dest_sum = dest_sum val mk_coeff = mk_fcoeff val dest_coeff = dest_fcoeff 1 val left_distrib = @{thm combine_common_factor} RS trans val prove_conv = Arith_Data.prove_conv_nohyps val trans_tac = trans_tac val norm_ss1a = - simpset_of (put_simpset norm_ss1 \<^context> addsimps inverse_1s @ divide_simps) + simpset_of (put_simpset norm_ss1 \<^context> addsimps (inverse_1s @ divide_simps)) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss1a ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) val numeral_simp_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps add_0s @ simps @ [@{thm add_frac_eq}, @{thm not_False_eq_True}]) + addsimps (simps @ @{thms add_frac_eq not_False_eq_True})) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq field_post_simps end; structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); val combine_numerals = CombineNumerals.proc val field_combine_numerals = FieldCombineNumerals.proc (** Constant folding for multiplication in semirings **) (*We do not need folding for addition: combine_numerals does the same thing*) structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = struct val assoc_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms ac_simps minus_mult_commute}) val eq_reflection = eq_reflection val is_numeral = can HOLogic.dest_number end; structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); fun assoc_fold ctxt ct = Semiring_Times_Assoc.proc ctxt (Thm.term_of ct) structure CancelNumeralFactorCommon = struct val mk_coeff = mk_coeff val dest_coeff = dest_coeff 1 val trans_tac = trans_tac val norm_ss1 = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps minus_from_mult_simps @ mult_1s) val norm_ss2 = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps @ mult_minus_simps) val norm_ss3 = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms ac_simps minus_mult_commute numeral_times_minus_swap}) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) (* simp_thms are necessary because some of the cancellation rules below (e.g. mult_less_cancel_left) introduce various logical connectives *) val numeral_simp_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps @ @{thms simp_thms}) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq - ([@{thm Nat.add_0}, @{thm Nat.add_0_right}] @ post_simps) + (@{thms Nat.add_0 Nat.add_0_right} @ post_simps) val prove_conv = Arith_Data.prove_conv end (*Version for semiring_div*) structure DivCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon val mk_bal = HOLogic.mk_binop \<^const_name>\Rings.divide\ val dest_bal = HOLogic.dest_bin \<^const_name>\Rings.divide\ dummyT val cancel = @{thm div_mult_mult1} RS trans val neg_exchanges = false ) (*Version for fields*) structure DivideCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon val mk_bal = HOLogic.mk_binop \<^const_name>\Rings.divide\ val dest_bal = HOLogic.dest_bin \<^const_name>\Rings.divide\ dummyT val cancel = @{thm mult_divide_mult_cancel_left} RS trans val neg_exchanges = false ) structure EqCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin \<^const_name>\HOL.eq\ dummyT val cancel = @{thm mult_cancel_left} RS trans val neg_exchanges = false ) structure LessCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon val mk_bal = HOLogic.mk_binrel \<^const_name>\Orderings.less\ val dest_bal = HOLogic.dest_bin \<^const_name>\Orderings.less\ dummyT val cancel = @{thm mult_less_cancel_left} RS trans val neg_exchanges = true ) structure LeCancelNumeralFactor = CancelNumeralFactorFun ( open CancelNumeralFactorCommon val mk_bal = HOLogic.mk_binrel \<^const_name>\Orderings.less_eq\ val dest_bal = HOLogic.dest_bin \<^const_name>\Orderings.less_eq\ dummyT val cancel = @{thm mult_le_cancel_left} RS trans val neg_exchanges = true ) val eq_cancel_numeral_factor = EqCancelNumeralFactor.proc val less_cancel_numeral_factor = LessCancelNumeralFactor.proc val le_cancel_numeral_factor = LeCancelNumeralFactor.proc val div_cancel_numeral_factor = DivCancelNumeralFactor.proc val divide_cancel_numeral_factor = DivideCancelNumeralFactor.proc val field_divide_cancel_numeral_factor = Simplifier.make_simproc \<^context> "field_divide_cancel_numeral_factor" {lhss = [\<^term>\((l::'a::field) * m) / n\, \<^term>\(l::'a::field) / (m * n)\, \<^term>\((numeral v)::'a::field) / (numeral w)\, \<^term>\((numeral v)::'a::field) / (- numeral w)\, \<^term>\((- numeral v)::'a::field) / (numeral w)\, \<^term>\((- numeral v)::'a::field) / (- numeral w)\], proc = K DivideCancelNumeralFactor.proc} val field_cancel_numeral_factors = [Simplifier.make_simproc \<^context> "field_eq_cancel_numeral_factor" {lhss = [\<^term>\(l::'a::field) * m = n\, \<^term>\(l::'a::field) = m * n\], proc = K EqCancelNumeralFactor.proc}, field_divide_cancel_numeral_factor] (** Declarations for ExtractCommonTerm **) (*Find first term that matches u*) fun find_first_t past u [] = raise TERM ("find_first_t", []) | find_first_t past u (t::terms) = if u aconv t then (rev past @ terms) else find_first_t (t::past) u terms handle TERM _ => find_first_t (t::past) u terms; (** Final simplification for the CancelFactor simprocs **) val simplify_one = Arith_Data.simplify_meta_eq [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_One}]; fun cancel_simplify_meta_eq ctxt cancel_th th = simplify_one ctxt (([th, cancel_th]) MRS trans); local val Tp_Eq = Thm.reflexive (Thm.cterm_of \<^theory_context>\HOL\ HOLogic.Trueprop) fun Eq_True_elim Eq = Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI} in fun sign_conv pos_th neg_th ctxt t = let val T = fastype_of t; val zero = Const(\<^const_name>\Groups.zero\, T); val less = Const(\<^const_name>\Orderings.less\, [T,T] ---> HOLogic.boolT); val pos = less $ zero $ t and neg = less $ t $ zero fun prove p = SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.cterm_of ctxt p))) handle THM _ => NONE in case prove pos of SOME th => SOME(th RS pos_th) | NONE => (case prove neg of SOME th => SOME(th RS neg_th) | NONE => NONE) end; end structure CancelFactorCommon = struct val mk_sum = long_mk_prod val dest_sum = dest_prod val mk_coeff = mk_coeff val dest_coeff = dest_coeff val find_first = find_first_t [] val trans_tac = trans_tac val norm_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps mult_1s @ @{thms ac_simps minus_mult_commute}) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt)) val simplify_meta_eq = cancel_simplify_meta_eq fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b)) end; (*mult_cancel_left requires a ring with no zero divisors.*) structure EqCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin \<^const_name>\HOL.eq\ dummyT fun simp_conv _ _ = SOME @{thm mult_cancel_left} ); (*for ordered rings*) structure LeCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val mk_bal = HOLogic.mk_binrel \<^const_name>\Orderings.less_eq\ val dest_bal = HOLogic.dest_bin \<^const_name>\Orderings.less_eq\ dummyT val simp_conv = sign_conv @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg} ); (*for ordered rings*) structure LessCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val mk_bal = HOLogic.mk_binrel \<^const_name>\Orderings.less\ val dest_bal = HOLogic.dest_bin \<^const_name>\Orderings.less\ dummyT val simp_conv = sign_conv @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg} ); (*for semirings with division*) structure DivCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val mk_bal = HOLogic.mk_binop \<^const_name>\Rings.divide\ val dest_bal = HOLogic.dest_bin \<^const_name>\Rings.divide\ dummyT fun simp_conv _ _ = SOME @{thm div_mult_mult1_if} ); structure ModCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val mk_bal = HOLogic.mk_binop \<^const_name>\modulo\ val dest_bal = HOLogic.dest_bin \<^const_name>\modulo\ dummyT fun simp_conv _ _ = SOME @{thm mod_mult_mult1} ); (*for idoms*) structure DvdCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val mk_bal = HOLogic.mk_binrel \<^const_name>\Rings.dvd\ val dest_bal = HOLogic.dest_bin \<^const_name>\Rings.dvd\ dummyT fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left} ); (*Version for all fields, including unordered ones (type complex).*) structure DivideCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val mk_bal = HOLogic.mk_binop \<^const_name>\Rings.divide\ val dest_bal = HOLogic.dest_bin \<^const_name>\Rings.divide\ dummyT fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if} ); fun eq_cancel_factor ctxt ct = EqCancelFactor.proc ctxt (Thm.term_of ct) fun le_cancel_factor ctxt ct = LeCancelFactor.proc ctxt (Thm.term_of ct) fun less_cancel_factor ctxt ct = LessCancelFactor.proc ctxt (Thm.term_of ct) fun div_cancel_factor ctxt ct = DivCancelFactor.proc ctxt (Thm.term_of ct) fun mod_cancel_factor ctxt ct = ModCancelFactor.proc ctxt (Thm.term_of ct) fun dvd_cancel_factor ctxt ct = DvdCancelFactor.proc ctxt (Thm.term_of ct) fun divide_cancel_factor ctxt ct = DivideCancelFactor.proc ctxt (Thm.term_of ct) local val cterm_of = Thm.cterm_of \<^context>; fun tvar S = (("'a", 0), S); val zero_tvar = tvar \<^sort>\zero\; val zero = cterm_of (Const (\<^const_name>\zero_class.zero\, TVar zero_tvar)); val type_tvar = tvar \<^sort>\type\; val geq = cterm_of (Const (\<^const_name>\HOL.eq\, TVar type_tvar --> TVar type_tvar --> \<^typ>\bool\)); -val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} -val add_frac_num = mk_meta_eq @{thm "add_frac_num"} -val add_num_frac = mk_meta_eq @{thm "add_num_frac"} +val add_frac_eq = mk_meta_eq @{thm add_frac_eq} +val add_frac_num = mk_meta_eq @{thm add_frac_num} +val add_num_frac = mk_meta_eq @{thm add_num_frac} fun prove_nz ctxt T t = let val z = Thm.instantiate_cterm (TVars.make [(zero_tvar, T)], Vars.empty) zero val eq = Thm.instantiate_cterm (TVars.make [(type_tvar, T)], Vars.empty) geq val th = Simplifier.rewrite (ctxt addsimps @{thms simp_thms}) (Thm.apply \<^cterm>\Trueprop\ (Thm.apply \<^cterm>\Not\ (Thm.apply (Thm.apply eq t) z))) in Thm.equal_elim (Thm.symmetric th) TrueI end fun proc ctxt ct = let val ((x,y),(w,z)) = (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z,w] val T = Thm.ctyp_of_cterm x val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z] val th = Thm.instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) end handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE fun proc2 ctxt ct = let val (l,r) = Thm.dest_binop ct val T = Thm.ctyp_of_cterm l in (case (Thm.term_of l, Thm.term_of r) of (Const(\<^const_name>\Rings.divide\,_)$_$_, _) => let val (x,y) = Thm.dest_binop l val z = r val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z] val ynz = prove_nz ctxt T y in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) end | (_, Const (\<^const_name>\Rings.divide\,_)$_$_) => let val (x,y) = Thm.dest_binop r val z = l val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z] val ynz = prove_nz ctxt T y in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) end | _ => NONE) end handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE fun is_number (Const(\<^const_name>\Rings.divide\,_)$a$b) = is_number a andalso is_number b | is_number t = can HOLogic.dest_number t val is_number = is_number o Thm.term_of fun proc3 ctxt ct = (case Thm.term_of ct of Const(\<^const_name>\Orderings.less\,_)$(Const(\<^const_name>\Rings.divide\,_)$_$_)$_ => let val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop val _ = map is_number [a,b,c] val T = Thm.ctyp_of_cterm c val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} in SOME (mk_meta_eq th) end | Const(\<^const_name>\Orderings.less_eq\,_)$(Const(\<^const_name>\Rings.divide\,_)$_$_)$_ => let val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop val _ = map is_number [a,b,c] val T = Thm.ctyp_of_cterm c val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} in SOME (mk_meta_eq th) end | Const(\<^const_name>\HOL.eq\,_)$(Const(\<^const_name>\Rings.divide\,_)$_$_)$_ => let val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop val _ = map is_number [a,b,c] val T = Thm.ctyp_of_cterm c val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} in SOME (mk_meta_eq th) end | Const(\<^const_name>\Orderings.less\,_)$_$(Const(\<^const_name>\Rings.divide\,_)$_$_) => let val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop val _ = map is_number [a,b,c] val T = Thm.ctyp_of_cterm c val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} in SOME (mk_meta_eq th) end | Const(\<^const_name>\Orderings.less_eq\,_)$_$(Const(\<^const_name>\Rings.divide\,_)$_$_) => let val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop val _ = map is_number [a,b,c] val T = Thm.ctyp_of_cterm c val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} in SOME (mk_meta_eq th) end | Const(\<^const_name>\HOL.eq\,_)$_$(Const(\<^const_name>\Rings.divide\,_)$_$_) => let val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop val _ = map is_number [a,b,c] val T = Thm.ctyp_of_cterm c val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} in SOME (mk_meta_eq th) end | _ => NONE) handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE val add_frac_frac_simproc = Simplifier.make_simproc \<^context> "add_frac_frac_simproc" {lhss = [\<^term>\(x::'a::field) / y + (w::'a::field) / z\], proc = K proc} val add_frac_num_simproc = Simplifier.make_simproc \<^context> "add_frac_num_simproc" {lhss = [\<^term>\(x::'a::field) / y + z\, \<^term>\z + (x::'a::field) / y\], proc = K proc2} val ord_frac_simproc = Simplifier.make_simproc \<^context> "ord_frac_simproc" {lhss = [\<^term>\(a::'a::{field,ord}) / b < c\, \<^term>\(a::'a::{field,ord}) / b \ c\, \<^term>\c < (a::'a::{field,ord}) / b\, \<^term>\c \ (a::'a::{field,ord}) / b\, \<^term>\c = (a::'a::{field,ord}) / b\, \<^term>\(a::'a::{field, ord}) / b = c\], proc = K proc3} -val ths = - [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, - @{thm "divide_numeral_1"}, - @{thm "div_by_0"}, @{thm div_0}, - @{thm "divide_divide_eq_left"}, - @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"}, - @{thm "times_divide_times_eq"}, - @{thm "divide_divide_eq_right"}, - @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"}, - @{thm "add_divide_distrib"} RS sym, - @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide}, - Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute})))) - (@{thm Fields.field_divide_inverse} RS sym)] - val field_comp_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms "semiring_norm"} - addsimps ths addsimps @{thms simp_thms} + addsimps @{thms semiring_norm + mult_numeral_1 + mult_numeral_1_right + divide_numeral_1 + div_by_0 + div_0 + divide_divide_eq_left + times_divide_eq_left + times_divide_eq_right + times_divide_times_eq + divide_divide_eq_right + diff_conv_add_uminus + minus_divide_left + add_divide_distrib [symmetric] + Fields.field_divide_inverse [symmetric] + inverse_divide + divide_inverse_commute [symmetric] + simp_thms} addsimprocs field_cancel_numeral_factors addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc] - |> Simplifier.add_cong @{thm "if_weak_cong"}) + |> Simplifier.add_cong @{thm if_weak_cong}) in fun field_comp_conv ctxt = Simplifier.rewrite (put_simpset field_comp_ss ctxt) then_conv - Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_One}]) + Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_One}) end end;