src/HOL/Number_Theory/MiscAlgebra.thy
changeset 41541 1fa4725c4656
parent 35416 d8d7d1b785af
child 41959 b460124855b8
     1.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Thu Jan 13 21:50:13 2011 +0100
     1.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Thu Jan 13 23:50:16 2011 +0100
     1.3 @@ -69,10 +69,10 @@
     1.4  lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
     1.5    apply (rule group.group_comm_groupI)
     1.6    apply (rule units_group)
     1.7 -  apply (insert prems)
     1.8 +  apply (insert comm_monoid_axioms)
     1.9    apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
    1.10 -  apply auto;
    1.11 -done;
    1.12 +  apply auto
    1.13 +  done
    1.14  
    1.15  lemma units_of_carrier: "carrier (units_of G) = Units G"
    1.16    by (unfold units_of_def, auto)
    1.17 @@ -174,18 +174,18 @@
    1.18  lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}.
    1.19      x : Units R \<Longrightarrow> field R"
    1.20    apply (unfold_locales)
    1.21 -  apply (insert prems, auto)
    1.22 +  apply (insert cring_axioms, auto)
    1.23    apply (rule trans)
    1.24    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
    1.25    apply assumption
    1.26    apply (subst m_assoc) 
    1.27 -  apply (auto simp add: Units_r_inv)
    1.28 +  apply auto
    1.29    apply (unfold Units_def)
    1.30    apply auto
    1.31 -done
    1.32 +  done
    1.33  
    1.34  lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
    1.35 -  x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
    1.36 +    x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
    1.37    apply (subgoal_tac "x : Units G")
    1.38    apply (subgoal_tac "y = inv x \<otimes> \<one>")
    1.39    apply simp
    1.40 @@ -194,19 +194,19 @@
    1.41    apply auto
    1.42    apply (unfold Units_def)
    1.43    apply auto
    1.44 -done
    1.45 +  done
    1.46  
    1.47  lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
    1.48    x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
    1.49    apply (rule inv_char)
    1.50    apply auto
    1.51    apply (subst m_comm, auto) 
    1.52 -done
    1.53 +  done
    1.54  
    1.55  lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"  
    1.56    apply (rule inv_char)
    1.57    apply (auto simp add: l_minus r_minus)
    1.58 -done
    1.59 +  done
    1.60  
    1.61  lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow> 
    1.62      inv x = inv y \<Longrightarrow> x = y"
    1.63 @@ -281,8 +281,8 @@
    1.64    apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y") 
    1.65    apply (erule ssubst)back
    1.66    apply (erule subst)
    1.67 -  apply (simp add: ring_simprules)+
    1.68 -done
    1.69 +  apply (simp_all add: ring_simprules)
    1.70 +  done
    1.71  
    1.72  (* there's a name conflict -- maybe "domain" should be
    1.73     "integral_domain" *)
    1.74 @@ -336,9 +336,8 @@
    1.75      "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
    1.76    apply (induct n)
    1.77    apply (auto simp add: units_group group.is_monoid  
    1.78 -    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult
    1.79 -    One_nat_def)
    1.80 -done
    1.81 +    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
    1.82 +  done
    1.83  
    1.84  lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
    1.85      \<Longrightarrow> a (^) card(Units R) = \<one>"
    1.86 @@ -349,6 +348,6 @@
    1.87    apply (rule comm_group.power_order_eq_one)
    1.88    apply (rule units_comm_group)
    1.89    apply (unfold units_of_def, auto)
    1.90 -done
    1.91 +  done
    1.92  
    1.93  end