--- 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;
--- 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
--- 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";
--- 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
--- 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";