--- a/src/HOL/ex/LocaleGroup.ML Tue Nov 10 16:28:08 1998 +0100
+++ b/src/HOL/ex/LocaleGroup.ML Wed Nov 11 15:44:24 1998 +0100
@@ -12,190 +12,134 @@
Addsimps [simp_G, thm "Group_G"];
-goal LocaleGroup.thy "e : carrier G";
-by (afs [thm "e_def"] 1);
-val e_closed = result();
+Goal "e : carrier G";
+by (simp_tac (simpset() addsimps [thm "e_def"]) 1);
+qed "e_closed";
(* Mit dieser Def ist es halt schwierig *)
-goal LocaleGroup.thy "op # : carrier G -> carrier G -> carrier G";
+Goal "op # : carrier G -> carrier G -> carrier G";
by (res_inst_tac [("t","op #")] ssubst 1);
by (rtac ext 1);
by (rtac ext 1);
by (rtac meta_eq_to_obj_eq 1);
by (rtac (thm "binop_def") 1);
by (Asm_full_simp_tac 1);
-val binop_funcset = result();
+qed "binop_funcset";
-goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G |] ==> x # y : carrier G";
-by (afs [binop_funcset RS funcset2E1] 1);
-val binop_closed = result();
+Goal "[| x: carrier G; y: carrier G |] ==> x # y : carrier G";
+by (asm_simp_tac
+ (simpset() addsimps [binop_funcset RS funcset_mem RS funcset_mem]) 1);
+qed "binop_closed";
-goal LocaleGroup.thy "inv : carrier G -> carrier G";
-by (res_inst_tac [("t","inv")] ssubst 1);
-by (rtac ext 1);
-by (rtac meta_eq_to_obj_eq 1);
-by (rtac (thm "inv_def") 1);
-by (Asm_full_simp_tac 1);
-val inv_funcset = result();
+Addsimps [binop_closed, e_closed];
-goal LocaleGroup.thy "!! x . x: carrier G ==> x -| : carrier G";
-by (afs [inv_funcset RS funcsetE1] 1);
-val inv_closed = result();
+Goal "INV : carrier G -> carrier G";
+by (asm_simp_tac (simpset() addsimps [thm "inv_def"]) 1);
+qed "inv_funcset";
+Goal "x: carrier G ==> x -| : carrier G";
+by (asm_simp_tac (simpset() addsimps [inv_funcset RS funcset_mem]) 1);
+qed "inv_closed";
-goal LocaleGroup.thy "!! x . x: carrier G ==> e # x = x";
-by (afs [thm "e_def", thm "binop_def"] 1);
-val e_ax1 = result();
+Goal "x: carrier G ==> e # x = x";
+by (asm_simp_tac (simpset() addsimps [thm "e_def", thm "binop_def"]) 1);
+qed "e_ax1";
-goal LocaleGroup.thy "!! x. x: carrier G ==> (x -|) # x = e";
-by (afs [thm "binop_def", thm "inv_def", thm "e_def"] 1);
-val inv_ax2 = result();
+Goal "x: carrier G ==> (x -|) # x = e";
+by (asm_simp_tac
+ (simpset() addsimps [thm "binop_def", thm "inv_def", thm "e_def"]) 1);
+qed "inv_ax2";
-goal LocaleGroup.thy "!! x y z. [| x: carrier G; y: carrier G; z: carrier G |]\
+Addsimps [inv_closed, e_ax1, inv_ax2];
+
+Goal "[| x: carrier G; y: carrier G; z: carrier G |]\
\ ==> (x # y) # z = x # (y # z)";
-by (afs [thm "binop_def"] 1);
-val binop_assoc = result();
+by (asm_simp_tac (simpset() addsimps [thm "binop_def"]) 1);
+qed "binop_assoc";
-goal LocaleGroup.thy "!! G f i e1. [|f : G -> G -> G; i: G -> G; e1: G;\
-\ ! x: G. (f (i x) x = e1); ! x: G. (f e1 x = x);\
-\ ! x: G. ! y: G. ! z: G.(f (f x y) z = f (x) (f y z)) |] \
-\ ==> (| carrier = G, bin_op = f, inverse = i, unit = e1 |) : Group";
-by (afs [Group_def] 1);
-val GroupI = result();
+Goal "[|f : A -> A -> A; i: A -> A; e1: A;\
+\ ! x: A. (f (i x) x = e1); ! x: A. (f e1 x = x);\
+\ ! x: A. ! y: A. ! z: A.(f (f x y) z = f (x) (f y z)) |] \
+\ ==> (| carrier = A, bin_op = f, inverse = i, unit = e1 |) : Group";
+by (asm_simp_tac (simpset() addsimps [Group_def]) 1);
+qed "GroupI";
(*****)
(* Now the real derivations *)
-goal LocaleGroup.thy "!! x y z. [| x : carrier G ; y : carrier G; z : carrier G;\
-\ x # y = x # z |] ==> y = z";
-(* remarkable: In the following step the use of e_ax1 instead of unit_ax1
- is better! It doesn't produce G: Group as subgoal and the nice syntax stays *)
+Goal "[| x # y = x # z; \
+\ x : carrier G ; y : carrier G; z : carrier G |] ==> y = z";
by (res_inst_tac [("P","%r. r = z")] (e_ax1 RS subst) 1);
by (assume_tac 1);
(* great: we can use the nice syntax even in res_inst_tac *)
-by (res_inst_tac [("P","%r. r # y = z")] subst 1);
-by (res_inst_tac [("x","x")] inv_ax2 1);
-by (assume_tac 1);
-by (stac binop_assoc 1);
-by (rtac inv_closed 1);
-by (assume_tac 1);
-by (assume_tac 1);
+by (res_inst_tac [("P","%r. r # y = z")] (inv_ax2 RS subst) 1);
by (assume_tac 1);
-by (etac ssubst 1);
-by (rtac (binop_assoc RS subst) 1);
-by (rtac inv_closed 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (stac inv_ax2 1);
-by (assume_tac 1);
-by (stac e_ax1 1);
-by (assume_tac 1);
-by (rtac refl 1);
-val left_cancellation = result();
+by (asm_simp_tac (simpset() delsimps [inv_ax2] addsimps [binop_assoc]) 1);
+by (asm_simp_tac (simpset() addsimps [binop_assoc RS sym]) 1);
+qed "left_cancellation";
-(* here are the other directions of basic lemmas, they needed a cancellation (left) *)
-(* to be able to show the other directions of inverse and unity axiom we need:*)
-goal LocaleGroup.thy "!! x. x: carrier G ==> x # e = x";
-(* here is a problem with res_inst_tac: in Fun there is a
- constant inv, and that gets addressed when we type in -|.
- We have to use the defining term and then fold the def of inv *)
-by (res_inst_tac [("x","inverse G x")] left_cancellation 1);
-by (fold_goals_tac [thm "inv_def"]);
-by (fast_tac (claset() addSEs [inv_closed]) 1);
-by (afs [binop_closed, e_closed] 1);
-by (assume_tac 1);
-by (rtac (binop_assoc RS subst) 1);
-by (fast_tac (claset() addSEs [inv_closed]) 1);
-by (assume_tac 1);
-by (rtac (e_closed) 1);
-by (stac inv_ax2 1);
-by (assume_tac 1);
-by (stac e_ax1 1);
-by (rtac e_closed 1);
-by (rtac refl 1);
-val e_ax2 = result();
+(* Here are the other directions of basic lemmas.
+ They needed a cancellation (left) to be able to show the other
+ directions of inverse and unity axiom.*)
+Goal "x: carrier G ==> x # e = x";
+by (rtac left_cancellation 1);
+by (etac inv_closed 2);
+by (auto_tac (claset(), simpset() addsimps [binop_assoc RS sym]));
+qed "e_ax2";
+
+Addsimps [e_ax2];
+
+Goal "[| x: carrier G; x # x = x |] ==> x = e";
+by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS ssubst) 1);
+by (etac left_cancellation 2);
+by Auto_tac;
+qed "idempotent_e";
-goal LocaleGroup.thy "!! x. [| x: carrier G; x # x = x |] ==> x = e";
-by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS forw_subst) 1);
-by (assume_tac 1);
-by (res_inst_tac [("x","x")] left_cancellation 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (rtac e_closed 1);
-by (assume_tac 1);
-val idempotent_e = result();
-
-goal LocaleGroup.thy "!! x. x: carrier G ==> x # (x -|) = e";
+Goal "x: carrier G ==> x # (x -|) = e";
by (rtac idempotent_e 1);
-by (afs [binop_closed,inv_closed] 1);
-by (stac binop_assoc 1);
-by (assume_tac 1);
-by (afs [inv_closed] 1);
-by (afs [binop_closed,inv_closed] 1);
-by (res_inst_tac [("t","x -| # x # x -|")] subst 1);
-by (rtac binop_assoc 1);
-by (afs [inv_closed] 1);
-by (assume_tac 1);
-by (afs [inv_closed] 1);
-by (stac inv_ax2 1);
-by (assume_tac 1);
-by (stac e_ax1 1);
-by (afs [inv_closed] 1);
-by (rtac refl 1);
-val inv_ax1 = result();
+by (Asm_simp_tac 1);
+by (subgoal_tac "(x # x -|) # x # x -| = x # (x -| # x) # x -|" 1);
+by (asm_simp_tac (simpset() delsimps [inv_ax2]
+ addsimps [binop_assoc]) 2);
+by Auto_tac;
+qed "inv_ax1";
+
+Addsimps [inv_ax1];
+
+Goal "[| x # y = e; x: carrier G; y: carrier G |] ==> y = x -|";
+by (res_inst_tac [("x","x")] left_cancellation 1);
+by Auto_tac;
+qed "inv_unique";
+
+Goal "x : carrier G ==> x -| -| = x";
+by (res_inst_tac [("x","x -|")] left_cancellation 1);
+by Auto_tac;
+qed "inv_inv";
+
+Addsimps [inv_inv];
+
+Goal "[| x : carrier G; y : carrier G |] ==> (x # y) -| = y -| # x -|";
+by (rtac (inv_unique RS sym) 1);
+by (subgoal_tac "(x # y) # y -| # x -| = x # (y # y -|) # x -|" 1);
+by (asm_simp_tac (simpset() delsimps [inv_ax1, inv_ax2]
+ addsimps [binop_assoc]) 2);
+by Auto_tac;
+qed "inv_prod";
-goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G; \
-\ x # y = e |] ==> y = x -|";
-by (res_inst_tac [("x","x")] left_cancellation 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (afs [inv_closed] 1);
-by (stac inv_ax1 1);
-by (assume_tac 1);
-by (assume_tac 1);
-val inv_unique = result();
-
-goal LocaleGroup.thy "!! x. x : carrier G ==> x -| -| = x";
-by (res_inst_tac [("x","inverse G x")] left_cancellation 1);
-by (fold_goals_tac [thm "inv_def"]);
-by (afs [inv_closed] 1);
-by (afs [inv_closed] 1);
-by (assume_tac 1);
-by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
-val inv_inv = result();
-
-goal LocaleGroup.thy "!! x y. [| x : carrier G; y : carrier G |]\
-\ ==> (x # y) -| = y -| # x -|";
-by (rtac sym 1);
-by (rtac inv_unique 1);
-by (afs [binop_closed] 1);
-by (afs [inv_closed,binop_closed] 1);
-by (afs [binop_assoc,inv_closed,binop_closed] 1);
-by (res_inst_tac [("x1","y")] (binop_assoc RS subst) 1);
-by (assume_tac 1);
-by (afs [inv_closed] 1);
-by (afs [inv_closed] 1);
-by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
-val inv_prod = result();
-
-
-goal LocaleGroup.thy "!! x y z. [| x : carrier G; y : carrier G;\
-\ z : carrier G; y # x = z # x|] ==> y = z";
+Goal "[| y # x = z # x; x : carrier G; y : carrier G; \
+\ z : carrier G |] ==> y = z";
by (res_inst_tac [("P","%r. r = z")] (e_ax2 RS subst) 1);
by (assume_tac 1);
-by (res_inst_tac [("P","%r. y # r = z")] subst 1);
-by (rtac inv_ax1 1);
-by (assume_tac 1);
-by (rtac (binop_assoc RS subst) 1);
+by (res_inst_tac [("P","%r. y # r = z")] (inv_ax1 RS subst) 1);
by (assume_tac 1);
-by (assume_tac 1);
-by (afs [inv_closed] 1);
-by (etac ssubst 1);
-by (afs [binop_assoc,inv_closed,inv_ax1,e_ax2] 1);
-val right_cancellation = result();
+by (asm_simp_tac (simpset() delsimps [inv_ax1]
+ addsimps [binop_assoc RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [binop_assoc]) 1);
+qed "right_cancellation";
+
+Close_locale();
(* example what happens if export *)
val Left_cancellation = export left_cancellation;