src/HOL/ex/LocaleGroup.ML
author paulson
Thu Nov 12 10:26:08 1998 +0100 (1998-11-12)
changeset 5848 99dea3c24efb
parent 5845 eb183b062eae
child 6024 cb87f103d114
permissions -rw-r--r--
changed inverse syntax from x-| to i(x)
     1 (*  Title:      HOL/ex/LocaleGroup.ML
     2     ID:         $Id$
     3     Author:     Florian Kammueller, University of Cambridge
     4 
     5 Group theory via records and locales.
     6 *)
     7 
     8 Open_locale "groups";
     9 print_locales LocaleGroup.thy;
    10 
    11 val simp_G = simplify (simpset() addsimps [Group_def]) (thm "Group_G");
    12 Addsimps [simp_G, thm "Group_G"];
    13 
    14 
    15 Goal "e : carrier G";
    16 by (simp_tac (simpset() addsimps [thm "e_def"]) 1);
    17 qed "e_closed";
    18 
    19 (* Mit dieser Def ist es halt schwierig *)
    20 Goal "op # : carrier G -> carrier G -> carrier G";
    21 by (res_inst_tac [("t","op #")] ssubst 1);
    22 by (rtac ext 1);
    23 by (rtac ext 1);
    24 by (rtac meta_eq_to_obj_eq 1);
    25 by (rtac (thm "binop_def") 1);
    26 by (Asm_full_simp_tac 1);
    27 qed "binop_funcset";
    28 
    29 Goal "[| x: carrier G; y: carrier G |] ==> x # y : carrier G";
    30 by (asm_simp_tac
    31     (simpset() addsimps [binop_funcset RS funcset_mem RS funcset_mem]) 1);
    32 qed "binop_closed";
    33 
    34 Addsimps [binop_closed, e_closed];
    35 
    36 Goal "INV : carrier G -> carrier G";
    37 by (asm_simp_tac (simpset() addsimps [thm "inv_def"]) 1);
    38 qed "inv_funcset";
    39 
    40 Goal "x: carrier G ==> i(x) : carrier G";
    41 by (asm_simp_tac (simpset() addsimps [inv_funcset RS funcset_mem]) 1);
    42 qed "inv_closed"; 
    43 
    44 Goal "x: carrier G ==> e # x = x";
    45 by (asm_simp_tac (simpset() addsimps [thm "e_def", thm "binop_def"]) 1);
    46 qed "e_ax1";
    47 
    48 Goal "x: carrier G ==> i(x) # x = e";
    49 by (asm_simp_tac
    50     (simpset() addsimps [thm "binop_def", thm "inv_def", thm "e_def"]) 1);
    51 qed "inv_ax2";
    52 
    53 Addsimps [inv_closed, e_ax1, inv_ax2];
    54 
    55 Goal "[| x: carrier G; y: carrier G; z: carrier G |]\
    56 \               ==> (x # y) # z = x # (y # z)";
    57 by (asm_simp_tac (simpset() addsimps [thm "binop_def"]) 1);
    58 qed "binop_assoc";
    59 
    60 Goal "[|f : A -> A -> A; i: A -> A; e1: A;\
    61 \        ! x: A. (f (i x) x = e1); ! x: A. (f e1 x = x);\
    62 \        ! x: A. ! y: A. ! z: A.(f (f x y) z = f (x) (f y z)) |] \
    63 \     ==> (| carrier = A, bin_op = f, inverse = i, unit = e1 |) : Group";
    64 by (asm_simp_tac (simpset() addsimps [Group_def]) 1);
    65 qed "GroupI";
    66 
    67 (*****)
    68 (* Now the real derivations *)
    69 
    70 Goal "[| x # y  =  x # z;  \
    71 \        x : carrier G ; y : carrier G; z : carrier G |] ==> y = z";
    72 by (res_inst_tac [("P","%r. r = z")] (e_ax1 RS subst) 1);
    73 by (assume_tac 1);
    74 (* great: we can use the nice syntax even in res_inst_tac *)
    75 by (res_inst_tac [("P","%r. r # y = z")] (inv_ax2 RS subst) 1);
    76 by (assume_tac 1);
    77 by (asm_simp_tac (simpset() delsimps [inv_ax2] addsimps [binop_assoc]) 1);
    78 by (asm_simp_tac (simpset() addsimps [binop_assoc RS sym]) 1);
    79 qed "left_cancellation";
    80 
    81 
    82 (* Here are the other directions of basic lemmas. 
    83    They needed a cancellation (left) to be able to show the other
    84    directions of inverse and unity axiom.*)
    85 Goal "x: carrier G ==> x # e = x";
    86 by (rtac left_cancellation 1);
    87 by (etac inv_closed 2);
    88 by (auto_tac (claset(), simpset() addsimps [binop_assoc RS sym]));
    89 qed "e_ax2";
    90 
    91 Addsimps [e_ax2];
    92 
    93 Goal "[| x: carrier G; x # x = x |] ==> x = e";
    94 by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS ssubst) 1);
    95 by (etac left_cancellation 2);
    96 by Auto_tac;
    97 qed "idempotent_e";
    98 
    99 Goal  "x: carrier G ==> x # i(x) = e";
   100 by (rtac idempotent_e 1);
   101 by (Asm_simp_tac 1);
   102 by (subgoal_tac "(x # i(x)) # x # i(x) = x # (i(x) # x) # i(x)" 1);
   103 by (asm_simp_tac (simpset() delsimps [inv_ax2]
   104 			    addsimps [binop_assoc]) 2);
   105 by Auto_tac;
   106 qed "inv_ax1";
   107 
   108 Addsimps [inv_ax1];
   109 
   110 Goal "[| x # y = e; x: carrier G; y: carrier G |] ==> y = i(x)";
   111 by (res_inst_tac [("x","x")] left_cancellation 1);
   112 by Auto_tac;
   113 qed "inv_unique";
   114 
   115 Goal "x : carrier G ==> i(i(x)) = x";
   116 by (res_inst_tac [("x","i(x)")] left_cancellation 1);
   117 by Auto_tac;
   118 qed "inv_inv";
   119 
   120 Addsimps [inv_inv];
   121 
   122 Goal "[| x : carrier G; y : carrier G |] ==> i(x # y) = i(y) # i(x)";
   123 by (rtac (inv_unique RS sym) 1);
   124 by (subgoal_tac "(x # y) # i(y) # i(x) = x # (y # i(y)) # i(x)" 1);
   125 by (asm_simp_tac (simpset() delsimps [inv_ax1, inv_ax2]
   126 			    addsimps [binop_assoc]) 2);
   127 by Auto_tac;
   128 qed "inv_prod";
   129 
   130 
   131 Goal "[| y # x = z # x;  x : carrier G; y : carrier G; \
   132 \        z : carrier G |] ==> y = z";
   133 by (res_inst_tac [("P","%r. r = z")] (e_ax2 RS subst) 1);
   134 by (assume_tac 1);
   135 by (res_inst_tac [("P","%r. y # r = z")] (inv_ax1 RS subst) 1);
   136 by (assume_tac 1);
   137 by (asm_simp_tac (simpset() delsimps [inv_ax1] 
   138 		  addsimps [binop_assoc RS sym]) 1);
   139 by (asm_simp_tac (simpset() addsimps [binop_assoc]) 1);
   140 qed "right_cancellation";
   141 
   142 Close_locale();
   143 
   144 (* example what happens if export *)
   145 val Left_cancellation = export left_cancellation;