# HG changeset patch # User ballarin # Date 1077205461 -3600 # Node ID dc677b35e54fc3dc6d5ead4da0be7c495fbd7848 # Parent c5c47703f763b1bc8f0041ba9c5067833dd52eea New lemmas about inversion of restricted functions. HOL-Algebra: new locale "ring" for non-commutative rings. diff -r c5c47703f763 -r dc677b35e54f NEWS --- a/NEWS Thu Feb 19 15:57:34 2004 +0100 +++ b/NEWS Thu Feb 19 16:44:21 2004 +0100 @@ -117,6 +117,8 @@ * arith(_tac) is now able to generate counterexamples for reals as well. +* HOL-Algebra: new locale "ring" for non-commutative rings. + * SET-Protocol: formalization and verification of the SET protocol suite; * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function diff -r c5c47703f763 -r dc677b35e54f src/HOL/Algebra/CRing.thy --- a/src/HOL/Algebra/CRing.thy Thu Feb 19 15:57:34 2004 +0100 +++ b/src/HOL/Algebra/CRing.thy Thu Feb 19 16:44:21 2004 +0100 @@ -276,8 +276,8 @@ simplified monoid_record_simps]) lemma (in abelian_monoid) finsum_cong: - "[| A = B; - f : B -> carrier G = True; !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B" + "[| A = B; f : B -> carrier G = True; + !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B" by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def, simplified monoid_record_simps]) auto @@ -289,9 +289,13 @@ subsection {* Basic Definitions *} -locale cring = abelian_group R + comm_monoid R + +locale ring = abelian_group R + monoid R + assumes l_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] ==> (x \ y) \ z = x \ z \ y \ z" + and r_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] + ==> z \ (x \ y) = z \ x \ z \ y" + +locale cring = ring + comm_monoid R locale "domain" = cring + assumes one_not_zero [simp]: "\ ~= \" @@ -300,18 +304,54 @@ subsection {* Basic Facts of Rings *} +lemma ringI: + includes struct R + assumes abelian_group: "abelian_group R" + and monoid: "monoid R" + and l_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] + ==> mult R (add R x y) z = add R (mult R x z) (mult R y z)" + and r_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] + ==> z \ (x \ y) = z \ x \ z \ y" + shows "ring R" + by (auto intro: ring.intro + abelian_group.axioms monoid.axioms ring_axioms.intro prems) + +lemma (in ring) is_abelian_group: + "abelian_group R" + by (auto intro!: abelian_groupI a_assoc a_comm l_neg) + +lemma (in ring) is_monoid: + "monoid R" + by (auto intro!: monoidI m_assoc) + lemma cringI: + includes struct R assumes abelian_group: "abelian_group R" and comm_monoid: "comm_monoid R" and l_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] ==> mult R (add R x y) z = add R (mult R x z) (mult R y z)" shows "cring R" - by (auto intro: cring.intro - abelian_group.axioms comm_monoid.axioms cring_axioms.intro prems) - -lemma (in cring) is_abelian_group: - "abelian_group R" - by (auto intro!: abelian_groupI a_assoc a_comm l_neg) + proof (rule cring.intro) + show "ring_axioms R" + -- {* Right-distributivity follows from left-distributivity and + commutativity. *} + proof (rule ring_axioms.intro) + fix x y z + assume R: "x \ carrier R" "y \ carrier R" "z \ carrier R" + note [simp]= comm_monoid.axioms [OF comm_monoid] + abelian_group.axioms [OF abelian_group] + abelian_monoid.a_closed + magma.m_closed + + from R have "z \ (x \ y) = (x \ y) \ z" + by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro]) + also from R have "... = x \ z \ y \ z" by (simp add: l_distr) + also from R have "... = z \ x \ z \ y" + by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro]) + finally show "z \ (x \ y) = z \ x \ z \ y" . + qed + qed (auto intro: cring.intro + abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems) lemma (in cring) is_comm_monoid: "comm_monoid R" @@ -338,22 +378,11 @@ with G show ?thesis by (simp add: a_ac) qed -lemma (in cring) r_distr: - "[| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> z \ (x \ y) = z \ x \ z \ y" -proof - - assume R: "x \ carrier R" "y \ carrier R" "z \ carrier R" - then have "z \ (x \ y) = (x \ y) \ z" by (simp add: m_comm) - also from R have "... = x \ z \ y \ z" by (simp add: l_distr) - also from R have "... = z \ x \ z \ y" by (simp add: m_comm) - finally show ?thesis . -qed - text {* The following proofs are from Jacobson, Basic Algebra I, pp.~88--89 *} -lemma (in cring) l_null [simp]: +lemma (in ring) l_null [simp]: "x \ carrier R ==> \ \ x = \" proof - assume R: "x \ carrier R" @@ -364,16 +393,18 @@ with R show ?thesis by (simp del: r_zero) qed -lemma (in cring) r_null [simp]: +lemma (in ring) r_null [simp]: "x \ carrier R ==> x \ \ = \" proof - assume R: "x \ carrier R" - then have "x \ \ = \ \ x" by (simp add: m_ac) - also from R have "... = \" by simp - finally show ?thesis . + then have "x \ \ \ x \ \ = x \ (\ \ \)" + by (simp add: r_distr del: l_zero r_zero) + also from R have "... = x \ \ \ \" by simp + finally have "x \ \ \ x \ \ = x \ \ \ \" . + with R show ?thesis by (simp del: r_zero) qed -lemma (in cring) l_minus: +lemma (in ring) l_minus: "[| x \ carrier R; y \ carrier R |] ==> \ x \ y = \ (x \ y)" proof - assume R: "x \ carrier R" "y \ carrier R" @@ -384,20 +415,27 @@ with R show ?thesis by (simp add: a_assoc r_neg ) qed -lemma (in cring) r_minus: +lemma (in ring) r_minus: "[| x \ carrier R; y \ carrier R |] ==> x \ \ y = \ (x \ y)" proof - assume R: "x \ carrier R" "y \ carrier R" - then have "x \ \ y = \ y \ x" by (simp add: m_ac) - also from R have "... = \ (y \ x)" by (simp add: l_minus) - also from R have "... = \ (x \ y)" by (simp add: m_ac) - finally show ?thesis . + then have "x \ (\ y) \ x \ y = x \ (\ y \ y)" by (simp add: r_distr) + also from R have "... = \" by (simp add: l_neg r_null) + finally have "x \ (\ y) \ x \ y = \" . + with R have "x \ (\ y) \ x \ y \ \ (x \ y) = \ \ \ (x \ y)" by simp + with R show ?thesis by (simp add: a_assoc r_neg ) qed -lemma (in cring) minus_eq: +lemma (in ring) minus_eq: "[| x \ carrier R; y \ carrier R |] ==> x \ y = x \ \ y" by (simp only: minus_def) +lemmas (in ring) ring_simprules = + a_closed zero_closed a_inv_closed minus_closed m_closed one_closed + a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq + r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero + a_lcomm r_distr l_null r_null l_minus r_minus + lemmas (in cring) cring_simprules = a_closed zero_closed a_inv_closed minus_closed m_closed one_closed a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq @@ -417,7 +455,7 @@ text {* Two examples for use of method algebra *} lemma - includes cring R + cring S + includes ring R + cring S shows "[| a \ carrier R; b \ carrier R; c \ carrier S; d \ carrier S |] ==> a \ \ (a \ \ b) = b & c \\<^sub>2 d = d \\<^sub>2 c" by algebra diff -r c5c47703f763 -r dc677b35e54f src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Thu Feb 19 15:57:34 2004 +0100 +++ b/src/HOL/Algebra/UnivPoly.thy Thu Feb 19 16:44:21 2004 +0100 @@ -370,10 +370,14 @@ by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr) +lemma (in UP_cring) UP_ring: (* preliminary *) + "ring P" + by (auto intro: ring.intro cring.axioms UP_cring) + lemma (in UP_cring) UP_a_inv_closed [intro, simp]: "p \ carrier P ==> \\<^sub>2 p \ carrier P" by (rule abelian_group.a_inv_closed - [OF cring.is_abelian_group [OF UP_cring]]) + [OF ring.is_abelian_group [OF UP_ring]]) lemma (in UP_cring) coeff_a_inv [simp]: assumes R: "p \ carrier P" @@ -384,7 +388,7 @@ by algebra also from R have "... = \ (coeff P p n)" by (simp del: coeff_add add: coeff_add [THEN sym] - abelian_group.r_neg [OF cring.is_abelian_group [OF UP_cring]]) + abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]]) finally show ?thesis . qed @@ -409,11 +413,11 @@ lemma (in UP_cring) UP_abelian_monoid: "abelian_monoid P" - by (fast intro!: abelian_group.axioms cring.is_abelian_group UP_cring) + by (fast intro!: abelian_group.axioms ring.is_abelian_group UP_ring) lemma (in UP_cring) UP_abelian_group: "abelian_group P" - by (fast intro!: cring.is_abelian_group UP_cring) + by (fast intro!: ring.is_abelian_group UP_ring) lemmas (in UP_cring) UP_r_one [simp] = monoid.r_one [OF UP_monoid] @@ -521,19 +525,19 @@ abelian_group.r_neg1 [OF UP_abelian_group] lemmas (in UP_cring) UP_r_distr = - cring.r_distr [OF UP_cring] + ring.r_distr [OF UP_ring] lemmas (in UP_cring) UP_l_null [simp] = - cring.l_null [OF UP_cring] + ring.l_null [OF UP_ring] lemmas (in UP_cring) UP_r_null [simp] = - cring.r_null [OF UP_cring] + ring.r_null [OF UP_ring] lemmas (in UP_cring) UP_l_minus = - cring.l_minus [OF UP_cring] + ring.l_minus [OF UP_ring] lemmas (in UP_cring) UP_r_minus = - cring.r_minus [OF UP_cring] + ring.r_minus [OF UP_ring] lemmas (in UP_cring) UP_finsum_ldistr = cring.finsum_ldistr [OF UP_cring] diff -r c5c47703f763 -r dc677b35e54f src/HOL/Algebra/ringsimp.ML --- a/src/HOL/Algebra/ringsimp.ML Thu Feb 19 15:57:34 2004 +0100 +++ b/src/HOL/Algebra/ringsimp.ML Thu Feb 19 16:44:21 2004 +0100 @@ -64,16 +64,28 @@ val cring_ss = HOL_ss settermless termless_ring; fun cring_normalise ctxt = let - fun filter t = (case HOLogic.dest_Trueprop t of - Const ("CRing.cring_axioms", _) $ Free (s, _) => [s] + fun ring_filter t = (case HOLogic.dest_Trueprop t of + Const ("CRing.ring_axioms", _) $ Free (s, _) => [s] + | _ => []) + handle TERM _ => []; + fun comm_filter t = (case HOLogic.dest_Trueprop t of + Const ("Group.comm_semigroup_axioms", _) $ Free (s, _) => [s] | _ => []) handle TERM _ => []; - val insts = flat (map (filter o #prop o rep_thm) - (ProofContext.prems_of ctxt)); -val _ = warning ("Rings in proof context: " ^ implode insts); + + val prems = ProofContext.prems_of ctxt; + val rings = flat (map (ring_filter o #prop o rep_thm) prems); + val comms = flat (map (comm_filter o #prop o rep_thm) prems); + val non_comm_rings = rings \\ comms; + val comm_rings = rings inter_string comms; + val _ = tracing + ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^ + "\nCommutative rings in proof context: " ^ commas comm_rings); val simps = + flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules")) + non_comm_rings) @ flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules")) - insts); + comm_rings); in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps)) end; diff -r c5c47703f763 -r dc677b35e54f src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Thu Feb 19 15:57:34 2004 +0100 +++ b/src/HOL/Hilbert_Choice.thy Thu Feb 19 16:44:21 2004 +0100 @@ -51,6 +51,23 @@ apply (fast intro: someI2) done +lemma Inv_f_eq: + "[| inj_on f A; f x = y; x : A |] ==> Inv A f y = x" + apply (erule subst) + apply (erule Inv_f_f) + apply assumption + done + +lemma Inv_comp: + "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==> + Inv A (f o g) x = (Inv A g o Inv (g ` A) f) x" + apply simp + apply (rule Inv_f_eq) + apply (fast intro: comp_inj_on) + apply (simp add: f_Inv_f Inv_mem) + apply (simp add: Inv_mem) + done + lemma tfl_some: "\P x. P x --> P (Eps P)" -- {* dynamically-scoped fact for TFL *} by (blast intro: someI)