--- a/NEWS Wed Feb 25 10:28:49 2009 +0000
+++ b/NEWS Wed Feb 25 10:29:01 2009 +0000
@@ -367,6 +367,50 @@
mult_div ~> div_mult_self2_is_id
mult_mod ~> mod_mult_self2_is_0
+* HOL/IntDiv: removed most (all?) lemmas that are instances of class-based
+generalizations (from Divides and Ring_and_Field).
+INCOMPATIBILITY. Rename old lemmas as follows:
+
+dvd_diff -> nat_dvd_diff
+dvd_zminus_iff -> dvd_minus_iff
+nat_mod_add_left_eq -> mod_add_left_eq
+nat_mod_add_right_eq -> mod_add_right_eq
+nat_mod_div_trivial -> mod_div_trivial
+nat_mod_mod_trivial -> mod_mod_trivial
+zdiv_zadd_self1 -> div_add_self1
+zdiv_zadd_self2 -> div_add_self2
+zdiv_zmult_self2 -> div_mult_self1_is_id
+zdvd_triv_left -> dvd_triv_left
+zdvd_triv_right -> dvd_triv_right
+zdvd_zmult_cancel_disj -> dvd_mult_cancel_left
+zmod_eq0_zdvd_iff -> dvd_eq_mod_eq_0[symmetric]
+zmod_zadd_left_eq -> mod_add_left_eq
+zmod_zadd_right_eq -> mod_add_right_eq
+zmod_zadd_self1 -> mod_add_self1
+zmod_zadd_self2 -> mod_add_self2
+zmod_zdiff1_eq -> mod_diff_eq
+zmod_zdvd_zmod -> mod_mod_cancel
+zmod_zmod_cancel -> mod_mod_cancel
+zmod_zmult_self1 -> mod_mult_self2_is_0
+zmod_zmult_self2 -> mod_mult_self1_is_0
+zmod_1 -> mod_by_1
+zdiv_1 -> div_by_1
+zdvd_abs1 -> abs_dvd_iff
+zdvd_abs2 -> dvd_abs_iff
+zdvd_refl -> dvd_refl
+zdvd_trans -> dvd_trans
+zdvd_zadd -> dvd_add
+zdvd_zdiff -> dvd_diff
+zdvd_zminus_iff -> dvd_minus_iff
+zdvd_zminus2_iff -> minus_dvd_iff
+zdvd_zmultD -> dvd_mult_right
+zdvd_zmultD2 -> dvd_mult_left
+zdvd_zmult_mono -> mult_dvd_mono
+zdvd_0_right -> dvd_0_right
+zdvd_0_left -> dvd_0_left_iff
+zdvd_1_left -> one_dvd
+zminus_dvd_iff -> minus_dvd_iff
+
* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
zlcm (for int); carried together from various gcd/lcm developements in
the HOL Distribution. zgcd and zlcm replace former igcd and ilcm;
--- a/src/HOL/Algebra/Exponent.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Algebra/Exponent.thy Wed Feb 25 10:29:01 2009 +0000
@@ -210,12 +210,12 @@
lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]
==> (p^r) dvd (p^a) - k"
-apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
+apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto)
apply (subgoal_tac "p^r dvd p^a*m")
prefer 2 apply (blast intro: dvd_mult2)
apply (drule dvd_diffD1)
apply assumption
- prefer 2 apply (blast intro: dvd_diff)
+ prefer 2 apply (blast intro: nat_dvd_diff)
apply (drule gr0_implies_Suc, auto)
done
@@ -226,12 +226,12 @@
lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0; k < p^a; (p^r) dvd p^a - k |]
==> (p^r) dvd (p^a)*m - k"
-apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
+apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
apply (subgoal_tac "p^r dvd p^a*m")
prefer 2 apply (blast intro: dvd_mult2)
apply (drule dvd_diffD1)
apply assumption
- prefer 2 apply (blast intro: dvd_diff)
+ prefer 2 apply (blast intro: nat_dvd_diff)
apply (drule less_imp_Suc_add, auto)
done
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Wed Feb 25 10:29:01 2009 +0000
@@ -1,6 +1,5 @@
(*
Title: Univariate Polynomials
- Id: $Id$
Author: Clemens Ballarin, started 9 December 1996
Copyright: Clemens Ballarin
*)
@@ -388,7 +387,7 @@
proof (cases k)
case 0 then show ?thesis by simp ring
next
- case Suc then show ?thesis by (simp add: algebra_simps) ring
+ case Suc then show ?thesis by simp (ring, simp)
qed
then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
qed
--- a/src/HOL/Arith_Tools.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Arith_Tools.thy Wed Feb 25 10:29:01 2009 +0000
@@ -68,8 +68,9 @@
apply (subst add_eq_if)
apply (simp split add: nat.split
del: nat_numeral_1_eq_1
- add: numeral_1_eq_Suc_0 [symmetric] Let_def
- neg_imp_number_of_eq_0 neg_number_of_pred_iff_0)
+ add: nat_numeral_1_eq_1 [symmetric]
+ numeral_1_eq_Suc_0 [symmetric]
+ neg_number_of_pred_iff_0)
done
lemma nat_rec_number_of [simp]:
@@ -89,7 +90,8 @@
apply (subst add_eq_if)
apply (simp split add: nat.split
del: nat_numeral_1_eq_1
- add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
+ add: nat_numeral_1_eq_1 [symmetric]
+ numeral_1_eq_Suc_0 [symmetric]
neg_number_of_pred_iff_0)
done
--- a/src/HOL/Decision_Procs/Cooper.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Decision_Procs/Cooper.thy Wed Feb 25 10:29:01 2009 +0000
@@ -620,7 +620,7 @@
{assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def)}
moreover
{assume i1: "abs i = 1"
- from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
+ from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
have ?case using i1 apply (cases "i=0", simp_all add: Let_def)
by (cases "i > 0", simp_all)}
moreover
@@ -640,7 +640,7 @@
{assume "i=0" hence ?case using "13.hyps" by (simp add: dvd_def Let_def)}
moreover
{assume i1: "abs i = 1"
- from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
+ from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
have ?case using i1 apply (cases "i=0", simp_all add: Let_def)
apply (cases "i > 0", simp_all) done}
moreover
@@ -990,7 +990,7 @@
have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
moreover
{assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def)
- hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
+ hence ?case using prems by (simp del: zlfm.simps)}
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
using zsplit0_I[OF spl, where x="i" and bs="bs"]
@@ -1005,7 +1005,7 @@
moreover
{assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
+ hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r" ]
by (simp add: Let_def split_def) }
ultimately show ?case by blast
next
@@ -1019,7 +1019,7 @@
have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
moreover
{assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def)
- hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
+ hence ?case using prems by (simp del: zlfm.simps)}
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
using zsplit0_I[OF spl, where x="i" and bs="bs"]
@@ -1034,7 +1034,7 @@
moreover
{assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
+ hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
by (simp add: Let_def split_def)}
ultimately show ?case by blast
qed auto
@@ -1092,10 +1092,10 @@
using lin ad d
proof(induct p rule: iszlfm.induct)
case (9 i c e) thus ?case using d
- by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
+ by (simp add: dvd_trans[of "i" "d" "d'"])
next
case (10 i c e) thus ?case using d
- by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
+ by (simp add: dvd_trans[of "i" "d" "d'"])
qed simp_all
lemma \<delta> : assumes lin:"iszlfm p"
@@ -1354,7 +1354,7 @@
case (9 j c e) hence nb: "numbound0 e" by simp
have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
also have "\<dots> = (j dvd (- (c*x - ?e)))"
- by (simp only: zdvd_zminus_iff)
+ by (simp only: dvd_minus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
by (simp add: algebra_simps)
@@ -1366,7 +1366,7 @@
case (10 j c e) hence nb: "numbound0 e" by simp
have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
also have "\<dots> = (j dvd (- (c*x - ?e)))"
- by (simp only: zdvd_zminus_iff)
+ by (simp only: dvd_minus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
by (simp add: algebra_simps)
@@ -1392,7 +1392,7 @@
and dr: "d\<beta> p l"
and d: "l dvd l'"
shows "d\<beta> p l'"
-using dr linp zdvd_trans[where n="l" and k="l'", simplified d]
+using dr linp dvd_trans[of _ "l" "l'", simplified d]
by (induct p rule: iszlfm.induct) simp_all
lemma \<alpha>_l: assumes lp: "iszlfm p"
@@ -1431,7 +1431,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l*x + (l div c) * Inum (x # bs) e < 0) =
@@ -1449,7 +1449,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
@@ -1467,7 +1467,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l*x + (l div c)* Inum (x # bs) e > 0) =
@@ -1485,7 +1485,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
@@ -1505,7 +1505,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l * x + (l div c) * Inum (x # bs) e = 0) =
@@ -1523,7 +1523,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
@@ -1541,7 +1541,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp
@@ -1558,7 +1558,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp
--- a/src/HOL/Decision_Procs/Ferrack.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Feb 25 10:29:01 2009 +0000
@@ -501,9 +501,9 @@
assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'"
shows "dvdnumcoeff t g"
using dgt' gdg
- by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg zdvd_trans[OF gdg])
+ by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg])
-declare zdvd_trans [trans add]
+declare dvd_trans [trans add]
lemma natabs0: "(nat (abs x) = 0) = (x = 0)"
by arith
--- a/src/HOL/Decision_Procs/MIR.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Decision_Procs/MIR.thy Wed Feb 25 10:29:01 2009 +0000
@@ -132,13 +132,13 @@
assume d: "real d rdvd t"
from d int_rdvd_real have d2: "d dvd (floor t)" and ti: "real (floor t) = t" by auto
- from iffD2[OF zdvd_abs1] d2 have "(abs d) dvd (floor t)" by blast
+ from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd (floor t)" by blast
with ti int_rdvd_real[symmetric] have "real (abs d) rdvd t" by blast
thus "abs (real d) rdvd t" by simp
next
assume "abs (real d) rdvd t" hence "real (abs d) rdvd t" by simp
with int_rdvd_real[where i="abs d" and x="t"] have d2: "abs d dvd floor t" and ti: "real (floor t) =t" by auto
- from iffD1[OF zdvd_abs1] d2 have "d dvd floor t" by blast
+ from iffD1[OF abs_dvd_iff] d2 have "d dvd floor t" by blast
with ti int_rdvd_real[symmetric] show "real d rdvd t" by blast
qed
@@ -675,9 +675,9 @@
assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'"
shows "dvdnumcoeff t g"
using dgt' gdg
- by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg zdvd_trans[OF gdg])
-
-declare zdvd_trans [trans add]
+ by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg])
+
+declare dvd_trans [trans add]
lemma natabs0: "(nat (abs x) = 0) = (x = 0)"
by arith
@@ -2114,10 +2114,10 @@
using lin ad d
proof(induct p rule: iszlfm.induct)
case (9 i c e) thus ?case using d
- by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
+ by (simp add: dvd_trans[of "i" "d" "d'"])
next
case (10 i c e) thus ?case using d
- by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
+ by (simp add: dvd_trans[of "i" "d" "d'"])
qed simp_all
lemma \<delta> : assumes lin:"iszlfm p bs"
@@ -2496,7 +2496,7 @@
and dr: "d\<beta> p l"
and d: "l dvd l'"
shows "d\<beta> p l'"
-using dr linp zdvd_trans[where n="l" and k="l'", simplified d]
+using dr linp dvd_trans[of _ "l" "l'", simplified d]
by (induct p rule: iszlfm.induct) simp_all
lemma \<alpha>_l: assumes lp: "iszlfm p (a#bs)"
@@ -2535,7 +2535,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e < (0\<Colon>real)) =
@@ -2553,7 +2553,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<le> (0\<Colon>real)) =
@@ -2571,7 +2571,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e > (0\<Colon>real)) =
@@ -2589,7 +2589,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<ge> (0\<Colon>real)) =
@@ -2607,7 +2607,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e = (0\<Colon>real)) =
@@ -2625,7 +2625,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<noteq> (0\<Colon>real)) =
@@ -2643,7 +2643,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)" by simp
@@ -2660,7 +2660,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)" by simp
--- a/src/HOL/Decision_Procs/cooper_tac.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Feb 25 10:29:01 2009 +0000
@@ -28,11 +28,9 @@
val imp_le_cong = @{thm imp_le_cong};
val conj_le_cong = @{thm conj_le_cong};
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
-val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
-val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
+val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
+val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
val int_mod_add_eq = @{thm mod_add_eq} RS sym;
-val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
-val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
@@ -70,14 +68,13 @@
val (t,np,nh) = prepare_for_linz q g
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset = HOL_basic_ss
- addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq,
- nat_mod_add_right_eq, int_mod_add_eq,
- int_mod_add_right_eq, int_mod_add_left_eq,
+ addsimps [refl,nat_mod_add_eq, mod_add_left_eq,
+ mod_add_right_eq, int_mod_add_eq,
nat_div_add_eq, int_div_add_eq,
@{thm mod_self}, @{thm "zmod_self"},
@{thm mod_by_0}, @{thm div_by_0},
@{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
- @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
+ @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
Suc_plus1]
addsimps @{thms add_ac}
addsimprocs [cancel_div_mod_proc]
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed Feb 25 10:29:01 2009 +0000
@@ -32,11 +32,9 @@
val imp_le_cong = @{thm imp_le_cong};
val conj_le_cong = @{thm conj_le_cong};
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
-val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
-val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
+val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
+val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
val int_mod_add_eq = @{thm mod_add_eq} RS sym;
-val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
-val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
--- a/src/HOL/Decision_Procs/mir_tac.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Feb 25 10:29:01 2009 +0000
@@ -47,11 +47,9 @@
val imp_le_cong = @{thm "imp_le_cong"};
val conj_le_cong = @{thm "conj_le_cong"};
val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
-val nat_mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
-val nat_mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
+val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
+val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
-val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
-val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
@@ -99,7 +97,7 @@
addsimps [refl,nat_mod_add_eq,
@{thm "mod_self"}, @{thm "zmod_self"},
@{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
- @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
+ @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
@{thm "Suc_plus1"}]
addsimps @{thms add_ac}
addsimprocs [cancel_div_mod_proc]
--- a/src/HOL/Divides.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Divides.thy Wed Feb 25 10:29:01 2009 +0000
@@ -178,6 +178,12 @@
lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
+lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a"
+apply (cases "a = 0")
+ apply simp
+apply (auto simp: dvd_def mult_assoc)
+done
+
lemma div_dvd_div[simp]:
"a dvd b \<Longrightarrow> a dvd c \<Longrightarrow> (b div a dvd c div a) = (b dvd c)"
apply (cases "a = 0")
@@ -188,6 +194,12 @@
apply(fastsimp simp add: mult_assoc)
done
+lemma dvd_mod_imp_dvd: "[| k dvd m mod n; k dvd n |] ==> k dvd m"
+ apply (subgoal_tac "k dvd (m div n) *n + m mod n")
+ apply (simp add: mod_div_equality)
+ apply (simp only: dvd_add dvd_mult)
+ done
+
text {* Addition respects modular equivalence. *}
lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
@@ -478,9 +490,9 @@
from divmod_rel have divmod_m_n: "divmod_rel m n (m div n) (m mod n)" .
with assms have m_div_n: "m div n \<ge> 1"
by (cases "m div n") (auto simp add: divmod_rel_def)
- from assms divmod_m_n have "divmod_rel (m - n) n (m div n - 1) (m mod n)"
+ from assms divmod_m_n have "divmod_rel (m - n) n (m div n - Suc 0) (m mod n)"
by (cases "m div n") (auto simp add: divmod_rel_def)
- with divmod_eq have "divmod (m - n) n = (m div n - 1, m mod n)" by simp
+ with divmod_eq have "divmod (m - n) n = (m div n - Suc 0, m mod n)" by simp
moreover from divmod_div_mod have "divmod (m - n) n = ((m - n) div n, (m - n) mod n)" .
ultimately have "m div n = Suc ((m - n) div n)"
and "m mod n = (m - n) mod n" using m_div_n by simp_all
@@ -795,12 +807,6 @@
apply (auto simp add: Suc_diff_le le_mod_geq)
done
-lemma nat_mod_div_trivial: "m mod n div n = (0 :: nat)"
-by simp
-
-lemma nat_mod_mod_trivial: "m mod n mod n = (m mod n :: nat)"
-by simp
-
subsubsection {* The Divides Relation *}
@@ -810,6 +816,9 @@
lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
by (simp add: dvd_def)
+lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
+by (simp add: dvd_def)
+
lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
unfolding dvd_def
by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
@@ -819,9 +828,9 @@
interpretation dvd!: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
-lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
- unfolding dvd_def
- by (blast intro: diff_mult_distrib2 [symmetric])
+lemma nat_dvd_diff[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
+unfolding dvd_def
+by (blast intro: diff_mult_distrib2 [symmetric])
lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
@@ -829,7 +838,7 @@
done
lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
-by (drule_tac m = m in dvd_diff, auto)
+by (drule_tac m = m in nat_dvd_diff, auto)
lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
apply (rule iffI)
@@ -838,7 +847,7 @@
apply (subgoal_tac "n = (n+k) -k")
prefer 2 apply simp
apply (erule ssubst)
- apply (erule dvd_diff)
+ apply (erule nat_dvd_diff)
apply (rule dvd_refl)
done
@@ -848,12 +857,6 @@
apply (blast intro: mod_mult_distrib2 [symmetric])
done
-lemma dvd_mod_imp_dvd: "[| (k::nat) dvd m mod n; k dvd n |] ==> k dvd m"
- apply (subgoal_tac "k dvd (m div n) *n + m mod n")
- apply (simp add: mod_div_equality)
- apply (simp only: dvd_add dvd_mult)
- done
-
lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
by (blast intro: dvd_mod_imp_dvd dvd_mod)
--- a/src/HOL/Extraction/Euclid.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Extraction/Euclid.thy Wed Feb 25 10:29:01 2009 +0000
@@ -189,7 +189,7 @@
assume pn: "p \<le> n"
from `prime p` have "0 < p" by (rule prime_g_zero)
then have "p dvd n!" using pn by (rule dvd_factorial)
- with dvd have "p dvd ?k - n!" by (rule dvd_diff)
+ with dvd have "p dvd ?k - n!" by (rule nat_dvd_diff)
then have "p dvd 1" by simp
with prime show False using prime_nd_one by auto
qed
--- a/src/HOL/Fact.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Fact.thy Wed Feb 25 10:29:01 2009 +0000
@@ -7,7 +7,7 @@
header{*Factorial Function*}
theory Fact
-imports Nat
+imports Main
begin
consts fact :: "nat => nat"
@@ -58,7 +58,7 @@
"n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
apply (induct n arbitrary: m)
apply auto
-apply (drule_tac x = "m - 1" in meta_spec, auto)
+apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
done
lemma fact_num0: "fact 0 = 1"
--- a/src/HOL/GCD.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/GCD.thy Wed Feb 25 10:29:01 2009 +0000
@@ -60,9 +60,12 @@
lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
by simp
-lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = 1"
+lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
by simp
+lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
+ unfolding One_nat_def by (rule gcd_1)
+
declare gcd.simps [simp del]
text {*
@@ -116,9 +119,12 @@
apply (blast intro: dvd_trans)
done
-lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = 1"
+lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
by (simp add: gcd_commute)
+lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
+ unfolding One_nat_def by (rule gcd_1_left)
+
text {*
\medskip Multiplication laws
*}
@@ -156,7 +162,6 @@
apply (simp add: gcd_assoc)
apply (simp add: gcd_commute)
apply (simp_all add: mult_commute)
- apply (blast intro: dvd_mult)
done
@@ -404,7 +409,7 @@
{fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
- from dvd_diff[OF dv(1,2)] dvd_diff[OF dv(3,4)] H
+ from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
have ?rhs by auto}
ultimately show ?thesis by blast
qed
@@ -597,8 +602,8 @@
from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
then show ?thesis
- apply (subst zdvd_abs1 [symmetric])
- apply (subst zdvd_abs2 [symmetric])
+ apply (subst abs_dvd_iff [symmetric])
+ apply (subst dvd_abs_iff [symmetric])
apply (unfold dvd_def)
apply (rule_tac x = "int h'" in exI, simp)
done
@@ -614,11 +619,11 @@
let ?m' = "nat \<bar>m\<bar>"
let ?n' = "nat \<bar>n\<bar>"
from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
- unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2)
+ unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
unfolding zgcd_def by (simp only: zdvd_int)
then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
- then show "k dvd zgcd m n" by (simp add: zdvd_abs1)
+ then show "k dvd zgcd m n" by simp
qed
lemma div_zgcd_relprime:
@@ -721,7 +726,7 @@
assumes "k dvd i" shows "k dvd (zlcm i j)"
proof -
have "nat(abs k) dvd nat(abs i)" using `k dvd i`
- by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
+ by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
qed
@@ -729,7 +734,7 @@
assumes "k dvd j" shows "k dvd (zlcm i j)"
proof -
have "nat(abs k) dvd nat(abs j)" using `k dvd j`
- by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
+ by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
qed
--- a/src/HOL/Groebner_Basis.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Groebner_Basis.thy Wed Feb 25 10:29:01 2009 +0000
@@ -147,7 +147,7 @@
next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
next show "pwr x 0 = r1" using pwr_0 .
-next show "pwr x 1 = x" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
+next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr)
@@ -436,8 +436,8 @@
*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
declare dvd_def[algebra]
declare dvd_eq_mod_eq_0[symmetric, algebra]
-declare nat_mod_div_trivial[algebra]
-declare nat_mod_mod_trivial[algebra]
+declare mod_div_trivial[algebra]
+declare mod_mod_trivial[algebra]
declare conjunct1[OF DIVISION_BY_ZERO, algebra]
declare conjunct2[OF DIVISION_BY_ZERO, algebra]
declare zmod_zdiv_equality[symmetric,algebra]
@@ -448,16 +448,16 @@
declare zmod_zminus2[algebra]
declare zdiv_zero[algebra]
declare zmod_zero[algebra]
-declare zmod_1[algebra]
-declare zdiv_1[algebra]
+declare mod_by_1[algebra]
+declare div_by_1[algebra]
declare zmod_minus1_right[algebra]
declare zdiv_minus1_right[algebra]
declare mod_div_trivial[algebra]
declare mod_mod_trivial[algebra]
-declare zmod_zmult_self1[algebra]
-declare zmod_zmult_self2[algebra]
+declare mod_mult_self2_is_0[algebra]
+declare mod_mult_self1_is_0[algebra]
declare zmod_eq_0_iff[algebra]
-declare zdvd_0_left[algebra]
+declare dvd_0_left_iff[algebra]
declare zdvd1_eq[algebra]
declare zmod_eq_dvd_iff[algebra]
declare nat_mod_eq_iff[algebra]
--- a/src/HOL/HOL.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/HOL.thy Wed Feb 25 10:29:01 2009 +0000
@@ -28,7 +28,8 @@
("~~/src/Tools/induct_tacs.ML")
"~~/src/Tools/value.ML"
"~~/src/Tools/code/code_name.ML"
- "~~/src/Tools/code/code_funcgr.ML"
+ "~~/src/Tools/code/code_wellsorted.ML" (* formal dependency *)
+ (*"~~/src/Tools/code/code_funcgr.ML"*)
"~~/src/Tools/code/code_thingol.ML"
"~~/src/Tools/code/code_printer.ML"
"~~/src/Tools/code/code_target.ML"
--- a/src/HOL/Hoare/Arith2.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Hoare/Arith2.thy Wed Feb 25 10:29:01 2009 +0000
@@ -42,12 +42,12 @@
lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n"
apply (unfold cd_def)
- apply (blast intro: dvd_diff dest: dvd_diffD)
+ apply (fastsimp dest: dvd_diffD)
done
lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)"
apply (unfold cd_def)
- apply (blast intro: dvd_diff dest: dvd_diffD)
+ apply (fastsimp dest: dvd_diffD)
done
--- a/src/HOL/Int.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Int.thy Wed Feb 25 10:29:01 2009 +0000
@@ -832,8 +832,8 @@
le_imp_0_less [THEN order_less_imp_le])
next
case (neg n)
- thus ?thesis by (simp del: of_nat_Suc of_nat_add
- add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric])
+ thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
+ add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
qed
lemma bin_less_0_simps:
@@ -1165,8 +1165,8 @@
le_imp_0_less [THEN order_less_imp_le])
next
case (neg n)
- thus ?thesis by (simp del: of_nat_Suc of_nat_add
- add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric])
+ thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
+ add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
qed
text {* Less-Than or Equals *}
@@ -1785,11 +1785,12 @@
lemma int_val_lemma:
"(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
+unfolding One_nat_def
apply (induct n, simp)
apply (intro strip)
apply (erule impE, simp)
apply (erule_tac x = n in allE, simp)
-apply (case_tac "k = f (n+1) ")
+apply (case_tac "k = f (Suc n)")
apply force
apply (erule impE)
apply (simp add: abs_if split add: split_if_asm)
@@ -1803,6 +1804,7 @@
f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
in int_val_lemma)
+unfolding One_nat_def
apply simp
apply (erule exE)
apply (rule_tac x = "i+m" in exI, arith)
--- a/src/HOL/IntDiv.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/IntDiv.thy Wed Feb 25 10:29:01 2009 +0000
@@ -547,34 +547,6 @@
simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
{* K (divmod_proc (@{thm divmod_rel_mod_eq})) *}
-(* The following 8 lemmas are made unnecessary by the above simprocs: *)
-
-lemmas div_pos_pos_number_of =
- div_pos_pos [of "number_of v" "number_of w", standard]
-
-lemmas div_neg_pos_number_of =
- div_neg_pos [of "number_of v" "number_of w", standard]
-
-lemmas div_pos_neg_number_of =
- div_pos_neg [of "number_of v" "number_of w", standard]
-
-lemmas div_neg_neg_number_of =
- div_neg_neg [of "number_of v" "number_of w", standard]
-
-
-lemmas mod_pos_pos_number_of =
- mod_pos_pos [of "number_of v" "number_of w", standard]
-
-lemmas mod_neg_pos_number_of =
- mod_neg_pos [of "number_of v" "number_of w", standard]
-
-lemmas mod_pos_neg_number_of =
- mod_pos_neg [of "number_of v" "number_of w", standard]
-
-lemmas mod_neg_neg_number_of =
- mod_neg_neg [of "number_of v" "number_of w", standard]
-
-
lemmas posDivAlg_eqn_number_of [simp] =
posDivAlg_eqn [of "number_of v" "number_of w", standard]
@@ -584,15 +556,6 @@
text{*Special-case simplification *}
-lemma zmod_1 [simp]: "a mod (1::int) = 0"
-apply (cut_tac a = a and b = 1 in pos_mod_sign)
-apply (cut_tac [2] a = a and b = 1 in pos_mod_bound)
-apply (auto simp del:pos_mod_bound pos_mod_sign)
-done
-
-lemma zdiv_1 [simp]: "a div (1::int) = a"
-by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto)
-
lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"
apply (cut_tac a = a and b = "-1" in neg_mod_sign)
apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
@@ -784,41 +747,12 @@
show ?thesis by simp
qed
-lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
-by (rule div_add_self1) (* already declared [simp] *)
-
-lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
-by (rule div_add_self2) (* already declared [simp] *)
-
-lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
-by (rule div_mult_self1_is_id) (* already declared [simp] *)
-
-lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
-by (rule mod_mult_self2_is_0) (* already declared [simp] *)
-
-lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
-by (rule mod_mult_self1_is_0) (* already declared [simp] *)
-
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
(* REVISIT: should this be generalized to all semiring_div types? *)
lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
-lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
-by (rule mod_add_left_eq)
-
-lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
-by (rule mod_add_right_eq)
-
-lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
-by (rule mod_add_self1) (* already declared [simp] *)
-
-lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
-by (rule mod_add_self2) (* already declared [simp] *)
-
-lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
-by (rule mod_diff_eq)
subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *}
@@ -902,13 +836,6 @@
"(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"
by (simp add:zdiv_zmult_zmult1)
-(*
-lemma zdiv_zmult_zmult2: "c \<noteq> (0::int) ==> (a*c) div (b*c) = a div b"
-apply (drule zdiv_zmult_zmult1)
-apply (auto simp add: mult_commute)
-done
-*)
-
subsection{*Distribution of Factors over mod*}
@@ -933,9 +860,6 @@
apply (auto simp add: mult_commute)
done
-lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
-by (rule mod_mod_cancel)
-
subsection {*Splitting Rules for div and mod*}
@@ -1070,7 +994,7 @@
apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) =
1 + 2* ((-b - 1) mod (-a))")
apply (rule_tac [2] pos_zmod_mult_2)
-apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib)
+apply (auto simp add: right_diff_distrib)
apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
prefer 2 apply simp
apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric])
@@ -1132,38 +1056,8 @@
subsection {* The Divides Relation *}
-lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
- by (rule dvd_eq_mod_eq_0)
-
lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
- zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
-
-lemma zdvd_0_right: "(m::int) dvd 0"
- by (rule dvd_0_right) (* already declared [iff] *)
-
-lemma zdvd_0_left: "(0 dvd (m::int)) = (m = 0)"
- by (rule dvd_0_left_iff) (* already declared [noatp,simp] *)
-
-lemma zdvd_1_left: "1 dvd (m::int)"
- by (rule one_dvd) (* already declared [simp] *)
-
-lemma zdvd_refl: "m dvd (m::int)"
- by (rule dvd_refl) (* already declared [simp] *)
-
-lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
- by (rule dvd_trans)
-
-lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
- by (rule dvd_minus_iff) (* already declared [simp] *)
-
-lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
- by (rule minus_dvd_iff) (* already declared [simp] *)
-
-lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
- by (rule abs_dvd_iff) (* already declared [simp] *)
-
-lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
- by (rule dvd_abs_iff) (* already declared [simp] *)
+ dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
lemma zdvd_anti_sym:
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
@@ -1171,58 +1065,32 @@
apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
done
-lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
- by (rule dvd_add)
-
-lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a"
+lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a"
shows "\<bar>a\<bar> = \<bar>b\<bar>"
proof-
- from ab obtain k where k:"b = a*k" unfolding dvd_def by blast
- from ba obtain k' where k':"a = b*k'" unfolding dvd_def by blast
+ from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
+ from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
from k k' have "a = a*k*k'" by simp
with mult_cancel_left1[where c="a" and b="k*k'"]
- have kk':"k*k' = 1" using anz by (simp add: mult_assoc)
+ have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
thus ?thesis using k k' by auto
qed
-lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
- by (rule Ring_and_Field.dvd_diff)
-
lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
apply (subgoal_tac "m = n + (m - n)")
apply (erule ssubst)
- apply (blast intro: zdvd_zadd, simp)
+ apply (blast intro: dvd_add, simp)
done
-lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
- by (rule dvd_mult)
-
-lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
- by (rule dvd_mult2)
-
-lemma zdvd_triv_right: "(k::int) dvd m * k"
- by (rule dvd_triv_right) (* already declared [simp] *)
-
-lemma zdvd_triv_left: "(k::int) dvd k * m"
- by (rule dvd_triv_left) (* already declared [simp] *)
-
-lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
- by (rule dvd_mult_left)
-
-lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
- by (rule dvd_mult_right)
-
-lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
- by (rule mult_dvd_mono)
-
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
- apply (rule iffI)
- apply (erule_tac [2] zdvd_zadd)
- apply (subgoal_tac "n = (n + k * m) - k * m")
- apply (erule ssubst)
- apply (erule zdvd_zdiff, simp_all)
- done
+apply (rule iffI)
+ apply (erule_tac [2] dvd_add)
+ apply (subgoal_tac "n = (n + k * m) - k * m")
+ apply (erule ssubst)
+ apply (erule dvd_diff)
+ apply(simp_all)
+done
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
apply (simp add: dvd_def)
@@ -1232,7 +1100,7 @@
lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
apply (subgoal_tac "k dvd n * (m div n) + m mod n")
apply (simp add: zmod_zdiv_equality [symmetric])
- apply (simp only: zdvd_zadd zdvd_zmult2)
+ apply (simp only: dvd_add dvd_mult2)
done
lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
@@ -1252,7 +1120,7 @@
lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
apply (subgoal_tac "m mod n = 0")
apply (simp add: zmult_div_cancel)
-apply (simp only: zdvd_iff_zmod_eq_0)
+apply (simp only: dvd_eq_mod_eq_0)
done
lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
@@ -1265,10 +1133,6 @@
thus ?thesis by simp
qed
-lemma zdvd_zmult_cancel_disj:
- "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
-by (rule dvd_mult_cancel_left) (* already declared [simp] *)
-
theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
apply (simp split add: split_nat)
@@ -1300,44 +1164,38 @@
then show ?thesis by (simp only: negative_eq_positive) auto
qed
qed
- then show ?thesis by (auto elim!: dvdE simp only: zdvd_triv_left int_mult)
+ then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult)
qed
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
proof
- assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
+ assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
hence "nat \<bar>x\<bar> = 1" by simp
thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
next
assume "\<bar>x\<bar>=1" thus "x dvd 1"
- by(cases "x < 0",simp_all add: minus_equation_iff zdvd_iff_zmod_eq_0)
+ by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0)
qed
lemma zdvd_mult_cancel1:
assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
proof
assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
- by (cases "n >0", auto simp add: zdvd_zminus2_iff minus_equation_iff)
+ by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
next
assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
qed
lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
- unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus_iff)
+ unfolding zdvd_int by (cases "z \<ge> 0") simp_all
lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
- unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus2_iff)
+ unfolding zdvd_int by (cases "z \<ge> 0") simp_all
lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
by (auto simp add: dvd_int_iff)
-lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
- by (rule minus_dvd_iff)
-
-lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
- by (rule dvd_minus_iff)
-
lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
apply (rule_tac z=n in int_cases)
apply (auto simp add: dvd_int_iff)
@@ -1370,7 +1228,7 @@
text{*Suggested by Matthias Daum*}
lemma int_power_div_base:
"\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
-apply (subgoal_tac "k ^ m = k ^ ((m - 1) + 1)")
+apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
apply (erule ssubst)
apply (simp only: power_add)
apply simp_all
@@ -1387,8 +1245,8 @@
by (rule mod_diff_right_eq [symmetric])
lemmas zmod_simps =
- IntDiv.zmod_zadd_left_eq [symmetric]
- IntDiv.zmod_zadd_right_eq [symmetric]
+ mod_add_left_eq [symmetric]
+ mod_add_right_eq [symmetric]
IntDiv.zmod_zmult1_eq [symmetric]
mod_mult_left_eq [symmetric]
IntDiv.zpower_zmod
@@ -1463,14 +1321,14 @@
assume H: "x mod n = y mod n"
hence "x mod n - y mod n = 0" by simp
hence "(x mod n - y mod n) mod n = 0" by simp
- hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric])
- thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
+ hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
+ thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
next
assume H: "n dvd x - y"
then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
hence "x = n*k + y" by simp
hence "x mod n = (n*k + y) mod n" by simp
- thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq)
+ thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
qed
lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
--- a/src/HOL/Integration.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Integration.thy Wed Feb 25 10:29:01 2009 +0000
@@ -134,7 +134,7 @@
apply (frule partition [THEN iffD1], safe)
apply (drule_tac x = "psize D" and P="%n. psize D \<le> n --> ?P n" in spec, safe)
apply (case_tac "psize D = 0")
-apply (drule_tac [2] n = "psize D - 1" in partition_lt, auto)
+apply (drule_tac [2] n = "psize D - Suc 0" in partition_lt, auto)
done
lemma partition_gt: "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)"
@@ -145,7 +145,7 @@
apply (rotate_tac 2)
apply (drule_tac x = "psize D" in spec)
apply (rule ccontr)
-apply (drule_tac n = "psize D - 1" in partition_lt)
+apply (drule_tac n = "psize D - Suc 0" in partition_lt)
apply auto
done
--- a/src/HOL/IsaMakefile Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/IsaMakefile Wed Feb 25 10:29:01 2009 +0000
@@ -86,7 +86,7 @@
Tools/simpdata.ML \
$(SRC)/Tools/atomize_elim.ML \
$(SRC)/Tools/code/code_funcgr.ML \
- $(SRC)/Tools/code/code_funcgr.ML \
+ $(SRC)/Tools/code/code_wellsorted.ML \
$(SRC)/Tools/code/code_name.ML \
$(SRC)/Tools/code/code_printer.ML \
$(SRC)/Tools/code/code_target.ML \
@@ -339,6 +339,8 @@
Library/Random.thy Library/Quickcheck.thy \
Library/Poly_Deriv.thy \
Library/Polynomial.thy \
+ Library/Product_plus.thy \
+ Library/Product_Vector.thy \
Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
Library/reify_data.ML Library/reflection.ML
@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
--- a/src/HOL/Library/Abstract_Rat.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Abstract_Rat.thy Wed Feb 25 10:29:01 2009 +0000
@@ -247,7 +247,7 @@
(of_int(n div d)::'a::{field, ring_char_0}) = of_int n / of_int d"
apply (frule of_int_div_aux [of d n, where ?'a = 'a])
apply simp
- apply (simp add: zdvd_iff_zmod_eq_0)
+ apply (simp add: dvd_eq_mod_eq_0)
done
--- a/src/HOL/Library/Code_Char.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Code_Char.thy Wed Feb 25 10:29:01 2009 +0000
@@ -1,5 +1,4 @@
(* Title: HOL/Library/Code_Char.thy
- ID: $Id$
Author: Florian Haftmann
*)
--- a/src/HOL/Library/Determinants.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Determinants.thy Wed Feb 25 10:29:01 2009 +0000
@@ -1048,7 +1048,7 @@
note th0 = this
let ?g = "\<lambda>x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)"
{fix x:: "real ^'n" assume nx: "norm x = 1"
- have "?g x = f x" using nx by (simp add: norm_eq_0[symmetric])}
+ have "?g x = f x" using nx by auto}
hence thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" by blast
have g0: "?g 0 = 0" by simp
{fix x y :: "real ^'n"
@@ -1057,15 +1057,15 @@
moreover
{assume "x = 0" "y \<noteq> 0"
then have "dist (?g x) (?g y) = dist x y"
- apply (simp add: dist_def norm_neg norm_mul norm_eq_0)
+ apply (simp add: dist_def norm_mul)
apply (rule f1[rule_format])
- by(simp add: norm_mul norm_eq_0 field_simps)}
+ by(simp add: norm_mul field_simps)}
moreover
{assume "x \<noteq> 0" "y = 0"
then have "dist (?g x) (?g y) = dist x y"
- apply (simp add: dist_def norm_neg norm_mul norm_eq_0)
+ apply (simp add: dist_def norm_mul)
apply (rule f1[rule_format])
- by(simp add: norm_mul norm_eq_0 field_simps)}
+ by(simp add: norm_mul field_simps)}
moreover
{assume z: "x \<noteq> 0" "y \<noteq> 0"
have th00: "x = norm x *s inverse (norm x) *s x" "y = norm y *s inverse (norm y) *s y" "norm x *s f (inverse (norm x) *s x) = norm x *s f (inverse (norm x) *s x)"
@@ -1077,7 +1077,7 @@
"norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) =
norm (inverse (norm x) *s x - inverse (norm y) *s y)"
using z
- by (auto simp add: norm_eq_0 vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_def])
+ by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_def])
from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
by (simp add: dist_def)}
ultimately have "dist (?g x) (?g y) = dist x y" by blast}
@@ -1148,4 +1148,4 @@
by (simp add: ring_simps)
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Euclidean_Space.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Euclidean_Space.thy Wed Feb 25 10:29:01 2009 +0000
@@ -8,6 +8,7 @@
theory Euclidean_Space
imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
+ Inner_Product
uses ("normarith.ML")
begin
@@ -84,7 +85,13 @@
instance by (intro_classes)
end
-text{* Also the scalar-vector multiplication. FIXME: We should unify this with the scalar multiplication in @{text real_vector} *}
+instantiation "^" :: (scaleR, type) scaleR
+begin
+definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
+instance ..
+end
+
+text{* Also the scalar-vector multiplication. *}
definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75)
where "c *s x = (\<chi> i. c * (x$i))"
@@ -118,6 +125,7 @@
[@{thm vector_add_def}, @{thm vector_mult_def},
@{thm vector_minus_def}, @{thm vector_uminus_def},
@{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def},
+ @{thm vector_scaleR_def},
@{thm Cart_lambda_beta'}, @{thm vector_scalar_mult_def}]
fun vector_arith_tac ths =
simp_tac ss1
@@ -166,9 +174,18 @@
shows "(- x)$i = - (x$i)"
using i by vector
+lemma vector_scaleR_component:
+ fixes x :: "'a::scaleR ^ 'n"
+ assumes i: "i \<in> {1 .. dimindex(UNIV :: 'n set)}"
+ shows "(scaleR r x)$i = scaleR r (x$i)"
+ using i by vector
+
lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector
-lemmas vector_component = vec_component vector_add_component vector_mult_component vector_smult_component vector_minus_component vector_uminus_component cond_component
+lemmas vector_component =
+ vec_component vector_add_component vector_mult_component
+ vector_smult_component vector_minus_component vector_uminus_component
+ vector_scaleR_component cond_component
subsection {* Some frequently useful arithmetic lemmas over vectors. *}
@@ -199,6 +216,9 @@
apply (intro_classes)
by (vector Cart_eq)
+instance "^" :: (real_vector, type) real_vector
+ by default (vector scaleR_left_distrib scaleR_right_distrib)+
+
instance "^" :: (semigroup_mult,type) semigroup_mult
apply (intro_classes) by (vector mult_assoc)
@@ -242,6 +262,18 @@
instance "^" :: (ring,type) ring by (intro_classes)
instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes)
instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes)
+
+instance "^" :: (ring_1,type) ring_1 ..
+
+instance "^" :: (real_algebra,type) real_algebra
+ apply intro_classes
+ apply (simp_all add: vector_scaleR_def ring_simps)
+ apply vector
+ apply vector
+ done
+
+instance "^" :: (real_algebra_1,type) real_algebra_1 ..
+
lemma of_nat_index:
"i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n"
apply (induct n)
@@ -290,8 +322,7 @@
qed
instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes
- (* FIXME!!! Why does the axclass package complain here !!*)
-(* instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes *)
+instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes
lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
by (vector mult_assoc)
@@ -314,6 +345,241 @@
apply (auto simp add: vec_def Cart_eq vec_component Cart_lambda_beta )
using dimindex_ge_1 apply auto done
+subsection {* Square root of sum of squares *}
+
+definition
+ "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)"
+
+lemma setL2_cong:
+ "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
+ unfolding setL2_def by simp
+
+lemma strong_setL2_cong:
+ "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
+ unfolding setL2_def simp_implies_def by simp
+
+lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"
+ unfolding setL2_def by simp
+
+lemma setL2_empty [simp]: "setL2 f {} = 0"
+ unfolding setL2_def by simp
+
+lemma setL2_insert [simp]:
+ "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
+ setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)"
+ unfolding setL2_def by (simp add: setsum_nonneg)
+
+lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
+ unfolding setL2_def by (simp add: setsum_nonneg)
+
+lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
+ unfolding setL2_def by simp
+
+lemma setL2_mono:
+ assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
+ assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
+ shows "setL2 f K \<le> setL2 g K"
+ unfolding setL2_def
+ by (simp add: setsum_nonneg setsum_mono power_mono prems)
+
+lemma setL2_right_distrib:
+ "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
+ unfolding setL2_def
+ apply (simp add: power_mult_distrib)
+ apply (simp add: setsum_right_distrib [symmetric])
+ apply (simp add: real_sqrt_mult setsum_nonneg)
+ done
+
+lemma setL2_left_distrib:
+ "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
+ unfolding setL2_def
+ apply (simp add: power_mult_distrib)
+ apply (simp add: setsum_left_distrib [symmetric])
+ apply (simp add: real_sqrt_mult setsum_nonneg)
+ done
+
+lemma setsum_nonneg_eq_0_iff:
+ fixes f :: "'a \<Rightarrow> 'b::pordered_ab_group_add"
+ shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+ apply (induct set: finite, simp)
+ apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
+ done
+
+lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+ unfolding setL2_def
+ by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)
+
+lemma setL2_triangle_ineq:
+ shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
+proof (cases "finite A")
+ case False
+ thus ?thesis by simp
+next
+ case True
+ thus ?thesis
+ proof (induct set: finite)
+ case empty
+ show ?case by simp
+ next
+ case (insert x F)
+ hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le>
+ sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)"
+ by (intro real_sqrt_le_mono add_left_mono power_mono insert
+ setL2_nonneg add_increasing zero_le_power2)
+ also have
+ "\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)"
+ by (rule real_sqrt_sum_squares_triangle_ineq)
+ finally show ?case
+ using insert by simp
+ qed
+qed
+
+lemma sqrt_sum_squares_le_sum:
+ "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"
+ apply (rule power2_le_imp_le)
+ apply (simp add: power2_sum)
+ apply (simp add: mult_nonneg_nonneg)
+ apply (simp add: add_nonneg_nonneg)
+ done
+
+lemma setL2_le_setsum [rule_format]:
+ "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply simp
+ apply clarsimp
+ apply (erule order_trans [OF sqrt_sum_squares_le_sum])
+ apply simp
+ apply simp
+ apply simp
+ done
+
+lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
+ apply (rule power2_le_imp_le)
+ apply (simp add: power2_sum)
+ apply (simp add: mult_nonneg_nonneg)
+ apply (simp add: add_nonneg_nonneg)
+ done
+
+lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply simp
+ apply simp
+ apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
+ apply simp
+ apply simp
+ done
+
+lemma setL2_mult_ineq_lemma:
+ fixes a b c d :: real
+ shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
+proof -
+ have "0 \<le> (a * d - b * c)\<twosuperior>" by simp
+ also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * d) * (b * c)"
+ by (simp only: power2_diff power_mult_distrib)
+ also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * c) * (b * d)"
+ by simp
+ finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
+ by simp
+qed
+
+lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply simp
+ apply (rule power2_le_imp_le, simp)
+ apply (rule order_trans)
+ apply (rule power_mono)
+ apply (erule add_left_mono)
+ apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg)
+ apply (simp add: power2_sum)
+ apply (simp add: power_mult_distrib)
+ apply (simp add: right_distrib left_distrib)
+ apply (rule ord_le_eq_trans)
+ apply (rule setL2_mult_ineq_lemma)
+ apply simp
+ apply (intro mult_nonneg_nonneg setL2_nonneg)
+ apply simp
+ done
+
+lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
+ apply (rule_tac s="insert i (A - {i})" and t="A" in subst)
+ apply fast
+ apply (subst setL2_insert)
+ apply simp
+ apply simp
+ apply simp
+ done
+
+subsection {* Norms *}
+
+instantiation "^" :: (real_normed_vector, type) real_normed_vector
+begin
+
+definition vector_norm_def:
+ "norm (x::'a^'b) = setL2 (\<lambda>i. norm (x$i)) {1 .. dimindex (UNIV:: 'b set)}"
+
+definition vector_sgn_def:
+ "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
+
+instance proof
+ fix a :: real and x y :: "'a ^ 'b"
+ show "0 \<le> norm x"
+ unfolding vector_norm_def
+ by (rule setL2_nonneg)
+ show "norm x = 0 \<longleftrightarrow> x = 0"
+ unfolding vector_norm_def
+ by (simp add: setL2_eq_0_iff Cart_eq)
+ show "norm (x + y) \<le> norm x + norm y"
+ unfolding vector_norm_def
+ apply (rule order_trans [OF _ setL2_triangle_ineq])
+ apply (rule setL2_mono)
+ apply (simp add: vector_component norm_triangle_ineq)
+ apply simp
+ done
+ show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
+ unfolding vector_norm_def
+ by (simp add: vector_component norm_scaleR setL2_right_distrib
+ cong: strong_setL2_cong)
+ show "sgn x = scaleR (inverse (norm x)) x"
+ by (rule vector_sgn_def)
+qed
+
+end
+
+subsection {* Inner products *}
+
+instantiation "^" :: (real_inner, type) real_inner
+begin
+
+definition vector_inner_def:
+ "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) {1 .. dimindex(UNIV::'b set)}"
+
+instance proof
+ fix r :: real and x y z :: "'a ^ 'b"
+ show "inner x y = inner y x"
+ unfolding vector_inner_def
+ by (simp add: inner_commute)
+ show "inner (x + y) z = inner x z + inner y z"
+ unfolding vector_inner_def
+ by (vector inner_left_distrib)
+ show "inner (scaleR r x) y = r * inner x y"
+ unfolding vector_inner_def
+ by (vector inner_scaleR_left)
+ show "0 \<le> inner x x"
+ unfolding vector_inner_def
+ by (simp add: setsum_nonneg)
+ show "inner x x = 0 \<longleftrightarrow> x = 0"
+ unfolding vector_inner_def
+ by (simp add: Cart_eq setsum_nonneg_eq_0_iff)
+ show "norm x = sqrt (inner x x)"
+ unfolding vector_inner_def vector_norm_def setL2_def
+ by (simp add: power2_norm_eq_inner)
+qed
+
+end
+
subsection{* Properties of the dot product. *}
lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"
@@ -363,18 +629,7 @@
lemma dot_pos_lt: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
by (auto simp add: le_less)
-subsection {* Introduce norms, but defer many properties till we get square roots. *}
-text{* FIXME : This is ugly *}
-defs (overloaded)
- real_of_real_def [code inline, simp]: "real == id"
-
-instantiation "^" :: ("{times, comm_monoid_add}", type) norm begin
-definition real_vector_norm_def: "norm \<equiv> (\<lambda>x. sqrt (real (x \<bullet> x)))"
-instance ..
-end
-
-
-subsection{* The collapse of the general concepts to dimention one. *}
+subsection{* The collapse of the general concepts to dimension one. *}
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
by (vector dimindex_def)
@@ -385,11 +640,15 @@
apply (simp only: vector_one[symmetric])
done
+lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
+ by (simp add: vector_norm_def dimindex_def)
+
lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
- by (simp add: real_vector_norm_def)
+ by (simp add: norm_vector_1)
text{* Metric *}
+text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *}
definition dist:: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real" where
"dist x y = norm (x - y)"
@@ -501,27 +760,18 @@
text{* Hence derive more interesting properties of the norm. *}
lemma norm_0: "norm (0::real ^ 'n) = 0"
- by (simp add: real_vector_norm_def dot_eq_0)
-
-lemma norm_pos_le: "0 <= norm (x::real^'n)"
- by (simp add: real_vector_norm_def dot_pos_le)
-lemma norm_neg: " norm(-x) = norm (x:: real ^ 'n)"
- by (simp add: real_vector_norm_def dot_lneg dot_rneg)
-lemma norm_sub: "norm(x - y) = norm(y - (x::real ^ 'n))"
- by (metis norm_neg minus_diff_eq)
+ by (rule norm_zero)
+
lemma norm_mul: "norm(a *s x) = abs(a) * norm x"
- by (simp add: real_vector_norm_def dot_lmult dot_rmult mult_assoc[symmetric] real_sqrt_mult)
+ by (simp add: vector_norm_def vector_component setL2_right_distrib
+ abs_mult cong: strong_setL2_cong)
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))"
+ by (simp add: vector_norm_def dot_def setL2_def power2_eq_square)
+lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"
+ by (simp add: vector_norm_def setL2_def dot_def power2_eq_square)
+lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
by (simp add: real_vector_norm_def)
-lemma norm_eq_0: "norm x = 0 \<longleftrightarrow> x = (0::real ^ 'n)"
- by (simp add: real_vector_norm_def dot_eq_0)
-lemma norm_pos_lt: "0 < norm x \<longleftrightarrow> x \<noteq> (0::real ^ 'n)"
- by (metis less_le real_vector_norm_def norm_pos_le norm_eq_0)
-lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
- by (simp add: real_vector_norm_def dot_pos_le)
-lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_0)
-lemma norm_le_0: "norm x <= 0 \<longleftrightarrow> x = (0::real ^'n)"
- by (metis norm_eq_0 norm_pos_le order_antisym)
+lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
lemma vector_mul_eq_0: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
by vector
lemma vector_mul_lcancel: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
@@ -535,14 +785,14 @@
lemma norm_cauchy_schwarz: "x \<bullet> y <= norm x * norm y"
proof-
{assume "norm x = 0"
- hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
+ hence ?thesis by (simp add: dot_lzero dot_rzero)}
moreover
{assume "norm y = 0"
- hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
+ hence ?thesis by (simp add: dot_lzero dot_rzero)}
moreover
{assume h: "norm x \<noteq> 0" "norm y \<noteq> 0"
let ?z = "norm y *s x - norm x *s y"
- from h have p: "norm x * norm y > 0" by (metis norm_pos_le le_less zero_compare_simps)
+ from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps)
from dot_pos_le[of ?z]
have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2"
apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps)
@@ -553,26 +803,16 @@
ultimately show ?thesis by metis
qed
-lemma norm_abs[simp]: "abs (norm x) = norm (x::real ^'n)"
- using norm_pos_le[of x] by (simp add: real_abs_def linorder_linear)
-
lemma norm_cauchy_schwarz_abs: "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"
using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]
- by (simp add: real_abs_def dot_rneg norm_neg)
-lemma norm_triangle: "norm(x + y) <= norm x + norm (y::real ^'n)"
- unfolding real_vector_norm_def
- apply (rule real_le_lsqrt)
- apply (auto simp add: dot_pos_le real_vector_norm_def[symmetric] norm_pos_le norm_pow_2[symmetric] intro: add_nonneg_nonneg)[1]
- apply (auto simp add: dot_pos_le real_vector_norm_def[symmetric] norm_pos_le norm_pow_2[symmetric] intro: add_nonneg_nonneg)[1]
- apply (simp add: dot_ladd dot_radd dot_sym )
- by (simp add: norm_pow_2[symmetric] power2_eq_square ring_simps norm_cauchy_schwarz)
+ by (simp add: real_abs_def dot_rneg)
lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x - y)"
- using norm_triangle[of "y" "x - y"] by (simp add: ring_simps)
+ using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)
lemma norm_triangle_le: "norm(x::real ^'n) + norm y <= e ==> norm(x + y) <= e"
- by (metis order_trans norm_triangle)
+ by (metis order_trans norm_triangle_ineq)
lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e"
- by (metis basic_trans_rules(21) norm_triangle)
+ by (metis basic_trans_rules(21) norm_triangle_ineq)
lemma setsum_delta:
assumes fS: "finite S"
@@ -597,19 +837,10 @@
qed
lemma component_le_norm: "i \<in> {1 .. dimindex(UNIV :: 'n set)} ==> \<bar>x$i\<bar> <= norm (x::real ^ 'n)"
-proof(simp add: real_vector_norm_def, rule real_le_rsqrt, clarsimp)
- assume i: "Suc 0 \<le> i" "i \<le> dimindex (UNIV :: 'n set)"
- let ?S = "{1 .. dimindex(UNIV :: 'n set)}"
- let ?f = "(\<lambda>k. if k = i then x$i ^2 else 0)"
- have fS: "finite ?S" by simp
- from i setsum_delta[OF fS, of i "\<lambda>k. x$i ^ 2"]
- have th: "x$i^2 = setsum ?f ?S" by simp
- let ?g = "\<lambda>k. x$k * x$k"
- {fix x assume x: "x \<in> ?S" have "?f x \<le> ?g x" by (simp add: power2_eq_square)}
- with setsum_mono[of ?S ?f ?g]
- have "setsum ?f ?S \<le> setsum ?g ?S" by blast
- then show "x$i ^2 \<le> x \<bullet> (x:: real ^ 'n)" unfolding dot_def th[symmetric] .
-qed
+ apply (simp add: vector_norm_def)
+ apply (rule member_le_setL2, simp_all)
+ done
+
lemma norm_bound_component_le: "norm(x::real ^ 'n) <= e
==> \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. \<bar>x$i\<bar> <= e"
by (metis component_le_norm order_trans)
@@ -619,24 +850,12 @@
by (metis component_le_norm basic_trans_rules(21))
lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\<lambda>i. \<bar>x$i\<bar>) {1..dimindex(UNIV::'n set)}"
-proof (simp add: real_vector_norm_def, rule real_le_lsqrt,simp add: dot_pos_le, simp add: setsum_mono, simp add: dot_def, induct "dimindex(UNIV::'n set)")
- case 0 thus ?case by simp
-next
- case (Suc n)
- have th: "2 * (\<bar>x$(Suc n)\<bar> * (\<Sum>i = Suc 0..n. \<bar>x$i\<bar>)) \<ge> 0"
- apply simp
- apply (rule mult_nonneg_nonneg)
- by (simp_all add: setsum_abs_ge_zero)
-
- from Suc
- show ?case using th by (simp add: power2_eq_square ring_simps)
-qed
+ by (simp add: vector_norm_def setL2_le_setsum)
lemma real_abs_norm: "\<bar> norm x\<bar> = norm (x :: real ^'n)"
- by (simp add: norm_pos_le)
+ by (rule abs_norm_cancel)
lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n) - norm y\<bar> <= norm(x - y)"
- apply (simp add: abs_le_iff ring_simps)
- by (metis norm_triangle_sub norm_sub)
+ by (rule norm_triangle_ineq3)
lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
by (simp add: real_vector_norm_def)
lemma norm_lt: "norm(x::real ^'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
@@ -652,13 +871,7 @@
by (simp add: real_vector_norm_def dot_pos_le )
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
-proof-
- have th: "\<And>x y::real. x^2 = y^2 \<longleftrightarrow> x = y \<or> x = -y" by algebra
- show ?thesis using norm_pos_le[of x]
- apply (simp add: dot_square_norm th)
- apply arith
- done
-qed
+ by (auto simp add: real_vector_norm_def)
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
proof-
@@ -668,14 +881,14 @@
qed
lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
- using norm_pos_le[of x]
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
+ using norm_ge_zero[of x]
apply arith
done
lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"
- using norm_pos_le[of x]
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
+ using norm_ge_zero[of x]
apply arith
done
@@ -746,14 +959,14 @@
lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector
lemma norm_imp_pos_and_ge: "norm (x::real ^ 'n) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
- by (atomize) (auto simp add: norm_pos_le)
+ by (atomize) (auto simp add: norm_ge_zero)
lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
lemma norm_pths:
"(x::real ^'n) = y \<longleftrightarrow> norm (x - y) \<le> 0"
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
- using norm_pos_le[of "x - y"] by (auto simp add: norm_0 norm_eq_0)
+ using norm_ge_zero[of "x - y"] by auto
use "normarith.ML"
@@ -797,11 +1010,6 @@
lemma dist_le_0: "dist x y <= 0 \<longleftrightarrow> x = y" by norm
-instantiation "^" :: (monoid_add,type) monoid_add
-begin
- instance by (intro_classes)
-end
-
lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)"
apply vector
apply auto
@@ -873,7 +1081,7 @@
assumes fS: "finite S"
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
proof(induct rule: finite_induct[OF fS])
- case 1 thus ?case by (simp add: norm_zero)
+ case 1 thus ?case by simp
next
case (2 x S)
from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)
@@ -887,10 +1095,10 @@
assumes fS: "finite S"
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
proof(induct rule: finite_induct[OF fS])
- case 1 thus ?case by simp norm
+ case 1 thus ?case by simp
next
case (2 x S)
- from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" apply (simp add: norm_triangle_ineq) by norm
+ from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)
also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S"
using "2.hyps" by simp
finally show ?case using "2.hyps" by simp
@@ -936,45 +1144,6 @@
using real_setsum_norm_le[OF fS K] setsum_constant[symmetric]
by simp
-instantiation "^" :: ("{scaleR, one, times}",type) scaleR
-begin
-
-definition vector_scaleR_def: "(scaleR :: real \<Rightarrow> 'a ^'b \<Rightarrow> 'a ^'b) \<equiv> (\<lambda> c x . (scaleR c 1) *s x)"
-instance ..
-end
-
-instantiation "^" :: ("ring_1",type) ring_1
-begin
-instance by intro_classes
-end
-
-instantiation "^" :: (real_algebra_1,type) real_vector
-begin
-
-instance
- apply intro_classes
- apply (simp_all add: vector_scaleR_def)
- apply (simp_all add: vector_sadd_rdistrib vector_add_ldistrib vector_smult_lid vector_smult_assoc scaleR_left_distrib mult_commute)
- done
-end
-
-instantiation "^" :: (real_algebra_1,type) real_algebra
-begin
-
-instance
- apply intro_classes
- apply (simp_all add: vector_scaleR_def ring_simps)
- apply vector
- apply vector
- done
-end
-
-instantiation "^" :: (real_algebra_1,type) real_algebra_1
-begin
-
-instance ..
-end
-
lemma setsum_vmul:
fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector,semiring, mult_zero}"
assumes fS: "finite S"
@@ -1211,7 +1380,7 @@
by (auto simp add: setsum_component intro: abs_le_D1)
have Pne: "setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn \<le> e"
using i component_le_norm[OF i, of "setsum (\<lambda>x. - f x) ?Pn"] fPs[OF PnP]
- by (auto simp add: setsum_negf norm_neg setsum_component vector_component intro: abs_le_D1)
+ by (auto simp add: setsum_negf setsum_component vector_component intro: abs_le_D1)
have "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn"
apply (subst thp)
apply (rule setsum_Un_nonzero)
@@ -1535,7 +1704,7 @@
unfolding norm_mul
apply (simp only: mult_commute)
apply (rule mult_mono)
- by (auto simp add: ring_simps norm_pos_le) }
+ by (auto simp add: ring_simps norm_ge_zero) }
then have th: "\<forall>i\<in> ?S. norm ((x$i) *s f (basis i :: real ^'m)) \<le> norm (f (basis i)) * norm x" by metis
from real_setsum_norm_le[OF fS, of "\<lambda>i. (x$i) *s (f (basis i))", OF th]
have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}
@@ -1552,16 +1721,18 @@
let ?K = "\<bar>B\<bar> + 1"
have Kp: "?K > 0" by arith
{assume C: "B < 0"
- have "norm (1::real ^ 'n) > 0" by (simp add: norm_pos_lt)
+ have "norm (1::real ^ 'n) > 0" by (simp add: zero_less_norm_iff)
with C have "B * norm (1:: real ^ 'n) < 0"
by (simp add: zero_compare_simps)
- with B[rule_format, of 1] norm_pos_le[of "f 1"] have False by simp
+ with B[rule_format, of 1] norm_ge_zero[of "f 1"] have False by simp
}
then have Bp: "B \<ge> 0" by ferrack
{fix x::"real ^ 'n"
have "norm (f x) \<le> ?K * norm x"
- using B[rule_format, of x] norm_pos_le[of x] norm_pos_le[of "f x"] Bp
- by (auto simp add: ring_simps split add: abs_split)
+ using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
+ apply (auto simp add: ring_simps split add: abs_split)
+ apply (erule order_trans, simp)
+ done
}
then show ?thesis using Kp by blast
qed
@@ -1641,9 +1812,9 @@
apply simp
apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] norm_mul ring_simps)
apply (rule mult_mono)
- apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
+ apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
apply (rule mult_mono)
- apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
+ apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
done}
then show ?thesis by metis
qed
@@ -1663,7 +1834,7 @@
have "B * norm x * norm y \<le> ?K * norm x * norm y"
apply -
apply (rule mult_right_mono, rule mult_right_mono)
- by (auto simp add: norm_pos_le)
+ by (auto simp add: norm_ge_zero)
then have "norm (h x y) \<le> ?K * norm x * norm y"
using B[rule_format, of x y] by simp}
with Kp show ?thesis by blast
@@ -2276,21 +2447,21 @@
moreover
{assume H: ?lhs
from H[rule_format, of "basis 1"]
- have bp: "b \<ge> 0" using norm_pos_le[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
- by (auto simp add: norm_basis)
+ have bp: "b \<ge> 0" using norm_ge_zero[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
+ by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero])
{fix x :: "real ^'n"
{assume "x = 0"
- then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] norm_0 bp)}
+ then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)}
moreover
{assume x0: "x \<noteq> 0"
- hence n0: "norm x \<noteq> 0" by (metis norm_eq_0)
+ hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
let ?c = "1/ norm x"
- have "norm (?c*s x) = 1" by (simp add: n0 norm_mul)
+ have "norm (?c*s x) = 1" using x0 by (simp add: n0 norm_mul)
with H have "norm (f(?c*s x)) \<le> b" by blast
hence "?c * norm (f x) \<le> b"
by (simp add: linear_cmul[OF lf] norm_mul)
hence "norm (f x) \<le> b * norm x"
- using n0 norm_pos_le[of x] by (auto simp add: field_simps)}
+ using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}
ultimately have "norm (f x) \<le> b * norm x" by blast}
then have ?rhs by blast}
ultimately show ?thesis by blast
@@ -2322,12 +2493,12 @@
qed
lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" shows "0 <= onorm f"
- using order_trans[OF norm_pos_le onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
+ using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)"
shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
using onorm[OF lf]
- apply (auto simp add: norm_0 onorm_pos_le norm_le_0)
+ apply (auto simp add: onorm_pos_le)
apply atomize
apply (erule allE[where x="0::real"])
using onorm_pos_le[OF lf]
@@ -2365,7 +2536,7 @@
lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
shows "onorm (\<lambda>x. - f x) \<le> onorm f"
using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
- unfolding norm_neg by metis
+ unfolding norm_minus_cancel by metis
lemma onorm_neg: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
shows "onorm (\<lambda>x. - f x) = onorm f"
@@ -2377,7 +2548,7 @@
shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"
apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
apply (rule order_trans)
- apply (rule norm_triangle)
+ apply (rule norm_triangle_ineq)
apply (simp add: distrib)
apply (rule add_mono)
apply (rule onorm(1)[OF lf])
@@ -2594,7 +2765,7 @@
by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square del: One_nat_def)
then show ?thesis
unfolding th0
- unfolding real_vector_norm_def real_sqrt_le_iff real_of_real_def id_def
+ unfolding real_vector_norm_def real_sqrt_le_iff id_def
by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)
qed
@@ -2626,7 +2797,7 @@
by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square setsum_reindex[OF finj, unfolded fS] del: One_nat_def)
then show ?thesis
unfolding th0
- unfolding real_vector_norm_def real_sqrt_le_iff real_of_real_def id_def
+ unfolding real_vector_norm_def real_sqrt_le_iff id_def
by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)
qed
@@ -2683,7 +2854,7 @@
qed
lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ _) + norm(y)"
- unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff real_of_real_def id_def
+ unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff id_def
apply (rule power2_le_imp_le)
apply (simp add: real_sqrt_pow2[OF add_nonneg_nonneg[OF dot_pos_le[of x] dot_pos_le[of y]]])
apply (auto simp add: power2_eq_square ring_simps)
@@ -5007,7 +5178,7 @@
apply blast
by (rule abs_ge_zero)
from real_le_lsqrt[OF dot_pos_le th th1]
- show ?thesis unfolding real_vector_norm_def real_of_real_def id_def .
+ show ?thesis unfolding real_vector_norm_def id_def .
qed
(* Equality in Cauchy-Schwarz and triangle inequalities. *)
@@ -5015,10 +5186,10 @@
lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *s y = norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
{assume h: "x = 0"
- hence ?thesis by (simp add: norm_0)}
+ hence ?thesis by simp}
moreover
{assume h: "y = 0"
- hence ?thesis by (simp add: norm_0)}
+ hence ?thesis by simp}
moreover
{assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
from dot_eq_0[of "norm y *s x - norm x *s y"]
@@ -5032,7 +5203,7 @@
also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
by (simp add: ring_simps dot_sym)
also have "\<dots> \<longleftrightarrow> ?lhs" using x y
- apply (simp add: norm_eq_0)
+ apply simp
by metis
finally have ?thesis by blast}
ultimately show ?thesis by blast
@@ -5043,14 +5214,14 @@
proof-
have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> abs x = a \<longleftrightarrow> x = a \<or> x = - a" by arith
have "?rhs \<longleftrightarrow> norm x *s y = norm y *s x \<or> norm (- x) *s y = norm y *s (- x)"
- apply (simp add: norm_neg) by vector
+ apply simp by vector
also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or>
(-x) \<bullet> y = norm x * norm y)"
unfolding norm_cauchy_schwarz_eq[symmetric]
- unfolding norm_neg
+ unfolding norm_minus_cancel
norm_mul by blast
also have "\<dots> \<longleftrightarrow> ?lhs"
- unfolding th[OF mult_nonneg_nonneg, OF norm_pos_le[of x] norm_pos_le[of y]] dot_lneg
+ unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] dot_lneg
by arith
finally show ?thesis ..
qed
@@ -5058,17 +5229,17 @@
lemma norm_triangle_eq: "norm(x + y) = norm x + norm y \<longleftrightarrow> norm x *s y = norm y *s x"
proof-
{assume x: "x =0 \<or> y =0"
- hence ?thesis by (cases "x=0", simp_all add: norm_0)}
+ hence ?thesis by (cases "x=0", simp_all)}
moreover
{assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
hence "norm x \<noteq> 0" "norm y \<noteq> 0"
- by (simp_all add: norm_eq_0)
+ by simp_all
hence n: "norm x > 0" "norm y > 0"
- using norm_pos_le[of x] norm_pos_le[of y]
+ using norm_ge_zero[of x] norm_ge_zero[of y]
by arith+
have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a^2 = (b + c)^2)" by algebra
have "norm(x + y) = norm x + norm y \<longleftrightarrow> norm(x + y)^ 2 = (norm x + norm y) ^2"
- apply (rule th) using n norm_pos_le[of "x + y"]
+ apply (rule th) using n norm_ge_zero[of "x + y"]
by arith
also have "\<dots> \<longleftrightarrow> norm x *s y = norm y *s x"
unfolding norm_cauchy_schwarz_eq[symmetric]
@@ -5138,8 +5309,8 @@
lemma norm_cauchy_schwarz_equal: "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow> collinear {(0::real^'n),x,y}"
unfolding norm_cauchy_schwarz_abs_eq
-apply (cases "x=0", simp_all add: collinear_2 norm_0)
-apply (cases "y=0", simp_all add: collinear_2 norm_0 insert_commute)
+apply (cases "x=0", simp_all add: collinear_2)
+apply (cases "y=0", simp_all add: collinear_2 insert_commute)
unfolding collinear_lemma
apply simp
apply (subgoal_tac "norm x \<noteq> 0")
@@ -5164,8 +5335,8 @@
apply (simp add: ring_simps)
apply (case_tac "c <= 0", simp add: ring_simps)
apply (simp add: ring_simps)
-apply (simp add: norm_eq_0)
-apply (simp add: norm_eq_0)
+apply simp
+apply simp
done
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Float.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Float.thy Wed Feb 25 10:29:01 2009 +0000
@@ -795,7 +795,7 @@
have "x \<noteq> y"
proof (rule ccontr)
assume "\<not> x \<noteq> y" hence "x = y" by auto
- have "?X mod y = 0" unfolding `x = y` using zmod_zmult_self2 by auto
+ have "?X mod y = 0" unfolding `x = y` using mod_mult_self1_is_0 by auto
thus False using False by auto
qed
hence "x < y" using `x \<le> y` by auto
--- a/src/HOL/Library/Inner_Product.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Inner_Product.thy Wed Feb 25 10:29:01 2009 +0000
@@ -21,19 +21,10 @@
begin
lemma inner_zero_left [simp]: "inner 0 x = 0"
-proof -
- have "inner 0 x = inner (0 + 0) x" by simp
- also have "\<dots> = inner 0 x + inner 0 x" by (rule inner_left_distrib)
- finally show "inner 0 x = 0" by simp
-qed
+ using inner_left_distrib [of 0 0 x] by simp
lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
-proof -
- have "inner (- x) y + inner x y = inner (- x + x) y"
- by (rule inner_left_distrib [symmetric])
- also have "\<dots> = - inner x y + inner x y" by simp
- finally show "inner (- x) y = - inner x y" by simp
-qed
+ using inner_left_distrib [of x "- x" y] by simp
lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
by (simp add: diff_minus inner_left_distrib)
@@ -65,7 +56,7 @@
lemma power2_norm_eq_inner: "(norm x)\<twosuperior> = inner x x"
by (simp add: norm_eq_sqrt_inner)
-lemma Cauchy_Schwartz_ineq:
+lemma Cauchy_Schwarz_ineq:
"(inner x y)\<twosuperior> \<le> inner x x * inner y y"
proof (cases)
assume "y = 0"
@@ -86,11 +77,11 @@
by (simp add: pos_divide_le_eq y)
qed
-lemma Cauchy_Schwartz_ineq2:
+lemma Cauchy_Schwarz_ineq2:
"\<bar>inner x y\<bar> \<le> norm x * norm y"
proof (rule power2_le_imp_le)
have "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
- using Cauchy_Schwartz_ineq .
+ using Cauchy_Schwarz_ineq .
thus "\<bar>inner x y\<bar>\<twosuperior> \<le> (norm x * norm y)\<twosuperior>"
by (simp add: power_mult_distrib power2_norm_eq_inner)
show "0 \<le> norm x * norm y"
@@ -108,7 +99,7 @@
show "norm (x + y) \<le> norm x + norm y"
proof (rule power2_le_imp_le)
have "inner x y \<le> norm x * norm y"
- by (rule order_trans [OF abs_ge_self Cauchy_Schwartz_ineq2])
+ by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])
thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>"
unfolding power2_sum power2_norm_eq_inner
by (simp add: inner_distrib inner_commute)
@@ -140,7 +131,7 @@
show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
proof
show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
- by (simp add: Cauchy_Schwartz_ineq2)
+ by (simp add: Cauchy_Schwarz_ineq2)
qed
qed
--- a/src/HOL/Library/Library.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Library.thy Wed Feb 25 10:29:01 2009 +0000
@@ -41,6 +41,7 @@
Poly_Deriv
Polynomial
Primes
+ Product_Vector
Quickcheck
Quicksort
Quotient
--- a/src/HOL/Library/Numeral_Type.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Numeral_Type.thy Wed Feb 25 10:29:01 2009 +0000
@@ -267,6 +267,22 @@
subsection {* Number ring instances *}
+text {*
+ Unfortunately a number ring instance is not possible for
+ @{typ num1}, since 0 and 1 are not distinct.
+*}
+
+instantiation num1 :: "{comm_ring,comm_monoid_mult,number,recpower}"
+begin
+
+lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
+ by (induct x, induct y) simp
+
+instance proof
+qed (simp_all add: num1_eq_iff)
+
+end
+
instantiation
bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}"
begin
--- a/src/HOL/Library/Permutations.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Permutations.thy Wed Feb 25 10:29:01 2009 +0000
@@ -6,7 +6,7 @@
header {* Permutations, both general and specifically on finite sets.*}
theory Permutations
-imports Main Finite_Cartesian_Product Parity
+imports Main Finite_Cartesian_Product Parity Fact
begin
(* Why should I import Main just to solve the Typerep problem! *)
@@ -683,13 +683,13 @@
(* ------------------------------------------------------------------------- *)
lemma permutes_natset_le:
- assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S. p i <= i" shows "p = id"
+ assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S. p i <= i" shows "p = id"
proof-
{fix n
have "p n = n"
using p le
- proof(induct n arbitrary: S rule: nat_less_induct)
- fix n S assume H: "\<forall> m< n. \<forall>S. p permutes S \<longrightarrow> (\<forall>i\<in>S. p i \<le> i) \<longrightarrow> p m = m"
+ proof(induct n arbitrary: S rule: less_induct)
+ fix n S assume H: "\<And>m S. \<lbrakk>m < n; p permutes S; \<forall>i\<in>S. p i \<le> i\<rbrakk> \<Longrightarrow> p m = m"
"p permutes S" "\<forall>i \<in>S. p i \<le> i"
{assume "n \<notin> S"
with H(2) have "p n = n" unfolding permutes_def by metis}
@@ -699,7 +699,7 @@
moreover{assume h: "p n < n"
from H h have "p (p n) = p n" by metis
with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast
- with h have False by arith}
+ with h have False by simp}
ultimately have "p n = n" by blast }
ultimately show "p n = n" by blast
qed}
@@ -707,7 +707,7 @@
qed
lemma permutes_natset_ge:
- assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S. p i \<ge> i" shows "p = id"
+ assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S. p i \<ge> i" shows "p = id"
proof-
{fix i assume i: "i \<in> S"
from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S" by simp
@@ -757,13 +757,13 @@
done
term setsum
-lemma setsum_permutations_inverse: "setsum f {p. p permutes {m..n}} = setsum (\<lambda>p. f(inv p)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
+lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs")
proof-
- let ?S = "{p . p permutes {m .. n}}"
+ let ?S = "{p . p permutes S}"
have th0: "inj_on inv ?S"
proof(auto simp add: inj_on_def)
fix q r
- assume q: "q permutes {m .. n}" and r: "r permutes {m .. n}" and qr: "inv q = inv r"
+ assume q: "q permutes S" and r: "r permutes S" and qr: "inv q = inv r"
hence "inv (inv q) = inv (inv r)" by simp
with permutes_inv_inv[OF q] permutes_inv_inv[OF r]
show "q = r" by metis
@@ -774,17 +774,17 @@
qed
lemma setum_permutations_compose_left:
- assumes q: "q permutes {m..n}"
- shows "setsum f {p. p permutes {m..n}} =
- setsum (\<lambda>p. f(q o p)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
+ assumes q: "q permutes S"
+ shows "setsum f {p. p permutes S} =
+ setsum (\<lambda>p. f(q o p)) {p. p permutes S}" (is "?lhs = ?rhs")
proof-
- let ?S = "{p. p permutes {m..n}}"
+ let ?S = "{p. p permutes S}"
have th0: "?rhs = setsum (f o (op o q)) ?S" by (simp add: o_def)
have th1: "inj_on (op o q) ?S"
apply (auto simp add: inj_on_def)
proof-
fix p r
- assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "q \<circ> p = q \<circ> r"
+ assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r"
hence "inv q o q o p = inv q o q o r" by (simp add: o_assoc[symmetric])
with permutes_inj[OF q, unfolded inj_iff]
@@ -796,17 +796,17 @@
qed
lemma sum_permutations_compose_right:
- assumes q: "q permutes {m..n}"
- shows "setsum f {p. p permutes {m..n}} =
- setsum (\<lambda>p. f(p o q)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
+ assumes q: "q permutes S"
+ shows "setsum f {p. p permutes S} =
+ setsum (\<lambda>p. f(p o q)) {p. p permutes S}" (is "?lhs = ?rhs")
proof-
- let ?S = "{p. p permutes {m..n}}"
+ let ?S = "{p. p permutes S}"
have th0: "?rhs = setsum (f o (\<lambda>p. p o q)) ?S" by (simp add: o_def)
have th1: "inj_on (\<lambda>p. p o q) ?S"
apply (auto simp add: inj_on_def)
proof-
fix p r
- assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "p o q = r o q"
+ assume "p permutes S" and r:"r permutes S" and rp: "p o q = r o q"
hence "p o (q o inv q) = r o (q o inv q)" by (simp add: o_assoc)
with permutes_surj[OF q, unfolded surj_iff]
--- a/src/HOL/Library/Pocklington.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Pocklington.thy Wed Feb 25 10:29:01 2009 +0000
@@ -873,7 +873,7 @@
from lh[unfolded nat_mod]
obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" by blast
hence "a ^ d + n * q1 - n * q2 = 1" by simp
- with dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp
+ with nat_dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp
with p(3) have False by simp
hence ?rhs ..}
ultimately have ?rhs by blast}
--- a/src/HOL/Library/Polynomial.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Polynomial.thy Wed Feb 25 10:29:01 2009 +0000
@@ -1020,6 +1020,16 @@
lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
+lemma poly_div_minus_left [simp]:
+ fixes x y :: "'a::field poly"
+ shows "(- x) div y = - (x div y)"
+ using div_smult_left [of "- 1::'a"] by simp
+
+lemma poly_mod_minus_left [simp]:
+ fixes x y :: "'a::field poly"
+ shows "(- x) mod y = - (x mod y)"
+ using mod_smult_left [of "- 1::'a"] by simp
+
lemma pdivmod_rel_smult_right:
"\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
\<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
@@ -1032,6 +1042,17 @@
lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
+lemma poly_div_minus_right [simp]:
+ fixes x y :: "'a::field poly"
+ shows "x div (- y) = - (x div y)"
+ using div_smult_right [of "- 1::'a"]
+ by (simp add: nonzero_inverse_minus_eq)
+
+lemma poly_mod_minus_right [simp]:
+ fixes x y :: "'a::field poly"
+ shows "x mod (- y) = x mod y"
+ using mod_smult_right [of "- 1::'a"] by simp
+
lemma pdivmod_rel_mult:
"\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
\<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"
--- a/src/HOL/Library/Primes.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Library/Primes.thy Wed Feb 25 10:29:01 2009 +0000
@@ -45,12 +45,14 @@
by (rule prime_dvd_square) (simp_all add: power2_eq_square)
-lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0" by (induct n, auto)
+lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0"
+by (induct n, auto)
+
lemma exp_mono_lt: "(x::nat) ^ (Suc n) < y ^ (Suc n) \<longleftrightarrow> x < y"
- using power_less_imp_less_base[of x "Suc n" y] power_strict_mono[of x y "Suc n"]
- by auto
+by(metis linorder_not_less not_less0 power_le_imp_le_base power_less_imp_less_base)
+
lemma exp_mono_le: "(x::nat) ^ (Suc n) \<le> y ^ (Suc n) \<longleftrightarrow> x \<le> y"
- by (simp only: linorder_not_less[symmetric] exp_mono_lt)
+by (simp only: linorder_not_less[symmetric] exp_mono_lt)
lemma exp_mono_eq: "(x::nat) ^ Suc n = y ^ Suc n \<longleftrightarrow> x = y"
using power_inject_base[of x n y] by auto
@@ -307,8 +309,8 @@
{fix e assume H: "e dvd a^n" "e dvd b^n"
from bezout_gcd_pow[of a n b] obtain x y
where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast
- from dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
- dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
+ from nat_dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
+ nat_dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd a b ^ n", simp_all)}
hence th: "\<forall>e. e dvd a^n \<and> e dvd b^n \<longrightarrow> e dvd ?gn" by blast
from divides_exp[OF gcd_dvd1[of a b], of n] divides_exp[OF gcd_dvd2[of a b], of n] th
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Product_Vector.thy Wed Feb 25 10:29:01 2009 +0000
@@ -0,0 +1,273 @@
+(* Title: HOL/Library/Product_Vector.thy
+ Author: Brian Huffman
+*)
+
+header {* Cartesian Products as Vector Spaces *}
+
+theory Product_Vector
+imports Inner_Product Product_plus
+begin
+
+subsection {* Product is a real vector space *}
+
+instantiation "*" :: (real_vector, real_vector) real_vector
+begin
+
+definition scaleR_prod_def:
+ "scaleR r A = (scaleR r (fst A), scaleR r (snd A))"
+
+lemma fst_scaleR [simp]: "fst (scaleR r A) = scaleR r (fst A)"
+ unfolding scaleR_prod_def by simp
+
+lemma snd_scaleR [simp]: "snd (scaleR r A) = scaleR r (snd A)"
+ unfolding scaleR_prod_def by simp
+
+lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)"
+ unfolding scaleR_prod_def by simp
+
+instance proof
+ fix a b :: real and x y :: "'a \<times> 'b"
+ show "scaleR a (x + y) = scaleR a x + scaleR a y"
+ by (simp add: expand_prod_eq scaleR_right_distrib)
+ show "scaleR (a + b) x = scaleR a x + scaleR b x"
+ by (simp add: expand_prod_eq scaleR_left_distrib)
+ show "scaleR a (scaleR b x) = scaleR (a * b) x"
+ by (simp add: expand_prod_eq)
+ show "scaleR 1 x = x"
+ by (simp add: expand_prod_eq)
+qed
+
+end
+
+subsection {* Product is a normed vector space *}
+
+instantiation
+ "*" :: (real_normed_vector, real_normed_vector) real_normed_vector
+begin
+
+definition norm_prod_def:
+ "norm x = sqrt ((norm (fst x))\<twosuperior> + (norm (snd x))\<twosuperior>)"
+
+definition sgn_prod_def:
+ "sgn (x::'a \<times> 'b) = scaleR (inverse (norm x)) x"
+
+lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<twosuperior> + (norm b)\<twosuperior>)"
+ unfolding norm_prod_def by simp
+
+instance proof
+ fix r :: real and x y :: "'a \<times> 'b"
+ show "0 \<le> norm x"
+ unfolding norm_prod_def by simp
+ show "norm x = 0 \<longleftrightarrow> x = 0"
+ unfolding norm_prod_def
+ by (simp add: expand_prod_eq)
+ show "norm (x + y) \<le> norm x + norm y"
+ unfolding norm_prod_def
+ apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
+ apply (simp add: add_mono power_mono norm_triangle_ineq)
+ done
+ show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
+ unfolding norm_prod_def
+ apply (simp add: norm_scaleR power_mult_distrib)
+ apply (simp add: right_distrib [symmetric])
+ apply (simp add: real_sqrt_mult_distrib)
+ done
+ show "sgn x = scaleR (inverse (norm x)) x"
+ by (rule sgn_prod_def)
+qed
+
+end
+
+subsection {* Product is an inner product space *}
+
+instantiation "*" :: (real_inner, real_inner) real_inner
+begin
+
+definition inner_prod_def:
+ "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"
+
+lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
+ unfolding inner_prod_def by simp
+
+instance proof
+ fix r :: real
+ fix x y z :: "'a::real_inner * 'b::real_inner"
+ show "inner x y = inner y x"
+ unfolding inner_prod_def
+ by (simp add: inner_commute)
+ show "inner (x + y) z = inner x z + inner y z"
+ unfolding inner_prod_def
+ by (simp add: inner_left_distrib)
+ show "inner (scaleR r x) y = r * inner x y"
+ unfolding inner_prod_def
+ by (simp add: inner_scaleR_left right_distrib)
+ show "0 \<le> inner x x"
+ unfolding inner_prod_def
+ by (intro add_nonneg_nonneg inner_ge_zero)
+ show "inner x x = 0 \<longleftrightarrow> x = 0"
+ unfolding inner_prod_def expand_prod_eq
+ by (simp add: add_nonneg_eq_0_iff)
+ show "norm x = sqrt (inner x x)"
+ unfolding norm_prod_def inner_prod_def
+ by (simp add: power2_norm_eq_inner)
+qed
+
+end
+
+subsection {* Pair operations are linear and continuous *}
+
+interpretation fst!: bounded_linear fst
+ apply (unfold_locales)
+ apply (rule fst_add)
+ apply (rule fst_scaleR)
+ apply (rule_tac x="1" in exI, simp add: norm_Pair)
+ done
+
+interpretation snd!: bounded_linear snd
+ apply (unfold_locales)
+ apply (rule snd_add)
+ apply (rule snd_scaleR)
+ apply (rule_tac x="1" in exI, simp add: norm_Pair)
+ done
+
+text {* TODO: move to NthRoot *}
+lemma sqrt_add_le_add_sqrt:
+ assumes x: "0 \<le> x" and y: "0 \<le> y"
+ shows "sqrt (x + y) \<le> sqrt x + sqrt y"
+apply (rule power2_le_imp_le)
+apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y)
+apply (simp add: mult_nonneg_nonneg x y)
+apply (simp add: add_nonneg_nonneg x y)
+done
+
+lemma bounded_linear_Pair:
+ assumes f: "bounded_linear f"
+ assumes g: "bounded_linear g"
+ shows "bounded_linear (\<lambda>x. (f x, g x))"
+proof
+ interpret f: bounded_linear f by fact
+ interpret g: bounded_linear g by fact
+ fix x y and r :: real
+ show "(f (x + y), g (x + y)) = (f x, g x) + (f y, g y)"
+ by (simp add: f.add g.add)
+ show "(f (r *\<^sub>R x), g (r *\<^sub>R x)) = r *\<^sub>R (f x, g x)"
+ by (simp add: f.scaleR g.scaleR)
+ obtain Kf where "0 < Kf" and norm_f: "\<And>x. norm (f x) \<le> norm x * Kf"
+ using f.pos_bounded by fast
+ obtain Kg where "0 < Kg" and norm_g: "\<And>x. norm (g x) \<le> norm x * Kg"
+ using g.pos_bounded by fast
+ have "\<forall>x. norm (f x, g x) \<le> norm x * (Kf + Kg)"
+ apply (rule allI)
+ apply (simp add: norm_Pair)
+ apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp)
+ apply (simp add: right_distrib)
+ apply (rule add_mono [OF norm_f norm_g])
+ done
+ then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
+qed
+
+text {*
+ TODO: The next three proofs are nearly identical to each other.
+ Is there a good way to factor out the common parts?
+*}
+
+lemma LIMSEQ_Pair:
+ assumes "X ----> a" and "Y ----> b"
+ shows "(\<lambda>n. (X n, Y n)) ----> (a, b)"
+proof (rule LIMSEQ_I)
+ fix r :: real assume "0 < r"
+ then have "0 < r / sqrt 2" (is "0 < ?s")
+ by (simp add: divide_pos_pos)
+ obtain M where M: "\<forall>n\<ge>M. norm (X n - a) < ?s"
+ using LIMSEQ_D [OF `X ----> a` `0 < ?s`] ..
+ obtain N where N: "\<forall>n\<ge>N. norm (Y n - b) < ?s"
+ using LIMSEQ_D [OF `Y ----> b` `0 < ?s`] ..
+ have "\<forall>n\<ge>max M N. norm ((X n, Y n) - (a, b)) < r"
+ using M N by (simp add: real_sqrt_sum_squares_less norm_Pair)
+ then show "\<exists>n0. \<forall>n\<ge>n0. norm ((X n, Y n) - (a, b)) < r" ..
+qed
+
+lemma Cauchy_Pair:
+ assumes "Cauchy X" and "Cauchy Y"
+ shows "Cauchy (\<lambda>n. (X n, Y n))"
+proof (rule CauchyI)
+ fix r :: real assume "0 < r"
+ then have "0 < r / sqrt 2" (is "0 < ?s")
+ by (simp add: divide_pos_pos)
+ obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < ?s"
+ using CauchyD [OF `Cauchy X` `0 < ?s`] ..
+ obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (Y m - Y n) < ?s"
+ using CauchyD [OF `Cauchy Y` `0 < ?s`] ..
+ have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. norm ((X m, Y m) - (X n, Y n)) < r"
+ using M N by (simp add: real_sqrt_sum_squares_less norm_Pair)
+ then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. norm ((X m, Y m) - (X n, Y n)) < r" ..
+qed
+
+lemma LIM_Pair:
+ assumes "f -- x --> a" and "g -- x --> b"
+ shows "(\<lambda>x. (f x, g x)) -- x --> (a, b)"
+proof (rule LIM_I)
+ fix r :: real assume "0 < r"
+ then have "0 < r / sqrt 2" (is "0 < ?e")
+ by (simp add: divide_pos_pos)
+ obtain s where s: "0 < s"
+ "\<forall>z. z \<noteq> x \<and> norm (z - x) < s \<longrightarrow> norm (f z - a) < ?e"
+ using LIM_D [OF `f -- x --> a` `0 < ?e`] by fast
+ obtain t where t: "0 < t"
+ "\<forall>z. z \<noteq> x \<and> norm (z - x) < t \<longrightarrow> norm (g z - b) < ?e"
+ using LIM_D [OF `g -- x --> b` `0 < ?e`] by fast
+ have "0 < min s t \<and>
+ (\<forall>z. z \<noteq> x \<and> norm (z - x) < min s t \<longrightarrow> norm ((f z, g z) - (a, b)) < r)"
+ using s t by (simp add: real_sqrt_sum_squares_less norm_Pair)
+ then show
+ "\<exists>s>0. \<forall>z. z \<noteq> x \<and> norm (z - x) < s \<longrightarrow> norm ((f z, g z) - (a, b)) < r" ..
+qed
+
+lemma isCont_Pair [simp]:
+ "\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x"
+ unfolding isCont_def by (rule LIM_Pair)
+
+
+subsection {* Product is a complete vector space *}
+
+instance "*" :: (banach, banach) banach
+proof
+ fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
+ have 1: "(\<lambda>n. fst (X n)) ----> lim (\<lambda>n. fst (X n))"
+ using fst.Cauchy [OF `Cauchy X`]
+ by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
+ have 2: "(\<lambda>n. snd (X n)) ----> lim (\<lambda>n. snd (X n))"
+ using snd.Cauchy [OF `Cauchy X`]
+ by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
+ have "X ----> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
+ using LIMSEQ_Pair [OF 1 2] by simp
+ then show "convergent X"
+ by (rule convergentI)
+qed
+
+subsection {* Frechet derivatives involving pairs *}
+
+lemma FDERIV_Pair:
+ assumes f: "FDERIV f x :> f'" and g: "FDERIV g x :> g'"
+ shows "FDERIV (\<lambda>x. (f x, g x)) x :> (\<lambda>h. (f' h, g' h))"
+apply (rule FDERIV_I)
+apply (rule bounded_linear_Pair)
+apply (rule FDERIV_bounded_linear [OF f])
+apply (rule FDERIV_bounded_linear [OF g])
+apply (simp add: norm_Pair)
+apply (rule real_LIM_sandwich_zero)
+apply (rule LIM_add_zero)
+apply (rule FDERIV_D [OF f])
+apply (rule FDERIV_D [OF g])
+apply (rename_tac h)
+apply (simp add: divide_nonneg_pos)
+apply (rename_tac h)
+apply (subst add_divide_distrib [symmetric])
+apply (rule divide_right_mono [OF _ norm_ge_zero])
+apply (rule order_trans [OF sqrt_add_le_add_sqrt])
+apply simp
+apply simp
+apply simp
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Product_plus.thy Wed Feb 25 10:29:01 2009 +0000
@@ -0,0 +1,115 @@
+(* Title: HOL/Library/Product_plus.thy
+ Author: Brian Huffman
+*)
+
+header {* Additive group operations on product types *}
+
+theory Product_plus
+imports Main
+begin
+
+subsection {* Operations *}
+
+instantiation "*" :: (zero, zero) zero
+begin
+
+definition zero_prod_def: "0 = (0, 0)"
+
+instance ..
+end
+
+instantiation "*" :: (plus, plus) plus
+begin
+
+definition plus_prod_def:
+ "x + y = (fst x + fst y, snd x + snd y)"
+
+instance ..
+end
+
+instantiation "*" :: (minus, minus) minus
+begin
+
+definition minus_prod_def:
+ "x - y = (fst x - fst y, snd x - snd y)"
+
+instance ..
+end
+
+instantiation "*" :: (uminus, uminus) uminus
+begin
+
+definition uminus_prod_def:
+ "- x = (- fst x, - snd x)"
+
+instance ..
+end
+
+lemma fst_zero [simp]: "fst 0 = 0"
+ unfolding zero_prod_def by simp
+
+lemma snd_zero [simp]: "snd 0 = 0"
+ unfolding zero_prod_def by simp
+
+lemma fst_add [simp]: "fst (x + y) = fst x + fst y"
+ unfolding plus_prod_def by simp
+
+lemma snd_add [simp]: "snd (x + y) = snd x + snd y"
+ unfolding plus_prod_def by simp
+
+lemma fst_diff [simp]: "fst (x - y) = fst x - fst y"
+ unfolding minus_prod_def by simp
+
+lemma snd_diff [simp]: "snd (x - y) = snd x - snd y"
+ unfolding minus_prod_def by simp
+
+lemma fst_uminus [simp]: "fst (- x) = - fst x"
+ unfolding uminus_prod_def by simp
+
+lemma snd_uminus [simp]: "snd (- x) = - snd x"
+ unfolding uminus_prod_def by simp
+
+lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)"
+ unfolding plus_prod_def by simp
+
+lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)"
+ unfolding minus_prod_def by simp
+
+lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
+ unfolding uminus_prod_def by simp
+
+lemmas expand_prod_eq = Pair_fst_snd_eq
+
+
+subsection {* Class instances *}
+
+instance "*" :: (semigroup_add, semigroup_add) semigroup_add
+ by default (simp add: expand_prod_eq add_assoc)
+
+instance "*" :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
+ by default (simp add: expand_prod_eq add_commute)
+
+instance "*" :: (monoid_add, monoid_add) monoid_add
+ by default (simp_all add: expand_prod_eq)
+
+instance "*" :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
+ by default (simp add: expand_prod_eq)
+
+instance "*" ::
+ (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
+ by default (simp_all add: expand_prod_eq)
+
+instance "*" ::
+ (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
+ by default (simp add: expand_prod_eq)
+
+instance "*" ::
+ (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
+
+instance "*" :: (group_add, group_add) group_add
+ by default (simp_all add: expand_prod_eq diff_minus)
+
+instance "*" :: (ab_group_add, ab_group_add) ab_group_add
+ by default (simp_all add: expand_prod_eq)
+
+end
--- a/src/HOL/List.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/List.thy Wed Feb 25 10:29:01 2009 +0000
@@ -1438,10 +1438,10 @@
apply (auto split:nat.split)
done
-lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
+lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - Suc 0)"
by(induct xs)(auto simp:neq_Nil_conv)
-lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
+lemma butlast_conv_take: "butlast xs = take (length xs - Suc 0) xs"
by (induct xs, simp, case_tac xs, simp_all)
@@ -1588,7 +1588,7 @@
done
lemma butlast_take:
- "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
+ "n <= length xs ==> butlast (take n xs) = take (n - Suc 0) xs"
by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
@@ -1639,7 +1639,7 @@
done
lemma take_hd_drop:
- "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs"
+ "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (Suc n) xs"
apply(induct xs arbitrary: n)
apply simp
apply(simp add:drop_Cons split:nat.split)
@@ -2458,7 +2458,7 @@
done
lemma length_remove1:
- "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
+ "length(remove1 x xs) = (if x : set xs then length xs - Suc 0 else length xs)"
apply (induct xs)
apply (auto dest!:length_pos_if_in_set)
done
@@ -3564,52 +3564,51 @@
open Basic_Code_Thingol;
-fun implode_list (nil', cons') t =
- let
- fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
- if c = cons'
- then SOME (t1, t2)
- else NONE
- | dest_cons _ = NONE;
- val (ts, t') = Code_Thingol.unfoldr dest_cons t;
- in case t'
- of IConst (c, _) => if c = nil' then SOME ts else NONE
+fun implode_list naming t = case pairself
+ (Code_Thingol.lookup_const naming) (@{const_name Nil}, @{const_name Cons})
+ of (SOME nil', SOME cons') => let
+ fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
+ if c = cons'
+ then SOME (t1, t2)
+ else NONE
+ | dest_cons _ = NONE;
+ val (ts, t') = Code_Thingol.unfoldr dest_cons t;
+ in case t'
+ of IConst (c, _) => if c = nil' then SOME ts else NONE
+ | _ => NONE
+ end
| _ => NONE
- end;
-
-fun decode_char nibbles' (IConst (c1, _), IConst (c2, _)) =
- let
- fun idx c = find_index (curry (op =) c) nibbles';
- fun decode ~1 _ = NONE
- | decode _ ~1 = NONE
- | decode n m = SOME (chr (n * 16 + m));
- in decode (idx c1) (idx c2) end
- | decode_char _ _ = NONE;
-
-fun implode_string (char', nibbles') mk_char mk_string ts =
- let
- fun implode_char (IConst (c, _) `$ t1 `$ t2) =
- if c = char' then decode_char nibbles' (t1, t2) else NONE
- | implode_char _ = NONE;
- val ts' = map implode_char ts;
- in if forall is_some ts'
- then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
- else NONE
- end;
-
-fun list_names naming = pairself (the o Code_Thingol.lookup_const naming)
- (@{const_name Nil}, @{const_name Cons});
-fun char_name naming = (the o Code_Thingol.lookup_const naming)
- @{const_name Char}
-fun nibble_names naming = map (the o Code_Thingol.lookup_const naming)
- [@{const_name Nibble0}, @{const_name Nibble1},
+
+fun decode_char naming (IConst (c1, _), IConst (c2, _)) = (case map_filter
+ (Code_Thingol.lookup_const naming)[@{const_name Nibble0}, @{const_name Nibble1},
@{const_name Nibble2}, @{const_name Nibble3},
@{const_name Nibble4}, @{const_name Nibble5},
@{const_name Nibble6}, @{const_name Nibble7},
@{const_name Nibble8}, @{const_name Nibble9},
@{const_name NibbleA}, @{const_name NibbleB},
@{const_name NibbleC}, @{const_name NibbleD},
- @{const_name NibbleE}, @{const_name NibbleF}];
+ @{const_name NibbleE}, @{const_name NibbleF}]
+ of nibbles' as [_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _] => let
+ fun idx c = find_index (curry (op =) c) nibbles';
+ fun decode ~1 _ = NONE
+ | decode _ ~1 = NONE
+ | decode n m = SOME (chr (n * 16 + m));
+ in decode (idx c1) (idx c2) end
+ | _ => NONE)
+ | decode_char _ _ = NONE
+
+fun implode_string naming mk_char mk_string ts = case
+ Code_Thingol.lookup_const naming @{const_name Char}
+ of SOME char' => let
+ fun implode_char (IConst (c, _) `$ t1 `$ t2) =
+ if c = char' then decode_char naming (t1, t2) else NONE
+ | implode_char _ = NONE;
+ val ts' = map implode_char ts;
+ in if forall is_some ts'
+ then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
+ else NONE
+ end
+ | _ => NONE;
fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
@@ -3622,7 +3621,7 @@
let
val mk_list = Code_Printer.literal_list literals;
fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (implode_list (list_names naming) t2)
+ case Option.map (cons t1) (implode_list naming t2)
of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
| NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
in (2, pretty) end;
@@ -3633,8 +3632,8 @@
val mk_char = Code_Printer.literal_char literals;
val mk_string = Code_Printer.literal_string literals;
fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (implode_list (list_names naming) t2)
- of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
+ case Option.map (cons t1) (implode_list naming t2)
+ of SOME ts => (case implode_string naming mk_char mk_string ts
of SOME p => p
| NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
| NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
@@ -3644,7 +3643,7 @@
let
val mk_char = Code_Printer.literal_char literals;
fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
- case decode_char (nibble_names naming) (t1, t2)
+ case decode_char naming (t1, t2)
of SOME c => (Code_Printer.str o mk_char) c
| NONE => Code_Printer.nerror thm "Illegal character expression";
in (2, pretty) end;
@@ -3654,8 +3653,8 @@
val mk_char = Code_Printer.literal_char literals;
val mk_string = Code_Printer.literal_string literals;
fun pretty _ naming thm _ _ [(t, _)] =
- case implode_list (list_names naming) t
- of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
+ case implode_list naming t
+ of SOME ts => (case implode_string naming mk_char mk_string ts
of SOME p => p
| NONE => Code_Printer.nerror thm "Illegal message expression")
| NONE => Code_Printer.nerror thm "Illegal message expression";
--- a/src/HOL/MacLaurin.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/MacLaurin.thy Wed Feb 25 10:29:01 2009 +0000
@@ -81,7 +81,7 @@
prefer 2 apply simp
apply (frule less_iff_Suc_add [THEN iffD1], clarify)
apply (simp del: setsum_op_ivl_Suc)
- apply (insert sumr_offset4 [of 1])
+ apply (insert sumr_offset4 [of "Suc 0"])
apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
apply (rule lemma_DERIV_subst)
apply (rule DERIV_add)
@@ -124,7 +124,7 @@
have g2: "g 0 = 0 & g h = 0"
apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
- apply (cut_tac n = m and k = 1 in sumr_offset2)
+ apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
done
@@ -144,7 +144,7 @@
apply (simp add: m difg_def)
apply (frule less_iff_Suc_add [THEN iffD1], clarify)
apply (simp del: setsum_op_ivl_Suc)
- apply (insert sumr_offset4 [of 1])
+ apply (insert sumr_offset4 [of "Suc 0"])
apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
done
@@ -552,6 +552,10 @@
"[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
by auto
+text {* TODO: move to Parity.thy *}
+lemma nat_odd_1 [simp]: "odd (1::nat)"
+ unfolding even_nat_def by simp
+
lemma Maclaurin_sin_bound:
"abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
x ^ m)) \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
--- a/src/HOL/NSA/NSA.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NSA/NSA.thy Wed Feb 25 10:29:01 2009 +0000
@@ -157,7 +157,7 @@
by transfer (rule norm_divide)
lemma hypreal_hnorm_def [simp]:
- "\<And>r::hypreal. hnorm r \<equiv> \<bar>r\<bar>"
+ "\<And>r::hypreal. hnorm r = \<bar>r\<bar>"
by transfer (rule real_norm_def)
lemma hnorm_add_less:
--- a/src/HOL/Nat.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Nat.thy Wed Feb 25 10:29:01 2009 +0000
@@ -196,8 +196,8 @@
instance proof
fix n m q :: nat
- show "0 \<noteq> (1::nat)" by simp
- show "1 * n = n" by simp
+ show "0 \<noteq> (1::nat)" unfolding One_nat_def by simp
+ show "1 * n = n" unfolding One_nat_def by simp
show "n * m = m * n" by (induct n) simp_all
show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
@@ -307,18 +307,24 @@
lemmas nat_distrib =
add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2
-lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
+lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = Suc 0 & n = Suc 0)"
apply (induct m)
apply simp
apply (induct n)
apply auto
done
-lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
+lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
apply (rule trans)
apply (rule_tac [2] mult_eq_1_iff, fastsimp)
done
+lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"
+ unfolding One_nat_def by (rule mult_eq_1_iff)
+
+lemma nat_1_eq_mult_iff [simp]: "(1::nat) = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
+ unfolding One_nat_def by (rule one_eq_mult_iff)
+
lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
proof -
have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
@@ -465,11 +471,11 @@
lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
unfolding less_Suc_eq_le le_less ..
-lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
+lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
by (simp add: less_Suc_eq)
-lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
- by (simp add: less_Suc_eq)
+lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
+ unfolding One_nat_def by (rule less_Suc0)
lemma Suc_mono: "m < n ==> Suc m < Suc n"
by simp
@@ -735,6 +741,11 @@
show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
qed
+instance nat :: no_zero_divisors
+proof
+ fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
+qed
+
lemma nat_mult_1: "(1::nat) * n = n"
by simp
@@ -795,6 +806,7 @@
done
lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
+ unfolding One_nat_def
apply (cases n)
apply blast
apply (frule (1) ex_least_nat_le)
@@ -1084,7 +1096,7 @@
apply simp_all
done
-lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)"
+lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (Suc 0 \<le> m & Suc 0 \<le> n)"
apply (induct m)
apply simp
apply (case_tac n)
@@ -1120,7 +1132,7 @@
by (cases m) (auto intro: le_add1)
text {* Lemma for @{text gcd} *}
-lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
+lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = Suc 0 | m = 0"
apply (drule sym)
apply (rule disjCI)
apply (rule nat_less_cases, erule_tac [2] _)
@@ -1159,7 +1171,7 @@
| of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
lemma of_nat_1 [simp]: "of_nat 1 = 1"
- by simp
+ unfolding One_nat_def by simp
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
by (induct m) (simp_all add: add_ac)
@@ -1271,7 +1283,7 @@
end
lemma of_nat_id [simp]: "of_nat n = n"
- by (induct n) auto
+ by (induct n) (auto simp add: One_nat_def)
lemma of_nat_eq_id [simp]: "of_nat = id"
by (auto simp add: expand_fun_eq)
@@ -1376,7 +1388,7 @@
apply(induct_tac k)
apply simp
apply(erule_tac x="m+n" in meta_allE)
-apply(erule_tac x="m+n+1" in meta_allE)
+apply(erule_tac x="Suc(m+n)" in meta_allE)
apply simp
done
--- a/src/HOL/NatBin.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NatBin.thy Wed Feb 25 10:29:01 2009 +0000
@@ -159,6 +159,21 @@
unfolding nat_number_of_def number_of_is_id numeral_simps
by (simp add: nat_add_distrib)
+lemma nat_number_of_add_1 [simp]:
+ "number_of v + (1::nat) =
+ (if v < Int.Pls then 1 else number_of (Int.succ v))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by (simp add: nat_add_distrib)
+
+lemma nat_1_add_number_of [simp]:
+ "(1::nat) + number_of v =
+ (if v < Int.Pls then 1 else number_of (Int.succ v))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by (simp add: nat_add_distrib)
+
+lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
+ by (rule int_int_eq [THEN iffD1]) simp
+
subsubsection{*Subtraction *}
@@ -178,6 +193,12 @@
unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
by auto
+lemma nat_number_of_diff_1 [simp]:
+ "number_of v - (1::nat) =
+ (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by auto
+
subsubsection{*Multiplication *}
@@ -442,19 +463,13 @@
(* These two can be useful when m = number_of... *)
lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
-apply (case_tac "m")
-apply (simp_all add: numerals)
-done
+ unfolding One_nat_def by (cases m) simp_all
lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
-apply (case_tac "m")
-apply (simp_all add: numerals)
-done
+ unfolding One_nat_def by (cases m) simp_all
lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
-apply (case_tac "m")
-apply (simp_all add: numerals)
-done
+ unfolding One_nat_def by (cases m) simp_all
subsection{*Comparisons involving (0::nat) *}
--- a/src/HOL/NumberTheory/Chinese.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NumberTheory/Chinese.thy Wed Feb 25 10:29:01 2009 +0000
@@ -90,10 +90,8 @@
"k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
apply (induct l)
apply auto
- apply (rule_tac [1] zdvd_zmult2)
- apply (rule_tac [2] zdvd_zmult)
- apply (subgoal_tac "i = Suc (k + l)")
- apply (simp_all (no_asm_simp))
+ apply (subgoal_tac "i = Suc (k + l)")
+ apply (simp_all (no_asm_simp))
done
lemma funsum_mod:
@@ -103,7 +101,7 @@
apply (rule trans)
apply (rule mod_add_eq)
apply simp
- apply (rule zmod_zadd_right_eq [symmetric])
+ apply (rule mod_add_right_eq [symmetric])
done
lemma funsum_zero [rule_format (no_asm)]:
@@ -196,8 +194,8 @@
apply (case_tac [2] "i = n")
apply (simp_all (no_asm_simp))
apply (case_tac [3] "j < i")
- apply (rule_tac [3] zdvd_zmult2)
- apply (rule_tac [4] zdvd_zmult)
+ apply (rule_tac [3] dvd_mult2)
+ apply (rule_tac [4] dvd_mult)
apply (rule_tac [!] funprod_zdvd)
apply arith
apply arith
@@ -217,8 +215,8 @@
apply (subst funsum_mod)
apply (subst funsum_oneelem)
apply auto
- apply (subst zdvd_iff_zmod_eq_0 [symmetric])
- apply (rule zdvd_zmult)
+ apply (subst dvd_eq_mod_eq_0 [symmetric])
+ apply (rule dvd_mult)
apply (rule x_sol_lin_aux)
apply auto
done
@@ -238,20 +236,20 @@
apply safe
apply (tactic {* stac (thm "zcong_zmod") 3 *})
apply (tactic {* stac (thm "mod_mult_eq") 3 *})
- apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
- apply (tactic {* stac (thm "x_sol_lin") 5 *})
- apply (tactic {* stac (thm "mod_mult_eq" RS sym) 7 *})
- apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
- apply (subgoal_tac [7]
+ apply (tactic {* stac (thm "mod_mod_cancel") 3 *})
+ apply (tactic {* stac (thm "x_sol_lin") 4 *})
+ apply (tactic {* stac (thm "mod_mult_eq" RS sym) 6 *})
+ apply (tactic {* stac (thm "zcong_zmod" RS sym) 6 *})
+ apply (subgoal_tac [6]
"0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
\<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
- prefer 7
+ prefer 6
apply (simp add: zmult_ac)
apply (unfold xilin_sol_def)
- apply (tactic {* asm_simp_tac @{simpset} 7 *})
- apply (rule_tac [7] ex1_implies_ex [THEN someI_ex])
- apply (rule_tac [7] unique_xi_sol)
- apply (rule_tac [4] funprod_zdvd)
+ apply (tactic {* asm_simp_tac @{simpset} 6 *})
+ apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
+ apply (rule_tac [6] unique_xi_sol)
+ apply (rule_tac [3] funprod_zdvd)
apply (unfold m_cond_def)
apply (rule funprod_pos [THEN pos_mod_sign])
apply (rule_tac [2] funprod_pos [THEN pos_mod_bound])
--- a/src/HOL/NumberTheory/Euler.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NumberTheory/Euler.thy Wed Feb 25 10:29:01 2009 +0000
@@ -272,7 +272,7 @@
text {* \medskip Prove the final part of Euler's Criterion: *}
lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
- by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div zdvd_trans)
+ by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
lemma aux__2: "2 * nat((p - 1) div 2) = nat (2 * ((p - 1) div 2))"
by (auto simp add: nat_mult_distrib)
--- a/src/HOL/NumberTheory/EulerFermat.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NumberTheory/EulerFermat.thy Wed Feb 25 10:29:01 2009 +0000
@@ -155,7 +155,7 @@
prefer 2
apply (subst zdvd_iff_zgcd [symmetric])
apply (rule_tac [4] zgcd_zcong_zgcd)
- apply (simp_all add: zdvd_zminus_iff zcong_sym)
+ apply (simp_all add: zcong_sym)
done
--- a/src/HOL/NumberTheory/Gauss.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NumberTheory/Gauss.thy Wed Feb 25 10:29:01 2009 +0000
@@ -64,14 +64,14 @@
qed
lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
- using zdiv_zmult_self2 [of 2 "p - 1"] by auto
+ using div_mult_self1_is_id [of 2 "p - 1"] by auto
lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
apply (frule odd_minus_one_even)
apply (simp add: zEven_def)
apply (subgoal_tac "2 \<noteq> 0")
- apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)
+ apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id)
apply (auto simp add: even_div_2_prop2)
done
--- a/src/HOL/NumberTheory/Int2.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NumberTheory/Int2.thy Wed Feb 25 10:29:01 2009 +0000
@@ -18,7 +18,7 @@
lemma zpower_zdvd_prop1:
"0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
- by (induct n) (auto simp add: zdvd_zmult zdvd_zmult2 [of p y])
+ by (induct n) (auto simp add: dvd_mult2 [of p y])
lemma zdvd_bounds: "n dvd m ==> m \<le> (0::int) | n \<le> m"
proof -
@@ -42,7 +42,7 @@
apply simp
apply (frule zprime_zdvd_zmult_better)
apply simp
- apply force
+ apply (force simp del:dvd_mult)
done
lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"
@@ -86,7 +86,7 @@
by (auto simp add: zcong_def)
lemma zcong_id: "[m = 0] (mod m)"
- by (auto simp add: zcong_def zdvd_0_right)
+ by (auto simp add: zcong_def)
lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)"
by (auto simp add: zcong_refl zcong_zadd)
--- a/src/HOL/NumberTheory/IntPrimes.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NumberTheory/IntPrimes.thy Wed Feb 25 10:29:01 2009 +0000
@@ -50,7 +50,7 @@
lemma zrelprime_zdvd_zmult_aux:
"zgcd n k = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
- by (metis abs_of_nonneg zdvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
+ by (metis abs_of_nonneg dvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
lemma zrelprime_zdvd_zmult: "zgcd n k = 1 ==> k dvd m * n ==> k dvd m"
apply (case_tac "0 \<le> m")
@@ -73,7 +73,7 @@
lemma zprime_imp_zrelprime:
"zprime p ==> \<not> p dvd n ==> zgcd n p = 1"
apply (auto simp add: zprime_def)
- apply (metis zgcd_commute zgcd_geq_zero zgcd_zdvd1 zgcd_zdvd2)
+ apply (metis zgcd_geq_zero zgcd_zdvd1 zgcd_zdvd2)
done
lemma zless_zprime_imp_zrelprime:
@@ -93,9 +93,7 @@
done
lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n"
- apply (simp add: zgcd_greatest_iff)
- apply (blast intro: zdvd_trans dvd_triv_right)
- done
+by (simp add: zgcd_greatest_iff)
lemma zgcd_zmult_zdvd_zgcd:
"zgcd k n = 1 ==> zgcd (k * m) n dvd zgcd m n"
@@ -127,20 +125,20 @@
by (unfold zcong_def, auto)
lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)"
- unfolding zcong_def minus_diff_eq [of a, symmetric] zdvd_zminus_iff ..
+ unfolding zcong_def minus_diff_eq [of a, symmetric] dvd_minus_iff ..
lemma zcong_zadd:
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)"
apply (unfold zcong_def)
apply (rule_tac s = "(a - b) + (c - d)" in subst)
- apply (rule_tac [2] zdvd_zadd, auto)
+ apply (rule_tac [2] dvd_add, auto)
done
lemma zcong_zdiff:
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a - c = b - d] (mod m)"
apply (unfold zcong_def)
apply (rule_tac s = "(a - b) - (c - d)" in subst)
- apply (rule_tac [2] zdvd_zdiff, auto)
+ apply (rule_tac [2] dvd_diff, auto)
done
lemma zcong_trans:
@@ -151,8 +149,8 @@
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)"
apply (rule_tac b = "b * c" in zcong_trans)
apply (unfold zcong_def)
- apply (metis zdiff_zmult_distrib2 zdvd_zmult zmult_commute)
- apply (metis zdiff_zmult_distrib2 zdvd_zmult)
+ apply (metis zdiff_zmult_distrib2 dvd_mult zmult_commute)
+ apply (metis zdiff_zmult_distrib2 dvd_mult)
done
lemma zcong_scalar: "[a = b] (mod m) ==> [a * k = b * k] (mod m)"
@@ -163,7 +161,7 @@
lemma zcong_zmult_self: "[a * m = b * m] (mod m)"
apply (unfold zcong_def)
- apply (rule zdvd_zdiff, simp_all)
+ apply (rule dvd_diff, simp_all)
done
lemma zcong_square:
@@ -191,7 +189,7 @@
apply (simp_all add: zdiff_zmult_distrib)
apply (subgoal_tac "m dvd (-(a * k - b * k))")
apply simp
- apply (subst zdvd_zminus_iff, assumption)
+ apply (subst dvd_minus_iff, assumption)
done
lemma zcong_cancel2:
@@ -206,10 +204,10 @@
apply (subgoal_tac "m dvd n * ka")
apply (subgoal_tac "m dvd ka")
apply (case_tac [2] "0 \<le> ka")
- apply (metis zdvd_mult_div_cancel zdvd_refl zdvd_zminus2_iff zdvd_zmultD2 zgcd_zminus zmult_commute zmult_zminus zrelprime_zdvd_zmult)
- apply (metis IntDiv.zdvd_abs1 abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute)
- apply (metis abs_eq_0 int_0_neq_1 mult_le_0_iff zdvd_mono zdvd_mult_cancel zdvd_mult_cancel1 zdvd_refl zdvd_triv_left zdvd_zmult2 zero_le_mult_iff zgcd_greatest_iff zle_anti_sym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult)
- apply (metis zdvd_triv_left)
+ apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left zmult_commute zrelprime_zdvd_zmult)
+ apply (metis abs_dvd_iff abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute)
+ apply (metis mult_le_0_iff zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff zle_anti_sym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult)
+ apply (metis dvd_triv_left)
done
lemma zcong_zless_imp_eq:
@@ -217,7 +215,7 @@
a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
apply (unfold zcong_def dvd_def, auto)
apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
- apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff zmod_zadd_right_eq)
+ apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff mod_add_right_eq)
done
lemma zcong_square_zless:
@@ -237,7 +235,7 @@
lemma zcong_zless_0:
"0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
apply (unfold zcong_def dvd_def, auto)
- apply (metis div_pos_pos_trivial linorder_not_less zdiv_zmult_self2 zle_refl zle_trans)
+ apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id)
done
lemma zcong_zless_unique:
@@ -302,7 +300,7 @@
lemma zmod_zdvd_zmod:
"0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
- by (rule zmod_zmod_cancel)
+ by (rule mod_mod_cancel)
subsection {* Extended GCD *}
@@ -403,7 +401,7 @@
prefer 2
apply simp
apply (unfold zcong_def)
- apply (simp (no_asm) add: zmult_commute zdvd_zminus_iff)
+ apply (simp (no_asm) add: zmult_commute)
done
lemma zcong_lineq_unique:
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Feb 25 10:29:01 2009 +0000
@@ -322,7 +322,7 @@
by (rule zdiv_mono1) (insert p_g_2, auto)
then show "b \<le> (q * a) div p"
apply (subgoal_tac "p \<noteq> 0")
- apply (frule zdiv_zmult_self2, force)
+ apply (frule div_mult_self1_is_id, force)
apply (insert p_g_2, auto)
done
qed
@@ -356,7 +356,7 @@
by (rule zdiv_mono1) (insert q_g_2, auto)
then show "a \<le> (p * b) div q"
apply (subgoal_tac "q \<noteq> 0")
- apply (frule zdiv_zmult_self2, force)
+ apply (frule div_mult_self1_is_id, force)
apply (insert q_g_2, auto)
done
qed
--- a/src/HOL/NumberTheory/Residues.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NumberTheory/Residues.thy Wed Feb 25 10:29:01 2009 +0000
@@ -48,7 +48,7 @@
by (auto simp add: StandardRes_def zcong_zmod_eq)
lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))"
- by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0)
+ by (auto simp add: StandardRes_def zcong_def dvd_eq_mod_eq_0)
lemma StandardRes_prop4: "2 < m
==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)"
--- a/src/HOL/NumberTheory/WilsonBij.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NumberTheory/WilsonBij.thy Wed Feb 25 10:29:01 2009 +0000
@@ -57,7 +57,7 @@
apply (rule_tac [2] zdvd_not_zless)
apply (subgoal_tac "p dvd 1")
prefer 2
- apply (subst zdvd_zminus_iff [symmetric])
+ apply (subst dvd_minus_iff [symmetric])
apply auto
done
@@ -79,7 +79,7 @@
apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
apply (simp add: mult_commute)
- apply (subst zdvd_zminus_iff)
+ apply (subst dvd_minus_iff)
apply (subst zdvd_reduce)
apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
apply (subst zdvd_reduce)
--- a/src/HOL/NumberTheory/WilsonRuss.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Wed Feb 25 10:29:01 2009 +0000
@@ -68,7 +68,7 @@
apply (rule_tac [2] zdvd_not_zless)
apply (subgoal_tac "p dvd 1")
prefer 2
- apply (subst zdvd_zminus_iff [symmetric], auto)
+ apply (subst dvd_minus_iff [symmetric], auto)
done
lemma inv_not_1:
@@ -87,7 +87,7 @@
apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
apply (simp add: mult_commute)
- apply (subst zdvd_zminus_iff)
+ apply (subst dvd_minus_iff)
apply (subst zdvd_reduce)
apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
apply (subst zdvd_reduce, auto)
--- a/src/HOL/Parity.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Parity.thy Wed Feb 25 10:29:01 2009 +0000
@@ -228,20 +228,9 @@
lemma zero_le_odd_power: "odd n ==>
(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"
- apply (simp add: odd_nat_equiv_def2)
- apply (erule exE)
- apply (erule ssubst)
- apply (subst power_Suc)
- apply (subst power_add)
- apply (subst zero_le_mult_iff)
- apply auto
- apply (subgoal_tac "x = 0 & y > 0")
- apply (erule conjE, assumption)
- apply (subst power_eq_0_iff [symmetric])
- apply (subgoal_tac "0 <= x^y * x^y")
- apply simp
- apply (rule zero_le_square)+
- done
+apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
+apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
+done
lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) =
(even n | (odd n & 0 <= x))"
--- a/src/HOL/Plain.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Plain.thy Wed Feb 25 10:29:01 2009 +0000
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Record Extraction Divides Fact
+imports Datatype FunDef Record Extraction Divides
begin
text {*
--- a/src/HOL/Power.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Power.thy Wed Feb 25 10:29:01 2009 +0000
@@ -31,7 +31,7 @@
by (induct n) (simp_all add: power_Suc)
lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
- by (simp add: power_Suc)
+ unfolding One_nat_def by (simp add: power_Suc)
lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
by (induct n) (simp_all add: power_Suc mult_assoc)
@@ -143,11 +143,13 @@
done
lemma power_eq_0_iff [simp]:
- "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n>0)"
+ "(a^n = 0) \<longleftrightarrow>
+ (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)"
apply (induct "n")
-apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
+apply (auto simp add: power_Suc zero_neq_one [THEN not_sym] no_zero_divisors)
done
+
lemma field_power_not_zero:
"a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
by force
@@ -364,12 +366,19 @@
"of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
by (induct n, simp_all add: power_Suc of_nat_mult)
-lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
-by (insert one_le_power [of i n], simp)
+lemma nat_one_le_power [simp]: "Suc 0 \<le> i ==> Suc 0 \<le> i^n"
+by (rule one_le_power [of i n, unfolded One_nat_def])
lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
by (induct "n", auto)
+lemma nat_power_eq_Suc_0_iff [simp]:
+ "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
+by (induct_tac m, auto)
+
+lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
+by simp
+
text{*Valid for the naturals, but what if @{text"0<i<1"}?
Premises cannot be weakened: consider the case where @{term "i=0"},
@{term "m=1"} and @{term "n=0"}.*}
@@ -443,4 +452,3 @@
*}
end
-
--- a/src/HOL/Presburger.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Presburger.thy Wed Feb 25 10:29:01 2009 +0000
@@ -412,19 +412,15 @@
"(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
by (rule eq_number_of_eq)
-lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
-unfolding dvd_eq_mod_eq_0[symmetric] ..
-
-lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
-unfolding zdvd_iff_zmod_eq_0[symmetric] ..
+declare dvd_eq_mod_eq_0[symmetric, presburger]
declare mod_1[presburger]
declare mod_0[presburger]
-declare zmod_1[presburger]
+declare mod_by_1[presburger]
declare zmod_zero[presburger]
declare zmod_self[presburger]
declare mod_self[presburger]
declare mod_by_0[presburger]
-declare nat_mod_div_trivial[presburger]
+declare mod_div_trivial[presburger]
declare div_mod_equality2[presburger]
declare div_mod_equality[presburger]
declare mod_div_equality2[presburger]
--- a/src/HOL/RealDef.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/RealDef.thy Wed Feb 25 10:29:01 2009 +0000
@@ -655,7 +655,7 @@
real(n div d) = real n / real d"
apply (frule real_of_int_div_aux [of d n])
apply simp
- apply (simp add: zdvd_iff_zmod_eq_0)
+ apply (simp add: dvd_eq_mod_eq_0)
done
lemma real_of_int_div2:
@@ -705,6 +705,9 @@
lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
by (simp add: real_of_nat_def)
+lemma real_of_nat_1 [simp]: "real (1::nat) = 1"
+by (simp add: real_of_nat_def)
+
lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
by (simp add: real_of_nat_def)
--- a/src/HOL/RealPow.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/RealPow.thy Wed Feb 25 10:29:01 2009 +0000
@@ -44,7 +44,8 @@
by (insert power_decreasing [of 1 "Suc n" r], simp)
lemma realpow_minus_mult [rule_format]:
- "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
+ "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
+unfolding One_nat_def
apply (simp split add: nat_diff_split)
done
--- a/src/HOL/RealVector.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/RealVector.thy Wed Feb 25 10:29:01 2009 +0000
@@ -46,8 +46,10 @@
locale vector_space =
fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b"
- assumes scale_right_distrib: "scale a (x + y) = scale a x + scale a y"
- and scale_left_distrib: "scale (a + b) x = scale a x + scale b x"
+ assumes scale_right_distrib [algebra_simps]:
+ "scale a (x + y) = scale a x + scale a y"
+ and scale_left_distrib [algebra_simps]:
+ "scale (a + b) x = scale a x + scale b x"
and scale_scale [simp]: "scale a (scale b x) = scale (a * b) x"
and scale_one [simp]: "scale 1 x = x"
begin
@@ -58,7 +60,8 @@
lemma scale_zero_left [simp]: "scale 0 x = 0"
and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
- and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x"
+ and scale_left_diff_distrib [algebra_simps]:
+ "scale (a - b) x = scale a x - scale b x"
proof -
interpret s: additive "\<lambda>a. scale a x"
proof qed (rule scale_left_distrib)
@@ -69,7 +72,8 @@
lemma scale_zero_right [simp]: "scale a 0 = 0"
and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
- and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y"
+ and scale_right_diff_distrib [algebra_simps]:
+ "scale a (x - y) = scale a x - scale a y"
proof -
interpret s: additive "\<lambda>x. scale a x"
proof qed (rule scale_right_distrib)
@@ -135,21 +139,11 @@
end
-instantiation real :: scaleR
-begin
-
-definition
- real_scaleR_def [simp]: "scaleR a x = a * x"
-
-instance ..
-
-end
-
class real_vector = scaleR + ab_group_add +
assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
- and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
- and scaleR_one [simp]: "scaleR 1 x = x"
+ and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
+ and scaleR_one: "scaleR 1 x = x"
interpretation real_vector!:
vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
@@ -185,15 +179,16 @@
class real_field = real_div_algebra + field
-instance real :: real_field
-apply (intro_classes, unfold real_scaleR_def)
-apply (rule right_distrib)
-apply (rule left_distrib)
-apply (rule mult_assoc [symmetric])
-apply (rule mult_1_left)
-apply (rule mult_assoc)
-apply (rule mult_left_commute)
-done
+instantiation real :: real_field
+begin
+
+definition
+ real_scaleR_def [simp]: "scaleR a x = a * x"
+
+instance proof
+qed (simp_all add: algebra_simps)
+
+end
interpretation scaleR_left!: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
proof qed (rule scaleR_left_distrib)
@@ -307,7 +302,7 @@
definition
Reals :: "'a::real_algebra_1 set" where
- [code del]: "Reals \<equiv> range of_real"
+ [code del]: "Reals = range of_real"
notation (xsymbols)
Reals ("\<real>")
@@ -421,16 +416,6 @@
class norm =
fixes norm :: "'a \<Rightarrow> real"
-instantiation real :: norm
-begin
-
-definition
- real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>"
-
-instance ..
-
-end
-
class sgn_div_norm = scaleR + norm + sgn +
assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
@@ -462,7 +447,13 @@
thus "norm (1::'a) = 1" by simp
qed
-instance real :: real_normed_field
+instantiation real :: real_normed_field
+begin
+
+definition
+ real_norm_def [simp]: "norm r = \<bar>r\<bar>"
+
+instance
apply (intro_classes, unfold real_norm_def real_scaleR_def)
apply (simp add: real_sgn_def)
apply (rule abs_ge_zero)
@@ -472,6 +463,8 @@
apply (rule abs_mult)
done
+end
+
lemma norm_zero [simp]: "norm (0::'a::real_normed_vector) = 0"
by simp
--- a/src/HOL/Relation_Power.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Relation_Power.thy Wed Feb 25 10:29:01 2009 +0000
@@ -61,16 +61,16 @@
lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
proof -
- have "f((f^n) x) = (f^(n+1)) x" by simp
+ have "f((f^n) x) = (f^(n+1)) x" unfolding One_nat_def by simp
also have "\<dots> = (f^n o f^1) x" by (simp only: funpow_add)
- also have "\<dots> = (f^n)(f x)" by simp
+ also have "\<dots> = (f^n)(f x)" unfolding One_nat_def by simp
finally show ?thesis .
qed
lemma rel_pow_1 [simp]:
fixes R :: "('a*'a)set"
shows "R^1 = R"
- by simp
+ unfolding One_nat_def by simp
lemma rel_pow_0_I: "(x,x) : R^0"
by simp
--- a/src/HOL/Ring_and_Field.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Ring_and_Field.thy Wed Feb 25 10:29:01 2009 +0000
@@ -147,10 +147,10 @@
lemma one_dvd [simp]: "1 dvd a"
by (auto intro!: dvdI)
-lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
+lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
by (auto intro!: mult_left_commute dvdI elim!: dvdE)
-lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
+lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
apply (subst mult_commute)
apply (erule dvd_mult)
done
@@ -162,12 +162,12 @@
by (rule dvd_mult2) (rule dvd_refl)
lemma mult_dvd_mono:
- assumes ab: "a dvd b"
- and "cd": "c dvd d"
+ assumes "a dvd b"
+ and "c dvd d"
shows "a * c dvd b * d"
proof -
- from ab obtain b' where "b = a * b'" ..
- moreover from "cd" obtain d' where "d = c * d'" ..
+ from `a dvd b` obtain b' where "b = a * b'" ..
+ moreover from `c dvd d` obtain d' where "d = c * d'" ..
ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
then show ?thesis ..
qed
@@ -310,8 +310,8 @@
then show "- x dvd y" ..
qed
-lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
-by (simp add: diff_minus dvd_add dvd_minus_iff)
+lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
+by (simp add: diff_minus dvd_minus_iff)
end
--- a/src/HOL/SEQ.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/SEQ.thy Wed Feb 25 10:29:01 2009 +0000
@@ -338,10 +338,10 @@
done
lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
-by (drule_tac k="1" in LIMSEQ_ignore_initial_segment, simp)
+by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp)
lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l"
-by (rule_tac k="1" in LIMSEQ_offset, simp)
+by (rule_tac k="Suc 0" in LIMSEQ_offset, simp)
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
--- a/src/HOL/Series.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Series.thy Wed Feb 25 10:29:01 2009 +0000
@@ -312,6 +312,7 @@
shows "\<lbrakk>summable f;
\<forall>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
\<Longrightarrow> setsum f {0..<k} < suminf f"
+unfolding One_nat_def
apply (subst suminf_split_initial_segment [where k="k"])
apply assumption
apply simp
@@ -537,7 +538,7 @@
apply (safe, subgoal_tac "\<forall>n. N < n --> f (n) = 0")
prefer 2
apply clarify
- apply(erule_tac x = "n - 1" in allE)
+ apply(erule_tac x = "n - Suc 0" in allE)
apply (simp add:diff_Suc split:nat.splits)
apply (blast intro: norm_ratiotest_lemma)
apply (rule_tac x = "Suc N" in exI, clarify)
--- a/src/HOL/SetInterval.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/SetInterval.thy Wed Feb 25 10:29:01 2009 +0000
@@ -352,11 +352,11 @@
corollary image_Suc_atLeastAtMost[simp]:
"Suc ` {i..j} = {Suc i..Suc j}"
-using image_add_atLeastAtMost[where k=1] by simp
+using image_add_atLeastAtMost[where k="Suc 0"] by simp
corollary image_Suc_atLeastLessThan[simp]:
"Suc ` {i..<j} = {Suc i..<Suc j}"
-using image_add_atLeastLessThan[where k=1] by simp
+using image_add_atLeastLessThan[where k="Suc 0"] by simp
lemma image_add_int_atLeastLessThan:
"(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
@@ -556,7 +556,7 @@
qed
lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
-apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - 1"])
+apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - Suc 0"])
apply simp
apply fastsimp
apply auto
@@ -803,7 +803,7 @@
lemma setsum_head_upt_Suc:
"m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}"
-apply(insert setsum_head_Suc[of m "n - 1" f])
+apply(insert setsum_head_Suc[of m "n - Suc 0" f])
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps)
done
@@ -835,11 +835,11 @@
corollary setsum_shift_bounds_cl_Suc_ivl:
"setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}"
-by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified])
+by (simp add:setsum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
corollary setsum_shift_bounds_Suc_ivl:
"setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
-by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
+by (simp add:setsum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
lemma setsum_shift_lb_Suc0_0:
"f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}"
@@ -883,6 +883,7 @@
by (rule setsum_addf)
also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
+ unfolding One_nat_def
by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
by (simp add: left_distrib right_distrib)
@@ -890,7 +891,7 @@
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
also from ngt1
have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
- by (simp only: mult_ac gauss_sum [of "n - 1"])
+ by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
(simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
finally show ?thesis by (simp add: algebra_simps)
next
@@ -906,7 +907,8 @@
"((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
of_nat(n) * (a + (a + of_nat(n - 1)*d))"
by (rule arith_series_general)
- thus ?thesis by (auto simp add: of_nat_id)
+ thus ?thesis
+ unfolding One_nat_def by (auto simp add: of_nat_id)
qed
lemma arith_series_int:
--- a/src/HOL/Tools/Qelim/presburger.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Tools/Qelim/presburger.ML Wed Feb 25 10:29:01 2009 +0000
@@ -122,14 +122,13 @@
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
val div_mod_ss = HOL_basic_ss addsimps simp_thms
@ map (symmetric o mk_meta_eq)
- [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"},
+ [@{thm "dvd_eq_mod_eq_0"}, @{thm "mod_add1_eq"},
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
- @{thm "mod_add_eq"}, @{thm "zmod_zadd_left_eq"},
- @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
+ @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},
@{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
@{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"},
- @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"},
+ @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
@{thm "mod_1"}, @{thm "Suc_plus1"}]
@ @{thms add_ac}
addsimprocs [cancel_div_mod_proc]
--- a/src/HOL/Tools/atp_wrapper.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Tools/atp_wrapper.ML Wed Feb 25 10:29:01 2009 +0000
@@ -78,10 +78,14 @@
val failure = find_failure proof
val success = rc = 0 andalso is_none failure
val message =
- if isSome failure then "Could not prove: " ^ the failure
- else if rc <> 0
- then "Exited with return code " ^ string_of_int rc ^ ": " ^ proof
- else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
+ if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
+ else "Could not prove goal."
+ val _ = if isSome failure
+ then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
+ else ()
+ val _ = if rc <> 0
+ then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
+ else ()
in (success, message) end;
--- a/src/HOL/Tools/datatype_codegen.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Tools/datatype_codegen.ML Wed Feb 25 10:29:01 2009 +0000
@@ -6,8 +6,8 @@
signature DATATYPE_CODEGEN =
sig
- val get_eq: theory -> string -> thm list
- val get_case_cert: theory -> string -> thm
+ val mk_eq: theory -> string -> thm list
+ val mk_case_cert: theory -> string -> thm
val setup: theory -> theory
end;
@@ -323,7 +323,7 @@
(* case certificates *)
-fun get_case_cert thy tyco =
+fun mk_case_cert thy tyco =
let
val raw_thms =
(#case_rewrites o DatatypePackage.the_datatype thy) tyco;
@@ -357,10 +357,13 @@
fun add_datatype_cases dtco thy =
let
val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco;
- val certs = get_case_cert thy dtco;
+ val cert = mk_case_cert thy dtco;
+ fun add_case_liberal thy = thy
+ |> try (Code.add_case cert)
+ |> the_default thy;
in
thy
- |> Code.add_case certs
+ |> add_case_liberal
|> fold_rev Code.add_default_eqn case_rewrites
end;
@@ -369,10 +372,10 @@
local
-val not_sym = thm "HOL.not_sym";
-val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
-val refl = thm "refl";
-val eqTrueI = thm "eqTrueI";
+val not_sym = @{thm HOL.not_sym};
+val not_false_true = iffD2 OF [nth @{thms HOL.simp_thms} 7, TrueI];
+val refl = @{thm refl};
+val eqTrueI = @{thm eqTrueI};
fun mk_distinct cos =
let
@@ -397,7 +400,7 @@
in
-fun get_eq thy dtco =
+fun mk_eq thy dtco =
let
val (vs, cs) = DatatypePackage.the_datatype_spec thy dtco;
fun mk_triv_inject co =
@@ -445,7 +448,7 @@
in (thm', lthy') end;
fun tac thms = Class.intro_classes_tac []
THEN ALLGOALS (ProofContext.fact_tac thms);
- fun get_eq' thy dtco = get_eq thy dtco
+ fun mk_eq' thy dtco = mk_eq thy dtco
|> map (Code_Unit.constrain_thm thy [HOLogic.class_eq])
|> map Simpdata.mk_eq
|> map (MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}])
@@ -460,10 +463,10 @@
([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
|> Simpdata.mk_eq
|> AxClass.unoverload thy;
- fun get_thms () = (eq_refl, false)
- :: rev (map (rpair true) (get_eq' (Theory.deref thy_ref) dtco));
+ fun mk_thms () = (eq_refl, false)
+ :: rev (map (rpair true) (mk_eq' (Theory.deref thy_ref) dtco));
in
- Code.add_eqnl (const, Lazy.lazy get_thms) thy
+ Code.add_eqnl (const, Lazy.lazy mk_thms) thy
end;
in
thy
--- a/src/HOL/Tools/datatype_package.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Tools/datatype_package.ML Wed Feb 25 10:29:01 2009 +0000
@@ -659,7 +659,7 @@
| pretty_constr (co, [ty']) =
(Pretty.block o Pretty.breaks)
[Syntax.pretty_term ctxt (Const (co, ty' --> ty)),
- Syntax.pretty_typ ctxt ty']
+ pretty_typ_br ty']
| pretty_constr (co, tys) =
(Pretty.block o Pretty.breaks)
(Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
--- a/src/HOL/Tools/int_factor_simprocs.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Tools/int_factor_simprocs.ML Wed Feb 25 10:29:01 2009 +0000
@@ -216,7 +216,7 @@
(** Final simplification for the CancelFactor simprocs **)
val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq
- [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, @{thm numeral_1_eq_1}];
+ [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
fun cancel_simplify_meta_eq cancel_th ss th =
simplify_one ss (([th, cancel_th]) MRS trans);
--- a/src/HOL/Transcendental.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Transcendental.thy Wed Feb 25 10:29:01 2009 +0000
@@ -120,7 +120,7 @@
case (Suc n)
have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) =
(\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
- using Suc.hyps by auto
+ using Suc.hyps unfolding One_nat_def by auto
also have "\<dots> = (\<Sum> i = 0 ..< Suc n. f (2 * i)) + (\<Sum> i = 0 ..< Suc n. g (2 * i + 1))" by auto
finally show ?case .
qed auto
@@ -187,16 +187,18 @@
((\<forall>n. l \<le> (\<Sum>i=0..<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i=0..<2*n + 1. -1^i*a i) ----> l)"
(is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
proof -
- have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" by auto
+ have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
have "\<forall> n. ?f n \<le> ?f (Suc n)"
proof fix n show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto qed
moreover
have "\<forall> n. ?g (Suc n) \<le> ?g n"
- proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"] by auto qed
+ proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
+ unfolding One_nat_def by auto qed
moreover
have "\<forall> n. ?f n \<le> ?g n"
- proof fix n show "?f n \<le> ?g n" using fg_diff a_pos by auto qed
+ proof fix n show "?f n \<le> ?g n" using fg_diff a_pos
+ unfolding One_nat_def by auto qed
moreover
have "(\<lambda> n. ?f n - ?g n) ----> 0" unfolding fg_diff
proof (rule LIMSEQ_I)
@@ -904,7 +906,7 @@
proof -
have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
by (rule sums_unique [OF series_zero], simp add: power_0_left)
- thus ?thesis by simp
+ thus ?thesis unfolding One_nat_def by simp
qed
lemma exp_zero [simp]: "exp 0 = 1"
@@ -1234,10 +1236,11 @@
show "x - 1 \<in> {- 1<..<1}" and "(0 :: real) < 1" using `0 < x` `x < 2` by auto
{ fix x :: real assume "x \<in> {- 1<..<1}" hence "norm (-x) < 1" by auto
show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
+ unfolding One_nat_def
by (auto simp del: power_mult_distrib simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
}
qed
- hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)" by auto
+ hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)" unfolding One_nat_def by auto
hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)" unfolding DERIV_iff repos .
ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
by (rule DERIV_diff)
@@ -1514,6 +1517,7 @@
lemma DERIV_fun_pow: "DERIV g x :> m ==>
DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
+unfolding One_nat_def
apply (rule lemma_DERIV_subst)
apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
apply (rule DERIV_pow, auto)
@@ -1635,7 +1639,7 @@
sums sin x"
unfolding sin_def
by (rule sin_converges [THEN sums_summable, THEN sums_group], simp)
- thus ?thesis by (simp add: mult_ac)
+ thus ?thesis unfolding One_nat_def by (simp add: mult_ac)
qed
lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
@@ -1647,6 +1651,7 @@
apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp)
apply (rotate_tac 2)
apply (drule sin_paired [THEN sums_unique, THEN ssubst])
+unfolding One_nat_def
apply (auto simp del: fact_Suc realpow_Suc)
apply (frule sums_unique)
apply (auto simp del: fact_Suc realpow_Suc)
@@ -1720,6 +1725,7 @@
apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
apply (rule sumr_pos_lt_pair)
apply (erule sums_summable, safe)
+unfolding One_nat_def
apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
del: fact_Suc)
apply (rule real_mult_inverse_cancel2)
@@ -2792,7 +2798,7 @@
lemma monoseq_arctan_series: fixes x :: real
assumes "\<bar>x\<bar> \<le> 1" shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
-proof (cases "x = 0") case True thus ?thesis unfolding monoseq_def by auto
+proof (cases "x = 0") case True thus ?thesis unfolding monoseq_def One_nat_def by auto
next
case False
have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
@@ -2823,7 +2829,7 @@
lemma zeroseq_arctan_series: fixes x :: real
assumes "\<bar>x\<bar> \<le> 1" shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
-proof (cases "x = 0") case True thus ?thesis by (auto simp add: LIMSEQ_const)
+proof (cases "x = 0") case True thus ?thesis unfolding One_nat_def by (auto simp add: LIMSEQ_const)
next
case False
have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
@@ -2831,12 +2837,14 @@
proof (cases "\<bar>x\<bar> < 1")
case True hence "norm x < 1" by auto
from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
- show ?thesis unfolding inverse_eq_divide Suc_plus1 using LIMSEQ_linear[OF _ pos2] by auto
+ have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
+ unfolding inverse_eq_divide Suc_plus1 by simp
+ then show ?thesis using pos2 by (rule LIMSEQ_linear)
next
case False hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
- hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" by auto
+ hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" unfolding One_nat_def by auto
from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] LIMSEQ_const[of x]]
- show ?thesis unfolding n_eq by auto
+ show ?thesis unfolding n_eq Suc_plus1 by auto
qed
qed
@@ -2989,7 +2997,7 @@
from `even n` obtain m where "2 * m = n" unfolding even_mult_two_ex by auto
from bounds[of m, unfolded this atLeastAtMost_iff]
have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n + 1. (?c x i)) - (\<Sum>i = 0..<n. (?c x i))" by auto
- also have "\<dots> = ?c x n" by auto
+ also have "\<dots> = ?c x n" unfolding One_nat_def by auto
also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
finally show ?thesis .
next
@@ -2998,7 +3006,7 @@
hence m_plus: "2 * (m + 1) = n + 1" by auto
from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n. (?c x i)) - (\<Sum>i = 0..<n+1. (?c x i))" by auto
- also have "\<dots> = - ?c x n" by auto
+ also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto
finally show ?thesis .
qed
@@ -3011,7 +3019,9 @@
ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound)
hence "?diff 1 n \<le> ?a 1 n" by auto
}
- have "?a 1 ----> 0" unfolding LIMSEQ_rabs_zero power_one divide_inverse by (auto intro!: LIMSEQ_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
+ have "?a 1 ----> 0"
+ unfolding LIMSEQ_rabs_zero power_one divide_inverse One_nat_def
+ by (auto intro!: LIMSEQ_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
have "?diff 1 ----> 0"
proof (rule LIMSEQ_I)
fix r :: real assume "0 < r"
@@ -3031,7 +3041,7 @@
have "- (pi / 2) < 0" using pi_gt_zero by auto
have "- (2 * pi) < 0" using pi_gt_zero by auto
- have c_minus_minus: "\<And> i. ?c (- 1) i = - ?c 1 i" by auto
+ have c_minus_minus: "\<And> i. ?c (- 1) i = - ?c 1 i" unfolding One_nat_def by auto
have "arctan (- 1) = arctan (tan (-(pi / 4)))" unfolding tan_45 tan_minus ..
also have "\<dots> = - (pi / 4)" by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
@@ -3179,4 +3189,4 @@
apply (erule polar_ex2)
done
-end
+end
--- a/src/HOL/Word/BinGeneral.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Word/BinGeneral.thy Wed Feb 25 10:29:01 2009 +0000
@@ -433,7 +433,7 @@
"!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)"
apply (induct n)
apply clarsimp
- apply (subst zmod_zadd_left_eq)
+ apply (subst mod_add_left_eq)
apply (simp add: bin_last_mod)
apply (simp add: number_of_eq)
apply clarsimp
@@ -767,23 +767,23 @@
lemmas zpower_zmod' = zpower_zmod [where m="c" and y="k", standard]
lemmas brdmod1s' [symmetric] =
- zmod_zadd_left_eq zmod_zadd_right_eq
+ mod_add_left_eq mod_add_right_eq
zmod_zsub_left_eq zmod_zsub_right_eq
zmod_zmult1_eq zmod_zmult1_eq_rev
lemmas brdmods' [symmetric] =
zpower_zmod' [symmetric]
- trans [OF zmod_zadd_left_eq zmod_zadd_right_eq]
+ trans [OF mod_add_left_eq mod_add_right_eq]
trans [OF zmod_zsub_left_eq zmod_zsub_right_eq]
trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev]
zmod_uminus' [symmetric]
- zmod_zadd_left_eq [where b = "1"]
+ mod_add_left_eq [where b = "1::int"]
zmod_zsub_left_eq [where b = "1"]
lemmas bintr_arith1s =
- brdmod1s' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard]
+ brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
lemmas bintr_ariths =
- brdmods' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard]
+ brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p, standard]
--- a/src/HOL/Word/Num_Lemmas.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Word/Num_Lemmas.thy Wed Feb 25 10:29:01 2009 +0000
@@ -95,7 +95,7 @@
lemma z1pdiv2:
"(2 * b + 1) div 2 = (b::int)" by arith
-lemmas zdiv_le_dividend = xtr3 [OF zdiv_1 [symmetric] zdiv_mono2,
+lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2,
simplified int_one_le_iff_zero_less, simplified, standard]
lemma axxbyy:
@@ -127,12 +127,12 @@
lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
apply (unfold diff_int_def)
- apply (rule trans [OF _ zmod_zadd_right_eq [symmetric]])
- apply (simp add : zmod_uminus zmod_zadd_right_eq [symmetric])
+ apply (rule trans [OF _ mod_add_right_eq [symmetric]])
+ apply (simp add : zmod_uminus mod_add_right_eq [symmetric])
done
lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c"
- by (rule zmod_zadd_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
+ by (rule mod_add_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
lemma zmod_zsub_self [simp]:
"((b :: int) - a) mod a = b mod a"
@@ -146,8 +146,8 @@
done
lemmas rdmods [symmetric] = zmod_uminus [symmetric]
- zmod_zsub_left_eq zmod_zsub_right_eq zmod_zadd_left_eq
- zmod_zadd_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
+ zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq
+ mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
lemma mod_plus_right:
"((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"
@@ -169,7 +169,8 @@
lemmas push_mods = push_mods' [THEN eq_reflection, standard]
lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard]
lemmas mod_simps =
- zmod_zmult_self1 [THEN eq_reflection] zmod_zmult_self2 [THEN eq_reflection]
+ mod_mult_self2_is_0 [THEN eq_reflection]
+ mod_mult_self1_is_0 [THEN eq_reflection]
mod_mod_trivial [THEN eq_reflection]
lemma nat_mod_eq:
@@ -313,7 +314,7 @@
"a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)"
apply clarsimp
apply safe
- apply (simp add: zdvd_iff_zmod_eq_0 [symmetric])
+ apply (simp add: dvd_eq_mod_eq_0 [symmetric])
apply (drule le_iff_add [THEN iffD1])
apply (force simp: zpower_zadd_distrib)
apply (rule mod_pos_pos_trivial)
--- a/src/HOL/Word/WordGenLib.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Word/WordGenLib.thy Wed Feb 25 10:29:01 2009 +0000
@@ -273,7 +273,7 @@
have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
show ?thesis
apply (subst x)
- apply (subst word_uint.Abs_norm [symmetric], subst zmod_zadd_self2)
+ apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
apply simp
done
qed
--- a/src/HOL/Word/WordShift.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/Word/WordShift.thy Wed Feb 25 10:29:01 2009 +0000
@@ -530,7 +530,7 @@
done
lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
- apply (simp add: zdvd_iff_zmod_eq_0 and_mask_mod_2p)
+ apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs)
apply (subst word_uint.norm_Rep [symmetric])
apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
--- a/src/HOL/ex/Eval_Examples.thy Wed Feb 25 10:28:49 2009 +0000
+++ b/src/HOL/ex/Eval_Examples.thy Wed Feb 25 10:29:01 2009 +0000
@@ -1,6 +1,4 @@
-(* ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
+(* Author: Florian Haftmann, TU Muenchen *)
header {* Small examples for evaluation mechanisms *}
--- a/src/Pure/Isar/code.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/Pure/Isar/code.ML Wed Feb 25 10:29:01 2009 +0000
@@ -35,7 +35,7 @@
val these_raw_eqns: theory -> string -> (thm * bool) list
val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
val get_datatype_of_constr: theory -> string -> string option
- val get_case_scheme: theory -> string -> (int * string list) option
+ val get_case_scheme: theory -> string -> (int * (int * string list)) option
val is_undefined: theory -> string -> bool
val default_typscheme: theory -> string -> (string * sort) list * typ
@@ -111,7 +111,7 @@
(** logical and syntactical specification of executable code **)
-(* defining equations *)
+(* code equations *)
type eqns = bool * (thm * bool) list lazy;
(*default flag, theorems with linear flag (perhaps lazy)*)
@@ -136,7 +136,7 @@
Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
fun drop (thm', linear') = if (linear orelse not linear')
andalso matches_args (args_of thm') then
- (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); true)
+ (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true)
else false;
in (thm, linear) :: filter_out drop thms end;
@@ -157,7 +157,7 @@
(*with explicit history*),
dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table
(*with explicit history*),
- cases: (int * string list) Symtab.table * unit Symtab.table
+ cases: (int * (int * string list)) Symtab.table * unit Symtab.table
};
fun mk_spec ((concluded_history, eqns), (dtyps, cases)) =
@@ -409,7 +409,7 @@
in
(Pretty.writeln o Pretty.chunks) [
Pretty.block (
- Pretty.str "defining equations:"
+ Pretty.str "code equations:"
:: Pretty.fbrk
:: (Pretty.fbreaks o map pretty_eqn) eqns
),
@@ -452,7 +452,7 @@
val ty1 :: tys = map (snd o Code_Unit.const_typ_eqn) thms';
fun unify ty env = Sign.typ_unify thy (ty1, ty) env
handle Type.TUNIFY =>
- error ("Type unificaton failed, while unifying defining equations\n"
+ error ("Type unificaton failed, while unifying code equations\n"
^ (cat_lines o map Display.string_of_thm) thms
^ "\nwith types\n"
^ (cat_lines o map (Code_Unit.string_of_typ thy)) (ty1 :: tys));
@@ -463,7 +463,7 @@
fun check_linear (eqn as (thm, linear)) =
if linear then eqn else Code_Unit.bad_thm
- ("Duplicate variables on left hand side of defining equation:\n"
+ ("Duplicate variables on left hand side of code equation:\n"
^ Display.string_of_thm thm);
fun mk_eqn thy linear =
@@ -489,7 +489,7 @@
fun retrieve_algebra thy operational =
Sorts.subalgebra (Syntax.pp_global thy) operational
- (arity_constraints thy (Sign.classes_of thy))
+ (SOME o arity_constraints thy (Sign.classes_of thy))
(Sign.classes_of thy);
in
@@ -525,22 +525,13 @@
then SOME tyco else NONE
| _ => NONE;
-fun get_constr_typ thy c =
- case get_datatype_of_constr thy c
- of SOME tyco => let
- val (vs, cos) = get_datatype thy tyco;
- val SOME tys = AList.lookup (op =) cos c;
- val ty = tys ---> Type (tyco, map TFree vs);
- in SOME (Logic.varifyT ty) end
- | NONE => NONE;
-
fun recheck_eqn thy = Code_Unit.error_thm
(Code_Unit.assert_linear (is_some o get_datatype_of_constr thy) o apfst (Code_Unit.assert_eqn thy));
fun recheck_eqns_const thy c eqns =
let
fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
- then eqn else error ("Wrong head of defining equation,\nexpected constant "
+ then eqn else error ("Wrong head of code equation,\nexpected constant "
^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
in map (cert o recheck_eqn thy) eqns end;
@@ -554,11 +545,11 @@
let
val c = Code_Unit.const_eqn thm;
val _ = if not default andalso (is_some o AxClass.class_of_param thy) c
- then error ("Rejected polymorphic equation for overloaded constant:\n"
+ then error ("Rejected polymorphic code equation for overloaded constant:\n"
^ Display.string_of_thm thm)
else ();
val _ = if not default andalso (is_some o get_datatype_of_constr thy) c
- then error ("Rejected equation for datatype constructor:\n"
+ then error ("Rejected code equation for datatype constructor:\n"
^ Display.string_of_thm thm)
else ();
in change_eqns false c (add_thm thy default (thm, linear)) thy end
@@ -593,11 +584,17 @@
let
val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
val (tyco, vs_cos) = Code_Unit.constrset_of_consts thy cs;
+ val old_cs = (map fst o snd o get_datatype thy) tyco;
+ fun drop_outdated_cases cases = fold Symtab.delete_safe
+ (Symtab.fold (fn (c, (_, (_, cos))) =>
+ if exists (member (op =) old_cs) cos
+ then insert (op =) c else I) cases []) cases;
in
thy
|> map_exec_purge NONE
((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
- #> map_eqns (fold (Symtab.delete_safe o fst) cs))
+ #> map_eqns (fold (Symtab.delete_safe o fst) cs)
+ #> (map_cases o apfst) drop_outdated_cases)
|> TypeInterpretation.data (tyco, serial ())
end;
@@ -611,10 +608,12 @@
fun add_case thm thy =
let
- val entry as (c, _) = Code_Unit.case_cert thm;
- in
- (map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update entry) thy
- end;
+ val (c, (k, case_pats)) = Code_Unit.case_cert thm;
+ val _ = case filter (is_none o get_datatype_of_constr thy) case_pats
+ of [] => ()
+ | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
+ val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
+ in (map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update (c, entry)) thy end;
fun add_undefined c thy =
(map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy;
@@ -727,18 +726,16 @@
fun default_typscheme thy c =
let
- val typscheme = curry (Code_Unit.typscheme thy) c
- val the_const_type = snd o dest_Const o TermSubst.zero_var_indexes
- o curry Const "" o Sign.the_const_type thy;
+ fun the_const_typscheme c = (curry (Code_Unit.typscheme thy) c o snd o dest_Const
+ o TermSubst.zero_var_indexes o curry Const "" o Sign.the_const_type thy) c;
+ fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty);
in case AxClass.class_of_param thy c
- of SOME class => the_const_type c
- |> Term.map_type_tvar (K (TVar ((Name.aT, 0), [class])))
- |> typscheme
- | NONE => (case get_constr_typ thy c
- of SOME ty => typscheme ty
- | NONE => (case get_eqns thy c
- of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm))
- | [] => typscheme (the_const_type c))) end;
+ of SOME class => ([(Name.aT, [class])], snd (the_const_typscheme c))
+ | NONE => if is_some (get_datatype_of_constr thy c)
+ then strip_sorts (the_const_typscheme c)
+ else case get_eqns thy c
+ of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm))
+ | [] => strip_sorts (the_const_typscheme c) end;
end; (*local*)
--- a/src/Pure/Isar/code_unit.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/Pure/Isar/code_unit.ML Wed Feb 25 10:29:01 2009 +0000
@@ -34,7 +34,7 @@
val constrset_of_consts: theory -> (string * typ) list
-> string * ((string * sort) list * (string * typ list) list)
- (*defining equations*)
+ (*code equations*)
val assert_eqn: theory -> thm -> thm
val mk_eqn: theory -> thm -> thm * bool
val assert_linear: (string -> bool) -> thm * bool -> thm * bool
@@ -76,10 +76,11 @@
fun typscheme thy (c, ty) =
let
- fun dest (TVar ((v, 0), sort)) = (v, sort)
+ val ty' = Logic.unvarifyT ty;
+ fun dest (TFree (v, sort)) = (v, sort)
| dest ty = error ("Illegal type parameter in type scheme: " ^ Syntax.string_of_typ_global thy ty);
- val vs = map dest (Sign.const_typargs thy (c, ty));
- in (vs, ty) end;
+ val vs = map dest (Sign.const_typargs thy (c, ty'));
+ in (vs, Type.strip_sorts ty') end;
fun inst_thm thy tvars' thm =
let
@@ -313,10 +314,10 @@
val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
val vs = Name.names Name.context Name.aT sorts;
val cs''' = map (inst vs) cs'';
- in (tyco, (vs, cs''')) end;
+ in (tyco, (vs, rev cs''')) end;
-(* defining equations *)
+(* code equations *)
fun assert_eqn thy thm =
let
@@ -351,7 +352,7 @@
^ Display.string_of_thm thm)
| check 0 (Var _) = ()
| check _ (Var _) = bad_thm
- ("Variable with application on left hand side of defining equation\n"
+ ("Variable with application on left hand side of code equation\n"
^ Display.string_of_thm thm)
| check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
| check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
@@ -363,7 +364,7 @@
val ty_decl = Sign.the_const_type thy c;
val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
then () else bad_thm ("Type\n" ^ string_of_typ thy ty
- ^ "\nof defining equation\n"
+ ^ "\nof code equation\n"
^ Display.string_of_thm thm
^ "\nis incompatible with declared function type\n"
^ string_of_typ thy ty_decl)
@@ -388,7 +389,7 @@
fun assert_linear is_cons (thm, false) = (thm, false)
| assert_linear is_cons (thm, true) = if snd (add_linear (assert_pat is_cons thm)) then (thm, true)
else bad_thm
- ("Duplicate variables on left hand side of defining equation:\n"
+ ("Duplicate variables on left hand side of code equation:\n"
^ Display.string_of_thm thm);
--- a/src/Pure/sorts.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/Pure/sorts.ML Wed Feb 25 10:29:01 2009 +0000
@@ -46,9 +46,7 @@
val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
val empty_algebra: algebra
val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
- val classrels_of: algebra -> (class * class list) list
- val instances_of: algebra -> (string * class) list
- val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list)
+ val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list option)
-> algebra -> (sort -> sort) * algebra
type class_error
val class_error: Pretty.pp -> class_error -> string
@@ -302,29 +300,14 @@
(* algebra projections *)
-val sorted_classes = rev o flat o Graph.strong_conn o classes_of;
-
-fun classrels_of algebra =
- map (fn c => (c, Graph.imm_succs (classes_of algebra) c)) (sorted_classes algebra);
-
-fun instances_of algebra =
- let
- val arities = arities_of algebra;
- val all_classes = sorted_classes algebra;
- fun sort_classes cs = filter (member (op = o apsnd fst) cs)
- all_classes;
- in
- Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs))
- arities []
- end;
-
fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
let
val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
fun restrict_arity tyco (c, (_, Ss)) =
- if P c then
- SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) (sargs (c, tyco))
+ if P c then case sargs (c, tyco)
+ of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
|> map restrict_sort))
+ | NONE => NONE
else NONE;
val classes' = classes |> Graph.subgraph P;
val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
--- a/src/Tools/code/code_funcgr.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/Tools/code/code_funcgr.ML Wed Feb 25 10:29:01 2009 +0000
@@ -317,13 +317,13 @@
in
val _ =
- OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag
+ OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
(Scan.repeat P.term_group
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
val _ =
- OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag
+ OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
(Scan.repeat P.term_group
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
--- a/src/Tools/code/code_funcgr_new.ML Wed Feb 25 10:28:49 2009 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,401 +0,0 @@
-(* Title: Tools/code/code_funcgr.ML
- Author: Florian Haftmann, TU Muenchen
-
-Retrieving, well-sorting and structuring code equations in graph
-with explicit dependencies -- the waisenhaus algorithm.
-*)
-
-signature CODE_FUNCGR =
-sig
- type T
- val eqns: T -> string -> (thm * bool) list
- val typ: T -> string -> (string * sort) list * typ
- val all: T -> string list
- val pretty: theory -> T -> Pretty.T
- val make: theory -> string list
- -> ((sort -> sort) * Sorts.algebra) * T
- val eval_conv: theory
- -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
- val eval_term: theory
- -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
-end
-
-structure Code_Funcgr : CODE_FUNCGR =
-struct
-
-(** the graph type **)
-
-type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
-
-fun eqns funcgr = these o Option.map snd o try (Graph.get_node funcgr);
-fun typ funcgr = fst o Graph.get_node funcgr;
-fun all funcgr = Graph.keys funcgr;
-
-fun pretty thy funcgr =
- AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr)
- |> (map o apfst) (Code_Unit.string_of_const thy)
- |> sort (string_ord o pairself fst)
- |> map (fn (s, thms) =>
- (Pretty.block o Pretty.fbreaks) (
- Pretty.str s
- :: map (Display.pretty_thm o fst) thms
- ))
- |> Pretty.chunks;
-
-
-(** graph algorithm **)
-
-(* generic *)
-
-fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
-
-fun complete_proper_sort thy =
- Sign.complete_sort thy #> filter (can (AxClass.get_info thy));
-
-fun inst_params thy tyco class =
- map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
- ((#params o AxClass.get_info thy) class);
-
-fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
- (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
- (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
-
-fun lhs_rhss_of thy c =
- let
- val eqns = Code.these_eqns thy c
- |> burrow_fst (Code_Unit.norm_args thy)
- |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
- val (lhs, _) = case eqns of [] => Code.default_typscheme thy c
- | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm;
- val rhss = consts_of thy eqns;
- in (lhs, rhss) end;
-
-
-(* data structures *)
-
-datatype const = Fun of string | Inst of class * string;
-
-fun const_ord (Fun c1, Fun c2) = fast_string_ord (c1, c2)
- | const_ord (Inst class_tyco1, Inst class_tyco2) =
- prod_ord fast_string_ord fast_string_ord (class_tyco1, class_tyco2)
- | const_ord (Fun _, Inst _) = LESS
- | const_ord (Inst _, Fun _) = GREATER;
-
-type var = const * int;
-
-structure Vargraph =
- GraphFun(type key = var val ord = prod_ord const_ord int_ord);
-
-datatype styp = Tyco of string * styp list | Var of var;
-
-type vardeps = const list * ((string * styp list) list * class list) Vargraph.T;
-
-
-(* computing instantiations -- FIXME does not consider existing things *)
-
-fun add_classes thy c_k new_classes vardeps =
- let
- val _ = tracing "add_classes";
- val (styps, old_classes) = Vargraph.get_node (snd vardeps) c_k;
- val diff_classes = new_classes |> subtract (op =) old_classes;
- in if null diff_classes then vardeps
- else let
- val c_ks = Vargraph.imm_succs (snd vardeps) c_k |> insert (op =) c_k;
- in
- vardeps
- |> (apsnd o Vargraph.map_node c_k o apsnd) (append diff_classes)
- |> fold (fn styp => fold (add_typmatch_inst thy styp) new_classes) styps
- |> fold (fn c_k => add_classes thy c_k diff_classes) c_ks
- end end
-and add_styp thy c_k tyco_styps vardeps =
- let
- val _ = tracing "add_styp";
- val (old_styps, classes) = Vargraph.get_node (snd vardeps) c_k;
- in if member (op =) old_styps tyco_styps then vardeps
- else
- vardeps
- |> (apsnd o Vargraph.map_node c_k o apfst) (cons tyco_styps)
- |> fold (add_typmatch_inst thy tyco_styps) classes
- end
-and add_dep thy c_k c_k' vardeps =
- let
- val _ = tracing ("add_dep " ^ makestring c_k ^ " -> " ^ makestring c_k');
- val (_, classes) = Vargraph.get_node (snd vardeps) c_k;
- in
- vardeps
- |> add_classes thy c_k' classes
- |> apsnd (Vargraph.add_edge (c_k, c_k'))
- end
-and add_typmatch_inst thy (tyco, styps) class vardeps = if can (Sign.arity_sorts thy tyco) [class]
- then vardeps
- |> tap (fn _ => tracing "add_typmatch_inst")
- |> assert thy (Inst (class, tyco))
- |> fold_index (fn (k, styp) =>
- add_typmatch thy styp (Inst (class, tyco), k)) styps
- else vardeps (*permissive!*)
-and add_typmatch thy (Var c_k') c_k vardeps =
- vardeps
- |> tap (fn _ => tracing "add_typmatch (Inst)")
- |> add_dep thy c_k c_k'
- | add_typmatch thy (Tyco tyco_styps) c_k vardeps =
- vardeps
- |> tap (fn _ => tracing "add_typmatch (Tyco)")
- |> add_styp thy c_k tyco_styps
-and add_inst thy (class, tyco) vardeps =
- let
- val _ = tracing ("add_inst " ^ tyco ^ "::" ^ class);
- val superclasses = complete_proper_sort thy
- (Sign.super_classes thy class);
- val classess = map (complete_proper_sort thy)
- (Sign.arity_sorts thy tyco [class]);
- val inst_params = inst_params thy tyco class;
- (*FIXME also consider existing things here*)
- in
- vardeps
- |> fold (fn superclass => assert thy (Inst (superclass, tyco))) superclasses
- |> fold (assert thy o Fun) inst_params
- |> fold_index (fn (k, classes) =>
- apsnd (Vargraph.default_node ((Inst (class, tyco), k), ([] ,[])))
- #> add_classes thy (Inst (class, tyco), k) classes
- #> fold (fn superclass =>
- add_dep thy (Inst (superclass, tyco), k)
- (Inst (class, tyco), k)) superclasses
- #> fold (fn inst_param =>
- add_dep thy (Fun inst_param, k)
- (Inst (class, tyco), k)
- ) inst_params
- ) classess
- end
-and add_const thy c vardeps =
- let
- val _ = tracing "add_const";
- val (lhs, rhss) = lhs_rhss_of thy c;
- (*FIXME build lhs_rhss_of such that it points to existing graph if possible*)
- fun styp_of (Type (tyco, tys)) = Tyco (tyco, map styp_of tys)
- | styp_of (TFree (v, _)) = Var (Fun c, find_index (fn (v', _) => v = v') lhs);
- val rhss' = (map o apsnd o map) styp_of rhss;
- in
- vardeps
- |> fold_index (fn (k, (_, sort)) =>
- apsnd (Vargraph.default_node ((Fun c, k), ([] ,[])))
- #> add_classes thy (Fun c, k) (complete_proper_sort thy sort)) lhs
- |> fold (assert thy o Fun o fst) rhss'
- |> fold (fn (c', styps) => fold_index (fn (k', styp) =>
- add_typmatch thy styp (Fun c', k')) styps) rhss'
- end
-and assert thy c (vardeps as (asserted, _)) =
- if member (op =) asserted c then vardeps
- else case c
- of Fun const => vardeps |> apfst (cons c) |> add_const thy const
- | Inst inst => vardeps |> apfst (cons c) |> add_inst thy inst;
-
-
-(* applying instantiations *)
-
-fun dicts_of thy (proj_sort, algebra) (T, sort) =
- let
- fun class_relation (x, _) _ = x;
- fun type_constructor tyco xs class =
- inst_params thy tyco class @ (maps o maps) fst xs;
- fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
- in
- flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
- { class_relation = class_relation, type_constructor = type_constructor,
- type_variable = type_variable } (T, proj_sort sort)
- handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
- end;
-
-fun algebra_of thy vardeps =
- let
- val pp = Syntax.pp_global thy;
- val thy_algebra = Sign.classes_of thy;
- val is_proper = can (AxClass.get_info thy);
- val classrels = Sorts.classrels_of thy_algebra
- |> filter (is_proper o fst)
- |> (map o apsnd) (filter is_proper);
- val instances = Sorts.instances_of thy_algebra
- |> filter (is_proper o snd);
- fun add_class (class, superclasses) algebra =
- Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;
- val arity_constraints = Vargraph.fold (fn ((Fun _, _), _) => I
- | ((Inst (class, tyco), k), ((_, classes), _)) =>
- AList.map_default (op =)
- ((tyco, class), replicate (Sign.arity_number thy tyco) [])
- (nth_map k (K classes))) vardeps [];
- fun add_arity (tyco, class) algebra =
- case AList.lookup (op =) arity_constraints (tyco, class)
- of SOME sorts => (tracing (Pretty.output (Syntax.pretty_arity (ProofContext.init thy)
- (tyco, sorts, [class])));
- Sorts.add_arities pp
- (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra)
- | NONE => if Sign.arity_number thy tyco = 0
- then Sorts.add_arities pp (tyco, [(class, [])]) algebra
- else algebra;
- in
- Sorts.empty_algebra
- |> fold add_class classrels
- |> fold add_arity instances
- end;
-
-fun add_eqs thy (proj_sort, algebra) vardeps c gr =
- let
- val eqns = Code.these_eqns thy c
- |> burrow_fst (Code_Unit.norm_args thy)
- |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
- val (vs, _) = case eqns of [] => Code.default_typscheme thy c
- | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm;
- val inst = Vartab.empty |> fold_index (fn (k, (v, _)) =>
- Vartab.update ((v, 0), snd (Vargraph.get_node vardeps (Fun c, k)))) vs;
- val eqns' = eqns
- |> (map o apfst) (Code_Unit.inst_thm thy inst);
- val tyscm = case eqns' of [] => Code.default_typscheme thy c
- | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm;
- val _ = tracing ("tyscm " ^ makestring (map snd (fst tyscm)));
- val rhss = consts_of thy eqns';
- in
- gr
- |> Graph.new_node (c, (tyscm, eqns'))
- |> fold (fn (c', Ts) => ensure_eqs_dep thy (proj_sort, algebra) vardeps c c'
- #-> (fn (vs, _) =>
- fold2 (ensure_match thy (proj_sort, algebra) vardeps c) Ts (map snd vs))) rhss
- |> pair tyscm
- end
-and ensure_match thy (proj_sort, algebra) vardeps c T sort gr =
- gr
- |> fold (fn c' => ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' #> snd)
- (dicts_of thy (proj_sort, algebra) (T, proj_sort sort))
-and ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' gr =
- gr
- |> ensure_eqs thy (proj_sort, algebra) vardeps c'
- ||> Graph.add_edge (c, c')
-and ensure_eqs thy (proj_sort, algebra) vardeps c gr =
- case try (Graph.get_node gr) c
- of SOME (tyscm, _) => (tyscm, gr)
- | NONE => add_eqs thy (proj_sort, algebra) vardeps c gr;
-
-fun extend_graph thy cs gr =
- let
- val _ = tracing ("extending with " ^ commas cs);
- val _ = tracing "obtaining instantiations";
- val (_, vardeps) = fold (assert thy o Fun) cs ([], Vargraph.empty)
- val _ = tracing "obtaining algebra";
- val algebra = algebra_of thy vardeps;
- val _ = tracing "obtaining equations";
- val proj_sort = complete_proper_sort thy #> Sorts.minimize_sort algebra;
- val (_, gr') = fold_map (ensure_eqs thy (proj_sort, algebra) vardeps) cs gr;
- val _ = tracing "sort projection";
- in ((proj_sort, algebra), gr') end;
-
-
-(** retrieval interfaces **)
-
-fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct funcgr =
- let
- val ct = cterm_of proto_ct;
- val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
- val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
- fun consts_of t =
- fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
- val thm = Code.preprocess_conv thy ct;
- val ct' = Thm.rhs_of thm;
- val t' = Thm.term_of ct';
- val consts = map fst (consts_of t');
- val (algebra', funcgr') = extend_graph thy consts funcgr;
- val (t'', evaluator_funcgr) = evaluator t';
- val consts' = consts_of t'';
- val const_matches = fold (fn (c, ty) =>
- insert (op =) (Sign.const_typargs thy (c, Logic.unvarifyT ty), c)) consts' [];
- val typ_matches = maps (fn (tys, c) => tys ~~ map snd (fst (fst (Graph.get_node funcgr' c))))
- const_matches;
- val dicts = maps (dicts_of thy algebra') typ_matches;
- val (algebra'', funcgr'') = extend_graph thy dicts funcgr';
- in (evaluator_lift (evaluator_funcgr algebra'') thm funcgr'', funcgr'') end;
-
-fun proto_eval_conv thy =
- let
- fun evaluator_lift evaluator thm1 funcgr =
- let
- val thm2 = evaluator funcgr;
- val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
- in
- Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
- error ("could not construct evaluation proof:\n"
- ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
- end;
- in proto_eval thy I evaluator_lift end;
-
-fun proto_eval_term thy =
- let
- fun evaluator_lift evaluator _ funcgr = evaluator funcgr;
- in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
-
-structure Funcgr = CodeDataFun
-(
- type T = T;
- val empty = Graph.empty;
- fun purge _ cs funcgr =
- Graph.del_nodes ((Graph.all_preds funcgr
- o filter (can (Graph.get_node funcgr))) cs) funcgr;
-);
-
-fun make thy = Funcgr.change_yield thy o extend_graph thy;
-
-fun eval_conv thy f =
- fst o Funcgr.change_yield thy o proto_eval_conv thy f;
-
-fun eval_term thy f =
- fst o Funcgr.change_yield thy o proto_eval_term thy f;
-
-
-(** diagnostic commands **)
-
-fun code_depgr thy consts =
- let
- val (_, gr) = make thy consts;
- val select = Graph.all_succs gr consts;
- in
- gr
- |> not (null consts) ? Graph.subgraph (member (op =) select)
- |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
- end;
-
-fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
-
-fun code_deps thy consts =
- let
- val gr = code_depgr thy consts;
- fun mk_entry (const, (_, (_, parents))) =
- let
- val name = Code_Unit.string_of_const thy const;
- val nameparents = map (Code_Unit.string_of_const thy) parents;
- in { name = name, ID = name, dir = "", unfold = true,
- path = "", parents = nameparents }
- end;
- val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
- in Present.display_graph prgr end;
-
-local
-
-structure P = OuterParse
-and K = OuterKeyword
-
-fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
-fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
-
-in
-
-val _ =
- OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag
- (Scan.repeat P.term_group
- >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
- o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
-
-val _ =
- OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag
- (Scan.repeat P.term_group
- >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
- o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
-
-end;
-
-end; (*struct*)
--- a/src/Tools/code/code_target.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/Tools/code/code_target.ML Wed Feb 25 10:29:01 2009 +0000
@@ -418,7 +418,7 @@
val program4 = Graph.subgraph (member (op =) names_all) program3;
val empty_funs = filter_out (member (op =) abortable)
(Code_Thingol.empty_funs program3);
- val _ = if null empty_funs then () else error ("No defining equations for "
+ val _ = if null empty_funs then () else error ("No code equations for "
^ commas (map (Sign.extern_const thy) empty_funs));
in
serializer module args (labelled_name thy program2) reserved includes
--- a/src/Tools/code/code_thingol.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/Tools/code/code_thingol.ML Wed Feb 25 10:29:01 2009 +0000
@@ -453,7 +453,7 @@
let
val err_class = Sorts.class_error (Syntax.pp_global thy) e;
val err_thm = case thm
- of SOME thm => "\n(in defining equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
+ of SOME thm => "\n(in code equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
^ Syntax.string_of_sort_global thy sort;
in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
@@ -495,9 +495,8 @@
and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
#>> (fn sort => (unprefix "'" v, sort))
-and translate_typ thy algbr funcgr (TFree v_sort) =
- translate_tyvar_sort thy algbr funcgr v_sort
- #>> (fn (v, sort) => ITyVar v)
+and translate_typ thy algbr funcgr (TFree (v, _)) =
+ pair (ITyVar (unprefix "'" v))
| translate_typ thy algbr funcgr (Type (tyco, tys)) =
ensure_tyco thy algbr funcgr tyco
##>> fold_map (translate_typ thy algbr funcgr) tys
@@ -583,9 +582,8 @@
fun stmt_classparam class =
ensure_class thy algbr funcgr class
#>> (fn class => Classparam (c, class));
- fun stmt_fun ((vs, raw_ty), raw_thms) =
+ fun stmt_fun ((vs, ty), raw_thms) =
let
- val ty = Logic.unvarifyT raw_ty;
val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
then raw_thms
else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
@@ -644,11 +642,6 @@
val ts_clause = nth_drop t_pos ts;
fun mk_clause (co, num_co_args) t =
let
- val _ = if (is_some o Code.get_datatype_of_constr thy) co then ()
- else error ("Non-constructor " ^ quote co
- ^ " encountered in case pattern"
- ^ (case thm of NONE => ""
- | SOME thm => ", in equation\n" ^ Display.string_of_thm thm))
val (vs, body) = Term.strip_abs_eta num_co_args t;
val not_undefined = case body
of (Const (c, _)) => not (Code.is_undefined thy c)
@@ -703,9 +696,7 @@
translate_case thy algbr funcgr thm case_scheme ((c, ty), ts)
and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) =
case Code.get_case_scheme thy c
- of SOME (base_case_scheme as (_, case_pats)) =>
- translate_app_case thy algbr funcgr thm
- (1 + Int.max (1, length case_pats), base_case_scheme) c_ty_ts
+ of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts
| NONE => translate_app_const thy algbr funcgr thm c_ty_ts;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/code/code_wellsorted.ML Wed Feb 25 10:29:01 2009 +0000
@@ -0,0 +1,390 @@
+(* Title: Tools/code/code_wellsorted.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Producing well-sorted systems of code equations in a graph
+with explicit dependencies -- the Waisenhaus algorithm.
+*)
+
+signature CODE_FUNCGR =
+sig
+ type T
+ val eqns: T -> string -> (thm * bool) list
+ val typ: T -> string -> (string * sort) list * typ
+ val all: T -> string list
+ val pretty: theory -> T -> Pretty.T
+ val make: theory -> string list
+ -> ((sort -> sort) * Sorts.algebra) * T
+ val eval_conv: theory
+ -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
+ val eval_term: theory
+ -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
+end
+
+structure Code_Funcgr : CODE_FUNCGR =
+struct
+
+(** the equation graph type **)
+
+type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
+
+fun eqns eqngr = these o Option.map snd o try (Graph.get_node eqngr);
+fun typ eqngr = fst o Graph.get_node eqngr;
+fun all eqngr = Graph.keys eqngr;
+
+fun pretty thy eqngr =
+ AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
+ |> (map o apfst) (Code_Unit.string_of_const thy)
+ |> sort (string_ord o pairself fst)
+ |> map (fn (s, thms) =>
+ (Pretty.block o Pretty.fbreaks) (
+ Pretty.str s
+ :: map (Display.pretty_thm o fst) thms
+ ))
+ |> Pretty.chunks;
+
+
+(** the Waisenhaus algorithm **)
+
+(* auxiliary *)
+
+fun complete_proper_sort thy =
+ Sign.complete_sort thy #> filter (can (AxClass.get_info thy));
+
+fun inst_params thy tyco =
+ map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
+ o maps (#params o AxClass.get_info thy);
+
+fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
+ (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
+ (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
+
+fun tyscm_rhss_of thy c eqns =
+ let
+ val tyscm = case eqns of [] => Code.default_typscheme thy c
+ | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm;
+ val rhss = consts_of thy eqns;
+ in (tyscm, rhss) end;
+
+
+(* data structures *)
+
+datatype const = Fun of string | Inst of class * string;
+
+fun const_ord (Fun c1, Fun c2) = fast_string_ord (c1, c2)
+ | const_ord (Inst class_tyco1, Inst class_tyco2) =
+ prod_ord fast_string_ord fast_string_ord (class_tyco1, class_tyco2)
+ | const_ord (Fun _, Inst _) = LESS
+ | const_ord (Inst _, Fun _) = GREATER;
+
+type var = const * int;
+
+structure Vargraph =
+ GraphFun(type key = var val ord = prod_ord const_ord int_ord);
+
+datatype styp = Tyco of string * styp list | Var of var | Free;
+
+fun styp_of c_lhs (Type (tyco, tys)) = Tyco (tyco, map (styp_of c_lhs) tys)
+ | styp_of c_lhs (TFree (v, _)) = case c_lhs
+ of SOME (c, lhs) => Var (Fun c, find_index (fn (v', _) => v = v') lhs)
+ | NONE => Free;
+
+type vardeps_data = ((string * styp list) list * class list) Vargraph.T
+ * (((string * sort) list * (thm * bool) list) Symtab.table
+ * (class * string) list);
+
+val empty_vardeps_data : vardeps_data =
+ (Vargraph.empty, (Symtab.empty, []));
+
+(* retrieving equations and instances from the background context *)
+
+fun obtain_eqns thy eqngr c =
+ case try (Graph.get_node eqngr) c
+ of SOME ((lhs, _), eqns) => ((lhs, []), [])
+ | NONE => let
+ val eqns = Code.these_eqns thy c
+ |> burrow_fst (Code_Unit.norm_args thy)
+ |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
+ val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns;
+ in ((lhs, rhss), eqns) end;
+
+fun obtain_instance thy arities (inst as (class, tyco)) =
+ case AList.lookup (op =) arities inst
+ of SOME classess => (classess, ([], []))
+ | NONE => let
+ val all_classes = complete_proper_sort thy [class];
+ val superclasses = remove (op =) class all_classes
+ val classess = map (complete_proper_sort thy)
+ (Sign.arity_sorts thy tyco [class]);
+ val inst_params = inst_params thy tyco all_classes;
+ in (classess, (superclasses, inst_params)) end;
+
+
+(* computing instantiations *)
+
+fun add_classes thy arities eqngr c_k new_classes vardeps_data =
+ let
+ val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
+ val diff_classes = new_classes |> subtract (op =) old_classes;
+ in if null diff_classes then vardeps_data
+ else let
+ val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k;
+ in
+ vardeps_data
+ |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
+ |> fold (fn styp => fold (assert_typmatch_inst thy arities eqngr styp) new_classes) styps
+ |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
+ end end
+and add_styp thy arities eqngr c_k tyco_styps vardeps_data =
+ let
+ val (old_styps, classes) = Vargraph.get_node (fst vardeps_data) c_k;
+ in if member (op =) old_styps tyco_styps then vardeps_data
+ else
+ vardeps_data
+ |> (apfst o Vargraph.map_node c_k o apfst) (cons tyco_styps)
+ |> fold (assert_typmatch_inst thy arities eqngr tyco_styps) classes
+ end
+and add_dep thy arities eqngr c_k c_k' vardeps_data =
+ let
+ val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k;
+ in
+ vardeps_data
+ |> add_classes thy arities eqngr c_k' classes
+ |> apfst (Vargraph.add_edge (c_k, c_k'))
+ end
+and assert_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
+ if can (Sign.arity_sorts thy tyco) [class]
+ then vardeps_data
+ |> assert_inst thy arities eqngr (class, tyco)
+ |> fold_index (fn (k, styp) =>
+ assert_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
+ else vardeps_data (*permissive!*)
+and assert_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
+ if member (op =) insts inst then vardeps_data
+ else let
+ val (classess, (superclasses, inst_params)) =
+ obtain_instance thy arities inst;
+ in
+ vardeps_data
+ |> (apsnd o apsnd) (insert (op =) inst)
+ |> fold_index (fn (k, _) =>
+ apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess
+ |> fold (fn superclass => assert_inst thy arities eqngr (superclass, tyco)) superclasses
+ |> fold (assert_fun thy arities eqngr) inst_params
+ |> fold_index (fn (k, classes) =>
+ add_classes thy arities eqngr (Inst (class, tyco), k) classes
+ #> fold (fn superclass =>
+ add_dep thy arities eqngr (Inst (superclass, tyco), k)
+ (Inst (class, tyco), k)) superclasses
+ #> fold (fn inst_param =>
+ add_dep thy arities eqngr (Fun inst_param, k)
+ (Inst (class, tyco), k)
+ ) inst_params
+ ) classess
+ end
+and assert_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
+ vardeps_data
+ |> add_styp thy arities eqngr c_k tyco_styps
+ | assert_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
+ vardeps_data
+ |> add_dep thy arities eqngr c_k c_k'
+ | assert_typmatch thy arities eqngr Free c_k vardeps_data =
+ vardeps_data
+and assert_rhs thy arities eqngr (c', styps) vardeps_data =
+ vardeps_data
+ |> assert_fun thy arities eqngr c'
+ |> fold_index (fn (k, styp) =>
+ assert_typmatch thy arities eqngr styp (Fun c', k)) styps
+and assert_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) =
+ if Symtab.defined eqntab c then vardeps_data
+ else let
+ val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
+ val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
+ in
+ vardeps_data
+ |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
+ |> fold_index (fn (k, _) =>
+ apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs
+ |> fold_index (fn (k, (_, sort)) =>
+ add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
+ |> fold (assert_rhs thy arities eqngr) rhss'
+ end;
+
+
+(* applying instantiations *)
+
+fun dicts_of thy (proj_sort, algebra) (T, sort) =
+ let
+ fun class_relation (x, _) _ = x;
+ fun type_constructor tyco xs class =
+ inst_params thy tyco (Sorts.complete_sort algebra [class])
+ @ (maps o maps) fst xs;
+ fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
+ in
+ flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
+ { class_relation = class_relation, type_constructor = type_constructor,
+ type_variable = type_variable } (T, proj_sort sort)
+ handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
+ end;
+
+fun add_arity thy vardeps (class, tyco) =
+ AList.default (op =)
+ ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
+ (0 upto Sign.arity_number thy tyco - 1));
+
+fun add_eqs thy (proj_sort, algebra) vardeps
+ (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
+ if can (Graph.get_node eqngr) c then (rhss, eqngr)
+ else let
+ val lhs = map_index (fn (k, (v, _)) =>
+ (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
+ val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
+ Vartab.update ((v, 0), sort)) lhs;
+ val eqns = proto_eqns
+ |> (map o apfst) (Code_Unit.inst_thm thy inst_tab);
+ val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
+ val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
+ in (map (pair c) rhss' @ rhss, eqngr') end;
+
+fun extend_arities_eqngr thy cs cs_rhss (arities, eqngr) =
+ let
+ val cs_rhss' = (map o apsnd o map) (styp_of NONE) cs_rhss;
+ val (vardeps, (eqntab, insts)) = empty_vardeps_data
+ |> fold (assert_fun thy arities eqngr) cs
+ |> fold (assert_rhs thy arities eqngr) cs_rhss';
+ val arities' = fold (add_arity thy vardeps) insts arities;
+ val pp = Syntax.pp_global thy;
+ val is_proper_class = can (AxClass.get_info thy);
+ val (proj_sort, algebra) = Sorts.subalgebra pp is_proper_class
+ (AList.lookup (op =) arities') (Sign.classes_of thy);
+ val (rhss, eqngr') = Symtab.fold
+ (add_eqs thy (proj_sort, algebra) vardeps) eqntab ([], eqngr);
+ fun deps_of (c, rhs) = c ::
+ maps (dicts_of thy (proj_sort, algebra))
+ (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
+ val eqngr'' = fold (fn (c, rhs) => fold
+ (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
+ in ((proj_sort, algebra), (arities', eqngr'')) end;
+
+
+(** retrieval interfaces **)
+
+fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct arities_eqngr =
+ let
+ val ct = cterm_of proto_ct;
+ val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
+ val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
+ fun consts_of t =
+ fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
+ val thm = Code.preprocess_conv thy ct;
+ val ct' = Thm.rhs_of thm;
+ val t' = Thm.term_of ct';
+ val (t'', evaluator_eqngr) = evaluator t';
+ val consts = map fst (consts_of t');
+ val consts' = consts_of t'';
+ val const_matches' = fold (fn (c, ty) =>
+ insert (op =) (c, Sign.const_typargs thy (c, ty))) consts' [];
+ val (algebra', arities_eqngr') =
+ extend_arities_eqngr thy consts const_matches' arities_eqngr;
+ in
+ (evaluator_lift (evaluator_eqngr algebra') thm (snd arities_eqngr'),
+ arities_eqngr')
+ end;
+
+fun proto_eval_conv thy =
+ let
+ fun evaluator_lift evaluator thm1 eqngr =
+ let
+ val thm2 = evaluator eqngr;
+ val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
+ in
+ Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
+ error ("could not construct evaluation proof:\n"
+ ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
+ end;
+ in proto_eval thy I evaluator_lift end;
+
+fun proto_eval_term thy =
+ let
+ fun evaluator_lift evaluator _ eqngr = evaluator eqngr;
+ in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
+
+structure Wellsorted = CodeDataFun
+(
+ type T = ((string * class) * sort list) list * T;
+ val empty = ([], Graph.empty);
+ fun purge thy cs (arities, eqngr) =
+ let
+ val del_cs = ((Graph.all_preds eqngr
+ o filter (can (Graph.get_node eqngr))) cs);
+ val del_arities = del_cs
+ |> map_filter (AxClass.inst_of_param thy)
+ |> maps (fn (c, tyco) =>
+ (map (rpair tyco) o Sign.complete_sort thy o the_list
+ o AxClass.class_of_param thy) c);
+ val arities' = fold (AList.delete (op =)) del_arities arities;
+ val eqngr' = Graph.del_nodes del_cs eqngr;
+ in (arities', eqngr') end;
+);
+
+fun make thy cs = apsnd snd
+ (Wellsorted.change_yield thy (extend_arities_eqngr thy cs []));
+
+fun eval_conv thy f =
+ fst o Wellsorted.change_yield thy o proto_eval_conv thy f;
+
+fun eval_term thy f =
+ fst o Wellsorted.change_yield thy o proto_eval_term thy f;
+
+
+(** diagnostic commands **)
+
+fun code_depgr thy consts =
+ let
+ val (_, eqngr) = make thy consts;
+ val select = Graph.all_succs eqngr consts;
+ in
+ eqngr
+ |> not (null consts) ? Graph.subgraph (member (op =) select)
+ |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
+ end;
+
+fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
+
+fun code_deps thy consts =
+ let
+ val eqngr = code_depgr thy consts;
+ fun mk_entry (const, (_, (_, parents))) =
+ let
+ val name = Code_Unit.string_of_const thy const;
+ val nameparents = map (Code_Unit.string_of_const thy) parents;
+ in { name = name, ID = name, dir = "", unfold = true,
+ path = "", parents = nameparents }
+ end;
+ val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) eqngr [];
+ in Present.display_graph prgr end;
+
+local
+
+structure P = OuterParse
+and K = OuterKeyword
+
+fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
+fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
+
+in
+
+val _ =
+ OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
+ (Scan.repeat P.term_group
+ >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
+ o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
+
+val _ =
+ OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
+ (Scan.repeat P.term_group
+ >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
+ o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
+
+end;
+
+end; (*struct*)
--- a/src/Tools/nbe.ML Wed Feb 25 10:28:49 2009 +0000
+++ b/src/Tools/nbe.ML Wed Feb 25 10:29:01 2009 +0000
@@ -389,8 +389,8 @@
val ts' = take_until is_dict ts;
val c = const_of_idx idx;
val (_, T) = Code.default_typscheme thy c;
- val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T;
- val typidx' = typidx + maxidx_of_typ T' + 1;
+ val T' = map_type_tfree (fn (v, _) => TypeInfer.param typidx (v, [])) T;
+ val typidx' = typidx + 1;
in of_apps bounds (Term.Const (c, T'), ts') typidx' end
| of_univ bounds (Free (name, ts)) typidx =
of_apps bounds (Term.Free (name, dummyT), ts) typidx