src/HOL/ex/LocaleGroup.ML
author wenzelm
Tue, 04 Aug 1998 18:40:18 +0200
changeset 5250 1bff4b1e5ba9
child 5318 72bf8039b53f
permissions -rw-r--r--
added LocaleGroup, PiSets examples;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/LocaleGroup.ML
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     3
    Author:     Florian Kammueller, University of Cambridge
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     4
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     5
Group theory via records and locales.
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     6
*)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     7
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     8
Open_locale "groups";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     9
print_locales LocaleGroup.thy;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    10
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    11
val simp_G = simplify (simpset() addsimps [Group_def]) (thm "Group_G");
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    12
Addsimps [simp_G, thm "Group_G"];
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    13
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    14
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    15
goal LocaleGroup.thy "e : carrier G";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    16
by (afs [thm "e_def"] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    17
val e_closed = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    18
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    19
(* Mit dieser Def ist es halt schwierig *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    20
goal LocaleGroup.thy "op # : carrier G -> carrier G -> carrier G";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    21
by (res_inst_tac [("t","op #")] ssubst 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    22
br ext 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    23
br ext 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    24
br meta_eq_to_obj_eq 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    25
br (thm "binop_def") 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    26
by (Asm_full_simp_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    27
val binop_funcset = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    28
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    29
goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G |] ==> x # y : carrier G";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    30
by (afs [binop_funcset RS funcset2E1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    31
val binop_closed = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    32
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    33
goal LocaleGroup.thy "inv : carrier G -> carrier G";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    34
by (res_inst_tac [("t","inv")] ssubst 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    35
br ext 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    36
br meta_eq_to_obj_eq 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    37
br (thm "inv_def") 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    38
by (Asm_full_simp_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    39
val inv_funcset = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    40
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    41
goal LocaleGroup.thy "!! x . x: carrier G ==> x -| : carrier G";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    42
by (afs [inv_funcset RS funcsetE1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    43
val inv_closed = result(); 
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    44
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    45
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    46
goal LocaleGroup.thy "!! x . x: carrier G ==> e # x = x";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    47
by (afs [thm "e_def", thm "binop_def"] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    48
val e_ax1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    49
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    50
goal LocaleGroup.thy "!! x. x: carrier G ==> (x -|) # x = e";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    51
by (afs [thm "binop_def", thm "inv_def", thm "e_def"] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    52
val inv_ax2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    53
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    54
goal LocaleGroup.thy "!! x y z. [| x: carrier G; y: carrier G; z: carrier G |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    55
\               ==> (x # y) # z = x # (y # z)";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    56
by (afs [thm "binop_def"] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    57
val binop_assoc = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    58
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    59
goal LocaleGroup.thy "!! G f i e1. [|f : G -> G -> G; i: G -> G; e1: G;\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    60
\        ! x: G. (f (i x) x = e1); ! x: G. (f e1 x = x);\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    61
\        ! x: G. ! y: G. ! z: G.(f (f x y) z = f (x) (f y z)) |] \
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    62
\ ==> (| carrier = G, bin_op = f, inverse = i, unit = e1 |) : Group";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    63
by (afs [Group_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    64
val GroupI = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    65
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    66
(*****)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    67
(* Now the real derivations *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    68
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    69
goal LocaleGroup.thy "!! x y z. [| x : carrier G ; y : carrier G; z : carrier G;\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    70
\                  x # y  =  x # z |] ==> y = z";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    71
(* remarkable: In the following step the use of e_ax1 instead of unit_ax1
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    72
   is better! It doesn't produce G: Group as subgoal and the nice syntax stays *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    73
by (res_inst_tac [("P","%r. r = z")] (e_ax1 RS subst) 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    74
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    75
(* great: we can use the nice syntax even in res_inst_tac *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    76
by (res_inst_tac [("P","%r. r # y = z")] subst 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    77
by (res_inst_tac [("x","x")] inv_ax2 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    78
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    79
br (binop_assoc RS ssubst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    80
br inv_closed 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    81
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    82
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    83
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    84
be ssubst 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    85
br (binop_assoc RS subst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    86
br inv_closed 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    87
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    88
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    89
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    90
br (inv_ax2 RS ssubst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    91
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    92
br (e_ax1 RS ssubst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    93
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    94
br refl 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    95
val left_cancellation = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    96
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    97
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    98
(* here are the other directions of basic lemmas, they needed a cancellation (left) *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    99
(* to be able to show the other directions of inverse and unity axiom we need:*)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   100
goal LocaleGroup.thy "!! x. x: carrier G ==> x # e = x";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   101
(* here is a problem with res_inst_tac: in Fun there is a 
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   102
   constant inv, and that gets addressed when we type in -|.
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   103
   We have to use the defining term and then fold the def of inv *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   104
by (res_inst_tac [("x","inverse G x")] left_cancellation 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   105
by (fold_goals_tac [thm "inv_def"]);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   106
by (fast_tac (claset() addSEs [inv_closed]) 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   107
by (afs [binop_closed, e_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   108
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   109
br (binop_assoc RS subst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   110
by (fast_tac (claset() addSEs [inv_closed]) 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   111
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   112
br (e_closed) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   113
br (inv_ax2 RS ssubst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   114
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   115
br (e_ax1 RS ssubst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   116
br e_closed 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   117
br refl 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   118
val e_ax2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   119
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   120
goal LocaleGroup.thy "!! x. [| x: carrier G; x # x = x |] ==> x = e";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   121
by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS forw_subst) 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   122
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   123
by (res_inst_tac [("x","x")] left_cancellation 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   124
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   125
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   126
br e_closed 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   127
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   128
val idempotent_e = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   129
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   130
goal LocaleGroup.thy  "!! x. x: carrier G ==> x # (x -|) = e";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   131
br idempotent_e 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   132
by (afs [binop_closed,inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   133
br (binop_assoc RS ssubst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   134
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   135
by (afs [inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   136
by (afs [binop_closed,inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   137
by (res_inst_tac [("t","x -| # x # x -|")] subst 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   138
br binop_assoc 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   139
by (afs [inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   140
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   141
by (afs [inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   142
br (inv_ax2 RS ssubst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   143
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   144
br (e_ax1 RS ssubst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   145
by (afs [inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   146
br refl 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   147
val inv_ax1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   148
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   149
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   150
goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G; \
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   151
\                     x # y = e |] ==> y = x -|";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   152
by (res_inst_tac [("x","x")] left_cancellation 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   153
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   154
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   155
by (afs [inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   156
br (inv_ax1 RS ssubst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   157
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   158
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   159
val inv_unique = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   160
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   161
goal LocaleGroup.thy "!! x. x : carrier G ==> x -| -| = x";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   162
by (res_inst_tac [("x","inverse G x")] left_cancellation 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   163
by (fold_goals_tac [thm "inv_def"]);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   164
by (afs [inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   165
by (afs [inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   166
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   167
by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   168
val inv_inv = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   169
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   170
goal LocaleGroup.thy "!! x y. [| x : carrier G; y : carrier G |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   171
\           ==> (x # y) -| = y -| # x -|";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   172
br sym 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   173
br inv_unique 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   174
by (afs [binop_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   175
by (afs [inv_closed,binop_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   176
by (afs [binop_assoc,inv_closed,binop_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   177
by (res_inst_tac [("x1","y")] (binop_assoc RS subst) 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   178
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   179
by (afs [inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   180
by (afs [inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   181
by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   182
val inv_prod = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   183
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   184
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   185
goal LocaleGroup.thy "!! x y z. [| x : carrier G; y : carrier G;\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   186
\ z : carrier G; y # x =  z # x|] ==> y = z";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   187
by (res_inst_tac [("P","%r. r = z")] (e_ax2 RS subst) 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   188
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   189
by (res_inst_tac [("P","%r. y # r = z")] subst 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   190
br inv_ax1 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   191
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   192
br (binop_assoc RS subst) 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   193
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   194
ba 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   195
by (afs [inv_closed] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   196
be ssubst 1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   197
by (afs [binop_assoc,inv_closed,inv_ax1,e_ax2] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   198
val right_cancellation = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   199
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   200
(* example what happens if export *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   201
val Left_cancellation = export left_cancellation;