src/HOL/ex/Group.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8936 a1c426541757
child 11701 3d51fbf81c17
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Integ/Group.ML
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     2
    ID:         $Id$
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     3
    Author:     Tobias Nipkow
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     4
    Copyright   1997 TU Muenchen
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     5
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     6
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     7
(*** Groups ***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     8
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     9
(* Derives the well-known convergent set of equations for groups
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    10
   based on the unary inverse 0-x.
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    11
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    12
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    13
Goal "!!x::'a::add_group. (0-x)+(x+y) = y";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    14
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    15
by (rtac (plus_assoc RS sym) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    16
by (stac left_inv 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    17
by (rtac zeroL 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    18
qed "left_inv2";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    19
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    20
Goal "!!x::'a::add_group. (0-(0-x)) = x";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    21
by (rtac trans 1);
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    22
by (res_inst_tac [("x","0-x")] left_inv2 2);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    23
by (stac left_inv 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    24
by (rtac (zeroR RS sym) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    25
qed "inv_inv";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    26
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    27
Goal "0-0 = (0::'a::add_group)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    28
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    29
by (rtac (zeroR RS sym) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    30
by (rtac trans 1);
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    31
by (res_inst_tac [("x","0")] left_inv2 2);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    32
by (simp_tac (simpset() addsimps [zeroR]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    33
qed "inv_zero";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    34
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    35
Goal "!!x::'a::add_group. x+(0-x) = 0";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    36
by (rtac trans 1);
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    37
by (res_inst_tac [("x","0-x")] left_inv 2);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    38
by (stac inv_inv 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    39
by (rtac refl 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    40
qed "right_inv";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    41
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    42
Goal "!!x::'a::add_group. x+((0-x)+y) = y";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    43
by (rtac trans 1);
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    44
by (res_inst_tac [("x","0-x")] left_inv2 2);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    45
by (stac inv_inv 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    46
by (rtac refl 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    47
qed "right_inv2";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    48
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    49
val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    50
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    51
Goal "!!x::'a::add_group. 0-(x+y) = (0-y)+(0-x)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    52
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    53
 by (rtac zeroR 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    54
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    55
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    56
  by (rtac refl 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    57
 by (res_inst_tac [("x","x+y")] right_inv 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    58
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    59
 by (rtac plus_assoc 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    60
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    61
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    62
  by (simp_tac (simpset() addsimps
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    63
        [plus_assoc,left_inv,left_inv2,right_inv,right_inv2]) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    64
 by (rtac refl 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    65
by (rtac (zeroL RS sym) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    66
qed "inv_plus";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    67
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    68
(*** convergent TRS for groups with unary inverse 0-x ***)
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    69
val group1_simps =
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    70
  [zeroL,zeroR,plus_assoc,left_inv,left_inv2,right_inv,right_inv2,inv_inv,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    71
   inv_zero,inv_plus];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    72
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    73
val group1_tac =
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    74
  let val ss = HOL_basic_ss addsimps group1_simps
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    75
  in simp_tac ss end;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    76
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    77
(* I believe there is no convergent TRS for groups with binary `-',
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    78
   unless you have an extra unary `-' and simply define x-y = x+(-y).
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    79
   This does not work with only a binary `-' because x-y = x+(0-y) does
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    80
   not terminate. Hence we have a special tactic for converting all
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    81
   occurrences of x-y into x+(0-y):
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    82
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    83
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    84
local
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    85
fun find(Const("op -",Type("fun",[T,_]))$s$t) = [(T,s,t)] @ find s @ find t
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    86
  | find(s$t) = find s @ find t
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    87
  | find _ = [];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    88
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    89
fun subst_tac sg (tacf,(T,s,t)) = 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    90
  let val typinst = [(("'a",0),ctyp_of sg T)];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    91
      val terminst = [(cterm_of sg (Var(("x",0),T)),cterm_of sg s),
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    92
                      (cterm_of sg (Var(("y",0),T)),cterm_of sg t)];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    93
  in tacf THEN' rtac ((instantiate(typinst,terminst) minus_inv) RS ssubst) end;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    94
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    95
in
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    96
val mk_group1_tac = SUBGOAL(fn (t,i) => fn st =>
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    97
      let val sg = #sign(rep_thm st)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    98
      in foldl (subst_tac sg) (K all_tac,find t) i st
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    99
      end)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   100
end;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   101
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   102
(* The following two equations are not used in any of the decision procedures,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   103
   but are still very useful. They also demonstrate mk_group1_tac.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   104
*)
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
   105
Goal "x-x = (0::'a::add_group)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   106
by (mk_group1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   107
by (group1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   108
qed "minus_self_zero";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   109
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
   110
Goal "x-0 = (x::'a::add_group)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   111
by (mk_group1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   112
by (group1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   113
qed "minus_zero";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   114
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   115
(*** Abelian Groups ***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   116
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   117
Goal "x+(y+z)=y+(x+z::'a::add_agroup)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   118
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   119
by (rtac plus_commute 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   120
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   121
by (rtac plus_assoc 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   122
by (simp_tac (simpset() addsimps [plus_commute]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   123
qed "plus_commuteL";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   124
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
   125
(* Convergent TRS for Abelian groups with unary inverse 0-x.
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   126
   Requires ordered rewriting
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   127
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   128
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   129
val agroup1_simps = plus_commute::plus_commuteL::group1_simps;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   130
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   131
val agroup1_tac =
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   132
  let val ss = HOL_basic_ss addsimps agroup1_simps
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   133
  in simp_tac ss end;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   134
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   135
(* Again, I do not believe there is a convergent TRS for Abelian Groups with
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   136
   binary `-'. However, we can still decide the word problem using additional
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   137
   rules for 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   138
   1. floating `-' to the top:
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   139
      "x + (y - z) = (x + y) - (z::'a::add_group)"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   140
      "(x - y) + z = (x + z) - (y::'a::add_agroup)"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   141
      "(x - y) - z = x - (y + (z::'a::add_agroup))"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   142
      "x - (y - z) = (x + z) - (y::'a::add_agroup)"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   143
   2. and for moving `-' over to the other side:
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   144
      (x-y = z) = (x = z+y) and (x = y-z) = (x+z = y)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   145
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   146
Goal "x + (y - z) = (x + y) - (z::'a::add_group)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   147
by (mk_group1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   148
by (group1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   149
qed "plus_minusR";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   150
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   151
Goal "(x - y) + z = (x + z) - (y::'a::add_agroup)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   152
by (mk_group1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   153
by (agroup1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   154
qed "plus_minusL";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   155
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   156
Goal "(x - y) - z = x - (y + (z::'a::add_agroup))";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   157
by (mk_group1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   158
by (agroup1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   159
qed "minus_minusL";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   160
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   161
Goal "x - (y - z) = (x + z) - (y::'a::add_agroup)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   162
by (mk_group1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   163
by (agroup1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   164
qed "minus_minusR";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   165
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   166
Goal "!!x::'a::add_group. (x-y = z) = (x = z+y)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   167
by (stac minus_inv 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   168
by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   169
qed "minusL_iff";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   170
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   171
Goal "!!x::'a::add_group. (x = y-z) = (x+z = y)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   172
by (stac minus_inv 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   173
by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   174
qed "minusR_iff";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   175
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   176
val agroup2_simps =
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   177
  [zeroL,zeroR,plus_assoc,plus_commute,plus_commuteL,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   178
   plus_minusR,plus_minusL,minus_minusL,minus_minusR,minusL_iff,minusR_iff];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   179
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   180
(* This two-phase ordered rewriting tactic works, but agroup_simps are
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   181
   simpler. However, agroup_simps is not confluent for arbitrary terms,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   182
   it merely decides equality.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   183
(* Phase 1 *)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   184
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
   185
Goal "!!x::'a::add_agroup. (x+(0-y))+z = (x+z)+(0-y)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   186
by (Simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   187
val lemma = result();
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   188
bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   189
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
   190
Goal "!!x::'a::add_agroup. x+(0-(y+z)) = (x+(0-y))+(0-z)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   191
by (Simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   192
val lemma = result();
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   193
bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   194
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
   195
Goal "!!x::'a::add_agroup. x+(0-(y+(0-z))) = (x+z)+(0-y)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   196
by (Simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   197
val lemma = result();
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   198
bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   199
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
   200
Goal "!!x::'a::add_agroup. x+(y+(0-z)) = (x+y)+(0-z)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   201
by (Simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   202
val lemma = result();
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   203
bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   204
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   205
(* Phase 2 *)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   206
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
   207
Goal "!!x::'a::add_agroup. (x+y)+(0-z) = x+(y+(0-z))";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   208
by (Simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   209
val lemma = result();
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   210
bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   211
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
   212
Goal "!!x::'a::add_agroup. (x+y)+(0-x) = y";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   213
by (rtac (plus_assoc RS trans) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   214
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   215
 by (rtac plus_cong 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   216
  by (rtac refl 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   217
 by (rtac right_inv2 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   218
by (rtac plus_commute 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   219
val lemma = result();
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   220
bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   221
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   222
*)