35 |
35 |
36 Goal "INV : carrier G -> carrier G"; |
36 Goal "INV : carrier G -> carrier G"; |
37 by (asm_simp_tac (simpset() addsimps [thm "inv_def"]) 1); |
37 by (asm_simp_tac (simpset() addsimps [thm "inv_def"]) 1); |
38 qed "inv_funcset"; |
38 qed "inv_funcset"; |
39 |
39 |
40 Goal "x: carrier G ==> x -| : carrier G"; |
40 Goal "x: carrier G ==> i(x) : carrier G"; |
41 by (asm_simp_tac (simpset() addsimps [inv_funcset RS funcset_mem]) 1); |
41 by (asm_simp_tac (simpset() addsimps [inv_funcset RS funcset_mem]) 1); |
42 qed "inv_closed"; |
42 qed "inv_closed"; |
43 |
43 |
44 Goal "x: carrier G ==> e # x = x"; |
44 Goal "x: carrier G ==> e # x = x"; |
45 by (asm_simp_tac (simpset() addsimps [thm "e_def", thm "binop_def"]) 1); |
45 by (asm_simp_tac (simpset() addsimps [thm "e_def", thm "binop_def"]) 1); |
46 qed "e_ax1"; |
46 qed "e_ax1"; |
47 |
47 |
48 Goal "x: carrier G ==> (x -|) # x = e"; |
48 Goal "x: carrier G ==> i(x) # x = e"; |
49 by (asm_simp_tac |
49 by (asm_simp_tac |
50 (simpset() addsimps [thm "binop_def", thm "inv_def", thm "e_def"]) 1); |
50 (simpset() addsimps [thm "binop_def", thm "inv_def", thm "e_def"]) 1); |
51 qed "inv_ax2"; |
51 qed "inv_ax2"; |
52 |
52 |
53 Addsimps [inv_closed, e_ax1, inv_ax2]; |
53 Addsimps [inv_closed, e_ax1, inv_ax2]; |
94 by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS ssubst) 1); |
94 by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS ssubst) 1); |
95 by (etac left_cancellation 2); |
95 by (etac left_cancellation 2); |
96 by Auto_tac; |
96 by Auto_tac; |
97 qed "idempotent_e"; |
97 qed "idempotent_e"; |
98 |
98 |
99 Goal "x: carrier G ==> x # (x -|) = e"; |
99 Goal "x: carrier G ==> x # i(x) = e"; |
100 by (rtac idempotent_e 1); |
100 by (rtac idempotent_e 1); |
101 by (Asm_simp_tac 1); |
101 by (Asm_simp_tac 1); |
102 by (subgoal_tac "(x # x -|) # x # x -| = x # (x -| # x) # x -|" 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] |
103 by (asm_simp_tac (simpset() delsimps [inv_ax2] |
104 addsimps [binop_assoc]) 2); |
104 addsimps [binop_assoc]) 2); |
105 by Auto_tac; |
105 by Auto_tac; |
106 qed "inv_ax1"; |
106 qed "inv_ax1"; |
107 |
107 |
108 Addsimps [inv_ax1]; |
108 Addsimps [inv_ax1]; |
109 |
109 |
110 Goal "[| x # y = e; x: carrier G; y: carrier G |] ==> y = x -|"; |
110 Goal "[| x # y = e; x: carrier G; y: carrier G |] ==> y = i(x)"; |
111 by (res_inst_tac [("x","x")] left_cancellation 1); |
111 by (res_inst_tac [("x","x")] left_cancellation 1); |
112 by Auto_tac; |
112 by Auto_tac; |
113 qed "inv_unique"; |
113 qed "inv_unique"; |
114 |
114 |
115 Goal "x : carrier G ==> x -| -| = x"; |
115 Goal "x : carrier G ==> i(i(x)) = x"; |
116 by (res_inst_tac [("x","x -|")] left_cancellation 1); |
116 by (res_inst_tac [("x","i(x)")] left_cancellation 1); |
117 by Auto_tac; |
117 by Auto_tac; |
118 qed "inv_inv"; |
118 qed "inv_inv"; |
119 |
119 |
120 Addsimps [inv_inv]; |
120 Addsimps [inv_inv]; |
121 |
121 |
122 Goal "[| x : carrier G; y : carrier G |] ==> (x # y) -| = y -| # x -|"; |
122 Goal "[| x : carrier G; y : carrier G |] ==> i(x # y) = i(y) # i(x)"; |
123 by (rtac (inv_unique RS sym) 1); |
123 by (rtac (inv_unique RS sym) 1); |
124 by (subgoal_tac "(x # y) # y -| # x -| = x # (y # y -|) # x -|" 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] |
125 by (asm_simp_tac (simpset() delsimps [inv_ax1, inv_ax2] |
126 addsimps [binop_assoc]) 2); |
126 addsimps [binop_assoc]) 2); |
127 by Auto_tac; |
127 by Auto_tac; |
128 qed "inv_prod"; |
128 qed "inv_prod"; |
129 |
129 |