<commit_before>(*  Title:      HOL/OrderedGroup.ML
    ID:         $Id$
    Author:     <NAME>, <NAME>, Technische Universitt Mnchen
*)

structure ab_group_add_cancel_data :> ABEL_CANCEL  = 
struct

(*** Term order for abelian groups ***)

fun agrp_ord a = find_index_eq a ["0", "op +", "uminus", "op -"];

fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);

val cancel_ss = HOL_basic_ss settermless termless_agrp addsimps
  [thm "add_assoc", thm "add_commute", thm "add_left_commute",
   thm "add_0", thm "add_0_right",
   thm "diff_def", thm "minus_add_distrib",
   thm "minus_minus", thm "minus_zero",
   thm "right_minus", thm "left_minus",
   thm "add_minus_cancel", thm "minus_add_cancel"];
  
  val eq_reflection = thm "eq_reflection"
  
  val thy_ref = Theory.self_ref (theory "OrderedGroup")

  val T = TFree("'a", ["OrderedGroup.ab_group_add"])

  val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]<commit_msg>speedup: use simproc for AC rules<commit_after>(*  Title:      HOL/OrderedGroup.ML
    ID:         $Id$
    Author:     <NAME>, <NAME>, Technische Universit� Mnchen
*)

structure ab_group_add_cancel_data :> ABEL_CANCEL  = 
struct

(*** Term order for abelian groups ***)

fun agrp_ord a = find_index_eq a ["0", "op +", "uminus", "op -"];

fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);

local
  val ac1 = mk_meta_eq (thm "add_assoc");
  val ac2 = mk_meta_eq (thm "add_commute");
  val ac3 = mk_meta_eq (thm "add_left_commute");
  fun solve_add_ac thy _ (_ $ (Const ("op +",_) $ _ $ _) $ _) =
        SOME ac1
    | solve_add_ac thy _ (_ $ x $ (Const ("op +",_) $ y $ z)) =
        if termless_agrp (y, x) then SOME ac3 else NONE
    | solve_add_ac thy _ (_ $ x $ y) =
        if termless_agrp (y, x) then SOME ac2 else NONE
    | solve_add_ac thy _ _ = NONE
in
  val add_ac_proc = Simplifier.simproc (the_context ())
    "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
end;

val cancel_ss = HOL_basic_ss settermless termless_agrp
  addsimprocs [add_ac_proc] addsimps
  [thm "add_0", thm "add_0_right",
   thm "diff_def", thm "minus_add_distrib",
   thm "minus_minus", thm "minus_zero",
   thm "right_minus", thm "left_minus",
   thm "add_minus_cancel", thm "minus_add_cancel"];
  
  val eq_reflection = thm "eq_reflection"
  
  val thy_ref = Theory.self_ref (theory "OrderedGroup")

  val T = TFree("'a", ["OrderedGroup.ab_group_add"])

  val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
{'fraction_non_alphanumeric': 0.13968510294711345, 'fraction_numerical': 0.004844570044408559, 'mean_word_length': 3.877952755905512, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4590741', 'n_tokens_mistral': 1024, 'n_tokens_neox': 1000, 'n_words': 247}