Quelle Generated_Fields.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/Generated_Fields.thy
    Author:     Martin Baillon
*)

theory Generated_Fields
imports Generated_Rings Subrings Multiplicative_Group
begin

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

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

lemma (in field) generate_field_in_carrier:
  assumes "H \ carrier R"
  shows "h \ generate_field R H \ h \ carrier R"
  apply (induction rule: generate_field.induct)
  using assms field_Units
  by blast+

lemma (in field) generate_field_incl:
  assumes "H \ carrier R"
  shows "generate_field R H \ carrier R"
  using generate_field_in_carrier[OF assms] by auto

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

lemma (in field) generate_field_is_subfield:
  assumes "H \ carrier R"
  shows "subfield (generate_field R H) R"
proof (intro subfieldI', simp_all add: m_inv)
  show "subring (generate_field R H) R"
    by (auto intro: subringI[of "generate_field R H"]
             simp add: eng_add a_inv eng_mult one generate_field_in_carrier[OF assms])
qed

lemma (in field) generate_field_is_add_subgroup:
  assumes "H \ carrier R"
  shows "subgroup (generate_field R H) (add_monoid R)"
  using subring.axioms(1)[OF subfieldE(1)[OF generate_field_is_subfield[OF assms]]] .

lemma (in field) generate_field_is_field :
  assumes "H \ carrier R"
  shows "field (R \ carrier := generate_field R H \)"
  using subfield_iff generate_field_is_subfield assms by simp

lemma (in field) generate_field_min_subfield1:
  assumes "H \ carrier R"
    and "subfield E R" "H \ E"
  shows "generate_field R H \ E"
proof
  fix h
  assume h: "h \ generate_field R H"
  show "h \ E"
    using h and assms(3) and subfield_m_inv[OF assms(2)]
    by (induct rule: generate_field.induct)
       (auto simp add: subringE(3,5-7)[OF subfieldE(1)[OF assms(2)]])
qed

lemma (in field) generate_fieldI:
  assumes "H \ carrier R"
    and "subfield E R" "H \ E"
    and "\K. \ subfield K R; H \ K \ \ E \ K"
  shows "E = generate_field R H"
proof
  show "E \ generate_field R H"
    using assms generate_field_is_subfield generate_field.incl by (metis subset_iff)
  show "generate_field R H \ E"
    using generate_field_min_subfield1[OF assms(1-3)] by simp
qed

lemma (in field) generate_fieldE:
  assumes "H \ carrier R" and "E = generate_field R H"
  shows "subfield E R" and "H \ E" and "\K. \ subfield K R; H \ K \ \ E \ K"
proof -
  show "subfield E R" using assms generate_field_is_subfield by simp
  show "H \ E" using assms(2) by (simp add: generate_field.incl subsetI)
  show "\K. subfield K R \ H \ K \ E \ K"
    using assms generate_field_min_subfield1 by auto
qed

lemma (in field) generate_field_min_subfield2:
  assumes "H \ carrier R"
  shows "generate_field R H = \{K. subfield K R \ H \ K}"
proof
  have "subfield (generate_field R H) R \ H \ generate_field R H"
    by (simp add: assms generate_fieldE(2) generate_field_is_subfield)
  thus "\{K. subfield K R \ H \ K} \ generate_field R H" by blast
next
  have "\K. subfield K R \ H \ K \ generate_field R H \ K"
    by (simp add: assms generate_field_min_subfield1)
  thus "generate_field R H \ \{K. subfield K R \ H \ K}" by blast
qed

lemma (in field) mono_generate_field:
  assumes "I \ J" and "J \ carrier R"
  shows "generate_field R I \ generate_field R J"
proof-
  have "I \ generate_field R J "
    using assms generate_fieldE(2) by blast
  thus "generate_field R I \ generate_field R J"
    using generate_field_min_subfield1[of I "generate_field R J"] assms generate_field_is_subfield[OF assms(2)]
    by blast
qed

lemma (in field) subfield_gen_incl :
  assumes "subfield H R"
    and  "subfield K R"
    and "I \ H"
    and "I \ K"
  shows "generate_field (R\carrier := K\) I \ generate_field (R\carrier := H\) I"
proof
  have incl_HK: "generate_field (R \ carrier := J \) I \ J"
    if J_def : "subfield J R" "I \ J" for J
    using field.mono_generate_field[of "(R\carrier := J\)" I J] subfield_iff(2)[OF J_def(1)]
      field.generate_field_in_carrier[of "R\carrier := J\"] field_axioms J_def
    by auto

  fix x
  have "x \ generate_field (R\carrier := K\) I \ x \ generate_field (R\carrier := H\) I"
  proof (induction  rule : generate_field.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_field.one by metis
  next
    case (incl h)
    thus ?case using generate_field.incl by force
  next
    case (a_inv h)
    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] a_inv
        subring.axioms(1)[OF subfieldE(1)[OF assms(2)]]
      unfolding 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] a_inv
        subring.axioms(1)[OF subfieldE(1)[OF assms(1)]]
      unfolding  comm_group_def a_inv_def by auto
    ultimately show ?case using generate_field.a_inv a_inv.IH by fastforce
  next
    case (m_inv h)
    have h_K : "h \ (K - {\})" using incl_HK[OF assms(2) assms(4)] m_inv by auto
    hence "m_inv (R\carrier := K\) h = m_inv R h"
      using  field.m_inv_mult_of[OF subfield_iff(2)[OF assms(2)]]
        group.m_inv_consistent[of "mult_of R" "K - {\}"] field_mult_group units_of_inv
        subgroup_mult_of subfieldE[OF assms(2)] unfolding mult_of_def apply simp
      by (metis h_K mult_of_def mult_of_is_Units subgroup.mem_carrier units_of_carrier assms(2))
    moreover have h_H : "h \ (H - {\})" using incl_HK[OF assms(1) assms(3)] m_inv by auto
    hence "m_inv (R\carrier := H\) h = m_inv R h"
      using  field.m_inv_mult_of[OF subfield_iff(2)[OF assms(1)]]
        group.m_inv_consistent[of "mult_of R" "H - {\}"] field_mult_group
        subgroup_mult_of[OF assms(1)]  unfolding mult_of_def apply simp
      by (metis h_H field_Units m_inv_mult_of mult_of_is_Units subgroup.mem_carrier units_of_def)
    ultimately show ?case using generate_field.m_inv m_inv.IH h_H by fastforce
  next
    case (eng_add h1 h2)
    thus ?case using incl_HK assms generate_field.eng_add by force
  next
    case (eng_mult h1 h2)
    thus ?case using generate_field.eng_mult by force
  qed
  thus "x \ generate_field (R\carrier := K\) I \ x \ generate_field (R\carrier := H\) I"
    by auto
qed

lemma (in field) subfield_gen_equality:
  assumes "subfield H R" "K \ H"
  shows "generate_field R K = generate_field (R \ carrier := H \) K"
  using subfield_gen_incl[OF assms(1) carrier_is_subfield assms(2)] assms subringE(1)
        subfield_gen_incl[OF carrier_is_subfield assms(1) _ assms(2)] subfieldE(1)[OF assms(1)]
  by force

end

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.