src/HOL/Groebner_Basis.thy
changeset 28402 09e4aa3ddc25
parent 27666 1436d81d1294
child 28699 32b6a8f12c1c
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Sep 29 12:31:58 2008 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Sep 29 12:31:59 2008 +0200
     1.3 @@ -4,8 +4,9 @@
     1.4  *)
     1.5  
     1.6  header {* Semiring normalization and Groebner Bases *}
     1.7 +
     1.8  theory Groebner_Basis
     1.9 -imports NatBin
    1.10 +imports Arith_Tools
    1.11  uses
    1.12    "Tools/Groebner_Basis/misc.ML"
    1.13    "Tools/Groebner_Basis/normalizer_data.ML"
    1.14 @@ -461,4 +462,220 @@
    1.15  declare zmod_eq_dvd_iff[algebra]
    1.16  declare nat_mod_eq_iff[algebra]
    1.17  
    1.18 +
    1.19 +subsection{* Groebner Bases for fields *}
    1.20 +
    1.21 +interpretation class_fieldgb:
    1.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)
    1.23 +
    1.24 +lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
    1.25 +lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
    1.26 +  by simp
    1.27 +lemma mult_frac_frac: "((x::'a::{field,division_by_zero}) / y) * (z / w) = (x*z) / (y*w)"
    1.28 +  by simp
    1.29 +lemma mult_frac_num: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
    1.30 +  by simp
    1.31 +lemma mult_num_frac: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
    1.32 +  by simp
    1.33 +
    1.34 +lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
    1.35 +
    1.36 +lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_by_zero}) / y + z = (x + z*y) / y"
    1.37 +  by (simp add: add_divide_distrib)
    1.38 +lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
    1.39 +  by (simp add: add_divide_distrib)
    1.40 +
    1.41 +
    1.42 +ML{* 
    1.43 +local
    1.44 + val zr = @{cpat "0"}
    1.45 + val zT = ctyp_of_term zr
    1.46 + val geq = @{cpat "op ="}
    1.47 + val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
    1.48 + val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
    1.49 + val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
    1.50 + val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
    1.51 +
    1.52 + fun prove_nz ss T t =
    1.53 +    let
    1.54 +      val z = instantiate_cterm ([(zT,T)],[]) zr
    1.55 +      val eq = instantiate_cterm ([(eqT,T)],[]) geq
    1.56 +      val th = Simplifier.rewrite (ss addsimps simp_thms)
    1.57 +           (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
    1.58 +                  (Thm.capply (Thm.capply eq t) z)))
    1.59 +    in equal_elim (symmetric th) TrueI
    1.60 +    end
    1.61 +
    1.62 + fun proc phi ss ct =
    1.63 +  let
    1.64 +    val ((x,y),(w,z)) =
    1.65 +         (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
    1.66 +    val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
    1.67 +    val T = ctyp_of_term x
    1.68 +    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
    1.69 +    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
    1.70 +  in SOME (implies_elim (implies_elim th y_nz) z_nz)
    1.71 +  end
    1.72 +  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
    1.73 +
    1.74 + fun proc2 phi ss ct =
    1.75 +  let
    1.76 +    val (l,r) = Thm.dest_binop ct
    1.77 +    val T = ctyp_of_term l
    1.78 +  in (case (term_of l, term_of r) of
    1.79 +      (Const(@{const_name "HOL.divide"},_)$_$_, _) =>
    1.80 +        let val (x,y) = Thm.dest_binop l val z = r
    1.81 +            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    1.82 +            val ynz = prove_nz ss T y
    1.83 +        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
    1.84 +        end
    1.85 +     | (_, Const (@{const_name "HOL.divide"},_)$_$_) =>
    1.86 +        let val (x,y) = Thm.dest_binop r val z = l
    1.87 +            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    1.88 +            val ynz = prove_nz ss T y
    1.89 +        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
    1.90 +        end
    1.91 +     | _ => NONE)
    1.92 +  end
    1.93 +  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
    1.94 +
    1.95 + fun is_number (Const(@{const_name "HOL.divide"},_)$a$b) = is_number a andalso is_number b
    1.96 +   | is_number t = can HOLogic.dest_number t
    1.97 +
    1.98 + val is_number = is_number o term_of
    1.99 +
   1.100 + fun proc3 phi ss ct =
   1.101 +  (case term_of ct of
   1.102 +    Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
   1.103 +      let
   1.104 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   1.105 +        val _ = map is_number [a,b,c]
   1.106 +        val T = ctyp_of_term c
   1.107 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
   1.108 +      in SOME (mk_meta_eq th) end
   1.109 +  | Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
   1.110 +      let
   1.111 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   1.112 +        val _ = map is_number [a,b,c]
   1.113 +        val T = ctyp_of_term c
   1.114 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
   1.115 +      in SOME (mk_meta_eq th) end
   1.116 +  | Const("op =",_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
   1.117 +      let
   1.118 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   1.119 +        val _ = map is_number [a,b,c]
   1.120 +        val T = ctyp_of_term c
   1.121 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
   1.122 +      in SOME (mk_meta_eq th) end
   1.123 +  | Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
   1.124 +    let
   1.125 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   1.126 +        val _ = map is_number [a,b,c]
   1.127 +        val T = ctyp_of_term c
   1.128 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
   1.129 +      in SOME (mk_meta_eq th) end
   1.130 +  | Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
   1.131 +    let
   1.132 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   1.133 +        val _ = map is_number [a,b,c]
   1.134 +        val T = ctyp_of_term c
   1.135 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   1.136 +      in SOME (mk_meta_eq th) end
   1.137 +  | Const("op =",_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
   1.138 +    let
   1.139 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   1.140 +        val _ = map is_number [a,b,c]
   1.141 +        val T = ctyp_of_term c
   1.142 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
   1.143 +      in SOME (mk_meta_eq th) end
   1.144 +  | _ => NONE)
   1.145 +  handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
   1.146 +
   1.147 +val add_frac_frac_simproc =
   1.148 +       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
   1.149 +                     name = "add_frac_frac_simproc",
   1.150 +                     proc = proc, identifier = []}
   1.151 +
   1.152 +val add_frac_num_simproc =
   1.153 +       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
   1.154 +                     name = "add_frac_num_simproc",
   1.155 +                     proc = proc2, identifier = []}
   1.156 +
   1.157 +val ord_frac_simproc =
   1.158 +  make_simproc
   1.159 +    {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
   1.160 +             @{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"},
   1.161 +             @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
   1.162 +             @{cpat "?c \<le> (?a::(?'a::{field, ord}))/?b"},
   1.163 +             @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
   1.164 +             @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
   1.165 +             name = "ord_frac_simproc", proc = proc3, identifier = []}
   1.166 +
   1.167 +val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of",
   1.168 +               "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]
   1.169 +
   1.170 +val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0",
   1.171 +                 "add_Suc", "add_number_of_left", "mult_number_of_left",
   1.172 +                 "Suc_eq_add_numeral_1"])@
   1.173 +                 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
   1.174 +                 @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps}
   1.175 +val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
   1.176 +           @{thm "divide_Numeral1"},
   1.177 +           @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
   1.178 +           @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
   1.179 +           @{thm "mult_num_frac"}, @{thm "mult_frac_num"},
   1.180 +           @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
   1.181 +           @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
   1.182 +           @{thm "diff_def"}, @{thm "minus_divide_left"},
   1.183 +           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
   1.184 +
   1.185 +local
   1.186 +open Conv
   1.187 +in
   1.188 +val comp_conv = (Simplifier.rewrite
   1.189 +(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
   1.190 +              addsimps ths addsimps comp_arith addsimps simp_thms
   1.191 +              addsimprocs field_cancel_numeral_factors
   1.192 +               addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
   1.193 +                            ord_frac_simproc]
   1.194 +                addcongs [@{thm "if_weak_cong"}]))
   1.195 +then_conv (Simplifier.rewrite (HOL_basic_ss addsimps
   1.196 +  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
   1.197  end
   1.198 +
   1.199 +fun numeral_is_const ct =
   1.200 +  case term_of ct of
   1.201 +   Const (@{const_name "HOL.divide"},_) $ a $ b =>
   1.202 +     numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct)
   1.203 + | Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct)
   1.204 + | t => can HOLogic.dest_number t
   1.205 +
   1.206 +fun dest_const ct = ((case term_of ct of
   1.207 +   Const (@{const_name "HOL.divide"},_) $ a $ b=>
   1.208 +    Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   1.209 + | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
   1.210 +   handle TERM _ => error "ring_dest_const")
   1.211 +
   1.212 +fun mk_const phi cT x =
   1.213 + let val (a, b) = Rat.quotient_of_rat x
   1.214 + in if b = 1 then Numeral.mk_cnumber cT a
   1.215 +    else Thm.capply
   1.216 +         (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
   1.217 +                     (Numeral.mk_cnumber cT a))
   1.218 +         (Numeral.mk_cnumber cT b)
   1.219 +  end
   1.220 +
   1.221 +in
   1.222 + val field_comp_conv = comp_conv;
   1.223 + val fieldgb_declaration = 
   1.224 +  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'}
   1.225 +   {is_const = K numeral_is_const,
   1.226 +    dest_const = K dest_const,
   1.227 +    mk_const = mk_const,
   1.228 +    conv = K (K comp_conv)}
   1.229 +end;
   1.230 +*}
   1.231 +
   1.232 +declaration fieldgb_declaration
   1.233 +
   1.234 +end