# HG changeset patch # User fleury # Date 1487093573 -3600 # Node ID 00731700e54f067ecf897e565cc9259b3b044d46 # Parent 87e003397834ef8f8c2532951d78c74470eff0d5 cancellation simprocs generalising the multiset simprocs diff -r 87e003397834 -r 00731700e54f src/HOL/Library/Cancellation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Cancellation.thy Tue Feb 14 18:32:53 2017 +0100 @@ -0,0 +1,101 @@ +(* Title: HOL/Library/Cancellation.thy + Author: Mathias Fleury, MPII + Copyright 2017 + +This theory defines cancelation simprocs that work on cancel_comm_monoid_add and support the simplification of an operation +that repeats the additions. +*) + +theory Cancellation +imports Main +begin + +named_theorems cancelation_simproc_pre \These theorems are here to normalise the term. Special + handling of constructors should be here. Remark that only the simproc @{term NO_MATCH} is also + included.\ + +named_theorems cancelation_simproc_post \These theorems are here to normalise the term, after the + cancelation simproc. Normalisation of \iterate_add\ back to the normale representation + should be put here.\ + +named_theorems cancelation_simproc_eq_elim \These theorems are here to help deriving contradiction + (e.g., \Suc _ = 0\).\ + +definition iterate_add :: \nat \ 'a::cancel_comm_monoid_add \ 'a\ where + \iterate_add n a = ((op + a) ^^ n) 0\ + +lemma iterate_add_simps[simp]: + \iterate_add 0 a = 0\ + \iterate_add (Suc n) a = a + iterate_add n a\ + unfolding iterate_add_def by auto + +lemma iterate_add_empty[simp]: \iterate_add n 0 = 0\ + unfolding iterate_add_def by (induction n) auto + +lemma iterate_add_distrib[simp]: \iterate_add (m+n) a = iterate_add m a + iterate_add n a\ + by (induction n) (auto simp: ac_simps) + +lemma iterate_add_Numeral1: \iterate_add n Numeral1 = of_nat n\ + by (induction n) auto + +lemma iterate_add_1: \iterate_add n 1 = of_nat n\ + by (induction n) auto + +lemma iterate_add_eq_add_iff1: + \i \ j \ (iterate_add j u + m = iterate_add i u + n) = (iterate_add (j - i) u + m = n)\ + by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1)) + +lemma iterate_add_eq_add_iff2: + \i \ j \ (iterate_add i u + m = iterate_add j u + n) = (m = iterate_add (j - i) u + n)\ + by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1)) + +lemma iterate_add_less_iff1: + "j \ (i::nat) \ (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)" + by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1)) + +lemma iterate_add_less_iff2: + "i \ (j::nat) \ (iterate_add i (u:: 'a :: {cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m < iterate_add j u + n) = (m (i::nat) \ (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)" + by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1)) + +lemma iterate_add_less_eq_iff2: + "i \ (j::nat) \ (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)" + by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1)) + +lemma iterate_add_add_eq1: + "j \ (i::nat) \ ((iterate_add i u + m) - (iterate_add j u + n)) = ((iterate_add (i-j) u + m) - n)" + by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1)) + +lemma iterate_add_diff_add_eq2: + "i \ (j::nat) \ ((iterate_add i u + m) - (iterate_add j u + n)) = (m - (iterate_add (j-i) u + n))" + by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1)) + + +subsection \Simproc Set-Up\ + +ML_file "Cancellation/cancel.ML" +ML_file "Cancellation/cancel_data.ML" +ML_file "Cancellation/cancel_simprocs.ML" + +simproc_setup comm_monoid_cancel_numerals + ("(l::'a::cancel_comm_monoid_add) + m = n" | "l = m + n") = + \fn phi => Cancel_Simprocs.eq_cancel\ + +text \Can we reduce the sorts?\ +simproc_setup comm_monoid_cancel_less_numerals + ("(l::'a::{cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m < n" | "l < m + n") = + \fn phi => Cancel_Simprocs.less_cancel\ + +simproc_setup comm_monoid_cancel_less_eq_numerals + ("(l::'a::{cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m \ n" | "l \ m + n") = + \fn phi => Cancel_Simprocs.less_eq_cancel\ + +simproc_setup comm_monoid_cancel_cancel_numerals + ("((l::'a :: cancel_comm_monoid_add) + m) - n" | "l - (m + n)") = + \fn phi => Cancel_Simprocs.diff_cancel\ + +end + diff -r 87e003397834 -r 00731700e54f src/HOL/Library/Cancellation/cancel.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Cancellation/cancel.ML Tue Feb 14 18:32:53 2017 +0100 @@ -0,0 +1,89 @@ +(* Title: Provers/Arith/cancel.ML + Author: Mathias Fleury, MPII + Copyright 2017 + +Based on: + + Title: Provers/Arith/cancel_numerals.ML + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2000 University of Cambridge + + +This simproc allows handling of types with constructors (e.g., add_mset for multisets) and iteration +of the addition (e.g., repeat_mset for multisets). + +Beware that this simproc should not compete with any more specialised especially: + - nat: the handling for Suc is more complicated than what can be done here + - int: some normalisation is done (after the cancelation) and linarith relies on these. + +Instead of "*", we have "iterate_add". + + +To quote Provers/Arith/cancel_numerals.ML: + + Cancel common coefficients in balanced expressions: + + i + #m*u + j ~~ i' + #m'*u + j' == #(m-m')*u + i + j ~~ i' + j' + + where ~~ is an appropriate balancing operation (e.g. =, <=, <, -). + + It works by (a) massaging both sides to bring the selected term to the front: + + #m*u + (i + j) ~~ #m'*u + (i' + j') + + (b) then using bal_add1 or bal_add2 to reach + + #(m-m')*u + i + j ~~ i' + j' (if m'<=m) + + or + + i + j ~~ #(m'-m)*u + i' + j' (otherwise) +*) + +signature CANCEL = +sig + val proc: Proof.context -> cterm -> thm option +end; + +functor Cancel_Fun(Data: CANCEL_NUMERALS_DATA): CANCEL = +struct + +structure Cancel_Numerals_Fun = CancelNumeralsFun(open Data) +exception SORT_NOT_GENERAL_ENOUGH of string * typ * term +(*the simplification procedure*) +fun proc ctxt ct = + let + val t = Thm.term_of ct + val ([t'], ctxt') = Variable.import_terms true [t] ctxt + val pre_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt addsimps + Named_Theorems.get ctxt @{named_theorems cancelation_simproc_pre} addsimprocs + [@{simproc NO_MATCH}]) (Thm.cterm_of ctxt t'); + val t' = Thm.term_of (Thm.rhs_of pre_simplified_ct) + val export = singleton (Variable.export ctxt' ctxt) + + val (t1,_) = Data.dest_bal t' + val sort_not_general_enough = ((fastype_of t1) = @{typ nat}) orelse + Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) + (fastype_of t1, @{sort "comm_ring_1"}) + val _ = + if sort_not_general_enough + then raise SORT_NOT_GENERAL_ENOUGH("type too precise, another simproc should do the job", + fastype_of t1, t1) + else () + val canceled_thm = Cancel_Numerals_Fun.proc ctxt (Thm.rhs_of pre_simplified_ct) + fun add_pre_simplification thm = @{thm Pure.transitive} OF [pre_simplified_ct, thm] + fun add_post_simplification thm = + (let val post_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt addsimps + Named_Theorems.get ctxt @{named_theorems cancelation_simproc_post} addsimprocs + [@{simproc NO_MATCH}]) + (Thm.rhs_of thm) + in @{thm Pure.transitive} OF [thm, post_simplified_ct] end) + in + Option.map (export o add_post_simplification o add_pre_simplification) canceled_thm + end + (* FIXME avoid handling of generic exceptions *) + handle TERM _ => NONE + | TYPE _ => NONE + | SORT_NOT_GENERAL_ENOUGH _ => NONE + +end; diff -r 87e003397834 -r 00731700e54f src/HOL/Library/Cancellation/cancel_data.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Cancellation/cancel_data.ML Tue Feb 14 18:32:53 2017 +0100 @@ -0,0 +1,176 @@ +(* Title: Provers/Arith/cancel_data.ML + Author: Mathias Fleury, MPII + Copyright 2017 + +Based on: + Title: Tools/nat_numeral_simprocs.ML + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + +Datastructure for the cancelation simprocs. + +*) +signature CANCEL_DATA = +sig + val mk_sum : typ -> term list -> term + val dest_sum : term -> term list + val mk_coeff : int * term -> term + val dest_coeff : term -> int * term + val find_first_coeff : term -> term list -> int * term list + val trans_tac : Proof.context -> thm option -> tactic + + val norm_ss1 : simpset + val norm_ss2: simpset + val norm_tac: Proof.context -> tactic + + val numeral_simp_tac : Proof.context -> tactic + val simplify_meta_eq : Proof.context -> thm -> thm + val prove_conv : tactic list -> Proof.context -> thm list -> term * term -> thm option +end; + +structure Cancel_Data : CANCEL_DATA = +struct + +(*** Utilities ***) + +(*No reordering of the arguments.*) +fun fast_mk_iterate_add (n, mset) = + let val T = fastype_of mset + in + Const (@{const_name "iterate_add"}, @{typ nat} --> T --> T) $ n $ mset + end; + +(*iterate_add is not symmetric, unlike multiplication over natural numbers.*) +fun mk_iterate_add (t, u) = + (if fastype_of t = @{typ nat} then (t, u) else (u, t)) + |> fast_mk_iterate_add; + +(*Maps n to #n for n = 1, 2*) +val numeral_syms = + map (fn th => th RS sym) @{thms numeral_One numeral_2_eq_2 numeral_1_eq_Suc_0}; + +val numeral_sym_ss = + simpset_of (put_simpset HOL_basic_ss @{context} addsimps numeral_syms); + +fun mk_number 1 = HOLogic.numeral_const HOLogic.natT $ HOLogic.one_const + | mk_number n = HOLogic.mk_number HOLogic.natT n; +fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); + +fun find_first_numeral past (t::terms) = + ((dest_number t, t, rev past @ terms) + handle TERM _ => find_first_numeral (t::past) terms) + | find_first_numeral _ [] = raise TERM("find_first_numeral", []); + +fun typed_zero T = Const (@{const_name "Groups.zero"}, T); +fun typed_one T = HOLogic.numeral_const T $ HOLogic.one_const +val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; + +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero.*) +fun mk_sum T [] = typed_zero T + | mk_sum _ [t,u] = mk_plus (t, u) + | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); + +val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} dummyT; + + +(*** Other simproc items ***) + +val bin_simps = + (@{thm numeral_One} RS sym) :: + @{thms add_numeral_left diff_nat_numeral diff_0_eq_0 mult_numeral_left(1) + if_True if_False not_False_eq_True nat_0 nat_numeral nat_neg_numeral iterate_add_simps(1) + iterate_add_empty arith_simps rel_simps of_nat_numeral}; + + +(*** CancelNumerals simprocs ***) + +val one = mk_number 1; + +fun mk_prod T [] = typed_one T + | mk_prod _ [t] = t + | mk_prod T (t :: ts) = if t = one then mk_prod T ts else mk_iterate_add (t, mk_prod T ts); + +val dest_iterate_add = HOLogic.dest_bin @{const_name iterate_add} dummyT; + +fun dest_iterate_adds t = + let val (t,u) = dest_iterate_add t in + t :: dest_iterate_adds u end + handle TERM _ => [t]; + +fun mk_coeff (k,t) = mk_iterate_add (mk_number k, t); + +(*Express t as a product of (possibly) a numeral with other factors, sorted*) +fun dest_coeff t = + let + val T = fastype_of t + val ts = sort Term_Ord.term_ord (dest_iterate_adds t); + val (n, _, ts') = + find_first_numeral [] ts + handle TERM _ => (1, one, ts); + in (n, mk_prod T ts') end; + +(*Find first coefficient-term THAT MATCHES u*) +fun find_first_coeff _ _ [] = raise TERM("find_first_coeff", []) + | find_first_coeff past u (t::terms) = + let val (n,u') = dest_coeff 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; + +(* + Split up a sum into the list of its constituent terms. +*) +fun dest_summation (t, ts) = + let val (t1,t2) = dest_plus t in + dest_summation (t1, dest_summation (t2, ts)) end + handle TERM _ => t :: ts; + +fun dest_sum t = dest_summation (t, []); + +val rename_numerals = simplify (put_simpset numeral_sym_ss @{context}) o Thm.transfer @{theory}; + +(*Simplify \iterate_add (Suc 0) n\, \iterate_add n (Suc 0)\, \n+0\, and \0+n\ to \n\*) +val add_0s = map rename_numerals @{thms monoid_add_class.add_0_left monoid_add_class.add_0_right}; +val mult_1s = map rename_numerals @{thms iterate_add_1 iterate_add_simps(2)[of 0]}; + +(*And these help the simproc return False when appropriate. We use the same list as the +simproc for natural numbers, but adapted.*) +fun contra_rules ctxt = + @{thms le_zero_eq} @ Named_Theorems.get ctxt @{named_theorems cancelation_simproc_eq_elim}; + +fun simplify_meta_eq ctxt = + Arith_Data.simplify_meta_eq + (@{thms numeral_1_eq_Suc_0 Nat.add_0_right + mult_0 mult_0_right mult_1 mult_1_right iterate_add_Numeral1 of_nat_numeral + monoid_add_class.add_0_left iterate_add_simps(1) monoid_add_class.add_0_right + iterate_add_Numeral1} @ + contra_rules ctxt) ctxt; + +val mk_sum = mk_sum; +val dest_sum = dest_sum; +val mk_coeff = mk_coeff; +val dest_coeff = dest_coeff; +val find_first_coeff = find_first_coeff []; +val trans_tac = Numeral_Simprocs.trans_tac; + +val norm_ss1 = + simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps + numeral_syms @ add_0s @ mult_1s @ @{thms ac_simps iterate_add_simps}); + +val norm_ss2 = + simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps + bin_simps @ + @{thms ac_simps}); + +fun norm_tac ctxt = + ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) + THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)); + +val mset_simps_ss = + simpset_of (put_simpset HOL_basic_ss @{context} addsimps bin_simps); + +fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset mset_simps_ss ctxt)); + +val simplify_meta_eq = simplify_meta_eq; +val prove_conv = Arith_Data.prove_conv; + +end + diff -r 87e003397834 -r 00731700e54f src/HOL/Library/Cancellation/cancel_simprocs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Cancellation/cancel_simprocs.ML Tue Feb 14 18:32:53 2017 +0100 @@ -0,0 +1,60 @@ +(* Title: Provers/Arith/cancel_simprocs.ML + Author: Mathias Fleury, MPII + Copyright 2017 + +Base on: + Title: Provers/Arith/nat_numeral_simprocs.ML + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + +Cancelation simprocs declaration. +*) + +signature CANCEL_SIMPROCS = +sig + val eq_cancel: Proof.context -> cterm -> thm option + val less_cancel: Proof.context -> cterm -> thm option + val less_eq_cancel: Proof.context -> cterm -> thm option + val diff_cancel: Proof.context -> cterm -> thm option +end; + +structure Cancel_Simprocs : CANCEL_SIMPROCS = +struct + +structure Eq_Cancel_Comm_Monoid_add = Cancel_Fun + (open Cancel_Data + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT + val bal_add1 = @{thm iterate_add_eq_add_iff1} RS trans + val bal_add2 = @{thm iterate_add_eq_add_iff2} RS trans +); + +structure Eq_Cancel_Comm_Monoid_less = Cancel_Fun + (open Cancel_Data + 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 iterate_add_less_iff1} RS trans + val bal_add2 = @{thm iterate_add_less_iff2} RS trans +); + +structure Eq_Cancel_Comm_Monoid_less_eq = Cancel_Fun + (open Cancel_Data + 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 iterate_add_less_eq_iff1} RS trans + val bal_add2 = @{thm iterate_add_less_eq_iff2} RS trans +); + +structure Diff_Cancel_Comm_Monoid_less_eq = Cancel_Fun + (open Cancel_Data + val mk_bal = HOLogic.mk_binop @{const_name Groups.minus} + val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} dummyT + val bal_add1 = @{thm iterate_add_add_eq1} RS trans + val bal_add2 = @{thm iterate_add_diff_add_eq2} RS trans +); + +val eq_cancel = Eq_Cancel_Comm_Monoid_add.proc; +val less_cancel = Eq_Cancel_Comm_Monoid_less.proc; +val less_eq_cancel = Eq_Cancel_Comm_Monoid_less_eq.proc; +val diff_cancel = Diff_Cancel_Comm_Monoid_less_eq.proc; + +end diff -r 87e003397834 -r 00731700e54f src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Feb 13 16:03:55 2017 +0100 +++ b/src/HOL/Library/Multiset.thy Tue Feb 14 18:32:53 2017 +0100 @@ -9,7 +9,7 @@ section \(Finite) multisets\ theory Multiset -imports Main +imports Cancellation begin subsection \The type of multisets\ @@ -972,15 +972,33 @@ "i \ (j::nat) \ (repeat_mset i u + m \# repeat_mset j u + n) = (m \# repeat_mset (j-i) u + n)" unfolding subset_mset_def by (simp add: mset_eq_add_iff2 mset_subseteq_add_iff2) -ML_file "multiset_simprocs_util.ML" +lemma repeat_mset_iterate_add: \repeat_mset n M = iterate_add n M\ + unfolding iterate_add_def by (induction n) auto + ML_file "multiset_simprocs.ML" +lemma add_mset_replicate_mset_safe[cancelation_simproc_pre]: \NO_MATCH {#} M \ add_mset a M = {#a#} + M\ + by simp + +declare repeat_mset_iterate_add[cancelation_simproc_pre] + +declare iterate_add_distrib[cancelation_simproc_pre] +declare repeat_mset_iterate_add[symmetric, cancelation_simproc_post] + +declare add_mset_not_empty[cancelation_simproc_eq_elim] + empty_not_add_mset[cancelation_simproc_eq_elim] + subset_mset.le_zero_eq[cancelation_simproc_eq_elim] + empty_not_add_mset[cancelation_simproc_eq_elim] + add_mset_not_empty[cancelation_simproc_eq_elim] + subset_mset.le_zero_eq[cancelation_simproc_eq_elim] + le_zero_eq[cancelation_simproc_eq_elim] + simproc_setup mseteq_cancel ("(l::'a multiset) + m = n" | "(l::'a multiset) = m + n" | "add_mset a m = n" | "m = add_mset a n" | "replicate_mset p a = n" | "m = replicate_mset p a" | "repeat_mset p m = n" | "m = repeat_mset p m") = - \fn phi => Multiset_Simprocs.eq_cancel_msets\ + \fn phi => Cancel_Simprocs.eq_cancel\ simproc_setup msetsubset_cancel ("(l::'a multiset) + m \# n" | "(l::'a multiset) \# m + n" | @@ -1001,7 +1019,7 @@ "add_mset a m - n" | "m - add_mset a n" | "replicate_mset p r - n" | "m - replicate_mset p r" | "repeat_mset p m - n" | "m - repeat_mset p m") = - \fn phi => Multiset_Simprocs.diff_cancel_msets\ + \fn phi => Cancel_Simprocs.diff_cancel\ subsubsection \Conditionally complete lattice\ diff -r 87e003397834 -r 00731700e54f src/HOL/Library/multiset_order_simprocs.ML --- a/src/HOL/Library/multiset_order_simprocs.ML Mon Feb 13 16:03:55 2017 +0100 +++ b/src/HOL/Library/multiset_order_simprocs.ML Tue Feb 14 18:32:53 2017 +0100 @@ -13,20 +13,20 @@ structure Multiset_Order_Simprocs : MULTISET_ORDER_SIMPROCS = struct -structure LessCancelMultiset = CancelNumeralsFun - (open Multiset_Cancel_Common +structure LessCancelMultiset = Cancel_Fun + (open Cancel_Data 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 mset_less_add_iff1} RS trans - val bal_add2 = @{thm mset_less_add_iff2} RS trans + val bal_add1 = @{thm mset_less_add_iff1[unfolded repeat_mset_iterate_add]} RS trans + val bal_add2 = @{thm mset_less_add_iff2[unfolded repeat_mset_iterate_add]} RS trans ); -structure LeCancelMultiset = CancelNumeralsFun - (open Multiset_Cancel_Common +structure LeCancelMultiset = Cancel_Fun + (open Cancel_Data 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 mset_le_add_iff1} RS trans - val bal_add2 = @{thm mset_le_add_iff2} RS trans + val bal_add1 = @{thm mset_le_add_iff1[unfolded repeat_mset_iterate_add]} RS trans + val bal_add2 = @{thm mset_le_add_iff2[unfolded repeat_mset_iterate_add]} RS trans ); val less_cancel_msets = LessCancelMultiset.proc; diff -r 87e003397834 -r 00731700e54f src/HOL/Library/multiset_simprocs.ML --- a/src/HOL/Library/multiset_simprocs.ML Mon Feb 13 16:03:55 2017 +0100 +++ b/src/HOL/Library/multiset_simprocs.ML Tue Feb 14 18:32:53 2017 +0100 @@ -7,50 +7,30 @@ signature MULTISET_SIMPROCS = sig - val eq_cancel_msets: Proof.context -> cterm -> thm option val subset_cancel_msets: Proof.context -> cterm -> thm option val subseteq_cancel_msets: Proof.context -> cterm -> thm option - val diff_cancel_msets: Proof.context -> cterm -> thm option end; structure Multiset_Simprocs : MULTISET_SIMPROCS = struct -structure EqCancelMultiset = CancelNumeralsFun - (open Multiset_Cancel_Common - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT - val bal_add1 = @{thm mset_eq_add_iff1} RS trans - val bal_add2 = @{thm mset_eq_add_iff2} RS trans -); - -structure SubsetCancelMultiset = CancelNumeralsFun - (open Multiset_Cancel_Common +structure Subset_Cancel_Multiset = Cancel_Fun + (open Cancel_Data val mk_bal = HOLogic.mk_binrel @{const_name subset_mset} val dest_bal = HOLogic.dest_bin @{const_name subset_mset} dummyT - val bal_add1 = @{thm mset_subset_add_iff1} RS trans - val bal_add2 = @{thm mset_subset_add_iff2} RS trans + val bal_add1 = @{thm mset_subset_add_iff1[unfolded repeat_mset_iterate_add]} RS trans + val bal_add2 = @{thm mset_subset_add_iff2[unfolded repeat_mset_iterate_add]} RS trans ); -structure SubseteqCancelMultiset = CancelNumeralsFun - (open Multiset_Cancel_Common +structure Subseteq_Cancel_Multiset = Cancel_Fun + (open Cancel_Data val mk_bal = HOLogic.mk_binrel @{const_name subseteq_mset} val dest_bal = HOLogic.dest_bin @{const_name subseteq_mset} dummyT - val bal_add1 = @{thm mset_subseteq_add_iff1} RS trans - val bal_add2 = @{thm mset_subseteq_add_iff2} RS trans + val bal_add1 = @{thm mset_subseteq_add_iff1[unfolded repeat_mset_iterate_add]} RS trans + val bal_add2 = @{thm mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add]} RS trans ); -structure DiffCancelMultiset = CancelNumeralsFun - (open Multiset_Cancel_Common - val mk_bal = HOLogic.mk_binop @{const_name Groups.minus} - val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} dummyT - val bal_add1 = @{thm mset_diff_add_eq1} RS trans - val bal_add2 = @{thm mset_diff_add_eq2} RS trans -); - -val eq_cancel_msets = EqCancelMultiset.proc; -val subset_cancel_msets = SubsetCancelMultiset.proc; -val subseteq_cancel_msets = SubseteqCancelMultiset.proc; -val diff_cancel_msets = DiffCancelMultiset.proc; +val subset_cancel_msets = Subset_Cancel_Multiset.proc; +val subseteq_cancel_msets = Subseteq_Cancel_Multiset.proc; end diff -r 87e003397834 -r 00731700e54f src/HOL/Library/multiset_simprocs_util.ML --- a/src/HOL/Library/multiset_simprocs_util.ML Mon Feb 13 16:03:55 2017 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,183 +0,0 @@ -(* Author: Mathias Fleury, MPII - - -Datatructure for the cancelation simprocs for multisets, based on Larry Paulson's simprocs for -natural numbers and numerals. -*) -signature MULTISET_CANCEL_COMMON = -sig - val mk_sum : typ -> term list -> term - val dest_sum : term -> term list - val mk_coeff : int * term -> term - val dest_coeff : term -> int * term - val find_first_coeff : term -> term list -> int * term list - val trans_tac : Proof.context -> thm option -> tactic - - val norm_ss1 : simpset - val norm_ss2: simpset - val norm_tac: Proof.context -> tactic - - val numeral_simp_tac : Proof.context -> tactic - val simplify_meta_eq : Proof.context -> thm -> thm - val prove_conv : tactic list -> Proof.context -> thm list -> term * term -> thm option -end; - -structure Multiset_Cancel_Common : MULTISET_CANCEL_COMMON = -struct - -(*** Utilities ***) - -(*No reordering of the arguments.*) -fun fast_mk_repeat_mset (n, mset) = - let val T = fastype_of mset in - Const (@{const_name "repeat_mset"}, @{typ nat} --> T --> T) $ n $ mset - end; - -(*repeat_mset is not symmetric, unlike multiplication over natural numbers.*) -fun mk_repeat_mset (t, u) = - (if fastype_of t = @{typ nat} then (t, u) else (u, t)) - |> fast_mk_repeat_mset; - -(*Maps n to #n for n = 1, 2*) -val numeral_syms = - map (fn th => th RS sym) @{thms numeral_One numeral_2_eq_2 numeral_1_eq_Suc_0}; - -val numeral_sym_ss = - simpset_of (put_simpset HOL_basic_ss @{context} addsimps numeral_syms); - -fun mk_number 1 = HOLogic.numeral_const HOLogic.natT $ HOLogic.one_const - | mk_number n = HOLogic.mk_number HOLogic.natT n; -fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); - -fun find_first_numeral past (t::terms) = - ((dest_number t, t, rev past @ terms) - handle TERM _ => find_first_numeral (t::past) terms) - | find_first_numeral _ [] = raise TERM("find_first_numeral", []); - -fun typed_zero T = Const (@{const_name "Groups.zero"}, T); -val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; - -(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero.*) -fun mk_sum T [] = typed_zero T - | mk_sum _ [t,u] = mk_plus (t, u) - | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); - -val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} dummyT; - - -(*** Other simproc items ***) - -val bin_simps = - (@{thm numeral_One} RS sym) :: - @{thms add_numeral_left diff_nat_numeral diff_0_eq_0 mult_numeral_left(1) - if_True if_False not_False_eq_True - nat_0 nat_numeral nat_neg_numeral add_mset_commute repeat_mset.simps(1) - replicate_mset_0 repeat_mset_empty - arith_simps rel_simps}; - - -(*** CancelNumerals simprocs ***) - -val one = mk_number 1; - -fun mk_prod [] = one - | mk_prod [t] = t - | mk_prod (t :: ts) = if t = one then mk_prod ts else mk_repeat_mset (t, mk_prod ts); - -val dest_repeat_mset = HOLogic.dest_bin @{const_name repeat_mset} dummyT; - -fun dest_repeat_msets t = - let val (t,u) = dest_repeat_mset t in - t :: dest_repeat_msets u end - handle TERM _ => [t]; - -fun mk_coeff (k,t) = mk_repeat_mset (mk_number k, t); - -(*Express t as a product of (possibly) a numeral with other factors, sorted*) -fun dest_coeff t = - let - val ts = sort Term_Ord.term_ord (dest_repeat_msets t); - val (n, _, ts') = - find_first_numeral [] ts - handle TERM _ => (1, one, ts); - in (n, mk_prod ts') end; - -(*Find first coefficient-term THAT MATCHES u*) -fun find_first_coeff _ _ [] = raise TERM("find_first_coeff", []) - | find_first_coeff past u (t::terms) = - let val (n,u') = dest_coeff 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; - -(* - Split up a sum into the list of its constituent terms, on the way replace: - * the \add_mset a C\ by \add_mset a {#}\ and \C\, iff C was not already the empty set; - * the \replicate_mset n a\ by \repeat_mset n {#a#}\. -*) -fun dest_add_mset (Const (@{const_name add_mset}, T) $ a $ - Const (@{const_name "Groups.zero_class.zero"}, U), ts) = - Const (@{const_name add_mset}, T) $ a $ typed_zero U :: ts - | dest_add_mset (Const (@{const_name add_mset}, T) $ a $ mset, ts) = - dest_add_mset (mset, Const (@{const_name add_mset}, T) $ a $ - typed_zero (fastype_of mset) :: ts) - | dest_add_mset (Const (@{const_name replicate_mset}, - Type (_, [_, Type (_, [T, U])])) $ n $ a, ts) = - let val single_a = Const (@{const_name add_mset}, T --> U --> U) $ a $ typed_zero U in - fast_mk_repeat_mset (n, single_a) :: ts end - | dest_add_mset (t, ts) = - let val (t1,t2) = dest_plus t in - dest_add_mset (t1, dest_add_mset (t2, ts)) end - handle TERM _ => t :: ts; - -fun dest_add_mset_sum t = dest_add_mset (t, []); - -val rename_numerals = simplify (put_simpset numeral_sym_ss @{context}) o Thm.transfer @{theory}; - -(*Simplify \repeat_mset (Suc 0) n\, \n+0\, and \0+n\ to \n\*) -val add_0s = map rename_numerals @{thms Groups.add_0 Groups.add_0_right}; -val mult_1s = map rename_numerals @{thms repeat_mset.simps(2)[of 0]}; - - -(*And these help the simproc return False when appropriate. We use the same list as the -simproc for natural numbers, but adapted to multisets.*) -val contra_rules = - @{thms union_mset_add_mset_left union_mset_add_mset_right - empty_not_add_mset add_mset_not_empty subset_mset.le_zero_eq le_zero_eq}; - -val simplify_meta_eq = - Arith_Data.simplify_meta_eq - (@{thms numeral_1_eq_Suc_0 Nat.add_0_right - mult_0 mult_0_right mult_1 mult_1_right - Groups.add_0 repeat_mset.simps(1) monoid_add_class.add_0_right} @ - contra_rules); - -val mk_sum = mk_sum; -val dest_sum = dest_add_mset_sum; -val mk_coeff = mk_coeff; -val dest_coeff = dest_coeff; -val find_first_coeff = find_first_coeff []; -val trans_tac = Numeral_Simprocs.trans_tac; - -val norm_ss1 = - simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps - numeral_syms @ add_0s @ mult_1s @ @{thms ac_simps}); - -val norm_ss2 = - simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps - bin_simps @ - @{thms union_mset_add_mset_left union_mset_add_mset_right - repeat_mset_replicate_mset ac_simps}); - -fun norm_tac ctxt = - ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) - THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)); - -val mset_simps_ss = - simpset_of (put_simpset HOL_basic_ss @{context} addsimps bin_simps); - -fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset mset_simps_ss ctxt)); - -val simplify_meta_eq = simplify_meta_eq; -val prove_conv = Arith_Data.prove_conv; - -end