PiSets moved to GroupTheory, while LocaleGroup deleted
authorpaulson
Mon Jul 23 17:45:35 2001 +0200 (2001-07-23)
changeset 1144501ee48a80800
parent 11444 b24017251fc1
child 11446 882d6b54cebf
PiSets moved to GroupTheory, while LocaleGroup deleted
src/HOL/ex/LocaleGroup.ML
src/HOL/ex/LocaleGroup.thy
src/HOL/ex/PiSets.ML
src/HOL/ex/PiSets.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/ex/LocaleGroup.ML	Mon Jul 23 17:45:07 2001 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,145 +0,0 @@
     1.4 -(*  Title:      HOL/ex/LocaleGroup.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Florian Kammueller, University of Cambridge
     1.7 -
     1.8 -Group theory via records and locales.
     1.9 -*)
    1.10 -
    1.11 -Open_locale "groups";
    1.12 -print_locales LocaleGroup.thy;
    1.13 -
    1.14 -val simp_G = simplify (simpset() addsimps [Group_def]) (thm "Group_G");
    1.15 -Addsimps [simp_G, thm "Group_G"];
    1.16 -
    1.17 -
    1.18 -Goal "e : carrier G";
    1.19 -by (simp_tac (simpset() addsimps [thm "e_def"]) 1);
    1.20 -qed "e_closed";
    1.21 -
    1.22 -(* Mit dieser Def ist es halt schwierig *)
    1.23 -Goal "op # : carrier G -> carrier G -> carrier G";
    1.24 -by (res_inst_tac [("t","op #")] ssubst 1);
    1.25 -by (rtac ext 1);
    1.26 -by (rtac ext 1);
    1.27 -by (rtac meta_eq_to_obj_eq 1);
    1.28 -by (rtac (thm "binop_def") 1);
    1.29 -by (Asm_full_simp_tac 1);
    1.30 -qed "binop_funcset";
    1.31 -
    1.32 -Goal "[| x: carrier G; y: carrier G |] ==> x # y : carrier G";
    1.33 -by (asm_simp_tac
    1.34 -    (simpset() addsimps [binop_funcset RS funcset_mem RS funcset_mem]) 1);
    1.35 -qed "binop_closed";
    1.36 -
    1.37 -Addsimps [binop_closed, e_closed];
    1.38 -
    1.39 -Goal "INV : carrier G -> carrier G";
    1.40 -by (asm_simp_tac (simpset() addsimps [thm "inv_def"]) 1);
    1.41 -qed "inv_funcset";
    1.42 -
    1.43 -Goal "x: carrier G ==> i(x) : carrier G";
    1.44 -by (asm_simp_tac (simpset() addsimps [inv_funcset RS funcset_mem]) 1);
    1.45 -qed "inv_closed"; 
    1.46 -
    1.47 -Goal "x: carrier G ==> e # x = x";
    1.48 -by (asm_simp_tac (simpset() addsimps [thm "e_def", thm "binop_def"]) 1);
    1.49 -qed "e_ax1";
    1.50 -
    1.51 -Goal "x: carrier G ==> i(x) # x = e";
    1.52 -by (asm_simp_tac
    1.53 -    (simpset() addsimps [thm "binop_def", thm "inv_def", thm "e_def"]) 1);
    1.54 -qed "inv_ax2";
    1.55 -
    1.56 -Addsimps [inv_closed, e_ax1, inv_ax2];
    1.57 -
    1.58 -Goal "[| x: carrier G; y: carrier G; z: carrier G |]\
    1.59 -\               ==> (x # y) # z = x # (y # z)";
    1.60 -by (asm_simp_tac (simpset() addsimps [thm "binop_def"]) 1);
    1.61 -qed "binop_assoc";
    1.62 -
    1.63 -Goal "[|f : A -> A -> A; i: A -> A; e1: A;\
    1.64 -\        ! x: A. (f (i x) x = e1); ! x: A. (f e1 x = x);\
    1.65 -\        ! x: A. ! y: A. ! z: A.(f (f x y) z = f (x) (f y z)) |] \
    1.66 -\     ==> (| carrier = A, bin_op = f, inverse = i, unit = e1 |) : Group";
    1.67 -by (asm_simp_tac (simpset() addsimps [Group_def]) 1);
    1.68 -qed "GroupI";
    1.69 -
    1.70 -(*****)
    1.71 -(* Now the real derivations *)
    1.72 -
    1.73 -Goal "[| x # y  =  x # z;  \
    1.74 -\        x : carrier G ; y : carrier G; z : carrier G |] ==> y = z";
    1.75 -by (res_inst_tac [("P","%r. r = z")] (e_ax1 RS subst) 1);
    1.76 -by (assume_tac 1);
    1.77 -(* great: we can use the nice syntax even in res_inst_tac *)
    1.78 -by (res_inst_tac [("P","%r. r # y = z")] (inv_ax2 RS subst) 1);
    1.79 -by (assume_tac 1);
    1.80 -by (asm_simp_tac (simpset() delsimps [inv_ax2] addsimps [binop_assoc]) 1);
    1.81 -by (asm_simp_tac (simpset() addsimps [binop_assoc RS sym]) 1);
    1.82 -qed "left_cancellation";
    1.83 -
    1.84 -
    1.85 -(* Here are the other directions of basic lemmas. 
    1.86 -   They needed a cancellation (left) to be able to show the other
    1.87 -   directions of inverse and unity axiom.*)
    1.88 -Goal "x: carrier G ==> x # e = x";
    1.89 -by (rtac left_cancellation 1);
    1.90 -by (etac inv_closed 2);
    1.91 -by (auto_tac (claset(), simpset() addsimps [binop_assoc RS sym]));
    1.92 -qed "e_ax2";
    1.93 -
    1.94 -Addsimps [e_ax2];
    1.95 -
    1.96 -Goal "[| x: carrier G; x # x = x |] ==> x = e";
    1.97 -by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS ssubst) 1);
    1.98 -by (etac left_cancellation 2);
    1.99 -by Auto_tac;
   1.100 -qed "idempotent_e";
   1.101 -
   1.102 -Goal  "x: carrier G ==> x # i(x) = e";
   1.103 -by (rtac idempotent_e 1);
   1.104 -by (Asm_simp_tac 1);
   1.105 -by (subgoal_tac "(x # i(x)) # x # i(x) = x # (i(x) # x) # i(x)" 1);
   1.106 -by (asm_simp_tac (simpset() delsimps [inv_ax2]
   1.107 -			    addsimps [binop_assoc]) 2);
   1.108 -by Auto_tac;
   1.109 -qed "inv_ax1";
   1.110 -
   1.111 -Addsimps [inv_ax1];
   1.112 -
   1.113 -Goal "[| x # y = e; x: carrier G; y: carrier G |] ==> y = i(x)";
   1.114 -by (res_inst_tac [("x","x")] left_cancellation 1);
   1.115 -by Auto_tac;
   1.116 -qed "inv_unique";
   1.117 -
   1.118 -Goal "x : carrier G ==> i(i(x)) = x";
   1.119 -by (res_inst_tac [("x","i(x)")] left_cancellation 1);
   1.120 -by Auto_tac;
   1.121 -qed "inv_inv";
   1.122 -
   1.123 -Addsimps [inv_inv];
   1.124 -
   1.125 -Goal "[| x : carrier G; y : carrier G |] ==> i(x # y) = i(y) # i(x)";
   1.126 -by (rtac (inv_unique RS sym) 1);
   1.127 -by (subgoal_tac "(x # y) # i(y) # i(x) = x # (y # i(y)) # i(x)" 1);
   1.128 -by (asm_simp_tac (simpset() delsimps [inv_ax1, inv_ax2]
   1.129 -			    addsimps [binop_assoc]) 2);
   1.130 -by Auto_tac;
   1.131 -qed "inv_prod";
   1.132 -
   1.133 -
   1.134 -Goal "[| y # x = z # x;  x : carrier G; y : carrier G; \
   1.135 -\        z : carrier G |] ==> y = z";
   1.136 -by (res_inst_tac [("P","%r. r = z")] (e_ax2 RS subst) 1);
   1.137 -by (assume_tac 1);
   1.138 -by (res_inst_tac [("P","%r. y # r = z")] (inv_ax1 RS subst) 1);
   1.139 -by (assume_tac 1);
   1.140 -by (asm_simp_tac (simpset() delsimps [inv_ax1] 
   1.141 -		  addsimps [binop_assoc RS sym]) 1);
   1.142 -by (asm_simp_tac (simpset() addsimps [binop_assoc]) 1);
   1.143 -qed "right_cancellation";
   1.144 -
   1.145 -Close_locale "groups";
   1.146 -
   1.147 -(* example what happens if export *)
   1.148 -val Left_cancellation = export left_cancellation;
     2.1 --- a/src/HOL/ex/LocaleGroup.thy	Mon Jul 23 17:45:07 2001 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,41 +0,0 @@
     2.4 -(*  Title:      HOL/ex/LocaleGroup.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Florian Kammueller, University of Cambridge
     2.7 -
     2.8 -Group theory via records and locales.
     2.9 -*)
    2.10 -
    2.11 -LocaleGroup =   PiSets + Record +
    2.12 -
    2.13 -record 'a grouptype = 
    2.14 -  carrier  :: "'a set"    
    2.15 -  bin_op   :: "['a, 'a] => 'a"
    2.16 -  inverse  :: "'a => 'a"
    2.17 -  unit     :: "'a"
    2.18 -
    2.19 -constdefs
    2.20 -  Group :: "('a, 'more::more) grouptype_scheme set"
    2.21 -  "Group == {G. (bin_op G): carrier G -> carrier G -> carrier G &
    2.22 -	        inverse G : carrier G -> carrier G 
    2.23 -             & unit G : carrier G &
    2.24 -             (! x: carrier G. ! y: carrier G. !z: carrier G.
    2.25 -                       (bin_op G (inverse G x) x = unit G) 
    2.26 -                     & (bin_op G (unit G) x = x) 
    2.27 -                     & (bin_op G (bin_op G x y) z =
    2.28 -			bin_op G (x) (bin_op G y z)))}"
    2.29 -
    2.30 -locale groups =
    2.31 -  fixes 
    2.32 -    G        ::"('a, 'more :: more) grouptype_scheme"
    2.33 -    e        :: "'a"
    2.34 -    binop    :: "'a => 'a => 'a" 	(infixr "#" 80)
    2.35 -	(*INV renamed from inv temporarily to avoid clash with Fun.inv*)
    2.36 -    INV      :: "'a => 'a"              ("i'(_')")
    2.37 -  assumes
    2.38 -    Group_G   "G: Group"
    2.39 -  defines
    2.40 -    e_def      "e == unit G"
    2.41 -    binop_def  "x # y == bin_op G x y"
    2.42 -    inv_def    "INV == inverse G"
    2.43 -
    2.44 -end
     3.1 --- a/src/HOL/ex/PiSets.ML	Mon Jul 23 17:45:07 2001 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,72 +0,0 @@
     3.4 -(*  Title:      HOL/ex/PiSets.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Florian Kammueller, University of Cambridge
     3.7 -
     3.8 -Pi sets and their application.
     3.9 -*)
    3.10 -
    3.11 -(*** Bijection between Pi in terms of => and Pi in terms of Sigma ***)
    3.12 -Goal "f: Pi A B ==> PiBij A B f <= Sigma A B";
    3.13 -by (auto_tac (claset(),
    3.14 -	      simpset() addsimps [PiBij_def,Pi_def]));
    3.15 -qed "PiBij_subset_Sigma";
    3.16 -
    3.17 -Goal "f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";
    3.18 -by (auto_tac (claset(), simpset() addsimps [PiBij_def]));
    3.19 -qed "PiBij_unique";
    3.20 -
    3.21 -Goal "f: Pi A B ==> PiBij A B f : Graph A B";
    3.22 -by (asm_simp_tac (simpset() addsimps [Graph_def,PiBij_unique,
    3.23 -				      PiBij_subset_Sigma]) 1);
    3.24 -qed "PiBij_in_Graph";
    3.25 -
    3.26 -Goalw [PiBij_def, Graph_def] "PiBij A B:  Pi A B -> Graph A B";
    3.27 -by (rtac restrictI 1);
    3.28 -by (auto_tac (claset(), simpset() addsimps [Pi_def]));
    3.29 -qed "PiBij_func";
    3.30 -
    3.31 -Goal "inj_on (PiBij A B) (Pi A B)";
    3.32 -by (rtac inj_onI 1);
    3.33 -by (rtac Pi_extensionality 1);			
    3.34 -by (assume_tac 1);
    3.35 -by (assume_tac 1);
    3.36 -by (asm_full_simp_tac (simpset() addsimps [PiBij_def]) 1);
    3.37 -by (Blast_tac 1);
    3.38 -qed "inj_PiBij";
    3.39 -
    3.40 -
    3.41 -Goal "x \\<in> Graph A B \\<Longrightarrow> (lam a:A. SOME y. (a, y) \\<in> x) \\<in> Pi A B";
    3.42 -by (rtac restrictI 1);
    3.43 -by (res_inst_tac [("P", "%xa. (a, xa) : x")] ex1E 1);
    3.44 - by (force_tac (claset(), simpset() addsimps [Graph_def]) 1);
    3.45 -by (full_simp_tac (simpset() addsimps [Graph_def]) 1);
    3.46 -by (stac some_equality 1);
    3.47 -  by (assume_tac 1);
    3.48 - by (Blast_tac 1);
    3.49 -by (Blast_tac 1);
    3.50 -qed "in_Graph_imp_in_Pi";
    3.51 -
    3.52 -Goal "PiBij A B ` (Pi A B) = Graph A B";
    3.53 -by (rtac equalityI 1);
    3.54 -by (force_tac (claset(), simpset() addsimps [PiBij_in_Graph]) 1);
    3.55 -by (rtac subsetI 1);
    3.56 -by (rtac image_eqI 1); 
    3.57 -by (etac in_Graph_imp_in_Pi 2); 
    3.58 -(* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
    3.59 -by (asm_simp_tac (simpset() addsimps [in_Graph_imp_in_Pi, PiBij_def]) 1);
    3.60 -by (auto_tac (claset(), simpset() addsimps [some1_equality, Graph_def])); 
    3.61 -by (fast_tac (claset() addIs [someI2]) 1);
    3.62 -qed "surj_PiBij";
    3.63 -
    3.64 -Goal "f: Pi A B ==> \
    3.65 -\     (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";
    3.66 -by (asm_simp_tac (simpset() addsimps [Inv_f_f, PiBij_in_Graph, PiBij_func, 
    3.67 -                                      inj_PiBij, surj_PiBij]) 1);
    3.68 -qed "PiBij_bij1";
    3.69 -
    3.70 -Goal "[| f: Graph A B  |] ==> \
    3.71 -\    (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f";
    3.72 -by (rtac (PiBij_func RS f_Inv_f) 1);
    3.73 -by (asm_full_simp_tac (simpset() addsimps [surj_PiBij]) 1);
    3.74 -by (assume_tac 1);
    3.75 -qed "PiBij_bij2";
     4.1 --- a/src/HOL/ex/PiSets.thy	Mon Jul 23 17:45:07 2001 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,26 +0,0 @@
     4.4 -(*  Title:      HOL/ex/PiSets.thy
     4.5 -    ID:         $Id$
     4.6 -    Author:     Florian Kammueller, University of Cambridge
     4.7 -
     4.8 -The bijection between elements of the Pi set and functional graphs
     4.9 -
    4.10 -Also the nice -> operator for function space
    4.11 -*)
    4.12 -
    4.13 -PiSets = Datatype_Universe + Finite +
    4.14 -
    4.15 -syntax
    4.16 -  "->" :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
    4.17 -
    4.18 -translations
    4.19 -  "A -> B" == "A funcset B"
    4.20 -
    4.21 -constdefs
    4.22 -(* bijection between Pi_sig and Pi_=> *)
    4.23 -  PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
    4.24 -    "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
    4.25 -
    4.26 -  Graph ::  "['a set, 'a => 'b set] => ('a * 'b) set set"
    4.27 -   "Graph A B == {f. f: Pow(Sigma A B) & (! x: A. (?! y. (x, y): f))}"
    4.28 -
    4.29 -end
     5.1 --- a/src/HOL/ex/ROOT.ML	Mon Jul 23 17:45:07 2001 +0200
     5.2 +++ b/src/HOL/ex/ROOT.ML	Mon Jul 23 17:45:35 2001 +0200
     5.3 @@ -33,10 +33,6 @@
     5.4  time_use_thy "MonoidGroup";
     5.5  time_use_thy "Records";
     5.6  
     5.7 -(*groups via locales*)
     5.8 -time_use_thy "PiSets";
     5.9 -time_use_thy "LocaleGroup";
    5.10 -
    5.11  (*advanced concrete syntax*)
    5.12  time_use_thy "Tuple";
    5.13  time_use_thy "Antiquote";