--- 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
--- 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.
--- 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:
- "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> 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 \<and> 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
--- 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 \<in> carrier L ==> x \<sqsubseteq> x"
- and weak_le_anti_sym [intro]:
+ and weak_le_antisym [intro]:
"[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
and le_trans [trans]:
"[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
@@ -636,7 +636,7 @@
fix s
assume sup: "least L s (Upper L {x, y, z})"
show "x \<squnion> (y \<squnion> z) .= s"
- proof (rule weak_le_anti_sym)
+ proof (rule weak_le_antisym)
from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> 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 \<sqinter> (y \<sqinter> z) .= i"
- proof (rule weak_le_anti_sym)
+ proof (rule weak_le_antisym)
from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> 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 \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> 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 \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
--- 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: "\<exists>H. subgroup H G & card(H) = p^a"
apply (cut_tac lemma_A1, clarify)
--- 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 = \<zero>;
!!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> 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 ~= \<zero>; a \<in> 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 \<in> 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 \<zero>\<^bsub>P\<^esub> = 0"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
show "deg R \<zero>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
next
show "0 <= deg R \<zero>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
@@ -846,7 +846,7 @@
lemma deg_one [simp]:
"deg R \<one>\<^bsub>P\<^esub> = 0"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
show "deg R \<one>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
next
show "0 <= deg R \<one>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
@@ -854,7 +854,7 @@
lemma deg_uminus [simp]:
assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^bsub>P\<^esub> p) = deg R p"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
show "deg R (\<ominus>\<^bsub>P\<^esub> p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
next
show "deg R p <= deg R (\<ominus>\<^bsub>P\<^esub> p)"
@@ -878,7 +878,7 @@
lemma deg_smult [simp]:
assumes R: "a \<in> carrier R" "p \<in> carrier P"
shows "deg R (a \<odot>\<^bsub>P\<^esub> p) = (if a = \<zero> then 0 else deg R p)"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
show "deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)"
using R by (rule deg_smult_ring)
next
@@ -920,7 +920,7 @@
lemma deg_mult [simp]:
"[| p ~= \<zero>\<^bsub>P\<^esub>; q ~= \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==>
deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
assume "p \<in> carrier P" " q \<in> carrier P"
then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_ring)
next
--- 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))"
--- 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 \<le> x & x \<le> 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 = "\<forall>M. \<exists>x. a \<le> x & x \<le> b & ~ f x \<le> 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 \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>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 \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>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: "\<forall>h > 0. h < d' \<longrightarrow> 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: "\<forall>h > 0. h < d' \<longrightarrow> 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 "\<forall>x. a \<le> x & x \<le> 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 \<le> b" and
+ "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y \<ge> 0)"
+ shows "f a \<le> f b"
+proof (rule ccontr, cases "a = b")
+ assume "~ f a \<le> f b"
+ assume "a = b"
+ with prems show False by auto
+ next assume "~ f a \<le> 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
+ "\<forall>x. a \<le> x & x \<le> b --> (\<exists>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 \<le> b" and
+ "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y \<le> 0)"
+ shows "f a \<ge> f b"
+proof -
+ have "(%x. -f x) a \<le> (%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 *}
--- 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 \<subseteq> B; inj_on g B; g ` B \<subseteq> 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 *}
--- 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 \<and> d dvd b \<and>
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> 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 \<and> d dvd b \<and>
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> 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 \<Longrightarrow> gcd x y = x"
@@ -417,7 +412,7 @@
by (auto intro: coprime_dvd_mult_int)
lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> 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 \<and> b dvd d \<and>
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> 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 \<and> (a::int) dvd d \<and> b dvd d \<and>
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> 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 \<Longrightarrow> lcm x y = y"
apply (rule sym)
--- 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"
--- 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"
--- 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"
--- 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 \<noteq> 0" and "(a::int) dvd b" and "b dvd a"
+lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
shows "\<bar>a\<bar> = \<bar>b\<bar>"
-proof-
+proof cases
+ assume "a = 0" with assms show ?thesis by simp
+next
+ assume "a \<noteq> 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]
--- 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 \
--- 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
--- 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
--- /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 \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ base: "rtrancl_path r x [] x"
+| step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z"
+
+lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y = (\<exists>xs. rtrancl_path r x xs y)"
+proof
+ assume "r\<^sup>*\<^sup>* x y"
+ then show "\<exists>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 `\<exists>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 "\<exists>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 "\<exists>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 \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ base: "rtrancl_tab r xs x x"
+| step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> 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} \<union> set xs) \<inter> 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 \<notin> set ys" by auto
+ from step have "distinct (y # zs)" by simp
+ moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}"
+ by auto
+ ultimately have "rtrancl_tab r (x # ys) y z"
+ by (rule step)
+ with `x \<notin> 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} \<union> set xs') \<inter> 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 \<Rightarrow> ty \<Rightarrow> 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
+
--- 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: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> 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: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> 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:
--- 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 \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
by (rule order_trans)
-lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
+lemma le_antisym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
by (rule antisym)
lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
@@ -1611,14 +1611,14 @@
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)"
+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" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> 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
--- 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 \<Longrightarrow> 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 \<Longrightarrow> 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
--- 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 \<le> 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
--- 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 \<Longrightarrow> is_gcd a b n \<Longrightarrow> 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" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> 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: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
--- 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
--- 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 \<Longrightarrow> b = 0 \<or> a \<le> b" unfolding dvd_def by auto
lemma divides_antisym: "(x::nat) dvd y \<and> y dvd x \<longleftrightarrow> 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"
--- 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 "\<exists>n. f w \<le> g w - inverse(real(Suc n))" using w
--- 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
--- 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 \<le> w; w \<le> z |] ==> z = (w::real)"
+lemma real_le_antisym: "[| z \<le> w; w \<le> 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 \<longleftrightarrow> u \<le> v \<and> \<not> v \<le> 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) \<le> w | w \<le> z"
--- 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 \<in> X \<Longrightarrow> x \<le> a)
\<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> 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 \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> 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 \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> 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"
--- 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 ()
--- 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,
--- 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) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> 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"
--- 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 "\<sqsubseteq>" 50)
assumes refl [intro, simp]: "x \<sqsubseteq> x"
- and anti_sym [intro]: "[| x \<sqsubseteq> y; y \<sqsubseteq> x |] ==> x = y"
+ and antisym [intro]: "[| x \<sqsubseteq> y; y \<sqsubseteq> x |] ==> x = y"
and trans [trans]: "[| x \<sqsubseteq> y; y \<sqsubseteq> z |] ==> x \<sqsubseteq> 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 \<sqsubseteq> i'"
proof (rule is_inf_greatest)
from inf show "i \<sqsubseteq> 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 \<sqsubseteq> s'"
proof (rule is_sup_least)
from sup' show "x \<sqsubseteq> s'" ..
@@ -457,7 +457,7 @@
moreover
{ assume c: "x \<sqsubseteq> y | x \<sqsubseteq> 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" . }
--- 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 [