src/HOL/OrderedGroup.thy
changeset 22482 8fc3d7237e03
parent 22452 8a86fd2a1bf0
child 22548 6ce4bddf3bcb
     1.1 --- a/src/HOL/OrderedGroup.thy	Tue Mar 20 15:52:38 2007 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Tue Mar 20 15:52:39 2007 +0100
     1.3 @@ -1042,6 +1042,9 @@
     1.4    show ?thesis by (rule le_add_right_mono[OF 2 3])
     1.5  qed
     1.6  
     1.7 +
     1.8 +subsection {* Tools setup *}
     1.9 +
    1.10  text{*Simplification of @{term "x-y < 0"}, etc.*}
    1.11  lemmas diff_less_0_iff_less = less_iff_diff_less_0 [symmetric]
    1.12  lemmas diff_eq_0_iff_eq = eq_iff_diff_eq_0 [symmetric]
    1.13 @@ -1050,6 +1053,58 @@
    1.14  declare diff_eq_0_iff_eq [simp]
    1.15  declare diff_le_0_iff_le [simp]
    1.16  
    1.17 +ML {*
    1.18 +structure ab_group_add_cancel = Abel_Cancel(
    1.19 +struct
    1.20 +
    1.21 +(* term order for abelian groups *)
    1.22 +
    1.23 +fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
    1.24 +      ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"]
    1.25 +  | agrp_ord _ = ~1;
    1.26 +
    1.27 +fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
    1.28 +
    1.29 +local
    1.30 +  val ac1 = mk_meta_eq @{thm add_assoc};
    1.31 +  val ac2 = mk_meta_eq @{thm add_commute};
    1.32 +  val ac3 = mk_meta_eq @{thm add_left_commute};
    1.33 +  fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
    1.34 +        SOME ac1
    1.35 +    | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
    1.36 +        if termless_agrp (y, x) then SOME ac3 else NONE
    1.37 +    | solve_add_ac thy _ (_ $ x $ y) =
    1.38 +        if termless_agrp (y, x) then SOME ac2 else NONE
    1.39 +    | solve_add_ac thy _ _ = NONE
    1.40 +in
    1.41 +  val add_ac_proc = Simplifier.simproc @{theory}
    1.42 +    "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
    1.43 +end;
    1.44 +
    1.45 +val cancel_ss = HOL_basic_ss settermless termless_agrp
    1.46 +  addsimprocs [add_ac_proc] addsimps
    1.47 +  [@{thm add_0}, @{thm add_0_right}, @{thm diff_def},
    1.48 +   @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
    1.49 +   @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
    1.50 +   @{thm minus_add_cancel}];
    1.51 +  
    1.52 +val eq_reflection = @{thm eq_reflection}
    1.53 +  
    1.54 +val thy_ref = Theory.self_ref @{theory}
    1.55 +
    1.56 +val T = TFree("'a", ["OrderedGroup.ab_group_add"])
    1.57 +
    1.58 +val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}]
    1.59 +
    1.60 +val dest_eqI = 
    1.61 +  fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
    1.62 +
    1.63 +end);
    1.64 +*}
    1.65 +
    1.66 +ML_setup {*
    1.67 +  Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
    1.68 +*}
    1.69  
    1.70  ML {*
    1.71  val add_assoc = thm "add_assoc";