Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Bij.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Algebra/Bij.thy
    Author:     Florian Kammueller, with new proofs by L C Paulson
*)

theory Bij
imports Group
begin

section \<open>Bijections of a Set, Permutation and Automorphism Groups\<close>

definition
  Bij :: "'a set \ ('a \ 'a) set"
    \<comment> \<open>Only extensional functions, since otherwise we get too many.\<close>
   where "Bij S = extensional S \ {f. bij_betw f S S}"

definition
  BijGroup :: "'a set \ ('a \ 'a) monoid"
  where "BijGroup S =
    \<lparr>carrier = Bij S,
     mult = \<lambda>g \<in> Bij S. \<lambda>f \<in> Bij S. compose S g f,
     one = \<lambda>x \<in> S. x\<rparr>"

declare Id_compose [simp] compose_Id [simp]

lemma Bij_imp_extensional: "f \ Bij S \ f \ extensional S"
  by (simp add: Bij_def)

lemma Bij_imp_funcset: "f \ Bij S \ f \ S \ S"
  by (auto simp add: Bij_def bij_betw_imp_funcset)

subsection \<open>Bijections Form a Group\<close>

lemma restrict_inv_into_Bij: "f \ Bij S \ (\x \ S. (inv_into S f) x) \ Bij S"
  by (simp add: Bij_def bij_betw_inv_into)

lemma id_Bij: "(\x\S. x) \ Bij S "
  by (auto simp add: Bij_def bij_betw_def inj_on_def)

lemma compose_Bij: "\x \ Bij S; y \ Bij S\ \ compose S x y \ Bij S"
  by (auto simp add: Bij_def bij_betw_compose)

lemma Bij_compose_restrict_eq:
     "f \ Bij S \ compose S (restrict (inv_into S f) S) f = (\x\S. x)"
  by (simp add: Bij_def compose_inv_into_id)

theorem group_BijGroup: "group (BijGroup S)"
  apply (simp add: BijGroup_def)
  apply (rule groupI)
      apply (auto simp: compose_Bij id_Bij Bij_imp_funcset Bij_imp_extensional compose_assoc [symmetric])
  apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij)
  done

subsection\<open>Automorphisms Form a Group\<close>

lemma Bij_inv_into_mem: "\ f \ Bij S; x \ S\ \ inv_into S f x \ S"
by (simp add: Bij_def bij_betw_def inv_into_into)

lemma Bij_inv_into_lemma:
  assumes eq: "\x y. \x \ S; y \ S\ \ h(g x y) = g (h x) (h y)"
      and hg: "h \ Bij S" "g \ S \ S \ S" and "x \ S" "y \ S"
  shows "inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)"
proof -
  have "h ` S = S"
    by (metis (no_types) Bij_def Int_iff assms(2) bij_betw_def mem_Collect_eq)
  with \<open>x \<in> S\<close> \<open>y \<in> S\<close> have "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' \<and> y = h y'"
    by auto
  then show ?thesis
    using assms
    by (auto simp add: Bij_def bij_betw_def eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem])
qed

definition
  auto :: "('a, 'b) monoid_scheme \ ('a \ 'a) set"
  where "auto G = hom G G \ Bij (carrier G)"

definition
  AutoGroup :: "('a, 'c) monoid_scheme \ ('a \ 'a) monoid"
  where "AutoGroup G = BijGroup (carrier G) \carrier := auto G\"

lemma (in group) id_in_auto: "(\x \ carrier G. x) \ auto G"
  by (simp add: auto_def hom_def restrictI group.axioms id_Bij)

lemma (in group) mult_funcset: "mult G \ carrier G \ carrier G \ carrier G"
  by (simp add:  Pi_I group.axioms)

lemma (in group) restrict_inv_into_hom:
      "\h \ hom G G; h \ Bij (carrier G)\
       \<Longrightarrow> restrict (inv_into (carrier G) h) (carrier G) \<in> hom G G"
  by (simp add: hom_def Bij_inv_into_mem restrictI mult_funcset
                group.axioms Bij_inv_into_lemma)

lemma inv_BijGroup:
     "f \ Bij S \ m_inv (BijGroup S) f = (\x \ S. (inv_into S f) x)"
apply (rule group.inv_equality [OF group_BijGroup])
apply (simp_all add:BijGroup_def restrict_inv_into_Bij Bij_compose_restrict_eq)
done

lemma (in group) subgroup_auto:
      "subgroup (auto G) (BijGroup (carrier G))"
proof (rule subgroup.intro)
  show "auto G \ carrier (BijGroup (carrier G))"
    by (force simp add: auto_def BijGroup_def)
next
  fix x y
  assume "x \ auto G" "y \ auto G"
  thus "x \\<^bsub>BijGroup (carrier G)\<^esub> y \ auto G"
    by (force simp add: BijGroup_def is_group auto_def Bij_imp_funcset
                        group.hom_compose compose_Bij)
next
  show "\\<^bsub>BijGroup (carrier G)\<^esub> \ auto G" by (simp add: BijGroup_def id_in_auto)
next
  fix x
  assume "x \ auto G"
  thus "inv\<^bsub>BijGroup (carrier G)\<^esub> x \ auto G"
    by (simp del: restrict_apply
        add: inv_BijGroup auto_def restrict_inv_into_Bij restrict_inv_into_hom)
qed

theorem (in group) AutoGroup: "group (AutoGroup G)"
by (simp add: AutoGroup_def subgroup.subgroup_is_group subgroup_auto
              group_BijGroup)

end

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.