author haftmann Mon Sep 29 12:31:59 2008 +0200 (2008-09-29) changeset 28402 09e4aa3ddc25 parent 28401 d5f39173444c child 28403 da9ae7774513
clarified dependencies between arith tools
 src/HOL/Arith_Tools.thy file | annotate | diff | revisions src/HOL/Groebner_Basis.thy file | annotate | diff | revisions src/HOL/Library/Dense_Linear_Order.thy file | annotate | diff | revisions src/HOL/Presburger.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Arith_Tools.thy	Mon Sep 29 12:31:58 2008 +0200
1.2 +++ b/src/HOL/Arith_Tools.thy	Mon Sep 29 12:31:59 2008 +0200
1.3 @@ -7,12 +7,13 @@
1.4  header {* Setup of arithmetic tools *}
1.5
1.6  theory Arith_Tools
1.7 -imports Groebner_Basis
1.8 +imports NatBin
1.9  uses
1.10    "~~/src/Provers/Arith/cancel_numeral_factor.ML"
1.11    "~~/src/Provers/Arith/extract_common_term.ML"
1.12    "int_factor_simprocs.ML"
1.13    "nat_simprocs.ML"
1.14 +  "Tools/Qelim/qelim.ML"
1.15  begin
1.16
1.17  subsection {* Simprocs for the Naturals *}
1.18 @@ -382,219 +383,4 @@
1.19  val minus1_divide = @{thm minus1_divide};
1.20  *}
1.21
1.22 -
1.23 -subsection{* Groebner Bases for fields *}
1.24 -
1.25 -interpretation class_fieldgb:
1.26 -  fieldgb["op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse"] apply (unfold_locales) by (simp_all add: divide_inverse)
1.27 -
1.28 -lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
1.29 -lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
1.30 -  by simp
1.31 -lemma mult_frac_frac: "((x::'a::{field,division_by_zero}) / y) * (z / w) = (x*z) / (y*w)"
1.32 -  by simp
1.33 -lemma mult_frac_num: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
1.34 -  by simp
1.35 -lemma mult_num_frac: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
1.36 -  by simp
1.37 -
1.38 -lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
1.39 -
1.40 -lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_by_zero}) / y + z = (x + z*y) / y"
1.42 -lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
1.44 -
1.45 -
1.46 -ML{*
1.47 -local
1.48 - val zr = @{cpat "0"}
1.49 - val zT = ctyp_of_term zr
1.50 - val geq = @{cpat "op ="}
1.51 - val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
1.55 -
1.56 - fun prove_nz ss T t =
1.57 -    let
1.58 -      val z = instantiate_cterm ([(zT,T)],[]) zr
1.59 -      val eq = instantiate_cterm ([(eqT,T)],[]) geq
1.60 -      val th = Simplifier.rewrite (ss addsimps simp_thms)
1.61 -           (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
1.62 -                  (Thm.capply (Thm.capply eq t) z)))
1.63 -    in equal_elim (symmetric th) TrueI
1.64 -    end
1.65 -
1.66 - fun proc phi ss ct =
1.67 -  let
1.68 -    val ((x,y),(w,z)) =
1.69 -         (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
1.70 -    val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
1.71 -    val T = ctyp_of_term x
1.72 -    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
1.73 -    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
1.74 -  in SOME (implies_elim (implies_elim th y_nz) z_nz)
1.75 -  end
1.76 -  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
1.77 -
1.78 - fun proc2 phi ss ct =
1.79 -  let
1.80 -    val (l,r) = Thm.dest_binop ct
1.81 -    val T = ctyp_of_term l
1.82 -  in (case (term_of l, term_of r) of
1.83 -      (Const(@{const_name "HOL.divide"},_)\$_\$_, _) =>
1.84 -        let val (x,y) = Thm.dest_binop l val z = r
1.85 -            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
1.86 -            val ynz = prove_nz ss T y
1.87 -        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
1.88 -        end
1.89 -     | (_, Const (@{const_name "HOL.divide"},_)\$_\$_) =>
1.90 -        let val (x,y) = Thm.dest_binop r val z = l
1.91 -            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
1.92 -            val ynz = prove_nz ss T y
1.93 -        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
1.94 -        end
1.95 -     | _ => NONE)
1.96 -  end
1.97 -  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
1.98 -
1.99 - fun is_number (Const(@{const_name "HOL.divide"},_)\$a\$b) = is_number a andalso is_number b
1.100 -   | is_number t = can HOLogic.dest_number t
1.101 -
1.102 - val is_number = is_number o term_of
1.103 -
1.104 - fun proc3 phi ss ct =
1.105 -  (case term_of ct of
1.106 -    Const(@{const_name HOL.less},_)\$(Const(@{const_name "HOL.divide"},_)\$_\$_)\$_ =>
1.107 -      let
1.108 -        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
1.109 -        val _ = map is_number [a,b,c]
1.110 -        val T = ctyp_of_term c
1.111 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
1.112 -      in SOME (mk_meta_eq th) end
1.113 -  | Const(@{const_name HOL.less_eq},_)\$(Const(@{const_name "HOL.divide"},_)\$_\$_)\$_ =>
1.114 -      let
1.115 -        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
1.116 -        val _ = map is_number [a,b,c]
1.117 -        val T = ctyp_of_term c
1.118 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
1.119 -      in SOME (mk_meta_eq th) end
1.120 -  | Const("op =",_)\$(Const(@{const_name "HOL.divide"},_)\$_\$_)\$_ =>
1.121 -      let
1.122 -        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
1.123 -        val _ = map is_number [a,b,c]
1.124 -        val T = ctyp_of_term c
1.125 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
1.126 -      in SOME (mk_meta_eq th) end
1.127 -  | Const(@{const_name HOL.less},_)\$_\$(Const(@{const_name "HOL.divide"},_)\$_\$_) =>
1.128 -    let
1.129 -      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
1.130 -        val _ = map is_number [a,b,c]
1.131 -        val T = ctyp_of_term c
1.132 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
1.133 -      in SOME (mk_meta_eq th) end
1.134 -  | Const(@{const_name HOL.less_eq},_)\$_\$(Const(@{const_name "HOL.divide"},_)\$_\$_) =>
1.135 -    let
1.136 -      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
1.137 -        val _ = map is_number [a,b,c]
1.138 -        val T = ctyp_of_term c
1.139 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
1.140 -      in SOME (mk_meta_eq th) end
1.141 -  | Const("op =",_)\$_\$(Const(@{const_name "HOL.divide"},_)\$_\$_) =>
1.142 -    let
1.143 -      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
1.144 -        val _ = map is_number [a,b,c]
1.145 -        val T = ctyp_of_term c
1.146 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
1.147 -      in SOME (mk_meta_eq th) end
1.148 -  | _ => NONE)
1.149 -  handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
1.150 -
1.152 -       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
1.154 -                     proc = proc, identifier = []}
1.155 -
1.157 -       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
1.159 -                     proc = proc2, identifier = []}
1.160 -
1.161 -val ord_frac_simproc =
1.162 -  make_simproc
1.163 -    {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
1.164 -             @{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"},
1.165 -             @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
1.166 -             @{cpat "?c \<le> (?a::(?'a::{field, ord}))/?b"},
1.167 -             @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
1.168 -             @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
1.169 -             name = "ord_frac_simproc", proc = proc3, identifier = []}
1.170 -
1.171 -val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of",
1.172 -               "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]
1.173 -
1.174 -val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0",
1.177 -                 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
1.178 -                 @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps}
1.179 -val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
1.180 -           @{thm "divide_Numeral1"},
1.181 -           @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
1.182 -           @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
1.183 -           @{thm "mult_num_frac"}, @{thm "mult_frac_num"},
1.184 -           @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
1.185 -           @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
1.186 -           @{thm "diff_def"}, @{thm "minus_divide_left"},
1.187 -           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
1.188 -
1.189 -local
1.190 -open Conv
1.191 -in
1.192 -val comp_conv = (Simplifier.rewrite
1.197 -                            ord_frac_simproc]
1.200 -  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
1.201  end
1.202 -
1.203 -fun numeral_is_const ct =
1.204 -  case term_of ct of
1.205 -   Const (@{const_name "HOL.divide"},_) \$ a \$ b =>
1.206 -     numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct)
1.207 - | Const (@{const_name "HOL.uminus"},_)\$t => numeral_is_const (Thm.dest_arg ct)
1.208 - | t => can HOLogic.dest_number t
1.209 -
1.210 -fun dest_const ct = ((case term_of ct of
1.211 -   Const (@{const_name "HOL.divide"},_) \$ a \$ b=>
1.212 -    Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
1.213 - | t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
1.214 -   handle TERM _ => error "ring_dest_const")
1.215 -
1.216 -fun mk_const phi cT x =
1.217 - let val (a, b) = Rat.quotient_of_rat x
1.218 - in if b = 1 then Numeral.mk_cnumber cT a
1.219 -    else Thm.capply
1.220 -         (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
1.221 -                     (Numeral.mk_cnumber cT a))
1.222 -         (Numeral.mk_cnumber cT b)
1.223 -  end
1.224 -
1.225 -in
1.226 - val field_comp_conv = comp_conv;
1.227 - val fieldgb_declaration =
1.228 -  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'}
1.229 -   {is_const = K numeral_is_const,
1.230 -    dest_const = K dest_const,
1.231 -    mk_const = mk_const,
1.232 -    conv = K (K comp_conv)}
1.233 -end;
1.234 -*}
1.235 -
1.236 -declaration{* fieldgb_declaration *}
1.237 -end
```
```     2.1 --- a/src/HOL/Groebner_Basis.thy	Mon Sep 29 12:31:58 2008 +0200
2.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Sep 29 12:31:59 2008 +0200
2.3 @@ -4,8 +4,9 @@
2.4  *)
2.5
2.6  header {* Semiring normalization and Groebner Bases *}
2.7 +
2.8  theory Groebner_Basis
2.9 -imports NatBin
2.10 +imports Arith_Tools
2.11  uses
2.12    "Tools/Groebner_Basis/misc.ML"
2.13    "Tools/Groebner_Basis/normalizer_data.ML"
2.14 @@ -461,4 +462,220 @@
2.15  declare zmod_eq_dvd_iff[algebra]
2.16  declare nat_mod_eq_iff[algebra]
2.17
2.18 +
2.19 +subsection{* Groebner Bases for fields *}
2.20 +
2.21 +interpretation class_fieldgb:
2.22 +  fieldgb["op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse"] apply (unfold_locales) by (simp_all add: divide_inverse)
2.23 +
2.24 +lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
2.25 +lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
2.26 +  by simp
2.27 +lemma mult_frac_frac: "((x::'a::{field,division_by_zero}) / y) * (z / w) = (x*z) / (y*w)"
2.28 +  by simp
2.29 +lemma mult_frac_num: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
2.30 +  by simp
2.31 +lemma mult_num_frac: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
2.32 +  by simp
2.33 +
2.34 +lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
2.35 +
2.36 +lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_by_zero}) / y + z = (x + z*y) / y"
2.38 +lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
2.40 +
2.41 +
2.42 +ML{*
2.43 +local
2.44 + val zr = @{cpat "0"}
2.45 + val zT = ctyp_of_term zr
2.46 + val geq = @{cpat "op ="}
2.47 + val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
2.51 +
2.52 + fun prove_nz ss T t =
2.53 +    let
2.54 +      val z = instantiate_cterm ([(zT,T)],[]) zr
2.55 +      val eq = instantiate_cterm ([(eqT,T)],[]) geq
2.56 +      val th = Simplifier.rewrite (ss addsimps simp_thms)
2.57 +           (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
2.58 +                  (Thm.capply (Thm.capply eq t) z)))
2.59 +    in equal_elim (symmetric th) TrueI
2.60 +    end
2.61 +
2.62 + fun proc phi ss ct =
2.63 +  let
2.64 +    val ((x,y),(w,z)) =
2.65 +         (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
2.66 +    val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
2.67 +    val T = ctyp_of_term x
2.68 +    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
2.69 +    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
2.70 +  in SOME (implies_elim (implies_elim th y_nz) z_nz)
2.71 +  end
2.72 +  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
2.73 +
2.74 + fun proc2 phi ss ct =
2.75 +  let
2.76 +    val (l,r) = Thm.dest_binop ct
2.77 +    val T = ctyp_of_term l
2.78 +  in (case (term_of l, term_of r) of
2.79 +      (Const(@{const_name "HOL.divide"},_)\$_\$_, _) =>
2.80 +        let val (x,y) = Thm.dest_binop l val z = r
2.81 +            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
2.82 +            val ynz = prove_nz ss T y
2.83 +        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
2.84 +        end
2.85 +     | (_, Const (@{const_name "HOL.divide"},_)\$_\$_) =>
2.86 +        let val (x,y) = Thm.dest_binop r val z = l
2.87 +            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
2.88 +            val ynz = prove_nz ss T y
2.89 +        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
2.90 +        end
2.91 +     | _ => NONE)
2.92 +  end
2.93 +  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
2.94 +
2.95 + fun is_number (Const(@{const_name "HOL.divide"},_)\$a\$b) = is_number a andalso is_number b
2.96 +   | is_number t = can HOLogic.dest_number t
2.97 +
2.98 + val is_number = is_number o term_of
2.99 +
2.100 + fun proc3 phi ss ct =
2.101 +  (case term_of ct of
2.102 +    Const(@{const_name HOL.less},_)\$(Const(@{const_name "HOL.divide"},_)\$_\$_)\$_ =>
2.103 +      let
2.104 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
2.105 +        val _ = map is_number [a,b,c]
2.106 +        val T = ctyp_of_term c
2.107 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
2.108 +      in SOME (mk_meta_eq th) end
2.109 +  | Const(@{const_name HOL.less_eq},_)\$(Const(@{const_name "HOL.divide"},_)\$_\$_)\$_ =>
2.110 +      let
2.111 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
2.112 +        val _ = map is_number [a,b,c]
2.113 +        val T = ctyp_of_term c
2.114 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
2.115 +      in SOME (mk_meta_eq th) end
2.116 +  | Const("op =",_)\$(Const(@{const_name "HOL.divide"},_)\$_\$_)\$_ =>
2.117 +      let
2.118 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
2.119 +        val _ = map is_number [a,b,c]
2.120 +        val T = ctyp_of_term c
2.121 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
2.122 +      in SOME (mk_meta_eq th) end
2.123 +  | Const(@{const_name HOL.less},_)\$_\$(Const(@{const_name "HOL.divide"},_)\$_\$_) =>
2.124 +    let
2.125 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
2.126 +        val _ = map is_number [a,b,c]
2.127 +        val T = ctyp_of_term c
2.128 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
2.129 +      in SOME (mk_meta_eq th) end
2.130 +  | Const(@{const_name HOL.less_eq},_)\$_\$(Const(@{const_name "HOL.divide"},_)\$_\$_) =>
2.131 +    let
2.132 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
2.133 +        val _ = map is_number [a,b,c]
2.134 +        val T = ctyp_of_term c
2.135 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
2.136 +      in SOME (mk_meta_eq th) end
2.137 +  | Const("op =",_)\$_\$(Const(@{const_name "HOL.divide"},_)\$_\$_) =>
2.138 +    let
2.139 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
2.140 +        val _ = map is_number [a,b,c]
2.141 +        val T = ctyp_of_term c
2.142 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
2.143 +      in SOME (mk_meta_eq th) end
2.144 +  | _ => NONE)
2.145 +  handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
2.146 +
2.148 +       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
2.150 +                     proc = proc, identifier = []}
2.151 +
2.153 +       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
2.155 +                     proc = proc2, identifier = []}
2.156 +
2.157 +val ord_frac_simproc =
2.158 +  make_simproc
2.159 +    {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
2.160 +             @{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"},
2.161 +             @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
2.162 +             @{cpat "?c \<le> (?a::(?'a::{field, ord}))/?b"},
2.163 +             @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
2.164 +             @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
2.165 +             name = "ord_frac_simproc", proc = proc3, identifier = []}
2.166 +
2.167 +val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of",
2.168 +               "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]
2.169 +
2.170 +val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0",
2.173 +                 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
2.174 +                 @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps}
2.175 +val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
2.176 +           @{thm "divide_Numeral1"},
2.177 +           @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
2.178 +           @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
2.179 +           @{thm "mult_num_frac"}, @{thm "mult_frac_num"},
2.180 +           @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
2.181 +           @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
2.182 +           @{thm "diff_def"}, @{thm "minus_divide_left"},
2.183 +           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
2.184 +
2.185 +local
2.186 +open Conv
2.187 +in
2.188 +val comp_conv = (Simplifier.rewrite
2.193 +                            ord_frac_simproc]
2.196 +  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
2.197  end
2.198 +
2.199 +fun numeral_is_const ct =
2.200 +  case term_of ct of
2.201 +   Const (@{const_name "HOL.divide"},_) \$ a \$ b =>
2.202 +     numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct)
2.203 + | Const (@{const_name "HOL.uminus"},_)\$t => numeral_is_const (Thm.dest_arg ct)
2.204 + | t => can HOLogic.dest_number t
2.205 +
2.206 +fun dest_const ct = ((case term_of ct of
2.207 +   Const (@{const_name "HOL.divide"},_) \$ a \$ b=>
2.208 +    Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
2.209 + | t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
2.210 +   handle TERM _ => error "ring_dest_const")
2.211 +
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 +
2.221 +in
2.222 + val field_comp_conv = comp_conv;
2.223 + val fieldgb_declaration =
2.224 +  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'}
2.225 +   {is_const = K numeral_is_const,
2.226 +    dest_const = K dest_const,
2.227 +    mk_const = mk_const,
2.228 +    conv = K (K comp_conv)}
2.229 +end;
2.230 +*}
2.231 +
2.232 +declaration fieldgb_declaration
2.233 +
2.234 +end
```
```     3.1 --- a/src/HOL/Library/Dense_Linear_Order.thy	Mon Sep 29 12:31:58 2008 +0200
3.2 +++ b/src/HOL/Library/Dense_Linear_Order.thy	Mon Sep 29 12:31:59 2008 +0200
3.3 @@ -7,17 +7,15 @@
3.4    and a quantifier elimination procedure in Ferrante and Rackoff style *}
3.5
3.6  theory Dense_Linear_Order
3.7 -imports Plain "~~/src/HOL/Presburger"
3.8 +imports Plain "~~/src/HOL/Groebner_Basis"
3.9  uses
3.10 -  "~~/src/HOL/Tools/Qelim/qelim.ML"
3.11    "~~/src/HOL/Tools/Qelim/langford_data.ML"
3.12    "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"
3.13    ("~~/src/HOL/Tools/Qelim/langford.ML")
3.14    ("~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML")
3.15  begin
3.16
3.17 -setup Langford_Data.setup
3.18 -setup Ferrante_Rackoff_Data.setup
3.19 +setup {* Langford_Data.setup #> Ferrante_Rackoff_Data.setup *}
3.20
3.21  context linorder
3.22  begin
```
```     4.1 --- a/src/HOL/Presburger.thy	Mon Sep 29 12:31:58 2008 +0200
4.2 +++ b/src/HOL/Presburger.thy	Mon Sep 29 12:31:59 2008 +0200
4.3 @@ -6,11 +6,10 @@
4.4  header {* Decision Procedure for Presburger Arithmetic *}
4.5
4.6  theory Presburger
4.7 -imports Arith_Tools SetInterval
4.8 +imports Groebner_Basis SetInterval
4.9  uses
4.10    "Tools/Qelim/cooper_data.ML"
4.11    "Tools/Qelim/generated_cooper.ML"
4.12 -  "Tools/Qelim/qelim.ML"
4.13    ("Tools/Qelim/cooper.ML")
4.14    ("Tools/Qelim/presburger.ML")
4.15  begin
```