src/HOL/Algebra/More_Ring.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66760 d44ea023ac09
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@65435
     1
(*  Title:      HOL/Algebra/More_Ring.thy
haftmann@65416
     2
    Author:     Jeremy Avigad
haftmann@65416
     3
*)
haftmann@65416
     4
haftmann@65416
     5
section \<open>More on rings etc.\<close>
haftmann@65416
     6
haftmann@65416
     7
theory More_Ring
wenzelm@66760
     8
  imports Ring
haftmann@65416
     9
begin
haftmann@65416
    10
wenzelm@66760
    11
lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> \<noteq> \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
haftmann@65416
    12
  apply (unfold_locales)
wenzelm@66760
    13
    apply (use cring_axioms in auto)
wenzelm@66760
    14
   apply (rule trans)
wenzelm@66760
    15
    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
wenzelm@66760
    16
     apply assumption
wenzelm@66760
    17
    apply (subst m_assoc)
wenzelm@66760
    18
       apply auto
haftmann@65416
    19
  apply (unfold Units_def)
haftmann@65416
    20
  apply auto
haftmann@65416
    21
  done
haftmann@65416
    22
wenzelm@66760
    23
lemma (in monoid) inv_char:
wenzelm@66760
    24
  "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
wenzelm@66760
    25
  apply (subgoal_tac "x \<in> Units G")
wenzelm@66760
    26
   apply (subgoal_tac "y = inv x \<otimes> \<one>")
wenzelm@66760
    27
    apply simp
wenzelm@66760
    28
   apply (erule subst)
wenzelm@66760
    29
   apply (subst m_assoc [symmetric])
wenzelm@66760
    30
      apply auto
haftmann@65416
    31
  apply (unfold Units_def)
haftmann@65416
    32
  apply auto
haftmann@65416
    33
  done
haftmann@65416
    34
wenzelm@66760
    35
lemma (in comm_monoid) comm_inv_char: "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
haftmann@65416
    36
  apply (rule inv_char)
wenzelm@66760
    37
     apply auto
haftmann@65416
    38
  apply (subst m_comm, auto)
haftmann@65416
    39
  done
haftmann@65416
    40
haftmann@65416
    41
lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
haftmann@65416
    42
  apply (rule inv_char)
wenzelm@66760
    43
     apply (auto simp add: l_minus r_minus)
haftmann@65416
    44
  done
haftmann@65416
    45
wenzelm@66760
    46
lemma (in monoid) inv_eq_imp_eq: "x \<in> Units G \<Longrightarrow> y \<in> Units G \<Longrightarrow> inv x = inv y \<Longrightarrow> x = y"
wenzelm@66760
    47
  apply (subgoal_tac "inv (inv x) = inv (inv y)")
wenzelm@66760
    48
   apply (subst (asm) Units_inv_inv)+
wenzelm@66760
    49
    apply auto
haftmann@65416
    50
  done
haftmann@65416
    51
wenzelm@66760
    52
lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
haftmann@65416
    53
  apply (unfold Units_def)
haftmann@65416
    54
  apply auto
haftmann@65416
    55
  apply (rule_tac x = "\<ominus> \<one>" in bexI)
wenzelm@66760
    56
   apply auto
haftmann@65416
    57
  apply (simp add: l_minus r_minus)
haftmann@65416
    58
  done
haftmann@65416
    59
haftmann@65416
    60
lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
haftmann@65416
    61
  apply (rule inv_char)
wenzelm@66760
    62
     apply auto
haftmann@65416
    63
  done
haftmann@65416
    64
wenzelm@66760
    65
lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
haftmann@65416
    66
  apply auto
haftmann@65416
    67
  apply (subst Units_inv_inv [symmetric])
wenzelm@66760
    68
   apply auto
haftmann@65416
    69
  done
haftmann@65416
    70
wenzelm@66760
    71
lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
haftmann@65416
    72
  by (metis Units_inv_inv inv_one)
haftmann@65416
    73
haftmann@65416
    74
end