--- /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;