# HG changeset patch # User haftmann # Date 1273219199 -7200 # Node ID 47ba1770da8e4a4464bca536807e01444c916907 # Parent 1b69f78be286b4a8402a91555186b359f56a9118# Parent 34c36a5cb808b56e1bad36a5355474f9d8ae546f merged diff -r 1b69f78be286 -r 47ba1770da8e NEWS --- a/NEWS Thu May 06 11:08:19 2010 -0700 +++ b/NEWS Fri May 07 09:59:59 2010 +0200 @@ -140,6 +140,8 @@ *** HOL *** +* Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY. + * Theory 'Finite_Set': various folding_* locales facilitate the application of the various fold combinators on finite sets. diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Fields.thy --- a/src/HOL/Fields.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Fields.thy Fri May 07 09:59:59 2010 +0200 @@ -234,6 +234,18 @@ "1 = a / b \ b \ 0 \ a = b" by (simp add: eq_commute [of 1]) +lemma times_divide_times_eq: + "(x / y) * (z / w) = (x * z) / (y * w)" + by simp + +lemma add_frac_num: + "y \ 0 \ x / y + z = (x + z * y) / y" + by (simp add: add_divide_distrib) + +lemma add_num_frac: + "y \ 0 \ z + x / y = (x + z * y) / y" + by (simp add: add_divide_distrib add.commute) + end diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Groebner_Basis.thy Fri May 07 09:59:59 2010 +0200 @@ -5,20 +5,17 @@ header {* Semiring normalization and Groebner Bases *} theory Groebner_Basis -imports Numeral_Simprocs +imports Numeral_Simprocs Nat_Transfer uses - "Tools/Groebner_Basis/misc.ML" - "Tools/Groebner_Basis/normalizer_data.ML" - ("Tools/Groebner_Basis/normalizer.ML") + "Tools/Groebner_Basis/normalizer.ML" ("Tools/Groebner_Basis/groebner.ML") begin subsection {* Semiring normalization *} -setup NormalizerData.setup +setup Normalizer.setup - -locale gb_semiring = +locale normalizing_semiring = fixes add mul pwr r0 r1 assumes add_a:"(add x (add y z) = add (add x y) z)" and add_c: "add x y = add y x" and add_0:"add r0 x = x" @@ -59,9 +56,6 @@ thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc) qed - -subsubsection {* Declaring the abstract theory *} - lemma semiring_ops: shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)" and "TERM r0" and "TERM r1" . @@ -156,71 +150,21 @@ qed -lemmas gb_semiring_axioms' = - gb_semiring_axioms [normalizer +lemmas normalizing_semiring_axioms' = + normalizing_semiring_axioms [normalizer semiring ops: semiring_ops semiring rules: semiring_rules] end -interpretation class_semiring: gb_semiring - "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1" - proof qed (auto simp add: algebra_simps) - -lemmas nat_arith = - add_nat_number_of - diff_nat_number_of - mult_nat_number_of - eq_nat_number_of - less_nat_number_of - -lemma not_iszero_Numeral1: "\ iszero (Numeral1::'a::number_ring)" - by simp - -lemmas comp_arith = - Let_def arith_simps nat_arith rel_simps neg_simps if_False - if_True add_0 add_Suc add_number_of_left mult_number_of_left - numeral_1_eq_1[symmetric] Suc_eq_plus1 - numeral_0_eq_0[symmetric] numerals[symmetric] - iszero_simps not_iszero_Numeral1 - -lemmas semiring_norm = comp_arith - -ML {* -local - -open Conv; +sublocale comm_semiring_1 + < normalizing!: normalizing_semiring plus times power zero one +proof +qed (simp_all add: algebra_simps) -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 - | _ => error "int_of_rat: bad int"); - -val numeral_conv = - Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}) then_conv - Simplifier.rewrite (HOL_basic_ss addsimps - (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)})); - -in +declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *} -fun normalizer_funs key = - NormalizerData.funs key - {is_const = fn phi => numeral_is_const, - dest_const = fn phi => fn ct => - Rat.rat_of_int (snd - (HOLogic.dest_number (Thm.term_of ct) - handle TERM _ => error "ring_dest_const")), - mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT (int_of_rat x), - conv = fn phi => K numeral_conv} - -end -*} - -declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms'} *} - - -locale gb_ring = gb_semiring + +locale normalizing_ring = normalizing_semiring + fixes sub :: "'a \ 'a \ 'a" and neg :: "'a \ 'a" assumes neg_mul: "neg x = mul (neg r1) x" @@ -231,8 +175,8 @@ lemmas ring_rules = neg_mul sub_add -lemmas gb_ring_axioms' = - gb_ring_axioms [normalizer +lemmas normalizing_ring_axioms' = + normalizing_ring_axioms [normalizer semiring ops: semiring_ops semiring rules: semiring_rules ring ops: ring_ops @@ -240,23 +184,14 @@ end - -interpretation class_ring: gb_ring "op +" "op *" "op ^" - "0::'a::{comm_semiring_1,number_ring}" 1 "op -" "uminus" - proof qed simp_all - - -declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *} +sublocale comm_ring_1 + < normalizing!: normalizing_ring plus times power zero one minus uminus +proof +qed (simp_all add: diff_minus) -use "Tools/Groebner_Basis/normalizer.ML" - +declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *} -method_setup sring_norm = {* - Scan.succeed (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac) -*} "semiring normalizer" - - -locale gb_field = gb_ring + +locale normalizing_field = normalizing_ring + fixes divide :: "'a \ 'a \ 'a" and inverse:: "'a \ 'a" assumes divide_inverse: "divide x y = mul x (inverse y)" @@ -267,8 +202,8 @@ lemmas field_rules = divide_inverse inverse_divide -lemmas gb_field_axioms' = - gb_field_axioms [normalizer +lemmas normalizing_field_axioms' = + normalizing_field_axioms [normalizer semiring ops: semiring_ops semiring rules: semiring_rules ring ops: ring_ops @@ -278,10 +213,7 @@ end - -subsection {* Groebner Bases *} - -locale semiringb = gb_semiring + +locale normalizing_semiring_cancel = normalizing_semiring + assumes add_cancel: "add (x::'a) y = add x z \ y = z" and add_mul_solve: "add (mul w y) (mul x z) = add (mul w z) (mul x y) \ w = x \ y = z" @@ -313,22 +245,23 @@ thus "x = add x a \ a = r0" by (auto simp add: add_c add_0) qed -declare gb_semiring_axioms' [normalizer del] +declare normalizing_semiring_axioms' [normalizer del] -lemmas semiringb_axioms' = semiringb_axioms [normalizer - semiring ops: semiring_ops - semiring rules: semiring_rules - idom rules: noteq_reduce add_scale_eq_noteq] +lemmas normalizing_semiring_cancel_axioms' = + normalizing_semiring_cancel_axioms [normalizer + semiring ops: semiring_ops + semiring rules: semiring_rules + idom rules: noteq_reduce add_scale_eq_noteq] end -locale ringb = semiringb + gb_ring + +locale normalizing_ring_cancel = normalizing_semiring_cancel + normalizing_ring + assumes subr0_iff: "sub x y = r0 \ x = y" begin -declare gb_ring_axioms' [normalizer del] +declare normalizing_ring_axioms' [normalizer del] -lemmas ringb_axioms' = ringb_axioms [normalizer +lemmas normalizing_ring_cancel_axioms' = normalizing_ring_cancel_axioms [normalizer semiring ops: semiring_ops semiring rules: semiring_rules ring ops: ring_ops @@ -338,33 +271,24 @@ end - -lemma no_zero_divirors_neq0: - assumes az: "(a::'a::no_zero_divisors) \ 0" - and ab: "a*b = 0" shows "b = 0" -proof - - { assume bz: "b \ 0" - from no_zero_divisors [OF az bz] ab have False by blast } - thus "b = 0" by blast -qed +sublocale idom + < normalizing!: normalizing_ring_cancel plus times power zero one minus uminus +proof + fix w x y z + show "w * y + x * z = w * z + x * y \ w = x \ y = z" + proof + assume "w * y + x * z = w * z + x * y" + then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps) + then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) + then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps) + then have "y - z = 0 \ w - x = 0" by (rule divisors_zero) + then show "w = x \ y = z" by auto + qed (auto simp add: add_ac) +qed (simp_all add: algebra_simps) -interpretation class_ringb: ringb - "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus" -proof(unfold_locales, simp add: algebra_simps, auto) - fix w x y z ::"'a::{idom,number_ring}" - assume p: "w * y + x * z = w * z + x * y" and ynz: "y \ z" - hence ynz': "y - z \ 0" by simp - from p have "w * y + x* z - w*z - x*y = 0" by simp - hence "w* (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) - hence "(y - z) * (w - x) = 0" by (simp add: algebra_simps) - with no_zero_divirors_neq0 [OF ynz'] - have "w - x = 0" by blast - thus "w = x" by simp -qed +declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *} -declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *} - -interpretation natgb: semiringb +interpretation normalizing_nat!: normalizing_semiring_cancel "op +" "op *" "op ^" "0::nat" "1" proof (unfold_locales, simp add: algebra_simps) fix w x y z ::"nat" @@ -386,14 +310,14 @@ thus "(w * y + x * z = w * z + x * y) = (w = x \ y = z)" by auto qed -declaration {* normalizer_funs @{thm natgb.semiringb_axioms'} *} +declaration {* Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *} -locale fieldgb = ringb + gb_field +locale normalizing_field_cancel = normalizing_ring_cancel + normalizing_field begin -declare gb_field_axioms' [normalizer del] +declare normalizing_field_axioms' [normalizer del] -lemmas fieldgb_axioms' = fieldgb_axioms [normalizer +lemmas normalizing_field_cancel_axioms' = normalizing_field_cancel_axioms [normalizer semiring ops: semiring_ops semiring rules: semiring_rules ring ops: ring_ops @@ -405,8 +329,18 @@ end +sublocale field + < normalizing!: normalizing_field_cancel plus times power zero one minus uminus divide inverse +proof +qed (simp_all add: divide_inverse) + +declaration {* Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *} + + +subsection {* Groebner Bases *} lemmas bool_simps = simp_thms(1-34) + lemma dnf: "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))" "(P \ Q) = (Q \ P)" "(P \ Q) = (Q \ P)" @@ -423,23 +357,16 @@ "P \ False \ \ P" "\ P \ (P \ False)" by auto -use "Tools/Groebner_Basis/groebner.ML" -method_setup algebra = -{* -let - fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () - val addN = "add" - val delN = "del" - val any_keyword = keyword addN || keyword delN - val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; -in - ((Scan.optional (keyword addN |-- thms) []) -- - (Scan.optional (keyword delN |-- thms) [])) >> - (fn (add_ths, del_ths) => fn ctxt => - SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt)) -end -*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" +ML {* +structure Algebra_Simplification = Named_Thms( + val name = "algebra" + val description = "pre-simplification rules for algebraic methods" +) +*} + +setup Algebra_Simplification.setup + declare dvd_def[algebra] declare dvd_eq_mod_eq_0[symmetric, algebra] declare mod_div_trivial[algebra] @@ -468,222 +395,9 @@ declare zmod_eq_dvd_iff[algebra] declare nat_mod_eq_iff[algebra] -subsection{* Groebner Bases for fields *} - -interpretation class_fieldgb: - fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse) - -lemma divide_Numeral1: "(x::'a::{field, number_ring}) / Numeral1 = x" by simp -lemma divide_Numeral0: "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0" - by simp -lemma mult_frac_frac: "((x::'a::field_inverse_zero) / y) * (z / w) = (x*z) / (y*w)" - by simp -lemma mult_frac_num: "((x::'a::field_inverse_zero) / y) * z = (x*z) / y" - by simp -lemma mult_num_frac: "((x::'a::field_inverse_zero) / y) * z = (x*z) / y" - by simp - -lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp - -lemma add_frac_num: "y\ 0 \ (x::'a::field_inverse_zero) / y + z = (x + z*y) / y" - by (simp add: add_divide_distrib) -lemma add_num_frac: "y\ 0 \ z + (x::'a::field_inverse_zero) / y = (x + z*y) / y" - by (simp add: add_divide_distrib) - -ML {* -let open Conv -in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) (@{thm field_divide_inverse} RS sym) -end -*} - -ML{* -local - val zr = @{cpat "0"} - val zT = ctyp_of_term zr - val geq = @{cpat "op ="} - val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd - val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} - val add_frac_num = mk_meta_eq @{thm "add_frac_num"} - val add_num_frac = mk_meta_eq @{thm "add_num_frac"} - - fun prove_nz ss T t = - let - val z = instantiate_cterm ([(zT,T)],[]) zr - val eq = instantiate_cterm ([(eqT,T)],[]) geq - val th = Simplifier.rewrite (ss addsimps @{thms simp_thms}) - (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} - (Thm.capply (Thm.capply eq t) z))) - in equal_elim (symmetric th) TrueI - end - - fun proc phi ss ct = - let - val ((x,y),(w,z)) = - (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct - val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] - val T = ctyp_of_term x - val [y_nz, z_nz] = map (prove_nz ss T) [y, z] - val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq - in SOME (implies_elim (implies_elim th y_nz) z_nz) - end - handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE - - fun proc2 phi ss ct = - let - val (l,r) = Thm.dest_binop ct - val T = ctyp_of_term l - in (case (term_of l, term_of r) of - (Const(@{const_name Rings.divide},_)$_$_, _) => - let val (x,y) = Thm.dest_binop l val z = r - val _ = map (HOLogic.dest_number o term_of) [x,y,z] - val ynz = prove_nz ss T y - in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) - end - | (_, Const (@{const_name Rings.divide},_)$_$_) => - let val (x,y) = Thm.dest_binop r val z = l - val _ = map (HOLogic.dest_number o term_of) [x,y,z] - val ynz = prove_nz ss T y - in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) - end - | _ => NONE) - end - handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE - - fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b - | is_number t = can HOLogic.dest_number t - - val is_number = is_number o term_of +use "Tools/Groebner_Basis/groebner.ML" - fun proc3 phi ss ct = - (case term_of ct of - Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => - let - val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} - in SOME (mk_meta_eq th) end - | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => - let - val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} - in SOME (mk_meta_eq th) end - | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => - let - val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} - in SOME (mk_meta_eq th) end - | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => - let - val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} - in SOME (mk_meta_eq th) end - | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => - let - val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} - in SOME (mk_meta_eq th) end - | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) => - let - val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} - in SOME (mk_meta_eq th) end - | _ => NONE) - handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE - -val add_frac_frac_simproc = - make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], - name = "add_frac_frac_simproc", - proc = proc, identifier = []} - -val add_frac_num_simproc = - make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], - name = "add_frac_num_simproc", - proc = proc2, identifier = []} - -val ord_frac_simproc = - make_simproc - {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, - @{cpat "(?a::(?'a::{field, ord}))/?b \ ?c"}, - @{cpat "?c < (?a::(?'a::{field, ord}))/?b"}, - @{cpat "?c \ (?a::(?'a::{field, ord}))/?b"}, - @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"}, - @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}], - name = "ord_frac_simproc", proc = proc3, identifier = []} - -local -open Conv -in - -val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, - @{thm "divide_Numeral1"}, - @{thm "divide_zero"}, @{thm "divide_Numeral0"}, - @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"}, - @{thm "mult_num_frac"}, @{thm "mult_frac_num"}, - @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"}, - @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"}, - @{thm "diff_def"}, @{thm "minus_divide_left"}, - @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym, - @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, - fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) - (@{thm field_divide_inverse} RS sym)] - -val comp_conv = (Simplifier.rewrite -(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} - addsimps ths addsimps @{thms simp_thms} - addsimprocs Numeral_Simprocs.field_cancel_numeral_factors - addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, - ord_frac_simproc] - addcongs [@{thm "if_weak_cong"}])) -then_conv (Simplifier.rewrite (HOL_basic_ss addsimps - [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)})) -end - -fun numeral_is_const ct = - case term_of ct of - Const (@{const_name Rings.divide},_) $ a $ b => - can HOLogic.dest_number a andalso can HOLogic.dest_number b - | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t - | t => can HOLogic.dest_number t - -fun dest_const ct = ((case term_of ct of - Const (@{const_name Rings.divide},_) $ a $ b=> - Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) - | Const (@{const_name Rings.inverse},_)$t => - Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t))) - | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) - handle TERM _ => error "ring_dest_const") - -fun mk_const phi cT x = - let val (a, b) = Rat.quotient_of_rat x - in if b = 1 then Numeral.mk_cnumber cT a - else Thm.capply - (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) - (Numeral.mk_cnumber cT a)) - (Numeral.mk_cnumber cT b) - end - -in - val field_comp_conv = comp_conv; - val fieldgb_declaration = - NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'} - {is_const = K numeral_is_const, - dest_const = K dest_const, - mk_const = mk_const, - conv = K (K comp_conv)} -end; -*} - -declaration fieldgb_declaration +method_setup algebra = Groebner.algebra_method + "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" end diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Int.thy --- a/src/HOL/Int.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Int.thy Fri May 07 09:59:59 2010 +0200 @@ -1063,20 +1063,24 @@ text {* First version by Norbert Voelker *} -definition (*for simplifying equalities*) - iszero :: "'a\semiring_1 \ bool" -where +definition (*for simplifying equalities*) iszero :: "'a\semiring_1 \ bool" where "iszero z \ z = 0" lemma iszero_0: "iszero 0" -by (simp add: iszero_def) - -lemma not_iszero_1: "~ iszero 1" -by (simp add: iszero_def eq_commute) + by (simp add: iszero_def) + +lemma iszero_Numeral0: "iszero (Numeral0 :: 'a::number_ring)" + by (simp add: iszero_0) + +lemma not_iszero_1: "\ iszero 1" + by (simp add: iszero_def) + +lemma not_iszero_Numeral1: "\ iszero (Numeral1 :: 'a::number_ring)" + by (simp add: not_iszero_1) lemma eq_number_of_eq [simp]: "((number_of x::'a::number_ring) = number_of y) = - iszero (number_of (x + uminus y) :: 'a)" + iszero (number_of (x + uminus y) :: 'a)" unfolding iszero_def number_of_add number_of_minus by (simp add: algebra_simps) @@ -2021,6 +2025,14 @@ lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard] +lemma divide_Numeral1: + "(x::'a::{field, number_ring}) / Numeral1 = x" + by simp + +lemma divide_Numeral0: + "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0" + by simp + subsection {* The divides relation *} diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/IsaMakefile Fri May 07 09:59:59 2010 +0200 @@ -284,9 +284,7 @@ Tools/ATP_Manager/atp_manager.ML \ Tools/ATP_Manager/atp_systems.ML \ Tools/Groebner_Basis/groebner.ML \ - Tools/Groebner_Basis/misc.ML \ Tools/Groebner_Basis/normalizer.ML \ - Tools/Groebner_Basis/normalizer_data.ML \ Tools/choice_specification.ML \ Tools/int_arith.ML \ Tools/list_code.ML \ diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri May 07 09:59:59 2010 +0200 @@ -1195,7 +1195,7 @@ fun real_nonlinear_prover proof_method ctxt = let val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main) @@ -1222,7 +1222,7 @@ in (let val th = tryfind trivial_axiom (keq @ klep @ kltp) in - (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th, RealArith.Trivial) + (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv Normalizer.field_comp_conv) th, RealArith.Trivial) end) handle Failure _ => (let val proof = @@ -1310,7 +1310,7 @@ fun real_nonlinear_subst_prover prover ctxt = let val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Library/normarith.ML --- a/src/HOL/Library/normarith.ML Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Library/normarith.ML Fri May 07 09:59:59 2010 +0200 @@ -167,8 +167,8 @@ (* FIXME : Should be computed statically!! *) val real_poly_conv = Normalizer.semiring_normalize_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) - in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv))) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) + in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Normalizer.field_comp_conv then_conv real_poly_conv))) end; fun absc cv ct = case term_of ct of @@ -190,8 +190,8 @@ val apply_pth5 = rewr_conv @{thm pth_5}; val apply_pth6 = rewr_conv @{thm pth_6}; val apply_pth7 = rewrs_conv @{thms pth_7}; - val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); - val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv field_comp_conv); + val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Normalizer.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); + val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Normalizer.field_comp_conv); val apply_ptha = rewr_conv @{thm pth_a}; val apply_pthb = rewrs_conv @{thms pth_b}; val apply_pthc = rewrs_conv @{thms pth_c}; @@ -204,7 +204,7 @@ | _ => error "headvector: non-canonical term" fun vector_cmul_conv ct = - ((apply_pth5 then_conv arg1_conv field_comp_conv) else_conv + ((apply_pth5 then_conv arg1_conv Normalizer.field_comp_conv) else_conv (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct fun vector_add_conv ct = apply_pth7 ct @@ -278,7 +278,7 @@ (* FIXME: Should be computed statically!!*) val real_poly_conv = Normalizer.semiring_normalize_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" @@ -384,7 +384,7 @@ let val real_poly_neg_conv = #neg (Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord) val (th1,th2) = conj_pair(rawrule th) in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc end @@ -396,7 +396,7 @@ fun init_conv ctxt = Simplifier.rewrite (Simplifier.context ctxt (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) - then_conv field_comp_conv + then_conv Normalizer.field_comp_conv then_conv nnf_conv fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Library/positivstellensatz.ML Fri May 07 09:59:59 2010 +0200 @@ -748,10 +748,10 @@ fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord in gen_real_arith ctxt - (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv, + (cterm_of_rat, Normalizer.field_comp_conv, Normalizer.field_comp_conv, Normalizer.field_comp_conv, main,neg,add,mul, prover) end; diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Metis_Examples/BT.thy --- a/src/HOL/Metis_Examples/BT.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Metis_Examples/BT.thy Fri May 07 09:59:59 2010 +0200 @@ -88,7 +88,7 @@ case Lf thus ?case by (metis reflect.simps(1)) next case (Br a t1 t2) thus ?case - by (metis class_semiring.semiring_rules(24) n_nodes.simps(2) reflect.simps(2)) + by (metis normalizing.semiring_rules(24) n_nodes.simps(2) reflect.simps(2)) qed declare [[ atp_problem_prefix = "BT__depth_reflect" ]] diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Metis_Examples/BigO.thy --- a/src/HOL/Metis_Examples/BigO.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Metis_Examples/BigO.thy Fri May 07 09:59:59 2010 +0200 @@ -41,7 +41,7 @@ fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" have F1: "\x\<^isub>1\'a\linordered_idom. 0 \ \x\<^isub>1\" by (metis abs_ge_zero) - have F2: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F2: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) have F3: "\x\<^isub>1 x\<^isub>3. x\<^isub>3 \ \h x\<^isub>1\ \ x\<^isub>3 \ c * \f x\<^isub>1\" by (metis A1 order_trans) have F4: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" by (metis abs_mult) @@ -70,7 +70,7 @@ proof - fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" - have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) have F2: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" by (metis abs_mult) have "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_mult_pos abs_one) @@ -92,7 +92,7 @@ proof - fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" - have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) have F2: "\x\<^isub>3 x\<^isub>1\'a\linordered_idom. 0 \ x\<^isub>1 \ \x\<^isub>3 * x\<^isub>1\ = \x\<^isub>3\ * x\<^isub>1" by (metis abs_mult_pos) hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_one) hence "\x\<^isub>3. 0 \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c\ * \f x\<^isub>3\" by (metis F2 A1 abs_ge_zero order_trans) @@ -111,7 +111,7 @@ proof - fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" - have "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) hence "\h x\ \ \c * f x\" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) @@ -145,12 +145,12 @@ declare [[ atp_problem_prefix = "BigO__bigo_refl" ]] lemma bigo_refl [intro]: "f : O(f)" apply (auto simp add: bigo_def) -by (metis class_semiring.mul_1 order_refl) +by (metis normalizing.mul_1 order_refl) declare [[ atp_problem_prefix = "BigO__bigo_zero" ]] lemma bigo_zero: "0 : O(g)" apply (auto simp add: bigo_def func_zero) -by (metis class_semiring.mul_0 order_refl) +by (metis normalizing.mul_0 order_refl) lemma bigo_zero2: "O(%x.0) = {%x.0}" apply (auto simp add: bigo_def) @@ -307,7 +307,7 @@ apply (auto simp add: diff_minus fun_Compl_def func_plus) prefer 2 apply (drule_tac x = x in spec)+ - apply (metis add_right_mono class_semiring.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans) + apply (metis add_right_mono normalizing.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans) proof - fix x :: 'a assume "\x. lb x \ f x" @@ -318,13 +318,13 @@ lemma bigo_abs: "(%x. abs(f x)) =o O(f)" apply (unfold bigo_def) apply auto -by (metis class_semiring.mul_1 order_refl) +by (metis normalizing.mul_1 order_refl) declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]] lemma bigo_abs2: "f =o O(%x. abs(f x))" apply (unfold bigo_def) apply auto -by (metis class_semiring.mul_1 order_refl) +by (metis normalizing.mul_1 order_refl) lemma bigo_abs3: "O(f) = O(%x. abs(f x))" proof - diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri May 07 09:59:59 2010 +0200 @@ -1877,7 +1877,7 @@ using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR apply (rule mult_left_le_imp_le[of "1 - u"]) - unfolding class_semiring.mul_a using `u<1` by auto + unfolding normalizing.mul_a using `u<1` by auto thus "y \ s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u] using as unfolding scaleR_scaleR by auto qed auto thus "u *\<^sub>R x \ s - frontier s" using frontier_def and interior_subset by auto qed @@ -2231,7 +2231,7 @@ apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof fix z assume z:"z\{x - ?d..x + ?d}" have e:"e = setsum (\i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1 - by (metis eq_divide_imp mult_frac_num real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute) + by (metis eq_divide_imp times_divide_eq_left real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute) show "dist x z \ e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono) using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed hence k:"\y\{x - ?d..x + ?d}. f y \ k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri May 07 09:59:59 2010 +0200 @@ -698,7 +698,7 @@ unfolding o_def apply(rule,rule has_derivative_lift_dot) using assms(3) by auto then guess x .. note x=this show ?thesis proof(cases "f a = f b") - case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:class_semiring.semiring_rules) + case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:normalizing.semiring_rules) also have "\ = (f b - f a) \ (f b - f a)" unfolding power2_norm_eq_inner .. also have "\ = (f b - f a) \ f' x (b - a)" using x unfolding inner_simps by auto also have "\ \ norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz) @@ -810,7 +810,7 @@ guess k using real_lbound_gt_zero[OF d[THEN conjunct1] d'[THEN conjunct1]] .. note k=this show ?case apply(rule_tac x=k in exI,rule) defer proof(rule,rule) fix z assume as:"norm(z - y) < k" hence "norm (g z - g y - g' (z - y)) \ e / B * norm(g z - g y)" using d' k by auto - also have "\ \ e * norm(z - y)" unfolding mult_frac_num pos_divide_le_eq[OF `B>0`] + also have "\ \ e * norm(z - y)" unfolding times_divide_eq_left pos_divide_le_eq[OF `B>0`] using lem2[THEN spec[where x=z]] using k as using `e>0` by(auto simp add:field_simps) finally show "norm (g z - g y - g' (z - y)) \ e * norm (z - y)" by simp qed(insert k, auto) qed qed diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri May 07 09:59:59 2010 +0200 @@ -2533,7 +2533,7 @@ show "content x \ 0" unfolding as snd_conv * interval_doublesplit by(rule content_pos_le) qed have **:"norm (1::real) \ 1" by auto note division_doublesplit[OF p'',unfolded interval_doublesplit] note dsum_bound[OF this **,unfolded interval_doublesplit[THEN sym]] - note this[unfolded real_scaleR_def real_norm_def class_semiring.semiring_rules, of k c d] note le_less_trans[OF this d(2)] + note this[unfolded real_scaleR_def real_norm_def normalizing.semiring_rules, of k c d] note le_less_trans[OF this d(2)] from this[unfolded abs_of_nonneg[OF *]] show "(\ka\snd ` p. content (ka \ {x. \x $ k - c\ \ d})) < e" apply(subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,THEN sym]) apply(rule finite_imageI p' content_empty)+ unfolding forall_in_division[OF p''] @@ -4723,7 +4723,7 @@ have "\e sg dsa dia ig. norm(sg) \ dsa \ abs(dsa - dia) < e / 2 \ norm(sg - ig) < e / 2 \ norm(ig) < dia + e" proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]]) - apply(subst real_sum_of_halves[of e,THEN sym]) unfolding class_semiring.add_a + apply(subst real_sum_of_halves[of e,THEN sym]) unfolding normalizing.add_a apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1) apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith qed note norm=this[rule_format] diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Nat_Numeral.thy Fri May 07 09:59:59 2010 +0200 @@ -319,6 +319,10 @@ lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)" by (simp add: nat_number_of_def) +lemma Numeral1_eq1_nat: + "(1::nat) = Numeral1" + by simp + lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0" by (simp only: nat_numeral_1_eq_1 One_nat_def) @@ -687,6 +691,20 @@ lemmas nat_number' = nat_number_of_Bit0 nat_number_of_Bit1 +lemmas nat_arith = + add_nat_number_of + diff_nat_number_of + mult_nat_number_of + eq_nat_number_of + less_nat_number_of + +lemmas semiring_norm = + Let_def arith_simps nat_arith rel_simps neg_simps if_False + if_True add_0 add_Suc add_number_of_left mult_number_of_left + numeral_1_eq_1 [symmetric] Suc_eq_plus1 + numeral_0_eq_0 [symmetric] numerals [symmetric] + iszero_simps not_iszero_Numeral1 + lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" by (fact Let_def) diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Parity.thy --- a/src/HOL/Parity.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Parity.thy Fri May 07 09:59:59 2010 +0200 @@ -229,7 +229,7 @@ lemma zero_le_odd_power: "odd n ==> (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)" apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff) -apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square) +apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square) done lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) = diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Probability/Lebesgue.thy --- a/src/HOL/Probability/Lebesgue.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Probability/Lebesgue.thy Fri May 07 09:59:59 2010 +0200 @@ -938,17 +938,17 @@ proof safe fix t assume t: "t \ space M" { fix m n :: nat assume "m \ n" - hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto + hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding normalizing.mul_pwr by auto have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \ real (natfloor (f t * 2 ^ n))" apply (subst *) - apply (subst class_semiring.mul_a) + apply (subst normalizing.mul_a) apply (subst real_of_nat_le_iff) apply (rule le_mult_natfloor) using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg) hence "real (natfloor (f t * 2^m)) * 2^n \ real (natfloor (f t * 2^n)) * 2^m" apply (subst *) - apply (subst (3) class_semiring.mul_c) - apply (subst class_semiring.mul_a) + apply (subst (3) normalizing.mul_c) + apply (subst normalizing.mul_a) by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) } thus "incseq (\n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def by (auto simp add: le_divide_eq divide_le_eq less_divide_eq) diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Rings.thy --- a/src/HOL/Rings.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Rings.thy Fri May 07 09:59:59 2010 +0200 @@ -183,9 +183,21 @@ end - class no_zero_divisors = zero + times + assumes no_zero_divisors: "a \ 0 \ b \ 0 \ a * b \ 0" +begin + +lemma divisors_zero: + assumes "a * b = 0" + shows "a = 0 \ b = 0" +proof (rule classical) + assume "\ (a = 0 \ b = 0)" + then have "a \ 0" and "b \ 0" by auto + with no_zero_divisors have "a * b \ 0" by blast + with assms show ?thesis by simp +qed + +end class semiring_1_cancel = semiring + cancel_comm_monoid_add + zero_neq_one + monoid_mult diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Fri May 07 09:59:59 2010 +0200 @@ -9,19 +9,20 @@ vars: cterm list, semiring: cterm list * thm list, ideal : thm list} -> (cterm -> Rat.rat) -> (Rat.rat -> cterm) -> conv -> conv -> - {ring_conv : conv, - simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list), - multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list, - poly_eq_ss: simpset, unwind_conv : conv} - val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic - val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic - val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic + {ring_conv : conv, + simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list), + multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list, + poly_eq_ss: simpset, unwind_conv : conv} + val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic + val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic + val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic + val algebra_method: (Proof.context -> Method.method) context_parser end structure Groebner : GROEBNER = struct -open Conv Normalizer Drule Thm; +open Conv Drule Thm; fun is_comb ct = (case Thm.term_of ct of @@ -50,11 +51,11 @@ val lcm_rat = fn x => fn y => Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y)); val (eqF_intr, eqF_elim) = - let val [th1,th2] = thms "PFalse" + let val [th1,th2] = @{thms PFalse} in (fn th => th COMP th2, fn th => th COMP th1) end; val (PFalse, PFalse') = - let val PFalse_eq = nth (thms "simp_thms") 13 + let val PFalse_eq = nth @{thms simp_thms} 13 in (PFalse_eq RS iffD1, PFalse_eq RS iffD2) end; @@ -398,7 +399,7 @@ compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE)) | _ => rfn tm ; -val notnotD = @{thm "notnotD"}; +val notnotD = @{thm notnotD}; fun mk_binop ct x y = capply (capply ct x) y val mk_comb = capply; @@ -440,10 +441,10 @@ | _ => false; val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq; -val bool_simps = @{thms "bool_simps"}; -val nnf_simps = @{thms "nnf_simps"}; +val bool_simps = @{thms bool_simps}; +val nnf_simps = @{thms nnf_simps}; val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps bool_simps addsimps nnf_simps) -val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms "weak_dnf_simps"}); +val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms weak_dnf_simps}); val initial_conv = Simplifier.rewrite (HOL_basic_ss addsimps nnf_simps @@ -947,29 +948,31 @@ case try (find_term 0) form of NONE => NONE | SOME tm => - (case NormalizerData.match ctxt tm of + (case Normalizer.match ctxt tm of NONE => NONE | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) => SOME (ring_and_ideal_conv theory dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt) - (semiring_normalize_wrapper ctxt res))) + (Normalizer.semiring_normalize_wrapper ctxt res))) fun ring_solve ctxt form = (case try (find_term 0 (* FIXME !? *)) form of NONE => reflexive form | SOME tm => - (case NormalizerData.match ctxt tm of + (case Normalizer.match ctxt tm of NONE => reflexive form | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) => #ring_conv (ring_and_ideal_conv theory dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt) - (semiring_normalize_wrapper ctxt res)) form)); + (Normalizer.semiring_normalize_wrapper ctxt res)) form)); + +fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (Simplifier.context ctxt + (HOL_basic_ss addsimps (Algebra_Simplification.get ctxt) delsimps del_thms addsimps add_thms)); fun ring_tac add_ths del_ths ctxt = Object_Logic.full_atomize_tac - THEN' asm_full_simp_tac - (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths) + THEN' presimplify ctxt add_ths del_ths THEN' CSUBGOAL (fn (p, i) => rtac (let val form = Object_Logic.dest_judgment p in case get_ring_ideal_convs ctxt form of @@ -988,8 +991,7 @@ | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1 in fun ideal_tac add_ths del_ths ctxt = - asm_full_simp_tac - (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths) + presimplify ctxt add_ths del_ths THEN' CSUBGOAL (fn (p, i) => case get_ring_ideal_convs ctxt p of @@ -1023,6 +1025,21 @@ fun algebra_tac add_ths del_ths ctxt i = ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i - +local + +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () +val addN = "add" +val delN = "del" +val any_keyword = keyword addN || keyword delN +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; + +in + +val algebra_method = ((Scan.optional (keyword addN |-- thms) []) -- + (Scan.optional (keyword delN |-- thms) [])) >> + (fn (add_ths, del_ths) => fn ctxt => + SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt)) end; + +end; diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Tools/Groebner_Basis/misc.ML --- a/src/HOL/Tools/Groebner_Basis/misc.ML Thu May 06 11:08:19 2010 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -(* Title: HOL/Tools/Groebner_Basis/misc.ML - ID: $Id$ - Author: Amine Chaieb, TU Muenchen - -Very basic stuff for cterms. -*) - -structure Misc = -struct - -fun is_comb ct = - (case Thm.term_of ct of - _ $ _ => true - | _ => false); - -val concl = Thm.cprop_of #> Thm.dest_arg; - -fun is_binop ct ct' = - (case Thm.term_of ct' of - c $ _ $ _ => term_of ct aconv c - | _ => false); - -fun dest_binop ct ct' = - if is_binop ct ct' then Thm.dest_binop ct' - else raise CTERM ("dest_binop: bad binop", [ct, ct']) - -fun inst_thm inst = Thm.instantiate ([], inst); - -end; diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Tools/Groebner_Basis/normalizer.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Fri May 07 09:59:59 2010 +0200 @@ -1,30 +1,376 @@ (* Title: HOL/Tools/Groebner_Basis/normalizer.ML Author: Amine Chaieb, TU Muenchen + +Normalization of expressions in semirings. *) signature NORMALIZER = sig - val semiring_normalize_conv : Proof.context -> conv - val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> conv - val semiring_normalize_tac : Proof.context -> int -> tactic - val semiring_normalize_wrapper : Proof.context -> NormalizerData.entry -> conv - val semiring_normalizers_ord_wrapper : - Proof.context -> NormalizerData.entry -> (cterm -> cterm -> bool) -> + type entry + val get: Proof.context -> (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, + 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, + mk_const: morphism -> ctyp -> Rat.rat -> cterm, + conv: morphism -> Proof.context -> cterm -> thm} -> declaration + val semiring_funs: thm -> declaration + val field_funs: thm -> declaration + + val semiring_normalize_conv: Proof.context -> conv + val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv + val semiring_normalize_wrapper: Proof.context -> entry -> conv + val semiring_normalize_ord_wrapper: Proof.context -> entry + -> (cterm -> cterm -> bool) -> conv + val semiring_normalizers_conv: 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} + val semiring_normalizers_ord_wrapper: Proof.context -> entry -> + (cterm -> cterm -> bool) -> {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} - 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 * thm list -> - (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) -> - {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} + val field_comp_conv: conv + + val setup: theory -> theory end structure Normalizer: NORMALIZER = struct -open Conv; +(** some conversion **) + +local + val zr = @{cpat "0"} + val zT = ctyp_of_term zr + val geq = @{cpat "op ="} + val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd + val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} + val add_frac_num = mk_meta_eq @{thm "add_frac_num"} + val add_num_frac = mk_meta_eq @{thm "add_num_frac"} + + fun prove_nz ss T t = + let + val z = instantiate_cterm ([(zT,T)],[]) zr + val eq = instantiate_cterm ([(eqT,T)],[]) geq + val th = Simplifier.rewrite (ss addsimps @{thms simp_thms}) + (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} + (Thm.capply (Thm.capply eq t) z))) + in equal_elim (symmetric th) TrueI + end + + fun proc phi ss ct = + let + val ((x,y),(w,z)) = + (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct + val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] + val T = ctyp_of_term x + val [y_nz, z_nz] = map (prove_nz ss T) [y, z] + val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq + in SOME (implies_elim (implies_elim th y_nz) z_nz) + end + handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE + + fun proc2 phi ss ct = + let + val (l,r) = Thm.dest_binop ct + val T = ctyp_of_term l + in (case (term_of l, term_of r) of + (Const(@{const_name Rings.divide},_)$_$_, _) => + let val (x,y) = Thm.dest_binop l val z = r + val _ = map (HOLogic.dest_number o term_of) [x,y,z] + val ynz = prove_nz ss T y + in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) + end + | (_, Const (@{const_name Rings.divide},_)$_$_) => + let val (x,y) = Thm.dest_binop r val z = l + val _ = map (HOLogic.dest_number o term_of) [x,y,z] + val ynz = prove_nz ss T y + in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) + end + | _ => NONE) + end + handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE + + fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b + | is_number t = can HOLogic.dest_number t + + val is_number = is_number o term_of + + fun proc3 phi ss ct = + (case term_of ct of + Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + let + val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} + in SOME (mk_meta_eq th) end + | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + let + val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} + in SOME (mk_meta_eq th) end + | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + let + val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} + in SOME (mk_meta_eq th) end + | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + let + val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} + in SOME (mk_meta_eq th) end + | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + let + val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} + in SOME (mk_meta_eq th) end + | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + let + val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} + in SOME (mk_meta_eq th) end + | _ => NONE) + handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE + +val add_frac_frac_simproc = + make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], + name = "add_frac_frac_simproc", + proc = proc, identifier = []} + +val add_frac_num_simproc = + make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], + name = "add_frac_num_simproc", + proc = proc2, identifier = []} + +val ord_frac_simproc = + make_simproc + {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, + @{cpat "(?a::(?'a::{field, ord}))/?b <= ?c"}, + @{cpat "?c < (?a::(?'a::{field, ord}))/?b"}, + @{cpat "?c <= (?a::(?'a::{field, ord}))/?b"}, + @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"}, + @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}], + name = "ord_frac_simproc", proc = proc3, identifier = []} + +val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, + @{thm "divide_Numeral1"}, + @{thm "divide_zero"}, @{thm "divide_Numeral0"}, + @{thm "divide_divide_eq_left"}, + @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"}, + @{thm "times_divide_times_eq"}, + @{thm "divide_divide_eq_right"}, + @{thm "diff_def"}, @{thm "minus_divide_left"}, + @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym, + @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, + Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute})))) + (@{thm field_divide_inverse} RS sym)] + +in + +val field_comp_conv = (Simplifier.rewrite +(HOL_basic_ss addsimps @{thms "semiring_norm"} + addsimps ths addsimps @{thms simp_thms} + addsimprocs Numeral_Simprocs.field_cancel_numeral_factors + addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, + ord_frac_simproc] + addcongs [@{thm "if_weak_cong"}])) +then_conv (Simplifier.rewrite (HOL_basic_ss addsimps + [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)})) + +end + + +(** data **) -(* Very basic stuff for terms *) +type entry = + {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, + dest_const: cterm -> Rat.rat, + mk_const: ctyp -> Rat.rat -> cterm, + conv: Proof.context -> cterm -> thm}; + +structure Data = Generic_Data +( + type T = (thm * entry) list; + val empty = []; + val extend = I; + val merge = AList.merge Thm.eq_thm (K true); +); + +val get = Data.get o Context.Proof; + +fun match ctxt tm = + let + fun match_inst + ({vars, semiring = (sr_ops, sr_rules), + 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 = + let + val substT = Thm.instantiate (instT, []); + val substT_cterm = Drule.cterm_rule substT; + + 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', field = field', idom = idom', ideal = ideal'}, fns); + in SOME result end + in (case try Thm.match (pat, tm) of + NONE => NONE + | SOME (instT, _) => h instT) + end; + + fun match_struct (_, + 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 (get ctxt) end; + + +(* logical content *) + +val semiringN = "semiring"; +val ringN = "ring"; +val idomN = "idom"; +val idealN = "ideal"; +val fieldN = "field"; + +fun undefined _ = raise Match; + +val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm); + +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; + + fun check kind name xs n = + null xs orelse length xs = n orelse + error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); + val check_ops = check "operations"; + val check_rules = check "rules"; + + val _ = + check_ops semiringN sr_ops 5 andalso + 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 = Local_Defs.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); + + val (cx, cy) = Thm.dest_binop (hd sr_ops); + val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; + val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; + val ((clx, crx), (cly, cry)) = + rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; + val ((ca, cb), (cc, cd)) = + rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; + val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; + val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg; + + 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 + AList.delete Thm.eq_thm key #> + cons (key, ({vars = vars, semiring = semiring, + ring = ring, field = field, idom = idom, ideal = ideal'}, + {is_const = undefined, dest_const = undefined, mk_const = undefined, + conv = undefined})) + end); + + +(* extra-logical functions *) + +fun funs raw_key {is_const, dest_const, mk_const, conv} phi = + Data.map (fn data => + let + val key = Morphism.thm phi raw_key; + val _ = AList.defined Thm.eq_thm data key orelse + raise THM ("No data entry for structure key", 0, [key]); + val fns = {is_const = is_const phi, dest_const = dest_const phi, + mk_const = mk_const phi, conv = conv phi}; + in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end); + +fun semiring_funs key = funs key + {is_const = fn phi => can HOLogic.dest_number o Thm.term_of, + dest_const = fn phi => fn ct => + Rat.rat_of_int (snd + (HOLogic.dest_number (Thm.term_of ct) + handle TERM _ => error "ring_dest_const")), + mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT + (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"), + conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}) + then_conv Simplifier.rewrite (HOL_basic_ss addsimps + (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))}; + +fun field_funs key = + let + fun numeral_is_const ct = + case term_of ct of + Const (@{const_name Rings.divide},_) $ a $ b => + can HOLogic.dest_number a andalso can HOLogic.dest_number b + | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t + | t => can HOLogic.dest_number t + fun dest_const ct = ((case term_of ct of + Const (@{const_name Rings.divide},_) $ a $ b=> + Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) + | Const (@{const_name Rings.inverse},_)$t => + Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t))) + | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) + handle TERM _ => error "ring_dest_const") + fun mk_const phi cT x = + let val (a, b) = Rat.quotient_of_rat x + in if b = 1 then Numeral.mk_cnumber cT a + else Thm.capply + (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) + (Numeral.mk_cnumber cT a)) + (Numeral.mk_cnumber cT b) + end + in funs key + {is_const = K numeral_is_const, + dest_const = K dest_const, + mk_const = mk_const, + conv = K (K field_comp_conv)} + end; + + + +(** auxiliary **) fun is_comb ct = (case Thm.term_of ct of @@ -55,6 +401,7 @@ val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"}, @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, @{thm "less_nat_number_of"}]; + val nat_add_conv = zerone_conv (Simplifier.rewrite @@ -64,13 +411,15 @@ @{thm add_number_of_left}, @{thm Suc_eq_plus1}] @ map (fn th => th RS sym) @{thms numerals})); -val nat_mul_conv = nat_add_conv; val zeron_tm = @{cterm "0::nat"}; val onen_tm = @{cterm "1::nat"}; val true_tm = @{cterm "True"}; -(* The main function! *) +(** normalizing conversions **) + +(* core conversion *) + 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 @@ -182,7 +531,7 @@ then let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34 val (l,r) = Thm.dest_comb(concl th1) - in transitive th1 (Drule.arg_cong_rule l (nat_mul_conv r)) + in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r)) end else if opr aconvc mul_tm @@ -563,7 +912,7 @@ let val (l,r) = Thm.dest_comb tm in if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else let val th1 = inst_thm [(cx',r)] neg_mul - val th2 = transitive th1 (arg1_conv semiring_mul_conv (concl th1)) + val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1)) in transitive th2 (polynomial_monomial_mul_conv (concl th2)) end end; @@ -606,7 +955,7 @@ 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) + val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv) (Thm.rhs_of th1) in transitive th1 th2 end @@ -638,11 +987,14 @@ fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; + +(* various normalizing conversions *) + fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = let val pow_conv = - arg_conv (Simplifier.rewrite nat_exp_ss) + Conv.arg_conv (Simplifier.rewrite nat_exp_ss) then_conv Simplifier.rewrite (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34]) then_conv conv ctxt @@ -656,14 +1008,57 @@ semiring_normalize_ord_wrapper ctxt data simple_cterm_ord; fun semiring_normalize_ord_conv ctxt ord tm = - (case NormalizerData.match ctxt tm of + (case match ctxt tm of NONE => reflexive tm | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm); - fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord; -fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) => - rtac (semiring_normalize_conv ctxt - (cterm_of (ProofContext.theory_of ctxt) (fst (Logic.dest_equals goal)))) i); + +(** Isar setup **) + +local + +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); +fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K (); +fun keyword3 k1 k2 k3 = + Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K (); + +val opsN = "ops"; +val rulesN = "rules"; + +val normN = "norm"; +val constN = "const"; +val delN = "del"; + +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; +val terms = thms >> map Drule.dest_term; + +fun optional scan = Scan.optional scan []; + +in + +val setup = + Attrib.setup @{binding normalizer} + (Scan.lift (Args.$$$ delN >> K del) || + ((keyword2 semiringN opsN |-- terms) -- + (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), f), id), idl) => + add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) + "semiring normalizer data"; + end; + +end; diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Tools/Groebner_Basis/normalizer_data.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Thu May 06 11:08:19 2010 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,227 +0,0 @@ -(* Title: HOL/Tools/Groebner_Basis/normalizer_data.ML - ID: $Id$ - Author: Amine Chaieb, TU Muenchen - -Ring normalization data. -*) - -signature NORMALIZER_DATA = -sig - type entry - 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, 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, - mk_const: morphism -> ctyp -> Rat.rat -> cterm, - conv: morphism -> Proof.context -> cterm -> thm} -> declaration - val setup: theory -> theory -end; - -structure NormalizerData: NORMALIZER_DATA = -struct - -(* data *) - -type entry = - {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, - dest_const: cterm -> Rat.rat, - mk_const: ctyp -> Rat.rat -> cterm, - conv: Proof.context -> cterm -> thm}; - -val eq_key = Thm.eq_thm; -fun eq_data arg = eq_fst eq_key arg; - -structure Data = Generic_Data -( - type T = simpset * (thm * entry) list; - val empty = (HOL_basic_ss, []); - val extend = I; - fun merge ((ss, e), (ss', e')) : T = - (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e')); -); - -val get = Data.get o Context.Proof; - - -(* match data *) - -fun match ctxt tm = - let - fun match_inst - ({vars, semiring = (sr_ops, sr_rules), - 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 = - let - val substT = Thm.instantiate (instT, []); - val substT_cterm = Drule.cterm_rule substT; - - 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', field = field', idom = idom', ideal = ideal'}, fns); - in SOME result end - in (case try Thm.match (pat, tm) of - NONE => NONE - | SOME (instT, _) => h instT) - end; - - fun match_struct (_, - 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; - - -(* logical content *) - -val semiringN = "semiring"; -val ringN = "ring"; -val idomN = "idom"; -val idealN = "ideal"; -val fieldN = "field"; - -fun undefined _ = raise Match; - -fun del_data key = apsnd (remove eq_data (key, [])); - -val del = Thm.declaration_attribute (Data.map o del_data); -val add_ss = Thm.declaration_attribute - (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data))); - -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), - field = (f_ops, f_rules), idom, ideal} = - Thm.declaration_attribute (fn key => fn context => context |> Data.map - let - val ctxt = Context.proof_of context; - - fun check kind name xs n = - null xs orelse length xs = n orelse - error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); - val check_ops = check "operations"; - val check_rules = check "rules"; - - val _ = - check_ops semiringN sr_ops 5 andalso - 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 = Local_Defs.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); - - val (cx, cy) = Thm.dest_binop (hd sr_ops); - val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; - val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; - val ((clx, crx), (cly, cry)) = - rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; - val ((ca, cb), (cc, cd)) = - rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; - val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; - val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg; - - 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, field = field, idom = idom, ideal = ideal'}, - {is_const = undefined, dest_const = undefined, mk_const = undefined, - conv = undefined}))) - end); - - -(* extra-logical functions *) - -fun funs raw_key {is_const, dest_const, mk_const, conv} phi = - (Data.map o apsnd) (fn data => - let - val key = Morphism.thm phi raw_key; - val _ = AList.defined eq_key data key orelse - raise THM ("No data entry for structure key", 0, [key]); - val fns = {is_const = is_const phi, dest_const = dest_const phi, - mk_const = mk_const phi, conv = conv phi}; - in AList.map_entry eq_key key (apsnd (K fns)) data end); - - -(* concrete syntax *) - -local - -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); -fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K (); -fun keyword3 k1 k2 k3 = - Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K (); - -val opsN = "ops"; -val rulesN = "rules"; - -val normN = "norm"; -val constN = "const"; -val delN = "del"; - -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; -val terms = thms >> map Drule.dest_term; - -fun optional scan = Scan.optional scan []; - -in - -val normalizer_setup = - Attrib.setup @{binding normalizer} - (Scan.lift (Args.$$$ delN >> K del) || - ((keyword2 semiringN opsN |-- terms) -- - (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), f), id), idl) => - add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) - "semiring normalizer data"; - -end; - - -(* theory setup *) - -val setup = - normalizer_setup #> - Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra"; - -end; diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri May 07 09:59:59 2010 +0200 @@ -3,7 +3,7 @@ *) signature COOPER = - sig +sig val cooper_conv : Proof.context -> conv exception COOPER of string * exn end; @@ -12,7 +12,6 @@ struct open Conv; -open Normalizer; exception COOPER of string * exn; fun simp_thms_conv ctxt = diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Tools/Qelim/cooper_data.ML --- a/src/HOL/Tools/Qelim/cooper_data.ML Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Tools/Qelim/cooper_data.ML Fri May 07 09:59:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/Qelim/cooper_data.ML - ID: $Id$ Author: Amine Chaieb, TU Muenchen *) @@ -16,8 +15,7 @@ struct type entry = simpset * (term list); -val start_ss = HOL_ss (* addsimps @{thms "Groebner_Basis.comp_arith"} - addcongs [if_weak_cong, @{thm "let_weak_cong"}];*) + val allowed_consts = [@{term "op + :: int => _"}, @{term "op + :: nat => _"}, @{term "op - :: int => _"}, @{term "op - :: nat => _"}, @@ -47,7 +45,7 @@ structure Data = Generic_Data ( type T = simpset * term list; - val empty = (start_ss, allowed_consts); + val empty = (HOL_ss, allowed_consts); val extend = I; fun merge ((ss1, ts1), (ss2, ts2)) = (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2)); @@ -64,7 +62,7 @@ (ss delsimps [th], subtract (op aconv) ts' ts ))) -(* concrete syntax *) +(* theory setup *) local @@ -79,16 +77,11 @@ in -val presburger_setup = +val setup = Attrib.setup @{binding presburger} ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del || optional (keyword constsN |-- terms) >> add) "Cooper data"; end; - -(* theory setup *) - -val setup = presburger_setup; - end; diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/Tools/Qelim/presburger.ML Fri May 07 09:59:59 2010 +0200 @@ -11,7 +11,7 @@ struct open Conv; -val comp_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"}; +val comp_ss = HOL_ss addsimps @{thms semiring_norm}; fun strip_objimp ct = (case Thm.term_of ct of diff -r 1b69f78be286 -r 47ba1770da8e src/HOL/ex/Groebner_Examples.thy --- a/src/HOL/ex/Groebner_Examples.thy Thu May 06 11:08:19 2010 -0700 +++ b/src/HOL/ex/Groebner_Examples.thy Fri May 07 09:59:59 2010 +0200 @@ -10,18 +10,30 @@ subsection {* Basic examples *} -schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})" - by sring_norm +lemma + fixes x :: int + shows "x ^ 3 = x ^ 3" + apply (tactic {* ALLGOALS (CONVERSION + (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) + by (rule refl) -schematic_lemma "(x - (-2))^5 == ?X::int" - by sring_norm +lemma + fixes x :: int + shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\ + (80 * x + 32))))" + apply (tactic {* ALLGOALS (CONVERSION + (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) + by (rule refl) -schematic_lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int" - by sring_norm +schematic_lemma + fixes x :: int + shows "(x - (-2))^5 * (y - 78) ^ 8 = ?X" + apply (tactic {* ALLGOALS (CONVERSION + (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) + by (rule refl) lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})" apply (simp only: power_Suc power_0) - apply (simp only: comp_arith) + apply (simp only: semiring_norm) oops lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \ x = z + 3 \ x = - y"