proper sublocales; no free-floating ML sections
authorhaftmann
Thu May 06 23:11:57 2010 +0200 (2010-05-06)
changeset 3672041da7025e59c
parent 36719 d396f6f63d94
child 36721 bfd7f5c3bf69
proper sublocales; no free-floating ML sections
src/HOL/Groebner_Basis.thy
src/HOL/Tools/Groebner_Basis/normalizer.ML
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu May 06 23:11:56 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu May 06 23:11:57 2010 +0200
     1.3 @@ -162,36 +162,7 @@
     1.4  proof
     1.5  qed (simp_all add: algebra_simps)
     1.6  
     1.7 -ML {*
     1.8 -local
     1.9 -
    1.10 -fun numeral_is_const ct = can HOLogic.dest_number (Thm.term_of ct);
    1.11 -
    1.12 -fun int_of_rat x =
    1.13 -  (case Rat.quotient_of_rat x of (i, 1) => i
    1.14 -  | _ => error "int_of_rat: bad int");
    1.15 -
    1.16 -val numeral_conv =
    1.17 -  Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}) then_conv
    1.18 -  Simplifier.rewrite (HOL_basic_ss addsimps
    1.19 -    (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}));
    1.20 -
    1.21 -in
    1.22 -
    1.23 -fun normalizer_funs' key =
    1.24 -  Normalizer.funs key
    1.25 -   {is_const = fn phi => numeral_is_const,
    1.26 -    dest_const = fn phi => fn ct =>
    1.27 -      Rat.rat_of_int (snd
    1.28 -        (HOLogic.dest_number (Thm.term_of ct)
    1.29 -          handle TERM _ => error "ring_dest_const")),
    1.30 -    mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT (int_of_rat x),
    1.31 -    conv = fn phi => K numeral_conv}
    1.32 -
    1.33 -end
    1.34 -*}
    1.35 -
    1.36 -declaration {* normalizer_funs' @{thm normalizing.normalizing_semiring_axioms'} *}
    1.37 +declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *}
    1.38  
    1.39  locale normalizing_ring = normalizing_semiring +
    1.40    fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.41 @@ -213,12 +184,12 @@
    1.42  
    1.43  end
    1.44  
    1.45 -(*FIXME add class*)
    1.46 -interpretation normalizing!: normalizing_ring plus times power
    1.47 -  "0::'a::{comm_semiring_1,number_ring}" 1 minus uminus proof
    1.48 -qed simp_all
    1.49 +sublocale comm_ring_1
    1.50 +  < normalizing!: normalizing_ring plus times power zero one minus uminus
    1.51 +proof
    1.52 +qed (simp_all add: diff_minus)
    1.53  
    1.54 -declaration {* normalizer_funs' @{thm normalizing.normalizing_ring_axioms'} *}
    1.55 +declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *}
    1.56  
    1.57  locale normalizing_field = normalizing_ring +
    1.58    fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.59 @@ -300,30 +271,22 @@
    1.60  
    1.61  end
    1.62  
    1.63 -lemma (in no_zero_divisors) prod_eq_zero_eq_zero:
    1.64 -  assumes "a * b = 0" and "a \<noteq> 0"
    1.65 -  shows "b = 0"
    1.66 -proof (rule classical)
    1.67 -  assume "b \<noteq> 0" with `a \<noteq> 0` no_zero_divisors have "a * b \<noteq> 0" by blast
    1.68 -  with `a * b = 0` show ?thesis by simp
    1.69 -qed
    1.70 +sublocale idom
    1.71 +  < normalizing!: normalizing_ring_cancel plus times power zero one minus uminus
    1.72 +proof
    1.73 +  fix w x y z
    1.74 +  show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
    1.75 +  proof
    1.76 +    assume "w * y + x * z = w * z + x * y"
    1.77 +    then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps)
    1.78 +    then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps)
    1.79 +    then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps)
    1.80 +    then have "y - z = 0 \<or> w - x = 0" by (rule divisors_zero)
    1.81 +    then show "w = x \<or> y = z" by auto
    1.82 +  qed (auto simp add: add_ac)
    1.83 +qed (simp_all add: algebra_simps)
    1.84  
    1.85 -(*FIXME introduce class*)
    1.86 -interpretation normalizing!: normalizing_ring_cancel
    1.87 -  "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus"
    1.88 -proof(unfold_locales, simp add: algebra_simps, auto)
    1.89 -  fix w x y z ::"'a::{idom,number_ring}"
    1.90 -  assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    1.91 -  hence ynz': "y - z \<noteq> 0" by simp
    1.92 -  from p have "w * y + x* z - w*z - x*y = 0" by simp
    1.93 -  hence "w* (y - z) - x * (y - z) = 0" by (simp add: algebra_simps)
    1.94 -  hence "(y - z) * (w - x) = 0" by (simp add: algebra_simps)
    1.95 -  with  prod_eq_zero_eq_zero [OF _ ynz']
    1.96 -  have "w - x = 0" by blast
    1.97 -  thus "w = x"  by simp
    1.98 -qed
    1.99 -
   1.100 -declaration {* normalizer_funs' @{thm normalizing.normalizing_ring_cancel_axioms'} *}
   1.101 +declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *}
   1.102  
   1.103  interpretation normalizing_nat!: normalizing_semiring_cancel
   1.104    "op +" "op *" "op ^" "0::nat" "1"
   1.105 @@ -347,7 +310,7 @@
   1.106    thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
   1.107  qed
   1.108  
   1.109 -declaration {* normalizer_funs' @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *}
   1.110 +declaration {* Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *}
   1.111  
   1.112  locale normalizing_field_cancel = normalizing_ring_cancel + normalizing_field
   1.113  begin
   1.114 @@ -366,221 +329,13 @@
   1.115  
   1.116  end
   1.117  
   1.118 -(*FIXME introduce class*)
   1.119 -interpretation normalizing!: normalizing_field_cancel "op +" "op *" "op ^"
   1.120 -  "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse"
   1.121 -apply (unfold_locales) by (simp_all add: divide_inverse)
   1.122 -
   1.123 -lemma divide_Numeral1: "(x::'a::{field, number_ring}) / Numeral1 = x" by simp
   1.124 -lemma divide_Numeral0: "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0"
   1.125 -  by simp
   1.126 -lemma mult_frac_frac: "((x::'a::field_inverse_zero) / y) * (z / w) = (x*z) / (y*w)"
   1.127 -  by simp
   1.128 -lemma mult_frac_num: "((x::'a::field_inverse_zero) / y) * z  = (x*z) / y"
   1.129 -  by (fact times_divide_eq_left)
   1.130 -lemma mult_num_frac: "((x::'a::field_inverse_zero) / y) * z  = (x*z) / y"
   1.131 -  by (fact times_divide_eq_left)
   1.132 -
   1.133 -lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
   1.134 -
   1.135 -lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::field_inverse_zero) / y + z = (x + z*y) / y"
   1.136 -  by (simp add: add_divide_distrib)
   1.137 -lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::field_inverse_zero) / y = (x + z*y) / y"
   1.138 -  by (simp add: add_divide_distrib)
   1.139 -
   1.140 -ML {* 
   1.141 -local
   1.142 - val zr = @{cpat "0"}
   1.143 - val zT = ctyp_of_term zr
   1.144 - val geq = @{cpat "op ="}
   1.145 - val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
   1.146 - val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
   1.147 - val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
   1.148 - val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
   1.149 -
   1.150 - fun prove_nz ss T t =
   1.151 -    let
   1.152 -      val z = instantiate_cterm ([(zT,T)],[]) zr
   1.153 -      val eq = instantiate_cterm ([(eqT,T)],[]) geq
   1.154 -      val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
   1.155 -           (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
   1.156 -                  (Thm.capply (Thm.capply eq t) z)))
   1.157 -    in equal_elim (symmetric th) TrueI
   1.158 -    end
   1.159 -
   1.160 - fun proc phi ss ct =
   1.161 -  let
   1.162 -    val ((x,y),(w,z)) =
   1.163 -         (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
   1.164 -    val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
   1.165 -    val T = ctyp_of_term x
   1.166 -    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
   1.167 -    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
   1.168 -  in SOME (implies_elim (implies_elim th y_nz) z_nz)
   1.169 -  end
   1.170 -  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
   1.171 -
   1.172 - fun proc2 phi ss ct =
   1.173 -  let
   1.174 -    val (l,r) = Thm.dest_binop ct
   1.175 -    val T = ctyp_of_term l
   1.176 -  in (case (term_of l, term_of r) of
   1.177 -      (Const(@{const_name Rings.divide},_)$_$_, _) =>
   1.178 -        let val (x,y) = Thm.dest_binop l val z = r
   1.179 -            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
   1.180 -            val ynz = prove_nz ss T y
   1.181 -        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
   1.182 -        end
   1.183 -     | (_, Const (@{const_name Rings.divide},_)$_$_) =>
   1.184 -        let val (x,y) = Thm.dest_binop r val z = l
   1.185 -            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
   1.186 -            val ynz = prove_nz ss T y
   1.187 -        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
   1.188 -        end
   1.189 -     | _ => NONE)
   1.190 -  end
   1.191 -  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
   1.192 -
   1.193 - fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
   1.194 -   | is_number t = can HOLogic.dest_number t
   1.195 -
   1.196 - val is_number = is_number o term_of
   1.197 +sublocale field 
   1.198 +  < normalizing!: normalizing_field_cancel plus times power zero one minus uminus divide inverse
   1.199 +proof
   1.200 +qed (simp_all add: divide_inverse)
   1.201  
   1.202 - fun proc3 phi ss ct =
   1.203 -  (case term_of ct of
   1.204 -    Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   1.205 -      let
   1.206 -        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   1.207 -        val _ = map is_number [a,b,c]
   1.208 -        val T = ctyp_of_term c
   1.209 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
   1.210 -      in SOME (mk_meta_eq th) end
   1.211 -  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   1.212 -      let
   1.213 -        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   1.214 -        val _ = map is_number [a,b,c]
   1.215 -        val T = ctyp_of_term c
   1.216 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
   1.217 -      in SOME (mk_meta_eq th) end
   1.218 -  | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   1.219 -      let
   1.220 -        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   1.221 -        val _ = map is_number [a,b,c]
   1.222 -        val T = ctyp_of_term c
   1.223 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
   1.224 -      in SOME (mk_meta_eq th) end
   1.225 -  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   1.226 -    let
   1.227 -      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   1.228 -        val _ = map is_number [a,b,c]
   1.229 -        val T = ctyp_of_term c
   1.230 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
   1.231 -      in SOME (mk_meta_eq th) end
   1.232 -  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   1.233 -    let
   1.234 -      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   1.235 -        val _ = map is_number [a,b,c]
   1.236 -        val T = ctyp_of_term c
   1.237 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   1.238 -      in SOME (mk_meta_eq th) end
   1.239 -  | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   1.240 -    let
   1.241 -      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   1.242 -        val _ = map is_number [a,b,c]
   1.243 -        val T = ctyp_of_term c
   1.244 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
   1.245 -      in SOME (mk_meta_eq th) end
   1.246 -  | _ => NONE)
   1.247 -  handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
   1.248 -
   1.249 -val add_frac_frac_simproc =
   1.250 -       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
   1.251 -                     name = "add_frac_frac_simproc",
   1.252 -                     proc = proc, identifier = []}
   1.253 -
   1.254 -val add_frac_num_simproc =
   1.255 -       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
   1.256 -                     name = "add_frac_num_simproc",
   1.257 -                     proc = proc2, identifier = []}
   1.258 -
   1.259 -val ord_frac_simproc =
   1.260 -  make_simproc
   1.261 -    {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
   1.262 -             @{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"},
   1.263 -             @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
   1.264 -             @{cpat "?c \<le> (?a::(?'a::{field, ord}))/?b"},
   1.265 -             @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
   1.266 -             @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
   1.267 -             name = "ord_frac_simproc", proc = proc3, identifier = []}
   1.268 -
   1.269 -val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
   1.270 -           @{thm "divide_Numeral1"},
   1.271 -           @{thm "divide_zero"}, @{thm "divide_Numeral0"},
   1.272 -           @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
   1.273 -           @{thm "mult_num_frac"}, @{thm "mult_frac_num"},
   1.274 -           @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
   1.275 -           @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
   1.276 -           @{thm "diff_def"}, @{thm "minus_divide_left"},
   1.277 -           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
   1.278 -           @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
   1.279 -           Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute}))))   
   1.280 -           (@{thm field_divide_inverse} RS sym)]
   1.281 -
   1.282 -in
   1.283 -
   1.284 -val field_comp_conv = (Simplifier.rewrite
   1.285 -(HOL_basic_ss addsimps @{thms "semiring_norm"}
   1.286 -              addsimps ths addsimps @{thms simp_thms}
   1.287 -              addsimprocs Numeral_Simprocs.field_cancel_numeral_factors
   1.288 -               addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
   1.289 -                            ord_frac_simproc]
   1.290 -                addcongs [@{thm "if_weak_cong"}]))
   1.291 -then_conv (Simplifier.rewrite (HOL_basic_ss addsimps
   1.292 -  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
   1.293 -
   1.294 -end
   1.295 -*}
   1.296 -
   1.297 -declaration {*
   1.298 -let
   1.299 -
   1.300 -fun numeral_is_const ct =
   1.301 -  case term_of ct of
   1.302 -   Const (@{const_name Rings.divide},_) $ a $ b =>
   1.303 -     can HOLogic.dest_number a andalso can HOLogic.dest_number b
   1.304 - | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
   1.305 - | t => can HOLogic.dest_number t
   1.306 -
   1.307 -fun dest_const ct = ((case term_of ct of
   1.308 -   Const (@{const_name Rings.divide},_) $ a $ b=>
   1.309 -    Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   1.310 - | Const (@{const_name Rings.inverse},_)$t => 
   1.311 -               Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
   1.312 - | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
   1.313 -   handle TERM _ => error "ring_dest_const")
   1.314 -
   1.315 -fun mk_const phi cT x =
   1.316 - let val (a, b) = Rat.quotient_of_rat x
   1.317 - in if b = 1 then Numeral.mk_cnumber cT a
   1.318 -    else Thm.capply
   1.319 -         (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
   1.320 -                     (Numeral.mk_cnumber cT a))
   1.321 -         (Numeral.mk_cnumber cT b)
   1.322 -  end
   1.323 -
   1.324 -in
   1.325 +declaration {* Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *}
   1.326   
   1.327 -  Normalizer.funs @{thm normalizing.normalizing_field_cancel_axioms'}
   1.328 -   {is_const = K numeral_is_const,
   1.329 -    dest_const = K dest_const,
   1.330 -    mk_const = mk_const,
   1.331 -    conv = K (K field_comp_conv)}
   1.332 -
   1.333 -end
   1.334 -*}
   1.335 -
   1.336 -lemmas comp_arith = semiring_norm (*FIXME*)
   1.337 -
   1.338  
   1.339  subsection {* Groebner Bases *}
   1.340  
   1.341 @@ -642,20 +397,7 @@
   1.342  
   1.343  use "Tools/Groebner_Basis/groebner.ML"
   1.344  
   1.345 -method_setup algebra =
   1.346 -{*
   1.347 -let
   1.348 - fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   1.349 - val addN = "add"
   1.350 - val delN = "del"
   1.351 - val any_keyword = keyword addN || keyword delN
   1.352 - val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   1.353 -in
   1.354 -  ((Scan.optional (keyword addN |-- thms) []) -- 
   1.355 -   (Scan.optional (keyword delN |-- thms) [])) >>
   1.356 -  (fn (add_ths, del_ths) => fn ctxt =>
   1.357 -       SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
   1.358 -end
   1.359 -*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
   1.360 +method_setup algebra = Groebner.algebra_method
   1.361 +  "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
   1.362  
   1.363  end
     2.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 23:11:56 2010 +0200
     2.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 23:11:57 2010 +0200
     2.3 @@ -16,6 +16,8 @@
     2.4      dest_const: morphism -> cterm -> Rat.rat,
     2.5      mk_const: morphism -> ctyp -> Rat.rat -> cterm,
     2.6      conv: morphism -> Proof.context -> cterm -> thm} -> declaration
     2.7 +  val semiring_funs: thm -> declaration
     2.8 +  val field_funs: thm -> declaration
     2.9  
    2.10    val semiring_normalize_conv: Proof.context -> conv
    2.11    val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
    2.12 @@ -29,6 +31,7 @@
    2.13    val semiring_normalizers_ord_wrapper:  Proof.context -> entry ->
    2.14      (cterm -> cterm -> bool) ->
    2.15        {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    2.16 +  val field_comp_conv: conv
    2.17  
    2.18    val setup: theory -> theory
    2.19  end
    2.20 @@ -36,6 +39,160 @@
    2.21  structure Normalizer: NORMALIZER = 
    2.22  struct
    2.23  
    2.24 +(** some conversion **)
    2.25 +
    2.26 +local
    2.27 + val zr = @{cpat "0"}
    2.28 + val zT = ctyp_of_term zr
    2.29 + val geq = @{cpat "op ="}
    2.30 + val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
    2.31 + val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
    2.32 + val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
    2.33 + val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
    2.34 +
    2.35 + fun prove_nz ss T t =
    2.36 +    let
    2.37 +      val z = instantiate_cterm ([(zT,T)],[]) zr
    2.38 +      val eq = instantiate_cterm ([(eqT,T)],[]) geq
    2.39 +      val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
    2.40 +           (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
    2.41 +                  (Thm.capply (Thm.capply eq t) z)))
    2.42 +    in equal_elim (symmetric th) TrueI
    2.43 +    end
    2.44 +
    2.45 + fun proc phi ss ct =
    2.46 +  let
    2.47 +    val ((x,y),(w,z)) =
    2.48 +         (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
    2.49 +    val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
    2.50 +    val T = ctyp_of_term x
    2.51 +    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
    2.52 +    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
    2.53 +  in SOME (implies_elim (implies_elim th y_nz) z_nz)
    2.54 +  end
    2.55 +  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
    2.56 +
    2.57 + fun proc2 phi ss ct =
    2.58 +  let
    2.59 +    val (l,r) = Thm.dest_binop ct
    2.60 +    val T = ctyp_of_term l
    2.61 +  in (case (term_of l, term_of r) of
    2.62 +      (Const(@{const_name Rings.divide},_)$_$_, _) =>
    2.63 +        let val (x,y) = Thm.dest_binop l val z = r
    2.64 +            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    2.65 +            val ynz = prove_nz ss T y
    2.66 +        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
    2.67 +        end
    2.68 +     | (_, Const (@{const_name Rings.divide},_)$_$_) =>
    2.69 +        let val (x,y) = Thm.dest_binop r val z = l
    2.70 +            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    2.71 +            val ynz = prove_nz ss T y
    2.72 +        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
    2.73 +        end
    2.74 +     | _ => NONE)
    2.75 +  end
    2.76 +  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
    2.77 +
    2.78 + fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
    2.79 +   | is_number t = can HOLogic.dest_number t
    2.80 +
    2.81 + val is_number = is_number o term_of
    2.82 +
    2.83 + fun proc3 phi ss ct =
    2.84 +  (case term_of ct of
    2.85 +    Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    2.86 +      let
    2.87 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    2.88 +        val _ = map is_number [a,b,c]
    2.89 +        val T = ctyp_of_term c
    2.90 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
    2.91 +      in SOME (mk_meta_eq th) end
    2.92 +  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    2.93 +      let
    2.94 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    2.95 +        val _ = map is_number [a,b,c]
    2.96 +        val T = ctyp_of_term c
    2.97 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
    2.98 +      in SOME (mk_meta_eq th) end
    2.99 +  | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   2.100 +      let
   2.101 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   2.102 +        val _ = map is_number [a,b,c]
   2.103 +        val T = ctyp_of_term c
   2.104 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
   2.105 +      in SOME (mk_meta_eq th) end
   2.106 +  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   2.107 +    let
   2.108 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   2.109 +        val _ = map is_number [a,b,c]
   2.110 +        val T = ctyp_of_term c
   2.111 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
   2.112 +      in SOME (mk_meta_eq th) end
   2.113 +  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   2.114 +    let
   2.115 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   2.116 +        val _ = map is_number [a,b,c]
   2.117 +        val T = ctyp_of_term c
   2.118 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   2.119 +      in SOME (mk_meta_eq th) end
   2.120 +  | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   2.121 +    let
   2.122 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   2.123 +        val _ = map is_number [a,b,c]
   2.124 +        val T = ctyp_of_term c
   2.125 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
   2.126 +      in SOME (mk_meta_eq th) end
   2.127 +  | _ => NONE)
   2.128 +  handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
   2.129 +
   2.130 +val add_frac_frac_simproc =
   2.131 +       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
   2.132 +                     name = "add_frac_frac_simproc",
   2.133 +                     proc = proc, identifier = []}
   2.134 +
   2.135 +val add_frac_num_simproc =
   2.136 +       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
   2.137 +                     name = "add_frac_num_simproc",
   2.138 +                     proc = proc2, identifier = []}
   2.139 +
   2.140 +val ord_frac_simproc =
   2.141 +  make_simproc
   2.142 +    {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
   2.143 +             @{cpat "(?a::(?'a::{field, ord}))/?b <= ?c"},
   2.144 +             @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
   2.145 +             @{cpat "?c <= (?a::(?'a::{field, ord}))/?b"},
   2.146 +             @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
   2.147 +             @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
   2.148 +             name = "ord_frac_simproc", proc = proc3, identifier = []}
   2.149 +
   2.150 +val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
   2.151 +           @{thm "divide_Numeral1"},
   2.152 +           @{thm "divide_zero"}, @{thm "divide_Numeral0"},
   2.153 +           @{thm "divide_divide_eq_left"}, 
   2.154 +           @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
   2.155 +           @{thm "times_divide_times_eq"},
   2.156 +           @{thm "divide_divide_eq_right"},
   2.157 +           @{thm "diff_def"}, @{thm "minus_divide_left"},
   2.158 +           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
   2.159 +           @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
   2.160 +           Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute}))))   
   2.161 +           (@{thm field_divide_inverse} RS sym)]
   2.162 +
   2.163 +in
   2.164 +
   2.165 +val field_comp_conv = (Simplifier.rewrite
   2.166 +(HOL_basic_ss addsimps @{thms "semiring_norm"}
   2.167 +              addsimps ths addsimps @{thms simp_thms}
   2.168 +              addsimprocs Numeral_Simprocs.field_cancel_numeral_factors
   2.169 +               addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
   2.170 +                            ord_frac_simproc]
   2.171 +                addcongs [@{thm "if_weak_cong"}]))
   2.172 +then_conv (Simplifier.rewrite (HOL_basic_ss addsimps
   2.173 +  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
   2.174 +
   2.175 +end
   2.176 +
   2.177 +
   2.178  (** data **)
   2.179  
   2.180  type entry =
   2.181 @@ -169,6 +326,49 @@
   2.182        mk_const = mk_const phi, conv = conv phi};
   2.183    in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
   2.184  
   2.185 +fun semiring_funs key = funs key
   2.186 +   {is_const = fn phi => can HOLogic.dest_number o Thm.term_of,
   2.187 +    dest_const = fn phi => fn ct =>
   2.188 +      Rat.rat_of_int (snd
   2.189 +        (HOLogic.dest_number (Thm.term_of ct)
   2.190 +          handle TERM _ => error "ring_dest_const")),
   2.191 +    mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT
   2.192 +      (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"),
   2.193 +    conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm})
   2.194 +      then_conv Simplifier.rewrite (HOL_basic_ss addsimps
   2.195 +        (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))};
   2.196 +
   2.197 +fun field_funs key =
   2.198 +  let
   2.199 +    fun numeral_is_const ct =
   2.200 +      case term_of ct of
   2.201 +       Const (@{const_name Rings.divide},_) $ a $ b =>
   2.202 +         can HOLogic.dest_number a andalso can HOLogic.dest_number b
   2.203 +     | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
   2.204 +     | t => can HOLogic.dest_number t
   2.205 +    fun dest_const ct = ((case term_of ct of
   2.206 +       Const (@{const_name Rings.divide},_) $ a $ b=>
   2.207 +        Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   2.208 +     | Const (@{const_name Rings.inverse},_)$t => 
   2.209 +                   Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
   2.210 +     | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
   2.211 +       handle TERM _ => error "ring_dest_const")
   2.212 +    fun mk_const phi cT x =
   2.213 +      let val (a, b) = Rat.quotient_of_rat x
   2.214 +      in if b = 1 then Numeral.mk_cnumber cT a
   2.215 +        else Thm.capply
   2.216 +             (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
   2.217 +                         (Numeral.mk_cnumber cT a))
   2.218 +             (Numeral.mk_cnumber cT b)
   2.219 +      end
   2.220 +  in funs key
   2.221 +     {is_const = K numeral_is_const,
   2.222 +      dest_const = K dest_const,
   2.223 +      mk_const = mk_const,
   2.224 +      conv = K (K field_comp_conv)}
   2.225 +  end;
   2.226 +
   2.227 +
   2.228  
   2.229  (** auxiliary **)
   2.230