cancellation simprocs generalising the multiset simprocs
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Tue Feb 14 18:32:53 2017 +0100 (2017-02-14)
changeset 6502900731700e54f
parent 65028 87e003397834
child 65030 7fd4130cd0a4
cancellation simprocs generalising the multiset simprocs
src/HOL/Library/Cancellation.thy
src/HOL/Library/Cancellation/cancel.ML
src/HOL/Library/Cancellation/cancel_data.ML
src/HOL/Library/Cancellation/cancel_simprocs.ML
src/HOL/Library/Multiset.thy
src/HOL/Library/multiset_order_simprocs.ML
src/HOL/Library/multiset_simprocs.ML
src/HOL/Library/multiset_simprocs_util.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Cancellation.thy	Tue Feb 14 18:32:53 2017 +0100
     1.3 @@ -0,0 +1,101 @@
     1.4 +(*  Title:      HOL/Library/Cancellation.thy
     1.5 +    Author:     Mathias Fleury, MPII
     1.6 +    Copyright   2017
     1.7 +
     1.8 +This theory defines cancelation simprocs that work on cancel_comm_monoid_add and support the simplification of an operation
     1.9 +that repeats the additions.
    1.10 +*)
    1.11 +
    1.12 +theory Cancellation
    1.13 +imports Main
    1.14 +begin
    1.15 +
    1.16 +named_theorems cancelation_simproc_pre \<open>These theorems are here to normalise the term. Special
    1.17 +  handling of constructors should be here. Remark that only the simproc @{term NO_MATCH} is also
    1.18 +  included.\<close>
    1.19 +
    1.20 +named_theorems cancelation_simproc_post \<open>These theorems are here to normalise the term, after the
    1.21 +  cancelation simproc. Normalisation of \<open>iterate_add\<close> back to the normale representation
    1.22 +  should be put here.\<close>
    1.23 +
    1.24 +named_theorems cancelation_simproc_eq_elim \<open>These theorems are here to help deriving contradiction
    1.25 +  (e.g., \<open>Suc _ = 0\<close>).\<close>
    1.26 +
    1.27 +definition iterate_add :: \<open>nat \<Rightarrow> 'a::cancel_comm_monoid_add \<Rightarrow> 'a\<close> where
    1.28 +  \<open>iterate_add n a = ((op + a) ^^ n) 0\<close>
    1.29 +
    1.30 +lemma iterate_add_simps[simp]:
    1.31 +  \<open>iterate_add 0 a = 0\<close>
    1.32 +  \<open>iterate_add (Suc n) a = a + iterate_add n a\<close>
    1.33 +  unfolding iterate_add_def by auto
    1.34 +
    1.35 +lemma iterate_add_empty[simp]: \<open>iterate_add n 0 = 0\<close>
    1.36 +  unfolding iterate_add_def by (induction n) auto
    1.37 +
    1.38 +lemma iterate_add_distrib[simp]: \<open>iterate_add (m+n) a = iterate_add m a + iterate_add n a\<close>
    1.39 +  by (induction n) (auto simp: ac_simps)
    1.40 +
    1.41 +lemma iterate_add_Numeral1: \<open>iterate_add n Numeral1 = of_nat n\<close>
    1.42 +  by (induction n) auto
    1.43 +
    1.44 +lemma iterate_add_1: \<open>iterate_add n 1 = of_nat n\<close>
    1.45 +  by (induction n) auto
    1.46 +
    1.47 +lemma iterate_add_eq_add_iff1:
    1.48 +  \<open>i \<le> j \<Longrightarrow> (iterate_add j u + m = iterate_add i u + n) = (iterate_add (j - i) u + m = n)\<close>
    1.49 +  by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
    1.50 +
    1.51 +lemma iterate_add_eq_add_iff2:
    1.52 +   \<open>i \<le> j \<Longrightarrow> (iterate_add i u + m = iterate_add j u + n) = (m = iterate_add (j - i) u + n)\<close>
    1.53 +  by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
    1.54 +
    1.55 +lemma iterate_add_less_iff1:
    1.56 +  "j \<le> (i::nat) \<Longrightarrow> (iterate_add i (u:: 'a :: {cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m < iterate_add j u + n) = (iterate_add (i-j) u + m < n)"
    1.57 +  by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
    1.58 +
    1.59 +lemma iterate_add_less_iff2:
    1.60 +  "i \<le> (j::nat) \<Longrightarrow> (iterate_add i (u:: 'a :: {cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m < iterate_add j u + n) = (m <iterate_add (j - i) u + n)"
    1.61 +  by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
    1.62 +
    1.63 +lemma iterate_add_less_eq_iff1:
    1.64 +  "j \<le> (i::nat) \<Longrightarrow> (iterate_add i (u:: 'a :: {cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m \<le> iterate_add j u + n) = (iterate_add (i-j) u + m \<le> n)"
    1.65 +  by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
    1.66 +
    1.67 +lemma iterate_add_less_eq_iff2:
    1.68 +  "i \<le> (j::nat) \<Longrightarrow> (iterate_add i (u:: 'a :: {cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m \<le> iterate_add j u + n) = (m \<le> iterate_add (j - i) u + n)"
    1.69 +  by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
    1.70 +
    1.71 +lemma iterate_add_add_eq1:
    1.72 +  "j \<le> (i::nat) \<Longrightarrow> ((iterate_add i u + m) - (iterate_add j u + n)) = ((iterate_add (i-j) u + m) - n)"
    1.73 +  by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
    1.74 +
    1.75 +lemma iterate_add_diff_add_eq2:
    1.76 +  "i \<le> (j::nat) \<Longrightarrow> ((iterate_add i u + m) - (iterate_add j u + n)) = (m - (iterate_add (j-i) u + n))"
    1.77 +  by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
    1.78 +
    1.79 +
    1.80 +subsection \<open>Simproc Set-Up\<close>
    1.81 +
    1.82 +ML_file "Cancellation/cancel.ML"
    1.83 +ML_file "Cancellation/cancel_data.ML"
    1.84 +ML_file "Cancellation/cancel_simprocs.ML"
    1.85 +
    1.86 +simproc_setup comm_monoid_cancel_numerals
    1.87 +  ("(l::'a::cancel_comm_monoid_add) + m = n" | "l = m + n") =
    1.88 +  \<open>fn phi => Cancel_Simprocs.eq_cancel\<close>
    1.89 +
    1.90 +text \<open>Can we reduce the sorts?\<close>
    1.91 +simproc_setup comm_monoid_cancel_less_numerals
    1.92 +  ("(l::'a::{cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m < n" | "l < m + n") =
    1.93 +  \<open>fn phi => Cancel_Simprocs.less_cancel\<close>
    1.94 +
    1.95 +simproc_setup comm_monoid_cancel_less_eq_numerals
    1.96 +  ("(l::'a::{cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m \<le> n" | "l \<le> m + n") =
    1.97 +  \<open>fn phi => Cancel_Simprocs.less_eq_cancel\<close>
    1.98 +
    1.99 +simproc_setup comm_monoid_cancel_cancel_numerals
   1.100 +  ("((l::'a :: cancel_comm_monoid_add) + m) - n" | "l - (m + n)") =
   1.101 +  \<open>fn phi => Cancel_Simprocs.diff_cancel\<close>
   1.102 +
   1.103 +end
   1.104 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Cancellation/cancel.ML	Tue Feb 14 18:32:53 2017 +0100
     2.3 @@ -0,0 +1,89 @@
     2.4 +(*  Title:      Provers/Arith/cancel.ML
     2.5 +    Author:     Mathias Fleury, MPII
     2.6 +    Copyright   2017
     2.7 +
     2.8 +Based on:
     2.9 +
    2.10 +    Title:      Provers/Arith/cancel_numerals.ML
    2.11 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    2.12 +    Copyright   2000  University of Cambridge
    2.13 +
    2.14 +
    2.15 +This simproc allows handling of types with constructors (e.g., add_mset for multisets) and iteration
    2.16 +of the addition (e.g., repeat_mset for multisets).
    2.17 +
    2.18 +Beware that this simproc should not compete with any more specialised especially:
    2.19 +  - nat: the handling for Suc is more complicated than what can be done here
    2.20 +  - int: some normalisation is done (after the cancelation) and linarith relies on these.
    2.21 +
    2.22 +Instead of "*", we have "iterate_add".
    2.23 +
    2.24 +
    2.25 +To quote Provers/Arith/cancel_numerals.ML:
    2.26 +
    2.27 +    Cancel common coefficients in balanced expressions:
    2.28 +
    2.29 +         i + #m*u + j ~~ i' + #m'*u + j'  ==  #(m-m')*u + i + j ~~ i' + j'
    2.30 +
    2.31 +    where ~~ is an appropriate balancing operation (e.g. =, <=, <, -).
    2.32 +
    2.33 +    It works by (a) massaging both sides to bring the selected term to the front:
    2.34 +
    2.35 +         #m*u + (i + j) ~~ #m'*u + (i' + j')
    2.36 +
    2.37 +    (b) then using bal_add1 or bal_add2 to reach
    2.38 +
    2.39 +         #(m-m')*u + i + j ~~ i' + j'       (if m'<=m)
    2.40 +
    2.41 +    or
    2.42 +
    2.43 +         i + j ~~ #(m'-m)*u + i' + j'       (otherwise)
    2.44 +*)
    2.45 +
    2.46 +signature CANCEL =
    2.47 +sig
    2.48 +  val proc: Proof.context -> cterm -> thm option
    2.49 +end;
    2.50 +
    2.51 +functor Cancel_Fun(Data: CANCEL_NUMERALS_DATA): CANCEL =
    2.52 +struct
    2.53 +
    2.54 +structure Cancel_Numerals_Fun = CancelNumeralsFun(open Data)
    2.55 +exception SORT_NOT_GENERAL_ENOUGH of string * typ * term
    2.56 +(*the simplification procedure*)
    2.57 +fun proc ctxt ct =
    2.58 +  let
    2.59 +    val t = Thm.term_of ct
    2.60 +    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
    2.61 +    val pre_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt addsimps
    2.62 +      Named_Theorems.get ctxt @{named_theorems cancelation_simproc_pre} addsimprocs
    2.63 +      [@{simproc NO_MATCH}]) (Thm.cterm_of ctxt t');
    2.64 +    val t' = Thm.term_of (Thm.rhs_of pre_simplified_ct)
    2.65 +    val export = singleton (Variable.export ctxt' ctxt)
    2.66 +
    2.67 +    val (t1,_) = Data.dest_bal t'
    2.68 +    val sort_not_general_enough = ((fastype_of t1) = @{typ nat}) orelse
    2.69 +        Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt))
    2.70 +         (fastype_of t1, @{sort "comm_ring_1"})
    2.71 +    val _ =
    2.72 +       if sort_not_general_enough
    2.73 +       then raise SORT_NOT_GENERAL_ENOUGH("type too precise, another simproc should do the job",
    2.74 +          fastype_of t1, t1)
    2.75 +       else ()
    2.76 +    val canceled_thm = Cancel_Numerals_Fun.proc ctxt (Thm.rhs_of pre_simplified_ct)
    2.77 +    fun add_pre_simplification thm = @{thm Pure.transitive} OF [pre_simplified_ct, thm]
    2.78 +    fun add_post_simplification thm =
    2.79 +      (let val post_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt addsimps
    2.80 +              Named_Theorems.get ctxt @{named_theorems cancelation_simproc_post} addsimprocs
    2.81 +              [@{simproc NO_MATCH}])
    2.82 +            (Thm.rhs_of thm)
    2.83 +        in @{thm Pure.transitive} OF [thm, post_simplified_ct] end)
    2.84 +  in
    2.85 +    Option.map (export o add_post_simplification o add_pre_simplification) canceled_thm
    2.86 +  end
    2.87 +  (* FIXME avoid handling of generic exceptions *)
    2.88 +  handle TERM _ => NONE
    2.89 +       | TYPE _ => NONE
    2.90 +       | SORT_NOT_GENERAL_ENOUGH _ => NONE
    2.91 +
    2.92 +end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Cancellation/cancel_data.ML	Tue Feb 14 18:32:53 2017 +0100
     3.3 @@ -0,0 +1,176 @@
     3.4 +(*  Title:      Provers/Arith/cancel_data.ML
     3.5 +    Author:     Mathias Fleury, MPII
     3.6 +    Copyright   2017
     3.7 +
     3.8 +Based on:
     3.9 +    Title:      Tools/nat_numeral_simprocs.ML
    3.10 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    3.11 +
    3.12 +Datastructure for the cancelation simprocs.
    3.13 +
    3.14 +*)
    3.15 +signature CANCEL_DATA =
    3.16 +sig
    3.17 +  val mk_sum : typ -> term list -> term
    3.18 +  val dest_sum : term -> term list
    3.19 +  val mk_coeff : int * term -> term
    3.20 +  val dest_coeff : term -> int * term
    3.21 +  val find_first_coeff : term -> term list -> int * term list
    3.22 +  val trans_tac : Proof.context -> thm option -> tactic
    3.23 +
    3.24 +  val norm_ss1 : simpset
    3.25 +  val norm_ss2: simpset
    3.26 +  val norm_tac: Proof.context -> tactic
    3.27 +
    3.28 +  val numeral_simp_tac : Proof.context -> tactic
    3.29 +  val simplify_meta_eq : Proof.context -> thm -> thm
    3.30 +  val prove_conv : tactic list -> Proof.context -> thm list -> term * term -> thm option
    3.31 +end;
    3.32 +
    3.33 +structure Cancel_Data : CANCEL_DATA =
    3.34 +struct
    3.35 +
    3.36 +(*** Utilities ***)
    3.37 +
    3.38 +(*No reordering of the arguments.*)
    3.39 +fun fast_mk_iterate_add (n, mset) =
    3.40 +  let val T = fastype_of mset
    3.41 +  in
    3.42 +    Const (@{const_name "iterate_add"}, @{typ nat} --> T --> T) $ n $ mset
    3.43 +  end;
    3.44 +
    3.45 +(*iterate_add is not symmetric, unlike multiplication over natural numbers.*)
    3.46 +fun mk_iterate_add (t, u) =
    3.47 +  (if fastype_of t = @{typ nat} then (t, u) else (u, t))
    3.48 +  |> fast_mk_iterate_add;
    3.49 +
    3.50 +(*Maps n to #n for n = 1, 2*)
    3.51 +val numeral_syms =
    3.52 +  map (fn th => th RS sym) @{thms numeral_One numeral_2_eq_2 numeral_1_eq_Suc_0};
    3.53 +
    3.54 +val numeral_sym_ss =
    3.55 +  simpset_of (put_simpset HOL_basic_ss @{context} addsimps numeral_syms);
    3.56 +
    3.57 +fun mk_number 1 = HOLogic.numeral_const HOLogic.natT $ HOLogic.one_const
    3.58 +  | mk_number n = HOLogic.mk_number HOLogic.natT n;
    3.59 +fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
    3.60 +
    3.61 +fun find_first_numeral past (t::terms) =
    3.62 +    ((dest_number t, t, rev past @ terms)
    3.63 +    handle TERM _ => find_first_numeral (t::past) terms)
    3.64 +  | find_first_numeral _ [] = raise TERM("find_first_numeral", []);
    3.65 +
    3.66 +fun typed_zero T = Const (@{const_name "Groups.zero"}, T);
    3.67 +fun typed_one T = HOLogic.numeral_const T $ HOLogic.one_const
    3.68 +val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    3.69 +
    3.70 +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero.*)
    3.71 +fun mk_sum T [] = typed_zero T
    3.72 +  | mk_sum _ [t,u] = mk_plus (t, u)
    3.73 +  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
    3.74 +
    3.75 +val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} dummyT;
    3.76 +
    3.77 +
    3.78 +(*** Other simproc items ***)
    3.79 +
    3.80 +val bin_simps =
    3.81 +  (@{thm numeral_One} RS sym) ::
    3.82 +  @{thms add_numeral_left diff_nat_numeral diff_0_eq_0 mult_numeral_left(1)
    3.83 +      if_True if_False not_False_eq_True nat_0 nat_numeral nat_neg_numeral iterate_add_simps(1)
    3.84 +      iterate_add_empty arith_simps rel_simps of_nat_numeral};
    3.85 +
    3.86 +
    3.87 +(*** CancelNumerals simprocs ***)
    3.88 +
    3.89 +val one = mk_number 1;
    3.90 +
    3.91 +fun mk_prod T [] = typed_one T
    3.92 +  | mk_prod _ [t] = t
    3.93 +  | mk_prod T (t :: ts) = if t = one then mk_prod T ts else mk_iterate_add (t, mk_prod T ts);
    3.94 +
    3.95 +val dest_iterate_add = HOLogic.dest_bin @{const_name iterate_add} dummyT;
    3.96 +
    3.97 +fun dest_iterate_adds t =
    3.98 +  let val (t,u) = dest_iterate_add t in
    3.99 +    t :: dest_iterate_adds u end
   3.100 +  handle TERM _ => [t];
   3.101 +
   3.102 +fun mk_coeff (k,t) = mk_iterate_add (mk_number k, t);
   3.103 +
   3.104 +(*Express t as a product of (possibly) a numeral with other factors, sorted*)
   3.105 +fun dest_coeff t =
   3.106 +  let
   3.107 +    val T = fastype_of t
   3.108 +    val ts = sort Term_Ord.term_ord (dest_iterate_adds t);
   3.109 +    val (n, _, ts') =
   3.110 +      find_first_numeral [] ts
   3.111 +      handle TERM _ => (1, one, ts);
   3.112 +  in (n, mk_prod T ts') end;
   3.113 +
   3.114 +(*Find first coefficient-term THAT MATCHES u*)
   3.115 +fun find_first_coeff _ _ [] = raise TERM("find_first_coeff", [])
   3.116 +  | find_first_coeff past u (t::terms) =
   3.117 +    let val (n,u') = dest_coeff t in
   3.118 +      if u aconv u' then (n, rev past @ terms) else find_first_coeff (t::past) u terms end
   3.119 +    handle TERM _ => find_first_coeff (t::past) u terms;
   3.120 +
   3.121 +(*
   3.122 +  Split up a sum into the list of its constituent terms.
   3.123 +*)
   3.124 +fun dest_summation (t, ts) =
   3.125 +    let val (t1,t2) = dest_plus t in
   3.126 +      dest_summation (t1, dest_summation (t2, ts)) end
   3.127 +    handle TERM _ => t :: ts;
   3.128 +
   3.129 +fun dest_sum t = dest_summation (t, []);
   3.130 +
   3.131 +val rename_numerals = simplify (put_simpset numeral_sym_ss @{context}) o Thm.transfer @{theory};
   3.132 +
   3.133 +(*Simplify \<open>iterate_add (Suc 0) n\<close>, \<open>iterate_add n (Suc 0)\<close>, \<open>n+0\<close>, and \<open>0+n\<close> to \<open>n\<close>*)
   3.134 +val add_0s  = map rename_numerals @{thms monoid_add_class.add_0_left monoid_add_class.add_0_right};
   3.135 +val mult_1s = map rename_numerals @{thms iterate_add_1 iterate_add_simps(2)[of 0]};
   3.136 +
   3.137 +(*And these help the simproc return False when appropriate. We use the same list as the
   3.138 +simproc for natural numbers, but adapted.*)
   3.139 +fun contra_rules ctxt =
   3.140 +  @{thms le_zero_eq}  @ Named_Theorems.get ctxt @{named_theorems cancelation_simproc_eq_elim};
   3.141 +
   3.142 +fun simplify_meta_eq ctxt =
   3.143 +  Arith_Data.simplify_meta_eq
   3.144 +    (@{thms numeral_1_eq_Suc_0 Nat.add_0_right
   3.145 +         mult_0 mult_0_right mult_1 mult_1_right iterate_add_Numeral1 of_nat_numeral
   3.146 +         monoid_add_class.add_0_left iterate_add_simps(1) monoid_add_class.add_0_right
   3.147 +         iterate_add_Numeral1} @
   3.148 +     contra_rules ctxt) ctxt;
   3.149 +
   3.150 +val mk_sum = mk_sum;
   3.151 +val dest_sum = dest_sum;
   3.152 +val mk_coeff = mk_coeff;
   3.153 +val dest_coeff = dest_coeff;
   3.154 +val find_first_coeff = find_first_coeff [];
   3.155 +val trans_tac = Numeral_Simprocs.trans_tac;
   3.156 +
   3.157 +val norm_ss1 =
   3.158 +  simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps
   3.159 +    numeral_syms @ add_0s @ mult_1s @ @{thms ac_simps iterate_add_simps});
   3.160 +
   3.161 +val norm_ss2 =
   3.162 +  simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps
   3.163 +    bin_simps @
   3.164 +    @{thms ac_simps});
   3.165 +
   3.166 +fun norm_tac ctxt =
   3.167 +  ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
   3.168 +  THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt));
   3.169 +
   3.170 +val mset_simps_ss =
   3.171 +  simpset_of (put_simpset HOL_basic_ss @{context} addsimps bin_simps);
   3.172 +
   3.173 +fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset mset_simps_ss ctxt));
   3.174 +
   3.175 +val simplify_meta_eq = simplify_meta_eq;
   3.176 +val prove_conv = Arith_Data.prove_conv;
   3.177 +
   3.178 +end
   3.179 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Cancellation/cancel_simprocs.ML	Tue Feb 14 18:32:53 2017 +0100
     4.3 @@ -0,0 +1,60 @@
     4.4 +(*  Title:      Provers/Arith/cancel_simprocs.ML
     4.5 +    Author:     Mathias Fleury, MPII
     4.6 +    Copyright   2017
     4.7 +
     4.8 +Base on:
     4.9 +    Title:      Provers/Arith/nat_numeral_simprocs.ML
    4.10 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    4.11 +
    4.12 +Cancelation simprocs declaration.
    4.13 +*)
    4.14 +
    4.15 +signature CANCEL_SIMPROCS =
    4.16 +sig
    4.17 +  val eq_cancel: Proof.context -> cterm -> thm option
    4.18 +  val less_cancel: Proof.context -> cterm -> thm option
    4.19 +  val less_eq_cancel: Proof.context -> cterm -> thm option
    4.20 +  val diff_cancel: Proof.context -> cterm -> thm option
    4.21 +end;
    4.22 +
    4.23 +structure Cancel_Simprocs : CANCEL_SIMPROCS =
    4.24 +struct
    4.25 +
    4.26 +structure Eq_Cancel_Comm_Monoid_add = Cancel_Fun
    4.27 + (open Cancel_Data
    4.28 +  val mk_bal   = HOLogic.mk_eq
    4.29 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
    4.30 +  val bal_add1 = @{thm iterate_add_eq_add_iff1} RS trans
    4.31 +  val bal_add2 = @{thm iterate_add_eq_add_iff2} RS trans
    4.32 +);
    4.33 +
    4.34 +structure Eq_Cancel_Comm_Monoid_less = Cancel_Fun
    4.35 + (open Cancel_Data
    4.36 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
    4.37 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
    4.38 +  val bal_add1 = @{thm iterate_add_less_iff1} RS trans
    4.39 +  val bal_add2 = @{thm iterate_add_less_iff2} RS trans
    4.40 +);
    4.41 +
    4.42 +structure Eq_Cancel_Comm_Monoid_less_eq = Cancel_Fun
    4.43 + (open Cancel_Data
    4.44 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
    4.45 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
    4.46 +  val bal_add1 = @{thm iterate_add_less_eq_iff1} RS trans
    4.47 +  val bal_add2 = @{thm iterate_add_less_eq_iff2} RS trans
    4.48 +);
    4.49 +
    4.50 +structure Diff_Cancel_Comm_Monoid_less_eq = Cancel_Fun
    4.51 + (open Cancel_Data
    4.52 +  val mk_bal   = HOLogic.mk_binop @{const_name Groups.minus}
    4.53 +  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} dummyT
    4.54 +  val bal_add1 = @{thm iterate_add_add_eq1} RS trans
    4.55 +  val bal_add2 = @{thm iterate_add_diff_add_eq2} RS trans
    4.56 +);
    4.57 +
    4.58 +val eq_cancel = Eq_Cancel_Comm_Monoid_add.proc;
    4.59 +val less_cancel = Eq_Cancel_Comm_Monoid_less.proc;
    4.60 +val less_eq_cancel = Eq_Cancel_Comm_Monoid_less_eq.proc;
    4.61 +val diff_cancel = Diff_Cancel_Comm_Monoid_less_eq.proc;
    4.62 +
    4.63 +end
     5.1 --- a/src/HOL/Library/Multiset.thy	Mon Feb 13 16:03:55 2017 +0100
     5.2 +++ b/src/HOL/Library/Multiset.thy	Tue Feb 14 18:32:53 2017 +0100
     5.3 @@ -9,7 +9,7 @@
     5.4  section \<open>(Finite) multisets\<close>
     5.5  
     5.6  theory Multiset
     5.7 -imports Main
     5.8 +imports Cancellation
     5.9  begin
    5.10  
    5.11  subsection \<open>The type of multisets\<close>
    5.12 @@ -972,15 +972,33 @@
    5.13    "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (m \<subset># repeat_mset (j-i) u + n)"
    5.14    unfolding subset_mset_def by (simp add: mset_eq_add_iff2 mset_subseteq_add_iff2)
    5.15  
    5.16 -ML_file "multiset_simprocs_util.ML"
    5.17 +lemma repeat_mset_iterate_add: \<open>repeat_mset n M = iterate_add n M\<close>
    5.18 +  unfolding iterate_add_def by (induction n) auto
    5.19 +
    5.20  ML_file "multiset_simprocs.ML"
    5.21  
    5.22 +lemma add_mset_replicate_mset_safe[cancelation_simproc_pre]: \<open>NO_MATCH {#} M \<Longrightarrow> add_mset a M = {#a#} + M\<close>
    5.23 +  by simp
    5.24 +
    5.25 +declare repeat_mset_iterate_add[cancelation_simproc_pre]
    5.26 +
    5.27 +declare iterate_add_distrib[cancelation_simproc_pre]
    5.28 +declare repeat_mset_iterate_add[symmetric, cancelation_simproc_post]
    5.29 +
    5.30 +declare add_mset_not_empty[cancelation_simproc_eq_elim]
    5.31 +    empty_not_add_mset[cancelation_simproc_eq_elim]
    5.32 +    subset_mset.le_zero_eq[cancelation_simproc_eq_elim]
    5.33 +    empty_not_add_mset[cancelation_simproc_eq_elim]
    5.34 +    add_mset_not_empty[cancelation_simproc_eq_elim]
    5.35 +    subset_mset.le_zero_eq[cancelation_simproc_eq_elim]
    5.36 +    le_zero_eq[cancelation_simproc_eq_elim]
    5.37 +
    5.38  simproc_setup mseteq_cancel
    5.39    ("(l::'a multiset) + m = n" | "(l::'a multiset) = m + n" |
    5.40     "add_mset a m = n" | "m = add_mset a n" |
    5.41     "replicate_mset p a = n" | "m = replicate_mset p a" |
    5.42     "repeat_mset p m = n" | "m = repeat_mset p m") =
    5.43 -  \<open>fn phi => Multiset_Simprocs.eq_cancel_msets\<close>
    5.44 +  \<open>fn phi => Cancel_Simprocs.eq_cancel\<close>
    5.45  
    5.46  simproc_setup msetsubset_cancel
    5.47    ("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
    5.48 @@ -1001,7 +1019,7 @@
    5.49     "add_mset a m - n" | "m - add_mset a n" |
    5.50     "replicate_mset p r - n" | "m - replicate_mset p r" |
    5.51     "repeat_mset p m - n" | "m - repeat_mset p m") =
    5.52 -  \<open>fn phi => Multiset_Simprocs.diff_cancel_msets\<close>
    5.53 +  \<open>fn phi => Cancel_Simprocs.diff_cancel\<close>
    5.54  
    5.55  
    5.56  subsubsection \<open>Conditionally complete lattice\<close>
     6.1 --- a/src/HOL/Library/multiset_order_simprocs.ML	Mon Feb 13 16:03:55 2017 +0100
     6.2 +++ b/src/HOL/Library/multiset_order_simprocs.ML	Tue Feb 14 18:32:53 2017 +0100
     6.3 @@ -13,20 +13,20 @@
     6.4  structure Multiset_Order_Simprocs : MULTISET_ORDER_SIMPROCS =
     6.5  struct
     6.6  
     6.7 -structure LessCancelMultiset = CancelNumeralsFun
     6.8 - (open Multiset_Cancel_Common
     6.9 +structure LessCancelMultiset = Cancel_Fun
    6.10 + (open Cancel_Data
    6.11    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
    6.12    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
    6.13 -  val bal_add1 = @{thm mset_less_add_iff1} RS trans
    6.14 -  val bal_add2 = @{thm mset_less_add_iff2} RS trans
    6.15 +  val bal_add1 = @{thm mset_less_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
    6.16 +  val bal_add2 = @{thm mset_less_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
    6.17  );
    6.18  
    6.19 -structure LeCancelMultiset = CancelNumeralsFun
    6.20 - (open Multiset_Cancel_Common
    6.21 +structure LeCancelMultiset = Cancel_Fun
    6.22 + (open Cancel_Data
    6.23    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
    6.24    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
    6.25 -  val bal_add1 = @{thm mset_le_add_iff1} RS trans
    6.26 -  val bal_add2 = @{thm mset_le_add_iff2} RS trans
    6.27 +  val bal_add1 = @{thm mset_le_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
    6.28 +  val bal_add2 = @{thm mset_le_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
    6.29  );
    6.30  
    6.31  val less_cancel_msets = LessCancelMultiset.proc;
     7.1 --- a/src/HOL/Library/multiset_simprocs.ML	Mon Feb 13 16:03:55 2017 +0100
     7.2 +++ b/src/HOL/Library/multiset_simprocs.ML	Tue Feb 14 18:32:53 2017 +0100
     7.3 @@ -7,50 +7,30 @@
     7.4  
     7.5  signature MULTISET_SIMPROCS =
     7.6  sig
     7.7 -  val eq_cancel_msets: Proof.context -> cterm -> thm option
     7.8    val subset_cancel_msets: Proof.context -> cterm -> thm option
     7.9    val subseteq_cancel_msets: Proof.context -> cterm -> thm option
    7.10 -  val diff_cancel_msets: Proof.context -> cterm -> thm option
    7.11  end;
    7.12  
    7.13  structure Multiset_Simprocs : MULTISET_SIMPROCS =
    7.14  struct
    7.15  
    7.16 -structure EqCancelMultiset = CancelNumeralsFun
    7.17 - (open Multiset_Cancel_Common
    7.18 -  val mk_bal   = HOLogic.mk_eq
    7.19 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
    7.20 -  val bal_add1 = @{thm mset_eq_add_iff1} RS trans
    7.21 -  val bal_add2 = @{thm mset_eq_add_iff2} RS trans
    7.22 -);
    7.23 -
    7.24 -structure SubsetCancelMultiset = CancelNumeralsFun
    7.25 - (open Multiset_Cancel_Common
    7.26 +structure Subset_Cancel_Multiset = Cancel_Fun
    7.27 + (open Cancel_Data
    7.28    val mk_bal   = HOLogic.mk_binrel @{const_name subset_mset}
    7.29    val dest_bal = HOLogic.dest_bin @{const_name subset_mset} dummyT
    7.30 -  val bal_add1 = @{thm mset_subset_add_iff1} RS trans
    7.31 -  val bal_add2 = @{thm mset_subset_add_iff2} RS trans
    7.32 +  val bal_add1 = @{thm mset_subset_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
    7.33 +  val bal_add2 = @{thm mset_subset_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
    7.34  );
    7.35  
    7.36 -structure SubseteqCancelMultiset = CancelNumeralsFun
    7.37 - (open Multiset_Cancel_Common
    7.38 +structure Subseteq_Cancel_Multiset = Cancel_Fun
    7.39 + (open Cancel_Data
    7.40    val mk_bal   = HOLogic.mk_binrel @{const_name subseteq_mset}
    7.41    val dest_bal = HOLogic.dest_bin @{const_name subseteq_mset} dummyT
    7.42 -  val bal_add1 = @{thm mset_subseteq_add_iff1} RS trans
    7.43 -  val bal_add2 = @{thm mset_subseteq_add_iff2} RS trans
    7.44 +  val bal_add1 = @{thm mset_subseteq_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
    7.45 +  val bal_add2 = @{thm mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
    7.46  );
    7.47  
    7.48 -structure DiffCancelMultiset = CancelNumeralsFun
    7.49 - (open Multiset_Cancel_Common
    7.50 -  val mk_bal   = HOLogic.mk_binop @{const_name Groups.minus}
    7.51 -  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} dummyT
    7.52 -  val bal_add1 = @{thm mset_diff_add_eq1} RS trans
    7.53 -  val bal_add2 = @{thm mset_diff_add_eq2} RS trans
    7.54 -);
    7.55 -
    7.56 -val eq_cancel_msets = EqCancelMultiset.proc;
    7.57 -val subset_cancel_msets = SubsetCancelMultiset.proc;
    7.58 -val subseteq_cancel_msets = SubseteqCancelMultiset.proc;
    7.59 -val diff_cancel_msets = DiffCancelMultiset.proc;
    7.60 +val subset_cancel_msets = Subset_Cancel_Multiset.proc;
    7.61 +val subseteq_cancel_msets = Subseteq_Cancel_Multiset.proc;
    7.62  
    7.63  end
     8.1 --- a/src/HOL/Library/multiset_simprocs_util.ML	Mon Feb 13 16:03:55 2017 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,183 +0,0 @@
     8.4 -(* Author: Mathias Fleury, MPII
     8.5 -
     8.6 -
     8.7 -Datatructure for the cancelation simprocs for multisets, based on Larry Paulson's simprocs for
     8.8 -natural numbers and numerals.
     8.9 -*)
    8.10 -signature MULTISET_CANCEL_COMMON =
    8.11 -sig
    8.12 -  val mk_sum : typ -> term list -> term
    8.13 -  val dest_sum : term -> term list
    8.14 -  val mk_coeff : int * term -> term
    8.15 -  val dest_coeff : term -> int * term
    8.16 -  val find_first_coeff : term -> term list -> int * term list
    8.17 -  val trans_tac : Proof.context -> thm option -> tactic
    8.18 -
    8.19 -  val norm_ss1 : simpset
    8.20 -  val norm_ss2: simpset
    8.21 -  val norm_tac: Proof.context -> tactic
    8.22 -
    8.23 -  val numeral_simp_tac : Proof.context -> tactic
    8.24 -  val simplify_meta_eq : Proof.context -> thm -> thm
    8.25 -  val prove_conv : tactic list -> Proof.context -> thm list -> term * term -> thm option
    8.26 -end;
    8.27 -
    8.28 -structure Multiset_Cancel_Common : MULTISET_CANCEL_COMMON =
    8.29 -struct
    8.30 -
    8.31 -(*** Utilities ***)
    8.32 -
    8.33 -(*No reordering of the arguments.*)
    8.34 -fun fast_mk_repeat_mset (n, mset) =
    8.35 -  let val T = fastype_of mset in
    8.36 -    Const (@{const_name "repeat_mset"}, @{typ nat} --> T --> T) $ n $ mset
    8.37 -  end;
    8.38 -
    8.39 -(*repeat_mset is not symmetric, unlike multiplication over natural numbers.*)
    8.40 -fun mk_repeat_mset (t, u) =
    8.41 -  (if fastype_of t = @{typ nat} then (t, u) else (u, t))
    8.42 -  |> fast_mk_repeat_mset;
    8.43 -
    8.44 -(*Maps n to #n for n = 1, 2*)
    8.45 -val numeral_syms =
    8.46 -  map (fn th => th RS sym) @{thms numeral_One numeral_2_eq_2 numeral_1_eq_Suc_0};
    8.47 -
    8.48 -val numeral_sym_ss =
    8.49 -  simpset_of (put_simpset HOL_basic_ss @{context} addsimps numeral_syms);
    8.50 -
    8.51 -fun mk_number 1 = HOLogic.numeral_const HOLogic.natT $ HOLogic.one_const
    8.52 -  | mk_number n = HOLogic.mk_number HOLogic.natT n;
    8.53 -fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
    8.54 -
    8.55 -fun find_first_numeral past (t::terms) =
    8.56 -    ((dest_number t, t, rev past @ terms)
    8.57 -    handle TERM _ => find_first_numeral (t::past) terms)
    8.58 -  | find_first_numeral _ [] = raise TERM("find_first_numeral", []);
    8.59 -
    8.60 -fun typed_zero T = Const (@{const_name "Groups.zero"}, T);
    8.61 -val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    8.62 -
    8.63 -(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero.*)
    8.64 -fun mk_sum T [] = typed_zero T
    8.65 -  | mk_sum _ [t,u] = mk_plus (t, u)
    8.66 -  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
    8.67 -
    8.68 -val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} dummyT;
    8.69 -
    8.70 -
    8.71 -(*** Other simproc items ***)
    8.72 -
    8.73 -val bin_simps =
    8.74 -  (@{thm numeral_One} RS sym) ::
    8.75 -  @{thms add_numeral_left diff_nat_numeral diff_0_eq_0 mult_numeral_left(1)
    8.76 -      if_True if_False not_False_eq_True
    8.77 -      nat_0 nat_numeral nat_neg_numeral add_mset_commute repeat_mset.simps(1)
    8.78 -      replicate_mset_0 repeat_mset_empty
    8.79 -      arith_simps rel_simps};
    8.80 -
    8.81 -
    8.82 -(*** CancelNumerals simprocs ***)
    8.83 -
    8.84 -val one = mk_number 1;
    8.85 -
    8.86 -fun mk_prod [] = one
    8.87 -  | mk_prod [t] = t
    8.88 -  | mk_prod (t :: ts) = if t = one then mk_prod ts else mk_repeat_mset (t, mk_prod ts);
    8.89 -
    8.90 -val dest_repeat_mset = HOLogic.dest_bin @{const_name repeat_mset} dummyT;
    8.91 -
    8.92 -fun dest_repeat_msets t =
    8.93 -  let val (t,u) = dest_repeat_mset t in
    8.94 -    t :: dest_repeat_msets u end
    8.95 -  handle TERM _ => [t];
    8.96 -
    8.97 -fun mk_coeff (k,t) = mk_repeat_mset (mk_number k, t);
    8.98 -
    8.99 -(*Express t as a product of (possibly) a numeral with other factors, sorted*)
   8.100 -fun dest_coeff t =
   8.101 -  let
   8.102 -    val ts = sort Term_Ord.term_ord (dest_repeat_msets t);
   8.103 -    val (n, _, ts') =
   8.104 -      find_first_numeral [] ts
   8.105 -      handle TERM _ => (1, one, ts);
   8.106 -  in (n, mk_prod ts') end;
   8.107 -
   8.108 -(*Find first coefficient-term THAT MATCHES u*)
   8.109 -fun find_first_coeff _ _ [] = raise TERM("find_first_coeff", [])
   8.110 -  | find_first_coeff past u (t::terms) =
   8.111 -    let val (n,u') = dest_coeff t in
   8.112 -      if u aconv u' then (n, rev past @ terms) else find_first_coeff (t::past) u terms end
   8.113 -    handle TERM _ => find_first_coeff (t::past) u terms;
   8.114 -
   8.115 -(*
   8.116 -  Split up a sum into the list of its constituent terms, on the way replace:
   8.117 -  * the \<open>add_mset a C\<close> by \<open>add_mset a {#}\<close> and \<open>C\<close>, iff C was not already the empty set;
   8.118 -  * the \<open>replicate_mset n a\<close> by \<open>repeat_mset n {#a#}\<close>.
   8.119 -*)
   8.120 -fun dest_add_mset (Const (@{const_name add_mset}, T) $ a $
   8.121 -      Const (@{const_name "Groups.zero_class.zero"}, U), ts) =
   8.122 -    Const (@{const_name add_mset}, T) $ a $ typed_zero U :: ts
   8.123 -  | dest_add_mset (Const (@{const_name add_mset}, T) $ a $ mset, ts) =
   8.124 -    dest_add_mset (mset, Const (@{const_name add_mset}, T) $ a $
   8.125 -      typed_zero (fastype_of mset) :: ts)
   8.126 -  | dest_add_mset (Const (@{const_name replicate_mset},
   8.127 -      Type (_, [_, Type (_, [T, U])])) $ n $ a, ts) =
   8.128 -    let val single_a = Const (@{const_name add_mset}, T --> U --> U) $ a $ typed_zero U in
   8.129 -      fast_mk_repeat_mset (n, single_a) :: ts end
   8.130 -  | dest_add_mset (t, ts) =
   8.131 -    let val (t1,t2) = dest_plus t in
   8.132 -      dest_add_mset (t1, dest_add_mset (t2, ts)) end
   8.133 -    handle TERM _ => t :: ts;
   8.134 -
   8.135 -fun dest_add_mset_sum t = dest_add_mset (t, []);
   8.136 -
   8.137 -val rename_numerals = simplify (put_simpset numeral_sym_ss @{context}) o Thm.transfer @{theory};
   8.138 -
   8.139 -(*Simplify \<open>repeat_mset (Suc 0) n\<close>, \<open>n+0\<close>, and \<open>0+n\<close> to \<open>n\<close>*)
   8.140 -val add_0s  = map rename_numerals @{thms Groups.add_0 Groups.add_0_right};
   8.141 -val mult_1s = map rename_numerals @{thms repeat_mset.simps(2)[of 0]};
   8.142 -
   8.143 -
   8.144 -(*And these help the simproc return False when appropriate. We use the same list as the
   8.145 -simproc for natural numbers, but adapted to multisets.*)
   8.146 -val contra_rules =
   8.147 -  @{thms union_mset_add_mset_left union_mset_add_mset_right
   8.148 -      empty_not_add_mset add_mset_not_empty subset_mset.le_zero_eq le_zero_eq};
   8.149 -
   8.150 -val simplify_meta_eq =
   8.151 -  Arith_Data.simplify_meta_eq
   8.152 -    (@{thms numeral_1_eq_Suc_0 Nat.add_0_right
   8.153 -         mult_0 mult_0_right mult_1 mult_1_right
   8.154 -         Groups.add_0 repeat_mset.simps(1) monoid_add_class.add_0_right} @
   8.155 -     contra_rules);
   8.156 -
   8.157 -val mk_sum = mk_sum;
   8.158 -val dest_sum = dest_add_mset_sum;
   8.159 -val mk_coeff = mk_coeff;
   8.160 -val dest_coeff = dest_coeff;
   8.161 -val find_first_coeff = find_first_coeff [];
   8.162 -val trans_tac = Numeral_Simprocs.trans_tac;
   8.163 -
   8.164 -val norm_ss1 =
   8.165 -  simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps
   8.166 -    numeral_syms @ add_0s @ mult_1s @ @{thms ac_simps});
   8.167 -
   8.168 -val norm_ss2 =
   8.169 -  simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps
   8.170 -    bin_simps @
   8.171 -    @{thms union_mset_add_mset_left union_mset_add_mset_right
   8.172 -        repeat_mset_replicate_mset ac_simps});
   8.173 -
   8.174 -fun norm_tac ctxt =
   8.175 -  ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
   8.176 -  THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt));
   8.177 -
   8.178 -val mset_simps_ss =
   8.179 -  simpset_of (put_simpset HOL_basic_ss @{context} addsimps bin_simps);
   8.180 -
   8.181 -fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset mset_simps_ss ctxt));
   8.182 -
   8.183 -val simplify_meta_eq = simplify_meta_eq;
   8.184 -val prove_conv = Arith_Data.prove_conv;
   8.185 -
   8.186 -end