misc tuning and modernization;
authorwenzelm
Mon Oct 02 22:48:01 2017 +0200 (18 months ago)
changeset 66760d44ea023ac09
parent 66759 918f15c9367a
child 66761 808e6ddb5a50
misc tuning and modernization;
src/HOL/Algebra/More_Finite_Product.thy
src/HOL/Algebra/More_Group.thy
src/HOL/Algebra/More_Ring.thy
     1.1 --- a/src/HOL/Algebra/More_Finite_Product.thy	Mon Oct 02 19:58:29 2017 +0200
     1.2 +++ b/src/HOL/Algebra/More_Finite_Product.thy	Mon Oct 02 22:48:01 2017 +0200
     1.3 @@ -5,71 +5,69 @@
     1.4  section \<open>More on finite products\<close>
     1.5  
     1.6  theory More_Finite_Product
     1.7 -imports
     1.8 -  More_Group
     1.9 +  imports More_Group
    1.10  begin
    1.11  
    1.12  lemma (in comm_monoid) finprod_UN_disjoint:
    1.13 -  "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
    1.14 -     (A i) Int (A j) = {}) \<longrightarrow>
    1.15 -      (ALL i:I. ALL x: (A i). g x : carrier G) \<longrightarrow>
    1.16 -        finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I"
    1.17 +  "finite I \<Longrightarrow> (\<forall>i\<in>I. finite (A i)) \<longrightarrow> (\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}) \<longrightarrow>
    1.18 +    (\<forall>i\<in>I. \<forall>x \<in> A i. g x \<in> carrier G) \<longrightarrow>
    1.19 +    finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
    1.20    apply (induct set: finite)
    1.21 -  apply force
    1.22 +   apply force
    1.23    apply clarsimp
    1.24    apply (subst finprod_Un_disjoint)
    1.25 -  apply blast
    1.26 -  apply (erule finite_UN_I)
    1.27 -  apply blast
    1.28 -  apply (fastforce)
    1.29 -  apply (auto intro!: funcsetI finprod_closed)
    1.30 +       apply blast
    1.31 +      apply (erule finite_UN_I)
    1.32 +      apply blast
    1.33 +     apply (fastforce)
    1.34 +    apply (auto intro!: funcsetI finprod_closed)
    1.35    done
    1.36  
    1.37  lemma (in comm_monoid) finprod_Union_disjoint:
    1.38 -  "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
    1.39 -      (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
    1.40 -   ==> finprod G f (\<Union>C) = finprod G (finprod G f) C"
    1.41 +  "finite C \<Longrightarrow>
    1.42 +    \<forall>A\<in>C. finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G) \<Longrightarrow>
    1.43 +    \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
    1.44 +    finprod G f (\<Union>C) = finprod G (finprod G f) C"
    1.45    apply (frule finprod_UN_disjoint [of C id f])
    1.46    apply auto
    1.47    done
    1.48  
    1.49 -lemma (in comm_monoid) finprod_one:
    1.50 -    "finite A \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
    1.51 +lemma (in comm_monoid) finprod_one: "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
    1.52    by (induct set: finite) auto
    1.53  
    1.54  
    1.55  (* need better simplification rules for rings *)
    1.56  (* the next one holds more generally for abelian groups *)
    1.57  
    1.58 -lemma (in cring) sum_zero_eq_neg: "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
    1.59 +lemma (in cring) sum_zero_eq_neg: "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
    1.60    by (metis minus_equality)
    1.61  
    1.62  lemma (in domain) square_eq_one:
    1.63    fixes x
    1.64 -  assumes [simp]: "x : carrier R"
    1.65 +  assumes [simp]: "x \<in> carrier R"
    1.66      and "x \<otimes> x = \<one>"
    1.67 -  shows "x = \<one> | x = \<ominus>\<one>"
    1.68 +  shows "x = \<one> \<or> x = \<ominus>\<one>"
    1.69  proof -
    1.70    have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
    1.71      by (simp add: ring_simprules)
    1.72    also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
    1.73      by (simp add: ring_simprules)
    1.74    finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
    1.75 -  then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
    1.76 -    by (intro integral, auto)
    1.77 +  then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>"
    1.78 +    by (intro integral) auto
    1.79    then show ?thesis
    1.80      apply auto
    1.81 -    apply (erule notE)
    1.82 -    apply (rule sum_zero_eq_neg)
    1.83 -    apply auto
    1.84 +     apply (erule notE)
    1.85 +     apply (rule sum_zero_eq_neg)
    1.86 +       apply auto
    1.87      apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
    1.88 -    apply (simp add: ring_simprules)
    1.89 +     apply (simp add: ring_simprules)
    1.90      apply (rule sum_zero_eq_neg)
    1.91 -    apply auto
    1.92 +      apply auto
    1.93      done
    1.94  qed
    1.95  
    1.96 -lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
    1.97 +lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
    1.98    by (metis Units_closed Units_l_inv square_eq_one)
    1.99  
   1.100  
   1.101 @@ -90,15 +88,15 @@
   1.102      monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
   1.103    done
   1.104  
   1.105 -lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
   1.106 -    \<Longrightarrow> a (^) card(Units R) = \<one>"
   1.107 +lemma (in cring) units_power_order_eq_one:
   1.108 +  "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a (^) card(Units R) = \<one>"
   1.109    apply (subst units_of_carrier [symmetric])
   1.110    apply (subst units_of_one [symmetric])
   1.111    apply (subst units_of_pow [symmetric])
   1.112 -  apply assumption
   1.113 +   apply assumption
   1.114    apply (rule comm_group.power_order_eq_one)
   1.115 -  apply (rule units_comm_group)
   1.116 -  apply (unfold units_of_def, auto)
   1.117 +    apply (rule units_comm_group)
   1.118 +   apply (unfold units_of_def, auto)
   1.119    done
   1.120  
   1.121 -end
   1.122 \ No newline at end of file
   1.123 +end
     2.1 --- a/src/HOL/Algebra/More_Group.thy	Mon Oct 02 19:58:29 2017 +0200
     2.2 +++ b/src/HOL/Algebra/More_Group.thy	Mon Oct 02 22:48:01 2017 +0200
     2.3 @@ -5,8 +5,7 @@
     2.4  section \<open>More on groups\<close>
     2.5  
     2.6  theory More_Group
     2.7 -imports
     2.8 -  Ring
     2.9 +  imports Ring
    2.10  begin
    2.11  
    2.12  text \<open>
    2.13 @@ -16,63 +15,62 @@
    2.14    facts about the unit group within the ring locale.
    2.15  \<close>
    2.16  
    2.17 -definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
    2.18 -  "units_of G == (| carrier = Units G,
    2.19 -     Group.monoid.mult = Group.monoid.mult G,
    2.20 -     one  = one G |)"
    2.21 +definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
    2.22 +  where "units_of G =
    2.23 +    \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
    2.24  
    2.25 -lemma (in monoid) units_group: "group(units_of G)"
    2.26 +lemma (in monoid) units_group: "group (units_of G)"
    2.27    apply (unfold units_of_def)
    2.28    apply (rule groupI)
    2.29 -  apply auto
    2.30 -  apply (subst m_assoc)
    2.31 -  apply auto
    2.32 +      apply auto
    2.33 +   apply (subst m_assoc)
    2.34 +      apply auto
    2.35    apply (rule_tac x = "inv x" in bexI)
    2.36 -  apply auto
    2.37 +   apply auto
    2.38    done
    2.39  
    2.40 -lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
    2.41 +lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
    2.42    apply (rule group.group_comm_groupI)
    2.43 -  apply (rule units_group)
    2.44 +   apply (rule units_group)
    2.45    apply (insert comm_monoid_axioms)
    2.46    apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
    2.47    apply auto
    2.48    done
    2.49  
    2.50  lemma units_of_carrier: "carrier (units_of G) = Units G"
    2.51 -  unfolding units_of_def by auto
    2.52 +  by (auto simp: units_of_def)
    2.53  
    2.54 -lemma units_of_mult: "mult(units_of G) = mult G"
    2.55 -  unfolding units_of_def by auto
    2.56 +lemma units_of_mult: "mult (units_of G) = mult G"
    2.57 +  by (auto simp: units_of_def)
    2.58  
    2.59 -lemma units_of_one: "one(units_of G) = one G"
    2.60 -  unfolding units_of_def by auto
    2.61 +lemma units_of_one: "one (units_of G) = one G"
    2.62 +  by (auto simp: units_of_def)
    2.63  
    2.64 -lemma (in monoid) units_of_inv: "x : Units G ==> m_inv (units_of G) x = m_inv G x"
    2.65 +lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
    2.66    apply (rule sym)
    2.67    apply (subst m_inv_def)
    2.68    apply (rule the1_equality)
    2.69 -  apply (rule ex_ex1I)
    2.70 -  apply (subst (asm) Units_def)
    2.71 -  apply auto
    2.72 -  apply (erule inv_unique)
    2.73 -  apply auto
    2.74 -  apply (rule Units_closed)
    2.75 -  apply (simp_all only: units_of_carrier [symmetric])
    2.76 -  apply (insert units_group)
    2.77 -  apply auto
    2.78 -  apply (subst units_of_mult [symmetric])
    2.79 -  apply (subst units_of_one [symmetric])
    2.80 -  apply (erule group.r_inv, assumption)
    2.81 +   apply (rule ex_ex1I)
    2.82 +    apply (subst (asm) Units_def)
    2.83 +    apply auto
    2.84 +     apply (erule inv_unique)
    2.85 +        apply auto
    2.86 +    apply (rule Units_closed)
    2.87 +    apply (simp_all only: units_of_carrier [symmetric])
    2.88 +    apply (insert units_group)
    2.89 +    apply auto
    2.90 +   apply (subst units_of_mult [symmetric])
    2.91 +   apply (subst units_of_one [symmetric])
    2.92 +   apply (erule group.r_inv, assumption)
    2.93    apply (subst units_of_mult [symmetric])
    2.94    apply (subst units_of_one [symmetric])
    2.95    apply (erule group.l_inv, assumption)
    2.96    done
    2.97  
    2.98 -lemma (in group) inj_on_const_mult: "a: (carrier G) ==> inj_on (%x. a \<otimes> x) (carrier G)"
    2.99 +lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
   2.100    unfolding inj_on_def by auto
   2.101  
   2.102 -lemma (in group) surj_const_mult: "a : (carrier G) ==> (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
   2.103 +lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
   2.104    apply (auto simp add: image_def)
   2.105    apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
   2.106    apply auto
   2.107 @@ -82,33 +80,29 @@
   2.108    apply auto
   2.109    done
   2.110  
   2.111 -lemma (in group) l_cancel_one [simp]:
   2.112 -    "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> (x \<otimes> a = x) = (a = one G)"
   2.113 +lemma (in group) l_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> a = one G"
   2.114    apply auto
   2.115    apply (subst l_cancel [symmetric])
   2.116 -  prefer 4
   2.117 -  apply (erule ssubst)
   2.118 -  apply auto
   2.119 +     prefer 4
   2.120 +     apply (erule ssubst)
   2.121 +     apply auto
   2.122    done
   2.123  
   2.124 -lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   2.125 -    (a \<otimes> x = x) = (a = one G)"
   2.126 +lemma (in group) r_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> a \<otimes> x = x \<longleftrightarrow> a = one G"
   2.127    apply auto
   2.128    apply (subst r_cancel [symmetric])
   2.129 -  prefer 4
   2.130 -  apply (erule ssubst)
   2.131 -  apply auto
   2.132 +     prefer 4
   2.133 +     apply (erule ssubst)
   2.134 +     apply auto
   2.135    done
   2.136  
   2.137  (* Is there a better way to do this? *)
   2.138 -lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   2.139 -    (x = x \<otimes> a) = (a = one G)"
   2.140 +lemma (in group) l_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = x \<otimes> a \<longleftrightarrow> a = one G"
   2.141    apply (subst eq_commute)
   2.142    apply simp
   2.143    done
   2.144  
   2.145 -lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   2.146 -    (x = a \<otimes> x) = (a = one G)"
   2.147 +lemma (in group) r_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> a = one G"
   2.148    apply (subst eq_commute)
   2.149    apply simp
   2.150    done
   2.151 @@ -118,7 +112,7 @@
   2.152  
   2.153  lemma (in comm_group) power_order_eq_one:
   2.154    assumes fin [simp]: "finite (carrier G)"
   2.155 -    and a [simp]: "a : carrier G"
   2.156 +    and a [simp]: "a \<in> carrier G"
   2.157    shows "a (^) card(carrier G) = one G"
   2.158  proof -
   2.159    have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
     3.1 --- a/src/HOL/Algebra/More_Ring.thy	Mon Oct 02 19:58:29 2017 +0200
     3.2 +++ b/src/HOL/Algebra/More_Ring.thy	Mon Oct 02 22:48:01 2017 +0200
     3.3 @@ -5,73 +5,70 @@
     3.4  section \<open>More on rings etc.\<close>
     3.5  
     3.6  theory More_Ring
     3.7 -imports
     3.8 -  Ring
     3.9 +  imports Ring
    3.10  begin
    3.11  
    3.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"
    3.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"
    3.14    apply (unfold_locales)
    3.15 -  apply (insert cring_axioms, auto)
    3.16 -  apply (rule trans)
    3.17 -  apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
    3.18 -  apply assumption
    3.19 -  apply (subst m_assoc)
    3.20 -  apply auto
    3.21 +    apply (use cring_axioms in auto)
    3.22 +   apply (rule trans)
    3.23 +    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
    3.24 +     apply assumption
    3.25 +    apply (subst m_assoc)
    3.26 +       apply auto
    3.27    apply (unfold Units_def)
    3.28    apply auto
    3.29    done
    3.30  
    3.31 -lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
    3.32 -    x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
    3.33 -  apply (subgoal_tac "x : Units G")
    3.34 -  apply (subgoal_tac "y = inv x \<otimes> \<one>")
    3.35 -  apply simp
    3.36 -  apply (erule subst)
    3.37 -  apply (subst m_assoc [symmetric])
    3.38 -  apply auto
    3.39 +lemma (in monoid) inv_char:
    3.40 +  "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
    3.41 +  apply (subgoal_tac "x \<in> Units G")
    3.42 +   apply (subgoal_tac "y = inv x \<otimes> \<one>")
    3.43 +    apply simp
    3.44 +   apply (erule subst)
    3.45 +   apply (subst m_assoc [symmetric])
    3.46 +      apply auto
    3.47    apply (unfold Units_def)
    3.48    apply auto
    3.49    done
    3.50  
    3.51 -lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
    3.52 -  x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
    3.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"
    3.54    apply (rule inv_char)
    3.55 -  apply auto
    3.56 +     apply auto
    3.57    apply (subst m_comm, auto)
    3.58    done
    3.59  
    3.60  lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
    3.61    apply (rule inv_char)
    3.62 -  apply (auto simp add: l_minus r_minus)
    3.63 +     apply (auto simp add: l_minus r_minus)
    3.64    done
    3.65  
    3.66 -lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
    3.67 -    inv x = inv y \<Longrightarrow> x = y"
    3.68 -  apply (subgoal_tac "inv(inv x) = inv(inv y)")
    3.69 -  apply (subst (asm) Units_inv_inv)+
    3.70 -  apply auto
    3.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"
    3.72 +  apply (subgoal_tac "inv (inv x) = inv (inv y)")
    3.73 +   apply (subst (asm) Units_inv_inv)+
    3.74 +    apply auto
    3.75    done
    3.76  
    3.77 -lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
    3.78 +lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
    3.79    apply (unfold Units_def)
    3.80    apply auto
    3.81    apply (rule_tac x = "\<ominus> \<one>" in bexI)
    3.82 -  apply auto
    3.83 +   apply auto
    3.84    apply (simp add: l_minus r_minus)
    3.85    done
    3.86  
    3.87  lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
    3.88    apply (rule inv_char)
    3.89 -  apply auto
    3.90 +     apply auto
    3.91    done
    3.92  
    3.93 -lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
    3.94 +lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
    3.95    apply auto
    3.96    apply (subst Units_inv_inv [symmetric])
    3.97 -  apply auto
    3.98 +   apply auto
    3.99    done
   3.100  
   3.101 -lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
   3.102 +lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
   3.103    by (metis Units_inv_inv inv_one)
   3.104  
   3.105  end