author ballarin Thu Feb 19 16:44:21 2004 +0100 (2004-02-19) changeset 14399 dc677b35e54f parent 14398 c5c47703f763 child 14400 6069098854b9
New lemmas about inversion of restricted functions.
HOL-Algebra: new locale "ring" for non-commutative rings.
 NEWS file | annotate | diff | revisions src/HOL/Algebra/CRing.thy file | annotate | diff | revisions src/HOL/Algebra/UnivPoly.thy file | annotate | diff | revisions src/HOL/Algebra/ringsimp.ML file | annotate | diff | revisions src/HOL/Hilbert_Choice.thy file | annotate | diff | revisions
```     1.1 --- a/NEWS	Thu Feb 19 15:57:34 2004 +0100
1.2 +++ b/NEWS	Thu Feb 19 16:44:21 2004 +0100
1.3 @@ -117,6 +117,8 @@
1.4
1.5  * arith(_tac) is now able to generate counterexamples for reals as well.
1.6
1.7 +* HOL-Algebra: new locale "ring" for non-commutative rings.
1.8 +
1.9  * SET-Protocol: formalization and verification of the SET protocol suite;
1.10
1.11  * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function
```
```     2.1 --- a/src/HOL/Algebra/CRing.thy	Thu Feb 19 15:57:34 2004 +0100
2.2 +++ b/src/HOL/Algebra/CRing.thy	Thu Feb 19 16:44:21 2004 +0100
2.3 @@ -276,8 +276,8 @@
2.4      simplified monoid_record_simps])
2.5
2.6  lemma (in abelian_monoid) finsum_cong:
2.7 -  "[| A = B;
2.8 -      f : B -> carrier G = True; !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
2.9 +  "[| A = B; f : B -> carrier G = True;
2.10 +      !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
2.11    by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
2.12      simplified monoid_record_simps]) auto
2.13
2.14 @@ -289,9 +289,13 @@
2.15
2.16  subsection {* Basic Definitions *}
2.17
2.18 -locale cring = abelian_group R + comm_monoid R +
2.19 +locale ring = abelian_group R + monoid R +
2.20    assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
2.21        ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
2.22 +    and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
2.23 +      ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
2.24 +
2.25 +locale cring = ring + comm_monoid R
2.26
2.27  locale "domain" = cring +
2.28    assumes one_not_zero [simp]: "\<one> ~= \<zero>"
2.29 @@ -300,18 +304,54 @@
2.30
2.31  subsection {* Basic Facts of Rings *}
2.32
2.33 +lemma ringI:
2.34 +  includes struct R
2.35 +  assumes abelian_group: "abelian_group R"
2.36 +    and monoid: "monoid R"
2.37 +    and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
2.38 +      ==> mult R (add R x y) z = add R (mult R x z) (mult R y z)"
2.39 +    and r_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
2.40 +      ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
2.41 +  shows "ring R"
2.42 +  by (auto intro: ring.intro
2.43 +    abelian_group.axioms monoid.axioms ring_axioms.intro prems)
2.44 +
2.45 +lemma (in ring) is_abelian_group:
2.46 +  "abelian_group R"
2.47 +  by (auto intro!: abelian_groupI a_assoc a_comm l_neg)
2.48 +
2.49 +lemma (in ring) is_monoid:
2.50 +  "monoid R"
2.51 +  by (auto intro!: monoidI m_assoc)
2.52 +
2.53  lemma cringI:
2.54 +  includes struct R
2.55    assumes abelian_group: "abelian_group R"
2.56      and comm_monoid: "comm_monoid R"
2.57      and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
2.58        ==> mult R (add R x y) z = add R (mult R x z) (mult R y z)"
2.59    shows "cring R"
2.60 -  by (auto intro: cring.intro
2.61 -    abelian_group.axioms comm_monoid.axioms cring_axioms.intro prems)
2.62 -
2.63 -lemma (in cring) is_abelian_group:
2.64 -  "abelian_group R"
2.65 -  by (auto intro!: abelian_groupI a_assoc a_comm l_neg)
2.66 +  proof (rule cring.intro)
2.67 +    show "ring_axioms R"
2.68 +    -- {* Right-distributivity follows from left-distributivity and
2.69 +          commutativity. *}
2.70 +    proof (rule ring_axioms.intro)
2.71 +      fix x y z
2.72 +      assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
2.73 +      note [simp]= comm_monoid.axioms [OF comm_monoid]
2.74 +        abelian_group.axioms [OF abelian_group]
2.75 +        abelian_monoid.a_closed
2.76 +        magma.m_closed
2.77 +
2.78 +      from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
2.79 +        by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
2.80 +      also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
2.81 +      also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
2.82 +        by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
2.83 +      finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
2.84 +    qed
2.85 +  qed (auto intro: cring.intro
2.86 +      abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
2.87
2.88  lemma (in cring) is_comm_monoid:
2.89    "comm_monoid R"
2.90 @@ -338,22 +378,11 @@
2.91    with G show ?thesis by (simp add: a_ac)
2.92  qed
2.93
2.94 -lemma (in cring) r_distr:
2.95 -  "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
2.96 -  ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
2.97 -proof -
2.98 -  assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
2.99 -  then have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" by (simp add: m_comm)
2.100 -  also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
2.101 -  also from R have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
2.102 -  finally show ?thesis .
2.103 -qed
2.104 -
2.105  text {*
2.106    The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
2.107  *}
2.108
2.109 -lemma (in cring) l_null [simp]:
2.110 +lemma (in ring) l_null [simp]:
2.111    "x \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
2.112  proof -
2.113    assume R: "x \<in> carrier R"
2.114 @@ -364,16 +393,18 @@
2.115    with R show ?thesis by (simp del: r_zero)
2.116  qed
2.117
2.118 -lemma (in cring) r_null [simp]:
2.119 +lemma (in ring) r_null [simp]:
2.120    "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
2.121  proof -
2.122    assume R: "x \<in> carrier R"
2.123 -  then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: m_ac)
2.124 -  also from R have "... = \<zero>" by simp
2.125 -  finally show ?thesis .
2.126 +  then have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> (\<zero> \<oplus> \<zero>)"
2.127 +    by (simp add: r_distr del: l_zero r_zero)
2.128 +  also from R have "... = x \<otimes> \<zero> \<oplus> \<zero>" by simp
2.129 +  finally have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> \<zero> \<oplus> \<zero>" .
2.130 +  with R show ?thesis by (simp del: r_zero)
2.131  qed
2.132
2.133 -lemma (in cring) l_minus:
2.134 +lemma (in ring) l_minus:
2.135    "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
2.136  proof -
2.137    assume R: "x \<in> carrier R" "y \<in> carrier R"
2.138 @@ -384,20 +415,27 @@
2.139    with R show ?thesis by (simp add: a_assoc r_neg )
2.140  qed
2.141
2.142 -lemma (in cring) r_minus:
2.143 +lemma (in ring) r_minus:
2.144    "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
2.145  proof -
2.146    assume R: "x \<in> carrier R" "y \<in> carrier R"
2.147 -  then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: m_ac)
2.148 -  also from R have "... = \<ominus> (y \<otimes> x)" by (simp add: l_minus)
2.149 -  also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: m_ac)
2.150 -  finally show ?thesis .
2.151 +  then have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = x \<otimes> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
2.152 +  also from R have "... = \<zero>" by (simp add: l_neg r_null)
2.153 +  finally have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = \<zero>" .
2.154 +  with R have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
2.155 +  with R show ?thesis by (simp add: a_assoc r_neg )
2.156  qed
2.157
2.158 -lemma (in cring) minus_eq:
2.159 +lemma (in ring) minus_eq:
2.160    "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
2.161    by (simp only: minus_def)
2.162
2.163 +lemmas (in ring) ring_simprules =
2.164 +  a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
2.165 +  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq
2.166 +  r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
2.167 +  a_lcomm r_distr l_null r_null l_minus r_minus
2.168 +
2.169  lemmas (in cring) cring_simprules =
2.170    a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
2.171    a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq
2.172 @@ -417,7 +455,7 @@
2.173  text {* Two examples for use of method algebra *}
2.174
2.175  lemma
2.176 -  includes cring R + cring S
2.177 +  includes ring R + cring S
2.178    shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==>
2.179    a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^sub>2 d = d \<otimes>\<^sub>2 c"
2.180    by algebra
```
```     3.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Feb 19 15:57:34 2004 +0100
3.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Feb 19 16:44:21 2004 +0100
3.3 @@ -370,10 +370,14 @@
3.4    by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
3.5      UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
3.6
3.7 +lemma (in UP_cring) UP_ring:  (* preliminary *)
3.8 +  "ring P"
3.9 +  by (auto intro: ring.intro cring.axioms UP_cring)
3.10 +
3.11  lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
3.12    "p \<in> carrier P ==> \<ominus>\<^sub>2 p \<in> carrier P"
3.13    by (rule abelian_group.a_inv_closed
3.14 -    [OF cring.is_abelian_group [OF UP_cring]])
3.15 +    [OF ring.is_abelian_group [OF UP_ring]])
3.16
3.17  lemma (in UP_cring) coeff_a_inv [simp]:
3.18    assumes R: "p \<in> carrier P"
3.19 @@ -384,7 +388,7 @@
3.20      by algebra
3.21    also from R have "... =  \<ominus> (coeff P p n)"
3.23 -      abelian_group.r_neg [OF cring.is_abelian_group [OF UP_cring]])
3.24 +      abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]])
3.25    finally show ?thesis .
3.26  qed
3.27
3.28 @@ -409,11 +413,11 @@
3.29
3.30  lemma (in UP_cring) UP_abelian_monoid:
3.31    "abelian_monoid P"
3.32 -  by (fast intro!: abelian_group.axioms cring.is_abelian_group UP_cring)
3.33 +  by (fast intro!: abelian_group.axioms ring.is_abelian_group UP_ring)
3.34
3.35  lemma (in UP_cring) UP_abelian_group:
3.36    "abelian_group P"
3.37 -  by (fast intro!: cring.is_abelian_group UP_cring)
3.38 +  by (fast intro!: ring.is_abelian_group UP_ring)
3.39
3.40  lemmas (in UP_cring) UP_r_one [simp] =
3.41    monoid.r_one [OF UP_monoid]
3.42 @@ -521,19 +525,19 @@
3.43    abelian_group.r_neg1 [OF UP_abelian_group]
3.44
3.45  lemmas (in UP_cring) UP_r_distr =
3.46 -  cring.r_distr [OF UP_cring]
3.47 +  ring.r_distr [OF UP_ring]
3.48
3.49  lemmas (in UP_cring) UP_l_null [simp] =
3.50 -  cring.l_null [OF UP_cring]
3.51 +  ring.l_null [OF UP_ring]
3.52
3.53  lemmas (in UP_cring) UP_r_null [simp] =
3.54 -  cring.r_null [OF UP_cring]
3.55 +  ring.r_null [OF UP_ring]
3.56
3.57  lemmas (in UP_cring) UP_l_minus =
3.58 -  cring.l_minus [OF UP_cring]
3.59 +  ring.l_minus [OF UP_ring]
3.60
3.61  lemmas (in UP_cring) UP_r_minus =
3.62 -  cring.r_minus [OF UP_cring]
3.63 +  ring.r_minus [OF UP_ring]
3.64
3.65  lemmas (in UP_cring) UP_finsum_ldistr =
3.66    cring.finsum_ldistr [OF UP_cring]
```
```     4.1 --- a/src/HOL/Algebra/ringsimp.ML	Thu Feb 19 15:57:34 2004 +0100
4.2 +++ b/src/HOL/Algebra/ringsimp.ML	Thu Feb 19 16:44:21 2004 +0100
4.3 @@ -64,16 +64,28 @@
4.4  val cring_ss = HOL_ss settermless termless_ring;
4.5
4.6  fun cring_normalise ctxt = let
4.7 -    fun filter t = (case HOLogic.dest_Trueprop t of
4.8 -        Const ("CRing.cring_axioms", _) \$ Free (s, _) => [s]
4.9 +    fun ring_filter t = (case HOLogic.dest_Trueprop t of
4.10 +        Const ("CRing.ring_axioms", _) \$ Free (s, _) => [s]
4.11 +      | _ => [])
4.12 +      handle TERM _ => [];
4.13 +    fun comm_filter t = (case HOLogic.dest_Trueprop t of
4.14 +        Const ("Group.comm_semigroup_axioms", _) \$ Free (s, _) => [s]
4.15        | _ => [])
4.16        handle TERM _ => [];
4.17 -    val insts = flat (map (filter o #prop o rep_thm)
4.18 -      (ProofContext.prems_of ctxt));
4.19 -val _ = warning ("Rings in proof context: " ^ implode insts);
4.20 +
4.21 +    val prems = ProofContext.prems_of ctxt;
4.22 +    val rings = flat (map (ring_filter o #prop o rep_thm) prems);
4.23 +    val comms = flat (map (comm_filter o #prop o rep_thm) prems);
4.24 +    val non_comm_rings = rings \\ comms;
4.25 +    val comm_rings = rings inter_string comms;
4.26 +    val _ = tracing
4.27 +      ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^
4.28 +       "\nCommutative rings in proof context: " ^ commas comm_rings);
4.29      val simps =
4.30 +      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules"))
4.31 +        non_comm_rings) @
4.32        flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules"))
4.33 -        insts);
4.34 +        comm_rings);
4.36    end;
4.37
```
```     5.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Feb 19 15:57:34 2004 +0100
5.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Feb 19 16:44:21 2004 +0100
5.3 @@ -51,6 +51,23 @@
5.4  apply (fast intro: someI2)
5.5  done
5.6
5.7 +lemma Inv_f_eq:
5.8 +  "[| inj_on f A; f x = y; x : A |] ==> Inv A f y = x"
5.9 +  apply (erule subst)
5.10 +  apply (erule Inv_f_f)
5.11 +  apply assumption
5.12 +  done
5.13 +
5.14 +lemma Inv_comp:
5.15 +  "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
5.16 +  Inv A (f o g) x = (Inv A g o Inv (g ` A) f) x"
5.17 +  apply simp
5.18 +  apply (rule Inv_f_eq)
5.19 +    apply (fast intro: comp_inj_on)
5.20 +   apply (simp add: f_Inv_f Inv_mem)
5.21 +  apply (simp add: Inv_mem)
5.22 +  done
5.23 +
5.24  lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
5.25    -- {* dynamically-scoped fact for TFL *}
5.26    by (blast intro: someI)
```