# HG changeset patch # User chaieb # Date 1238904430 -3600 # Node ID dd5117e2d73e121d02d00d92e33046791f5cf814 # Parent 5106e13d400fa6af8afdc17cca9c645fd1f9edbc now deals with devision in fields diff -r 5106e13d400f -r dd5117e2d73e src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Fri Apr 03 18:03:29 2009 +0200 +++ b/src/HOL/Groebner_Basis.thy Sun Apr 05 05:07:10 2009 +0100 @@ -191,8 +191,7 @@ open Conv; -fun numeral_is_const ct = - can HOLogic.dest_number (Thm.term_of ct); +fun numeral_is_const ct = can HOLogic.dest_number (Thm.term_of ct); fun int_of_rat x = (case Rat.quotient_of_rat x of (i, 1) => i @@ -260,16 +259,22 @@ locale gb_field = gb_ring + fixes divide :: "'a \ 'a \ 'a" and inverse:: "'a \ 'a" - assumes divide: "divide x y = mul x (inverse y)" - and inverse: "inverse x = divide r1 x" + assumes divide_inverse: "divide x y = mul x (inverse y)" + and inverse_divide: "inverse x = divide r1 x" begin +lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" . + +lemmas field_rules = divide_inverse inverse_divide + lemmas gb_field_axioms' = gb_field_axioms [normalizer semiring ops: semiring_ops semiring rules: semiring_rules ring ops: ring_ops - ring rules: ring_rules] + ring rules: ring_rules + field ops: field_ops + field rules: field_rules] end @@ -393,6 +398,8 @@ semiring rules: semiring_rules ring ops: ring_ops ring rules: ring_rules + field ops: field_ops + field rules: field_rules idom rules: noteq_reduce add_scale_eq_noteq ideal rules: subr0_iff add_r0_iff] @@ -636,8 +643,8 @@ fun numeral_is_const ct = case term_of ct of Const (@{const_name "HOL.divide"},_) $ a $ b => - numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct) - | Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct) + can HOLogic.dest_number a andalso can HOLogic.dest_number b + | Const (@{const_name "HOL.inverse"},_)$t => can HOLogic.dest_number t | t => can HOLogic.dest_number t fun dest_const ct = ((case term_of ct of diff -r 5106e13d400f -r dd5117e2d73e src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Fri Apr 03 18:03:29 2009 +0200 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Apr 05 05:07:10 2009 +0100 @@ -5,8 +5,8 @@ signature GROEBNER = sig val ring_and_ideal_conv : - {idom: thm list, ring: cterm list * thm list, vars: cterm list, - semiring: cterm list * thm list, ideal : thm list} -> + {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list, + vars: cterm list, semiring: cterm list * thm list, ideal : thm list} -> (cterm -> Rat.rat) -> (Rat.rat -> cterm) -> conv -> conv -> {ring_conv : conv, @@ -581,7 +581,8 @@ (** main **) fun ring_and_ideal_conv - {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal} + {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), + field = (f_ops, f_rules), idom, ideal} dest_const mk_const ring_eq_conv ring_normalize_conv = let val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops; @@ -590,32 +591,37 @@ val (ring_sub_tm, ring_neg_tm) = (case r_ops of - [] => (@{cterm "True"}, @{cterm "True"}) - | [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat)); + [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat) + |_ => (@{cterm "True"}, @{cterm "True"})); + + val (field_div_tm, field_inv_tm) = + (case f_ops of + [div_pat, inv_pat] => (dest_fun2 div_pat, dest_fun inv_pat) + | _ => (@{cterm "True"}, @{cterm "True"})); val [idom_thm, neq_thm] = idom; val [idl_sub, idl_add0] = if length ideal = 2 then ideal else [eq_commute, eq_commute] - val ring_dest_neg = - fn t => let val (l,r) = dest_comb t in - if Term.could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t]) - end + fun ring_dest_neg t = + let val (l,r) = dest_comb t + in if Term.could_unify(term_of l,term_of ring_neg_tm) then r + else raise CTERM ("ring_dest_neg", [t]) + end val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm); -(* - fun ring_dest_inv t = + fun field_dest_inv t = let val (l,r) = dest_comb t in - if Term.could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv" + if Term.could_unify(term_of l, term_of field_inv_tm) then r + else raise CTERM ("field_dest_inv", [t]) end -*) val ring_dest_add = dest_binary ring_add_tm; val ring_mk_add = mk_binop ring_add_tm; val ring_dest_sub = dest_binary ring_sub_tm; val ring_mk_sub = mk_binop ring_sub_tm; val ring_dest_mul = dest_binary ring_mul_tm; val ring_mk_mul = mk_binop ring_mul_tm; -(* val ring_dest_div = dest_binary ring_div_tm; - val ring_mk_div = mk_binop ring_div_tm;*) + val field_dest_div = dest_binary field_div_tm; + val field_mk_div = mk_binop field_div_tm; val ring_dest_pow = dest_binary ring_pow_tm; val ring_mk_pow = mk_binop ring_pow_tm ; fun grobvars tm acc = @@ -625,16 +631,16 @@ else if can ring_dest_add tm orelse can ring_dest_sub tm orelse can ring_dest_mul tm then grobvars (dest_arg1 tm) (grobvars (dest_arg tm) acc) -(* else if can ring_dest_inv tm - then - let val gvs = grobvars (dest_arg tm) [] in - if gvs = [] then acc else tm::acc - end - else if can ring_dest_div tm then - let val lvs = grobvars (dest_arg1 tm) acc - val gvs = grobvars (dest_arg tm) [] - in if gvs = [] then lvs else tm::acc - end *) + else if can field_dest_inv tm + then + let val gvs = grobvars (dest_arg tm) [] + in if null gvs then acc else tm::acc + end + else if can field_dest_div tm then + let val lvs = grobvars (dest_arg1 tm) acc + val gvs = grobvars (dest_arg tm) [] + in if null gvs then lvs else tm::acc + end else tm::acc ; fun grobify_term vars tm = @@ -648,8 +654,8 @@ ((grob_neg(grobify_term vars (ring_dest_neg tm))) handle CTERM _ => ( -(* (grob_inv(grobify_term vars (ring_dest_inv tm))) - handle CTERM _ => *) + (grob_inv(grobify_term vars (field_dest_inv tm))) + handle CTERM _ => ((let val (l,r) = ring_dest_add tm in grob_add (grobify_term vars l) (grobify_term vars r) end) @@ -662,18 +668,15 @@ in grob_mul (grobify_term vars l) (grobify_term vars r) end) handle CTERM _ => - ( -(* (let val (l,r) = ring_dest_div tm + ( (let val (l,r) = field_dest_div tm in grob_div (grobify_term vars l) (grobify_term vars r) end) - handle CTERM _ => *) + handle CTERM _ => ((let val (l,r) = ring_dest_pow tm in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r) end) handle CTERM _ => error "grobify_term: unknown or invalid term"))))))))); val eq_tm = idom_thm |> concl |> dest_arg |> dest_arg |> dest_fun2; -(*ring_integral |> hd |> concl |> dest_arg - |> dest_abs NONE |> snd |> dest_fun |> dest_fun; *) val dest_eq = dest_binary eq_tm; fun grobify_equation vars tm = diff -r 5106e13d400f -r dd5117e2d73e src/HOL/Tools/Groebner_Basis/normalizer.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Fri Apr 03 18:03:29 2009 +0200 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Sun Apr 05 05:07:10 2009 +0100 @@ -14,7 +14,7 @@ val semiring_normalize_ord_wrapper : Proof.context -> NormalizerData.entry -> (cterm -> cterm -> bool) -> conv val semiring_normalizers_conv : - cterm list -> cterm list * thm list -> cterm list * thm list -> + cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list -> (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) -> {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} end @@ -71,7 +71,7 @@ (* The main function! *) -fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) +fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules) (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) = let @@ -97,8 +97,7 @@ val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') = (case (r_ops, r_rules) of - ([], []) => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm) - | ([sub_pat, neg_pat], [neg_mul, sub_add]) => + ([sub_pat, neg_pat], [neg_mul, sub_add]) => let val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat) val neg_tm = Thm.dest_fun neg_pat @@ -106,7 +105,18 @@ val is_sub = is_binop sub_tm in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg, sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg) - end); + end + | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)); + +val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = + (case (f_ops, f_rules) of + ([divide_pat, inverse_pat], [div_inv, inv_div]) => + let val div_tm = funpow 2 Thm.dest_fun divide_pat + val inv_tm = Thm.dest_fun inverse_pat + in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm) + end + | _ => (TrueI, TrueI, true_tm, true_tm, K false)); + in fn variable_order => let @@ -579,6 +589,10 @@ let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) in transitive th1 (polynomial_neg_conv (concl th1)) end + else if lopr aconvc inverse_tm then + let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) + in transitive th1 (semiring_mul_conv (concl th1)) + end else if not(is_comb lopr) then reflexive tm else @@ -588,6 +602,14 @@ let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r in transitive th1 (polynomial_pow_conv (concl th1)) end + else if opr aconvc divide_tm + then + let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) + (polynomial_conv r) + val th2 = (rewr_conv divide_inverse then_conv polynomial_mul_conv) + (Thm.rhs_of th1) + in transitive th1 th2 + end else if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm then @@ -616,7 +638,7 @@ fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS; -fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, +fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = let val pow_conv = @@ -625,10 +647,10 @@ (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34]) then_conv conv ctxt val dat = (is_const, conv ctxt, conv ctxt, pow_conv) - in semiring_normalizers_conv vars semiring ring dat ord end; + in semiring_normalizers_conv vars semiring ring field dat ord end; -fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = - #main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord); +fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = + #main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord); fun semiring_normalize_wrapper ctxt data = semiring_normalize_ord_wrapper ctxt data simple_cterm_ord; diff -r 5106e13d400f -r dd5117e2d73e src/HOL/Tools/Groebner_Basis/normalizer_data.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Fri Apr 03 18:03:29 2009 +0200 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Apr 05 05:07:10 2009 +0100 @@ -11,7 +11,7 @@ val get: Proof.context -> simpset * (thm * entry) list val match: Proof.context -> cterm -> entry option val del: attribute - val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list, ideal: thm list} + val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute val funs: thm -> {is_const: morphism -> cterm -> bool, dest_const: morphism -> cterm -> Rat.rat, @@ -29,6 +29,7 @@ {vars: cterm list, semiring: cterm list * thm list, ring: cterm list * thm list, + field: cterm list * thm list, idom: thm list, ideal: thm list} * {is_const: cterm -> bool, @@ -57,7 +58,7 @@ let fun match_inst ({vars, semiring = (sr_ops, sr_rules), - ring = (r_ops, r_rules), idom, ideal}, + ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal}, fns as {is_const, dest_const, mk_const, conv}) pat = let fun h instT = @@ -68,11 +69,12 @@ val vars' = map substT_cterm vars; val semiring' = (map substT_cterm sr_ops, map substT sr_rules); val ring' = (map substT_cterm r_ops, map substT r_rules); + val field' = (map substT_cterm f_ops, map substT f_rules); val idom' = map substT idom; val ideal' = map substT ideal; val result = ({vars = vars', semiring = semiring', - ring = ring', idom = idom', ideal = ideal'}, fns); + ring = ring', field = field', idom = idom', ideal = ideal'}, fns); in SOME result end in (case try Thm.match (pat, tm) of NONE => NONE @@ -80,8 +82,8 @@ end; fun match_struct (_, - entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) = - get_first (match_inst entry) (sr_ops @ r_ops); + entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) = + get_first (match_inst entry) (sr_ops @ r_ops @ f_ops); in get_first match_struct (snd (get ctxt)) end; @@ -91,6 +93,7 @@ val ringN = "ring"; val idomN = "idom"; val idealN = "ideal"; +val fieldN = "field"; fun undefined _ = raise Match; @@ -103,7 +106,8 @@ val del_ss = Thm.declaration_attribute (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data))); -fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal} = +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), + field = (f_ops, f_rules), idom, ideal} = Thm.declaration_attribute (fn key => fn context => context |> Data.map let val ctxt = Context.proof_of context; @@ -119,11 +123,14 @@ check_rules semiringN sr_rules 37 andalso check_ops ringN r_ops 2 andalso check_rules ringN r_rules 2 andalso + check_ops fieldN f_ops 2 andalso + check_rules fieldN f_rules 2 andalso check_rules idomN idom 2; val mk_meta = LocalDefs.meta_rewrite_rule ctxt; val sr_rules' = map mk_meta sr_rules; val r_rules' = map mk_meta r_rules; + val f_rules' = map mk_meta f_rules; fun rule i = nth sr_rules' (i - 1); @@ -140,11 +147,12 @@ val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; val semiring = (sr_ops, sr_rules'); val ring = (r_ops, r_rules'); + val field = (f_ops, f_rules'); val ideal' = map (symmetric o mk_meta) ideal in del_data key #> apsnd (cons (key, ({vars = vars, semiring = semiring, - ring = ring, idom = idom, ideal = ideal'}, + ring = ring, field = field, idom = idom, ideal = ideal'}, {is_const = undefined, dest_const = undefined, mk_const = undefined, conv = undefined}))) end); @@ -182,6 +190,7 @@ val any_keyword = keyword2 semiringN opsN || keyword2 semiringN rulesN || keyword2 ringN opsN || keyword2 ringN rulesN || + keyword2 fieldN opsN || keyword2 fieldN rulesN || keyword2 idomN rulesN || keyword2 idealN rulesN; val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; @@ -198,9 +207,12 @@ (keyword2 semiringN rulesN |-- thms)) -- (optional (keyword2 ringN opsN |-- terms) -- optional (keyword2 ringN rulesN |-- thms)) -- + (optional (keyword2 fieldN opsN |-- terms) -- + optional (keyword2 fieldN rulesN |-- thms)) -- optional (keyword2 idomN rulesN |-- thms) -- optional (keyword2 idealN rulesN |-- thms) - >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl})) + >> (fn ((((sr, r), f), id), idl) => + add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) "semiring normalizer data"; end;