moving Bij.thy from GroupTheory to Algebra
authorpaulson
Thu May 01 10:29:44 2003 +0200 (2003-05-01)
changeset 1394383d842ccd4aa
parent 13942 dc93e3a68142
child 13944 9b34607cd83e
moving Bij.thy from GroupTheory to Algebra
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/ROOT.ML
src/HOL/GroupTheory/Bij.thy
src/HOL/GroupTheory/ROOT.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Algebra/Coset.thy	Thu May 01 08:39:37 2003 +0200
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Thu May 01 10:29:44 2003 +0200
     1.3 @@ -491,23 +491,4 @@
     1.4  apply (auto dest: coset.setrcos_inv_mult_group_eq simp add: setinv_closed)
     1.5  done
     1.6  
     1.7 -(*????????????????
     1.8 -theorem factorgroup_is_group: "H <| G ==> group (G Mod H)"
     1.9 -apply (frule normal_imp_coset) 
    1.10 -apply (simp add: FactGroup_def) 
    1.11 -apply (rule group.intro)
    1.12 -apply (rule magma.intro) 
    1.13 -apply (simp add: ); 
    1.14 -  apply (simp add: restrictI coset.setmult_closed) 
    1.15 - apply (rule semigroup.intro) 
    1.16 -  apply (simp add: restrictI coset.setmult_closed) 
    1.17 - apply (simp add: coset.setmult_closed coset.setrcos_assoc)  
    1.18 -apply (rule group_axioms.intro) 
    1.19 -   apply (simp add: restrictI setinv_closed) 
    1.20 -  apply (simp add: normal_imp_subgroup subgroup_in_rcosets) 
    1.21 - apply (simp add: setinv_closed coset.setrcos_inv_mult_group_eq) 
    1.22 -apply (simp add: normal_imp_subgroup subgroup_in_rcosets coset.setrcos_mult_eq)
    1.23 -done
    1.24 -*)
    1.25 -
    1.26  end
     2.1 --- a/src/HOL/Algebra/Group.thy	Thu May 01 08:39:37 2003 +0200
     2.2 +++ b/src/HOL/Algebra/Group.thy	Thu May 01 10:29:44 2003 +0200
     2.3 @@ -99,29 +99,23 @@
     2.4  
     2.5  lemma (in monoid) Units_inv_closed [intro, simp]:
     2.6    "x \<in> Units G ==> inv x \<in> carrier G"
     2.7 -  apply (unfold Units_def m_inv_def)
     2.8 -  apply auto
     2.9 +  apply (unfold Units_def m_inv_def, auto)
    2.10    apply (rule theI2, fast)
    2.11 -   apply (fast intro: inv_unique)
    2.12 -  apply fast
    2.13 +   apply (fast intro: inv_unique, fast)
    2.14    done
    2.15  
    2.16  lemma (in monoid) Units_l_inv:
    2.17    "x \<in> Units G ==> inv x \<otimes> x = \<one>"
    2.18 -  apply (unfold Units_def m_inv_def)
    2.19 -  apply auto
    2.20 +  apply (unfold Units_def m_inv_def, auto)
    2.21    apply (rule theI2, fast)
    2.22 -   apply (fast intro: inv_unique)
    2.23 -  apply fast
    2.24 +   apply (fast intro: inv_unique, fast)
    2.25    done
    2.26  
    2.27  lemma (in monoid) Units_r_inv:
    2.28    "x \<in> Units G ==> x \<otimes> inv x = \<one>"
    2.29 -  apply (unfold Units_def m_inv_def)
    2.30 -  apply auto
    2.31 +  apply (unfold Units_def m_inv_def, auto)
    2.32    apply (rule theI2, fast)
    2.33 -   apply (fast intro: inv_unique)
    2.34 -  apply fast
    2.35 +   apply (fast intro: inv_unique, fast)
    2.36    done
    2.37  
    2.38  lemma (in monoid) Units_inv_Units [intro, simp]:
    2.39 @@ -354,6 +348,14 @@
    2.40    "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
    2.41    by (rule Units_inv_comm) auto                          
    2.42  
    2.43 +lemma (in group) m_inv_equality:
    2.44 +     "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
    2.45 +apply (simp add: m_inv_def)
    2.46 +apply (rule the_equality)
    2.47 + apply (simp add: inv_comm [of y x]) 
    2.48 +apply (rule r_cancel [THEN iffD1], auto) 
    2.49 +done
    2.50 +
    2.51  text {* Power *}
    2.52  
    2.53  lemma (in group) int_pow_def2:
    2.54 @@ -594,6 +596,15 @@
    2.55    "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
    2.56    by (auto simp add: hom_def funcset_mem)
    2.57  
    2.58 +lemma compose_hom:
    2.59 +     "[|group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G -> carrier G|]
    2.60 +      ==> compose (carrier G) h h' \<in> hom G G"
    2.61 +apply (simp (no_asm_simp) add: hom_def)
    2.62 +apply (intro conjI) 
    2.63 + apply (force simp add: funcset_compose hom_def)
    2.64 +apply (simp add: compose_def group.axioms hom_mult funcset_mem) 
    2.65 +done
    2.66 +
    2.67  locale group_hom = group G + group H + var h +
    2.68    assumes homh: "h \<in> hom G H"
    2.69    notes hom_mult [simp] = hom_mult [OF homh]
     3.1 --- a/src/HOL/Algebra/ROOT.ML	Thu May 01 08:39:37 2003 +0200
     3.2 +++ b/src/HOL/Algebra/ROOT.ML	Thu May 01 10:29:44 2003 +0200
     3.3 @@ -8,6 +8,7 @@
     3.4  
     3.5  no_document use_thy "FuncSet";
     3.6  use_thy "Sylow";		(* Groups *)
     3.7 +use_thy "Bij";			(* Automorphism Groups *)
     3.8  use_thy "UnivPoly";		(* Rings and polynomials *)
     3.9  
    3.10  (* Old development, based on axiomatic type classes.
     4.1 --- a/src/HOL/GroupTheory/Bij.thy	Thu May 01 08:39:37 2003 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,131 +0,0 @@
     4.4 -(*  Title:      HOL/GroupTheory/Bij
     4.5 -    ID:         $Id$
     4.6 -    Author:     Florian Kammueller, with new proofs by L C Paulson
     4.7 -*)
     4.8 -
     4.9 -
    4.10 -header{*Bijections of a Set, Permutation Groups, Automorphism Groups*} 
    4.11 -
    4.12 -theory Bij = Group:
    4.13 -
    4.14 -constdefs
    4.15 -  Bij :: "'a set => (('a => 'a)set)" 
    4.16 -    --{*Only extensional functions, since otherwise we get too many.*}
    4.17 -    "Bij S == extensional S \<inter> {f. f`S = S & inj_on f S}"
    4.18 -
    4.19 -   BijGroup ::  "'a set => (('a => 'a) group)"
    4.20 -   "BijGroup S == (| carrier = Bij S, 
    4.21 -		     sum  = %g: Bij S. %f: Bij S. compose S g f,
    4.22 -		     gminus = %f: Bij S. %x: S. (Inv S f) x, 
    4.23 -		     zero = %x: S. x |)"
    4.24 -
    4.25 -
    4.26 -declare Id_compose [simp] compose_Id [simp]
    4.27 -
    4.28 -lemma Bij_imp_extensional: "f \<in> Bij S ==> f \<in> extensional S"
    4.29 -by (simp add: Bij_def)
    4.30 -
    4.31 -lemma Bij_imp_funcset: "f \<in> Bij S ==> f \<in> S -> S"
    4.32 -by (auto simp add: Bij_def Pi_def)
    4.33 -
    4.34 -lemma Bij_imp_apply: "f \<in> Bij S ==> f ` S = S"
    4.35 -by (simp add: Bij_def)
    4.36 -
    4.37 -lemma Bij_imp_inj_on: "f \<in> Bij S ==> inj_on f S"
    4.38 -by (simp add: Bij_def)
    4.39 -
    4.40 -lemma BijI: "[| f \<in> extensional(S); f`S = S; inj_on f S |] ==> f \<in> Bij S"
    4.41 -by (simp add: Bij_def)
    4.42 -
    4.43 -
    4.44 -subsection{*Bijections Form a Group*}
    4.45 -
    4.46 -lemma restrict_Inv_Bij: "f \<in> Bij S ==> (%x:S. (Inv S f) x) \<in> Bij S"
    4.47 -apply (simp add: Bij_def)
    4.48 -apply (intro conjI)
    4.49 -txt{*Proving @{term "restrict (Inv S f) S ` S = S"}*}
    4.50 - apply (rule equalityI)
    4.51 -  apply (force simp add: Inv_mem) --{*first inclusion*}
    4.52 - apply (rule subsetI)   --{*second inclusion*}
    4.53 - apply (rule_tac x = "f x" in image_eqI)
    4.54 -  apply (force intro:  simp add: Inv_f_f)
    4.55 - apply blast
    4.56 -txt{*Remaining goal: @{term "inj_on (restrict (Inv S f) S) S"}*}
    4.57 -apply (rule inj_onI)
    4.58 -apply (auto elim: Inv_injective)
    4.59 -done
    4.60 -
    4.61 -lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S "
    4.62 -apply (rule BijI)
    4.63 -apply (auto simp add: inj_on_def)
    4.64 -done
    4.65 -
    4.66 -lemma compose_Bij: "[| x \<in> Bij S; y \<in> Bij S|] ==> compose S x y \<in> Bij S"
    4.67 -apply (rule BijI)
    4.68 -  apply (simp add: compose_extensional) 
    4.69 - apply (blast del: equalityI
    4.70 -              intro: surj_compose dest: Bij_imp_apply Bij_imp_inj_on)
    4.71 -apply (blast intro: inj_on_compose dest: Bij_imp_apply Bij_imp_inj_on)
    4.72 -done
    4.73 -
    4.74 -theorem group_BijGroup: "group (BijGroup S)"
    4.75 -apply (simp add: group_def semigroup_def group_axioms_def 
    4.76 -                 BijGroup_def restrictI compose_Bij restrict_Inv_Bij id_Bij)
    4.77 -apply (auto intro!: compose_Bij) 
    4.78 -  apply (blast intro: compose_assoc [symmetric] Bij_imp_funcset)
    4.79 - apply (simp add: Bij_def compose_Inv_id) 
    4.80 -apply (simp add: Id_compose Bij_imp_funcset Bij_imp_extensional) 
    4.81 -done
    4.82 -
    4.83 -
    4.84 -subsection{*Automorphisms Form a Group*}
    4.85 -
    4.86 -lemma Bij_Inv_mem: "[|  f \<in> Bij S;  x : S |] ==> Inv S f x : S"
    4.87 -by (simp add: Bij_def Inv_mem) 
    4.88 -
    4.89 -lemma Bij_Inv_lemma:
    4.90 - assumes eq: "!!x y. [|x \<in> S; y \<in> S|] ==> h(g x y) = g (h x) (h y)"
    4.91 - shows "[| h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S |]        
    4.92 -        ==> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
    4.93 -apply (simp add: Bij_def) 
    4.94 -apply (subgoal_tac "EX x':S. EX y':S. x = h x' & y = h y'")
    4.95 - apply clarify
    4.96 - apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast) 
    4.97 -done
    4.98 -
    4.99 -constdefs
   4.100 - auto :: "('a,'b)group_scheme => ('a => 'a)set"
   4.101 -  "auto G == hom G G Int Bij (carrier G)"
   4.102 -
   4.103 -  AutoGroup :: "[('a,'c) group_scheme] => ('a=>'a) group"
   4.104 -  "AutoGroup G == BijGroup (carrier G) (|carrier := auto G |)"
   4.105 -
   4.106 -lemma id_in_auto: "group G ==> (%x: carrier G. x) \<in> auto G"
   4.107 -by (simp add: auto_def hom_def restrictI semigroup.sum_closed 
   4.108 -              group.axioms id_Bij) 
   4.109 -
   4.110 -lemma restrict_Inv_hom:
   4.111 -      "[|group G; h \<in> hom G G; h \<in> Bij (carrier G)|]
   4.112 -       ==> restrict (Inv (carrier G) h) (carrier G) \<in> hom G G"
   4.113 -by (simp add: hom_def Bij_Inv_mem restrictI semigroup.sum_closed 
   4.114 -              semigroup.sum_funcset group.axioms Bij_Inv_lemma)
   4.115 -
   4.116 -lemma subgroup_auto:
   4.117 -      "group G ==> subgroup (auto G) (BijGroup (carrier G))"
   4.118 -apply (rule group.subgroupI) 
   4.119 -    apply (rule group_BijGroup) 
   4.120 -   apply (force simp add: auto_def BijGroup_def) 
   4.121 -  apply (blast intro: dest: id_in_auto) 
   4.122 - apply (simp add: auto_def BijGroup_def restrict_Inv_Bij
   4.123 -                  restrict_Inv_hom) 
   4.124 -apply (simp add: auto_def BijGroup_def compose_Bij)
   4.125 -apply (simp add: hom_def compose_def Pi_def group.axioms)
   4.126 -done
   4.127 -
   4.128 -theorem AutoGroup: "group G ==> group (AutoGroup G)"
   4.129 -apply (drule subgroup_auto) 
   4.130 -apply (simp add: subgroup_def AutoGroup_def) 
   4.131 -done
   4.132 -
   4.133 -end
   4.134 -
     5.1 --- a/src/HOL/GroupTheory/ROOT.ML	Thu May 01 08:39:37 2003 +0200
     5.2 +++ b/src/HOL/GroupTheory/ROOT.ML	Thu May 01 10:29:44 2003 +0200
     5.3 @@ -1,3 +1,3 @@
     5.4  no_document use_thy "FuncSet";
     5.5  
     5.6 -use_thy "Bij";
     5.7 +use_thy "Group";
     6.1 --- a/src/HOL/IsaMakefile	Thu May 01 08:39:37 2003 +0200
     6.2 +++ b/src/HOL/IsaMakefile	Thu May 01 10:29:44 2003 +0200
     6.3 @@ -284,7 +284,6 @@
     6.4  
     6.5  $(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
     6.6    Library/Primes.thy Library/FuncSet.thy \
     6.7 -  GroupTheory/Bij.thy \
     6.8    GroupTheory/Group.thy \
     6.9    GroupTheory/ROOT.ML \
    6.10    GroupTheory/document/root.tex
    6.11 @@ -341,6 +340,7 @@
    6.12  HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
    6.13  
    6.14  $(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \
    6.15 +  Algebra/Bij.thy \
    6.16    Algebra/CRing.thy \
    6.17    Algebra/Coset.thy \
    6.18    Algebra/Exponent.thy \