# HG changeset patch # User haftmann # Date 1423905855 -3600 # Node ID 8d2b1bfb60b457cf2bbe18e2e93ae6cb8d153dbe # Parent 7f2b60cb5190642175dd26ffbc5b9d826ac0fecd more consistent teminology diff -r 7f2b60cb5190 -r 8d2b1bfb60b4 src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Sat Feb 14 10:24:15 2015 +0100 +++ b/src/HOL/Tools/semiring_normalizer.ML Sat Feb 14 10:24:15 2015 +0100 @@ -244,8 +244,8 @@ fun inst_thm inst = Thm.instantiate ([], inst); -val dest_numeral = term_of #> HOLogic.dest_number #> snd; -val is_numeral = can dest_numeral; +val dest_number = term_of #> HOLogic.dest_number #> snd; +val is_number = can dest_number; fun numeral01_conv ctxt = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_1_eq_1}]); @@ -297,7 +297,7 @@ val dest_mul = dest_binop mul_tm fun dest_pow tm = let val (l,r) = dest_binop pow_tm tm - in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm]) + in if is_number r then (l,r) else raise CTERM ("dest_pow",[tm]) end; val is_add = is_binop add_tm val is_mul = is_binop mul_tm @@ -384,7 +384,7 @@ let val (opr,l) = Thm.dest_comb lopr in - if opr aconvc pow_tm andalso is_numeral r + if opr aconvc pow_tm andalso is_number r then let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34 val (l,r) = Thm.dest_comb(concl th1) @@ -408,7 +408,7 @@ let val (lopr,r) = Thm.dest_comb tm val (opr,l) = Thm.dest_comb lopr - in if not (opr aconvc pow_tm) orelse not(is_numeral r) + in if not (opr aconvc pow_tm) orelse not(is_number r) then raise CTERM ("monomial_pow_conv", [tm]) else if r aconvc zeron_tm then inst_thm [(cx,l)] pthm_35 @@ -426,7 +426,7 @@ else ((let val (lopr,r) = Thm.dest_comb tm val (opr,l) = Thm.dest_comb lopr - in if opr aconvc pow_tm andalso is_numeral r then l + in if opr aconvc pow_tm andalso is_number r then l else raise CTERM ("monomial_mul_conv",[tm]) end) handle CTERM _ => tm) (* FIXME !? *) fun vorder x y = @@ -579,7 +579,7 @@ val num_0 = 0; val num_1 = 1; fun dest_varpow tm = - ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end) + ((let val (x,n) = dest_pow tm in (x,dest_number n) end) handle CTERM _ => (tm,(if is_semiring_constant tm then num_0 else num_1))); @@ -740,7 +740,7 @@ (* Power of polynomial (optimized for the monomial and trivial cases). *) fun num_conv ctxt n = - nat_add_conv ctxt (Thm.apply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1))) + nat_add_conv ctxt (Thm.apply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_number n - 1))) |> Thm.symmetric; @@ -804,7 +804,7 @@ if not(is_comb lopr) then Thm.reflexive tm else let val (opr,l) = Thm.dest_comb lopr - in if opr aconvc pow_tm andalso is_numeral r + in if opr aconvc pow_tm andalso is_number r then let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv ctxt l)) r in Thm.transitive th1 (polynomial_pow_conv ctxt (concl th1))