New lemmas about inversion of restricted functions.
authorballarin
Thu Feb 19 16:44:21 2004 +0100 (2004-02-19)
changeset 14399dc677b35e54f
parent 14398 c5c47703f763
child 14400 6069098854b9
New lemmas about inversion of restricted functions.
HOL-Algebra: new locale "ring" for non-commutative rings.
NEWS
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/ringsimp.ML
src/HOL/Hilbert_Choice.thy
     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.22      by (simp del: coeff_add add: coeff_add [THEN sym]
    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.35    in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
    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)