# HG changeset patch # User nipkow # Date 1241803200 -7200 # Node ID 35b437f7ad519c7ddee47314bcd1acf4a76d449d # Parent 710cd642650e7e4227184bbf2b8a29e71fc0edc8# Parent 9950ca962e2077e6310c679a91f3303c16df358a merged diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Fri May 08 08:07:05 2009 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri May 08 19:20:00 2009 +0200 @@ -83,7 +83,7 @@ addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}] (* Simp rules for changing (n::int) to int n *) val simpset1 = HOL_basic_ss - addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym) + addsimps [@{thm nat_number_of_def}, zdvd_int] @ map (fn r => r RS sym) [@{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}] addsplits [zdiff_int_split] (*simp rules for elimination of int n*) diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Fri May 08 08:07:05 2009 +0200 +++ b/src/HOL/Groebner_Basis.thy Fri May 08 19:20:00 2009 +0200 @@ -635,7 +635,7 @@ val comp_conv = (Simplifier.rewrite (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} addsimps ths addsimps simp_thms - addsimprocs field_cancel_numeral_factors + addsimprocs Numeral_Simprocs.field_cancel_numeral_factors addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc] addcongs [@{thm "if_weak_cong"}])) diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Int.thy --- a/src/HOL/Int.thy Fri May 08 08:07:05 2009 +0200 +++ b/src/HOL/Int.thy Fri May 08 19:20:00 2009 +0200 @@ -12,13 +12,13 @@ uses ("Tools/numeral.ML") ("Tools/numeral_syntax.ML") + ("Tools/int_arith.ML") "~~/src/Provers/Arith/assoc_fold.ML" "~~/src/Provers/Arith/cancel_numerals.ML" "~~/src/Provers/Arith/combine_numerals.ML" "~~/src/Provers/Arith/cancel_numeral_factor.ML" "~~/src/Provers/Arith/extract_common_term.ML" - ("Tools/int_factor_simprocs.ML") - ("Tools/int_arith.ML") + ("Tools/numeral_simprocs.ML") begin subsection {* The equivalence relation underlying the integers *} @@ -1518,9 +1518,10 @@ of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult of_int_0 of_int_1 of_int_add of_int_mult +use "Tools/numeral_simprocs.ML" + use "Tools/int_arith.ML" declaration {* K Int_Arith.setup *} -use "Tools/int_factor_simprocs.ML" setup {* ReorientProc.add diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Fri May 08 08:07:05 2009 +0200 +++ b/src/HOL/IntDiv.thy Fri May 08 19:20:00 2009 +0200 @@ -252,8 +252,8 @@ val div_name = @{const_name div}; val mod_name = @{const_name mod}; val mk_binop = HOLogic.mk_binop; - val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT; - val dest_sum = Int_Numeral_Simprocs.dest_sum; + val mk_sum = Numeral_Simprocs.mk_sum HOLogic.intT; + val dest_sum = Numeral_Simprocs.dest_sum; val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}]; diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri May 08 08:07:05 2009 +0200 +++ b/src/HOL/IsaMakefile Fri May 08 19:20:00 2009 +0200 @@ -226,19 +226,19 @@ $(SRC)/Provers/Arith/combine_numerals.ML \ $(SRC)/Provers/Arith/extract_common_term.ML \ $(SRC)/Tools/Metis/metis.ML \ - Tools/int_arith.ML \ - Tools/int_factor_simprocs.ML \ - Tools/nat_simprocs.ML \ Tools/Groebner_Basis/groebner.ML \ Tools/Groebner_Basis/misc.ML \ Tools/Groebner_Basis/normalizer_data.ML \ Tools/Groebner_Basis/normalizer.ML \ Tools/atp_manager.ML \ Tools/atp_wrapper.ML \ + Tools/int_arith.ML \ Tools/list_code.ML \ Tools/meson.ML \ Tools/metis_tools.ML \ + Tools/nat_numeral_simprocs.ML \ Tools/numeral.ML \ + Tools/numeral_simprocs.ML \ Tools/numeral_syntax.ML \ Tools/polyhash.ML \ Tools/Qelim/cooper_data.ML \ diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Fri May 08 08:07:05 2009 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Fri May 08 19:20:00 2009 +0200 @@ -1440,6 +1440,67 @@ lemma power_radical: fixes a:: "'a ::{field, ring_char_0} fps" + assumes a0: "a$0 \ 0" + shows "(r (Suc k) (a$0)) ^ Suc k = a$0 \ (fps_radical r (Suc k) a) ^ (Suc k) = a" +proof- + let ?r = "fps_radical r (Suc k) a" + {assume r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" + from a0 r0 have r00: "r (Suc k) (a$0) \ 0" by auto + {fix z have "?r ^ Suc k $ z = a$z" + proof(induct z rule: nat_less_induct) + fix n assume H: "\m 0" using n1 by arith + let ?Pnk = "natpermute n (k + 1)" + let ?Pnkn = "{xs \ ?Pnk. n \ set xs}" + let ?Pnknn = "{xs \ ?Pnk. n \ set xs}" + have eq: "?Pnkn \ ?Pnknn = ?Pnk" by blast + have d: "?Pnkn \ ?Pnknn = {}" by blast + have f: "finite ?Pnkn" "finite ?Pnknn" + using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] + by (metis natpermute_finite)+ + let ?f = "\v. \j\{0..k}. ?r $ v ! j" + have "setsum ?f ?Pnkn = setsum (\v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn" + proof(rule setsum_cong2) + fix v assume v: "v \ {xs \ natpermute n (k + 1). n \ set xs}" + let ?ths = "(\j\{0..k}. fps_radical r (Suc k) a $ v ! j) = fps_radical r (Suc k) a $ n * r (Suc k) (a $ 0) ^ k" + from v obtain i where i: "i \ {0..k}" "v = replicate (k+1) 0 [i:= n]" + unfolding natpermute_contain_maximal by auto + have "(\j\{0..k}. fps_radical r (Suc k) a $ v ! j) = (\j\{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))" + apply (rule setprod_cong, simp) + using i r0 by (simp del: replicate.simps) + also have "\ = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k" + unfolding setprod_gen_delta[OF fK] using i r0 by simp + finally show ?ths . + qed + then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k" + by (simp add: natpermute_max_card[OF nz, simplified]) + also have "\ = a$n - setsum ?f ?Pnknn" + unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc ) + finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" . + have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" + unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] .. + also have "\ = a$n" unfolding fn by simp + finally have "?r ^ Suc k $ n = a $n" .} + ultimately show "?r ^ Suc k $ n = a $n" by (cases n, auto) + qed } + then have ?thesis using r0 by (simp add: fps_eq_iff)} +moreover +{ assume h: "(fps_radical r (Suc k) a) ^ (Suc k) = a" + hence "((fps_radical r (Suc k) a) ^ (Suc k))$0 = a$0" by simp + then have "(r (Suc k) (a$0)) ^ Suc k = a$0" + unfolding fps_power_nth_Suc + by (simp add: setprod_constant del: replicate.simps)} +ultimately show ?thesis by blast +qed + +(* +lemma power_radical: + fixes a:: "'a ::{field, ring_char_0} fps" assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" and a0: "a$0 \ 0" shows "(fps_radical r (Suc k) a) ^ (Suc k) = a" proof- @@ -1490,6 +1551,7 @@ then show ?thesis by (simp add: fps_eq_iff) qed +*) lemma eq_divide_imp': assumes c0: "(c::'a::field) ~= 0" and eq: "a * c = b" shows "a = b / c" proof- @@ -1506,10 +1568,9 @@ let ?r = "fps_radical r (Suc k) b" have r00: "r (Suc k) (b$0) \ 0" using b0 r0 by auto {assume H: "a = ?r" - from H have "a^Suc k = b" using power_radical[of r k, OF r0 b0] by simp} + from H have "a^Suc k = b" using power_radical[OF b0, of r k, unfolded r0] by simp} moreover {assume H: "a^Suc k = b" - (* Generally a$0 would need to be the k+1 st root of b$0 *) have ceq: "card {0..k} = Suc k" by simp have fk: "finite {0..k}" by simp from a0 have a0r0: "a$0 = ?r$0" by simp @@ -1617,7 +1678,7 @@ from r0' have w0: "?w $ 0 \ 0" by (simp del: of_nat_Suc) note th0 = inverse_mult_eq_1[OF w0] let ?iw = "inverse ?w" - from power_radical[of r, OF r0 a0] + from iffD1[OF power_radical[of a r], OF a0 r0] have "fps_deriv (?r ^ Suc k) = fps_deriv a" by simp hence "fps_deriv ?r * ?w = fps_deriv a" by (simp add: fps_deriv_power mult_ac del: power_Suc) @@ -1630,9 +1691,43 @@ lemma radical_mult_distrib: fixes a:: "'a ::{field, ring_char_0} fps" assumes - ra0: "r (k) (a $ 0) ^ k = a $ 0" - and rb0: "r (k) (b $ 0) ^ k = b $ 0" - and r0': "r (k) ((a * b) $ 0) = r (k) (a $ 0) * r (k) (b $ 0)" + k: "k > 0" + and ra0: "r k (a $ 0) ^ k = a $ 0" + and rb0: "r k (b $ 0) ^ k = b $ 0" + and a0: "a$0 \ 0" + and b0: "b$0 \ 0" + shows "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0) \ fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)" +proof- + {assume r0': "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)" + from r0' have r0: "(r (k) ((a*b)$0)) ^ k = (a*b)$0" + by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib) + {assume "k=0" hence ?thesis using r0' by simp} + moreover + {fix h assume k: "k = Suc h" + let ?ra = "fps_radical r (Suc h) a" + let ?rb = "fps_radical r (Suc h) b" + have th0: "r (Suc h) ((a * b) $ 0) = (fps_radical r (Suc h) a * fps_radical r (Suc h) b) $ 0" + using r0' k by (simp add: fps_mult_nth) + have ab0: "(a*b) $ 0 \ 0" using a0 b0 by (simp add: fps_mult_nth) + from radical_unique[of r h "a*b" "fps_radical r (Suc h) a * fps_radical r (Suc h) b", OF r0[unfolded k] th0 ab0, symmetric] + iffD1[OF power_radical[of _ r], OF a0 ra0[unfolded k]] iffD1[OF power_radical[of _ r], OF b0 rb0[unfolded k]] k r0' + have ?thesis by (auto simp add: power_mult_distrib simp del: power_Suc)} +ultimately have ?thesis by (cases k, auto)} +moreover +{assume h: "fps_radical r k (a*b) = fps_radical r k a * fps_radical r k b" + hence "(fps_radical r k (a*b))$0 = (fps_radical r k a * fps_radical r k b)$0" by simp + then have "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)" + using k by (simp add: fps_mult_nth)} +ultimately show ?thesis by blast +qed + +(* +lemma radical_mult_distrib: + fixes a:: "'a ::{field, ring_char_0} fps" + assumes + ra0: "r k (a $ 0) ^ k = a $ 0" + and rb0: "r k (b $ 0) ^ k = b $ 0" + and r0': "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)" and a0: "a$0 \ 0" and b0: "b$0 \ 0" shows "fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)" @@ -1652,88 +1747,61 @@ have ?thesis by (auto simp add: power_mult_distrib simp del: power_Suc)} ultimately show ?thesis by (cases k, auto) qed +*) -lemma radical_inverse: - fixes a:: "'a ::{field, ring_char_0} fps" - assumes - ra0: "r (k) (a $ 0) ^ k = a $ 0" - and ria0: "r (k) (inverse (a $ 0)) = inverse (r (k) (a $ 0))" - and r1: "(r (k) 1) = 1" - and a0: "a$0 \ 0" - shows "fps_radical r (k) (inverse a) = inverse (fps_radical r (k) a)" -proof- - {assume "k=0" then have ?thesis by simp} - moreover - {fix h assume k[simp]: "k = Suc h" - let ?ra = "fps_radical r (Suc h) a" - let ?ria = "fps_radical r (Suc h) (inverse a)" - from ra0 a0 have th00: "r (Suc h) (a$0) \ 0" by auto - have ria0': "r (Suc h) (inverse a $ 0) ^ Suc h = inverse a$0" - using ria0 ra0 a0 - by (simp add: fps_inverse_def nonzero_power_inverse[OF th00, symmetric] - del: power_Suc) - from inverse_mult_eq_1[OF a0] have th0: "a * inverse a = 1" - by (simp add: mult_commute) - from radical_unique[where a=1 and b=1 and r=r and k=h, simplified, OF r1[unfolded k]] - have th01: "fps_radical r (Suc h) 1 = 1" . - have th1: "r (Suc h) ((a * inverse a) $ 0) ^ Suc h = (a * inverse a) $ 0" - "r (Suc h) ((a * inverse a) $ 0) = -r (Suc h) (a $ 0) * r (Suc h) (inverse a $ 0)" - using r1 unfolding th0 apply (simp_all add: ria0[symmetric]) - apply (simp add: fps_inverse_def a0) - unfolding ria0[unfolded k] - using th00 by simp - from nonzero_imp_inverse_nonzero[OF a0] a0 - have th2: "inverse a $ 0 \ 0" by (simp add: fps_inverse_def) - from radical_mult_distrib[of r "Suc h" a "inverse a", OF ra0[unfolded k] ria0' th1(2) a0 th2] - have th3: "?ra * ?ria = 1" unfolding th0 th01 by simp - from th00 have ra0: "?ra $ 0 \ 0" by simp - from fps_inverse_unique[OF ra0 th3] have ?thesis by simp} -ultimately show ?thesis by (cases k, auto) -qed - -lemma fps_divide_inverse: "(a::('a::field) fps) / b = a * inverse b" +lemma fps_divide_1[simp]: "(a:: ('a::field) fps) / 1 = a" by (simp add: fps_divide_def) lemma radical_divide: fixes a:: "'a ::{field, ring_char_0} fps" assumes - ra0: "r k (a $ 0) ^ k = a $ 0" - and rb0: "r k (b $ 0) ^ k = b $ 0" - and r1: "r k 1 = 1" - and rb0': "r k (inverse (b $ 0)) = inverse (r k (b $ 0))" - and raib': "r k (a$0 / (b$0)) = r k (a$0) / r k (b$0)" + kp: "k>0" + and ra0: "(r k (a $ 0)) ^ k = a $ 0" + and rb0: "(r k (b $ 0)) ^ k = b $ 0" + and r1: "(r k 1)^k = 1" and a0: "a$0 \ 0" and b0: "b$0 \ 0" - shows "fps_radical r k (a/b) = fps_radical r k a / fps_radical r k b" + shows "r k ((a $ 0) / (b$0)) = r k (a$0) / r k (b $ 0) \ fps_radical r k (a/b) = fps_radical r k a / fps_radical r k b" (is "?lhs = ?rhs") proof- - from raib' - have raib: "r k (a$0 / (b$0)) = r k (a$0) * r k (inverse (b$0))" - by (simp add: divide_inverse rb0'[symmetric]) - - {assume "k=0" hence ?thesis by (simp add: fps_divide_def)} - moreover - {assume k0: "k\ 0" - from b0 k0 rb0 have rbn0: "r k (b $0) \ 0" - by (auto simp add: power_0_left) + let ?r = "fps_radical r k" + from kp obtain h where k: "k = Suc h" by (cases k, auto) + have ra0': "r k (a$0) \ 0" using a0 ra0 k by auto + have rb0': "r k (b$0) \ 0" using b0 rb0 k by auto - from rb0 rb0' have rib0: "(r k (inverse (b $ 0)))^k = inverse (b$0)" - by (simp add: nonzero_power_inverse[OF rbn0, symmetric]) - from rib0 have th0: "r k (inverse b $ 0) ^ k = inverse b $ 0" - by (simp add:fps_inverse_def b0) - from raib - have th1: "r k ((a * inverse b) $ 0) = r k (a $ 0) * r k (inverse b $ 0)" - by (simp add: divide_inverse fps_inverse_def b0 fps_mult_nth) - from nonzero_imp_inverse_nonzero[OF b0] b0 have th2: "inverse b $ 0 \ 0" - by (simp add: fps_inverse_def) - from radical_mult_distrib[of r k a "inverse b", OF ra0 th0 th1 a0 th2] - have th: "fps_radical r k (a/b) = fps_radical r k a * fps_radical r k (inverse b)" - by (simp add: fps_divide_def) - with radical_inverse[of r k b, OF rb0 rb0' r1 b0] - have ?thesis by (simp add: fps_divide_def)} -ultimately show ?thesis by blast + {assume ?rhs + then have "?r (a/b) $ 0 = (?r a / ?r b)$0" by simp + then have ?lhs using k a0 b0 rb0' + by (simp add: fps_divide_def fps_mult_nth fps_inverse_def divide_inverse) } + moreover + {assume h: ?lhs + from a0 b0 have ab0[simp]: "(a/b)$0 = a$0 / b$0" + by (simp add: fps_divide_def fps_mult_nth divide_inverse fps_inverse_def) + have th0: "r k ((a/b)$0) ^ k = (a/b)$0" + by (simp add: h nonzero_power_divide[OF rb0'] ra0 rb0 del: k) + from a0 b0 ra0' rb0' kp h + have th1: "r k ((a / b) $ 0) = (fps_radical r k a / fps_radical r k b) $ 0" + by (simp add: fps_divide_def fps_mult_nth fps_inverse_def divide_inverse del: k) + from a0 b0 ra0' rb0' kp have ab0': "(a / b) $ 0 \ 0" + by (simp add: fps_divide_def fps_mult_nth fps_inverse_def nonzero_imp_inverse_nonzero) + note tha[simp] = iffD1[OF power_radical[where r=r and k=h], OF a0 ra0[unfolded k], unfolded k[symmetric]] + note thb[simp] = iffD1[OF power_radical[where r=r and k=h], OF b0 rb0[unfolded k], unfolded k[symmetric]] + have th2: "(?r a / ?r b)^k = a/b" + by (simp add: fps_divide_def power_mult_distrib fps_inverse_power[symmetric]) + from iffD1[OF radical_unique[where r=r and a="?r a / ?r b" and b="a/b" and k=h], symmetric, unfolded k[symmetric], OF th0 th1 ab0' th2] have ?rhs .} + ultimately show ?thesis by blast qed +lemma radical_inverse: + fixes a:: "'a ::{field, ring_char_0} fps" + assumes + k: "k>0" + and ra0: "r k (a $ 0) ^ k = a $ 0" + and r1: "(r k 1)^k = 1" + and a0: "a$0 \ 0" + shows "r k (inverse (a $ 0)) = r k 1 / (r k (a $ 0)) \ fps_radical r k (inverse a) = fps_radical r k 1 / fps_radical r k a" + using radical_divide[where k=k and r=r and a=1 and b=a, OF k ] ra0 r1 a0 + by (simp add: divide_inverse fps_divide_def) + subsection{* Derivative of composition *} lemma fps_compose_deriv: diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Fri May 08 08:07:05 2009 +0200 +++ b/src/HOL/Nat_Numeral.thy Fri May 08 19:20:00 2009 +0200 @@ -7,7 +7,7 @@ theory Nat_Numeral imports IntDiv -uses ("Tools/nat_simprocs.ML") +uses ("Tools/nat_numeral_simprocs.ML") begin subsection {* Numerals for natural numbers *} @@ -455,29 +455,6 @@ declare dvd_eq_mod_eq_0_number_of [simp] -ML -{* -val nat_number_of_def = thm"nat_number_of_def"; - -val nat_number_of = thm"nat_number_of"; -val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0"; -val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1"; -val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0"; -val numeral_2_eq_2 = thm"numeral_2_eq_2"; -val nat_div_distrib = thm"nat_div_distrib"; -val nat_mod_distrib = thm"nat_mod_distrib"; -val int_nat_number_of = thm"int_nat_number_of"; -val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1"; -val Suc_nat_number_of_add = thm"Suc_nat_number_of_add"; -val Suc_nat_number_of = thm"Suc_nat_number_of"; -val add_nat_number_of = thm"add_nat_number_of"; -val diff_nat_eq_if = thm"diff_nat_eq_if"; -val diff_nat_number_of = thm"diff_nat_number_of"; -val mult_nat_number_of = thm"mult_nat_number_of"; -val div_nat_number_of = thm"div_nat_number_of"; -val mod_nat_number_of = thm"mod_nat_number_of"; -*} - subsection{*Comparisons*} @@ -737,23 +714,6 @@ power_number_of_odd [of "number_of v", standard] - -ML -{* -val numeral_ss = @{simpset} addsimps @{thms numerals}; - -val nat_bin_arith_setup = - Lin_Arith.map_data - (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => - {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, - inj_thms = inj_thms, - lessD = lessD, neqE = neqE, - simpset = simpset addsimps @{thms neg_simps} @ - [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]}) -*} - -declaration {* K nat_bin_arith_setup *} - (* Enable arith to deal with div/mod k where k is a numeral: *) declare split_div[of _ _ "number_of k", standard, arith_split] declare split_mod[of _ _ "number_of k", standard, arith_split] @@ -912,8 +872,37 @@ subsection {* Simprocs for the Naturals *} -use "Tools/nat_simprocs.ML" -declaration {* K nat_simprocs_setup *} +use "Tools/nat_numeral_simprocs.ML" + +declaration {* +let + +val less_eq_rules = @{thms ring_distribs} @ + [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1}, + @{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}, @{thm le_number_of_eq_not_less}, + @{thm le_Suc_number_of}, @{thm le_number_of_Suc}, + @{thm less_Suc_number_of}, @{thm less_number_of_Suc}, + @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc}, + @{thm mult_Suc}, @{thm mult_Suc_right}, + @{thm add_Suc}, @{thm add_Suc_right}, + @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of}, + @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}]; + +val simprocs = Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals; + +in + +K (Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, + inj_thms = inj_thms, lessD = lessD, neqE = neqE, + simpset = simpset addsimps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]) + addsimps less_eq_rules + addsimprocs simprocs})) + +end +*} + subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Fri May 08 08:07:05 2009 +0200 +++ b/src/HOL/Tools/int_arith.ML Fri May 08 19:20:00 2009 +0200 @@ -1,420 +1,15 @@ -(* Authors: Larry Paulson and Tobias Nipkow - -Simprocs and decision procedure for numerals and linear arithmetic. -*) - -structure Int_Numeral_Simprocs = -struct - -(** Utilities **) - -fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; - -fun find_first_numeral past (t::terms) = - ((snd (HOLogic.dest_number t), rev past @ terms) - handle TERM _ => find_first_numeral (t::past) terms) - | find_first_numeral past [] = raise TERM("find_first_numeral", []); - -val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; - -fun mk_minus t = - let val T = Term.fastype_of t - in Const (@{const_name HOL.uminus}, T --> T) $ t end; - -(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) -fun mk_sum T [] = mk_number T 0 - | mk_sum T [t,u] = mk_plus (t, u) - | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); - -(*this version ALWAYS includes a trailing zero*) -fun long_mk_sum T [] = mk_number T 0 - | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); - -val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT; - -(*decompose additions AND subtractions as a sum*) -fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (pos, u, ts)) - | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (not pos, u, ts)) - | dest_summing (pos, t, ts) = - if pos then t::ts else mk_minus t :: ts; - -fun dest_sum t = dest_summing (true, t, []); - -val mk_diff = HOLogic.mk_binop @{const_name HOL.minus}; -val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT; - -val mk_times = HOLogic.mk_binop @{const_name HOL.times}; - -fun one_of T = Const(@{const_name HOL.one},T); - -(* build product with trailing 1 rather than Numeral 1 in order to avoid the - unnecessary restriction to type class number_ring - which is not required for cancellation of common factors in divisions. -*) -fun mk_prod T = - let val one = one_of T - fun mk [] = one - | mk [t] = t - | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts) - in mk end; - -(*This version ALWAYS includes a trailing one*) -fun long_mk_prod T [] = one_of T - | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); - -val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT; - -fun dest_prod t = - let val (t,u) = dest_times t - in dest_prod t @ dest_prod u end - handle TERM _ => [t]; - -(*DON'T do the obvious simplifications; that would create special cases*) -fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); - -(*Express t as a product of (possibly) a numeral with other sorted terms*) -fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t - | dest_coeff sign t = - let val ts = sort TermOrd.term_ord (dest_prod t) - val (n, ts') = find_first_numeral [] ts - handle TERM _ => (1, ts) - in (sign*n, mk_prod (Term.fastype_of t) ts') end; - -(*Find first coefficient-term THAT MATCHES u*) -fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) - | find_first_coeff past u (t::terms) = - let val (n,u') = dest_coeff 1 t - in if u aconv u' then (n, rev past @ terms) - else find_first_coeff (t::past) u terms - end - handle TERM _ => find_first_coeff (t::past) u terms; - -(*Fractions as pairs of ints. Can't use Rat.rat because the representation - needs to preserve negative values in the denominator.*) -fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); - -(*Don't reduce fractions; sums must be proved by rule add_frac_eq. - Fractions are reduced later by the cancel_numeral_factor simproc.*) -fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); - -val mk_divide = HOLogic.mk_binop @{const_name HOL.divide}; - -(*Build term (p / q) * t*) -fun mk_fcoeff ((p, q), t) = - let val T = Term.fastype_of t - in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; - -(*Express t as a product of a fraction with other sorted terms*) -fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t - | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) = - let val (p, t') = dest_coeff sign t - val (q, u') = dest_coeff 1 u - in (mk_frac (p, q), mk_divide (t', u')) end - | dest_fcoeff sign t = - let val (p, t') = dest_coeff sign t - val T = Term.fastype_of t - in (mk_frac (p, 1), mk_divide (t', one_of T)) end; - - -(** New term ordering so that AC-rewriting brings numerals to the front **) - -(*Order integers by absolute value and then by sign. The standard integer - ordering is not well-founded.*) -fun num_ord (i,j) = - (case int_ord (abs i, abs j) of - EQUAL => int_ord (Int.sign i, Int.sign j) - | ord => ord); - -(*This resembles TermOrd.term_ord, but it puts binary numerals before other - non-atomic terms.*) -local open Term -in -fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) = - (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord) - | numterm_ord - (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) = - num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w) - | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS - | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER - | numterm_ord (t, u) = - (case int_ord (size_of_term t, size_of_term u) of - EQUAL => - let val (f, ts) = strip_comb t and (g, us) = strip_comb u in - (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord) - end - | ord => ord) -and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) -end; - -fun numtermless tu = (numterm_ord tu = LESS); - -val num_ss = HOL_ss settermless numtermless; - -(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*) -val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym]; - -(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) -val add_0s = @{thms add_0s}; -val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1}; - -(*Simplify inverse Numeral1, a/Numeral1*) -val inverse_1s = [@{thm inverse_numeral_1}]; -val divide_1s = [@{thm divide_numeral_1}]; - -(*To perform binary arithmetic. The "left" rewriting handles patterns - created by the Int_Numeral_Simprocs, such as 3 * (5 * x). *) -val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym, - @{thm add_number_of_left}, @{thm mult_number_of_left}] @ - @{thms arith_simps} @ @{thms rel_simps}; - -(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms - during re-arrangement*) -val non_add_simps = - subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps; - -(*To evaluate binary negations of coefficients*) -val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @ - @{thms minus_bin_simps} @ @{thms pred_bin_simps}; - -(*To let us treat subtraction as addition*) -val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}]; - -(*To let us treat division as multiplication*) -val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; - -(*push the unary minus down: - x * y = x * - y *) -val minus_mult_eq_1_to_2 = - [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard; - -(*to extract again any uncancelled minuses*) -val minus_from_mult_simps = - [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}]; - -(*combine unary minus with numeric literals, however nested within a product*) -val mult_minus_simps = - [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2]; - -val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ - diff_simps @ minus_simps @ @{thms add_ac} -val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps -val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} +(* Author: Tobias Nipkow -structure CancelNumeralsCommon = - struct - val mk_sum = mk_sum - val dest_sum = dest_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val find_first_coeff = find_first_coeff [] - val trans_tac = K Arith_Data.trans_tac - - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) - - val numeral_simp_ss = HOL_ss addsimps add_0s @ simps - fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) - end; - - -structure EqCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" Term.dummyT - val bal_add1 = @{thm eq_add_iff1} RS trans - val bal_add2 = @{thm eq_add_iff2} RS trans -); - -structure LessCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT - val bal_add1 = @{thm less_add_iff1} RS trans - val bal_add2 = @{thm less_add_iff2} RS trans -); - -structure LeCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT - val bal_add1 = @{thm le_add_iff1} RS trans - val bal_add2 = @{thm le_add_iff2} RS trans -); - -val cancel_numerals = - map Arith_Data.prep_simproc - [("inteq_cancel_numerals", - ["(l::'a::number_ring) + m = n", - "(l::'a::number_ring) = m + n", - "(l::'a::number_ring) - m = n", - "(l::'a::number_ring) = m - n", - "(l::'a::number_ring) * m = n", - "(l::'a::number_ring) = m * n"], - K EqCancelNumerals.proc), - ("intless_cancel_numerals", - ["(l::'a::{ordered_idom,number_ring}) + m < n", - "(l::'a::{ordered_idom,number_ring}) < m + n", - "(l::'a::{ordered_idom,number_ring}) - m < n", - "(l::'a::{ordered_idom,number_ring}) < m - n", - "(l::'a::{ordered_idom,number_ring}) * m < n", - "(l::'a::{ordered_idom,number_ring}) < m * n"], - K LessCancelNumerals.proc), - ("intle_cancel_numerals", - ["(l::'a::{ordered_idom,number_ring}) + m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m + n", - "(l::'a::{ordered_idom,number_ring}) - m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m - n", - "(l::'a::{ordered_idom,number_ring}) * m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m * n"], - K LeCancelNumerals.proc)]; - - -structure CombineNumeralsData = - struct - type coeff = int - val iszero = (fn x => x = 0) - val add = op + - val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) - val dest_sum = dest_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val left_distrib = @{thm combine_common_factor} RS trans - val prove_conv = Arith_Data.prove_conv_nohyps - val trans_tac = K Arith_Data.trans_tac - - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) - - val numeral_simp_ss = HOL_ss addsimps add_0s @ simps - fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) - end; - -structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); - -(*Version for fields, where coefficients can be fractions*) -structure FieldCombineNumeralsData = - struct - type coeff = int * int - val iszero = (fn (p, q) => p = 0) - val add = add_frac - val mk_sum = long_mk_sum - val dest_sum = dest_sum - val mk_coeff = mk_fcoeff - val dest_coeff = dest_fcoeff 1 - val left_distrib = @{thm combine_common_factor} RS trans - val prove_conv = Arith_Data.prove_conv_nohyps - val trans_tac = K Arith_Data.trans_tac - - val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) - - val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}] - fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s) - end; - -structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); - -val combine_numerals = - Arith_Data.prep_simproc - ("int_combine_numerals", - ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], - K CombineNumerals.proc); - -val field_combine_numerals = - Arith_Data.prep_simproc - ("field_combine_numerals", - ["(i::'a::{number_ring,field,division_by_zero}) + j", - "(i::'a::{number_ring,field,division_by_zero}) - j"], - K FieldCombineNumerals.proc); - -(** Constant folding for multiplication in semirings **) - -(*We do not need folding for addition: combine_numerals does the same thing*) - -structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = -struct - val assoc_ss = HOL_ss addsimps @{thms mult_ac} - val eq_reflection = eq_reflection - fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true - | is_numeral _ = false; -end; - -structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); - -val assoc_fold_simproc = - Arith_Data.prep_simproc - ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"], - K Semiring_Times_Assoc.proc); - -end; - -Addsimprocs Int_Numeral_Simprocs.cancel_numerals; -Addsimprocs [Int_Numeral_Simprocs.combine_numerals]; -Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals]; -Addsimprocs [Int_Numeral_Simprocs.assoc_fold_simproc]; - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s, by (Simp_tac 1)); - -test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"; - -test "2*u = (u::int)"; -test "(i + j + 12 + (k::int)) - 15 = y"; -test "(i + j + 12 + (k::int)) - 5 = y"; - -test "y - b < (b::int)"; -test "y - (3*b + c) < (b::int) - 2*c"; - -test "(2*x - (u*v) + y) - v*3*u = (w::int)"; -test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"; -test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"; -test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"; - -test "(i + j + 12 + (k::int)) = u + 15 + y"; -test "(i + j*2 + 12 + (k::int)) = j + 5 + y"; - -test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"; - -test "a + -(b+c) + b = (d::int)"; -test "a + -(b+c) - b = (d::int)"; - -(*negative numerals*) -test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"; -test "(i + j + -3 + (k::int)) < u + 5 + y"; -test "(i + j + 3 + (k::int)) < u + -6 + y"; -test "(i + j + -12 + (k::int)) - 15 = y"; -test "(i + j + 12 + (k::int)) - -15 = y"; -test "(i + j + -12 + (k::int)) - -15 = y"; -*) - -(*** decision procedure for linear arithmetic ***) - -(*---------------------------------------------------------------------------*) -(* Linear arithmetic *) -(*---------------------------------------------------------------------------*) - -(* Instantiation of the generic linear arithmetic package for int. *) -structure Int_Arith = +signature INT_ARITH = +sig + val fast_int_arith_simproc: simproc + val setup: Context.generic -> Context.generic +end + +structure Int_Arith : INT_ARITH = struct (* Update parameters of arithmetic prover *) @@ -491,9 +86,9 @@ val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2] -val int_numeral_base_simprocs = Int_Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc - :: Int_Numeral_Simprocs.combine_numerals - :: Int_Numeral_Simprocs.cancel_numerals; +val numeral_base_simprocs = Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc + :: Numeral_Simprocs.combine_numerals + :: Numeral_Simprocs.cancel_numerals; val setup = Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => @@ -503,7 +98,7 @@ lessD = lessD @ [@{thm zless_imp_add1_zle}], neqE = neqE, simpset = simpset addsimps add_rules - addsimprocs int_numeral_base_simprocs + addsimprocs numeral_base_simprocs addcongs [if_weak_cong]}) #> arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #> arith_discrete @{type_name Int.int} diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Tools/int_factor_simprocs.ML --- a/src/HOL/Tools/int_factor_simprocs.ML Fri May 08 08:07:05 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,391 +0,0 @@ -(* Title: HOL/int_factor_simprocs.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2000 University of Cambridge - -Factor cancellation simprocs for the integers (and for fields). - -This file can't be combined with int_arith1 because it requires IntDiv.thy. -*) - - -(*To quote from Provers/Arith/cancel_numeral_factor.ML: - -Cancels common coefficients in balanced expressions: - - u*#m ~~ u'*#m' == #n*u ~~ #n'*u' - -where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) -and d = gcd(m,m') and n=m/d and n'=m'/d. -*) - -val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}]; - -local - open Int_Numeral_Simprocs -in - -structure CancelNumeralFactorCommon = - struct - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val trans_tac = K Arith_Data.trans_tac - - val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s - val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps - val norm_ss3 = HOL_ss addsimps @{thms mult_ac} - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) - - val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps - fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = Arith_Data.simplify_meta_eq - [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left}, - @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}]; - end - -(*Version for semiring_div*) -structure DivCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name Divides.div} - val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT - val cancel = @{thm div_mult_mult1} RS trans - val neg_exchanges = false -) - -(*Version for fields*) -structure DivideCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} - val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT - val cancel = @{thm mult_divide_mult_cancel_left} RS trans - val neg_exchanges = false -) - -structure EqCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" Term.dummyT - val cancel = @{thm mult_cancel_left} RS trans - val neg_exchanges = false -) - -structure LessCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT - val cancel = @{thm mult_less_cancel_left} RS trans - val neg_exchanges = true -) - -structure LeCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT - val cancel = @{thm mult_le_cancel_left} RS trans - val neg_exchanges = true -) - -val cancel_numeral_factors = - map Arith_Data.prep_simproc - [("ring_eq_cancel_numeral_factor", - ["(l::'a::{idom,number_ring}) * m = n", - "(l::'a::{idom,number_ring}) = m * n"], - K EqCancelNumeralFactor.proc), - ("ring_less_cancel_numeral_factor", - ["(l::'a::{ordered_idom,number_ring}) * m < n", - "(l::'a::{ordered_idom,number_ring}) < m * n"], - K LessCancelNumeralFactor.proc), - ("ring_le_cancel_numeral_factor", - ["(l::'a::{ordered_idom,number_ring}) * m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m * n"], - K LeCancelNumeralFactor.proc), - ("int_div_cancel_numeral_factors", - ["((l::'a::{semiring_div,number_ring}) * m) div n", - "(l::'a::{semiring_div,number_ring}) div (m * n)"], - K DivCancelNumeralFactor.proc), - ("divide_cancel_numeral_factor", - ["((l::'a::{division_by_zero,field,number_ring}) * m) / n", - "(l::'a::{division_by_zero,field,number_ring}) / (m * n)", - "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"], - K DivideCancelNumeralFactor.proc)]; - -(* referenced by rat_arith.ML *) -val field_cancel_numeral_factors = - map Arith_Data.prep_simproc - [("field_eq_cancel_numeral_factor", - ["(l::'a::{field,number_ring}) * m = n", - "(l::'a::{field,number_ring}) = m * n"], - K EqCancelNumeralFactor.proc), - ("field_cancel_numeral_factor", - ["((l::'a::{division_by_zero,field,number_ring}) * m) / n", - "(l::'a::{division_by_zero,field,number_ring}) / (m * n)", - "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"], - K DivideCancelNumeralFactor.proc)] - -end; - -Addsimprocs cancel_numeral_factors; - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Simp_tac 1)); - -test "9*x = 12 * (y::int)"; -test "(9*x) div (12 * (y::int)) = z"; -test "9*x < 12 * (y::int)"; -test "9*x <= 12 * (y::int)"; - -test "-99*x = 132 * (y::int)"; -test "(-99*x) div (132 * (y::int)) = z"; -test "-99*x < 132 * (y::int)"; -test "-99*x <= 132 * (y::int)"; - -test "999*x = -396 * (y::int)"; -test "(999*x) div (-396 * (y::int)) = z"; -test "999*x < -396 * (y::int)"; -test "999*x <= -396 * (y::int)"; - -test "-99*x = -81 * (y::int)"; -test "(-99*x) div (-81 * (y::int)) = z"; -test "-99*x <= -81 * (y::int)"; -test "-99*x < -81 * (y::int)"; - -test "-2 * x = -1 * (y::int)"; -test "-2 * x = -(y::int)"; -test "(-2 * x) div (-1 * (y::int)) = z"; -test "-2 * x < -(y::int)"; -test "-2 * x <= -1 * (y::int)"; -test "-x < -23 * (y::int)"; -test "-x <= -23 * (y::int)"; -*) - -(*And the same examples for fields such as rat or real: -test "0 <= (y::rat) * -2"; -test "9*x = 12 * (y::rat)"; -test "(9*x) / (12 * (y::rat)) = z"; -test "9*x < 12 * (y::rat)"; -test "9*x <= 12 * (y::rat)"; - -test "-99*x = 132 * (y::rat)"; -test "(-99*x) / (132 * (y::rat)) = z"; -test "-99*x < 132 * (y::rat)"; -test "-99*x <= 132 * (y::rat)"; - -test "999*x = -396 * (y::rat)"; -test "(999*x) / (-396 * (y::rat)) = z"; -test "999*x < -396 * (y::rat)"; -test "999*x <= -396 * (y::rat)"; - -test "(- ((2::rat) * x) <= 2 * y)"; -test "-99*x = -81 * (y::rat)"; -test "(-99*x) / (-81 * (y::rat)) = z"; -test "-99*x <= -81 * (y::rat)"; -test "-99*x < -81 * (y::rat)"; - -test "-2 * x = -1 * (y::rat)"; -test "-2 * x = -(y::rat)"; -test "(-2 * x) / (-1 * (y::rat)) = z"; -test "-2 * x < -(y::rat)"; -test "-2 * x <= -1 * (y::rat)"; -test "-x < -23 * (y::rat)"; -test "-x <= -23 * (y::rat)"; -*) - - -(** Declarations for ExtractCommonTerm **) - -local - open Int_Numeral_Simprocs -in - -(*Find first term that matches u*) -fun find_first_t past u [] = raise TERM ("find_first_t", []) - | find_first_t past u (t::terms) = - if u aconv t then (rev past @ terms) - else find_first_t (t::past) u terms - handle TERM _ => find_first_t (t::past) u terms; - -(** Final simplification for the CancelFactor simprocs **) -val simplify_one = Arith_Data.simplify_meta_eq - [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}]; - -fun cancel_simplify_meta_eq ss cancel_th th = - simplify_one ss (([th, cancel_th]) MRS trans); - -local - val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop) - fun Eq_True_elim Eq = - Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI} -in -fun sign_conv pos_th neg_th ss t = - let val T = fastype_of t; - val zero = Const(@{const_name HOL.zero}, T); - val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT); - val pos = less $ zero $ t and neg = less $ t $ zero - fun prove p = - Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p) - handle THM _ => NONE - in case prove pos of - SOME th => SOME(th RS pos_th) - | NONE => (case prove neg of - SOME th => SOME(th RS neg_th) - | NONE => NONE) - end; -end - -structure CancelFactorCommon = - struct - val mk_sum = long_mk_prod - val dest_sum = dest_prod - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first = find_first_t [] - val trans_tac = K Arith_Data.trans_tac - val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} - fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) - val simplify_meta_eq = cancel_simplify_meta_eq - end; - -(*mult_cancel_left requires a ring with no zero divisors.*) -structure EqCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" Term.dummyT - val simp_conv = K (K (SOME @{thm mult_cancel_left})) -); - -(*for ordered rings*) -structure LeCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT - val simp_conv = sign_conv - @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg} -); - -(*for ordered rings*) -structure LessCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT - val simp_conv = sign_conv - @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg} -); - -(*for semirings with division*) -structure DivCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name Divides.div} - val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT - val simp_conv = K (K (SOME @{thm div_mult_mult1_if})) -); - -structure ModCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} - val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT - val simp_conv = K (K (SOME @{thm mod_mult_mult1})) -); - -(*for idoms*) -structure DvdCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} - val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT - val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left})) -); - -(*Version for all fields, including unordered ones (type complex).*) -structure DivideCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} - val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT - val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if})) -); - -val cancel_factors = - map Arith_Data.prep_simproc - [("ring_eq_cancel_factor", - ["(l::'a::idom) * m = n", - "(l::'a::idom) = m * n"], - K EqCancelFactor.proc), - ("ordered_ring_le_cancel_factor", - ["(l::'a::ordered_ring) * m <= n", - "(l::'a::ordered_ring) <= m * n"], - K LeCancelFactor.proc), - ("ordered_ring_less_cancel_factor", - ["(l::'a::ordered_ring) * m < n", - "(l::'a::ordered_ring) < m * n"], - K LessCancelFactor.proc), - ("int_div_cancel_factor", - ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"], - K DivCancelFactor.proc), - ("int_mod_cancel_factor", - ["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"], - K ModCancelFactor.proc), - ("dvd_cancel_factor", - ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"], - K DvdCancelFactor.proc), - ("divide_cancel_factor", - ["((l::'a::{division_by_zero,field}) * m) / n", - "(l::'a::{division_by_zero,field}) / (m * n)"], - K DivideCancelFactor.proc)]; - -end; - -Addsimprocs cancel_factors; - - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Asm_simp_tac 1)); - -test "x*k = k*(y::int)"; -test "k = k*(y::int)"; -test "a*(b*c) = (b::int)"; -test "a*(b*c) = d*(b::int)*(x*a)"; - -test "(x*k) div (k*(y::int)) = (uu::int)"; -test "(k) div (k*(y::int)) = (uu::int)"; -test "(a*(b*c)) div ((b::int)) = (uu::int)"; -test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"; -*) - -(*And the same examples for fields such as rat or real: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Asm_simp_tac 1)); - -test "x*k = k*(y::rat)"; -test "k = k*(y::rat)"; -test "a*(b*c) = (b::rat)"; -test "a*(b*c) = d*(b::rat)*(x*a)"; - - -test "(x*k) / (k*(y::rat)) = (uu::rat)"; -test "(k) / (k*(y::rat)) = (uu::rat)"; -test "(a*(b*c)) / ((b::rat)) = (uu::rat)"; -test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"; - -(*FIXME: what do we do about this?*) -test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"; -*) diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Tools/nat_numeral_simprocs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Fri May 08 19:20:00 2009 +0200 @@ -0,0 +1,538 @@ +(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory + +Simprocs for nat numerals. +*) + +signature NAT_NUMERAL_SIMPROCS = +sig + val combine_numerals: simproc + val cancel_numerals: simproc list + val cancel_factors: simproc list + val cancel_numeral_factors: simproc list +end; + +structure Nat_Numeral_Simprocs = +struct + +(*Maps n to #n for n = 0, 1, 2*) +val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym]; +val numeral_sym_ss = HOL_ss addsimps numeral_syms; + +fun rename_numerals th = + simplify numeral_sym_ss (Thm.transfer (the_context ()) th); + +(*Utilities*) + +fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n; +fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); + +fun find_first_numeral past (t::terms) = + ((dest_number t, t, rev past @ terms) + handle TERM _ => find_first_numeral (t::past) terms) + | find_first_numeral past [] = raise TERM("find_first_numeral", []); + +val zero = mk_number 0; +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; + +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) +fun mk_sum [] = zero + | mk_sum [t,u] = mk_plus (t, u) + | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); + +(*this version ALWAYS includes a trailing zero*) +fun long_mk_sum [] = HOLogic.zero + | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); + +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT; + + +(** Other simproc items **) + +val bin_simps = + [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, + @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, + @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less}, + @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, + @{thm less_nat_number_of}, + @{thm Let_number_of}, @{thm nat_number_of}] @ + @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps}; + + +(*** CancelNumerals simprocs ***) + +val one = mk_number 1; +val mk_times = HOLogic.mk_binop @{const_name HOL.times}; + +fun mk_prod [] = one + | mk_prod [t] = t + | mk_prod (t :: ts) = if t = one then mk_prod ts + else mk_times (t, mk_prod ts); + +val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT; + +fun dest_prod t = + let val (t,u) = dest_times t + in dest_prod t @ dest_prod u end + handle TERM _ => [t]; + +(*DON'T do the obvious simplifications; that would create special cases*) +fun mk_coeff (k,t) = mk_times (mk_number k, t); + +(*Express t as a product of (possibly) a numeral with other factors, sorted*) +fun dest_coeff t = + let val ts = sort TermOrd.term_ord (dest_prod t) + val (n, _, ts') = find_first_numeral [] ts + handle TERM _ => (1, one, ts) + in (n, mk_prod ts') end; + +(*Find first coefficient-term THAT MATCHES u*) +fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) + | find_first_coeff past u (t::terms) = + let val (n,u') = dest_coeff t + in if u aconv u' then (n, rev past @ terms) + else find_first_coeff (t::past) u terms + end + handle TERM _ => find_first_coeff (t::past) u terms; + + +(*Split up a sum into the list of its constituent terms, on the way removing any + Sucs and counting them.*) +fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts)) + | dest_Suc_sum (t, (k,ts)) = + let val (t1,t2) = dest_plus t + in dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts))) end + handle TERM _ => (k, t::ts); + +(*Code for testing whether numerals are already used in the goal*) +fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true + | is_numeral _ = false; + +fun prod_has_numeral t = exists is_numeral (dest_prod t); + +(*The Sucs found in the term are converted to a binary numeral. If relaxed is false, + an exception is raised unless the original expression contains at least one + numeral in a coefficient position. This prevents nat_combine_numerals from + introducing numerals to goals.*) +fun dest_Sucs_sum relaxed t = + let val (k,ts) = dest_Suc_sum (t,(0,[])) + in + if relaxed orelse exists prod_has_numeral ts then + if k=0 then ts + else mk_number k :: ts + else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t]) + end; + + +(*Simplify 1*n and n*1 to n*) +val add_0s = map rename_numerals [@{thm add_0}, @{thm add_0_right}]; +val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}]; + +(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*) + +(*And these help the simproc return False when appropriate, which helps + the arith prover.*) +val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc}, + @{thm Suc_not_Zero}, @{thm le_0_eq}]; + +val simplify_meta_eq = + Arith_Data.simplify_meta_eq + ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right}, + @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules); + + +(*** Applying CancelNumeralsFun ***) + +structure CancelNumeralsCommon = + struct + val mk_sum = (fn T:typ => mk_sum) + val dest_sum = dest_Sucs_sum true + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first_coeff = find_first_coeff [] + val trans_tac = K Arith_Data.trans_tac + + val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ + [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} + val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)); + val simplify_meta_eq = simplify_meta_eq + end; + + +structure EqCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT + val bal_add1 = @{thm nat_eq_add_iff1} RS trans + val bal_add2 = @{thm nat_eq_add_iff2} RS trans +); + +structure LessCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT + val bal_add1 = @{thm nat_less_add_iff1} RS trans + val bal_add2 = @{thm nat_less_add_iff2} RS trans +); + +structure LeCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT + val bal_add1 = @{thm nat_le_add_iff1} RS trans + val bal_add2 = @{thm nat_le_add_iff2} RS trans +); + +structure DiffCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name HOL.minus} + val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT + val bal_add1 = @{thm nat_diff_add_eq1} RS trans + val bal_add2 = @{thm nat_diff_add_eq2} RS trans +); + + +val cancel_numerals = + map Arith_Data.prep_simproc + [("nateq_cancel_numerals", + ["(l::nat) + m = n", "(l::nat) = m + n", + "(l::nat) * m = n", "(l::nat) = m * n", + "Suc m = n", "m = Suc n"], + K EqCancelNumerals.proc), + ("natless_cancel_numerals", + ["(l::nat) + m < n", "(l::nat) < m + n", + "(l::nat) * m < n", "(l::nat) < m * n", + "Suc m < n", "m < Suc n"], + K LessCancelNumerals.proc), + ("natle_cancel_numerals", + ["(l::nat) + m <= n", "(l::nat) <= m + n", + "(l::nat) * m <= n", "(l::nat) <= m * n", + "Suc m <= n", "m <= Suc n"], + K LeCancelNumerals.proc), + ("natdiff_cancel_numerals", + ["((l::nat) + m) - n", "(l::nat) - (m + n)", + "(l::nat) * m - n", "(l::nat) - m * n", + "Suc m - n", "m - Suc n"], + K DiffCancelNumerals.proc)]; + + +(*** Applying CombineNumeralsFun ***) + +structure CombineNumeralsData = + struct + type coeff = int + val iszero = (fn x => x = 0) + val add = op + + val mk_sum = (fn T:typ => long_mk_sum) (*to work for 2*x + 3*x *) + val dest_sum = dest_Sucs_sum false + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val left_distrib = @{thm left_add_mult_distrib} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps + val trans_tac = K Arith_Data.trans_tac + + val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac} + val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = simplify_meta_eq + end; + +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); + +val combine_numerals = + Arith_Data.prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc); + + +(*** Applying CancelNumeralFactorFun ***) + +structure CancelNumeralFactorCommon = + struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val trans_tac = K Arith_Data.trans_tac + + val norm_ss1 = Numeral_Simprocs.num_ss addsimps + numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} + val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + + val numeral_simp_ss = HOL_ss addsimps bin_simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = simplify_meta_eq + end + +structure DivCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.div} + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT + val cancel = @{thm nat_mult_div_cancel1} RS trans + val neg_exchanges = false +) + +structure DvdCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} + val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT + val cancel = @{thm nat_mult_dvd_cancel1} RS trans + val neg_exchanges = false +) + +structure EqCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT + val cancel = @{thm nat_mult_eq_cancel1} RS trans + val neg_exchanges = false +) + +structure LessCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT + val cancel = @{thm nat_mult_less_cancel1} RS trans + val neg_exchanges = true +) + +structure LeCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT + val cancel = @{thm nat_mult_le_cancel1} RS trans + val neg_exchanges = true +) + +val cancel_numeral_factors = + map Arith_Data.prep_simproc + [("nateq_cancel_numeral_factors", + ["(l::nat) * m = n", "(l::nat) = m * n"], + K EqCancelNumeralFactor.proc), + ("natless_cancel_numeral_factors", + ["(l::nat) * m < n", "(l::nat) < m * n"], + K LessCancelNumeralFactor.proc), + ("natle_cancel_numeral_factors", + ["(l::nat) * m <= n", "(l::nat) <= m * n"], + K LeCancelNumeralFactor.proc), + ("natdiv_cancel_numeral_factors", + ["((l::nat) * m) div n", "(l::nat) div (m * n)"], + K DivCancelNumeralFactor.proc), + ("natdvd_cancel_numeral_factors", + ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], + K DvdCancelNumeralFactor.proc)]; + + + +(*** Applying ExtractCommonTermFun ***) + +(*this version ALWAYS includes a trailing one*) +fun long_mk_prod [] = one + | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts); + +(*Find first term that matches u*) +fun find_first_t past u [] = raise TERM("find_first_t", []) + | find_first_t past u (t::terms) = + if u aconv t then (rev past @ terms) + else find_first_t (t::past) u terms + handle TERM _ => find_first_t (t::past) u terms; + +(** Final simplification for the CancelFactor simprocs **) +val simplify_one = Arith_Data.simplify_meta_eq + [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}]; + +fun cancel_simplify_meta_eq ss cancel_th th = + simplify_one ss (([th, cancel_th]) MRS trans); + +structure CancelFactorCommon = + struct + val mk_sum = (fn T:typ => long_mk_prod) + val dest_sum = dest_prod + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first = find_first_t [] + val trans_tac = K Arith_Data.trans_tac + val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} + fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) + val simplify_meta_eq = cancel_simplify_meta_eq + end; + +structure EqCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT + val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj})) +); + +structure LessCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT + val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj})) +); + +structure LeCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT + val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj})) +); + +structure DivideCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.div} + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT + val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj})) +); + +structure DvdCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} + val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT + val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj})) +); + +val cancel_factor = + map Arith_Data.prep_simproc + [("nat_eq_cancel_factor", + ["(l::nat) * m = n", "(l::nat) = m * n"], + K EqCancelFactor.proc), + ("nat_less_cancel_factor", + ["(l::nat) * m < n", "(l::nat) < m * n"], + K LessCancelFactor.proc), + ("nat_le_cancel_factor", + ["(l::nat) * m <= n", "(l::nat) <= m * n"], + K LeCancelFactor.proc), + ("nat_divide_cancel_factor", + ["((l::nat) * m) div n", "(l::nat) div (m * n)"], + K DivideCancelFactor.proc), + ("nat_dvd_cancel_factor", + ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], + K DvdCancelFactor.proc)]; + +end; + + +Addsimprocs Nat_Numeral_Simprocs.cancel_numerals; +Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; +Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors; +Addsimprocs Nat_Numeral_Simprocs.cancel_factor; + + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Simp_tac 1)); + +(*cancel_numerals*) +test "l +( 2) + (2) + 2 + (l + 2) + (oo + 2) = (uu::nat)"; +test "(2*length xs < 2*length xs + j)"; +test "(2*length xs < length xs * 2 + j)"; +test "2*u = (u::nat)"; +test "2*u = Suc (u)"; +test "(i + j + 12 + (k::nat)) - 15 = y"; +test "(i + j + 12 + (k::nat)) - 5 = y"; +test "Suc u - 2 = y"; +test "Suc (Suc (Suc u)) - 2 = y"; +test "(i + j + 2 + (k::nat)) - 1 = y"; +test "(i + j + 1 + (k::nat)) - 2 = y"; + +test "(2*x + (u*v) + y) - v*3*u = (w::nat)"; +test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)"; +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)"; +test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w"; +test "Suc ((u*v)*4) - v*3*u = w"; +test "Suc (Suc ((u*v)*3)) - v*3*u = w"; + +test "(i + j + 12 + (k::nat)) = u + 15 + y"; +test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz"; +test "(i + j + 12 + (k::nat)) = u + 5 + y"; +(*Suc*) +test "(i + j + 12 + k) = Suc (u + y)"; +test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)"; +test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"; +test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v"; +test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"; +test "2*y + 3*z + 2*u = Suc (u)"; +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)"; +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::nat)"; +test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)"; +test "(2*n*m) < (3*(m*n)) + (u::nat)"; + +test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)"; + +test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1"; + +test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))"; + +test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un \ e) ST mxr c))))))) <= length (compT P E A ST mxr e))"; + + +(*negative numerals: FAIL*) +test "(i + j + -23 + (k::nat)) < u + 15 + y"; +test "(i + j + 3 + (k::nat)) < u + -15 + y"; +test "(i + j + -12 + (k::nat)) - 15 = y"; +test "(i + j + 12 + (k::nat)) - -15 = y"; +test "(i + j + -12 + (k::nat)) - -15 = y"; + +(*combine_numerals*) +test "k + 3*k = (u::nat)"; +test "Suc (i + 3) = u"; +test "Suc (i + j + 3 + k) = u"; +test "k + j + 3*k + j = (u::nat)"; +test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)"; +test "(2*n*m) + (3*(m*n)) = (u::nat)"; +(*negative numerals: FAIL*) +test "Suc (i + j + -3 + k) = u"; + +(*cancel_numeral_factors*) +test "9*x = 12 * (y::nat)"; +test "(9*x) div (12 * (y::nat)) = z"; +test "9*x < 12 * (y::nat)"; +test "9*x <= 12 * (y::nat)"; + +(*cancel_factor*) +test "x*k = k*(y::nat)"; +test "k = k*(y::nat)"; +test "a*(b*c) = (b::nat)"; +test "a*(b*c) = d*(b::nat)*(x*a)"; + +test "x*k < k*(y::nat)"; +test "k < k*(y::nat)"; +test "a*(b*c) < (b::nat)"; +test "a*(b*c) < d*(b::nat)*(x*a)"; + +test "x*k <= k*(y::nat)"; +test "k <= k*(y::nat)"; +test "a*(b*c) <= (b::nat)"; +test "a*(b*c) <= d*(b::nat)*(x*a)"; + +test "(x*k) div (k*(y::nat)) = (uu::nat)"; +test "(k) div (k*(y::nat)) = (uu::nat)"; +test "(a*(b*c)) div ((b::nat)) = (uu::nat)"; +test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)"; +*) diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Tools/nat_simprocs.ML --- a/src/HOL/Tools/nat_simprocs.ML Fri May 08 08:07:05 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,574 +0,0 @@ -(* Title: HOL/Tools/nat_simprocs.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - -Simprocs for nat numerals. -*) - -structure Nat_Numeral_Simprocs = -struct - -(*Maps n to #n for n = 0, 1, 2*) -val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym]; -val numeral_sym_ss = HOL_ss addsimps numeral_syms; - -fun rename_numerals th = - simplify numeral_sym_ss (Thm.transfer (the_context ()) th); - -(*Utilities*) - -fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n; -fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); - -fun find_first_numeral past (t::terms) = - ((dest_number t, t, rev past @ terms) - handle TERM _ => find_first_numeral (t::past) terms) - | find_first_numeral past [] = raise TERM("find_first_numeral", []); - -val zero = mk_number 0; -val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; - -(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) -fun mk_sum [] = zero - | mk_sum [t,u] = mk_plus (t, u) - | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); - -(*this version ALWAYS includes a trailing zero*) -fun long_mk_sum [] = HOLogic.zero - | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); - -val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT; - - -(** Other simproc items **) - -val bin_simps = - [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, - @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, - @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less}, - @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, - @{thm less_nat_number_of}, - @{thm Let_number_of}, @{thm nat_number_of}] @ - @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps}; - - -(*** CancelNumerals simprocs ***) - -val one = mk_number 1; -val mk_times = HOLogic.mk_binop @{const_name HOL.times}; - -fun mk_prod [] = one - | mk_prod [t] = t - | mk_prod (t :: ts) = if t = one then mk_prod ts - else mk_times (t, mk_prod ts); - -val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT; - -fun dest_prod t = - let val (t,u) = dest_times t - in dest_prod t @ dest_prod u end - handle TERM _ => [t]; - -(*DON'T do the obvious simplifications; that would create special cases*) -fun mk_coeff (k,t) = mk_times (mk_number k, t); - -(*Express t as a product of (possibly) a numeral with other factors, sorted*) -fun dest_coeff t = - let val ts = sort TermOrd.term_ord (dest_prod t) - val (n, _, ts') = find_first_numeral [] ts - handle TERM _ => (1, one, ts) - in (n, mk_prod ts') end; - -(*Find first coefficient-term THAT MATCHES u*) -fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) - | find_first_coeff past u (t::terms) = - let val (n,u') = dest_coeff t - in if u aconv u' then (n, rev past @ terms) - else find_first_coeff (t::past) u terms - end - handle TERM _ => find_first_coeff (t::past) u terms; - - -(*Split up a sum into the list of its constituent terms, on the way removing any - Sucs and counting them.*) -fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts)) - | dest_Suc_sum (t, (k,ts)) = - let val (t1,t2) = dest_plus t - in dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts))) end - handle TERM _ => (k, t::ts); - -(*Code for testing whether numerals are already used in the goal*) -fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true - | is_numeral _ = false; - -fun prod_has_numeral t = exists is_numeral (dest_prod t); - -(*The Sucs found in the term are converted to a binary numeral. If relaxed is false, - an exception is raised unless the original expression contains at least one - numeral in a coefficient position. This prevents nat_combine_numerals from - introducing numerals to goals.*) -fun dest_Sucs_sum relaxed t = - let val (k,ts) = dest_Suc_sum (t,(0,[])) - in - if relaxed orelse exists prod_has_numeral ts then - if k=0 then ts - else mk_number k :: ts - else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t]) - end; - - -(*Simplify 1*n and n*1 to n*) -val add_0s = map rename_numerals [@{thm add_0}, @{thm add_0_right}]; -val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}]; - -(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*) - -(*And these help the simproc return False when appropriate, which helps - the arith prover.*) -val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc}, - @{thm Suc_not_Zero}, @{thm le_0_eq}]; - -val simplify_meta_eq = - Arith_Data.simplify_meta_eq - ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right}, - @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules); - - -(*** Applying CancelNumeralsFun ***) - -structure CancelNumeralsCommon = - struct - val mk_sum = (fn T:typ => mk_sum) - val dest_sum = dest_Sucs_sum true - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first_coeff = find_first_coeff [] - val trans_tac = K Arith_Data.trans_tac - - val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ - [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} - val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) - - val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; - fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)); - val simplify_meta_eq = simplify_meta_eq - end; - - -structure EqCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT - val bal_add1 = @{thm nat_eq_add_iff1} RS trans - val bal_add2 = @{thm nat_eq_add_iff2} RS trans -); - -structure LessCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT - val bal_add1 = @{thm nat_less_add_iff1} RS trans - val bal_add2 = @{thm nat_less_add_iff2} RS trans -); - -structure LeCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT - val bal_add1 = @{thm nat_le_add_iff1} RS trans - val bal_add2 = @{thm nat_le_add_iff2} RS trans -); - -structure DiffCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name HOL.minus} - val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT - val bal_add1 = @{thm nat_diff_add_eq1} RS trans - val bal_add2 = @{thm nat_diff_add_eq2} RS trans -); - - -val cancel_numerals = - map Arith_Data.prep_simproc - [("nateq_cancel_numerals", - ["(l::nat) + m = n", "(l::nat) = m + n", - "(l::nat) * m = n", "(l::nat) = m * n", - "Suc m = n", "m = Suc n"], - K EqCancelNumerals.proc), - ("natless_cancel_numerals", - ["(l::nat) + m < n", "(l::nat) < m + n", - "(l::nat) * m < n", "(l::nat) < m * n", - "Suc m < n", "m < Suc n"], - K LessCancelNumerals.proc), - ("natle_cancel_numerals", - ["(l::nat) + m <= n", "(l::nat) <= m + n", - "(l::nat) * m <= n", "(l::nat) <= m * n", - "Suc m <= n", "m <= Suc n"], - K LeCancelNumerals.proc), - ("natdiff_cancel_numerals", - ["((l::nat) + m) - n", "(l::nat) - (m + n)", - "(l::nat) * m - n", "(l::nat) - m * n", - "Suc m - n", "m - Suc n"], - K DiffCancelNumerals.proc)]; - - -(*** Applying CombineNumeralsFun ***) - -structure CombineNumeralsData = - struct - type coeff = int - val iszero = (fn x => x = 0) - val add = op + - val mk_sum = (fn T:typ => long_mk_sum) (*to work for 2*x + 3*x *) - val dest_sum = dest_Sucs_sum false - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val left_distrib = @{thm left_add_mult_distrib} RS trans - val prove_conv = Arith_Data.prove_conv_nohyps - val trans_tac = K Arith_Data.trans_tac - - val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac} - val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) - - val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; - fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = simplify_meta_eq - end; - -structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); - -val combine_numerals = - Arith_Data.prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc); - - -(*** Applying CancelNumeralFactorFun ***) - -structure CancelNumeralFactorCommon = - struct - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val trans_tac = K Arith_Data.trans_tac - - val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps - numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} - val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) - - val numeral_simp_ss = HOL_ss addsimps bin_simps - fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = simplify_meta_eq - end - -structure DivCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name Divides.div} - val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT - val cancel = @{thm nat_mult_div_cancel1} RS trans - val neg_exchanges = false -) - -structure DvdCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} - val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT - val cancel = @{thm nat_mult_dvd_cancel1} RS trans - val neg_exchanges = false -) - -structure EqCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT - val cancel = @{thm nat_mult_eq_cancel1} RS trans - val neg_exchanges = false -) - -structure LessCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT - val cancel = @{thm nat_mult_less_cancel1} RS trans - val neg_exchanges = true -) - -structure LeCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT - val cancel = @{thm nat_mult_le_cancel1} RS trans - val neg_exchanges = true -) - -val cancel_numeral_factors = - map Arith_Data.prep_simproc - [("nateq_cancel_numeral_factors", - ["(l::nat) * m = n", "(l::nat) = m * n"], - K EqCancelNumeralFactor.proc), - ("natless_cancel_numeral_factors", - ["(l::nat) * m < n", "(l::nat) < m * n"], - K LessCancelNumeralFactor.proc), - ("natle_cancel_numeral_factors", - ["(l::nat) * m <= n", "(l::nat) <= m * n"], - K LeCancelNumeralFactor.proc), - ("natdiv_cancel_numeral_factors", - ["((l::nat) * m) div n", "(l::nat) div (m * n)"], - K DivCancelNumeralFactor.proc), - ("natdvd_cancel_numeral_factors", - ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], - K DvdCancelNumeralFactor.proc)]; - - - -(*** Applying ExtractCommonTermFun ***) - -(*this version ALWAYS includes a trailing one*) -fun long_mk_prod [] = one - | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts); - -(*Find first term that matches u*) -fun find_first_t past u [] = raise TERM("find_first_t", []) - | find_first_t past u (t::terms) = - if u aconv t then (rev past @ terms) - else find_first_t (t::past) u terms - handle TERM _ => find_first_t (t::past) u terms; - -(** Final simplification for the CancelFactor simprocs **) -val simplify_one = Arith_Data.simplify_meta_eq - [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}]; - -fun cancel_simplify_meta_eq ss cancel_th th = - simplify_one ss (([th, cancel_th]) MRS trans); - -structure CancelFactorCommon = - struct - val mk_sum = (fn T:typ => long_mk_prod) - val dest_sum = dest_prod - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first = find_first_t [] - val trans_tac = K Arith_Data.trans_tac - val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} - fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) - val simplify_meta_eq = cancel_simplify_meta_eq - end; - -structure EqCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT - val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj})) -); - -structure LessCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT - val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj})) -); - -structure LeCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT - val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj})) -); - -structure DivideCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name Divides.div} - val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT - val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj})) -); - -structure DvdCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} - val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT - val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj})) -); - -val cancel_factor = - map Arith_Data.prep_simproc - [("nat_eq_cancel_factor", - ["(l::nat) * m = n", "(l::nat) = m * n"], - K EqCancelFactor.proc), - ("nat_less_cancel_factor", - ["(l::nat) * m < n", "(l::nat) < m * n"], - K LessCancelFactor.proc), - ("nat_le_cancel_factor", - ["(l::nat) * m <= n", "(l::nat) <= m * n"], - K LeCancelFactor.proc), - ("nat_divide_cancel_factor", - ["((l::nat) * m) div n", "(l::nat) div (m * n)"], - K DivideCancelFactor.proc), - ("nat_dvd_cancel_factor", - ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], - K DvdCancelFactor.proc)]; - -end; - - -Addsimprocs Nat_Numeral_Simprocs.cancel_numerals; -Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; -Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors; -Addsimprocs Nat_Numeral_Simprocs.cancel_factor; - - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Simp_tac 1)); - -(*cancel_numerals*) -test "l +( 2) + (2) + 2 + (l + 2) + (oo + 2) = (uu::nat)"; -test "(2*length xs < 2*length xs + j)"; -test "(2*length xs < length xs * 2 + j)"; -test "2*u = (u::nat)"; -test "2*u = Suc (u)"; -test "(i + j + 12 + (k::nat)) - 15 = y"; -test "(i + j + 12 + (k::nat)) - 5 = y"; -test "Suc u - 2 = y"; -test "Suc (Suc (Suc u)) - 2 = y"; -test "(i + j + 2 + (k::nat)) - 1 = y"; -test "(i + j + 1 + (k::nat)) - 2 = y"; - -test "(2*x + (u*v) + y) - v*3*u = (w::nat)"; -test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)"; -test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)"; -test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w"; -test "Suc ((u*v)*4) - v*3*u = w"; -test "Suc (Suc ((u*v)*3)) - v*3*u = w"; - -test "(i + j + 12 + (k::nat)) = u + 15 + y"; -test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz"; -test "(i + j + 12 + (k::nat)) = u + 5 + y"; -(*Suc*) -test "(i + j + 12 + k) = Suc (u + y)"; -test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)"; -test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"; -test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v"; -test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"; -test "2*y + 3*z + 2*u = Suc (u)"; -test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)"; -test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::nat)"; -test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)"; -test "(2*n*m) < (3*(m*n)) + (u::nat)"; - -test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)"; - -test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1"; - -test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))"; - -test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un \ e) ST mxr c))))))) <= length (compT P E A ST mxr e))"; - - -(*negative numerals: FAIL*) -test "(i + j + -23 + (k::nat)) < u + 15 + y"; -test "(i + j + 3 + (k::nat)) < u + -15 + y"; -test "(i + j + -12 + (k::nat)) - 15 = y"; -test "(i + j + 12 + (k::nat)) - -15 = y"; -test "(i + j + -12 + (k::nat)) - -15 = y"; - -(*combine_numerals*) -test "k + 3*k = (u::nat)"; -test "Suc (i + 3) = u"; -test "Suc (i + j + 3 + k) = u"; -test "k + j + 3*k + j = (u::nat)"; -test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)"; -test "(2*n*m) + (3*(m*n)) = (u::nat)"; -(*negative numerals: FAIL*) -test "Suc (i + j + -3 + k) = u"; - -(*cancel_numeral_factors*) -test "9*x = 12 * (y::nat)"; -test "(9*x) div (12 * (y::nat)) = z"; -test "9*x < 12 * (y::nat)"; -test "9*x <= 12 * (y::nat)"; - -(*cancel_factor*) -test "x*k = k*(y::nat)"; -test "k = k*(y::nat)"; -test "a*(b*c) = (b::nat)"; -test "a*(b*c) = d*(b::nat)*(x*a)"; - -test "x*k < k*(y::nat)"; -test "k < k*(y::nat)"; -test "a*(b*c) < (b::nat)"; -test "a*(b*c) < d*(b::nat)*(x*a)"; - -test "x*k <= k*(y::nat)"; -test "k <= k*(y::nat)"; -test "a*(b*c) <= (b::nat)"; -test "a*(b*c) <= d*(b::nat)*(x*a)"; - -test "(x*k) div (k*(y::nat)) = (uu::nat)"; -test "(k) div (k*(y::nat)) = (uu::nat)"; -test "(a*(b*c)) div ((b::nat)) = (uu::nat)"; -test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)"; -*) - - -(*** Prepare linear arithmetic for nat numerals ***) - -local - -(* reduce contradictory <= to False *) -val add_rules = @{thms ring_distribs} @ - [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1}, - @{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}, @{thm le_number_of_eq_not_less}, - @{thm le_Suc_number_of}, @{thm le_number_of_Suc}, - @{thm less_Suc_number_of}, @{thm less_number_of_Suc}, - @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc}, - @{thm mult_Suc}, @{thm mult_Suc_right}, - @{thm add_Suc}, @{thm add_Suc_right}, - @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of}, - @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}]; - -(* Products are multiplied out during proof (re)construction via -ring_distribs. Ideally they should remain atomic. But that is -currently not possible because 1 is replaced by Suc 0, and then some -simprocs start to mess around with products like (n+1)*m. The rule -1 == Suc 0 is necessary for early parts of HOL where numerals and -simprocs are not yet available. But then it is difficult to remove -that rule later on, because it may find its way back in when theories -(and thus lin-arith simpsets) are merged. Otherwise one could turn the -rule around (Suc n = n+1) and see if that helps products being left -alone. *) - -val simprocs = Nat_Numeral_Simprocs.combine_numerals - :: Nat_Numeral_Simprocs.cancel_numerals; - -in - -val nat_simprocs_setup = - Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => - {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, - inj_thms = inj_thms, lessD = lessD, neqE = neqE, - simpset = simpset addsimps add_rules - addsimprocs simprocs}); - -end; diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Tools/numeral_simprocs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/numeral_simprocs.ML Fri May 08 19:20:00 2009 +0200 @@ -0,0 +1,786 @@ +(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2000 University of Cambridge + +Simprocs for the integer numerals. +*) + +(*To quote from Provers/Arith/cancel_numeral_factor.ML: + +Cancels common coefficients in balanced expressions: + + u*#m ~~ u'*#m' == #n*u ~~ #n'*u' + +where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) +and d = gcd(m,m') and n=m/d and n'=m'/d. +*) + +signature NUMERAL_SIMPROCS = +sig + val mk_sum: typ -> term list -> term + val dest_sum: term -> term list + + val assoc_fold_simproc: simproc + val combine_numerals: simproc + val cancel_numerals: simproc list + val cancel_factors: simproc list + val cancel_numeral_factors: simproc list + val field_combine_numerals: simproc + val field_cancel_numeral_factors: simproc list + val num_ss: simpset +end; + +structure Numeral_Simprocs : NUMERAL_SIMPROCS = +struct + +fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; + +fun find_first_numeral past (t::terms) = + ((snd (HOLogic.dest_number t), rev past @ terms) + handle TERM _ => find_first_numeral (t::past) terms) + | find_first_numeral past [] = raise TERM("find_first_numeral", []); + +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; + +fun mk_minus t = + let val T = Term.fastype_of t + in Const (@{const_name HOL.uminus}, T --> T) $ t end; + +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) +fun mk_sum T [] = mk_number T 0 + | mk_sum T [t,u] = mk_plus (t, u) + | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); + +(*this version ALWAYS includes a trailing zero*) +fun long_mk_sum T [] = mk_number T 0 + | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); + +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT; + +(*decompose additions AND subtractions as a sum*) +fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) = + dest_summing (pos, t, dest_summing (pos, u, ts)) + | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) = + dest_summing (pos, t, dest_summing (not pos, u, ts)) + | dest_summing (pos, t, ts) = + if pos then t::ts else mk_minus t :: ts; + +fun dest_sum t = dest_summing (true, t, []); + +val mk_diff = HOLogic.mk_binop @{const_name HOL.minus}; +val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT; + +val mk_times = HOLogic.mk_binop @{const_name HOL.times}; + +fun one_of T = Const(@{const_name HOL.one},T); + +(* build product with trailing 1 rather than Numeral 1 in order to avoid the + unnecessary restriction to type class number_ring + which is not required for cancellation of common factors in divisions. +*) +fun mk_prod T = + let val one = one_of T + fun mk [] = one + | mk [t] = t + | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts) + in mk end; + +(*This version ALWAYS includes a trailing one*) +fun long_mk_prod T [] = one_of T + | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); + +val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT; + +fun dest_prod t = + let val (t,u) = dest_times t + in dest_prod t @ dest_prod u end + handle TERM _ => [t]; + +(*DON'T do the obvious simplifications; that would create special cases*) +fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); + +(*Express t as a product of (possibly) a numeral with other sorted terms*) +fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t + | dest_coeff sign t = + let val ts = sort TermOrd.term_ord (dest_prod t) + val (n, ts') = find_first_numeral [] ts + handle TERM _ => (1, ts) + in (sign*n, mk_prod (Term.fastype_of t) ts') end; + +(*Find first coefficient-term THAT MATCHES u*) +fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) + | find_first_coeff past u (t::terms) = + let val (n,u') = dest_coeff 1 t + in if u aconv u' then (n, rev past @ terms) + else find_first_coeff (t::past) u terms + end + handle TERM _ => find_first_coeff (t::past) u terms; + +(*Fractions as pairs of ints. Can't use Rat.rat because the representation + needs to preserve negative values in the denominator.*) +fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); + +(*Don't reduce fractions; sums must be proved by rule add_frac_eq. + Fractions are reduced later by the cancel_numeral_factor simproc.*) +fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); + +val mk_divide = HOLogic.mk_binop @{const_name HOL.divide}; + +(*Build term (p / q) * t*) +fun mk_fcoeff ((p, q), t) = + let val T = Term.fastype_of t + in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; + +(*Express t as a product of a fraction with other sorted terms*) +fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t + | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) = + let val (p, t') = dest_coeff sign t + val (q, u') = dest_coeff 1 u + in (mk_frac (p, q), mk_divide (t', u')) end + | dest_fcoeff sign t = + let val (p, t') = dest_coeff sign t + val T = Term.fastype_of t + in (mk_frac (p, 1), mk_divide (t', one_of T)) end; + + +(** New term ordering so that AC-rewriting brings numerals to the front **) + +(*Order integers by absolute value and then by sign. The standard integer + ordering is not well-founded.*) +fun num_ord (i,j) = + (case int_ord (abs i, abs j) of + EQUAL => int_ord (Int.sign i, Int.sign j) + | ord => ord); + +(*This resembles TermOrd.term_ord, but it puts binary numerals before other + non-atomic terms.*) +local open Term +in +fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) = + (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord) + | numterm_ord + (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) = + num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w) + | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS + | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER + | numterm_ord (t, u) = + (case int_ord (size_of_term t, size_of_term u) of + EQUAL => + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in + (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord) + end + | ord => ord) +and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) +end; + +fun numtermless tu = (numterm_ord tu = LESS); + +val num_ss = HOL_ss settermless numtermless; + +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*) +val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym]; + +(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) +val add_0s = @{thms add_0s}; +val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1}; + +(*Simplify inverse Numeral1, a/Numeral1*) +val inverse_1s = [@{thm inverse_numeral_1}]; +val divide_1s = [@{thm divide_numeral_1}]; + +(*To perform binary arithmetic. The "left" rewriting handles patterns + created by the Numeral_Simprocs, such as 3 * (5 * x). *) +val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym, + @{thm add_number_of_left}, @{thm mult_number_of_left}] @ + @{thms arith_simps} @ @{thms rel_simps}; + +(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms + during re-arrangement*) +val non_add_simps = + subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps; + +(*To evaluate binary negations of coefficients*) +val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @ + @{thms minus_bin_simps} @ @{thms pred_bin_simps}; + +(*To let us treat subtraction as addition*) +val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}]; + +(*To let us treat division as multiplication*) +val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; + +(*push the unary minus down: - x * y = x * - y *) +val minus_mult_eq_1_to_2 = + [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard; + +(*to extract again any uncancelled minuses*) +val minus_from_mult_simps = + [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}]; + +(*combine unary minus with numeric literals, however nested within a product*) +val mult_minus_simps = + [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2]; + +val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ + diff_simps @ minus_simps @ @{thms add_ac} +val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps +val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} + +structure CancelNumeralsCommon = + struct + val mk_sum = mk_sum + val dest_sum = dest_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val find_first_coeff = find_first_coeff [] + val trans_tac = K Arith_Data.trans_tac + + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) + end; + + +structure EqCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" Term.dummyT + val bal_add1 = @{thm eq_add_iff1} RS trans + val bal_add2 = @{thm eq_add_iff2} RS trans +); + +structure LessCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT + val bal_add1 = @{thm less_add_iff1} RS trans + val bal_add2 = @{thm less_add_iff2} RS trans +); + +structure LeCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT + val bal_add1 = @{thm le_add_iff1} RS trans + val bal_add2 = @{thm le_add_iff2} RS trans +); + +val cancel_numerals = + map Arith_Data.prep_simproc + [("inteq_cancel_numerals", + ["(l::'a::number_ring) + m = n", + "(l::'a::number_ring) = m + n", + "(l::'a::number_ring) - m = n", + "(l::'a::number_ring) = m - n", + "(l::'a::number_ring) * m = n", + "(l::'a::number_ring) = m * n"], + K EqCancelNumerals.proc), + ("intless_cancel_numerals", + ["(l::'a::{ordered_idom,number_ring}) + m < n", + "(l::'a::{ordered_idom,number_ring}) < m + n", + "(l::'a::{ordered_idom,number_ring}) - m < n", + "(l::'a::{ordered_idom,number_ring}) < m - n", + "(l::'a::{ordered_idom,number_ring}) * m < n", + "(l::'a::{ordered_idom,number_ring}) < m * n"], + K LessCancelNumerals.proc), + ("intle_cancel_numerals", + ["(l::'a::{ordered_idom,number_ring}) + m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m + n", + "(l::'a::{ordered_idom,number_ring}) - m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m - n", + "(l::'a::{ordered_idom,number_ring}) * m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m * n"], + K LeCancelNumerals.proc)]; + +structure CombineNumeralsData = + struct + type coeff = int + val iszero = (fn x => x = 0) + val add = op + + val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) + val dest_sum = dest_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val left_distrib = @{thm combine_common_factor} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps + val trans_tac = K Arith_Data.trans_tac + + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) + end; + +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); + +(*Version for fields, where coefficients can be fractions*) +structure FieldCombineNumeralsData = + struct + type coeff = int * int + val iszero = (fn (p, q) => p = 0) + val add = add_frac + val mk_sum = long_mk_sum + val dest_sum = dest_sum + val mk_coeff = mk_fcoeff + val dest_coeff = dest_fcoeff 1 + val left_distrib = @{thm combine_common_factor} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps + val trans_tac = K Arith_Data.trans_tac + + val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}] + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s) + end; + +structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); + +val combine_numerals = + Arith_Data.prep_simproc + ("int_combine_numerals", + ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], + K CombineNumerals.proc); + +val field_combine_numerals = + Arith_Data.prep_simproc + ("field_combine_numerals", + ["(i::'a::{number_ring,field,division_by_zero}) + j", + "(i::'a::{number_ring,field,division_by_zero}) - j"], + K FieldCombineNumerals.proc); + +(** Constant folding for multiplication in semirings **) + +(*We do not need folding for addition: combine_numerals does the same thing*) + +structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = +struct + val assoc_ss = HOL_ss addsimps @{thms mult_ac} + val eq_reflection = eq_reflection + fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true + | is_numeral _ = false; +end; + +structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); + +val assoc_fold_simproc = + Arith_Data.prep_simproc + ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"], + K Semiring_Times_Assoc.proc); + +structure CancelNumeralFactorCommon = + struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val trans_tac = K Arith_Data.trans_tac + + val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s + val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps + val norm_ss3 = HOL_ss addsimps @{thms mult_ac} + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = HOL_ss addsimps + [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}] @ simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = Arith_Data.simplify_meta_eq + [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left}, + @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}]; + end + +(*Version for semiring_div*) +structure DivCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.div} + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT + val cancel = @{thm div_mult_mult1} RS trans + val neg_exchanges = false +) + +(*Version for fields*) +structure DivideCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} + val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT + val cancel = @{thm mult_divide_mult_cancel_left} RS trans + val neg_exchanges = false +) + +structure EqCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" Term.dummyT + val cancel = @{thm mult_cancel_left} RS trans + val neg_exchanges = false +) + +structure LessCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT + val cancel = @{thm mult_less_cancel_left} RS trans + val neg_exchanges = true +) + +structure LeCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT + val cancel = @{thm mult_le_cancel_left} RS trans + val neg_exchanges = true +) + +val cancel_numeral_factors = + map Arith_Data.prep_simproc + [("ring_eq_cancel_numeral_factor", + ["(l::'a::{idom,number_ring}) * m = n", + "(l::'a::{idom,number_ring}) = m * n"], + K EqCancelNumeralFactor.proc), + ("ring_less_cancel_numeral_factor", + ["(l::'a::{ordered_idom,number_ring}) * m < n", + "(l::'a::{ordered_idom,number_ring}) < m * n"], + K LessCancelNumeralFactor.proc), + ("ring_le_cancel_numeral_factor", + ["(l::'a::{ordered_idom,number_ring}) * m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m * n"], + K LeCancelNumeralFactor.proc), + ("int_div_cancel_numeral_factors", + ["((l::'a::{semiring_div,number_ring}) * m) div n", + "(l::'a::{semiring_div,number_ring}) div (m * n)"], + K DivCancelNumeralFactor.proc), + ("divide_cancel_numeral_factor", + ["((l::'a::{division_by_zero,field,number_ring}) * m) / n", + "(l::'a::{division_by_zero,field,number_ring}) / (m * n)", + "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"], + K DivideCancelNumeralFactor.proc)]; + +val field_cancel_numeral_factors = + map Arith_Data.prep_simproc + [("field_eq_cancel_numeral_factor", + ["(l::'a::{field,number_ring}) * m = n", + "(l::'a::{field,number_ring}) = m * n"], + K EqCancelNumeralFactor.proc), + ("field_cancel_numeral_factor", + ["((l::'a::{division_by_zero,field,number_ring}) * m) / n", + "(l::'a::{division_by_zero,field,number_ring}) / (m * n)", + "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"], + K DivideCancelNumeralFactor.proc)] + + +(** Declarations for ExtractCommonTerm **) + +(*Find first term that matches u*) +fun find_first_t past u [] = raise TERM ("find_first_t", []) + | find_first_t past u (t::terms) = + if u aconv t then (rev past @ terms) + else find_first_t (t::past) u terms + handle TERM _ => find_first_t (t::past) u terms; + +(** Final simplification for the CancelFactor simprocs **) +val simplify_one = Arith_Data.simplify_meta_eq + [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}]; + +fun cancel_simplify_meta_eq ss cancel_th th = + simplify_one ss (([th, cancel_th]) MRS trans); + +local + val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop) + fun Eq_True_elim Eq = + Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI} +in +fun sign_conv pos_th neg_th ss t = + let val T = fastype_of t; + val zero = Const(@{const_name HOL.zero}, T); + val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT); + val pos = less $ zero $ t and neg = less $ t $ zero + fun prove p = + Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p) + handle THM _ => NONE + in case prove pos of + SOME th => SOME(th RS pos_th) + | NONE => (case prove neg of + SOME th => SOME(th RS neg_th) + | NONE => NONE) + end; +end + +structure CancelFactorCommon = + struct + val mk_sum = long_mk_prod + val dest_sum = dest_prod + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first = find_first_t [] + val trans_tac = K Arith_Data.trans_tac + val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} + fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) + val simplify_meta_eq = cancel_simplify_meta_eq + end; + +(*mult_cancel_left requires a ring with no zero divisors.*) +structure EqCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" Term.dummyT + val simp_conv = K (K (SOME @{thm mult_cancel_left})) +); + +(*for ordered rings*) +structure LeCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT + val simp_conv = sign_conv + @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg} +); + +(*for ordered rings*) +structure LessCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT + val simp_conv = sign_conv + @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg} +); + +(*for semirings with division*) +structure DivCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.div} + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT + val simp_conv = K (K (SOME @{thm div_mult_mult1_if})) +); + +structure ModCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} + val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT + val simp_conv = K (K (SOME @{thm mod_mult_mult1})) +); + +(*for idoms*) +structure DvdCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} + val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT + val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left})) +); + +(*Version for all fields, including unordered ones (type complex).*) +structure DivideCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} + val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT + val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if})) +); + +val cancel_factors = + map Arith_Data.prep_simproc + [("ring_eq_cancel_factor", + ["(l::'a::idom) * m = n", + "(l::'a::idom) = m * n"], + K EqCancelFactor.proc), + ("ordered_ring_le_cancel_factor", + ["(l::'a::ordered_ring) * m <= n", + "(l::'a::ordered_ring) <= m * n"], + K LeCancelFactor.proc), + ("ordered_ring_less_cancel_factor", + ["(l::'a::ordered_ring) * m < n", + "(l::'a::ordered_ring) < m * n"], + K LessCancelFactor.proc), + ("int_div_cancel_factor", + ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"], + K DivCancelFactor.proc), + ("int_mod_cancel_factor", + ["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"], + K ModCancelFactor.proc), + ("dvd_cancel_factor", + ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"], + K DvdCancelFactor.proc), + ("divide_cancel_factor", + ["((l::'a::{division_by_zero,field}) * m) / n", + "(l::'a::{division_by_zero,field}) / (m * n)"], + K DivideCancelFactor.proc)]; + +end; + +Addsimprocs Numeral_Simprocs.cancel_numerals; +Addsimprocs [Numeral_Simprocs.combine_numerals]; +Addsimprocs [Numeral_Simprocs.field_combine_numerals]; +Addsimprocs [Numeral_Simprocs.assoc_fold_simproc]; + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s, by (Simp_tac 1)); + +test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"; + +test "2*u = (u::int)"; +test "(i + j + 12 + (k::int)) - 15 = y"; +test "(i + j + 12 + (k::int)) - 5 = y"; + +test "y - b < (b::int)"; +test "y - (3*b + c) < (b::int) - 2*c"; + +test "(2*x - (u*v) + y) - v*3*u = (w::int)"; +test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"; +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"; +test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"; + +test "(i + j + 12 + (k::int)) = u + 15 + y"; +test "(i + j*2 + 12 + (k::int)) = j + 5 + y"; + +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"; + +test "a + -(b+c) + b = (d::int)"; +test "a + -(b+c) - b = (d::int)"; + +(*negative numerals*) +test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"; +test "(i + j + -3 + (k::int)) < u + 5 + y"; +test "(i + j + 3 + (k::int)) < u + -6 + y"; +test "(i + j + -12 + (k::int)) - 15 = y"; +test "(i + j + 12 + (k::int)) - -15 = y"; +test "(i + j + -12 + (k::int)) - -15 = y"; +*) + +Addsimprocs Numeral_Simprocs.cancel_numeral_factors; + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Simp_tac 1)); + +test "9*x = 12 * (y::int)"; +test "(9*x) div (12 * (y::int)) = z"; +test "9*x < 12 * (y::int)"; +test "9*x <= 12 * (y::int)"; + +test "-99*x = 132 * (y::int)"; +test "(-99*x) div (132 * (y::int)) = z"; +test "-99*x < 132 * (y::int)"; +test "-99*x <= 132 * (y::int)"; + +test "999*x = -396 * (y::int)"; +test "(999*x) div (-396 * (y::int)) = z"; +test "999*x < -396 * (y::int)"; +test "999*x <= -396 * (y::int)"; + +test "-99*x = -81 * (y::int)"; +test "(-99*x) div (-81 * (y::int)) = z"; +test "-99*x <= -81 * (y::int)"; +test "-99*x < -81 * (y::int)"; + +test "-2 * x = -1 * (y::int)"; +test "-2 * x = -(y::int)"; +test "(-2 * x) div (-1 * (y::int)) = z"; +test "-2 * x < -(y::int)"; +test "-2 * x <= -1 * (y::int)"; +test "-x < -23 * (y::int)"; +test "-x <= -23 * (y::int)"; +*) + +(*And the same examples for fields such as rat or real: +test "0 <= (y::rat) * -2"; +test "9*x = 12 * (y::rat)"; +test "(9*x) / (12 * (y::rat)) = z"; +test "9*x < 12 * (y::rat)"; +test "9*x <= 12 * (y::rat)"; + +test "-99*x = 132 * (y::rat)"; +test "(-99*x) / (132 * (y::rat)) = z"; +test "-99*x < 132 * (y::rat)"; +test "-99*x <= 132 * (y::rat)"; + +test "999*x = -396 * (y::rat)"; +test "(999*x) / (-396 * (y::rat)) = z"; +test "999*x < -396 * (y::rat)"; +test "999*x <= -396 * (y::rat)"; + +test "(- ((2::rat) * x) <= 2 * y)"; +test "-99*x = -81 * (y::rat)"; +test "(-99*x) / (-81 * (y::rat)) = z"; +test "-99*x <= -81 * (y::rat)"; +test "-99*x < -81 * (y::rat)"; + +test "-2 * x = -1 * (y::rat)"; +test "-2 * x = -(y::rat)"; +test "(-2 * x) / (-1 * (y::rat)) = z"; +test "-2 * x < -(y::rat)"; +test "-2 * x <= -1 * (y::rat)"; +test "-x < -23 * (y::rat)"; +test "-x <= -23 * (y::rat)"; +*) + +Addsimprocs Numeral_Simprocs.cancel_factors; + + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Asm_simp_tac 1)); + +test "x*k = k*(y::int)"; +test "k = k*(y::int)"; +test "a*(b*c) = (b::int)"; +test "a*(b*c) = d*(b::int)*(x*a)"; + +test "(x*k) div (k*(y::int)) = (uu::int)"; +test "(k) div (k*(y::int)) = (uu::int)"; +test "(a*(b*c)) div ((b::int)) = (uu::int)"; +test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"; +*) + +(*And the same examples for fields such as rat or real: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Asm_simp_tac 1)); + +test "x*k = k*(y::rat)"; +test "k = k*(y::rat)"; +test "a*(b*c) = (b::rat)"; +test "a*(b*c) = d*(b::rat)*(x*a)"; + + +test "(x*k) / (k*(y::rat)) = (uu::rat)"; +test "(k) / (k*(y::rat)) = (uu::rat)"; +test "(a*(b*c)) / ((b::rat)) = (uu::rat)"; +test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"; + +(*FIXME: what do we do about this?*) +test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"; +*) diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Tools/rat_arith.ML --- a/src/HOL/Tools/rat_arith.ML Fri May 08 08:07:05 2009 +0200 +++ b/src/HOL/Tools/rat_arith.ML Fri May 08 19:20:00 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Real/rat_arith.ML - ID: $Id$ Author: Lawrence C Paulson Copyright 2004 University of Cambridge @@ -10,8 +9,6 @@ local -val simprocs = field_cancel_numeral_factors - val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals}, read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib}, @@ -42,7 +39,7 @@ lessD = lessD, (*Can't change lessD: the rats are dense!*) neqE = neqE, simpset = simpset addsimps simps - addsimprocs simprocs}) #> + addsimprocs Numeral_Simprocs.field_cancel_numeral_factors}) #> arith_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #> arith_inj_const (@{const_name of_int}, @{typ "int => rat"}) diff -r 9950ca962e20 -r 35b437f7ad51 src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Fri May 08 08:07:05 2009 +0200 +++ b/src/HOL/Word/WordArith.thy Fri May 08 19:20:00 2009 +0200 @@ -701,7 +701,8 @@ apply (erule (2) udvd_decr0) done -ML{*Delsimprocs cancel_factors*} +ML {* Delsimprocs Numeral_Simprocs.cancel_factors *} + lemma udvd_incr2_K: "p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==> 0 < K ==> p <= p + K & p + K <= a + s" @@ -717,7 +718,8 @@ apply arith apply simp done -ML{*Delsimprocs cancel_factors*} + +ML {* Addsimprocs Numeral_Simprocs.cancel_factors *} (* links with rbl operations *) lemma word_succ_rbl: diff -r 9950ca962e20 -r 35b437f7ad51 src/HOLCF/Pcpo.thy --- a/src/HOLCF/Pcpo.thy Fri May 08 08:07:05 2009 +0200 +++ b/src/HOLCF/Pcpo.thy Fri May 08 19:20:00 2009 +0200 @@ -13,28 +13,28 @@ text {* The class cpo of chain complete partial orders *} class cpo = po + - -- {* class axiom: *} - assumes cpo: "chain S \ \x :: 'a::po. range S <<| x" + assumes cpo: "chain S \ \x. range S <<| x" +begin text {* in cpo's everthing equal to THE lub has lub properties for every chain *} -lemma cpo_lubI: "chain (S::nat \ 'a::cpo) \ range S <<| (\i. S i)" -by (fast dest: cpo elim: lubI) +lemma cpo_lubI: "chain S \ range S <<| (\i. S i)" + by (fast dest: cpo elim: lubI) -lemma thelubE: "\chain S; (\i. S i) = (l::'a::cpo)\ \ range S <<| l" -by (blast dest: cpo intro: lubI) +lemma thelubE: "\chain S; (\i. S i) = l\ \ range S <<| l" + by (blast dest: cpo intro: lubI) text {* Properties of the lub *} -lemma is_ub_thelub: "chain (S::nat \ 'a::cpo) \ S x \ (\i. S i)" -by (blast dest: cpo intro: lubI [THEN is_ub_lub]) +lemma is_ub_thelub: "chain S \ S x \ (\i. S i)" + by (blast dest: cpo intro: lubI [THEN is_ub_lub]) lemma is_lub_thelub: - "\chain (S::nat \ 'a::cpo); range S <| x\ \ (\i. S i) \ x" -by (blast dest: cpo intro: lubI [THEN is_lub_lub]) + "\chain S; range S <| x\ \ (\i. S i) \ x" + by (blast dest: cpo intro: lubI [THEN is_lub_lub]) lemma lub_range_mono: - "\range X \ range Y; chain Y; chain (X::nat \ 'a::cpo)\ + "\range X \ range Y; chain Y; chain X\ \ (\i. X i) \ (\i. Y i)" apply (erule is_lub_thelub) apply (rule ub_rangeI) @@ -45,7 +45,7 @@ done lemma lub_range_shift: - "chain (Y::nat \ 'a::cpo) \ (\i. Y (i + j)) = (\i. Y i)" + "chain Y \ (\i. Y (i + j)) = (\i. Y i)" apply (rule antisym_less) apply (rule lub_range_mono) apply fast @@ -62,7 +62,7 @@ done lemma maxinch_is_thelub: - "chain Y \ max_in_chain i Y = ((\i. Y i) = ((Y i)::'a::cpo))" + "chain Y \ max_in_chain i Y = ((\i. Y i) = Y i)" apply (rule iffI) apply (fast intro!: thelubI lub_finch1) apply (unfold max_in_chain_def) @@ -75,7 +75,7 @@ text {* the @{text "\"} relation between two chains is preserved by their lubs *} lemma lub_mono: - "\chain (X::nat \ 'a::cpo); chain Y; \i. X i \ Y i\ + "\chain X; chain Y; \i. X i \ Y i\ \ (\i. X i) \ (\i. Y i)" apply (erule is_lub_thelub) apply (rule ub_rangeI) @@ -87,14 +87,14 @@ text {* the = relation between two chains is preserved by their lubs *} lemma lub_equal: - "\chain (X::nat \ 'a::cpo); chain Y; \k. X k = Y k\ + "\chain X; chain Y; \k. X k = Y k\ \ (\i. X i) = (\i. Y i)" -by (simp only: expand_fun_eq [symmetric]) + by (simp only: expand_fun_eq [symmetric]) text {* more results about mono and = of lubs of chains *} lemma lub_mono2: - "\\j. \i>j. X i = Y i; chain (X::nat \ 'a::cpo); chain Y\ + "\\j. \i>j. X i = Y i; chain X; chain Y\ \ (\i. X i) \ (\i. Y i)" apply (erule exE) apply (subgoal_tac "(\i. X (i + Suc j)) \ (\i. Y (i + Suc j))") @@ -104,12 +104,12 @@ done lemma lub_equal2: - "\\j. \i>j. X i = Y i; chain (X::nat \ 'a::cpo); chain Y\ + "\\j. \i>j. X i = Y i; chain X; chain Y\ \ (\i. X i) = (\i. Y i)" -by (blast intro: antisym_less lub_mono2 sym) + by (blast intro: antisym_less lub_mono2 sym) lemma lub_mono3: - "\chain (Y::nat \ 'a::cpo); chain X; \i. \j. Y i \ X j\ + "\chain Y; chain X; \i. \j. Y i \ X j\ \ (\i. Y i) \ (\i. X i)" apply (erule is_lub_thelub) apply (rule ub_rangeI) @@ -120,7 +120,6 @@ done lemma ch2ch_lub: - fixes Y :: "nat \ nat \ 'a::cpo" assumes 1: "\j. chain (\i. Y i j)" assumes 2: "\i. chain (\j. Y i j)" shows "chain (\i. \j. Y i j)" @@ -130,7 +129,6 @@ done lemma diag_lub: - fixes Y :: "nat \ nat \ 'a::cpo" assumes 1: "\j. chain (\i. Y i j)" assumes 2: "\i. chain (\j. Y i j)" shows "(\i. \j. Y i j) = (\i. Y i i)" @@ -159,12 +157,12 @@ qed lemma ex_lub: - fixes Y :: "nat \ nat \ 'a::cpo" assumes 1: "\j. chain (\i. Y i j)" assumes 2: "\i. chain (\j. Y i j)" shows "(\i. \j. Y i j) = (\j. \i. Y i j)" -by (simp add: diag_lub 1 2) + by (simp add: diag_lub 1 2) +end subsection {* Pointed cpos *} @@ -172,9 +170,9 @@ class pcpo = cpo + assumes least: "\x. \y. x \ y" +begin -definition - UU :: "'a::pcpo" where +definition UU :: 'a where "UU = (THE x. \y. x \ y)" notation (xsymbols) @@ -193,6 +191,8 @@ lemma minimal [iff]: "\ \ x" by (rule UU_least [THEN spec]) +end + text {* Simproc to rewrite @{term "\ = x"} to @{term "x = \"}. *} setup {* @@ -202,6 +202,9 @@ simproc_setup reorient_bottom ("\ = x") = ReorientProc.proc +context pcpo +begin + text {* useful lemmas about @{term \} *} lemma less_UU_iff [simp]: "(x \ \) = (x = \)" @@ -213,9 +216,6 @@ lemma UU_I: "x \ \ \ x = \" by (subst eq_UU_iff) -lemma not_less2not_eq: "\ (x::'a::po) \ y \ x \ y" -by auto - lemma chain_UU_I: "\chain Y; (\i. Y i) = \\ \ \i. Y i = \" apply (rule allI) apply (rule UU_I) @@ -230,49 +230,53 @@ done lemma chain_UU_I_inverse2: "(\i. Y i) \ \ \ \i::nat. Y i \ \" -by (blast intro: chain_UU_I_inverse) + by (blast intro: chain_UU_I_inverse) lemma notUU_I: "\x \ y; x \ \\ \ y \ \" -by (blast intro: UU_I) + by (blast intro: UU_I) lemma chain_mono2: "\\j. Y j \ \; chain Y\ \ \j. \i>j. Y i \ \" -by (blast dest: notUU_I chain_mono_less) + by (blast dest: notUU_I chain_mono_less) + +end subsection {* Chain-finite and flat cpos *} text {* further useful classes for HOLCF domains *} -class finite_po = finite + po +class chfin = po + + assumes chfin: "chain Y \ \n. max_in_chain n Y" +begin -class chfin = po + - assumes chfin: "chain Y \ \n. max_in_chain n (Y :: nat => 'a::po)" +subclass cpo +apply default +apply (frule chfin) +apply (blast intro: lub_finch1) +done -class flat = pcpo + - assumes ax_flat: "(x :: 'a::pcpo) \ y \ x = \ \ x = y" +lemma chfin2finch: "chain Y \ finite_chain Y" + by (simp add: chfin finite_chain_def) + +end -text {* finite partial orders are chain-finite *} +class finite_po = finite + po +begin -instance finite_po < chfin -apply intro_classes +subclass chfin +apply default apply (drule finite_range_imp_finch) apply (rule finite) apply (simp add: finite_chain_def) done -text {* some properties for chfin and flat *} - -text {* chfin types are cpo *} +end -instance chfin < cpo -apply intro_classes -apply (frule chfin) -apply (blast intro: lub_finch1) -done +class flat = pcpo + + assumes ax_flat: "x \ y \ x = \ \ x = y" +begin -text {* flat types are chfin *} - -instance flat < chfin -apply intro_classes +subclass chfin +apply default apply (unfold max_in_chain_def) apply (case_tac "\i. Y i = \") apply simp @@ -283,31 +287,28 @@ apply (blast dest: chain_mono ax_flat) done -text {* flat subclass of chfin; @{text adm_flat} not needed *} - lemma flat_less_iff: - fixes x y :: "'a::flat" shows "(x \ y) = (x = \ \ x = y)" -by (safe dest!: ax_flat) + by (safe dest!: ax_flat) -lemma flat_eq: "(a::'a::flat) \ \ \ a \ b = (a = b)" -by (safe dest!: ax_flat) +lemma flat_eq: "a \ \ \ a \ b = (a = b)" + by (safe dest!: ax_flat) -lemma chfin2finch: "chain (Y::nat \ 'a::chfin) \ finite_chain Y" -by (simp add: chfin finite_chain_def) +end text {* Discrete cpos *} class discrete_cpo = sq_ord + assumes discrete_cpo [simp]: "x \ y \ x = y" +begin -subclass (in discrete_cpo) po +subclass po proof qed simp_all text {* In a discrete cpo, every chain is constant *} lemma discrete_chain_const: - assumes S: "chain (S::nat \ 'a::discrete_cpo)" + assumes S: "chain S" shows "\x. S = (\i. x)" proof (intro exI ext) fix i :: nat @@ -316,7 +317,7 @@ thus "S i = S 0" by (rule sym) qed -instance discrete_cpo < cpo +subclass cpo proof fix S :: "nat \ 'a" assume S: "chain S" @@ -326,31 +327,6 @@ by (fast intro: lub_const) qed -text {* lemmata for improved admissibility introdution rule *} - -lemma infinite_chain_adm_lemma: - "\chain Y; \i. P (Y i); - \Y. \chain Y; \i. P (Y i); \ finite_chain Y\ \ P (\i. Y i)\ - \ P (\i. Y i)" -apply (case_tac "finite_chain Y") -prefer 2 apply fast -apply (unfold finite_chain_def) -apply safe -apply (erule lub_finch1 [THEN thelubI, THEN ssubst]) -apply assumption -apply (erule spec) -done - -lemma increasing_chain_adm_lemma: - "\chain Y; \i. P (Y i); \Y. \chain Y; \i. P (Y i); - \i. \j>i. Y i \ Y j \ Y i \ Y j\ \ P (\i. Y i)\ - \ P (\i. Y i)" -apply (erule infinite_chain_adm_lemma) -apply assumption -apply (erule thin_rl) -apply (unfold finite_chain_def) -apply (unfold max_in_chain_def) -apply (fast dest: le_imp_less_or_eq elim: chain_mono_less) -done +end end diff -r 9950ca962e20 -r 35b437f7ad51 src/HOLCF/Porder.thy --- a/src/HOLCF/Porder.thy Fri May 08 08:07:05 2009 +0200 +++ b/src/HOLCF/Porder.thy Fri May 08 19:20:00 2009 +0200 @@ -12,6 +12,7 @@ class sq_ord = fixes sq_le :: "'a \ 'a \ bool" +begin notation sq_le (infixl "<<" 55) @@ -19,35 +20,43 @@ notation (xsymbols) sq_le (infixl "\" 55) +lemma sq_ord_less_eq_trans: "\a \ b; b = c\ \ a \ c" + by (rule subst) + +lemma sq_ord_eq_less_trans: "\a = b; b \ c\ \ a \ c" + by (rule ssubst) + +end + class po = sq_ord + assumes refl_less [iff]: "x \ x" - assumes trans_less: "\x \ y; y \ z\ \ x \ z" - assumes antisym_less: "\x \ y; y \ x\ \ x = y" + assumes trans_less: "x \ y \ y \ z \ x \ z" + assumes antisym_less: "x \ y \ y \ x \ x = y" +begin text {* minimal fixes least element *} -lemma minimal2UU[OF allI] : "\x::'a::po. uu \ x \ uu = (THE u. \y. u \ y)" -by (blast intro: theI2 antisym_less) +lemma minimal2UU[OF allI] : "\x. uu \ x \ uu = (THE u. \y. u \ y)" + by (blast intro: theI2 antisym_less) text {* the reverse law of anti-symmetry of @{term "op <<"} *} -lemma antisym_less_inverse: "(x::'a::po) = y \ x \ y \ y \ x" -by simp +lemma antisym_less_inverse: "x = y \ x \ y \ y \ x" + by simp -lemma box_less: "\(a::'a::po) \ b; c \ a; b \ d\ \ c \ d" -by (rule trans_less [OF trans_less]) - -lemma po_eq_conv: "((x::'a::po) = y) = (x \ y \ y \ x)" -by (fast elim!: antisym_less_inverse intro!: antisym_less) +lemma box_less: "a \ b \ c \ a \ b \ d \ c \ d" + by (rule trans_less [OF trans_less]) -lemma rev_trans_less: "\(y::'a::po) \ z; x \ y\ \ x \ z" -by (rule trans_less) +lemma po_eq_conv: "x = y \ x \ y \ y \ x" + by (fast elim!: antisym_less_inverse intro!: antisym_less) -lemma sq_ord_less_eq_trans: "\a \ b; b = c\ \ a \ c" -by (rule subst) +lemma rev_trans_less: "y \ z \ x \ y \ x \ z" + by (rule trans_less) -lemma sq_ord_eq_less_trans: "\a = b; b \ c\ \ a \ c" -by (rule ssubst) +lemma not_less2not_eq: "\ x \ y \ x \ y" + by auto + +end lemmas HOLCF_trans_rules [trans] = trans_less @@ -55,49 +64,51 @@ sq_ord_less_eq_trans sq_ord_eq_less_trans +context po +begin + subsection {* Upper bounds *} -definition - is_ub :: "['a set, 'a::po] \ bool" (infixl "<|" 55) where - "(S <| x) = (\y. y \ S \ y \ x)" +definition is_ub :: "'a set \ 'a \ bool" (infixl "<|" 55) where + "S <| x \ (\y. y \ S \ y \ x)" lemma is_ubI: "(\x. x \ S \ x \ u) \ S <| u" -by (simp add: is_ub_def) + by (simp add: is_ub_def) lemma is_ubD: "\S <| u; x \ S\ \ x \ u" -by (simp add: is_ub_def) + by (simp add: is_ub_def) lemma ub_imageI: "(\x. x \ S \ f x \ u) \ (\x. f x) ` S <| u" -unfolding is_ub_def by fast + unfolding is_ub_def by fast lemma ub_imageD: "\f ` S <| u; x \ S\ \ f x \ u" -unfolding is_ub_def by fast + unfolding is_ub_def by fast lemma ub_rangeI: "(\i. S i \ x) \ range S <| x" -unfolding is_ub_def by fast + unfolding is_ub_def by fast lemma ub_rangeD: "range S <| x \ S i \ x" -unfolding is_ub_def by fast + unfolding is_ub_def by fast lemma is_ub_empty [simp]: "{} <| u" -unfolding is_ub_def by fast + unfolding is_ub_def by fast lemma is_ub_insert [simp]: "(insert x A) <| y = (x \ y \ A <| y)" -unfolding is_ub_def by fast + unfolding is_ub_def by fast lemma is_ub_upward: "\S <| x; x \ y\ \ S <| y" -unfolding is_ub_def by (fast intro: trans_less) + unfolding is_ub_def by (fast intro: trans_less) subsection {* Least upper bounds *} -definition - is_lub :: "['a set, 'a::po] \ bool" (infixl "<<|" 55) where - "(S <<| x) = (S <| x \ (\u. S <| u \ x \ u))" +definition is_lub :: "'a set \ 'a \ bool" (infixl "<<|" 55) where + "S <<| x \ S <| x \ (\u. S <| u \ x \ u)" -definition - lub :: "'a set \ 'a::po" where +definition lub :: "'a set \ 'a" where "lub S = (THE x. S <<| x)" +end + syntax "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" ("(3LUB _:_./ _)" [0,0, 10] 10) @@ -107,6 +118,9 @@ translations "LUB x:A. t" == "CONST lub ((%x. t) ` A)" +context po +begin + abbreviation Lub (binder "LUB " 10) where "LUB n. t n == lub (range t)" @@ -117,13 +131,13 @@ text {* access to some definition as inference rule *} lemma is_lubD1: "S <<| x \ S <| x" -unfolding is_lub_def by fast + unfolding is_lub_def by fast lemma is_lub_lub: "\S <<| x; S <| u\ \ x \ u" -unfolding is_lub_def by fast + unfolding is_lub_def by fast lemma is_lubI: "\S <| x; \u. S <| u \ x \ u\ \ S <<| x" -unfolding is_lub_def by fast + unfolding is_lub_def by fast text {* lubs are unique *} @@ -142,54 +156,53 @@ done lemma thelubI: "M <<| l \ lub M = l" -by (rule unique_lub [OF lubI]) + by (rule unique_lub [OF lubI]) lemma is_lub_singleton: "{x} <<| x" -by (simp add: is_lub_def) + by (simp add: is_lub_def) lemma lub_singleton [simp]: "lub {x} = x" -by (rule thelubI [OF is_lub_singleton]) + by (rule thelubI [OF is_lub_singleton]) lemma is_lub_bin: "x \ y \ {x, y} <<| y" -by (simp add: is_lub_def) + by (simp add: is_lub_def) lemma lub_bin: "x \ y \ lub {x, y} = y" -by (rule is_lub_bin [THEN thelubI]) + by (rule is_lub_bin [THEN thelubI]) lemma is_lub_maximal: "\S <| x; x \ S\ \ S <<| x" -by (erule is_lubI, erule (1) is_ubD) + by (erule is_lubI, erule (1) is_ubD) lemma lub_maximal: "\S <| x; x \ S\ \ lub S = x" -by (rule is_lub_maximal [THEN thelubI]) + by (rule is_lub_maximal [THEN thelubI]) subsection {* Countable chains *} -definition +definition chain :: "(nat \ 'a) \ bool" where -- {* Here we use countable chains and I prefer to code them as functions! *} - chain :: "(nat \ 'a::po) \ bool" where "chain Y = (\i. Y i \ Y (Suc i))" lemma chainI: "(\i. Y i \ Y (Suc i)) \ chain Y" -unfolding chain_def by fast + unfolding chain_def by fast lemma chainE: "chain Y \ Y i \ Y (Suc i)" -unfolding chain_def by fast + unfolding chain_def by fast text {* chains are monotone functions *} lemma chain_mono_less: "\chain Y; i < j\ \ Y i \ Y j" -by (erule less_Suc_induct, erule chainE, erule trans_less) + by (erule less_Suc_induct, erule chainE, erule trans_less) lemma chain_mono: "\chain Y; i \ j\ \ Y i \ Y j" -by (cases "i = j", simp, simp add: chain_mono_less) + by (cases "i = j", simp, simp add: chain_mono_less) lemma chain_shift: "chain Y \ chain (\i. Y (i + j))" -by (rule chainI, simp, erule chainE) + by (rule chainI, simp, erule chainE) text {* technical lemmas about (least) upper bounds of chains *} lemma is_ub_lub: "range S <<| x \ S i \ x" -by (rule is_lubD1 [THEN ub_rangeD]) + by (rule is_lubD1 [THEN ub_rangeD]) lemma is_ub_range_shift: "chain S \ range (\i. S (i + j)) <| x = range S <| x" @@ -205,45 +218,43 @@ lemma is_lub_range_shift: "chain S \ range (\i. S (i + j)) <<| x = range S <<| x" -by (simp add: is_lub_def is_ub_range_shift) + by (simp add: is_lub_def is_ub_range_shift) text {* the lub of a constant chain is the constant *} lemma chain_const [simp]: "chain (\i. c)" -by (simp add: chainI) + by (simp add: chainI) lemma lub_const: "range (\x. c) <<| c" by (blast dest: ub_rangeD intro: is_lubI ub_rangeI) lemma thelub_const [simp]: "(\i. c) = c" -by (rule lub_const [THEN thelubI]) + by (rule lub_const [THEN thelubI]) subsection {* Finite chains *} -definition +definition max_in_chain :: "nat \ (nat \ 'a) \ bool" where -- {* finite chains, needed for monotony of continuous functions *} - max_in_chain :: "[nat, nat \ 'a::po] \ bool" where - "max_in_chain i C = (\j. i \ j \ C i = C j)" + "max_in_chain i C \ (\j. i \ j \ C i = C j)" -definition - finite_chain :: "(nat \ 'a::po) \ bool" where +definition finite_chain :: "(nat \ 'a) \ bool" where "finite_chain C = (chain C \ (\i. max_in_chain i C))" text {* results about finite chains *} lemma max_in_chainI: "(\j. i \ j \ Y i = Y j) \ max_in_chain i Y" -unfolding max_in_chain_def by fast + unfolding max_in_chain_def by fast lemma max_in_chainD: "\max_in_chain i Y; i \ j\ \ Y i = Y j" -unfolding max_in_chain_def by fast + unfolding max_in_chain_def by fast lemma finite_chainI: "\chain C; max_in_chain i C\ \ finite_chain C" -unfolding finite_chain_def by fast + unfolding finite_chain_def by fast lemma finite_chainE: "\finite_chain C; \i. \chain C; max_in_chain i C\ \ R\ \ R" -unfolding finite_chain_def by fast + unfolding finite_chain_def by fast lemma lub_finch1: "\chain C; max_in_chain i C\ \ range C <<| C i" apply (rule is_lubI) @@ -311,11 +322,11 @@ done lemma bin_chain: "x \ y \ chain (\i. if i=0 then x else y)" -by (rule chainI, simp) + by (rule chainI, simp) lemma bin_chainmax: "x \ y \ max_in_chain (Suc 0) (\i. if i=0 then x else y)" -unfolding max_in_chain_def by simp + unfolding max_in_chain_def by simp lemma lub_bin_chain: "x \ y \ range (\i::nat. if i=0 then x else y) <<| y" @@ -328,36 +339,35 @@ text {* the maximal element in a chain is its lub *} lemma lub_chain_maxelem: "\Y i = c; \i. Y i \ c\ \ lub (range Y) = c" -by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI) + by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI) subsection {* Directed sets *} -definition - directed :: "'a::po set \ bool" where - "directed S = ((\x. x \ S) \ (\x\S. \y\S. \z\S. x \ z \ y \ z))" +definition directed :: "'a set \ bool" where + "directed S \ (\x. x \ S) \ (\x\S. \y\S. \z\S. x \ z \ y \ z)" lemma directedI: assumes 1: "\z. z \ S" assumes 2: "\x y. \x \ S; y \ S\ \ \z\S. x \ z \ y \ z" shows "directed S" -unfolding directed_def using prems by fast + unfolding directed_def using prems by fast lemma directedD1: "directed S \ \z. z \ S" -unfolding directed_def by fast + unfolding directed_def by fast lemma directedD2: "\directed S; x \ S; y \ S\ \ \z\S. x \ z \ y \ z" -unfolding directed_def by fast + unfolding directed_def by fast lemma directedE1: assumes S: "directed S" obtains z where "z \ S" -by (insert directedD1 [OF S], fast) + by (insert directedD1 [OF S], fast) lemma directedE2: assumes S: "directed S" assumes x: "x \ S" and y: "y \ S" obtains z where "z \ S" "x \ z" "y \ z" -by (insert directedD2 [OF S x y], fast) + by (insert directedD2 [OF S x y], fast) lemma directed_finiteI: assumes U: "\U. \finite U; U \ S\ \ \z\S. U <| z" @@ -395,13 +405,13 @@ qed lemma not_directed_empty [simp]: "\ directed {}" -by (rule notI, drule directedD1, simp) + by (rule notI, drule directedD1, simp) lemma directed_singleton: "directed {x}" -by (rule directedI, auto) + by (rule directedI, auto) lemma directed_bin: "x \ y \ directed {x, y}" -by (rule directedI, auto) + by (rule directedI, auto) lemma directed_chain: "chain S \ directed (range S)" apply (rule directedI) @@ -412,4 +422,33 @@ apply simp done +text {* lemmata for improved admissibility introdution rule *} + +lemma infinite_chain_adm_lemma: + "\chain Y; \i. P (Y i); + \Y. \chain Y; \i. P (Y i); \ finite_chain Y\ \ P (\i. Y i)\ + \ P (\i. Y i)" +apply (case_tac "finite_chain Y") +prefer 2 apply fast +apply (unfold finite_chain_def) +apply safe +apply (erule lub_finch1 [THEN thelubI, THEN ssubst]) +apply assumption +apply (erule spec) +done + +lemma increasing_chain_adm_lemma: + "\chain Y; \i. P (Y i); \Y. \chain Y; \i. P (Y i); + \i. \j>i. Y i \ Y j \ Y i \ Y j\ \ P (\i. Y i)\ + \ P (\i. Y i)" +apply (erule infinite_chain_adm_lemma) +apply assumption +apply (erule thin_rl) +apply (unfold finite_chain_def) +apply (unfold max_in_chain_def) +apply (fast dest: le_imp_less_or_eq elim: chain_mono_less) +done + end + +end \ No newline at end of file