# HG changeset patch
# User paulson
# Date 995903135 -7200
# Node ID 01ee48a808008017d8e1f0fdb48dce6ca244c3cf
# Parent  b24017251fc1166c728aaae6f7f5e3b608a3ecb4
PiSets moved to GroupTheory, while LocaleGroup deleted

diff -r b24017251fc1 -r 01ee48a80800 src/HOL/ex/LocaleGroup.ML
--- a/src/HOL/ex/LocaleGroup.ML	Mon Jul 23 17:45:07 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,145 +0,0 @@
-(*  Title:      HOL/ex/LocaleGroup.ML
-    ID:         $Id$
-    Author:     Florian Kammueller, University of Cambridge
-
-Group theory via records and locales.
-*)
-
-Open_locale "groups";
-print_locales LocaleGroup.thy;
-
-val simp_G = simplify (simpset() addsimps [Group_def]) (thm "Group_G");
-Addsimps [simp_G, thm "Group_G"];
-
-
-Goal "e : carrier G";
-by (simp_tac (simpset() addsimps [thm "e_def"]) 1);
-qed "e_closed";
-
-(* Mit dieser Def ist es halt schwierig *)
-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);
-qed "binop_funcset";
-
-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";
-
-Addsimps [binop_closed, e_closed];
-
-Goal "INV : carrier G -> carrier G";
-by (asm_simp_tac (simpset() addsimps [thm "inv_def"]) 1);
-qed "inv_funcset";
-
-Goal "x: carrier G ==> i(x) : carrier G";
-by (asm_simp_tac (simpset() addsimps [inv_funcset RS funcset_mem]) 1);
-qed "inv_closed"; 
-
-Goal "x: carrier G ==> e # x = x";
-by (asm_simp_tac (simpset() addsimps [thm "e_def", thm "binop_def"]) 1);
-qed "e_ax1";
-
-Goal "x: carrier G ==> i(x) # x = e";
-by (asm_simp_tac
-    (simpset() addsimps [thm "binop_def", thm "inv_def", thm "e_def"]) 1);
-qed "inv_ax2";
-
-Addsimps [inv_closed, e_ax1, inv_ax2];
-
-Goal "[| x: carrier G; y: carrier G; z: carrier G |]\
-\               ==> (x # y) # z = x # (y # z)";
-by (asm_simp_tac (simpset() addsimps [thm "binop_def"]) 1);
-qed "binop_assoc";
-
-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 "[| 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")] (inv_ax2 RS subst) 1);
-by (assume_tac 1);
-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.*)
-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  "x: carrier G ==> x # i(x) = e";
-by (rtac idempotent_e 1);
-by (Asm_simp_tac 1);
-by (subgoal_tac "(x # i(x)) # x # i(x) = x # (i(x) # x) # i(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 = i(x)";
-by (res_inst_tac [("x","x")] left_cancellation 1);
-by Auto_tac;
-qed "inv_unique";
-
-Goal "x : carrier G ==> i(i(x)) = x";
-by (res_inst_tac [("x","i(x)")] left_cancellation 1);
-by Auto_tac;
-qed "inv_inv";
-
-Addsimps [inv_inv];
-
-Goal "[| x : carrier G; y : carrier G |] ==> i(x # y) = i(y) # i(x)";
-by (rtac (inv_unique RS sym) 1);
-by (subgoal_tac "(x # y) # i(y) # i(x) = x # (y # i(y)) # i(x)" 1);
-by (asm_simp_tac (simpset() delsimps [inv_ax1, inv_ax2]
-			    addsimps [binop_assoc]) 2);
-by Auto_tac;
-qed "inv_prod";
-
-
-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")] (inv_ax1 RS subst) 1);
-by (assume_tac 1);
-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 "groups";
-
-(* example what happens if export *)
-val Left_cancellation = export left_cancellation;
diff -r b24017251fc1 -r 01ee48a80800 src/HOL/ex/LocaleGroup.thy
--- a/src/HOL/ex/LocaleGroup.thy	Mon Jul 23 17:45:07 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      HOL/ex/LocaleGroup.thy
-    ID:         $Id$
-    Author:     Florian Kammueller, University of Cambridge
-
-Group theory via records and locales.
-*)
-
-LocaleGroup =   PiSets + Record +
-
-record 'a grouptype = 
-  carrier  :: "'a set"    
-  bin_op   :: "['a, 'a] => 'a"
-  inverse  :: "'a => 'a"
-  unit     :: "'a"
-
-constdefs
-  Group :: "('a, 'more::more) grouptype_scheme set"
-  "Group == {G. (bin_op G): carrier G -> carrier G -> carrier G &
-	        inverse G : carrier G -> carrier G 
-             & unit G : carrier G &
-             (! x: carrier G. ! y: carrier G. !z: carrier G.
-                       (bin_op G (inverse G x) x = unit G) 
-                     & (bin_op G (unit G) x = x) 
-                     & (bin_op G (bin_op G x y) z =
-			bin_op G (x) (bin_op G y z)))}"
-
-locale groups =
-  fixes 
-    G        ::"('a, 'more :: more) grouptype_scheme"
-    e        :: "'a"
-    binop    :: "'a => 'a => 'a" 	(infixr "#" 80)
-	(*INV renamed from inv temporarily to avoid clash with Fun.inv*)
-    INV      :: "'a => 'a"              ("i'(_')")
-  assumes
-    Group_G   "G: Group"
-  defines
-    e_def      "e == unit G"
-    binop_def  "x # y == bin_op G x y"
-    inv_def    "INV == inverse G"
-
-end
diff -r b24017251fc1 -r 01ee48a80800 src/HOL/ex/PiSets.ML
--- a/src/HOL/ex/PiSets.ML	Mon Jul 23 17:45:07 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(*  Title:      HOL/ex/PiSets.ML
-    ID:         $Id$
-    Author:     Florian Kammueller, University of Cambridge
-
-Pi sets and their application.
-*)
-
-(*** Bijection between Pi in terms of => and Pi in terms of Sigma ***)
-Goal "f: Pi A B ==> PiBij A B f <= Sigma A B";
-by (auto_tac (claset(),
-	      simpset() addsimps [PiBij_def,Pi_def]));
-qed "PiBij_subset_Sigma";
-
-Goal "f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";
-by (auto_tac (claset(), simpset() addsimps [PiBij_def]));
-qed "PiBij_unique";
-
-Goal "f: Pi A B ==> PiBij A B f : Graph A B";
-by (asm_simp_tac (simpset() addsimps [Graph_def,PiBij_unique,
-				      PiBij_subset_Sigma]) 1);
-qed "PiBij_in_Graph";
-
-Goalw [PiBij_def, Graph_def] "PiBij A B:  Pi A B -> Graph A B";
-by (rtac restrictI 1);
-by (auto_tac (claset(), simpset() addsimps [Pi_def]));
-qed "PiBij_func";
-
-Goal "inj_on (PiBij A B) (Pi A B)";
-by (rtac inj_onI 1);
-by (rtac Pi_extensionality 1);			
-by (assume_tac 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [PiBij_def]) 1);
-by (Blast_tac 1);
-qed "inj_PiBij";
-
-
-Goal "x \\<in> Graph A B \\<Longrightarrow> (lam a:A. SOME y. (a, y) \\<in> x) \\<in> Pi A B";
-by (rtac restrictI 1);
-by (res_inst_tac [("P", "%xa. (a, xa) : x")] ex1E 1);
- by (force_tac (claset(), simpset() addsimps [Graph_def]) 1);
-by (full_simp_tac (simpset() addsimps [Graph_def]) 1);
-by (stac some_equality 1);
-  by (assume_tac 1);
- by (Blast_tac 1);
-by (Blast_tac 1);
-qed "in_Graph_imp_in_Pi";
-
-Goal "PiBij A B ` (Pi A B) = Graph A B";
-by (rtac equalityI 1);
-by (force_tac (claset(), simpset() addsimps [PiBij_in_Graph]) 1);
-by (rtac subsetI 1);
-by (rtac image_eqI 1); 
-by (etac in_Graph_imp_in_Pi 2); 
-(* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
-by (asm_simp_tac (simpset() addsimps [in_Graph_imp_in_Pi, PiBij_def]) 1);
-by (auto_tac (claset(), simpset() addsimps [some1_equality, Graph_def])); 
-by (fast_tac (claset() addIs [someI2]) 1);
-qed "surj_PiBij";
-
-Goal "f: Pi A B ==> \
-\     (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";
-by (asm_simp_tac (simpset() addsimps [Inv_f_f, PiBij_in_Graph, PiBij_func, 
-                                      inj_PiBij, surj_PiBij]) 1);
-qed "PiBij_bij1";
-
-Goal "[| f: Graph A B  |] ==> \
-\    (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f";
-by (rtac (PiBij_func RS f_Inv_f) 1);
-by (asm_full_simp_tac (simpset() addsimps [surj_PiBij]) 1);
-by (assume_tac 1);
-qed "PiBij_bij2";
diff -r b24017251fc1 -r 01ee48a80800 src/HOL/ex/PiSets.thy
--- a/src/HOL/ex/PiSets.thy	Mon Jul 23 17:45:07 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(*  Title:      HOL/ex/PiSets.thy
-    ID:         $Id$
-    Author:     Florian Kammueller, University of Cambridge
-
-The bijection between elements of the Pi set and functional graphs
-
-Also the nice -> operator for function space
-*)
-
-PiSets = Datatype_Universe + Finite +
-
-syntax
-  "->" :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
-
-translations
-  "A -> B" == "A funcset B"
-
-constdefs
-(* bijection between Pi_sig and Pi_=> *)
-  PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
-    "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
-
-  Graph ::  "['a set, 'a => 'b set] => ('a * 'b) set set"
-   "Graph A B == {f. f: Pow(Sigma A B) & (! x: A. (?! y. (x, y): f))}"
-
-end
diff -r b24017251fc1 -r 01ee48a80800 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Mon Jul 23 17:45:07 2001 +0200
+++ b/src/HOL/ex/ROOT.ML	Mon Jul 23 17:45:35 2001 +0200
@@ -33,10 +33,6 @@
 time_use_thy "MonoidGroup";
 time_use_thy "Records";
 
-(*groups via locales*)
-time_use_thy "PiSets";
-time_use_thy "LocaleGroup";
-
 (*advanced concrete syntax*)
 time_use_thy "Tuple";
 time_use_thy "Antiquote";