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