moved normalization proof tool infrastructure to canonical algebraic classes
authorhaftmann
Sat May 08 18:52:38 2010 +0200 (2010-05-08)
changeset 36756c1ae8a0b4265
parent 36754 5ce217fc769a
child 36757 21443c2858a7
moved normalization proof tool infrastructure to canonical algebraic classes
src/HOL/Semiring_Normalization.thy
     1.1 --- a/src/HOL/Semiring_Normalization.thy	Sat May 08 17:15:50 2010 +0200
     1.2 +++ b/src/HOL/Semiring_Normalization.thy	Sat May 08 18:52:38 2010 +0200
     1.3 @@ -10,6 +10,46 @@
     1.4    "Tools/semiring_normalizer.ML"
     1.5  begin
     1.6  
     1.7 +text {* FIXME prelude *}
     1.8 +
     1.9 +class comm_semiring_1_cancel_norm (*FIXME name*) = comm_semiring_1_cancel +
    1.10 +  assumes add_mult_solve: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
    1.11 +
    1.12 +sublocale idom < comm_semiring_1_cancel_norm
    1.13 +proof
    1.14 +  fix w x y z
    1.15 +  show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
    1.16 +  proof
    1.17 +    assume "w * y + x * z = w * z + x * y"
    1.18 +    then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps)
    1.19 +    then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps)
    1.20 +    then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps)
    1.21 +    then have "y - z = 0 \<or> w - x = 0" by (rule divisors_zero)
    1.22 +    then show "w = x \<or> y = z" by auto
    1.23 +  qed (auto simp add: add_ac)
    1.24 +qed
    1.25 +
    1.26 +instance nat :: comm_semiring_1_cancel_norm
    1.27 +proof
    1.28 +  fix w x y z :: nat
    1.29 +  { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    1.30 +    hence "y < z \<or> y > z" by arith
    1.31 +    moreover {
    1.32 +      assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto)
    1.33 +      then obtain k where kp: "k>0" and yz:"z = y + k" by blast
    1.34 +      from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps)
    1.35 +      hence "x*k = w*k" by simp
    1.36 +      hence "w = x" using kp by simp }
    1.37 +    moreover {
    1.38 +      assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto)
    1.39 +      then obtain k where kp: "k>0" and yz:"y = z + k" by blast
    1.40 +      from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps)
    1.41 +      hence "w*k = x*k" by simp
    1.42 +      hence "w = x" using kp by simp }
    1.43 +    ultimately have "w=x" by blast }
    1.44 +  then show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" by auto
    1.45 +qed
    1.46 +
    1.47  setup Semiring_Normalizer.setup
    1.48  
    1.49  locale normalizing_semiring =
    1.50 @@ -146,12 +186,6 @@
    1.51      by (simp add: nat_number' pwr_Suc mul_pwr)
    1.52  qed
    1.53  
    1.54 -
    1.55 -lemmas normalizing_semiring_axioms' =
    1.56 -  normalizing_semiring_axioms [normalizer
    1.57 -    semiring ops: semiring_ops
    1.58 -    semiring rules: semiring_rules]
    1.59 -
    1.60  end
    1.61  
    1.62  sublocale comm_semiring_1
    1.63 @@ -159,7 +193,13 @@
    1.64  proof
    1.65  qed (simp_all add: algebra_simps)
    1.66  
    1.67 -declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *}
    1.68 +lemmas (in comm_semiring_1) normalizing_comm_semiring_1_axioms =
    1.69 +  comm_semiring_1_axioms [normalizer
    1.70 +    semiring ops: normalizing.semiring_ops
    1.71 +    semiring rules: normalizing.semiring_rules]
    1.72 +
    1.73 +declaration (in comm_semiring_1)
    1.74 +  {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *}
    1.75  
    1.76  locale normalizing_ring = normalizing_semiring +
    1.77    fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.78 @@ -172,13 +212,6 @@
    1.79  
    1.80  lemmas ring_rules = neg_mul sub_add
    1.81  
    1.82 -lemmas normalizing_ring_axioms' =
    1.83 -  normalizing_ring_axioms [normalizer
    1.84 -    semiring ops: semiring_ops
    1.85 -    semiring rules: semiring_rules
    1.86 -    ring ops: ring_ops
    1.87 -    ring rules: ring_rules]
    1.88 -
    1.89  end
    1.90  
    1.91  sublocale comm_ring_1
    1.92 @@ -186,29 +219,15 @@
    1.93  proof
    1.94  qed (simp_all add: diff_minus)
    1.95  
    1.96 -declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *}
    1.97 -
    1.98 -locale normalizing_field = normalizing_ring +
    1.99 -  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.100 -    and inverse:: "'a \<Rightarrow> 'a"
   1.101 -  assumes divide_inverse: "divide x y = mul x (inverse y)"
   1.102 -     and inverse_divide: "inverse x = divide r1 x"
   1.103 -begin
   1.104 -
   1.105 -lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" .
   1.106 +lemmas (in comm_ring_1) normalizing_comm_ring_1_axioms =
   1.107 +  comm_ring_1_axioms [normalizer
   1.108 +    semiring ops: normalizing.semiring_ops
   1.109 +    semiring rules: normalizing.semiring_rules
   1.110 +    ring ops: normalizing.ring_ops
   1.111 +    ring rules: normalizing.ring_rules]
   1.112  
   1.113 -lemmas field_rules = divide_inverse inverse_divide
   1.114 -
   1.115 -lemmas normalizing_field_axioms' =
   1.116 -  normalizing_field_axioms [normalizer
   1.117 -    semiring ops: semiring_ops
   1.118 -    semiring rules: semiring_rules
   1.119 -    ring ops: ring_ops
   1.120 -    ring rules: ring_rules
   1.121 -    field ops: field_ops
   1.122 -    field rules: field_rules]
   1.123 -
   1.124 -end
   1.125 +declaration (in comm_ring_1)
   1.126 +  {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *}
   1.127  
   1.128  locale normalizing_semiring_cancel = normalizing_semiring +
   1.129    assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"
   1.130 @@ -242,95 +261,77 @@
   1.131    thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
   1.132  qed
   1.133  
   1.134 -declare normalizing_semiring_axioms' [normalizer del]
   1.135 +end
   1.136 +
   1.137 +sublocale comm_semiring_1_cancel_norm
   1.138 +  < normalizing!: normalizing_semiring_cancel plus times power zero one
   1.139 +proof
   1.140 +qed (simp_all add: add_mult_solve)
   1.141 +
   1.142 +declare (in comm_semiring_1_cancel_norm)
   1.143 +  normalizing_comm_semiring_1_axioms [normalizer del]
   1.144  
   1.145 -lemmas normalizing_semiring_cancel_axioms' =
   1.146 -  normalizing_semiring_cancel_axioms [normalizer
   1.147 -    semiring ops: semiring_ops
   1.148 -    semiring rules: semiring_rules
   1.149 -    idom rules: noteq_reduce add_scale_eq_noteq]
   1.150 +lemmas (in comm_semiring_1_cancel_norm)
   1.151 +  normalizing_comm_semiring_1_cancel_norm_axioms =
   1.152 +  comm_semiring_1_cancel_norm_axioms [normalizer
   1.153 +    semiring ops: normalizing.semiring_ops
   1.154 +    semiring rules: normalizing.semiring_rules
   1.155 +    idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq]
   1.156  
   1.157 -end
   1.158 +declaration (in comm_semiring_1_cancel_norm)
   1.159 +  {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_norm_axioms} *}
   1.160  
   1.161  locale normalizing_ring_cancel = normalizing_semiring_cancel + normalizing_ring + 
   1.162    assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
   1.163 -begin
   1.164 -
   1.165 -declare normalizing_ring_axioms' [normalizer del]
   1.166 -
   1.167 -lemmas normalizing_ring_cancel_axioms' = normalizing_ring_cancel_axioms [normalizer
   1.168 -  semiring ops: semiring_ops
   1.169 -  semiring rules: semiring_rules
   1.170 -  ring ops: ring_ops
   1.171 -  ring rules: ring_rules
   1.172 -  idom rules: noteq_reduce add_scale_eq_noteq
   1.173 -  ideal rules: subr0_iff add_r0_iff]
   1.174 -
   1.175 -end
   1.176  
   1.177  sublocale idom
   1.178    < normalizing!: normalizing_ring_cancel plus times power zero one minus uminus
   1.179  proof
   1.180 -  fix w x y z
   1.181 -  show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
   1.182 -  proof
   1.183 -    assume "w * y + x * z = w * z + x * y"
   1.184 -    then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps)
   1.185 -    then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps)
   1.186 -    then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps)
   1.187 -    then have "y - z = 0 \<or> w - x = 0" by (rule divisors_zero)
   1.188 -    then show "w = x \<or> y = z" by auto
   1.189 -  qed (auto simp add: add_ac)
   1.190 -qed (simp_all add: algebra_simps)
   1.191 +qed simp
   1.192  
   1.193 -declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *}
   1.194 +declare (in idom) normalizing_comm_ring_1_axioms [normalizer del]
   1.195  
   1.196 -interpretation normalizing_nat!: normalizing_semiring_cancel
   1.197 -  "op +" "op *" "op ^" "0::nat" "1"
   1.198 -proof (unfold_locales, simp add: algebra_simps)
   1.199 -  fix w x y z ::"nat"
   1.200 -  { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
   1.201 -    hence "y < z \<or> y > z" by arith
   1.202 -    moreover {
   1.203 -      assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto)
   1.204 -      then obtain k where kp: "k>0" and yz:"z = y + k" by blast
   1.205 -      from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps)
   1.206 -      hence "x*k = w*k" by simp
   1.207 -      hence "w = x" using kp by simp }
   1.208 -    moreover {
   1.209 -      assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto)
   1.210 -      then obtain k where kp: "k>0" and yz:"y = z + k" by blast
   1.211 -      from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps)
   1.212 -      hence "w*k = x*k" by simp
   1.213 -      hence "w = x" using kp by simp }
   1.214 -    ultimately have "w=x" by blast }
   1.215 -  thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
   1.216 -qed
   1.217 +lemmas (in idom) normalizing_idom_axioms = idom_axioms [normalizer
   1.218 +  semiring ops: normalizing.semiring_ops
   1.219 +  semiring rules: normalizing.semiring_rules
   1.220 +  ring ops: normalizing.ring_ops
   1.221 +  ring rules: normalizing.ring_rules
   1.222 +  idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq
   1.223 +  ideal rules: normalizing.subr0_iff normalizing.add_r0_iff]
   1.224  
   1.225 -declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *}
   1.226 +declaration (in idom)
   1.227 +  {* Semiring_Normalizer.semiring_funs @{thm normalizing_idom_axioms} *}
   1.228  
   1.229 -locale normalizing_field_cancel = normalizing_ring_cancel + normalizing_field
   1.230 +locale normalizing_field = normalizing_ring_cancel +
   1.231 +  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.232 +    and inverse:: "'a \<Rightarrow> 'a"
   1.233 +  assumes divide_inverse: "divide x y = mul x (inverse y)"
   1.234 +     and inverse_divide: "inverse x = divide r1 x"
   1.235  begin
   1.236  
   1.237 -declare normalizing_field_axioms' [normalizer del]
   1.238 +lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" .
   1.239  
   1.240 -lemmas normalizing_field_cancel_axioms' = normalizing_field_cancel_axioms [normalizer
   1.241 -  semiring ops: semiring_ops
   1.242 -  semiring rules: semiring_rules
   1.243 -  ring ops: ring_ops
   1.244 -  ring rules: ring_rules
   1.245 -  field ops: field_ops
   1.246 -  field rules: field_rules
   1.247 -  idom rules: noteq_reduce add_scale_eq_noteq
   1.248 -  ideal rules: subr0_iff add_r0_iff]
   1.249 +lemmas field_rules = divide_inverse inverse_divide
   1.250  
   1.251  end
   1.252  
   1.253  sublocale field 
   1.254 -  < normalizing!: normalizing_field_cancel plus times power zero one minus uminus divide inverse
   1.255 +  < normalizing!: normalizing_field plus times power zero one minus uminus divide inverse
   1.256  proof
   1.257  qed (simp_all add: divide_inverse)
   1.258  
   1.259 -declaration {* Semiring_Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *}
   1.260 +lemmas (in field) normalizing_field_axioms =
   1.261 +  field_axioms [normalizer
   1.262 +    semiring ops: normalizing.semiring_ops
   1.263 +    semiring rules: normalizing.semiring_rules
   1.264 +    ring ops: normalizing.ring_ops
   1.265 +    ring rules: normalizing.ring_rules
   1.266 +    field ops: normalizing.field_ops
   1.267 +    field rules: normalizing.field_rules
   1.268 +    idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq
   1.269 +    ideal rules: normalizing.subr0_iff normalizing.add_r0_iff]
   1.270 +
   1.271 +declaration (in field)
   1.272 +  {* Semiring_Normalizer.field_funs @{thm normalizing_field_axioms} *}
   1.273  
   1.274  end