isabelle: src/HOL/OrderedGroup.ML@81a4b4a245b0 (annotated)

14755 5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	1	(* Title: HOL/OrderedGroup.ML
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	2	ID: $Id$
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	3	Author: Steven Obua, Technische Universit�t M�nchen
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	4	*)
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	5
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	6	structure ab_group_add_cancel_data :> ABEL_CANCEL =
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	7	struct
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	8	val ss = simpset_of HOL.thy
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	9	val eq_reflection = thm "eq_reflection"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	10
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	11	val sg_ref = Sign.self_ref (sign_of (theory "OrderedGroup"))
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	12
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	13	val T = TFree("'a", ["OrderedGroup.ab_group_add"])
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	14
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	15	val restrict_to_left = thm "restrict_to_left"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	16	val add_cancel_21 = thm "add_cancel_21"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	17	val add_cancel_end = thm "add_cancel_end"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	18	val add_left_cancel = thm "add_left_cancel"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	19	val add_assoc = thm "add_assoc"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	20	val add_commute = thm "add_commute"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	21	val add_left_commute = thm "add_left_commute"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	22	val add_0 = thm "add_0"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	23	val add_0_right = thm "add_0_right"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	24
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	25	val eq_diff_eq = thm "eq_diff_eq"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	26
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	27	val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	28	fun dest_eqI th =
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	29	#1 (HOLogic.dest_bin "op =" HOLogic.boolT
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	30	(HOLogic.dest_Trueprop (concl_of th)))
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	31
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	32	val diff_def = thm "diff_def"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	33	val minus_add_distrib = thm "minus_add_distrib"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	34	val minus_minus = thm "minus_minus"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	35	val minus_0 = thm "minus_zero"
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	36	val add_inverses = [thm "right_minus", thm "left_minus"]
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	37	val cancel_simps = [thm "add_minus_cancel", thm "minus_add_cancel"]
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	38	end;
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	39
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	40	structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data);
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	41
5cc6e6b9e27a simplification for abelian groups obua parents: diff changeset	42	Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];

author	huffman
	Thu, 26 May 2005 02:23:27 +0200
changeset 16081	81a4b4a245b0
parent 14755	5cc6e6b9e27a
child 16423	24abe4c0e4b4
permissions	-rw-r--r--