--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Group.ML Thu Jun 25 13:57:34 1998 +0200
@@ -0,0 +1,222 @@
+(* Title: HOL/Integ/Group.ML
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1997 TU Muenchen
+*)
+
+(*** Groups ***)
+
+(* Derives the well-known convergent set of equations for groups
+ based on the unary inverse zero-x.
+*)
+
+Goal "!!x::'a::add_group. (zero-x)+(x+y) = y";
+by (rtac trans 1);
+by (rtac (plus_assoc RS sym) 1);
+by (stac left_inv 1);
+by (rtac zeroL 1);
+qed "left_inv2";
+
+Goal "!!x::'a::add_group. (zero-(zero-x)) = x";
+by (rtac trans 1);
+by (res_inst_tac [("x","zero-x")] left_inv2 2);
+by (stac left_inv 1);
+by (rtac (zeroR RS sym) 1);
+qed "inv_inv";
+
+Goal "zero-zero = (zero::'a::add_group)";
+by (rtac trans 1);
+by (rtac (zeroR RS sym) 1);
+by (rtac trans 1);
+by (res_inst_tac [("x","zero")] left_inv2 2);
+by (simp_tac (simpset() addsimps [zeroR]) 1);
+qed "inv_zero";
+
+Goal "!!x::'a::add_group. x+(zero-x) = zero";
+by (rtac trans 1);
+by (res_inst_tac [("x","zero-x")] left_inv 2);
+by (stac inv_inv 1);
+by (rtac refl 1);
+qed "right_inv";
+
+Goal "!!x::'a::add_group. x+((zero-x)+y) = y";
+by (rtac trans 1);
+by (res_inst_tac [("x","zero-x")] left_inv2 2);
+by (stac inv_inv 1);
+by (rtac refl 1);
+qed "right_inv2";
+
+val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
+
+Goal "!!x::'a::add_group. zero-(x+y) = (zero-y)+(zero-x)";
+by (rtac trans 1);
+ by (rtac zeroR 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 2);
+ by (res_inst_tac [("x","x+y")] right_inv 2);
+by (rtac trans 1);
+ by (rtac plus_assoc 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (simp_tac (simpset() addsimps
+ [plus_assoc,left_inv,left_inv2,right_inv,right_inv2]) 2);
+ by (rtac refl 2);
+by (rtac (zeroL RS sym) 1);
+qed "inv_plus";
+
+(*** convergent TRS for groups with unary inverse zero-x ***)
+val group1_simps =
+ [zeroL,zeroR,plus_assoc,left_inv,left_inv2,right_inv,right_inv2,inv_inv,
+ inv_zero,inv_plus];
+
+val group1_tac =
+ let val ss = HOL_basic_ss addsimps group1_simps
+ in simp_tac ss end;
+
+(* I believe there is no convergent TRS for groups with binary `-',
+ unless you have an extra unary `-' and simply define x-y = x+(-y).
+ This does not work with only a binary `-' because x-y = x+(zero-y) does
+ not terminate. Hence we have a special tactic for converting all
+ occurrences of x-y into x+(zero-y):
+*)
+
+local
+fun find(Const("op -",Type("fun",[T,_]))$s$t) = [(T,s,t)] @ find s @ find t
+ | find(s$t) = find s @ find t
+ | find _ = [];
+
+fun subst_tac sg (tacf,(T,s,t)) =
+ let val typinst = [(("'a",0),ctyp_of sg T)];
+ val terminst = [(cterm_of sg (Var(("x",0),T)),cterm_of sg s),
+ (cterm_of sg (Var(("y",0),T)),cterm_of sg t)];
+ in tacf THEN' rtac ((instantiate(typinst,terminst) minus_inv) RS ssubst) end;
+
+in
+val mk_group1_tac = SUBGOAL(fn (t,i) => fn st =>
+ let val sg = #sign(rep_thm st)
+ in foldl (subst_tac sg) (K all_tac,find t) i st
+ end)
+end;
+
+(* The following two equations are not used in any of the decision procedures,
+ but are still very useful. They also demonstrate mk_group1_tac.
+*)
+Goal "x-x = (zero::'a::add_group)";
+by (mk_group1_tac 1);
+by (group1_tac 1);
+qed "minus_self_zero";
+
+Goal "x-zero = (x::'a::add_group)";
+by (mk_group1_tac 1);
+by (group1_tac 1);
+qed "minus_zero";
+
+(*** Abelian Groups ***)
+
+Goal "x+(y+z)=y+(x+z::'a::add_agroup)";
+by (rtac trans 1);
+by (rtac plus_commute 1);
+by (rtac trans 1);
+by (rtac plus_assoc 1);
+by (simp_tac (simpset() addsimps [plus_commute]) 1);
+qed "plus_commuteL";
+
+(* Convergent TRS for Abelian groups with unary inverse zero-x.
+ Requires ordered rewriting
+*)
+
+val agroup1_simps = plus_commute::plus_commuteL::group1_simps;
+
+val agroup1_tac =
+ let val ss = HOL_basic_ss addsimps agroup1_simps
+ in simp_tac ss end;
+
+(* Again, I do not believe there is a convergent TRS for Abelian Groups with
+ binary `-'. However, we can still decide the word problem using additional
+ rules for
+ 1. floating `-' to the top:
+ "x + (y - z) = (x + y) - (z::'a::add_group)"
+ "(x - y) + z = (x + z) - (y::'a::add_agroup)"
+ "(x - y) - z = x - (y + (z::'a::add_agroup))"
+ "x - (y - z) = (x + z) - (y::'a::add_agroup)"
+ 2. and for moving `-' over to the other side:
+ (x-y = z) = (x = z+y) and (x = y-z) = (x+z = y)
+*)
+Goal "x + (y - z) = (x + y) - (z::'a::add_group)";
+by (mk_group1_tac 1);
+by (group1_tac 1);
+qed "plus_minusR";
+
+Goal "(x - y) + z = (x + z) - (y::'a::add_agroup)";
+by (mk_group1_tac 1);
+by (agroup1_tac 1);
+qed "plus_minusL";
+
+Goal "(x - y) - z = x - (y + (z::'a::add_agroup))";
+by (mk_group1_tac 1);
+by (agroup1_tac 1);
+qed "minus_minusL";
+
+Goal "x - (y - z) = (x + z) - (y::'a::add_agroup)";
+by (mk_group1_tac 1);
+by (agroup1_tac 1);
+qed "minus_minusR";
+
+Goal "!!x::'a::add_group. (x-y = z) = (x = z+y)";
+by (stac minus_inv 1);
+by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
+qed "minusL_iff";
+
+Goal "!!x::'a::add_group. (x = y-z) = (x+z = y)";
+by (stac minus_inv 1);
+by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
+qed "minusR_iff";
+
+val agroup2_simps =
+ [zeroL,zeroR,plus_assoc,plus_commute,plus_commuteL,
+ plus_minusR,plus_minusL,minus_minusL,minus_minusR,minusL_iff,minusR_iff];
+
+(* This two-phase ordered rewriting tactic works, but agroup_simps are
+ simpler. However, agroup_simps is not confluent for arbitrary terms,
+ it merely decides equality.
+(* Phase 1 *)
+
+Goal "!!x::'a::add_agroup. (x+(zero-y))+z = (x+z)+(zero-y)";
+by (Simp_tac 1);
+val lemma = result();
+bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+Goal "!!x::'a::add_agroup. x+(zero-(y+z)) = (x+(zero-y))+(zero-z)";
+by (Simp_tac 1);
+val lemma = result();
+bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+Goal "!!x::'a::add_agroup. x+(zero-(y+(zero-z))) = (x+z)+(zero-y)";
+by (Simp_tac 1);
+val lemma = result();
+bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+Goal "!!x::'a::add_agroup. x+(y+(zero-z)) = (x+y)+(zero-z)";
+by (Simp_tac 1);
+val lemma = result();
+bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+(* Phase 2 *)
+
+Goal "!!x::'a::add_agroup. (x+y)+(zero-z) = x+(y+(zero-z))";
+by (Simp_tac 1);
+val lemma = result();
+bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+Goal "!!x::'a::add_agroup. (x+y)+(zero-x) = y";
+by (rtac (plus_assoc RS trans) 1);
+by (rtac trans 1);
+ by (rtac plus_cong 1);
+ by (rtac refl 1);
+ by (rtac right_inv2 2);
+by (rtac plus_commute 1);
+val lemma = result();
+bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+*)