--- a/src/HOL/Equiv_Relations.thy Wed Nov 28 09:01:34 2007 +0100
+++ b/src/HOL/Equiv_Relations.thy Wed Nov 28 09:01:37 2007 +0100
@@ -288,7 +288,7 @@
apply (rule commute [THEN trans])
apply (rule_tac [3] commute [THEN trans, symmetric])
apply (rule_tac [5] sym)
- apply (assumption | rule congt |
+ apply (rule congt | assumption |
erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
done
--- a/src/HOL/Lattices.thy Wed Nov 28 09:01:34 2007 +0100
+++ b/src/HOL/Lattices.thy Wed Nov 28 09:01:37 2007 +0100
@@ -39,7 +39,8 @@
assumes "a \<sqsubseteq> x"
shows "a \<sqinter> b \<sqsubseteq> x"
proof (rule order_trans)
- show "a \<sqinter> b \<sqsubseteq> a" and "a \<sqsubseteq> x" using assms by simp
+ from assms show "a \<sqsubseteq> x" .
+ show "a \<sqinter> b \<sqsubseteq> a" by simp
qed
lemmas (in -) [rule del] = le_infI1
@@ -47,7 +48,8 @@
assumes "b \<sqsubseteq> x"
shows "a \<sqinter> b \<sqsubseteq> x"
proof (rule order_trans)
- show "a \<sqinter> b \<sqsubseteq> b" and "b \<sqsubseteq> x" using assms by simp
+ from assms show "b \<sqsubseteq> x" .
+ show "a \<sqinter> b \<sqsubseteq> b" by simp
qed
lemmas (in -) [rule del] = le_infI2
--- a/src/HOL/Nat.thy Wed Nov 28 09:01:34 2007 +0100
+++ b/src/HOL/Nat.thy Wed Nov 28 09:01:37 2007 +0100
@@ -813,20 +813,20 @@
\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$.
\end{itemize}
NB: the proof also shows how to use the previous lemma. *}
-corollary infinite_descent0_measure[case_names 0 smaller]:
-assumes 0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
-and 1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
-shows "P x"
+corollary infinite_descent0_measure [case_names 0 smaller]:
+ assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
+ and A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
+ shows "P x"
proof -
obtain n where "n = V x" by auto
- moreover have "!!x. V x = n \<Longrightarrow> P x"
+ moreover have "\<And>x. V x = n \<Longrightarrow> P x"
proof (induct n rule: infinite_descent0)
case 0 -- "i.e. $V(x) = 0$"
- with 0 show "P x" by auto
+ with A0 show "P x" by auto
next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
case (smaller n)
then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
- with 1 obtain y where "V y < V x \<and> \<not> P y" by auto
+ with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
thus ?case by auto
qed