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