src/HOL/ex/Group.ML

consts: include *all* names;

(*  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 0-x.
*)

Goal "!!x::'a::add_group. (0-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. (0-(0-x)) = x";
by (rtac trans 1);
by (res_inst_tac [("x","0-x")] left_inv2 2);
by (stac left_inv 1);
by (rtac (zeroR RS sym) 1);
qed "inv_inv";

Goal "0-0 = (0::'a::add_group)";
by (rtac trans 1);
by (rtac (zeroR RS sym) 1);
by (rtac trans 1);
by (res_inst_tac [("x","0")] left_inv2 2);
by (simp_tac (simpset() addsimps [zeroR]) 1);
qed "inv_zero";

Goal "!!x::'a::add_group. x+(0-x) = 0";
by (rtac trans 1);
by (res_inst_tac [("x","0-x")] left_inv 2);
by (stac inv_inv 1);
by (rtac refl 1);
qed "right_inv";

Goal "!!x::'a::add_group. x+((0-x)+y) = y";
by (rtac trans 1);
by (res_inst_tac [("x","0-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. 0-(x+y) = (0-y)+(0-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 0-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+(0-y) does
   not terminate. Hence we have a special tactic for converting all
   occurrences of x-y into x+(0-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 = (0::'a::add_group)";
by (mk_group1_tac 1);
by (group1_tac 1);
qed "minus_self_zero";

Goal "x-0 = (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 0-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+(0-y))+z = (x+z)+(0-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+(0-(y+z)) = (x+(0-y))+(0-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+(0-(y+(0-z))) = (x+z)+(0-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+(0-z)) = (x+y)+(0-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)+(0-z) = x+(y+(0-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)+(0-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);

*)