src/HOL/Semiring_Normalization.thy
changeset 36873 112e613e8d0b
parent 36872 6520ba1256a6
child 37946 be3c0df7bb90
     1.1 --- a/src/HOL/Semiring_Normalization.thy	Wed May 12 13:51:22 2010 +0200
     1.2 +++ b/src/HOL/Semiring_Normalization.thy	Wed May 12 15:27:15 2010 +0200
     1.3 @@ -10,12 +10,33 @@
     1.4    "Tools/semiring_normalizer.ML"
     1.5  begin
     1.6  
     1.7 -text {* FIXME prelude *}
     1.8 +text {* Prelude *}
     1.9 +
    1.10 +class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel +
    1.11 +  assumes crossproduct_eq: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
    1.12 +begin
    1.13 +
    1.14 +lemma crossproduct_noteq:
    1.15 +  "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> a * c + b * d \<noteq> a * d + b * c"
    1.16 +  by (simp add: crossproduct_eq)
    1.17  
    1.18 -class comm_semiring_1_cancel_norm (*FIXME name*) = comm_semiring_1_cancel +
    1.19 -  assumes add_mult_solve: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
    1.20 +lemma add_scale_eq_noteq:
    1.21 +  "r \<noteq> 0 \<Longrightarrow> a = b \<and> c \<noteq> d \<Longrightarrow> a + r * c \<noteq> b + r * d"
    1.22 +proof (rule notI)
    1.23 +  assume nz: "r\<noteq> 0" and cnd: "a = b \<and> c\<noteq>d"
    1.24 +    and eq: "a + (r * c) = b + (r * d)"
    1.25 +  have "(0 * d) + (r * c) = (0 * c) + (r * d)"
    1.26 +    using add_imp_eq eq mult_zero_left by (simp add: cnd)
    1.27 +  then show False using crossproduct_eq [of 0 d] nz cnd by simp
    1.28 +qed
    1.29  
    1.30 -sublocale idom < comm_semiring_1_cancel_norm
    1.31 +lemma add_0_iff:
    1.32 +  "b = b + a \<longleftrightarrow> a = 0"
    1.33 +  using add_imp_eq [of b a 0] by auto
    1.34 +
    1.35 +end
    1.36 +
    1.37 +sublocale idom < comm_semiring_1_cancel_crossproduct
    1.38  proof
    1.39    fix w x y z
    1.40    show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
    1.41 @@ -29,28 +50,24 @@
    1.42    qed (auto simp add: add_ac)
    1.43  qed
    1.44  
    1.45 -instance nat :: comm_semiring_1_cancel_norm
    1.46 +instance nat :: comm_semiring_1_cancel_crossproduct
    1.47  proof
    1.48    fix w x y z :: nat
    1.49 -  { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    1.50 -    hence "y < z \<or> y > z" by arith
    1.51 -    moreover {
    1.52 -      assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto)
    1.53 -      then obtain k where kp: "k>0" and yz:"z = y + k" by blast
    1.54 -      from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps)
    1.55 -      hence "x*k = w*k" by simp
    1.56 -      hence "w = x" using kp by simp }
    1.57 -    moreover {
    1.58 -      assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto)
    1.59 -      then obtain k where kp: "k>0" and yz:"y = z + k" by blast
    1.60 -      from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps)
    1.61 -      hence "w*k = x*k" by simp
    1.62 -      hence "w = x" using kp by simp }
    1.63 -    ultimately have "w=x" by blast }
    1.64 -  then show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" by auto
    1.65 +  have aux: "\<And>y z. y < z \<Longrightarrow> w * y + x * z = w * z + x * y \<Longrightarrow> w = x"
    1.66 +  proof -
    1.67 +    fix y z :: nat
    1.68 +    assume "y < z" then have "\<exists>k. z = y + k \<and> k \<noteq> 0" by (intro exI [of _ "z - y"]) auto
    1.69 +    then obtain k where "z = y + k" and "k \<noteq> 0" by blast
    1.70 +    assume "w * y + x * z = w * z + x * y"
    1.71 +    then have "(w * y + x * y) + x * k = (w * y + x * y) + w * k" by (simp add: `z = y + k` algebra_simps)
    1.72 +    then have "x * k = w * k" by simp
    1.73 +    then show "w = x" using `k \<noteq> 0` by simp
    1.74 +  qed
    1.75 +  show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
    1.76 +    by (auto simp add: neq_iff dest!: aux)
    1.77  qed
    1.78  
    1.79 -text {* semiring normalization proper *}
    1.80 +text {* Semiring normalization proper *}
    1.81  
    1.82  setup Semiring_Normalizer.setup
    1.83  
    1.84 @@ -133,39 +150,21 @@
    1.85  
    1.86  end
    1.87  
    1.88 -context comm_semiring_1_cancel_norm
    1.89 +context comm_semiring_1_cancel_crossproduct
    1.90  begin
    1.91  
    1.92 -lemma noteq_reduce:
    1.93 -  "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> a * c + b * d \<noteq> a * d + b * c"
    1.94 -  by (simp add: add_mult_solve)
    1.95 -
    1.96 -lemma add_scale_eq_noteq:
    1.97 -  "r \<noteq> 0 \<Longrightarrow> a = b \<and> c \<noteq> d \<Longrightarrow> a + r * c \<noteq> b + r * d"
    1.98 -proof (rule notI)
    1.99 -  assume nz: "r\<noteq> 0" and cnd: "a = b \<and> c\<noteq>d"
   1.100 -    and eq: "a + (r * c) = b + (r * d)"
   1.101 -  have "(0 * d) + (r * c) = (0 * c) + (r * d)"
   1.102 -    using add_imp_eq eq mult_zero_left by (simp add: cnd)
   1.103 -  then show False using add_mult_solve [of 0 d] nz cnd by simp
   1.104 -qed
   1.105 -
   1.106 -lemma add_0_iff:
   1.107 -  "x = x + a \<longleftrightarrow> a = 0"
   1.108 -  using add_imp_eq [of x a 0] by auto
   1.109 -
   1.110  declare
   1.111    normalizing_comm_semiring_1_axioms [normalizer del]
   1.112  
   1.113  lemmas
   1.114 -  normalizing_comm_semiring_1_cancel_norm_axioms =
   1.115 -  comm_semiring_1_cancel_norm_axioms [normalizer
   1.116 +  normalizing_comm_semiring_1_cancel_crossproduct_axioms =
   1.117 +  comm_semiring_1_cancel_crossproduct_axioms [normalizer
   1.118      semiring ops: normalizing_semiring_ops
   1.119      semiring rules: normalizing_semiring_rules
   1.120 -    idom rules: noteq_reduce add_scale_eq_noteq]
   1.121 +    idom rules: crossproduct_noteq add_scale_eq_noteq]
   1.122  
   1.123  declaration
   1.124 -  {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_norm_axioms} *}
   1.125 +  {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_crossproduct_axioms} *}
   1.126  
   1.127  end
   1.128  
   1.129 @@ -179,7 +178,7 @@
   1.130    semiring rules: normalizing_semiring_rules
   1.131    ring ops: normalizing_ring_ops
   1.132    ring rules: normalizing_ring_rules
   1.133 -  idom rules: noteq_reduce add_scale_eq_noteq
   1.134 +  idom rules: crossproduct_noteq add_scale_eq_noteq
   1.135    ideal rules: right_minus_eq add_0_iff]
   1.136  
   1.137  declaration
   1.138 @@ -203,7 +202,7 @@
   1.139      ring rules: normalizing_ring_rules
   1.140      field ops: normalizing_field_ops
   1.141      field rules: normalizing_field_rules
   1.142 -    idom rules: noteq_reduce add_scale_eq_noteq
   1.143 +    idom rules: crossproduct_noteq add_scale_eq_noteq
   1.144      ideal rules: right_minus_eq add_0_iff]
   1.145  
   1.146  declaration
   1.147 @@ -212,13 +211,11 @@
   1.148  end
   1.149  
   1.150  hide_fact (open) normalizing_comm_semiring_1_axioms
   1.151 -  normalizing_comm_semiring_1_cancel_norm_axioms normalizing_semiring_ops normalizing_semiring_rules
   1.152 +  normalizing_comm_semiring_1_cancel_crossproduct_axioms normalizing_semiring_ops normalizing_semiring_rules
   1.153  
   1.154  hide_fact (open) normalizing_comm_ring_1_axioms
   1.155    normalizing_idom_axioms normalizing_ring_ops normalizing_ring_rules
   1.156  
   1.157  hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules
   1.158  
   1.159 -hide_fact (open) add_scale_eq_noteq noteq_reduce
   1.160 -
   1.161  end