1.1 --- a/src/HOL/IsaMakefile Tue Mar 20 15:52:38 2007 +0100
1.2 +++ b/src/HOL/IsaMakefile Tue Mar 20 15:52:39 2007 +0100
1.3 @@ -93,7 +93,7 @@
1.4 Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML Integ/presburger.ML \
1.5 Integ/qelim.ML Integ/reflected_cooper.ML Integ/reflected_presburger.ML \
1.6 Lattices.thy List.thy Main.thy Map.thy Nat.ML Nat.thy \
1.7 - OrderedGroup.ML OrderedGroup.thy Orderings.thy Power.thy Predicate.thy PreList.thy \
1.8 + OrderedGroup.thy Orderings.thy Power.thy Predicate.thy PreList.thy \
1.9 Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy Relation.thy \
1.10 Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy \
1.11 Sum_Type.thy Tools/res_reconstruct.ML Tools/ATP/reduce_axiomsN.ML \
2.1 --- a/src/HOL/OrderedGroup.ML Tue Mar 20 15:52:38 2007 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,54 +0,0 @@
2.4 -(* Title: HOL/OrderedGroup.ML
2.5 - ID: $Id$
2.6 - Author: Steven Obua, Tobias Nipkow, Technische Universitaet Muenchen
2.7 -*)
2.8 -
2.9 -structure ab_group_add_cancel_data :> ABEL_CANCEL =
2.10 -struct
2.11 -
2.12 -(*** Term order for abelian groups ***)
2.13 -
2.14 -fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"]
2.15 - | agrp_ord _ = ~1;
2.16 -
2.17 -fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
2.18 -
2.19 -local
2.20 - val ac1 = mk_meta_eq (thm "add_assoc");
2.21 - val ac2 = mk_meta_eq (thm "add_commute");
2.22 - val ac3 = mk_meta_eq (thm "add_left_commute");
2.23 - fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
2.24 - SOME ac1
2.25 - | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
2.26 - if termless_agrp (y, x) then SOME ac3 else NONE
2.27 - | solve_add_ac thy _ (_ $ x $ y) =
2.28 - if termless_agrp (y, x) then SOME ac2 else NONE
2.29 - | solve_add_ac thy _ _ = NONE
2.30 -in
2.31 - val add_ac_proc = Simplifier.simproc (the_context ())
2.32 - "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
2.33 -end;
2.34 -
2.35 -val cancel_ss = HOL_basic_ss settermless termless_agrp
2.36 - addsimprocs [add_ac_proc] addsimps
2.37 - [thm "add_0", thm "add_0_right",
2.38 - thm "diff_def", thm "minus_add_distrib",
2.39 - thm "minus_minus", thm "minus_zero",
2.40 - thm "right_minus", thm "left_minus",
2.41 - thm "add_minus_cancel", thm "minus_add_cancel"];
2.42 -
2.43 - val eq_reflection = thm "eq_reflection"
2.44 -
2.45 - val thy_ref = Theory.self_ref (theory "OrderedGroup")
2.46 -
2.47 - val T = TFree("'a", ["OrderedGroup.ab_group_add"])
2.48 -
2.49 - val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
2.50 - fun dest_eqI th =
2.51 - #1 (HOLogic.dest_bin "op =" HOLogic.boolT
2.52 - (HOLogic.dest_Trueprop (concl_of th)))
2.53 -end;
2.54 -
2.55 -structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data);
2.56 -
2.57 -Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
3.1 --- a/src/HOL/OrderedGroup.thy Tue Mar 20 15:52:38 2007 +0100
3.2 +++ b/src/HOL/OrderedGroup.thy Tue Mar 20 15:52:39 2007 +0100
3.3 @@ -1042,6 +1042,9 @@
3.4 show ?thesis by (rule le_add_right_mono[OF 2 3])
3.5 qed
3.6
3.7 +
3.8 +subsection {* Tools setup *}
3.9 +
3.10 text{*Simplification of @{term "x-y < 0"}, etc.*}
3.11 lemmas diff_less_0_iff_less = less_iff_diff_less_0 [symmetric]
3.12 lemmas diff_eq_0_iff_eq = eq_iff_diff_eq_0 [symmetric]
3.13 @@ -1050,6 +1053,58 @@
3.14 declare diff_eq_0_iff_eq [simp]
3.15 declare diff_le_0_iff_le [simp]
3.16
3.17 +ML {*
3.18 +structure ab_group_add_cancel = Abel_Cancel(
3.19 +struct
3.20 +
3.21 +(* term order for abelian groups *)
3.22 +
3.23 +fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
3.24 + ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"]
3.25 + | agrp_ord _ = ~1;
3.26 +
3.27 +fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
3.28 +
3.29 +local
3.30 + val ac1 = mk_meta_eq @{thm add_assoc};
3.31 + val ac2 = mk_meta_eq @{thm add_commute};
3.32 + val ac3 = mk_meta_eq @{thm add_left_commute};
3.33 + fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
3.34 + SOME ac1
3.35 + | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
3.36 + if termless_agrp (y, x) then SOME ac3 else NONE
3.37 + | solve_add_ac thy _ (_ $ x $ y) =
3.38 + if termless_agrp (y, x) then SOME ac2 else NONE
3.39 + | solve_add_ac thy _ _ = NONE
3.40 +in
3.41 + val add_ac_proc = Simplifier.simproc @{theory}
3.42 + "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
3.43 +end;
3.44 +
3.45 +val cancel_ss = HOL_basic_ss settermless termless_agrp
3.46 + addsimprocs [add_ac_proc] addsimps
3.47 + [@{thm add_0}, @{thm add_0_right}, @{thm diff_def},
3.48 + @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
3.49 + @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
3.50 + @{thm minus_add_cancel}];
3.51 +
3.52 +val eq_reflection = @{thm eq_reflection}
3.53 +
3.54 +val thy_ref = Theory.self_ref @{theory}
3.55 +
3.56 +val T = TFree("'a", ["OrderedGroup.ab_group_add"])
3.57 +
3.58 +val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}]
3.59 +
3.60 +val dest_eqI =
3.61 + fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
3.62 +
3.63 +end);
3.64 +*}
3.65 +
3.66 +ML_setup {*
3.67 + Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
3.68 +*}
3.69
3.70 ML {*
3.71 val add_assoc = thm "add_assoc";