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