src/HOL/Algebra/Ideal_Product.thy
author wenzelm
Mon, 13 Apr 2020 22:08:14 +0200
changeset 71751 abf3e80bd815
parent 68606 96a49db47c97
child 75963 884dbbc8e1b3
permissions -rw-r--r--
tuned NEWS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68582
b9b9e2985878 more standard headers;
wenzelm
parents: 68569
diff changeset
     1
(*  Title:      HOL/Algebra/Ideal_Product.thy
b9b9e2985878 more standard headers;
wenzelm
parents: 68569
diff changeset
     2
    Author:     Paulo Emílio de Vilhena
b9b9e2985878 more standard headers;
wenzelm
parents: 68569
diff changeset
     3
*)
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     4
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     5
theory Ideal_Product
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     6
  imports Ideal
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     7
begin
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     8
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     9
section \<open>Product of Ideals\<close>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    10
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    11
text \<open>In this section, we study the structure of the set of ideals of a given ring.\<close>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    12
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    13
inductive_set
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    14
  ideal_prod :: "[ ('a, 'b) ring_scheme, 'a set, 'a set ] \<Rightarrow> 'a set" (infixl "\<cdot>\<index>" 80)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    15
  for R and I and J (* both I and J are supposed ideals *) where
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    16
    prod: "\<lbrakk> i \<in> I; j \<in> J \<rbrakk> \<Longrightarrow> i \<otimes>\<^bsub>R\<^esub> j \<in> ideal_prod R I J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    17
  |  sum: "\<lbrakk> s1 \<in> ideal_prod R I J; s2 \<in> ideal_prod R I J \<rbrakk> \<Longrightarrow> s1 \<oplus>\<^bsub>R\<^esub> s2 \<in> ideal_prod R I J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    18
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    19
definition ideals_set :: "('a, 'b) ring_scheme \<Rightarrow> ('a set) ring"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    20
  where "ideals_set R = \<lparr> carrier = { I. ideal I R },
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    21
                             mult = ideal_prod R,
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    22
                              one = carrier R,
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    23
                             zero = { \<zero>\<^bsub>R\<^esub> },
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    24
                              add = set_add R \<rparr>"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    25
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    26
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    27
subsection \<open>Basic Properties\<close>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    28
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    29
lemma (in ring) ideal_prod_in_carrier:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    30
  assumes "ideal I R" "ideal J R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    31
  shows "I \<cdot> J \<subseteq> carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    32
proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    33
  fix s assume "s \<in> I \<cdot> J" thus "s \<in> carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    34
    by (induct s rule: ideal_prod.induct) (auto, meson assms ideal.I_l_closed ideal.Icarr) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    35
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    36
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    37
lemma (in ring) ideal_prod_inter:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    38
  assumes "ideal I R" "ideal J R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    39
  shows "I \<cdot> J \<subseteq> I \<inter> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    40
proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    41
  fix s assume "s \<in> I \<cdot> J" thus "s \<in> I \<inter> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    42
    apply (induct s rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    43
    apply (auto, (meson assms ideal.I_r_closed ideal.I_l_closed ideal.Icarr)+)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    44
    apply (simp_all add: additive_subgroup.a_closed assms ideal.axioms(1))
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    45
    done
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    46
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    47
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    48
lemma (in ring) ideal_prod_is_ideal:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    49
  assumes "ideal I R" "ideal J R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    50
  shows "ideal (I \<cdot> J) R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    51
proof (rule idealI)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    52
  show "ring R" using is_ring .
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    53
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    54
  show "subgroup (I \<cdot> J) (add_monoid R)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    55
    unfolding subgroup_def
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    56
  proof (auto)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    57
    show "\<zero> \<in> I \<cdot> J" using ideal_prod.prod[of \<zero> I \<zero> J R]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    58
      by (simp add: additive_subgroup.zero_closed assms ideal.axioms(1))
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    59
  next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    60
    fix s1 s2 assume s1: "s1 \<in> I \<cdot> J" and s2: "s2 \<in> I \<cdot> J"
68605
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    61
    have IJcarr: "\<And>a. a \<in> I \<cdot> J \<Longrightarrow> a \<in> carrier R"
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    62
      by (meson assms subsetD ideal_prod_in_carrier)
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    63
    show "s1 \<in> carrier R" using ideal_prod_in_carrier[OF assms] s1 by blast
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    64
    show "s1 \<oplus> s2 \<in> I \<cdot> J" by (simp add: ideal_prod.sum[OF s1 s2])
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    65
    show "inv\<^bsub>add_monoid R\<^esub> s1 \<in> I \<cdot> J" using s1
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    66
    proof (induct s1 rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    67
      case (prod i j)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    68
      hence "inv\<^bsub>add_monoid R\<^esub> (i \<otimes> j) = (inv\<^bsub>add_monoid R\<^esub> i) \<otimes> j"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    69
        by (metis a_inv_def assms(1) assms(2) ideal.Icarr l_minus)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    70
      thus ?case using ideal_prod.prod[of "inv\<^bsub>add_monoid R\<^esub> i" I j J R] assms
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    71
        by (simp add: additive_subgroup.a_subgroup ideal.axioms(1) prod.hyps subgroup.m_inv_closed)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    72
    next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    73
      case (sum s1 s2) thus ?case
68605
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    74
        by (metis (no_types) IJcarr a_inv_def add.inv_mult_group ideal_prod.sum sum.hyps)
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    75
    qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    76
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    77
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    78
  fix s x assume s: "s \<in> I \<cdot> J" and x: "x \<in> carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    79
  show "x \<otimes> s \<in> I \<cdot> J" using s
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    80
  proof (induct s rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    81
    case (prod i j) thus ?case using ideal_prod.prod[of "x \<otimes> i" I j J R] assms
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    82
      by (simp add: x ideal.I_l_closed ideal.Icarr m_assoc)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    83
  next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    84
    case (sum s1 s2) thus ?case
68605
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    85
    proof -
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    86
      have IJ: "I \<cdot> J \<subseteq> carrier R"
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    87
        by (metis (no_types) assms(1) assms(2) ideal.axioms(2) ring.ideal_prod_in_carrier)
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    88
      then have "s2 \<in> carrier R"
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    89
        using sum.hyps(3) by blast
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    90
      moreover have "s1 \<in> carrier R"
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    91
        using IJ sum.hyps(1) by blast
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    92
      ultimately show ?thesis
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    93
        by (simp add: ideal_prod.sum r_distr sum.hyps x)
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
    94
    qed
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    95
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    96
  show "s \<otimes> x \<in> I \<cdot> J" using s
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    97
  proof (induct s rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    98
    case (prod i j) thus ?case using ideal_prod.prod[of i I "j \<otimes> x" J R] assms x
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    99
      by (simp add: x ideal.I_r_closed ideal.Icarr m_assoc)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   100
  next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   101
    case (sum s1 s2) thus ?case 
68605
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   102
    proof -
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   103
      have "s1 \<in> carrier R" "s2 \<in> carrier R"
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   104
        by (meson assms subsetD ideal_prod_in_carrier sum.hyps)+
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   105
      then show ?thesis
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   106
        by (metis ideal_prod.sum l_distr sum.hyps(2) sum.hyps(4) x)
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   107
    qed
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   108
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   109
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   110
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   111
lemma (in ring) ideal_prod_eq_genideal:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   112
  assumes "ideal I R" "ideal J R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   113
  shows "I \<cdot> J = Idl (I <#> J)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   114
proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   115
  have "I <#> J \<subseteq> I \<cdot> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   116
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   117
    fix s assume "s \<in> I <#> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   118
    then obtain i j where "i \<in> I" "j \<in> J" "s = i \<otimes> j"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   119
      unfolding set_mult_def by blast
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   120
    thus "s \<in> I \<cdot> J" using ideal_prod.prod by simp
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   121
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   122
  thus "Idl (I <#> J) \<subseteq> I \<cdot> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   123
    unfolding genideal_def using ideal_prod_is_ideal[OF assms] by blast
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   124
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   125
  show "I \<cdot> J \<subseteq> Idl (I <#> J)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   126
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   127
    fix s assume "s \<in> I \<cdot> J" thus "s \<in> Idl (I <#> J)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   128
    proof (induct s rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   129
      case (prod i j) hence "i \<otimes> j \<in> I <#> J" unfolding set_mult_def by blast
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   130
      thus ?case unfolding genideal_def by blast 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   131
    next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   132
      case (sum s1 s2) thus ?case
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   133
        by (simp add: additive_subgroup.a_closed additive_subgroup.a_subset
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   134
            assms genideal_ideal ideal.axioms(1) set_mult_closed)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   135
    qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   136
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   137
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   138
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   139
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   140
lemma (in ring) ideal_prod_simp:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   141
  assumes "ideal I R" "ideal J R" (* the second assumption could be suppressed *)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   142
  shows "I = I <+> (I \<cdot> J)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   143
proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   144
  show "I \<subseteq> I <+> I \<cdot> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   145
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   146
    fix i assume "i \<in> I" hence "i \<oplus> \<zero> \<in> I <+> I \<cdot> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   147
      using set_add_def'[of R I "I \<cdot> J"] ideal_prod_is_ideal[OF assms]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   148
            additive_subgroup.zero_closed[OF ideal.axioms(1), of "I \<cdot> J" R] by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   149
    thus "i \<in> I <+> I \<cdot> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   150
      using \<open>i \<in> I\<close> assms(1) ideal.Icarr by fastforce 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   151
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   152
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   153
  show "I <+> I \<cdot> J \<subseteq> I"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   154
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   155
    fix s assume "s \<in> I <+> I \<cdot> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   156
    then obtain i ij where "i \<in> I" "ij \<in> I \<cdot> J" "s = i \<oplus> ij"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   157
      using set_add_def'[of R I "I \<cdot> J"] by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   158
    thus "s \<in> I"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   159
      using ideal_prod_inter[OF assms]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   160
      by (meson additive_subgroup.a_closed assms(1) ideal.axioms(1) inf_sup_ord(1) subsetCE) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   161
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   162
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   163
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   164
lemma (in ring) ideal_prod_one:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   165
  assumes "ideal I R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   166
  shows "I \<cdot> (carrier R) = I"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   167
proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   168
  show "I \<cdot> (carrier R) \<subseteq> I"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   169
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   170
    fix s assume "s \<in> I \<cdot> (carrier R)" thus "s \<in> I"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   171
      by (induct s rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   172
         (simp_all add: assms ideal.I_r_closed additive_subgroup.a_closed ideal.axioms(1))
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   173
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   174
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   175
  show "I \<subseteq> I \<cdot> (carrier R)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   176
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   177
    fix i assume "i \<in> I" thus "i \<in>  I \<cdot> (carrier R)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   178
      by (metis assms ideal.Icarr ideal_prod.simps one_closed r_one)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   179
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   180
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   181
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   182
lemma (in ring) ideal_prod_zero:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   183
  assumes "ideal I R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   184
  shows "I \<cdot> { \<zero> } = { \<zero> }"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   185
proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   186
  show "I \<cdot> { \<zero> } \<subseteq> { \<zero> }"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   187
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   188
    fix s assume "s \<in> I \<cdot> {\<zero>}" thus "s \<in> { \<zero> }"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   189
      using assms ideal.Icarr by (induct s rule: ideal_prod.induct) (fastforce, simp)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   190
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   191
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   192
  show "{ \<zero> } \<subseteq> I \<cdot> { \<zero> }"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   193
    by (simp add: additive_subgroup.zero_closed assms
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   194
                  ideal.axioms(1) ideal_prod_is_ideal zeroideal)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   195
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   196
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   197
lemma (in ring) ideal_prod_assoc:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   198
  assumes "ideal I R" "ideal J R" "ideal K R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   199
  shows "(I \<cdot> J) \<cdot> K = I \<cdot> (J \<cdot> K)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   200
proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   201
  show "(I \<cdot> J) \<cdot> K \<subseteq> I \<cdot> (J \<cdot> K)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   202
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   203
    fix s assume "s \<in> (I \<cdot> J) \<cdot> K" thus "s \<in> I \<cdot> (J \<cdot> K)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   204
    proof (induct s rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   205
      case (sum s1 s2) thus ?case
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   206
        by (simp add: ideal_prod.sum)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   207
    next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   208
      case (prod i k) thus ?case
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   209
      proof (induct i rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   210
        case (prod i j) thus ?case
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   211
          using ideal_prod.prod[OF prod(1) ideal_prod.prod[OF prod(2-3),of R], of R]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   212
          by (metis assms ideal.Icarr m_assoc) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   213
      next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   214
        case (sum s1 s2) thus ?case
68605
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   215
        proof -
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   216
          have "s1 \<in> carrier R" "s2 \<in> carrier R"
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   217
            by (meson assms subsetD ideal.axioms(2) ring.ideal_prod_in_carrier sum.hyps)+
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   218
          moreover have "k \<in> carrier R"
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   219
            by (meson additive_subgroup.a_Hcarr assms(3) ideal.axioms(1) sum.prems)
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   220
          ultimately show ?thesis
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   221
            by (metis ideal_prod.sum l_distr sum.hyps(2) sum.hyps(4) sum.prems)
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   222
        qed
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   223
      qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   224
    qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   225
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   226
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   227
  show "I \<cdot> (J \<cdot> K) \<subseteq> (I \<cdot> J) \<cdot> K"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   228
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   229
    fix s assume "s \<in> I \<cdot> (J \<cdot> K)" thus "s \<in> (I \<cdot> J) \<cdot> K"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   230
    proof (induct s rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   231
      case (sum s1 s2) thus ?case by (simp add: ideal_prod.sum)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   232
    next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   233
      case (prod i j) show ?case using prod(2) prod(1)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   234
      proof (induct j rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   235
        case (prod j k) thus ?case
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   236
          using ideal_prod.prod[OF ideal_prod.prod[OF prod(3) prod(1), of R] prod (2), of R]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   237
          by (metis assms ideal.Icarr m_assoc)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   238
      next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   239
        case (sum s1 s2) thus ?case
68605
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   240
        proof -
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   241
          have "\<And>a A B. \<lbrakk>a \<in> B \<cdot> A; ideal A R; ideal B R\<rbrakk> \<Longrightarrow> a \<in> carrier R"
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   242
            by (meson subsetD ideal_prod_in_carrier)
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   243
          moreover have "i \<in> carrier R"
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   244
            by (meson additive_subgroup.a_Hcarr assms(1) ideal.axioms(1) sum.prems)
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   245
          ultimately show ?thesis
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   246
            by (metis (no_types) assms(2) assms(3) ideal_prod.sum r_distr sum)
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   247
        qed
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   248
      qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   249
    qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   250
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   251
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   252
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   253
lemma (in ring) ideal_prod_r_distr:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   254
  assumes "ideal I R" "ideal J R" "ideal K R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   255
  shows "I \<cdot> (J <+> K) = (I \<cdot> J) <+>  (I \<cdot> K)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   256
proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   257
  show "I \<cdot> (J <+> K) \<subseteq> I \<cdot> J <+> I \<cdot> K"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   258
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   259
    fix s assume "s \<in> I \<cdot> (J <+> K)" thus "s \<in> I \<cdot> J <+> I \<cdot> K"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   260
    proof(induct s rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   261
      case (prod i jk)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   262
      then obtain j k where j: "j \<in> J" and k: "k \<in> K" and jk: "jk = j \<oplus> k"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   263
        using set_add_def'[of R J K] by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   264
      hence "i \<otimes> j \<oplus> i \<otimes> k \<in> I \<cdot> J <+> I \<cdot> K"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   265
        using ideal_prod.prod[OF prod(1) j,of R]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   266
              ideal_prod.prod[OF prod(1) k,of R]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   267
              set_add_def'[of R "I \<cdot> J" "I \<cdot> K"] by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   268
      thus ?case
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   269
        using assms ideal.Icarr r_distr jk j k prod(1) by metis 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   270
    next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   271
      case (sum s1 s2) thus ?case
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   272
        by (simp add: add_ideals additive_subgroup.a_closed assms ideal.axioms(1)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   273
                      local.ring_axioms ring.ideal_prod_is_ideal) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   274
    qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   275
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   276
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   277
  { fix s J K assume A: "ideal J R" "ideal K R" "s \<in> I \<cdot> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   278
    have "s \<in> I \<cdot> (J <+> K) \<and> s \<in> I \<cdot> (K <+> J)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   279
    proof -
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   280
      from \<open>s \<in> I \<cdot> J\<close> have "s \<in> I \<cdot> (J <+> K)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   281
      proof (induct s rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   282
        case (prod i j)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   283
        hence "(j \<oplus> \<zero>) \<in> J <+> K"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   284
          using set_add_def'[of R J K]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   285
                additive_subgroup.zero_closed[OF ideal.axioms(1), of K R] A(2) by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   286
        thus ?case
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   287
          by (metis A(1) additive_subgroup.a_Hcarr ideal.axioms(1) ideal_prod.prod prod r_zero)  
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   288
      next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   289
        case (sum s1 s2) thus ?case
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   290
          by (simp add: ideal_prod.sum) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   291
      qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   292
      thus ?thesis
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   293
        by (metis A(1) A(2) ideal_def ring.union_genideal sup_commute) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   294
    qed } note aux_lemma = this
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   295
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   296
  show "I \<cdot> J <+> I \<cdot> K \<subseteq> I \<cdot> (J <+> K)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   297
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   298
    fix s assume "s \<in> I \<cdot> J <+> I \<cdot> K"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   299
    then obtain s1 s2 where s1: "s1 \<in> I \<cdot> J" and s2: "s2 \<in> I \<cdot> K" and  s: "s = s1 \<oplus> s2"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   300
      using set_add_def'[of R "I \<cdot> J" "I \<cdot> K"] by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   301
    thus "s \<in> I \<cdot> (J <+> K)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   302
      using aux_lemma[OF assms(2) assms(3) s1]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   303
            aux_lemma[OF assms(3) assms(2) s2] by (simp add: ideal_prod.sum)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   304
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   305
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   306
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   307
lemma (in cring) ideal_prod_commute:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   308
  assumes "ideal I R" "ideal J R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   309
  shows "I \<cdot> J = J \<cdot> I"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   310
proof -
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   311
  { fix I J assume A: "ideal I R" "ideal J R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   312
    have "I \<cdot> J \<subseteq> J \<cdot> I"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   313
    proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   314
      fix s assume "s \<in> I \<cdot> J" thus "s \<in> J \<cdot> I"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   315
      proof (induct s rule: ideal_prod.induct)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   316
        case (prod i j) thus ?case
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   317
          using m_comm[OF ideal.Icarr[OF A(1) prod(1)] ideal.Icarr[OF A(2) prod(2)]]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   318
          by (simp add: ideal_prod.prod)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   319
      next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   320
        case (sum s1 s2) thus ?case by (simp add: ideal_prod.sum) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   321
      qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   322
    qed }
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   323
  thus ?thesis using assms by blast 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   324
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   325
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   326
text \<open>The following result would also be true for locale ring\<close>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   327
lemma (in cring) ideal_prod_distr:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   328
  assumes "ideal I R" "ideal J R" "ideal K R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   329
  shows "I \<cdot> (J <+> K) = (I \<cdot> J) <+>  (I \<cdot> K)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   330
    and "(J <+> K) \<cdot> I = (J \<cdot> I) <+>  (K \<cdot> I)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   331
  by (simp_all add: assms ideal_prod_commute local.ring_axioms
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   332
                    ring.add_ideals ring.ideal_prod_r_distr)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   333
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   334
lemma (in cring) ideal_prod_eq_inter:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   335
  assumes "ideal I R" "ideal J R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   336
    and "I <+> J = carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   337
  shows "I \<cdot> J = I \<inter> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   338
proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   339
  show "I \<cdot> J \<subseteq> I \<inter> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   340
    using assms ideal_prod_inter by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   341
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   342
  show "I \<inter> J \<subseteq> I \<cdot> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   343
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   344
    have "\<one> \<in> I <+> J" using assms(3) one_closed by simp 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   345
    then obtain i j where ij: "i \<in> I" "j \<in> J" "\<one> = i \<oplus> j"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   346
      using set_add_def'[of R I J] by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   347
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   348
    fix s assume s: "s \<in> I \<inter> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   349
    hence "(i \<otimes> s \<in> I \<cdot> J) \<and> (s \<otimes> j \<in> I \<cdot> J)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   350
      using ij(1-2) by (simp add: ideal_prod.prod)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   351
    moreover have "s = (i \<otimes> s) \<oplus> (s \<otimes> j)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   352
      using ideal.Icarr[OF assms(1) ij(1)]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   353
            ideal.Icarr[OF assms(2) ij(2)]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   354
            ideal.Icarr[OF assms(1), of s]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   355
      by (metis ij(3) s m_comm[of s i] Int_iff r_distr r_one)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   356
    ultimately show "s \<in>  I \<cdot> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   357
      using ideal_prod.sum by fastforce
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   358
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   359
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   360
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   361
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   362
subsection \<open>Structure of the Set of Ideals\<close>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   363
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   364
text \<open>We focus on commutative rings for convenience.\<close>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   365
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   366
lemma (in cring) ideals_set_is_semiring: "semiring (ideals_set R)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   367
proof -
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   368
  have "abelian_monoid (ideals_set R)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   369
    apply (rule abelian_monoidI) unfolding ideals_set_def
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   370
    apply (simp_all add: add_ideals zeroideal)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   371
    apply (simp add: add.set_mult_assoc additive_subgroup.a_subset ideal.axioms(1) set_add_defs(1))
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   372
    apply (metis Un_absorb1 additive_subgroup.a_subset additive_subgroup.zero_closed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   373
        cgenideal_minimal cgenideal_self empty_iff genideal_minimal ideal.axioms(1)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   374
        local.ring_axioms order_refl ring.genideal_self subset_antisym subset_singletonD
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   375
        union_genideal zero_closed zeroideal)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   376
    by (metis sup_commute union_genideal)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   377
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   378
  moreover have "monoid (ideals_set R)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   379
    apply (rule monoidI) unfolding ideals_set_def
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   380
    apply (simp_all add: ideal_prod_is_ideal oneideal
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   381
                         ideal_prod_commute ideal_prod_one)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   382
    by (metis ideal_prod_assoc ideal_prod_commute)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   383
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   384
  ultimately show ?thesis
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   385
    unfolding semiring_def semiring_axioms_def ideals_set_def
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   386
    by (simp_all add: ideal_prod_distr ideal_prod_commute ideal_prod_zero zeroideal) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   387
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   388
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   389
lemma (in cring) ideals_set_is_comm_monoid: "comm_monoid (ideals_set R)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   390
proof -
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   391
  have "monoid (ideals_set R)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   392
    apply (rule monoidI) unfolding ideals_set_def
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   393
    apply (simp_all add: ideal_prod_is_ideal oneideal
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   394
                         ideal_prod_commute ideal_prod_one)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   395
    by (metis ideal_prod_assoc ideal_prod_commute)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   396
  thus ?thesis
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   397
    unfolding comm_monoid_def comm_monoid_axioms_def
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   398
    by (simp add: ideal_prod_commute ideals_set_def)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   399
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   400
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   401
lemma (in cring) ideal_prod_eq_Inter_aux:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   402
  assumes "I: {..(Suc n)} \<rightarrow> { J. ideal J R }" 
68606
96a49db47c97 removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents: 68605
diff changeset
   403
    and "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n \<rbrakk> \<Longrightarrow>
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   404
                 i \<noteq> j \<Longrightarrow> (I i) <+> (I j) = carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   405
  shows "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..n}. I k) <+> (I (Suc n)) = carrier R" using assms
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   406
proof (induct n arbitrary: I)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   407
  case 0
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   408
  hence "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..0}. I k) <+> I (Suc 0) = (I 0) <+> (I (Suc 0))"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   409
    using comm_monoid.finprod_0[OF ideals_set_is_comm_monoid, of I]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   410
    by (simp add: atMost_Suc ideals_set_def)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   411
  also have " ... = carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   412
    using 0(2)[of 0 "Suc 0"] by simp
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   413
  finally show ?case .
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   414
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   415
  interpret ISet: comm_monoid "ideals_set R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   416
    by (simp add: ideals_set_is_comm_monoid)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   417
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   418
  case (Suc n)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   419
  let ?I' = "\<lambda>i. I (Suc i)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   420
  have "?I': {..(Suc n)} \<rightarrow> { J. ideal J R }"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   421
    using Suc.prems(1) by auto
68606
96a49db47c97 removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents: 68605
diff changeset
   422
  moreover have "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n \<rbrakk> \<Longrightarrow>
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   423
                         i \<noteq> j \<Longrightarrow> (?I' i) <+> (?I' j) = carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   424
    by (simp add: Suc.prems(2))
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   425
  ultimately have "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..n}. ?I' k) <+> (?I' (Suc n)) = carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   426
    using Suc.hyps by metis
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   427
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   428
  moreover have I_carr: "I: {..Suc (Suc n)} \<rightarrow> carrier (ideals_set R)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   429
    unfolding ideals_set_def using Suc by simp
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   430
  hence I'_carr: "I \<in> Suc ` {..n} \<rightarrow> carrier (ideals_set R)" by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   431
  ultimately have "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {(Suc 0)..Suc n}. I k) <+> (I (Suc (Suc n))) = carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   432
    using ISet.finprod_reindex[of I "\<lambda>i. Suc i" "{..n}"] by (simp add: atMost_atLeast0) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   433
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   434
  hence "(carrier R) \<cdot> (I 0) = ((\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {Suc 0..Suc n}. I k) <+> I (Suc (Suc n))) \<cdot> (I 0)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   435
    by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   436
  moreover have fprod_cl1: "ideal (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {Suc 0..Suc n}. I k) R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   437
    by (metis I'_carr ISet.finprod_closed One_nat_def ideals_set_def image_Suc_atMost
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   438
        mem_Collect_eq partial_object.select_convs(1))
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   439
  ultimately
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   440
  have "I 0 = (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {Suc 0..Suc n}. I k) \<cdot> (I 0) <+> I (Suc (Suc n)) \<cdot> (I 0)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   441
    by (metis PiE Suc.prems(1) atLeast0_atMost_Suc atLeast0_atMost_Suc_eq_insert_0
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   442
        atMost_atLeast0 ideal_prod_commute ideal_prod_distr(2) ideal_prod_one insertI1
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   443
        mem_Collect_eq oneideal)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   444
  also have " ... = (I 0) \<cdot> (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {Suc 0..Suc n}. I k) <+> I (Suc (Suc n)) \<cdot> (I 0)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   445
    using fprod_cl1 ideal_prod_commute Suc.prems(1)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   446
    by (simp add: atLeast0_atMost_Suc_eq_insert_0 atMost_atLeast0) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   447
  also have " ... = (I 0) \<otimes>\<^bsub>(ideals_set R)\<^esub> (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {Suc 0..Suc n}. I k) <+>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   448
                     I (Suc (Suc n)) \<cdot> (I 0)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   449
    by (simp add: ideals_set_def)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   450
  finally have I0: "I 0 = (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) <+> I (Suc (Suc n)) \<cdot> (I 0)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   451
    using ISet.finprod_insert[of "{Suc 0..Suc n}" 0 I]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   452
          I_carr I'_carr atMost_atLeast0 ISet.finprod_0' atMost_Suc by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   453
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   454
  have I_SucSuc_I0: "ideal (I (Suc (Suc n))) R \<and> ideal (I 0) R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   455
    using Suc.prems(1) by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   456
  have fprod_cl2: "ideal (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) R"
68605
440aa6b7d99a removal of smt
paulson <lp15@cam.ac.uk>
parents: 68582
diff changeset
   457
    by (metis (no_types) ISet.finprod_closed I_carr Pi_split_insert_domain atMost_Suc ideals_set_def mem_Collect_eq partial_object.select_convs(1))
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   458
  have "carrier R = I (Suc (Suc n)) <+> I 0"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   459
    by (simp add: Suc.prems(2))
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   460
  also have " ... = I (Suc (Suc n)) <+>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   461
                    ((\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) <+> I (Suc (Suc n)) \<cdot> (I 0))"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   462
    using I0 by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   463
  also have " ... = I (Suc (Suc n)) <+>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   464
                    (I (Suc (Suc n)) \<cdot> (I 0) <+> (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k))"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   465
    using fprod_cl2 I_SucSuc_I0 by (metis Un_commute ideal_prod_is_ideal union_genideal)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   466
  also have " ... = (I (Suc (Suc n)) <+> I (Suc (Suc n)) \<cdot> (I 0)) <+>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   467
                    (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   468
    using fprod_cl2 I_SucSuc_I0 by (metis add.set_mult_assoc ideal_def ideal_prod_in_carrier
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   469
                                          oneideal ring.ideal_prod_one set_add_defs(1)) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   470
  also have " ... = I (Suc (Suc n)) <+> (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   471
    using ideal_prod_simp[of "I (Suc (Suc n))" "I 0"] I_SucSuc_I0 by simp 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   472
  also have " ... = (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) <+> I (Suc (Suc n))"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   473
    using fprod_cl2 I_SucSuc_I0 by (metis Un_commute union_genideal)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   474
  finally show ?case by simp
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   475
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   476
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   477
theorem (in cring) ideal_prod_eq_Inter:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   478
  assumes "I: {..n :: nat} \<rightarrow> { J. ideal J R }" 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   479
    and "\<And>i j. \<lbrakk> i \<in> {..n}; j \<in> {..n} \<rbrakk> \<Longrightarrow> i \<noteq> j \<Longrightarrow> (I i) <+> (I j) = carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   480
  shows "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..n}. I k) = (\<Inter> k \<in> {..n}. I k)" using assms
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   481
proof (induct n)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   482
  case 0 thus ?case
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   483
    using comm_monoid.finprod_0[OF ideals_set_is_comm_monoid] by (simp add: ideals_set_def) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   484
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   485
  interpret ISet: comm_monoid "ideals_set R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   486
    by (simp add: ideals_set_is_comm_monoid)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   487
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   488
  case (Suc n)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   489
  hence IH: "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..n}. I k) = (\<Inter> k \<in> {..n}. I k)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   490
    by (simp add: atMost_Suc)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   491
  hence "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) = I (Suc n) \<otimes>\<^bsub>(ideals_set R)\<^esub> (\<Inter> k \<in> {..n}. I k)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   492
    using ISet.finprod_insert[of "{Suc 0..Suc n}" 0 I] atMost_Suc_eq_insert_0[of n]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   493
    by (metis ISet.finprod_Suc Suc.prems(1) ideals_set_def partial_object.select_convs(1))
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   494
  hence "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) = I (Suc n) \<cdot> (\<Inter> k \<in> {..n}. I k)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   495
    by (simp add: ideals_set_def)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   496
  moreover have "(\<Inter> k \<in> {..n}. I k) <+> I (Suc n) = carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   497
    using ideal_prod_eq_Inter_aux[of I n] by (simp add: Suc.prems IH)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   498
  moreover have "ideal (\<Inter> k \<in> {..n}. I k) R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   499
    using ring.i_Intersect[of R "I ` {..n}"]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   500
    by (metis IH ISet.finprod_closed Pi_split_insert_domain Suc.prems(1) atMost_Suc
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   501
              ideals_set_def mem_Collect_eq partial_object.select_convs(1))
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   502
  ultimately
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   503
  have "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) = (\<Inter> k \<in> {..n}. I k) \<inter> I (Suc n)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   504
    using ideal_prod_eq_inter[of "\<Inter> k \<in> {..n}. I k" "I (Suc n)"]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   505
          ideal_prod_commute[of "\<Inter> k \<in> {..n}. I k" "I (Suc n)"]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   506
    by (metis PiE Suc.prems(1) atMost_iff mem_Collect_eq order_refl)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   507
  thus ?case by (simp add: Int_commute atMost_Suc) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   508
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   509
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   510
corollary (in cring) inter_plus_ideal_eq_carrier:
68606
96a49db47c97 removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents: 68605
diff changeset
   511
  assumes "\<And>i. i \<le> Suc n \<Longrightarrow> ideal (I i) R" 
96a49db47c97 removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents: 68605
diff changeset
   512
      and "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   513
  shows "(\<Inter> i \<le> n. I i) <+> (I (Suc n)) = carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   514
  using ideal_prod_eq_Inter[of I n] ideal_prod_eq_Inter_aux[of I n] by (auto simp add: assms)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   515
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   516
corollary (in cring) inter_plus_ideal_eq_carrier_arbitrary:
68606
96a49db47c97 removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents: 68605
diff changeset
   517
  assumes "\<And>i. i \<le> Suc n \<Longrightarrow> ideal (I i) R" 
96a49db47c97 removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents: 68605
diff changeset
   518
      and "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
96a49db47c97 removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents: 68605
diff changeset
   519
      and "j \<le> Suc n"
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   520
  shows "(\<Inter> i \<in> ({..(Suc n)} - { j }). I i) <+> (I j) = carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   521
proof -
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   522
  define I' where "I' = (\<lambda>i. if i = Suc n then (I j) else
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   523
                             if i = j     then (I (Suc n))
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   524
                                          else (I i))"
68606
96a49db47c97 removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents: 68605
diff changeset
   525
  have "\<And>i. i \<le> Suc n \<Longrightarrow> ideal (I' i) R"
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   526
    using I'_def assms(1) assms(3) by auto
68606
96a49db47c97 removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents: 68605
diff changeset
   527
  moreover have "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n; i \<noteq> j \<rbrakk> \<Longrightarrow> I' i <+> I' j = carrier R"
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   528
    using I'_def assms(2-3) by force
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   529
  ultimately have "(\<Inter> i \<le> n. I' i) <+> (I' (Suc n)) = carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   530
    using inter_plus_ideal_eq_carrier by simp
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   531
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   532
  moreover have "I' ` {..n} = I ` ({..(Suc n)} - { j })"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   533
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   534
    show "I' ` {..n} \<subseteq> I ` ({..Suc n} - {j})"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   535
    proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   536
      fix x assume "x \<in> I' ` {..n}"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   537
      then obtain i where i: "i \<in> {..n}" "I' i = x" by blast
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   538
      thus "x \<in> I ` ({..Suc n} - {j})"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   539
      proof (cases)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   540
        assume "i = j" thus ?thesis using i I'_def by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   541
      next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   542
        assume "i \<noteq> j" thus ?thesis using I'_def i insert_iff by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   543
      qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   544
    qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   545
  next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   546
    show "I ` ({..Suc n} - {j}) \<subseteq> I' ` {..n}"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   547
    proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   548
      fix x assume "x \<in> I ` ({..Suc n} - {j})"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   549
      then obtain i where i: "i \<in> {..Suc n}" "i \<noteq> j" "I i = x" by blast
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   550
      thus "x \<in> I' ` {..n}"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   551
      proof (cases)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   552
        assume "i = Suc n" thus ?thesis using I'_def assms(3) i(2-3) by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   553
      next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   554
        assume "i \<noteq> Suc n" thus ?thesis using I'_def i by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   555
      qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   556
    qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   557
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   558
  ultimately show ?thesis using I'_def by metis 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   559
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   560
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   561
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   562
subsection \<open>Another Characterization of Prime Ideals\<close>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   563
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   564
text \<open>With product of ideals being defined, we can give another definition of a prime ideal\<close>
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   565
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   566
lemma (in ring) primeideal_divides_ideal_prod:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   567
  assumes "primeideal P R" "ideal I R" "ideal J R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   568
      and "I \<cdot> J \<subseteq> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   569
    shows "I \<subseteq> P \<or> J \<subseteq> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   570
proof (cases)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   571
  assume "\<exists> i \<in> I. i \<notin> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   572
  then obtain i where i: "i \<in> I" "i \<notin> P" by blast
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   573
  have "J \<subseteq> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   574
  proof
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   575
    fix j assume j: "j \<in> J"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   576
    hence "i \<otimes> j \<in> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   577
      using ideal_prod.prod[OF i(1) j, of R] assms(4) by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   578
    thus "j \<in> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   579
      using primeideal.I_prime[OF assms(1), of i j] i j
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   580
      by (meson assms(2-3) ideal.Icarr) 
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   581
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   582
  thus ?thesis by blast
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   583
next
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   584
  assume "\<not> (\<exists> i \<in> I. i \<notin> P)" thus ?thesis by blast
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   585
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   586
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   587
lemma (in cring) divides_ideal_prod_imp_primeideal:
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   588
  assumes "ideal P R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   589
    and "P \<noteq> carrier R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   590
    and "\<And>I J. \<lbrakk> ideal I R; ideal J R; I \<cdot> J \<subseteq> P \<rbrakk> \<Longrightarrow> I \<subseteq> P \<or> J \<subseteq> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   591
  shows "primeideal P R"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   592
proof -
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   593
  have "\<And>a b. \<lbrakk> a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> P \<rbrakk> \<Longrightarrow> a \<in> P \<or> b \<in> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   594
  proof -
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   595
    fix a b assume A: "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b \<in> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   596
    have "(PIdl a) \<cdot> (PIdl b) = Idl (PIdl (a \<otimes> b))"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   597
      using ideal_prod_eq_genideal[of "Idl { a }" "Idl { b }"]
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   598
            A(1-2) cgenideal_eq_genideal cgenideal_ideal cgenideal_prod by auto
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   599
    hence "(PIdl a) \<cdot> (PIdl b) = PIdl (a \<otimes> b)"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   600
      by (simp add: A Idl_subset_ideal cgenideal_ideal cgenideal_minimal
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   601
                    genideal_self oneideal subset_antisym)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   602
    hence "(PIdl a) \<cdot> (PIdl b) \<subseteq> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   603
      by (simp add: A(3) assms(1) cgenideal_minimal)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   604
    hence "(PIdl a) \<subseteq> P \<or> (PIdl b) \<subseteq> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   605
      by (simp add: A assms(3) cgenideal_ideal)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   606
    thus "a \<in> P \<or> b \<in> P"
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   607
      using A cgenideal_self by blast
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   608
  qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   609
  thus ?thesis
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   610
    using assms is_cring by (simp add: primeidealI)
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   611
qed
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   612
68582
b9b9e2985878 more standard headers;
wenzelm
parents: 68569
diff changeset
   613
end