src/HOL/Algebra/More_Ring.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 66760 d44ea023ac09 permissions -rw-r--r--
tuned: each session has at most one defining entry;
```     1 (*  Title:      HOL/Algebra/More_Ring.thy
```
```     2     Author:     Jeremy Avigad
```
```     3 *)
```
```     4
```
```     5 section \<open>More on rings etc.\<close>
```
```     6
```
```     7 theory More_Ring
```
```     8   imports Ring
```
```     9 begin
```
```    10
```
```    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"
```
```    12   apply (unfold_locales)
```
```    13     apply (use cring_axioms in auto)
```
```    14    apply (rule trans)
```
```    15     apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
```
```    16      apply assumption
```
```    17     apply (subst m_assoc)
```
```    18        apply auto
```
```    19   apply (unfold Units_def)
```
```    20   apply auto
```
```    21   done
```
```    22
```
```    23 lemma (in monoid) inv_char:
```
```    24   "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
```
```    25   apply (subgoal_tac "x \<in> Units G")
```
```    26    apply (subgoal_tac "y = inv x \<otimes> \<one>")
```
```    27     apply simp
```
```    28    apply (erule subst)
```
```    29    apply (subst m_assoc [symmetric])
```
```    30       apply auto
```
```    31   apply (unfold Units_def)
```
```    32   apply auto
```
```    33   done
```
```    34
```
```    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"
```
```    36   apply (rule inv_char)
```
```    37      apply auto
```
```    38   apply (subst m_comm, auto)
```
```    39   done
```
```    40
```
```    41 lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
```
```    42   apply (rule inv_char)
```
```    43      apply (auto simp add: l_minus r_minus)
```
```    44   done
```
```    45
```
```    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"
```
```    47   apply (subgoal_tac "inv (inv x) = inv (inv y)")
```
```    48    apply (subst (asm) Units_inv_inv)+
```
```    49     apply auto
```
```    50   done
```
```    51
```
```    52 lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
```
```    53   apply (unfold Units_def)
```
```    54   apply auto
```
```    55   apply (rule_tac x = "\<ominus> \<one>" in bexI)
```
```    56    apply auto
```
```    57   apply (simp add: l_minus r_minus)
```
```    58   done
```
```    59
```
```    60 lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
```
```    61   apply (rule inv_char)
```
```    62      apply auto
```
```    63   done
```
```    64
```
```    65 lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
```
```    66   apply auto
```
```    67   apply (subst Units_inv_inv [symmetric])
```
```    68    apply auto
```
```    69   done
```
```    70
```
```    71 lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
```
```    72   by (metis Units_inv_inv inv_one)
```
```    73
```
```    74 end
```