src/HOL/Groups.thy
changeset 48556 62a3fbf9d35b
parent 45548 3e2722d66169
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Groups.thy	Fri Jul 27 14:56:37 2012 +0200
     1.2 +++ b/src/HOL/Groups.thy	Fri Jul 27 15:42:39 2012 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  theory Groups
     1.6  imports Orderings
     1.7 -uses ("Tools/abel_cancel.ML")
     1.8 +uses ("Tools/group_cancel.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Fact collections *}
    1.12 @@ -472,6 +472,9 @@
    1.13  lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
    1.14    by (rule right_minus_eq)
    1.15  
    1.16 +lemma add_diff_cancel_left: "(c + a) - (c + b) = a - b"
    1.17 +  by (simp add: diff_minus add_ac)
    1.18 +
    1.19  end
    1.20  
    1.21  
    1.22 @@ -827,15 +830,22 @@
    1.23  
    1.24  end
    1.25  
    1.26 -use "Tools/abel_cancel.ML"
    1.27 +use "Tools/group_cancel.ML"
    1.28 +
    1.29 +simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
    1.30 +  {* fn phi => fn ss => try Group_Cancel.cancel_add_conv *}
    1.31 +
    1.32 +simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
    1.33 +  {* fn phi => fn ss => try Group_Cancel.cancel_diff_conv *}
    1.34  
    1.35 -simproc_setup abel_cancel_sum
    1.36 -  ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
    1.37 -  {* fn phi => Abel_Cancel.sum_proc *}
    1.38 +simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
    1.39 +  {* fn phi => fn ss => try Group_Cancel.cancel_eq_conv *}
    1.40  
    1.41 -simproc_setup abel_cancel_relation
    1.42 -  ("a < (b::'a::ordered_ab_group_add)" | "a \<le> (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") =
    1.43 -  {* fn phi => Abel_Cancel.rel_proc *}
    1.44 +simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
    1.45 +  {* fn phi => fn ss => try Group_Cancel.cancel_le_conv *}
    1.46 +
    1.47 +simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
    1.48 +  {* fn phi => fn ss => try Group_Cancel.cancel_less_conv *}
    1.49  
    1.50  class linordered_ab_semigroup_add =
    1.51    linorder + ordered_ab_semigroup_add