# HG changeset patch # User boehmes # Date 1258123732 -3600 # Node ID bdcabcffaaf65a9bd1e57f340cfa7bef7708b865 # Parent d62805a237ef84dba01d8baba554bf23105d9ed8# Parent 2d7ab9458518f5cff54e7c8d8e2316f38d473410 merged diff -r d62805a237ef -r bdcabcffaaf6 CONTRIBUTORS --- a/CONTRIBUTORS Fri Nov 13 15:47:37 2009 +0100 +++ b/CONTRIBUTORS Fri Nov 13 15:48:52 2009 +0100 @@ -6,6 +6,10 @@ Contributions to this Isabelle version -------------------------------------- + +* November 2009: Stefan Berghofer, Lukas Bulwahn, TUM + A tabled implementation of the reflexive transitive closure + * November 2009: Lukas Bulwahn, TUM Predicate Compiler: a compiler for inductive predicates to equational specfications diff -r d62805a237ef -r bdcabcffaaf6 NEWS --- a/NEWS Fri Nov 13 15:47:37 2009 +0100 +++ b/NEWS Fri Nov 13 15:48:52 2009 +0100 @@ -37,6 +37,8 @@ *** HOL *** +* A tabled implementation of the reflexive transitive closure + * New commands "code_pred" and "values" to invoke the predicate compiler and to enumerate values of inductive predicates. diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Algebra/IntRing.thy Fri Nov 13 15:48:52 2009 +0100 @@ -12,26 +12,6 @@ subsection {* Some properties of @{typ int} *} -lemma dvds_imp_abseq: - "\l dvd k; k dvd l\ \ abs l = abs (k::int)" -apply (subst abs_split, rule conjI) - apply (clarsimp, subst abs_split, rule conjI) - apply (clarsimp) - apply (cases "k=0", simp) - apply (cases "l=0", simp) - apply (simp add: zdvd_anti_sym) - apply clarsimp - apply (cases "k=0", simp) - apply (simp add: zdvd_anti_sym) -apply (clarsimp, subst abs_split, rule conjI) - apply (clarsimp) - apply (cases "l=0", simp) - apply (simp add: zdvd_anti_sym) -apply (clarsimp) -apply (subgoal_tac "-l = -k", simp) -apply (intro zdvd_anti_sym, simp+) -done - lemma abseq_imp_dvd: assumes a_lk: "abs l = abs (k::int)" shows "l dvd k" @@ -55,7 +35,7 @@ lemma dvds_eq_abseq: "(l dvd k \ k dvd l) = (abs l = abs (k::int))" apply rule - apply (simp add: dvds_imp_abseq) + apply (simp add: zdvd_antisym_abs) apply (rule conjI) apply (simp add: abseq_imp_dvd)+ done diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Algebra/Lattice.thy Fri Nov 13 15:48:52 2009 +0100 @@ -18,7 +18,7 @@ locale weak_partial_order = equivalence L for L (structure) + assumes le_refl [intro, simp]: "x \ carrier L ==> x \ x" - and weak_le_anti_sym [intro]: + and weak_le_antisym [intro]: "[| x \ y; y \ x; x \ carrier L; y \ carrier L |] ==> x .= y" and le_trans [trans]: "[| x \ y; y \ z; x \ carrier L; y \ carrier L; z \ carrier L |] ==> x \ z" @@ -636,7 +636,7 @@ fix s assume sup: "least L s (Upper L {x, y, z})" show "x \ (y \ z) .= s" - proof (rule weak_le_anti_sym) + proof (rule weak_le_antisym) from sup L show "x \ (y \ z) \ s" by (fastsimp intro!: join_le elim: least_Upper_above) next @@ -877,7 +877,7 @@ fix i assume inf: "greatest L i (Lower L {x, y, z})" show "x \ (y \ z) .= i" - proof (rule weak_le_anti_sym) + proof (rule weak_le_antisym) from inf L show "i \ x \ (y \ z)" by (fastsimp intro!: meet_le elim: greatest_Lower_below) next @@ -1089,11 +1089,11 @@ assumes eq_is_equal: "op .= = op =" begin -declare weak_le_anti_sym [rule del] +declare weak_le_antisym [rule del] -lemma le_anti_sym [intro]: +lemma le_antisym [intro]: "[| x \ y; y \ x; x \ carrier L; y \ carrier L |] ==> x = y" - using weak_le_anti_sym unfolding eq_is_equal . + using weak_le_antisym unfolding eq_is_equal . lemma lless_eq: "x \ y \ x \ y & x \ y" diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Algebra/Sylow.thy --- a/src/HOL/Algebra/Sylow.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Algebra/Sylow.thy Fri Nov 13 15:48:52 2009 +0100 @@ -344,7 +344,7 @@ done lemma (in sylow_central) card_H_eq: "card(H) = p^a" -by (blast intro: le_anti_sym lemma_leq1 lemma_leq2) +by (blast intro: le_antisym lemma_leq1 lemma_leq2) lemma (in sylow) sylow_thm: "\H. subgroup H G & card(H) = p^a" apply (cut_tac lemma_A1, clarify) diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Algebra/UnivPoly.thy Fri Nov 13 15:48:52 2009 +0100 @@ -811,7 +811,7 @@ lemma deg_eqI: "[| !!m. n < m ==> coeff P p m = \; !!n. n ~= 0 ==> coeff P p n ~= \; p \ carrier P |] ==> deg R p = n" -by (fast intro: le_anti_sym deg_aboveI deg_belowI) +by (fast intro: le_antisym deg_aboveI deg_belowI) text {* Degree and polynomial operations *} @@ -826,11 +826,11 @@ lemma deg_monom [simp]: "[| a ~= \; a \ carrier R |] ==> deg R (monom P a n) = n" - by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI) + by (fastsimp intro: le_antisym deg_aboveI deg_belowI) lemma deg_const [simp]: assumes R: "a \ carrier R" shows "deg R (monom P a 0) = 0" -proof (rule le_anti_sym) +proof (rule le_antisym) show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R) next show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R) @@ -838,7 +838,7 @@ lemma deg_zero [simp]: "deg R \\<^bsub>P\<^esub> = 0" -proof (rule le_anti_sym) +proof (rule le_antisym) show "deg R \\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all next show "0 <= deg R \\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all @@ -846,7 +846,7 @@ lemma deg_one [simp]: "deg R \\<^bsub>P\<^esub> = 0" -proof (rule le_anti_sym) +proof (rule le_antisym) show "deg R \\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all next show "0 <= deg R \\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all @@ -854,7 +854,7 @@ lemma deg_uminus [simp]: assumes R: "p \ carrier P" shows "deg R (\\<^bsub>P\<^esub> p) = deg R p" -proof (rule le_anti_sym) +proof (rule le_antisym) show "deg R (\\<^bsub>P\<^esub> p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R) next show "deg R p <= deg R (\\<^bsub>P\<^esub> p)" @@ -878,7 +878,7 @@ lemma deg_smult [simp]: assumes R: "a \ carrier R" "p \ carrier P" shows "deg R (a \\<^bsub>P\<^esub> p) = (if a = \ then 0 else deg R p)" -proof (rule le_anti_sym) +proof (rule le_antisym) show "deg R (a \\<^bsub>P\<^esub> p) <= (if a = \ then 0 else deg R p)" using R by (rule deg_smult_ring) next @@ -920,7 +920,7 @@ lemma deg_mult [simp]: "[| p ~= \\<^bsub>P\<^esub>; q ~= \\<^bsub>P\<^esub>; p \ carrier P; q \ carrier P |] ==> deg R (p \\<^bsub>P\<^esub> q) = deg R p + deg R q" -proof (rule le_anti_sym) +proof (rule le_antisym) assume "p \ carrier P" " q \ carrier P" then show "deg R (p \\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_ring) next diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Algebra/poly/UnivPoly2.thy --- a/src/HOL/Algebra/poly/UnivPoly2.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy Fri Nov 13 15:48:52 2009 +0100 @@ -557,7 +557,7 @@ lemma deg_eqI: "[| !!m. n < m ==> coeff p m = 0; !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n" -by (fast intro: le_anti_sym deg_aboveI deg_belowI) +by (fast intro: le_antisym deg_aboveI deg_belowI) (* Degree and polynomial operations *) @@ -571,11 +571,11 @@ lemma deg_monom [simp]: "a ~= 0 ==> deg (monom a n::'a::ring up) = n" -by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI) +by (fastsimp intro: le_antisym deg_aboveI deg_belowI) lemma deg_const [simp]: "deg (monom (a::'a::ring) 0) = 0" -proof (rule le_anti_sym) +proof (rule le_antisym) show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp next show "0 <= deg (monom a 0)" by (rule deg_belowI) simp @@ -583,7 +583,7 @@ lemma deg_zero [simp]: "deg 0 = 0" -proof (rule le_anti_sym) +proof (rule le_antisym) show "deg 0 <= 0" by (rule deg_aboveI) simp next show "0 <= deg 0" by (rule deg_belowI) simp @@ -591,7 +591,7 @@ lemma deg_one [simp]: "deg 1 = 0" -proof (rule le_anti_sym) +proof (rule le_antisym) show "deg 1 <= 0" by (rule deg_aboveI) simp next show "0 <= deg 1" by (rule deg_belowI) simp @@ -612,7 +612,7 @@ lemma deg_uminus [simp]: "deg (-p::('a::ring) up) = deg p" -proof (rule le_anti_sym) +proof (rule le_antisym) show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD) next show "deg p <= deg (- p)" @@ -626,7 +626,7 @@ lemma deg_smult [simp]: "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)" -proof (rule le_anti_sym) +proof (rule le_antisym) show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring) next show "(if a = 0 then 0 else deg p) <= deg (a *s p)" @@ -657,7 +657,7 @@ lemma deg_mult [simp]: "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q" -proof (rule le_anti_sym) +proof (rule le_antisym) show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring) next let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))" diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Deriv.thy Fri Nov 13 15:48:52 2009 +0100 @@ -273,6 +273,11 @@ "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D" by (drule DERIV_mult' [OF DERIV_const], simp) +lemma DERIV_cdivide: "DERIV f x :> D ==> DERIV (%x. f x / c) x :> D / c" + apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x :> (1 / c) * D", force) + apply (erule DERIV_cmult) + done + text {* Standard version *} lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db" by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute) @@ -702,14 +707,10 @@ apply safe apply simp_all apply (rename_tac x xa ya M Ma) -apply (cut_tac x = M and y = Ma in linorder_linear, safe) -apply (rule_tac x = Ma in exI, clarify) -apply (cut_tac x = xb and y = xa in linorder_linear, force) -apply (rule_tac x = M in exI, clarify) -apply (cut_tac x = xb and y = xa in linorder_linear, force) +apply (metis linorder_not_less order_le_less real_le_trans) apply (case_tac "a \ x & x \ b") -apply (rule_tac [2] x = 1 in exI) -prefer 2 apply force + prefer 2 + apply (rule_tac x = 1 in exI, force) apply (simp add: LIM_eq isCont_iff) apply (drule_tac x = x in spec, auto) apply (erule_tac V = "\M. \x. a \ x & x \ b & ~ f x \ M" in thin_rl) @@ -815,7 +816,7 @@ text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*} -lemma DERIV_left_inc: +lemma DERIV_pos_inc_right: fixes f :: "real => real" assumes der: "DERIV f x :> l" and l: "0 < l" @@ -845,7 +846,7 @@ qed qed -lemma DERIV_left_dec: +lemma DERIV_neg_dec_left: fixes f :: "real => real" assumes der: "DERIV f x :> l" and l: "l < 0" @@ -875,6 +876,21 @@ qed qed + +lemma DERIV_pos_inc_left: + fixes f :: "real => real" + shows "DERIV f x :> l \ 0 < l \ \d > 0. \h > 0. h < d --> f(x - h) < f(x)" + apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified]) + apply (auto simp add: DERIV_minus) + done + +lemma DERIV_neg_dec_right: + fixes f :: "real => real" + shows "DERIV f x :> l \ l < 0 \ \d > 0. \h > 0. h < d --> f(x) > f(x + h)" + apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified]) + apply (auto simp add: DERIV_minus) + done + lemma DERIV_local_max: fixes f :: "real => real" assumes der: "DERIV f x :> l" @@ -885,7 +901,7 @@ case equal thus ?thesis . next case less - from DERIV_left_dec [OF der less] + from DERIV_neg_dec_left [OF der less] obtain d' where d': "0 < d'" and lt: "\h > 0. h < d' \ f x < f (x-h)" by blast from real_lbound_gt_zero [OF d d'] @@ -894,7 +910,7 @@ show ?thesis by (auto simp add: abs_if) next case greater - from DERIV_left_inc [OF der greater] + from DERIV_pos_inc_right [OF der greater] obtain d' where d': "0 < d'" and lt: "\h > 0. h < d' \ f x < f (x + h)" by blast from real_lbound_gt_zero [OF d d'] @@ -1205,6 +1221,87 @@ ultimately show ?thesis using neq by (force simp add: add_commute) qed +(* A function with positive derivative is increasing. + A simple proof using the MVT, by Jeremy Avigad. And variants. +*) + +lemma DERIV_pos_imp_increasing: + fixes a::real and b::real and f::"real => real" + assumes "a < b" and "\x. a \ x & x \ b --> (EX y. DERIV f x :> y & y > 0)" + shows "f a < f b" +proof (rule ccontr) + assume "~ f a < f b" + from assms have "EX l z. a < z & z < b & DERIV f z :> l + & f b - f a = (b - a) * l" + by (metis MVT DERIV_isCont differentiableI real_less_def) + then obtain l z where "a < z" and "z < b" and "DERIV f z :> l" + and "f b - f a = (b - a) * l" + by auto + + from prems have "~(l > 0)" + by (metis assms(1) linorder_not_le mult_le_0_iff real_le_eq_diff) + with prems show False + by (metis DERIV_unique real_less_def) +qed + + +lemma DERIV_nonneg_imp_nonincreasing: + fixes a::real and b::real and f::"real => real" + assumes "a \ b" and + "\x. a \ x & x \ b --> (\y. DERIV f x :> y & y \ 0)" + shows "f a \ f b" +proof (rule ccontr, cases "a = b") + assume "~ f a \ f b" + assume "a = b" + with prems show False by auto + next assume "~ f a \ f b" + assume "a ~= b" + with assms have "EX l z. a < z & z < b & DERIV f z :> l + & f b - f a = (b - a) * l" + apply (intro MVT) + apply auto + apply (metis DERIV_isCont) + apply (metis differentiableI real_less_def) + done + then obtain l z where "a < z" and "z < b" and "DERIV f z :> l" + and "f b - f a = (b - a) * l" + by auto + from prems have "~(l >= 0)" + by (metis diff_self le_eqI le_iff_diff_le_0 real_le_antisym real_le_linear + split_mult_pos_le) + with prems show False + by (metis DERIV_unique order_less_imp_le) +qed + +lemma DERIV_neg_imp_decreasing: + fixes a::real and b::real and f::"real => real" + assumes "a < b" and + "\x. a \ x & x \ b --> (\y. DERIV f x :> y & y < 0)" + shows "f a > f b" +proof - + have "(%x. -f x) a < (%x. -f x) b" + apply (rule DERIV_pos_imp_increasing [of a b "%x. -f x"]) + apply (insert prems, auto) + apply (metis DERIV_minus neg_0_less_iff_less) + done + thus ?thesis + by simp +qed + +lemma DERIV_nonpos_imp_nonincreasing: + fixes a::real and b::real and f::"real => real" + assumes "a \ b" and + "\x. a \ x & x \ b --> (\y. DERIV f x :> y & y \ 0)" + shows "f a \ f b" +proof - + have "(%x. -f x) a \ (%x. -f x) b" + apply (rule DERIV_nonneg_imp_nonincreasing [of a b "%x. -f x"]) + apply (insert prems, auto) + apply (metis DERIV_minus neg_0_le_iff_le) + done + thus ?thesis + by simp +qed subsection {* Continuous injective functions *} diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Finite_Set.thy Fri Nov 13 15:48:52 2009 +0100 @@ -2344,7 +2344,7 @@ lemma card_bij_eq: "[|inj_on f A; f ` A \ B; inj_on g B; g ` B \ A; finite A; finite B |] ==> card A = card B" -by (auto intro: le_anti_sym card_inj_on_le) +by (auto intro: le_antisym card_inj_on_le) subsubsection {* Cardinality of products *} diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/GCD.thy Fri Nov 13 15:48:52 2009 +0100 @@ -312,13 +312,13 @@ by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m" - by (rule dvd_anti_sym, auto) + by (rule dvd_antisym, auto) lemma gcd_commute_int: "gcd (m::int) n = gcd n m" by (auto simp add: gcd_int_def gcd_commute_nat) lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)" - apply (rule dvd_anti_sym) + apply (rule dvd_antisym) apply (blast intro: dvd_trans)+ done @@ -339,23 +339,18 @@ lemma gcd_unique_nat: "(d::nat) dvd a \ d dvd b \ (\e. e dvd a \ e dvd b \ e dvd d) \ d = gcd a b" apply auto - apply (rule dvd_anti_sym) + apply (rule dvd_antisym) apply (erule (1) gcd_greatest_nat) apply auto done lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \ d dvd b \ (\e. e dvd a \ e dvd b \ e dvd d) \ d = gcd a b" - apply (case_tac "d = 0") - apply force - apply (rule iffI) - apply (rule zdvd_anti_sym) - apply arith - apply (subst gcd_pos_int) - apply clarsimp - apply (drule_tac x = "d + 1" in spec) - apply (frule zdvd_imp_le) - apply (auto intro: gcd_greatest_int) +apply (case_tac "d = 0") + apply simp +apply (rule iffI) + apply (rule zdvd_antisym_nonneg) + apply (auto intro: gcd_greatest_int) done lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \ gcd x y = x" @@ -417,7 +412,7 @@ by (auto intro: coprime_dvd_mult_int) lemma gcd_mult_cancel_nat: "coprime k n \ gcd ((k::nat) * m) n = gcd m n" - apply (rule dvd_anti_sym) + apply (rule dvd_antisym) apply (rule gcd_greatest_nat) apply (rule_tac n = k in coprime_dvd_mult_nat) apply (simp add: gcd_assoc_nat) @@ -1381,11 +1376,11 @@ lemma lcm_unique_nat: "(a::nat) dvd d \ b dvd d \ (\e. a dvd e \ b dvd e \ d dvd e) \ d = lcm a b" - by (auto intro: dvd_anti_sym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat) + by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat) lemma lcm_unique_int: "d >= 0 \ (a::int) dvd d \ b dvd d \ (\e. a dvd e \ b dvd e \ d dvd e) \ d = lcm a b" - by (auto intro: dvd_anti_sym [transferred] lcm_least_int) + by (auto intro: dvd_antisym [transferred] lcm_least_int) lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \ lcm x y = y" apply (rule sym) diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Hoare/Arith2.thy --- a/src/HOL/Hoare/Arith2.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Hoare/Arith2.thy Fri Nov 13 15:48:52 2009 +0100 @@ -58,7 +58,7 @@ apply (frule cd_nnn) apply (rule some_equality [symmetric]) apply (blast dest: cd_le) - apply (blast intro: le_anti_sym dest: cd_le) + apply (blast intro: le_antisym dest: cd_le) done lemma gcd_swap: "gcd m n = gcd n m" diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Import/HOL/arithmetic.imp --- a/src/HOL/Import/HOL/arithmetic.imp Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Import/HOL/arithmetic.imp Fri Nov 13 15:48:52 2009 +0100 @@ -191,7 +191,7 @@ "LESS_EQ_ADD_SUB" > "Nat.add_diff_assoc" "LESS_EQ_ADD" > "Nat.le_add1" "LESS_EQ_0" > "Nat.le_0_eq" - "LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym" + "LESS_EQUAL_ANTISYM" > "Nat.le_antisym" "LESS_EQUAL_ADD" > "HOL4Base.arithmetic.LESS_EQUAL_ADD" "LESS_EQ" > "Nat.le_simps_3" "LESS_DIV_EQ_ZERO" > "Divides.div_less" diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Import/HOL/divides.imp --- a/src/HOL/Import/HOL/divides.imp Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Import/HOL/divides.imp Fri Nov 13 15:48:52 2009 +0100 @@ -16,7 +16,7 @@ "DIVIDES_MULT" > "Divides.dvd_mult2" "DIVIDES_LE" > "Divides.dvd_imp_le" "DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT" - "DIVIDES_ANTISYM" > "Divides.dvd_anti_sym" + "DIVIDES_ANTISYM" > "Divides.dvd_antisym" "DIVIDES_ADD_2" > "HOL4Base.divides.DIVIDES_ADD_2" "DIVIDES_ADD_1" > "Ring_and_Field.dvd_add" "ALL_DIVIDES_0" > "Divides.dvd_0_right" diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Int.thy --- a/src/HOL/Int.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Int.thy Fri Nov 13 15:48:52 2009 +0100 @@ -1986,15 +1986,18 @@ subsection {* The divides relation *} -lemma zdvd_anti_sym: - "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" +lemma zdvd_antisym_nonneg: + "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)" apply (simp add: dvd_def, auto) - apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff) + apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff) done -lemma zdvd_dvd_eq: assumes "a \ 0" and "(a::int) dvd b" and "b dvd a" +lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" shows "\a\ = \b\" -proof- +proof cases + assume "a = 0" with assms show ?thesis by simp +next + assume "a \ 0" 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 @@ -2326,7 +2329,7 @@ lemmas zle_refl = order_refl [of "w::int", standard] lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard] -lemmas zle_anti_sym = order_antisym [of "z::int" "w", standard] +lemmas zle_antisym = order_antisym [of "z::int" "w", standard] lemmas zle_linear = linorder_linear [of "z::int" "w", standard] lemmas zless_linear = linorder_less_linear [where 'a = int] diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/IsaMakefile Fri Nov 13 15:48:52 2009 +0100 @@ -382,8 +382,9 @@ Library/Order_Relation.thy Library/Nested_Environment.thy \ Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML \ Library/Library/document/root.tex Library/Library/document/root.bib \ - Library/While_Combinator.thy Library/Product_ord.thy \ - Library/Char_nat.thy Library/Char_ord.thy Library/Option_ord.thy \ + Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \ + Library/Product_ord.thy Library/Char_nat.thy \ + Library/Char_ord.thy Library/Option_ord.thy \ Library/Sublist_Order.thy Library/List_lexord.thy \ Library/Coinductive_List.thy Library/AssocList.thy \ Library/Formal_Power_Series.thy Library/Binomial.thy \ diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Library/Abstract_Rat.thy --- a/src/HOL/Library/Abstract_Rat.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Library/Abstract_Rat.thy Fri Nov 13 15:48:52 2009 +0100 @@ -206,7 +206,7 @@ apply simp apply algebra done - from zdvd_dvd_eq[OF bz coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)] + from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)] coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]] have eq1: "b = b'" using pos by arith with eq have "a = a'" using pos by simp diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Library/Library.thy Fri Nov 13 15:48:52 2009 +0100 @@ -51,6 +51,7 @@ SML_Quickcheck State_Monad Sum_Of_Squares + Transitive_Closure_Table Univ_Poly While_Combinator Word diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Library/Transitive_Closure_Table.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Fri Nov 13 15:48:52 2009 +0100 @@ -0,0 +1,230 @@ +(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *) + +header {* A tabled implementation of the reflexive transitive closure *} + +theory Transitive_Closure_Table +imports Main +begin + +inductive rtrancl_path :: "('a \ 'a \ bool) \ 'a \ 'a list \ 'a \ bool" + for r :: "'a \ 'a \ bool" +where + base: "rtrancl_path r x [] x" +| step: "r x y \ rtrancl_path r y ys z \ rtrancl_path r x (y # ys) z" + +lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y = (\xs. rtrancl_path r x xs y)" +proof + assume "r\<^sup>*\<^sup>* x y" + then show "\xs. rtrancl_path r x xs y" + proof (induct rule: converse_rtranclp_induct) + case 1 + have "rtrancl_path r y [] y" by (rule rtrancl_path.base) + then show ?case .. + next + case (2 x z) + from `\xs. rtrancl_path r z xs y` + obtain xs where "rtrancl_path r z xs y" .. + with `r x z` have "rtrancl_path r x (z # xs) y" + by (rule rtrancl_path.step) + then show ?case .. + qed +next + assume "\xs. rtrancl_path r x xs y" + then obtain xs where "rtrancl_path r x xs y" .. + then show "r\<^sup>*\<^sup>* x y" + proof induct + case (base x) + show ?case by (rule rtranclp.rtrancl_refl) + next + case (step x y ys z) + from `r x y` `r\<^sup>*\<^sup>* y z` show ?case + by (rule converse_rtranclp_into_rtranclp) + qed +qed + +lemma rtrancl_path_trans: + assumes xy: "rtrancl_path r x xs y" + and yz: "rtrancl_path r y ys z" + shows "rtrancl_path r x (xs @ ys) z" using xy yz +proof (induct arbitrary: z) + case (base x) + then show ?case by simp +next + case (step x y xs) + then have "rtrancl_path r y (xs @ ys) z" + by simp + with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z" + by (rule rtrancl_path.step) + then show ?case by simp +qed + +lemma rtrancl_path_appendE: + assumes xz: "rtrancl_path r x (xs @ y # ys) z" + obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz +proof (induct xs arbitrary: x) + case Nil + then have "rtrancl_path r x (y # ys) z" by simp + then obtain xy: "r x y" and yz: "rtrancl_path r y ys z" + by cases auto + from xy have "rtrancl_path r x [y] y" + by (rule rtrancl_path.step [OF _ rtrancl_path.base]) + then have "rtrancl_path r x ([] @ [y]) y" by simp + then show ?thesis using yz by (rule Nil) +next + case (Cons a as) + then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp + then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z" + by cases auto + show ?thesis + proof (rule Cons(1) [OF _ az]) + assume "rtrancl_path r y ys z" + assume "rtrancl_path r a (as @ [y]) y" + with xa have "rtrancl_path r x (a # (as @ [y])) y" + by (rule rtrancl_path.step) + then have "rtrancl_path r x ((a # as) @ [y]) y" + by simp + then show ?thesis using `rtrancl_path r y ys z` + by (rule Cons(2)) + qed +qed + +lemma rtrancl_path_distinct: + assumes xy: "rtrancl_path r x xs y" + obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy +proof (induct xs rule: measure_induct_rule [of length]) + case (less xs) + show ?case + proof (cases "distinct (x # xs)") + case True + with `rtrancl_path r x xs y` show ?thesis by (rule less) + next + case False + then have "\as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs" + by (rule not_distinct_decomp) + then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs" + by iprover + show ?thesis + proof (cases as) + case Nil + with xxs have x: "x = a" and xs: "xs = bs @ a # cs" + by auto + from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y" + by (auto elim: rtrancl_path_appendE) + from xs have "length cs < length xs" by simp + then show ?thesis + by (rule less(1)) (iprover intro: cs less(2))+ + next + case (Cons d ds) + with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)" + by auto + with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a" + and ay: "rtrancl_path r a (bs @ a # cs) y" + by (auto elim: rtrancl_path_appendE) + from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE) + with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y" + by (rule rtrancl_path_trans) + from xs have "length ((ds @ [a]) @ cs) < length xs" by simp + then show ?thesis + by (rule less(1)) (iprover intro: xy less(2))+ + qed + qed +qed + +inductive rtrancl_tab :: "('a \ 'a \ bool) \ 'a list \ 'a \ 'a \ bool" + for r :: "'a \ 'a \ bool" +where + base: "rtrancl_tab r xs x x" +| step: "x \ set xs \ r x y \ rtrancl_tab r (x # xs) y z \ rtrancl_tab r xs x z" + +lemma rtrancl_path_imp_rtrancl_tab: + assumes path: "rtrancl_path r x xs y" + and x: "distinct (x # xs)" + and ys: "({x} \ set xs) \ set ys = {}" + shows "rtrancl_tab r ys x y" using path x ys +proof (induct arbitrary: ys) + case base + show ?case by (rule rtrancl_tab.base) +next + case (step x y zs z) + then have "x \ set ys" by auto + from step have "distinct (y # zs)" by simp + moreover from step have "({y} \ set zs) \ set (x # ys) = {}" + by auto + ultimately have "rtrancl_tab r (x # ys) y z" + by (rule step) + with `x \ set ys` `r x y` + show ?case by (rule rtrancl_tab.step) +qed + +lemma rtrancl_tab_imp_rtrancl_path: + assumes tab: "rtrancl_tab r ys x y" + obtains xs where "rtrancl_path r x xs y" using tab +proof induct + case base + from rtrancl_path.base show ?case by (rule base) +next + case step show ?case by (iprover intro: step rtrancl_path.step) +qed + +lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y" +proof + assume "r\<^sup>*\<^sup>* x y" + then obtain xs where "rtrancl_path r x xs y" + by (auto simp add: rtranclp_eq_rtrancl_path) + then obtain xs' where xs': "rtrancl_path r x xs' y" + and distinct: "distinct (x # xs')" + by (rule rtrancl_path_distinct) + have "({x} \ set xs') \ set [] = {}" by simp + with xs' distinct show "rtrancl_tab r [] x y" + by (rule rtrancl_path_imp_rtrancl_tab) +next + assume "rtrancl_tab r [] x y" + then obtain xs where "rtrancl_path r x xs y" + by (rule rtrancl_tab_imp_rtrancl_path) + then show "r\<^sup>*\<^sup>* x y" + by (auto simp add: rtranclp_eq_rtrancl_path) +qed + +declare rtranclp_eq_rtrancl_tab_nil [code_unfold] + +declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro] + +code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil[THEN iffD1] by fastsimp + +subsection {* A simple example *} + +datatype ty = A | B | C + +inductive test :: "ty \ ty \ bool" +where + "test A B" +| "test B A" +| "test B C" + +subsubsection {* Invoking with the SML code generator *} + +code_module Test +contains +test1 = "test\<^sup>*\<^sup>* A C" +test2 = "test\<^sup>*\<^sup>* C A" +test3 = "test\<^sup>*\<^sup>* A _" +test4 = "test\<^sup>*\<^sup>* _ C" + +ML "Test.test1" +ML "Test.test2" +ML "DSeq.list_of Test.test3" +ML "DSeq.list_of Test.test4" + +subsubsection {* Invoking with the predicate compiler and the generic code generator *} + +code_pred test . + +values "{x. test\<^sup>*\<^sup>* A C}" +values "{x. test\<^sup>*\<^sup>* C A}" +values "{x. test\<^sup>*\<^sup>* A x}" +values "{x. test\<^sup>*\<^sup>* x C}" + +hide const test + +end + diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Matrix/Matrix.thy --- a/src/HOL/Matrix/Matrix.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Matrix/Matrix.thy Fri Nov 13 15:48:52 2009 +0100 @@ -873,7 +873,7 @@ have th: "\ (\m. m \ j)" "\n. \ n \ i" by arith+ from th show ?thesis apply (auto) -apply (rule le_anti_sym) +apply (rule le_antisym) apply (subst nrows_le) apply (simp add: singleton_matrix_def, auto) apply (subst RepAbs_matrix) @@ -889,7 +889,7 @@ have th: "\ (\m. m \ j)" "\n. \ n \ i" by arith+ from th show ?thesis apply (auto) -apply (rule le_anti_sym) +apply (rule le_antisym) apply (subst ncols_le) apply (simp add: singleton_matrix_def, auto) apply (subst RepAbs_matrix) @@ -1004,7 +1004,7 @@ apply (subst foldseq_almostzero[of _ j]) apply (simp add: prems)+ apply (auto) - apply (metis comm_monoid_add.mult_1 le_anti_sym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int) + apply (metis comm_monoid_add.mult_1 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int) done lemma mult_matrix_ext: diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Nat.thy Fri Nov 13 15:48:52 2009 +0100 @@ -596,7 +596,7 @@ lemma le_trans: "[| i \ j; j \ k |] ==> i \ (k::nat)" by (rule order_trans) -lemma le_anti_sym: "[| m \ n; n \ m |] ==> m = (n::nat)" +lemma le_antisym: "[| m \ n; n \ m |] ==> m = (n::nat)" by (rule antisym) lemma nat_less_le: "((m::nat) < n) = (m \ n & m \ n)" @@ -1611,14 +1611,14 @@ lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \ m = 1" by (simp add: dvd_def) -lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)" +lemma dvd_antisym: "[| 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) text {* @{term "op dvd"} is a partial order *} interpretation dvd: order "op dvd" "\n m \ nat. n dvd m \ \ m dvd n" - proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym) + proof qed (auto intro: dvd_refl dvd_trans dvd_antisym) lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)" unfolding dvd_def diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Number_Theory/UniqueFactorization.thy --- a/src/HOL/Number_Theory/UniqueFactorization.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Fri Nov 13 15:48:52 2009 +0100 @@ -844,7 +844,7 @@ mult_eq [simp]: "!!p. prime p \ multiplicity p x = multiplicity p y" shows "x = y" - apply (rule dvd_anti_sym) + apply (rule dvd_antisym) apply (auto intro: multiplicity_dvd'_nat) done @@ -854,7 +854,7 @@ mult_eq [simp]: "!!p. prime p \ multiplicity p x = multiplicity p y" shows "x = y" - apply (rule dvd_anti_sym [transferred]) + apply (rule dvd_antisym [transferred]) apply (auto intro: multiplicity_dvd'_int) done diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Old_Number_Theory/IntPrimes.thy --- a/src/HOL/Old_Number_Theory/IntPrimes.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Fri Nov 13 15:48:52 2009 +0100 @@ -204,7 +204,7 @@ apply (case_tac [2] "0 \ ka") 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 mult_le_0_iff zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff zle_antisym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult) apply (metis dvd_triv_left) done diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Old_Number_Theory/Legacy_GCD.thy --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Fri Nov 13 15:48:52 2009 +0100 @@ -23,7 +23,7 @@ text {* Uniqueness *} lemma is_gcd_unique: "is_gcd a b m \ is_gcd a b n \ m = n" - by (simp add: is_gcd_def) (blast intro: dvd_anti_sym) + by (simp add: is_gcd_def) (blast intro: dvd_antisym) text {* Connection to divides relation *} @@ -156,7 +156,7 @@ by (auto intro: relprime_dvd_mult dvd_mult2) lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n" - apply (rule dvd_anti_sym) + apply (rule dvd_antisym) apply (rule gcd_greatest) apply (rule_tac n = k in relprime_dvd_mult) apply (simp add: gcd_assoc) @@ -223,7 +223,7 @@ assume H: "d dvd a" "d dvd b" "\e. e dvd a \ e dvd b \ e dvd d" from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] have th: "gcd a b dvd d" by blast - from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]] show "d = gcd a b" by blast + from dvd_antisym[OF th gcd_greatest[OF H(1,2)]] show "d = gcd a b" by blast qed lemma gcd_eq: assumes H: "\d. d dvd x \ d dvd y \ d dvd u \ d dvd v" diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Old_Number_Theory/Pocklington.thy --- a/src/HOL/Old_Number_Theory/Pocklington.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy Fri Nov 13 15:48:52 2009 +0100 @@ -935,7 +935,7 @@ p: "prime p" "p dvd m" by blast from dvd_trans[OF p(2) m(1)] p(1) H have "p = n" by blast with p(2) have "n dvd m" by simp - hence "m=n" using dvd_anti_sym[OF m(1)] by simp } + hence "m=n" using dvd_antisym[OF m(1)] by simp } with n1 have "prime n" unfolding prime_def by auto } ultimately have ?thesis using n by blast} ultimately show ?thesis by auto diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Old_Number_Theory/Primes.thy --- a/src/HOL/Old_Number_Theory/Primes.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Old_Number_Theory/Primes.thy Fri Nov 13 15:48:52 2009 +0100 @@ -97,7 +97,7 @@ text {* Elementary theory of divisibility *} lemma divides_ge: "(a::nat) dvd b \ b = 0 \ a \ b" unfolding dvd_def by auto lemma divides_antisym: "(x::nat) dvd y \ y dvd x \ x = y" - using dvd_anti_sym[of x y] by auto + using dvd_antisym[of x y] by auto lemma divides_add_revr: assumes da: "(d::nat) dvd a" and dab:"d dvd (a + b)" shows "d dvd b" diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Probability/Borel.thy --- a/src/HOL/Probability/Borel.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Probability/Borel.thy Fri Nov 13 15:48:52 2009 +0100 @@ -73,7 +73,7 @@ with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)" by (metis lessI order_le_less_trans real_natceiling_ge real_of_nat_less_iff) hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < inverse(inverse(g w - f w))" - by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_ordered_idom nz positive_imp_inverse_positive real_le_anti_sym real_less_def w) + by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_ordered_idom nz positive_imp_inverse_positive real_le_antisym real_less_def w) hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w" by (metis inverse_inverse_eq order_less_le_trans real_le_refl) thus "\n. f w \ g w - inverse(real(Suc n))" using w diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Probability/Measure.thy --- a/src/HOL/Probability/Measure.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Probability/Measure.thy Fri Nov 13 15:48:52 2009 +0100 @@ -356,7 +356,7 @@ by (metis add_commute le_add_diff_inverse nat_less_le) thus ?thesis by (auto simp add: disjoint_family_def) - (metis insert_absorb insert_subset le_SucE le_anti_sym not_leE) + (metis insert_absorb insert_subset le_SucE le_antisym not_leE) qed diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/RealDef.thy Fri Nov 13 15:48:52 2009 +0100 @@ -321,7 +321,7 @@ apply (auto intro: real_le_lemma) done -lemma real_le_anti_sym: "[| z \ w; w \ z |] ==> z = (w::real)" +lemma real_le_antisym: "[| z \ w; w \ z |] ==> z = (w::real)" by (cases z, cases w, simp add: real_le) lemma real_trans_lemma: @@ -347,8 +347,8 @@ proof fix u v :: real show "u < v \ u \ v \ \ v \ u" - by (auto simp add: real_less_def intro: real_le_anti_sym) -qed (assumption | rule real_le_refl real_le_trans real_le_anti_sym)+ + by (auto simp add: real_less_def intro: real_le_antisym) +qed (assumption | rule real_le_refl real_le_trans real_le_antisym)+ (* Axiom 'linorder_linear' of class 'linorder': *) lemma real_le_linear: "(z::real) \ w | w \ z" diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/SupInf.thy --- a/src/HOL/SupInf.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/SupInf.thy Fri Nov 13 15:48:52 2009 +0100 @@ -118,7 +118,7 @@ shows "(!!x. x \ X \ x \ a) \ (!!y. (!!x. x \ X \ x \ y) \ a \ y) \ Sup X = a" by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb - insert_not_empty real_le_anti_sym) + insert_not_empty real_le_antisym) lemma Sup_le: fixes S :: "real set" @@ -317,7 +317,7 @@ fixes a :: real shows "(!!x. x \ X \ a \ x) \ (!!y. (!!x. x \ X \ y \ x) \ y \ a) \ Inf X = a" by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel - insert_absorb insert_not_empty real_le_anti_sym) + insert_absorb insert_not_empty real_le_antisym) lemma Inf_ge: fixes S :: "real set" @@ -397,7 +397,7 @@ fixes S :: "real set" shows "finite S \ S \ {} \ a \ Inf S \ (\ x \ S. a \ x)" by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le - real_le_anti_sym real_le_linear) + real_le_antisym real_le_linear) lemma Inf_finite_gt_iff: fixes S :: "real set" diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 13 15:48:52 2009 +0100 @@ -1047,7 +1047,6 @@ let val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^ p ^ " violates mode " ^ string_of_mode thy p m) - val _ = tracing (string_of_clause thy p (nth rs i)) in () end else () diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Nov 13 15:48:52 2009 +0100 @@ -23,6 +23,8 @@ val options = Options { expected_modes = NONE, + proposed_modes = [], + proposed_names = [], show_steps = true, show_intermediate_results = true, show_proof_trace = false, diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/Transitive_Closure.thy Fri Nov 13 15:48:52 2009 +0100 @@ -575,6 +575,25 @@ "(x,y) \ R\<^sup>* = (x=y \ x\y \ (x,y) \ R\<^sup>+)" by (fast elim: trancl_into_rtrancl dest: rtranclD) +lemma trancl_unfold_right: "r^+ = r^* O r" +by (auto dest: tranclD2 intro: rtrancl_into_trancl1) + +lemma trancl_unfold_left: "r^+ = r O r^*" +by (auto dest: tranclD intro: rtrancl_into_trancl2) + + +text {* Simplifying nested closures *} + +lemma rtrancl_trancl_absorb[simp]: "(R^*)^+ = R^*" +by (simp add: trans_rtrancl) + +lemma trancl_rtrancl_absorb[simp]: "(R^+)^* = R^*" +by (subst reflcl_trancl[symmetric]) simp + +lemma rtrancl_reflcl_absorb[simp]: "(R^*)^= = R^*" +by auto + + text {* @{text Domain} and @{text Range} *} lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV" diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/ex/LocaleTest2.thy --- a/src/HOL/ex/LocaleTest2.thy Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/ex/LocaleTest2.thy Fri Nov 13 15:48:52 2009 +0100 @@ -29,7 +29,7 @@ locale dpo = fixes le :: "['a, 'a] => bool" (infixl "\" 50) assumes refl [intro, simp]: "x \ x" - and anti_sym [intro]: "[| x \ y; y \ x |] ==> x = y" + and antisym [intro]: "[| x \ y; y \ x |] ==> x = y" and trans [trans]: "[| x \ y; y \ z |] ==> x \ z" begin @@ -87,7 +87,7 @@ assume inf: "is_inf x y i" assume inf': "is_inf x y i'" show ?thesis - proof (rule anti_sym) + proof (rule antisym) from inf' show "i \ i'" proof (rule is_inf_greatest) from inf show "i \ x" .. @@ -159,7 +159,7 @@ assume sup: "is_sup x y s" assume sup': "is_sup x y s'" show ?thesis - proof (rule anti_sym) + proof (rule antisym) from sup show "s \ s'" proof (rule is_sup_least) from sup' show "x \ s'" .. @@ -457,7 +457,7 @@ moreover { assume c: "x \ y | x \ z" from c have "?l = x" - by (metis (*anti_sym*) (*c*) (*circular*) (*join_assoc*)(* join_commute *) join_connection2 (*join_left*) join_related2 meet_connection(* meet_related2*) total trans) + by (metis (*antisym*) (*c*) (*circular*) (*join_assoc*)(* join_commute *) join_connection2 (*join_left*) join_related2 meet_connection(* meet_related2*) total trans) also from c have "... = ?r" by (metis join_commute join_related2 meet_connection meet_related2 total) finally have "?l = ?r" . } diff -r d62805a237ef -r bdcabcffaaf6 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Fri Nov 13 15:47:37 2009 +0100 +++ b/src/HOL/ex/ROOT.ML Fri Nov 13 15:48:52 2009 +0100 @@ -13,7 +13,8 @@ "Codegenerator_Pretty_Test", "NormalForm", "Predicate_Compile", - "Predicate_Compile_ex" + "Predicate_Compile_ex", + "Predicate_Compile_Quickcheck" ]; use_thys [