--- /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 \<open>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.\<close>
+
+named_theorems cancelation_simproc_post \<open>These theorems are here to normalise the term, after the
+ cancelation simproc. Normalisation of \<open>iterate_add\<close> back to the normale representation
+ should be put here.\<close>
+
+named_theorems cancelation_simproc_eq_elim \<open>These theorems are here to help deriving contradiction
+ (e.g., \<open>Suc _ = 0\<close>).\<close>
+
+definition iterate_add :: \<open>nat \<Rightarrow> 'a::cancel_comm_monoid_add \<Rightarrow> 'a\<close> where
+ \<open>iterate_add n a = ((op + a) ^^ n) 0\<close>
+
+lemma iterate_add_simps[simp]:
+ \<open>iterate_add 0 a = 0\<close>
+ \<open>iterate_add (Suc n) a = a + iterate_add n a\<close>
+ unfolding iterate_add_def by auto
+
+lemma iterate_add_empty[simp]: \<open>iterate_add n 0 = 0\<close>
+ unfolding iterate_add_def by (induction n) auto
+
+lemma iterate_add_distrib[simp]: \<open>iterate_add (m+n) a = iterate_add m a + iterate_add n a\<close>
+ by (induction n) (auto simp: ac_simps)
+
+lemma iterate_add_Numeral1: \<open>iterate_add n Numeral1 = of_nat n\<close>
+ by (induction n) auto
+
+lemma iterate_add_1: \<open>iterate_add n 1 = of_nat n\<close>
+ by (induction n) auto
+
+lemma iterate_add_eq_add_iff1:
+ \<open>i \<le> j \<Longrightarrow> (iterate_add j u + m = iterate_add i u + n) = (iterate_add (j - i) u + m = n)\<close>
+ by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
+
+lemma iterate_add_eq_add_iff2:
+ \<open>i \<le> j \<Longrightarrow> (iterate_add i u + m = iterate_add j u + n) = (m = iterate_add (j - i) u + n)\<close>
+ by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
+
+lemma iterate_add_less_iff1:
+ "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)"
+ by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
+
+lemma iterate_add_less_iff2:
+ "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)"
+ by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
+
+lemma iterate_add_less_eq_iff1:
+ "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)"
+ 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 \<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)"
+ by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
+
+lemma iterate_add_add_eq1:
+ "j \<le> (i::nat) \<Longrightarrow> ((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 \<le> (j::nat) \<Longrightarrow> ((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 \<open>Simproc Set-Up\<close>
+
+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") =
+ \<open>fn phi => Cancel_Simprocs.eq_cancel\<close>
+
+text \<open>Can we reduce the sorts?\<close>
+simproc_setup comm_monoid_cancel_less_numerals
+ ("(l::'a::{cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m < n" | "l < m + n") =
+ \<open>fn phi => Cancel_Simprocs.less_cancel\<close>
+
+simproc_setup comm_monoid_cancel_less_eq_numerals
+ ("(l::'a::{cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m \<le> n" | "l \<le> m + n") =
+ \<open>fn phi => Cancel_Simprocs.less_eq_cancel\<close>
+
+simproc_setup comm_monoid_cancel_cancel_numerals
+ ("((l::'a :: cancel_comm_monoid_add) + m) - n" | "l - (m + n)") =
+ \<open>fn phi => Cancel_Simprocs.diff_cancel\<close>
+
+end
+
--- /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;
--- /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 \<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>*)
+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
+
--- /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
--- 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 \<open>(Finite) multisets\<close>
theory Multiset
-imports Main
+imports Cancellation
begin
subsection \<open>The type of multisets\<close>
@@ -972,15 +972,33 @@
"i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (m \<subset># 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: \<open>repeat_mset n M = iterate_add n M\<close>
+ unfolding iterate_add_def by (induction n) auto
+
ML_file "multiset_simprocs.ML"
+lemma add_mset_replicate_mset_safe[cancelation_simproc_pre]: \<open>NO_MATCH {#} M \<Longrightarrow> add_mset a M = {#a#} + M\<close>
+ 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") =
- \<open>fn phi => Multiset_Simprocs.eq_cancel_msets\<close>
+ \<open>fn phi => Cancel_Simprocs.eq_cancel\<close>
simproc_setup msetsubset_cancel
("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># 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") =
- \<open>fn phi => Multiset_Simprocs.diff_cancel_msets\<close>
+ \<open>fn phi => Cancel_Simprocs.diff_cancel\<close>
subsubsection \<open>Conditionally complete lattice\<close>
--- 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;
--- 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
--- 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 \<open>add_mset a C\<close> by \<open>add_mset a {#}\<close> and \<open>C\<close>, iff C was not already the empty set;
- * the \<open>replicate_mset n a\<close> by \<open>repeat_mset n {#a#}\<close>.
-*)
-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 \<open>repeat_mset (Suc 0) n\<close>, \<open>n+0\<close>, and \<open>0+n\<close> to \<open>n\<close>*)
-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