--- a/NEWS Tue Jul 14 12:18:52 2009 +0200
+++ b/NEWS Tue Jul 14 15:55:27 2009 +0200
@@ -28,6 +28,14 @@
* New type class boolean_algebra.
+* Refinements to lattices classes:
+ - added boolean_algebra type class
+ - less default intro/elim rules in locale variant, more default
+ intro/elim rules in class variant: more uniformity
+ - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
+ - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
+ - renamed ACI to inf_sup_aci
+
* Class semiring_div requires superclass no_zero_divisors and proof of
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
--- a/src/HOL/Finite_Set.thy Tue Jul 14 12:18:52 2009 +0200
+++ b/src/HOL/Finite_Set.thy Tue Jul 14 15:55:27 2009 +0200
@@ -811,7 +811,7 @@
by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
-by (induct pred:finite) auto
+by (induct pred: finite) (auto intro: le_infI1)
lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
proof(induct arbitrary: a pred:finite)
@@ -822,7 +822,7 @@
proof cases
assume "A = {}" thus ?thesis using insert by simp
next
- assume "A \<noteq> {}" thus ?thesis using insert by auto
+ assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
qed
qed
--- a/src/HOL/Lattices.thy Tue Jul 14 12:18:52 2009 +0200
+++ b/src/HOL/Lattices.thy Tue Jul 14 15:55:27 2009 +0200
@@ -44,38 +44,27 @@
context lower_semilattice
begin
-lemma le_infI1[intro]:
- assumes "a \<sqsubseteq> x"
- shows "a \<sqinter> b \<sqsubseteq> x"
-proof (rule order_trans)
- from assms show "a \<sqsubseteq> x" .
- show "a \<sqinter> b \<sqsubseteq> a" by simp
-qed
-lemmas (in -) [rule del] = le_infI1
+lemma le_infI1:
+ "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+ by (rule order_trans) auto
-lemma le_infI2[intro]:
- assumes "b \<sqsubseteq> x"
- shows "a \<sqinter> b \<sqsubseteq> x"
-proof (rule order_trans)
- from assms show "b \<sqsubseteq> x" .
- show "a \<sqinter> b \<sqsubseteq> b" by simp
-qed
-lemmas (in -) [rule del] = le_infI2
+lemma le_infI2:
+ "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+ by (rule order_trans) auto
-lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
-by(blast intro: inf_greatest)
-lemmas (in -) [rule del] = le_infI
+lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
+ by (blast intro: inf_greatest)
-lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
- by (blast intro: order_trans)
-lemmas (in -) [rule del] = le_infE
+lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
+ by (blast intro: order_trans le_infI1 le_infI2)
lemma le_inf_iff [simp]:
- "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
-by blast
+ "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
+ by (blast intro: le_infI elim: le_infE)
-lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
- by (blast intro: antisym dest: eq_iff [THEN iffD1])
+lemma le_iff_inf:
+ "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
+ by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
lemma mono_inf:
fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice"
@@ -87,28 +76,29 @@
context upper_semilattice
begin
-lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI1:
+ "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
by (rule order_trans) auto
-lemmas (in -) [rule del] = le_supI1
-lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI2:
+ "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
by (rule order_trans) auto
-lemmas (in -) [rule del] = le_supI2
-lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
+lemma le_supI:
+ "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
by (blast intro: sup_least)
-lemmas (in -) [rule del] = le_supI
-lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
- by (blast intro: order_trans)
-lemmas (in -) [rule del] = le_supE
+lemma le_supE:
+ "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
+ by (blast intro: le_supI1 le_supI2 order_trans)
-lemma ge_sup_conv[simp]:
- "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
-by blast
+lemma le_sup_iff [simp]:
+ "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
+ by (blast intro: le_supI elim: le_supE)
-lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
- by (blast intro: antisym dest: eq_iff [THEN iffD1])
+lemma le_iff_sup:
+ "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
+ by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
lemma mono_sup:
fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice"
@@ -118,62 +108,61 @@
end
-subsubsection{* Equational laws *}
+subsubsection {* Equational laws *}
context lower_semilattice
begin
lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
- by (blast intro: antisym)
+ by (rule antisym) (auto intro: le_infI1 le_infI2)
lemma inf_idem[simp]: "x \<sqinter> x = x"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
- by (blast intro: antisym)
+ by (rule antisym) (auto intro: le_infI2)
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
- by (blast intro: antisym)
-
-lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem
+ by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+
+
+lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
end
-
context upper_semilattice
begin
lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
- by (blast intro: antisym)
+ by (rule antisym) (auto intro: le_supI1 le_supI2)
lemma sup_idem[simp]: "x \<squnion> x = x"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
- by (blast intro: antisym)
+ by (rule antisym) (auto intro: le_supI2)
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
- by (blast intro: antisym)
+ by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+
-lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem
+lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
end
@@ -191,18 +180,17 @@
lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
by (blast intro: antisym sup_ge1 sup_least inf_le1)
-lemmas ACI = inf_ACI sup_ACI
+lemmas inf_sup_aci = inf_aci sup_aci
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
text{* Towards distributivity *}
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
- by blast
+ by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
- by blast
-
+ by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
text{* If you have one of them, you have them all. *}
@@ -230,10 +218,6 @@
finally show ?thesis .
qed
-(* seems unused *)
-lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z"
-by blast
-
end
@@ -247,7 +231,7 @@
lemma sup_inf_distrib2:
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
-by(simp add:ACI sup_inf_distrib1)
+by(simp add: inf_sup_aci sup_inf_distrib1)
lemma inf_sup_distrib1:
"x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
@@ -255,7 +239,7 @@
lemma inf_sup_distrib2:
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
-by(simp add:ACI inf_sup_distrib1)
+by(simp add: inf_sup_aci inf_sup_distrib1)
lemma dual_distrib_lattice:
"distrib_lattice (op \<ge>) (op >) sup inf"
@@ -458,16 +442,6 @@
lemmas min_ac = min_max.inf_assoc min_max.inf_commute
mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
-text {*
- Now we have inherited antisymmetry as an intro-rule on all
- linear orders. This is a problem because it applies to bool, which is
- undesirable.
-*}
-
-lemmas [rule del] = min_max.le_infI min_max.le_supI
- min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
- min_max.le_infI1 min_max.le_infI2
-
subsection {* Bool as lattice *}
@@ -548,8 +522,6 @@
text {* redundant bindings *}
-lemmas inf_aci = inf_ACI
-lemmas sup_aci = sup_ACI
no_notation
less_eq (infix "\<sqsubseteq>" 50) and
--- a/src/HOL/OrderedGroup.thy Tue Jul 14 12:18:52 2009 +0200
+++ b/src/HOL/OrderedGroup.thy Tue Jul 14 15:55:27 2009 +0200
@@ -1075,16 +1075,16 @@
lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
-by (simp add: pprt_def le_iff_sup sup_ACI)
+by (simp add: pprt_def le_iff_sup sup_aci)
lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
-by (simp add: nprt_def le_iff_inf inf_ACI)
+by (simp add: nprt_def le_iff_inf inf_aci)
lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
-by (simp add: pprt_def le_iff_sup sup_ACI)
+by (simp add: pprt_def le_iff_sup sup_aci)
lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
-by (simp add: nprt_def le_iff_inf inf_ACI)
+by (simp add: nprt_def le_iff_inf inf_aci)
lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
proof -
@@ -1120,7 +1120,7 @@
assume "0 <= a + a"
hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
- by (simp add: add_sup_inf_distribs inf_ACI)
+ by (simp add: add_sup_inf_distribs inf_aci)
hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
hence "inf a 0 = 0" by (simp only: add_right_cancel)
then show "0 <= a" by (simp add: le_iff_inf inf_commute)
@@ -1206,10 +1206,10 @@
by (simp add: le_iff_inf nprt_def inf_commute)
lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
-by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
+by (simp add: le_iff_sup pprt_def sup_aci sup_assoc [symmetric, of a])
lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
-by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
+by (simp add: le_iff_inf nprt_def inf_aci inf_assoc [symmetric, of a])
end
@@ -1230,7 +1230,7 @@
then have "0 \<le> sup a (- a)" unfolding abs_lattice .
then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
then show ?thesis
- by (simp add: add_sup_inf_distribs sup_ACI
+ by (simp add: add_sup_inf_distribs sup_aci
pprt_def nprt_def diff_minus abs_lattice)
qed
@@ -1254,7 +1254,7 @@
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
proof -
have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
- by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
+ by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
have a:"a+b <= sup ?m ?n" by (simp)
have b:"-a-b <= ?n" by (simp)
have c:"?n <= sup ?m ?n" by (simp)
--- a/src/HOL/SEQ.thy Tue Jul 14 12:18:52 2009 +0200
+++ b/src/HOL/SEQ.thy Tue Jul 14 15:55:27 2009 +0200
@@ -113,8 +113,8 @@
lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
unfolding Bfun_def eventually_sequentially
apply (rule iffI)
-apply (simp add: Bseq_def, fast)
-apply (fast intro: BseqI2')
+apply (simp add: Bseq_def)
+apply (auto intro: BseqI2')
done
@@ -762,13 +762,25 @@
lemma lemma_NBseq_def:
"(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
(\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
-apply auto
- prefer 2 apply force
-apply (cut_tac x = K in reals_Archimedean2, clarify)
-apply (rule_tac x = n in exI, clarify)
-apply (drule_tac x = na in spec)
-apply (auto simp add: real_of_nat_Suc)
-done
+proof auto
+ fix K :: real
+ from reals_Archimedean2 obtain n :: nat where "K < real n" ..
+ then have "K \<le> real (Suc n)" by auto
+ assume "\<forall>m. norm (X m) \<le> K"
+ have "\<forall>m. norm (X m) \<le> real (Suc n)"
+ proof
+ fix m :: 'a
+ from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" ..
+ with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto
+ qed
+ then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
+next
+ fix N :: nat
+ have "real (Suc N) > 0" by (simp add: real_of_nat_Suc)
+ moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)"
+ ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast
+qed
+
text{* alternative definition for Bseq *}
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
@@ -1105,7 +1117,7 @@
lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u"
proof (rule reals_complete)
obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1"
- using CauchyD [OF X zero_less_one] by fast
+ using CauchyD [OF X zero_less_one] by auto
hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp
show "\<exists>x. x \<in> S"
proof
@@ -1129,7 +1141,7 @@
fix r::real assume "0 < r"
hence r: "0 < r/2" by simp
obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2"
- using CauchyD [OF X r] by fast
+ using CauchyD [OF X r] by auto
hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp
hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
by (simp only: real_norm_def real_abs_diff_less_iff)
--- a/src/HOL/Set.thy Tue Jul 14 12:18:52 2009 +0200
+++ b/src/HOL/Set.thy Tue Jul 14 15:55:27 2009 +0200
@@ -2249,10 +2249,10 @@
unfolding Inf_Sup by auto
lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
- by (auto intro: antisym Inf_greatest Inf_lower)
+ by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
- by (auto intro: antisym Sup_least Sup_upper)
+ by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
lemma Inf_singleton [simp]:
"\<Sqinter>{a} = a"