Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Generated_Rings.thy Sprache: Isabelle

Original von: Isabelle^©

(* ************************************************************************** *)
(* Title:      Generated_Rings.thy                                            *)
(* Author:     Martin Baillon                                                 *)
(* ************************************************************************** *)

theory Generated_Rings
  imports Subrings
begin

section\<open>Generated Rings\<close>

inductive_set
  generate_ring :: "('a, 'b) ring_scheme \ 'a set \ 'a set"
  for R and H where
    one:   "\\<^bsub>R\<^esub> \ generate_ring R H"
  | incl:  "h \ H \ h \ generate_ring R H"
  | a_inv: "h \ generate_ring R H \ \\<^bsub>R\<^esub> h \ generate_ring R H"
  | eng_add : "\ h1 \ generate_ring R H; h2 \ generate_ring R H \ \ h1 \\<^bsub>R\<^esub> h2 \ generate_ring R H"
  | eng_mult: "\ h1 \ generate_ring R H; h2 \ generate_ring R H \ \ h1 \\<^bsub>R\<^esub> h2 \ generate_ring R H"

subsection\<open>Basic Properties of Generated Rings - First Part\<close>

lemma (in ring) generate_ring_in_carrier:
  assumes "H \ carrier R"
  shows "h \ generate_ring R H \ h \ carrier R"
  apply (induction rule: generate_ring.induct) using assms
  by blast+

lemma (in ring) generate_ring_incl:
  assumes "H \ carrier R"
  shows "generate_ring R H \ carrier R"
  using generate_ring_in_carrier[OF assms] by auto

lemma (in ring) zero_in_generate: "\\<^bsub>R\<^esub> \ generate_ring R H"
  using one a_inv by (metis generate_ring.eng_add one_closed r_neg)

lemma (in ring) generate_ring_is_subring:
  assumes "H \ carrier R"
  shows "subring (generate_ring R H) R"
  by (auto intro!: subringI[of "generate_ring R H"]
         simp add: generate_ring_in_carrier[OF assms] one a_inv eng_mult eng_add)

lemma (in ring) generate_ring_is_ring:
  assumes "H \ carrier R"
  shows "ring (R \ carrier := generate_ring R H \)"
  using subring_iff[OF generate_ring_incl[OF assms]] generate_ring_is_subring[OF assms] by simp

lemma (in ring) generate_ring_min_subring1:
  assumes "H \ carrier R" and "subring E R" "H \ E"
  shows "generate_ring R H \ E"
proof
  fix h assume h: "h \ generate_ring R H"
  show "h \ E"
    using h and assms(3)
      by (induct rule: generate_ring.induct)
         (auto simp add: subringE(3,5-7)[OF assms(2)])
qed

lemma (in ring) generate_ringI:
  assumes "H \ carrier R"
    and "subring E R" "H \ E"
    and "\K. \ subring K R; H \ K \ \ E \ K"
  shows "E = generate_ring R H"
proof
  show "E \ generate_ring R H"
    using assms generate_ring_is_subring generate_ring.incl by (metis subset_iff)
  show "generate_ring R H \ E"
    using generate_ring_min_subring1[OF assms(1-3)] by simp
qed

lemma (in ring) generate_ringE:
  assumes "H \ carrier R" and "E = generate_ring R H"
  shows "subring E R" and "H \ E" and "\K. \ subring K R; H \ K \ \ E \ K"
proof -
  show "subring E R" using assms generate_ring_is_subring by simp
  show "H \ E" using assms(2) by (simp add: generate_ring.incl subsetI)
  show "\K. subring K R \ H \ K \ E \ K"
    using assms generate_ring_min_subring1 by auto
qed

lemma (in ring) generate_ring_min_subring2:
  assumes "H \ carrier R"
  shows "generate_ring R H = \{K. subring K R \ H \ K}"
proof
  have "subring (generate_ring R H) R \ H \ generate_ring R H"
    by (simp add: assms generate_ringE(2) generate_ring_is_subring)
  thus "\{K. subring K R \ H \ K} \ generate_ring R H" by blast
next
  have "\K. subring K R \ H \ K \ generate_ring R H \ K"
    by (simp add: assms generate_ring_min_subring1)
  thus "generate_ring R H \ \{K. subring K R \ H \ K}" by blast
qed

lemma (in ring) mono_generate_ring:
  assumes "I \ J" and "J \ carrier R"
  shows "generate_ring R I \ generate_ring R J"
proof-
  have "I \ generate_ring R J "
    using assms generate_ringE(2) by blast
  thus "generate_ring R I \ generate_ring R J"
    using generate_ring_min_subring1[of I "generate_ring R J"] assms generate_ring_is_subring[OF assms(2)]
    by blast
qed

lemma (in ring) subring_gen_incl :
  assumes "subring H R"
    and  "subring K R"
    and "I \ H"
    and "I \ K"
  shows "generate_ring (R\carrier := K\) I \ generate_ring (R\carrier := H\) I"
proof
  {fix J assume J_def : "subring J R" "I \ J"
    have "generate_ring (R \ carrier := J \) I \ J"
      using ring.mono_generate_ring[of "(R\carrier := J\)" I J ] subring_is_ring[OF J_def(1)]
          ring.generate_ring_in_carrier[of "R\carrier := J\"] ring_axioms J_def(2)
      by auto}
  note incl_HK = this
  {fix x have "x \ generate_ring (R\carrier := K\) I \ x \ generate_ring (R\carrier := H\) I"
    proof (induction  rule : generate_ring.induct)
      case one
        have "\\<^bsub>R\carrier := H\\<^esub> \ \\<^bsub>R\carrier := K\\<^esub> = \\<^bsub>R\carrier := H\\<^esub>" by simp
        moreover have "\\<^bsub>R\carrier := H\\<^esub> \ \\<^bsub>R\carrier := K\\<^esub> = \\<^bsub>R\carrier := K\\<^esub>" by simp
        ultimately show ?case using assms generate_ring.one by metis
    next
      case (incl h) thus ?case using generate_ring.incl by force
    next
      case (a_inv h)
      note hyp = this
      have "a_inv (R\carrier := K\) h = a_inv R h"
        using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] hyp
        unfolding subring_def comm_group_def a_inv_def by auto
      moreover have "a_inv (R\carrier := H\) h = a_inv R h"
        using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] hyp
        unfolding subring_def comm_group_def a_inv_def by auto
      ultimately show ?case using generate_ring.a_inv a_inv.IH by fastforce
    next
      case (eng_add h1 h2)
      thus ?case using incl_HK assms generate_ring.eng_add by force
    next
      case (eng_mult h1 h2)
      thus ?case using generate_ring.eng_mult by force
    qed}
  thus "\x. x \ generate_ring (R\carrier := K\) I \ x \ generate_ring (R\carrier := H\) I"
    by auto
qed

lemma (in ring) subring_gen_equality:
  assumes "subring H R" "K \ H"
  shows "generate_ring R K = generate_ring (R \ carrier := H \) K"
  using subring_gen_incl[OF assms(1)carrier_is_subring assms(2)] assms subringE(1)
        subring_gen_incl[OF carrier_is_subring assms(1) _ assms(2)]
  by force

end

¤ Dauer der Verarbeitung: 0.19 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.