src/HOL/Algebra/CRing.thy
author obua
Sun, 09 May 2004 23:04:36 +0200
changeset 14722 8e739a6eaf11
parent 14666 65f8680c3f16
child 14963 d584e32f7d46
permissions -rw-r--r--
replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
     1
(*
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
     2
  Title:     The algebraic hierarchy of rings
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
     3
  Id:        $Id$
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
     4
  Author:    Clemens Ballarin, started 9 December 1996
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
     5
  Copyright: Clemens Ballarin
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
     6
*)
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
     7
14577
dbb95b825244 tuned document;
wenzelm
parents: 14551
diff changeset
     8
header {* Abelian Groups *}
dbb95b825244 tuned document;
wenzelm
parents: 14551
diff changeset
     9
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    10
theory CRing = FiniteProduct
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
    11
files ("ringsimp.ML"):
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
    12
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    13
record 'a ring = "'a monoid" +
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    14
  zero :: 'a ("\<zero>\<index>")
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    15
  add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    16
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    17
text {* Derived operations. *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    18
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
    19
constdefs (structure R)
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
    20
  a_inv :: "[_, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    21
  "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    22
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    23
  minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
    24
  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    25
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    26
locale abelian_monoid = struct G +
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    27
  assumes a_comm_monoid: "comm_monoid (| carrier = carrier G,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    28
      mult = add G, one = zero G |)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    29
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    30
text {*
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    31
  The following definition is redundant but simple to use.
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    32
*}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    33
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    34
locale abelian_group = abelian_monoid +
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    35
  assumes a_comm_group: "comm_group (| carrier = carrier G,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    36
      mult = add G, one = zero G |)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    37
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    38
subsection {* Basic Properties *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    39
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    40
lemma abelian_monoidI:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    41
  assumes a_closed:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    42
      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y \<in> carrier R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    43
    and zero_closed: "zero R \<in> carrier R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    44
    and a_assoc:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    45
      "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    46
      add R (add R x y) z = add R x (add R y z)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    47
    and l_zero: "!!x. x \<in> carrier R ==> add R (zero R) x = x"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    48
    and a_comm:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    49
      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y = add R y x"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    50
  shows "abelian_monoid R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    51
  by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    52
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    53
lemma abelian_groupI:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    54
  assumes a_closed:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    55
      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y \<in> carrier R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    56
    and zero_closed: "zero R \<in> carrier R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    57
    and a_assoc:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    58
      "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    59
      add R (add R x y) z = add R x (add R y z)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    60
    and a_comm:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    61
      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y = add R y x"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    62
    and l_zero: "!!x. x \<in> carrier R ==> add R (zero R) x = x"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    63
    and l_inv_ex: "!!x. x \<in> carrier R ==> EX y : carrier R. add R y x = zero R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    64
  shows "abelian_group R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    65
  by (auto intro!: abelian_group.intro abelian_monoidI
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    66
      abelian_group_axioms.intro comm_monoidI comm_groupI
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    67
    intro: prems)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    68
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    69
(* TODO: The following thms are probably unnecessary. *)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    70
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    71
lemma (in abelian_monoid) a_magma:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    72
  "magma (| carrier = carrier G, mult = add G, one = zero G |)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    73
  by (rule comm_monoid.axioms) (rule a_comm_monoid)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    74
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    75
lemma (in abelian_monoid) a_semigroup:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    76
  "semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    77
  by (unfold semigroup_def) (fast intro: comm_monoid.axioms a_comm_monoid)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    78
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    79
lemma (in abelian_monoid) a_monoid:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    80
  "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    81
  by (unfold monoid_def) (fast intro: a_comm_monoid comm_monoid.axioms)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    82
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    83
lemma (in abelian_group) a_group:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    84
  "group (| carrier = carrier G, mult = add G, one = zero G |)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    85
  by (unfold group_def semigroup_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    86
    (fast intro: comm_group.axioms a_comm_group)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    87
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    88
lemma (in abelian_monoid) a_comm_semigroup:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    89
  "comm_semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    90
  by (unfold comm_semigroup_def semigroup_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    91
    (fast intro: comm_monoid.axioms a_comm_monoid)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    92
14286
0ae66ffb9784 New structure "partial_object" as common root for lattices and magmas.
ballarin
parents: 14213
diff changeset
    93
lemmas monoid_record_simps = partial_object.simps semigroup.simps monoid.simps
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    94
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    95
lemma (in abelian_monoid) a_closed [intro, simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    96
  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y \<in> carrier G"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    97
  by (rule magma.m_closed [OF a_magma, simplified monoid_record_simps]) 
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    98
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
    99
lemma (in abelian_monoid) zero_closed [intro, simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   100
  "\<zero> \<in> carrier G"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   101
  by (rule monoid.one_closed [OF a_monoid, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   102
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   103
lemma (in abelian_group) a_inv_closed [intro, simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   104
  "x \<in> carrier G ==> \<ominus> x \<in> carrier G"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   105
  by (simp add: a_inv_def
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   106
    group.inv_closed [OF a_group, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   107
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   108
lemma (in abelian_group) minus_closed [intro, simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   109
  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   110
  by (simp add: minus_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   111
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   112
lemma (in abelian_group) a_l_cancel [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   113
  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   114
   (x \<oplus> y = x \<oplus> z) = (y = z)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   115
  by (rule group.l_cancel [OF a_group, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   116
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   117
lemma (in abelian_group) a_r_cancel [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   118
  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   119
   (y \<oplus> x = z \<oplus> x) = (y = z)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   120
  by (rule group.r_cancel [OF a_group, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   121
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   122
lemma (in abelian_monoid) a_assoc:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   123
  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   124
  (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   125
  by (rule semigroup.m_assoc [OF a_semigroup, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   126
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   127
lemma (in abelian_monoid) l_zero [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   128
  "x \<in> carrier G ==> \<zero> \<oplus> x = x"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   129
  by (rule monoid.l_one [OF a_monoid, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   130
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   131
lemma (in abelian_group) l_neg:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   132
  "x \<in> carrier G ==> \<ominus> x \<oplus> x = \<zero>"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   133
  by (simp add: a_inv_def
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   134
    group.l_inv [OF a_group, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   135
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   136
lemma (in abelian_monoid) a_comm:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   137
  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y = y \<oplus> x"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   138
  by (rule comm_semigroup.m_comm [OF a_comm_semigroup,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   139
    simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   140
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   141
lemma (in abelian_monoid) a_lcomm:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   142
  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   143
   x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   144
  by (rule comm_semigroup.m_lcomm [OF a_comm_semigroup,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   145
    simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   146
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   147
lemma (in abelian_monoid) r_zero [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   148
  "x \<in> carrier G ==> x \<oplus> \<zero> = x"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   149
  using monoid.r_one [OF a_monoid]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   150
  by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   151
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   152
lemma (in abelian_group) r_neg:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   153
  "x \<in> carrier G ==> x \<oplus> (\<ominus> x) = \<zero>"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   154
  using group.r_inv [OF a_group]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   155
  by (simp add: a_inv_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   156
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   157
lemma (in abelian_group) minus_zero [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   158
  "\<ominus> \<zero> = \<zero>"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   159
  by (simp add: a_inv_def
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   160
    group.inv_one [OF a_group, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   161
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   162
lemma (in abelian_group) minus_minus [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   163
  "x \<in> carrier G ==> \<ominus> (\<ominus> x) = x"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   164
  using group.inv_inv [OF a_group, simplified monoid_record_simps]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   165
  by (simp add: a_inv_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   166
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   167
lemma (in abelian_group) a_inv_inj:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   168
  "inj_on (a_inv G) (carrier G)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   169
  using group.inv_inj [OF a_group, simplified monoid_record_simps]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   170
  by (simp add: a_inv_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   171
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   172
lemma (in abelian_group) minus_add:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   173
  "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   174
  using comm_group.inv_mult [OF a_comm_group]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   175
  by (simp add: a_inv_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   176
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   177
lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   178
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   179
subsection {* Sums over Finite Sets *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   180
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   181
text {*
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   182
  This definition makes it easy to lift lemmas from @{term finprod}.
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   183
*}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   184
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   185
constdefs
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   186
  finsum :: "[_, 'a => 'b, 'a set] => 'b"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   187
  "finsum G f A == finprod (| carrier = carrier G,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   188
     mult = add G, one = zero G |) f A"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   189
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   190
syntax
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   191
  "_finsum" :: "index => idt => 'a set => 'b => 'b"
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   192
      ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   193
syntax (xsymbols)
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   194
  "_finsum" :: "index => idt => 'a set => 'b => 'b"
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   195
      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   196
syntax (HTML output)
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   197
  "_finsum" :: "index => idt => 'a set => 'b => 'b"
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   198
      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   199
translations
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   200
  "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   201
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   202
(*
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   203
  lemmas (in abelian_monoid) finsum_empty [simp] =
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   204
    comm_monoid.finprod_empty [OF a_comm_monoid, simplified]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   205
  is dangeous, because attributes (like simplified) are applied upon opening
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   206
  the locale, simplified refers to the simpset at that time!!!
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   207
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   208
  lemmas (in abelian_monoid) finsum_empty [simp] =
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   209
    abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   210
      simplified monoid_record_simps]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   211
makes the locale slow, because proofs are repeated for every
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   212
"lemma (in abelian_monoid)" command.
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   213
When lemma is used time in UnivPoly.thy from beginning to UP_cring goes down
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   214
from 110 secs to 60 secs.
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   215
*)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   216
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   217
lemma (in abelian_monoid) finsum_empty [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   218
  "finsum G f {} = \<zero>"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   219
  by (rule comm_monoid.finprod_empty [OF a_comm_monoid,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   220
    folded finsum_def, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   221
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   222
lemma (in abelian_monoid) finsum_insert [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   223
  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   224
  ==> finsum G f (insert a F) = f a \<oplus> finsum G f F"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   225
  by (rule comm_monoid.finprod_insert [OF a_comm_monoid,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   226
    folded finsum_def, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   227
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   228
lemma (in abelian_monoid) finsum_zero [simp]:
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   229
  "finite A ==> (\<Oplus>i: A. \<zero>) = \<zero>"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   230
  by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   231
    simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   232
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   233
lemma (in abelian_monoid) finsum_closed [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   234
  fixes A
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   235
  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   236
  shows "finsum G f A \<in> carrier G"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   237
  by (rule comm_monoid.finprod_closed [OF a_comm_monoid,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   238
    folded finsum_def, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   239
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   240
lemma (in abelian_monoid) finsum_Un_Int:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   241
  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   242
     finsum G g (A Un B) \<oplus> finsum G g (A Int B) =
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   243
     finsum G g A \<oplus> finsum G g B"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   244
  by (rule comm_monoid.finprod_Un_Int [OF a_comm_monoid,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   245
    folded finsum_def, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   246
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   247
lemma (in abelian_monoid) finsum_Un_disjoint:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   248
  "[| finite A; finite B; A Int B = {};
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   249
      g \<in> A -> carrier G; g \<in> B -> carrier G |]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   250
   ==> finsum G g (A Un B) = finsum G g A \<oplus> finsum G g B"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   251
  by (rule comm_monoid.finprod_Un_disjoint [OF a_comm_monoid,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   252
    folded finsum_def, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   253
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   254
lemma (in abelian_monoid) finsum_addf:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   255
  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   256
   finsum G (%x. f x \<oplus> g x) A = (finsum G f A \<oplus> finsum G g A)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   257
  by (rule comm_monoid.finprod_multf [OF a_comm_monoid,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   258
    folded finsum_def, simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   259
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   260
lemma (in abelian_monoid) finsum_cong':
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   261
  "[| A = B; g : B -> carrier G;
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   262
      !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   263
  by (rule comm_monoid.finprod_cong' [OF a_comm_monoid,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   264
    folded finsum_def, simplified monoid_record_simps]) auto
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   265
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   266
lemma (in abelian_monoid) finsum_0 [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   267
  "f : {0::nat} -> carrier G ==> finsum G f {..0} = f 0"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   268
  by (rule comm_monoid.finprod_0 [OF a_comm_monoid, folded finsum_def,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   269
    simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   270
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   271
lemma (in abelian_monoid) finsum_Suc [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   272
  "f : {..Suc n} -> carrier G ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   273
   finsum G f {..Suc n} = (f (Suc n) \<oplus> finsum G f {..n})"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   274
  by (rule comm_monoid.finprod_Suc [OF a_comm_monoid, folded finsum_def,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   275
    simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   276
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   277
lemma (in abelian_monoid) finsum_Suc2:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   278
  "f : {..Suc n} -> carrier G ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   279
   finsum G f {..Suc n} = (finsum G (%i. f (Suc i)) {..n} \<oplus> f 0)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   280
  by (rule comm_monoid.finprod_Suc2 [OF a_comm_monoid, folded finsum_def,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   281
    simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   282
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   283
lemma (in abelian_monoid) finsum_add [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   284
  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   285
     finsum G (%i. f i \<oplus> g i) {..n::nat} =
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   286
     finsum G f {..n} \<oplus> finsum G g {..n}"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   287
  by (rule comm_monoid.finprod_mult [OF a_comm_monoid, folded finsum_def,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   288
    simplified monoid_record_simps])
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   289
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   290
lemma (in abelian_monoid) finsum_cong:
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   291
  "[| A = B; f : B -> carrier G = True;
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   292
      !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   293
  by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   294
    simplified monoid_record_simps]) auto
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   295
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   296
text {*Usually, if this rule causes a failed congruence proof error,
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   297
   the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   298
   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   299
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   300
section {* The Algebraic Hierarchy of Rings *}
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   301
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   302
subsection {* Basic Definitions *}
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   303
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   304
locale ring = abelian_group R + monoid R +
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   305
  assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   306
      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   307
    and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   308
      ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   309
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   310
locale cring = ring + comm_monoid R
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   311
13864
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   312
locale "domain" = cring +
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   313
  assumes one_not_zero [simp]: "\<one> ~= \<zero>"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   314
    and integral: "[| a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R |] ==>
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   315
                  a = \<zero> | b = \<zero>"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   316
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents: 14399
diff changeset
   317
locale field = "domain" +
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents: 14399
diff changeset
   318
  assumes field_Units: "Units R = carrier R - {\<zero>}"
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents: 14399
diff changeset
   319
13864
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   320
subsection {* Basic Facts of Rings *}
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   321
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   322
lemma ringI:
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   323
  includes struct R
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   324
  assumes abelian_group: "abelian_group R"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   325
    and monoid: "monoid R"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   326
    and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   327
      ==> mult R (add R x y) z = add R (mult R x z) (mult R y z)"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   328
    and r_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   329
      ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   330
  shows "ring R"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   331
  by (auto intro: ring.intro
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   332
    abelian_group.axioms monoid.axioms ring_axioms.intro prems)
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   333
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   334
lemma (in ring) is_abelian_group:
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   335
  "abelian_group R"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   336
  by (auto intro!: abelian_groupI a_assoc a_comm l_neg)
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   337
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   338
lemma (in ring) is_monoid:
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   339
  "monoid R"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   340
  by (auto intro!: monoidI m_assoc)
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   341
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   342
lemma cringI:
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   343
  includes struct R
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   344
  assumes abelian_group: "abelian_group R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   345
    and comm_monoid: "comm_monoid R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   346
    and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   347
      ==> mult R (add R x y) z = add R (mult R x z) (mult R y z)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   348
  shows "cring R"
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   349
  proof (rule cring.intro)
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   350
    show "ring_axioms R"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   351
    -- {* Right-distributivity follows from left-distributivity and
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   352
          commutativity. *}
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   353
    proof (rule ring_axioms.intro)
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   354
      fix x y z
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   355
      assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   356
      note [simp]= comm_monoid.axioms [OF comm_monoid]
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   357
        abelian_group.axioms [OF abelian_group]
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   358
        abelian_monoid.a_closed
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   359
        magma.m_closed
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   360
        
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   361
      from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   362
        by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   363
      also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   364
      also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   365
        by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   366
      finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   367
    qed
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   368
  qed (auto intro: cring.intro
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   369
      abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   370
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   371
lemma (in cring) is_comm_monoid:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   372
  "comm_monoid R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   373
  by (auto intro!: comm_monoidI m_assoc m_comm)
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   374
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents: 14399
diff changeset
   375
subsection {* Normaliser for Rings *}
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   376
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   377
lemma (in abelian_group) r_neg2:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   378
  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   379
proof -
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   380
  assume G: "x \<in> carrier G" "y \<in> carrier G"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   381
  then have "(x \<oplus> \<ominus> x) \<oplus> y = y"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   382
    by (simp only: r_neg l_zero)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   383
  with G show ?thesis 
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   384
    by (simp add: a_ac)
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   385
qed
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   386
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   387
lemma (in abelian_group) r_neg1:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   388
  "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   389
proof -
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   390
  assume G: "x \<in> carrier G" "y \<in> carrier G"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   391
  then have "(\<ominus> x \<oplus> x) \<oplus> y = y" 
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   392
    by (simp only: l_neg l_zero)
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   393
  with G show ?thesis by (simp add: a_ac)
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   394
qed
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   395
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   396
text {* 
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   397
  The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   398
*}
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   399
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   400
lemma (in ring) l_null [simp]:
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   401
  "x \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   402
proof -
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   403
  assume R: "x \<in> carrier R"
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   404
  then have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = (\<zero> \<oplus> \<zero>) \<otimes> x"
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   405
    by (simp add: l_distr del: l_zero r_zero)
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   406
  also from R have "... = \<zero> \<otimes> x \<oplus> \<zero>" by simp
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   407
  finally have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = \<zero> \<otimes> x \<oplus> \<zero>" .
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   408
  with R show ?thesis by (simp del: r_zero)
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   409
qed
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   410
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   411
lemma (in ring) r_null [simp]:
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   412
  "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   413
proof -
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   414
  assume R: "x \<in> carrier R"
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   415
  then have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> (\<zero> \<oplus> \<zero>)"
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   416
    by (simp add: r_distr del: l_zero r_zero)
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   417
  also from R have "... = x \<otimes> \<zero> \<oplus> \<zero>" by simp
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   418
  finally have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> \<zero> \<oplus> \<zero>" .
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   419
  with R show ?thesis by (simp del: r_zero)
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   420
qed
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   421
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   422
lemma (in ring) l_minus:
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   423
  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   424
proof -
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   425
  assume R: "x \<in> carrier R" "y \<in> carrier R"
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   426
  then have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = (\<ominus> x \<oplus> x) \<otimes> y" by (simp add: l_distr)
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   427
  also from R have "... = \<zero>" by (simp add: l_neg l_null)
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   428
  finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" .
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   429
  with R have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   430
  with R show ?thesis by (simp add: a_assoc r_neg )
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   431
qed
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   432
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   433
lemma (in ring) r_minus:
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   434
  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   435
proof -
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   436
  assume R: "x \<in> carrier R" "y \<in> carrier R"
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   437
  then have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = x \<otimes> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   438
  also from R have "... = \<zero>" by (simp add: l_neg r_null)
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   439
  finally have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = \<zero>" .
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   440
  with R have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   441
  with R show ?thesis by (simp add: a_assoc r_neg )
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   442
qed
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   443
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   444
lemma (in ring) minus_eq:
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   445
  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   446
  by (simp only: minus_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   447
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   448
lemmas (in ring) ring_simprules =
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   449
  a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   450
  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   451
  r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   452
  a_lcomm r_distr l_null r_null l_minus r_minus
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   453
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   454
lemmas (in cring) cring_simprules =
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   455
  a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   456
  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   457
  r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   458
  a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   459
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   460
use "ringsimp.ML"
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   461
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   462
method_setup algebra =
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   463
  {* Method.ctxt_args cring_normalise *}
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   464
  {* computes distributive normal form in locale context cring *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   465
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   466
lemma (in cring) nat_pow_zero:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   467
  "(n::nat) ~= 0 ==> \<zero> (^) n = \<zero>"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   468
  by (induct n) simp_all
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   469
13864
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   470
text {* Two examples for use of method algebra *}
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   471
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   472
lemma
14399
dc677b35e54f New lemmas about inversion of restricted functions.
ballarin
parents: 14286
diff changeset
   473
  includes ring R + cring S
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   474
  shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==> 
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   475
  a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^sub>2 d = d \<otimes>\<^sub>2 c"
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   476
  by algebra
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   477
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   478
lemma
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   479
  includes cring
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   480
  shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents: 13835
diff changeset
   481
  by algebra
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   482
13864
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   483
subsection {* Sums over Finite Sets *}
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   484
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   485
lemma (in cring) finsum_ldistr:
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   486
  "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   487
   finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   488
proof (induct set: Finites)
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   489
  case empty then show ?case by simp
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   490
next
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   491
  case (insert F x) then show ?case by (simp add: Pi_def l_distr)
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   492
qed
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   493
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   494
lemma (in cring) finsum_rdistr:
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   495
  "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   496
   a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   497
proof (induct set: Finites)
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   498
  case empty then show ?case by simp
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   499
next
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   500
  case (insert F x) then show ?case by (simp add: Pi_def r_distr)
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   501
qed
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   502
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   503
subsection {* Facts of Integral Domains *}
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   504
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   505
lemma (in "domain") zero_not_one [simp]:
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   506
  "\<zero> ~= \<one>"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   507
  by (rule not_sym) simp
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   508
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   509
lemma (in "domain") integral_iff: (* not by default a simp rule! *)
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   510
  "[| a \<in> carrier R; b \<in> carrier R |] ==> (a \<otimes> b = \<zero>) = (a = \<zero> | b = \<zero>)"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   511
proof
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   512
  assume "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b = \<zero>"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   513
  then show "a = \<zero> | b = \<zero>" by (simp add: integral)
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   514
next
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   515
  assume "a \<in> carrier R" "b \<in> carrier R" "a = \<zero> | b = \<zero>"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   516
  then show "a \<otimes> b = \<zero>" by auto
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   517
qed
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   518
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   519
lemma (in "domain") m_lcancel:
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   520
  assumes prem: "a ~= \<zero>"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   521
    and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   522
  shows "(a \<otimes> b = a \<otimes> c) = (b = c)"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   523
proof
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   524
  assume eq: "a \<otimes> b = a \<otimes> c"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   525
  with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   526
  with R have "a = \<zero> | (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   527
  with prem and R have "b \<ominus> c = \<zero>" by auto 
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   528
  with R have "b = b \<ominus> (b \<ominus> c)" by algebra 
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   529
  also from R have "b \<ominus> (b \<ominus> c) = c" by algebra
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   530
  finally show "b = c" .
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   531
next
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   532
  assume "b = c" then show "a \<otimes> b = a \<otimes> c" by simp
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   533
qed
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   534
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   535
lemma (in "domain") m_rcancel:
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   536
  assumes prem: "a ~= \<zero>"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   537
    and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   538
  shows conc: "(b \<otimes> a = c \<otimes> a) = (b = c)"
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   539
proof -
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   540
  from prem and R have "(a \<otimes> b = a \<otimes> c) = (b = c)" by (rule m_lcancel)
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   541
  with R show ?thesis by algebra
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   542
qed
f44f121dd275 Bugs fixed and operators finprod and finsum.
ballarin
parents: 13854
diff changeset
   543
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   544
subsection {* Morphisms *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   545
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   546
constdefs
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   547
  ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   548
  "ring_hom R S == {h. h \<in> carrier R -> carrier S &
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   549
      (ALL x y. x \<in> carrier R & y \<in> carrier R -->
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   550
        h (mult R x y) = mult S (h x) (h y) &
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   551
        h (add R x y) = add S (h x) (h y)) &
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   552
      h (one R) = one S}"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   553
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   554
lemma ring_hom_memI:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   555
  assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   556
    and hom_mult: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   557
      h (mult R x y) = mult S (h x) (h y)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   558
    and hom_add: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   559
      h (add R x y) = add S (h x) (h y)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   560
    and hom_one: "h (one R) = one S"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   561
  shows "h \<in> ring_hom R S"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   562
  by (auto simp add: ring_hom_def prems Pi_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   563
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   564
lemma ring_hom_closed:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   565
  "[| h \<in> ring_hom R S; x \<in> carrier R |] ==> h x \<in> carrier S"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   566
  by (auto simp add: ring_hom_def funcset_mem)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   567
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   568
lemma ring_hom_mult:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   569
  "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   570
  h (mult R x y) = mult S (h x) (h y)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   571
  by (simp add: ring_hom_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   572
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   573
lemma ring_hom_add:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   574
  "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   575
  h (add R x y) = add S (h x) (h y)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   576
  by (simp add: ring_hom_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   577
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   578
lemma ring_hom_one:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   579
  "h \<in> ring_hom R S ==> h (one R) = one S"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   580
  by (simp add: ring_hom_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   581
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   582
locale ring_hom_cring = cring R + cring S + var h +
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   583
  assumes homh [simp, intro]: "h \<in> ring_hom R S"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   584
  notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   585
    and hom_mult [simp] = ring_hom_mult [OF homh]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   586
    and hom_add [simp] = ring_hom_add [OF homh]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   587
    and hom_one [simp] = ring_hom_one [OF homh]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   588
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   589
lemma (in ring_hom_cring) hom_zero [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   590
  "h \<zero> = \<zero>\<^sub>2"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   591
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   592
  have "h \<zero> \<oplus>\<^sub>2 h \<zero> = h \<zero> \<oplus>\<^sub>2 \<zero>\<^sub>2"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   593
    by (simp add: hom_add [symmetric] del: hom_add)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   594
  then show ?thesis by (simp del: S.r_zero)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   595
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   596
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   597
lemma (in ring_hom_cring) hom_a_inv [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   598
  "x \<in> carrier R ==> h (\<ominus> x) = \<ominus>\<^sub>2 h x"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   599
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   600
  assume R: "x \<in> carrier R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   601
  then have "h x \<oplus>\<^sub>2 h (\<ominus> x) = h x \<oplus>\<^sub>2 (\<ominus>\<^sub>2 h x)"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   602
    by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   603
  with R show ?thesis by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   604
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   605
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   606
lemma (in ring_hom_cring) hom_finsum [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   607
  "[| finite A; f \<in> A -> carrier R |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   608
  h (finsum R f A) = finsum S (h o f) A"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   609
proof (induct set: Finites)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   610
  case empty then show ?case by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   611
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   612
  case insert then show ?case by (simp add: Pi_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   613
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   614
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   615
lemma (in ring_hom_cring) hom_finprod:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   616
  "[| finite A; f \<in> A -> carrier R |] ==>
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   617
  h (finprod R f A) = finprod S (h o f) A"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   618
proof (induct set: Finites)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   619
  case empty then show ?case by simp
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   620
next
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   621
  case insert then show ?case by (simp add: Pi_def)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   622
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   623
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   624
declare ring_hom_cring.hom_finprod [simp]
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   625
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   626
lemma id_ring_hom [simp]:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   627
  "id \<in> ring_hom R R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   628
  by (auto intro!: ring_hom_memI)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   629
13835
12b2ffbe543a Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
diff changeset
   630
end