clarified dependencies between arith tools
authorhaftmann
Mon Sep 29 12:31:59 2008 +0200 (2008-09-29)
changeset 2840209e4aa3ddc25
parent 28401 d5f39173444c
child 28403 da9ae7774513
clarified dependencies between arith tools
src/HOL/Arith_Tools.thy
src/HOL/Groebner_Basis.thy
src/HOL/Library/Dense_Linear_Order.thy
src/HOL/Presburger.thy
     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.41 -  by (simp add: add_divide_distrib)
    1.42 -lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
    1.43 -  by (simp add: add_divide_distrib)
    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.52 - val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
    1.53 - val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
    1.54 - val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
    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.151 -val add_frac_frac_simproc =
   1.152 -       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
   1.153 -                     name = "add_frac_frac_simproc",
   1.154 -                     proc = proc, identifier = []}
   1.155 -
   1.156 -val add_frac_num_simproc =
   1.157 -       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
   1.158 -                     name = "add_frac_num_simproc",
   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.175 -                 "add_Suc", "add_number_of_left", "mult_number_of_left",
   1.176 -                 "Suc_eq_add_numeral_1"])@
   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.193 -(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
   1.194 -              addsimps ths addsimps comp_arith addsimps simp_thms
   1.195 -              addsimprocs field_cancel_numeral_factors
   1.196 -               addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
   1.197 -                            ord_frac_simproc]
   1.198 -                addcongs [@{thm "if_weak_cong"}]))
   1.199 -then_conv (Simplifier.rewrite (HOL_basic_ss addsimps
   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.37 +  by (simp add: add_divide_distrib)
    2.38 +lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
    2.39 +  by (simp add: add_divide_distrib)
    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.48 + val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
    2.49 + val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
    2.50 + val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
    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.147 +val add_frac_frac_simproc =
   2.148 +       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
   2.149 +                     name = "add_frac_frac_simproc",
   2.150 +                     proc = proc, identifier = []}
   2.151 +
   2.152 +val add_frac_num_simproc =
   2.153 +       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
   2.154 +                     name = "add_frac_num_simproc",
   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.171 +                 "add_Suc", "add_number_of_left", "mult_number_of_left",
   2.172 +                 "Suc_eq_add_numeral_1"])@
   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.189 +(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
   2.190 +              addsimps ths addsimps comp_arith addsimps simp_thms
   2.191 +              addsimprocs field_cancel_numeral_factors
   2.192 +               addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
   2.193 +                            ord_frac_simproc]
   2.194 +                addcongs [@{thm "if_weak_cong"}]))
   2.195 +then_conv (Simplifier.rewrite (HOL_basic_ss addsimps
   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