src/HOL/Algebra/More_Ring.thy
 changeset 66760 d44ea023ac09 parent 65435 378175f44328
```     1.1 --- a/src/HOL/Algebra/More_Ring.thy	Mon Oct 02 19:58:29 2017 +0200
1.2 +++ b/src/HOL/Algebra/More_Ring.thy	Mon Oct 02 22:48:01 2017 +0200
1.3 @@ -5,73 +5,70 @@
1.4  section \<open>More on rings etc.\<close>
1.5
1.6  theory More_Ring
1.7 -imports
1.8 -  Ring
1.9 +  imports Ring
1.10  begin
1.11
1.12 -lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
1.13 +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.14    apply (unfold_locales)
1.15 -  apply (insert cring_axioms, auto)
1.16 -  apply (rule trans)
1.17 -  apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
1.18 -  apply assumption
1.19 -  apply (subst m_assoc)
1.20 -  apply auto
1.21 +    apply (use cring_axioms in auto)
1.22 +   apply (rule trans)
1.23 +    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
1.24 +     apply assumption
1.25 +    apply (subst m_assoc)
1.26 +       apply auto
1.27    apply (unfold Units_def)
1.28    apply auto
1.29    done
1.30
1.31 -lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
1.32 -    x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
1.33 -  apply (subgoal_tac "x : Units G")
1.34 -  apply (subgoal_tac "y = inv x \<otimes> \<one>")
1.35 -  apply simp
1.36 -  apply (erule subst)
1.37 -  apply (subst m_assoc [symmetric])
1.38 -  apply auto
1.39 +lemma (in monoid) inv_char:
1.40 +  "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
1.41 +  apply (subgoal_tac "x \<in> Units G")
1.42 +   apply (subgoal_tac "y = inv x \<otimes> \<one>")
1.43 +    apply simp
1.44 +   apply (erule subst)
1.45 +   apply (subst m_assoc [symmetric])
1.46 +      apply auto
1.47    apply (unfold Units_def)
1.48    apply auto
1.49    done
1.50
1.51 -lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
1.52 -  x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
1.53 +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.54    apply (rule inv_char)
1.55 -  apply auto
1.56 +     apply auto
1.57    apply (subst m_comm, auto)
1.58    done
1.59
1.60  lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
1.61    apply (rule inv_char)
1.62 -  apply (auto simp add: l_minus r_minus)
1.63 +     apply (auto simp add: l_minus r_minus)
1.64    done
1.65
1.66 -lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
1.67 -    inv x = inv y \<Longrightarrow> x = y"
1.68 -  apply (subgoal_tac "inv(inv x) = inv(inv y)")
1.69 -  apply (subst (asm) Units_inv_inv)+
1.70 -  apply auto
1.71 +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.72 +  apply (subgoal_tac "inv (inv x) = inv (inv y)")
1.73 +   apply (subst (asm) Units_inv_inv)+
1.74 +    apply auto
1.75    done
1.76
1.77 -lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
1.78 +lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
1.79    apply (unfold Units_def)
1.80    apply auto
1.81    apply (rule_tac x = "\<ominus> \<one>" in bexI)
1.82 -  apply auto
1.83 +   apply auto
1.84    apply (simp add: l_minus r_minus)
1.85    done
1.86
1.87  lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
1.88    apply (rule inv_char)
1.89 -  apply auto
1.90 +     apply auto
1.91    done
1.92
1.93 -lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
1.94 +lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
1.95    apply auto
1.96    apply (subst Units_inv_inv [symmetric])
1.97 -  apply auto
1.98 +   apply auto
1.99    done
1.100
1.101 -lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
1.102 +lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
1.103    by (metis Units_inv_inv inv_one)
1.104
1.105  end
```