New lemmas about inversion of restricted functions.
HOL-Algebra: new locale "ring" for non-commutative rings.
--- 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
--- 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 \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
+ and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+ ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
+
+locale cring = ring + comm_monoid R
locale "domain" = cring +
assumes one_not_zero [simp]: "\<one> ~= \<zero>"
@@ -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 \<in> carrier R; y \<in> carrier R; z \<in> 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 \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+ ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> 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 \<in> carrier R; y \<in> carrier R; z \<in> 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 \<in> carrier R" "y \<in> carrier R" "z \<in> 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 \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
+ by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
+ also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
+ also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
+ by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
+ finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> 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 \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
- ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
-proof -
- assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
- then have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" by (simp add: m_comm)
- also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
- also from R have "... = z \<otimes> x \<oplus> z \<otimes> 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 \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
proof -
assume R: "x \<in> 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 \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
proof -
assume R: "x \<in> carrier R"
- then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: m_ac)
- also from R have "... = \<zero>" by simp
- finally show ?thesis .
+ then have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> (\<zero> \<oplus> \<zero>)"
+ by (simp add: r_distr del: l_zero r_zero)
+ also from R have "... = x \<otimes> \<zero> \<oplus> \<zero>" by simp
+ finally have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> \<zero> \<oplus> \<zero>" .
+ with R show ?thesis by (simp del: r_zero)
qed
-lemma (in cring) l_minus:
+lemma (in ring) l_minus:
"[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
proof -
assume R: "x \<in> carrier R" "y \<in> 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 \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
proof -
assume R: "x \<in> carrier R" "y \<in> carrier R"
- then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: m_ac)
- also from R have "... = \<ominus> (y \<otimes> x)" by (simp add: l_minus)
- also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: m_ac)
- finally show ?thesis .
+ then have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = x \<otimes> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
+ also from R have "... = \<zero>" by (simp add: l_neg r_null)
+ finally have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = \<zero>" .
+ with R have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> 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 \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> 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 \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==>
a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^sub>2 d = d \<otimes>\<^sub>2 c"
by algebra
--- 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 \<in> carrier P ==> \<ominus>\<^sub>2 p \<in> 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 \<in> carrier P"
@@ -384,7 +388,7 @@
by algebra
also from R have "... = \<ominus> (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]
--- 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;
--- 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: "\<forall>P x. P x --> P (Eps P)"
-- {* dynamically-scoped fact for TFL *}
by (blast intro: someI)