src/HOL/Algebra/More_Ring.thy
 changeset 68445 c183a6a69f2d parent 68444 ff61cbfb3f2d child 68446 92ddca1edc43
```     1.1 --- a/src/HOL/Algebra/More_Ring.thy	Tue Jun 12 16:09:12 2018 +0100
1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,74 +0,0 @@
1.4 -(*  Title:      HOL/Algebra/More_Ring.thy
1.5 -    Author:     Jeremy Avigad
1.6 -*)
1.7 -
1.8 -section \<open>More on rings etc.\<close>
1.9 -
1.10 -theory More_Ring
1.11 -  imports Ring
1.12 -begin
1.13 -
1.14 -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"
1.15 -  apply (unfold_locales)
1.16 -    apply (use cring_axioms in auto)
1.17 -   apply (rule trans)
1.18 -    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
1.19 -     apply assumption
1.20 -    apply (subst m_assoc)
1.21 -       apply auto
1.22 -  apply (unfold Units_def)
1.23 -  apply auto
1.24 -  done
1.25 -
1.26 -lemma (in monoid) inv_char:
1.27 -  "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
1.28 -  apply (subgoal_tac "x \<in> Units G")
1.29 -   apply (subgoal_tac "y = inv x \<otimes> \<one>")
1.30 -    apply simp
1.31 -   apply (erule subst)
1.32 -   apply (subst m_assoc [symmetric])
1.33 -      apply auto
1.34 -  apply (unfold Units_def)
1.35 -  apply auto
1.36 -  done
1.37 -
1.38 -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"
1.39 -  apply (rule inv_char)
1.40 -     apply auto
1.41 -  apply (subst m_comm, auto)
1.42 -  done
1.43 -
1.44 -lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
1.45 -  apply (rule inv_char)
1.46 -     apply (auto simp add: l_minus r_minus)
1.47 -  done
1.48 -
1.49 -lemma (in monoid) inv_eq_imp_eq: "x \<in> Units G \<Longrightarrow> y \<in> Units G \<Longrightarrow> inv x = inv y \<Longrightarrow> x = y"
1.50 -  apply (subgoal_tac "inv (inv x) = inv (inv y)")
1.51 -   apply (subst (asm) Units_inv_inv)+
1.52 -    apply auto
1.53 -  done
1.54 -
1.55 -lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
1.56 -  apply (unfold Units_def)
1.57 -  apply auto
1.58 -  apply (rule_tac x = "\<ominus> \<one>" in bexI)
1.59 -   apply auto
1.60 -  apply (simp add: l_minus r_minus)
1.61 -  done
1.62 -
1.63 -lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
1.64 -  apply (rule inv_char)
1.65 -     apply auto
1.66 -  done
1.67 -
1.68 -lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
1.69 -  apply auto
1.70 -  apply (subst Units_inv_inv [symmetric])
1.71 -   apply auto
1.72 -  done
1.73 -
1.74 -lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
1.75 -  by (metis Units_inv_inv inv_one)
1.76 -
1.77 -end
```