# HG changeset patch
# User noschinl
# Date 1331586670 -3600
# Node ID 75208a489363b91d472cd5d0475bb612bd79ed8c
# Parent  9a95da60ca54fbc0d93b7bd113ffce8af7dfc821# Parent  48c82ef7d4687ebc947d4a9d664058f037f40c15
merged

diff -r 9a95da60ca54 -r 75208a489363 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -579,32 +579,32 @@
 definition
   "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
 
-lemma Inf_apply (* CANDIDATE [simp] *) [code]:
+lemma Inf_apply [simp, code]:
   "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
   by (simp add: Inf_fun_def)
 
 definition
   "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
 
-lemma Sup_apply (* CANDIDATE [simp] *) [code]:
+lemma Sup_apply [simp, code]:
   "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
   by (simp add: Sup_fun_def)
 
 instance proof
-qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_lower INF_greatest SUP_upper SUP_least)
+qed (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)
 
 end
 
-lemma INF_apply (* CANDIDATE [simp] *):
+lemma INF_apply [simp]:
   "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
-  by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
+  by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def)
 
-lemma SUP_apply (* CANDIDATE [simp] *):
+lemma SUP_apply [simp]:
   "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
-  by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
+  by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def)
 
 instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
-qed (auto simp add: inf_apply sup_apply Inf_apply Sup_apply INF_def SUP_def inf_Sup sup_Inf image_image)
+qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf image_image)
 
 instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
 
@@ -612,46 +612,46 @@
 subsection {* Complete lattice on unary and binary predicates *}
 
 lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
-  by (simp add: INF_apply)
+  by simp
 
 lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
-  by (simp add: INF_apply)
+  by simp
 
 lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
-  by (auto simp add: INF_apply)
+  by auto
 
 lemma INF2_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
-  by (auto simp add: INF_apply)
+  by auto
 
 lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
-  by (auto simp add: INF_apply)
+  by auto
 
 lemma INF2_D: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
-  by (auto simp add: INF_apply)
+  by auto
 
 lemma INF1_E: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
-  by (auto simp add: INF_apply)
+  by auto
 
 lemma INF2_E: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> (B a b c \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
-  by (auto simp add: INF_apply)
+  by auto
 
 lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
-  by (simp add: SUP_apply)
+  by simp
 
 lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
-  by (simp add: SUP_apply)
+  by simp
 
 lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
-  by (auto simp add: SUP_apply)
+  by auto
 
 lemma SUP2_I: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
-  by (auto simp add: SUP_apply)
+  by auto
 
 lemma SUP1_E: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R"
-  by (auto simp add: SUP_apply)
+  by auto
 
 lemma SUP2_E: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R"
-  by (auto simp add: SUP_apply)
+  by auto
 
 
 subsection {* Complete lattice on @{typ "_ set"} *}
diff -r 9a95da60ca54 -r 75208a489363 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/Lattices.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -650,24 +650,24 @@
 definition
   "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
 
-lemma inf_apply (* CANDIDATE [simp, code] *):
+lemma inf_apply [simp] (* CANDIDATE [code] *):
   "(f \<sqinter> g) x = f x \<sqinter> g x"
   by (simp add: inf_fun_def)
 
 definition
   "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
 
-lemma sup_apply (* CANDIDATE [simp, code] *):
+lemma sup_apply [simp] (* CANDIDATE [code] *):
   "(f \<squnion> g) x = f x \<squnion> g x"
   by (simp add: sup_fun_def)
 
 instance proof
-qed (simp_all add: le_fun_def inf_apply sup_apply)
+qed (simp_all add: le_fun_def)
 
 end
 
 instance "fun" :: (type, distrib_lattice) distrib_lattice proof
-qed (rule ext, simp add: sup_inf_distrib1 inf_apply sup_apply)
+qed (rule ext, simp add: sup_inf_distrib1)
 
 instance "fun" :: (type, bounded_lattice) bounded_lattice ..
 
@@ -677,7 +677,7 @@
 definition
   fun_Compl_def: "- A = (\<lambda>x. - A x)"
 
-lemma uminus_apply (* CANDIDATE [simp, code] *):
+lemma uminus_apply [simp] (* CANDIDATE [code] *):
   "(- A) x = - (A x)"
   by (simp add: fun_Compl_def)
 
@@ -691,7 +691,7 @@
 definition
   fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
 
-lemma minus_apply (* CANDIDATE [simp, code] *):
+lemma minus_apply [simp] (* CANDIDATE [code] *):
   "(A - B) x = A x - B x"
   by (simp add: fun_diff_def)
 
@@ -700,7 +700,7 @@
 end
 
 instance "fun" :: (type, boolean_algebra) boolean_algebra proof
-qed (rule ext, simp_all add: inf_apply sup_apply bot_apply top_apply uminus_apply minus_apply inf_compl_bot sup_compl_top diff_eq)+
+qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
 
 
 subsection {* Lattice on unary and binary predicates *}
diff -r 9a95da60ca54 -r 75208a489363 src/HOL/Library/Cset.thy
--- a/src/HOL/Library/Cset.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/Library/Cset.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -175,10 +175,10 @@
 subsection {* Simplified simprules *}
 
 lemma empty_simp [simp]: "member Cset.empty = bot"
-  by (simp add: fun_eq_iff bot_apply)
+  by (simp add: fun_eq_iff)
 
 lemma UNIV_simp [simp]: "member Cset.UNIV = top"
-  by (simp add: fun_eq_iff top_apply)
+  by (simp add: fun_eq_iff)
 
 lemma is_empty_simp [simp]:
   "is_empty A \<longleftrightarrow> set_of A = {}"
@@ -222,7 +222,7 @@
 
 lemma member_SUP [simp]:
   "member (SUPR A f) = SUPR A (member \<circ> f)"
-  by (auto simp add: fun_eq_iff SUP_apply member_def, unfold SUP_def, auto)
+  by (auto simp add: fun_eq_iff member_def, unfold SUP_def, auto)
 
 lemma member_bind [simp]:
   "member (P \<guillemotright>= f) = SUPR (set_of P) (member \<circ> f)"
@@ -247,14 +247,14 @@
  
 lemma bind_single [simp]:
   "A \<guillemotright>= single = A"
-  by (simp add: Cset.set_eq_iff SUP_apply fun_eq_iff single_def member_def)
+  by (simp add: Cset.set_eq_iff fun_eq_iff single_def member_def)
 
 lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
   by (auto simp add: Cset.set_eq_iff fun_eq_iff)
 
 lemma empty_bind [simp]:
   "Cset.empty \<guillemotright>= f = Cset.empty"
-  by (simp add: Cset.set_eq_iff fun_eq_iff bot_apply)
+  by (simp add: Cset.set_eq_iff fun_eq_iff )
 
 lemma member_of_pred [simp]:
   "member (of_pred P) = (\<lambda>x. x \<in> {x. Predicate.eval P x})"
@@ -360,7 +360,7 @@
      Predicate.Empty \<Rightarrow> Cset.empty
    | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
    | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
-  by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff sup_apply eval_member [symmetric] member_def [symmetric])
+  by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff eval_member [symmetric] member_def [symmetric])
 
 lemma of_seq_code [code]:
   "of_seq Predicate.Empty = Cset.empty"
diff -r 9a95da60ca54 -r 75208a489363 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -41,7 +41,7 @@
 
 lemma Diff[code_pred_inline]:
   "(A - B) = (%x. A x \<and> \<not> B x)"
-  by (simp add: fun_eq_iff minus_apply)
+  by (simp add: fun_eq_iff)
 
 lemma subset_eq[code_pred_inline]:
   "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
@@ -232,4 +232,4 @@
 lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
 unfolding less_nat[symmetric] by auto
 
-end
\ No newline at end of file
+end
diff -r 9a95da60ca54 -r 75208a489363 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/List.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -4533,7 +4533,7 @@
   "listsp A (x # xs)"
 
 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
-by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
+by (rule predicate1I, erule listsp.induct, blast+)
 
 lemmas lists_mono = listsp_mono [to_set]
 
diff -r 9a95da60ca54 -r 75208a489363 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/Orderings.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -1299,12 +1299,12 @@
 definition
   "\<bottom> = (\<lambda>x. \<bottom>)"
 
-lemma bot_apply (* CANDIDATE [simp, code] *):
+lemma bot_apply [simp] (* CANDIDATE [code] *):
   "\<bottom> x = \<bottom>"
   by (simp add: bot_fun_def)
 
 instance proof
-qed (simp add: le_fun_def bot_apply)
+qed (simp add: le_fun_def)
 
 end
 
@@ -1315,12 +1315,12 @@
   [no_atp]: "\<top> = (\<lambda>x. \<top>)"
 declare top_fun_def_raw [no_atp]
 
-lemma top_apply (* CANDIDATE [simp, code] *):
+lemma top_apply [simp] (* CANDIDATE [code] *):
   "\<top> x = \<top>"
   by (simp add: top_fun_def)
 
 instance proof
-qed (simp add: le_fun_def top_apply)
+qed (simp add: le_fun_def)
 
 end
 
diff -r 9a95da60ca54 -r 75208a489363 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/Predicate.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -123,7 +123,7 @@
   by (simp add: minus_pred_def)
 
 instance proof
-qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply INF_apply SUP_apply)
+qed (auto intro!: pred_eqI)
 
 end
 
@@ -143,7 +143,7 @@
 
 lemma bind_bind:
   "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
-  by (rule pred_eqI) (auto simp add: SUP_apply)
+  by (rule pred_eqI) auto
 
 lemma bind_single:
   "P \<guillemotright>= single = P"
@@ -163,7 +163,7 @@
 
 lemma Sup_bind:
   "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
-  by (rule pred_eqI) (auto simp add: SUP_apply)
+  by (rule pred_eqI) auto
 
 lemma pred_iffI:
   assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
diff -r 9a95da60ca54 -r 75208a489363 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -1417,7 +1417,7 @@
 proof
   fix a
   have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
-    by (auto simp: less_SUP_iff SUP_apply)
+    by (auto simp: less_SUP_iff)
   then show "?sup -` {a<..} \<inter> space M \<in> sets M"
     using assms by auto
 qed
@@ -1430,7 +1430,7 @@
 proof
   fix a
   have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
-    by (auto simp: INF_less_iff INF_apply)
+    by (auto simp: INF_less_iff)
   then show "?inf -` {..<a} \<inter> space M \<in> sets M"
     using assms by auto
 qed
diff -r 9a95da60ca54 -r 75208a489363 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -1044,7 +1044,7 @@
         with `a < 1` u_range[OF `x \<in> space M`]
         have "a * u x < 1 * u x"
           by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
-        also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def SUP_apply)
+        also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def)
         finally obtain i where "a * u x < f i x" unfolding SUP_def
           by (auto simp add: less_Sup_iff)
         hence "a * u x \<le> f i x" by auto
@@ -1115,7 +1115,7 @@
       using f by (auto intro!: SUP_upper2)
     ultimately show "integral\<^isup>S M g \<le> (SUP j. integral\<^isup>P M (f j))"
       by (intro  positive_integral_SUP_approx[OF f g _ g'])
-         (auto simp: le_fun_def max_def SUP_apply)
+         (auto simp: le_fun_def max_def)
   qed
 qed
 
diff -r 9a95da60ca54 -r 75208a489363 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -10,9 +10,8 @@
 
 text {* A preliminary: classical rules for reasoning on predicates *}
 
-(* CANDIDATE declare predicate1I [Pure.intro!, intro!] *)
-declare predicate1D [Pure.dest?, dest?]
-(* CANDIDATE declare predicate1D [Pure.dest, dest] *)
+declare predicate1I [Pure.intro!, intro!]
+declare predicate1D [Pure.dest, dest]
 declare predicate2I [Pure.intro!, intro!]
 declare predicate2D [Pure.dest, dest]
 declare bot1E [elim!] 
@@ -72,17 +71,17 @@
 lemma pred_subset_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S) \<longleftrightarrow> R \<subseteq> S"
   by (simp add: subset_iff le_fun_def)
 
-lemma bot_empty_eq (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x. x \<in> {})"
+lemma bot_empty_eq [pred_set_conv]: "\<bottom> = (\<lambda>x. x \<in> {})"
   by (auto simp add: fun_eq_iff)
 
-lemma bot_empty_eq2 (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
+lemma bot_empty_eq2 [pred_set_conv]: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
   by (auto simp add: fun_eq_iff)
 
-(* CANDIDATE lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)"
-  by (auto simp add: fun_eq_iff) *)
+lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)"
+  by (auto simp add: fun_eq_iff)
 
-(* CANDIDATE lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)"
-  by (auto simp add: fun_eq_iff) *)
+lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)"
+  by (auto simp add: fun_eq_iff)
 
 lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   by (simp add: inf_fun_def)
@@ -97,58 +96,41 @@
   by (simp add: sup_fun_def)
 
 lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
-  by (simp add: fun_eq_iff Inf_apply)
+  by (simp add: fun_eq_iff)
 
-(* CANDIDATE
 lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
-  by (simp add: fun_eq_iff INF_apply)
+  by (simp add: fun_eq_iff)
 
 lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (prod_case ` S) Collect)"
-  by (simp add: fun_eq_iff Inf_apply INF_apply)
+  by (simp add: fun_eq_iff)
 
 lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)"
-  by (simp add: fun_eq_iff INF_apply)
+  by (simp add: fun_eq_iff)
 
 lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> UNION S Collect)"
-  by (simp add: fun_eq_iff Sup_apply)
+  by (simp add: fun_eq_iff)
 
 lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)"
-  by (simp add: fun_eq_iff SUP_apply)
+  by (simp add: fun_eq_iff)
 
 lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)"
-  by (simp add: fun_eq_iff Sup_apply SUP_apply)
+  by (simp add: fun_eq_iff)
 
 lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
-  by (simp add: fun_eq_iff SUP_apply)
-*)
+  by (simp add: fun_eq_iff)
 
-(* CANDIDATE prefer those generalized versions:
-lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i\<in>S. r i))"
-  by (simp add: INF_apply fun_eq_iff)
+lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
+  by (simp add: fun_eq_iff)
 
 lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))"
-  by (simp add: INF_apply fun_eq_iff)
-*)
-
-lemma INF_INT_eq (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
-  by (simp add: INF_apply fun_eq_iff)
+  by (simp add: fun_eq_iff)
 
-lemma INF_INT_eq2 (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
-  by (simp add: INF_apply fun_eq_iff)
-
-(* CANDIDATE prefer those generalized versions:
-lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i\<in>S. r i))"
-  by (simp add: SUP_apply fun_eq_iff)
+lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
+  by (simp add: fun_eq_iff)
 
 lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
-  by (simp add: SUP_apply fun_eq_iff)
-*)
+  by (simp add: fun_eq_iff)
 
-lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
-  by (simp add: SUP_apply fun_eq_iff)
-
-lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
-  by (simp add: SUP_apply fun_eq_iff)
 
 
 subsection {* Properties of relations *}
@@ -558,22 +540,23 @@
   "{} O R = {}"
   by blast
 
-(* CANDIDATE lemma pred_comp_bot1 [simp]:
-  ""
-  by (fact rel_comp_empty1 [to_pred]) *)
+lemma prod_comp_bot1 [simp]:
+  "\<bottom> OO R = \<bottom>"
+  by (fact rel_comp_empty1 [to_pred])
 
 lemma rel_comp_empty2 [simp]:
   "R O {} = {}"
   by blast
 
-(* CANDIDATE lemma pred_comp_bot2 [simp]:
-  ""
-  by (fact rel_comp_empty2 [to_pred]) *)
+lemma pred_comp_bot2 [simp]:
+  "R OO \<bottom> = \<bottom>"
+  by (fact rel_comp_empty2 [to_pred])
 
 lemma O_assoc:
   "(R O S) O T = R O (S O T)"
   by blast
 
+
 lemma pred_comp_assoc:
   "(r OO s) OO t = r OO (s OO t)"
   by (fact O_assoc [to_pred])
@@ -602,7 +585,7 @@
   "R O (S \<union> T) = (R O S) \<union> (R O T)" 
   by auto
 
-lemma pred_comp_distrib (* CANDIDATE [simp] *):
+lemma pred_comp_distrib [simp]:
   "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
   by (fact rel_comp_distrib [to_pred])
 
@@ -610,7 +593,7 @@
   "(S \<union> T) O R = (S O R) \<union> (T O R)"
   by auto
 
-lemma pred_comp_distrib2 (* CANDIDATE [simp] *):
+lemma pred_comp_distrib2 [simp]:
   "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
   by (fact rel_comp_distrib2 [to_pred])
 
@@ -672,7 +655,7 @@
   "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P"
   by (cases yx) (simp, erule converse.cases, iprover)
 
-lemmas conversepE (* CANDIDATE [elim!] *) = conversep.cases
+lemmas conversepE [elim!] = conversep.cases
 
 lemma converse_iff [iff]:
   "(a, b) \<in> r\<inverse> \<longleftrightarrow> (b, a) \<in> r"
@@ -828,14 +811,14 @@
 lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}"
   by auto
 
-lemma Domain_insert (* CANDIDATE [simp] *): "Domain (insert (a, b) r) = insert a (Domain r)"
+lemma Domain_insert [simp]: "Domain (insert (a, b) r) = insert a (Domain r)"
   by blast
 
-lemma Range_insert (* CANDIDATE [simp] *): "Range (insert (a, b) r) = insert b (Range r)"
+lemma Range_insert [simp]: "Range (insert (a, b) r) = insert b (Range r)"
   by blast
 
 lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r"
-  by (auto simp add: Field_def Domain_insert Range_insert)
+  by (auto simp add: Field_def)
 
 lemma Domain_iff: "a \<in> Domain r \<longleftrightarrow> (\<exists>y. (a, y) \<in> r)"
   by blast
@@ -901,10 +884,10 @@
   by auto
 
 lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)"
-  by (induct set: finite) (auto simp add: Domain_insert)
+  by (induct set: finite) auto
 
 lemma finite_Range: "finite r \<Longrightarrow> finite (Range r)"
-  by (induct set: finite) (auto simp add: Range_insert)
+  by (induct set: finite) auto
 
 lemma finite_Field: "finite r \<Longrightarrow> finite (Field r)"
   by (simp add: Field_def finite_Domain finite_Range)
diff -r 9a95da60ca54 -r 75208a489363 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/Set.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -124,7 +124,8 @@
 qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def
   bot_set_def top_set_def uminus_set_def minus_set_def
   less_le_not_le inf_compl_bot sup_compl_top sup_inf_distrib1 diff_eq
-  set_eqI fun_eq_iff)
+  set_eqI fun_eq_iff
+  del: inf_apply sup_apply bot_apply top_apply minus_apply uminus_apply)
 
 end
 
diff -r 9a95da60ca54 -r 75208a489363 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -298,9 +298,8 @@
 
 lemma wfP_SUP:
   "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
-  apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred])
-  apply (simp_all add: inf_set_def)
-  apply auto
+  apply (rule wf_UN[to_pred])
+  apply simp_all
   done
 
 lemma wf_Union: 
diff -r 9a95da60ca54 -r 75208a489363 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Mon Mar 12 21:34:45 2012 +0100
+++ b/src/ZF/Cardinal.thy	Mon Mar 12 22:11:10 2012 +0100
@@ -440,15 +440,23 @@
   finally show "i \<lesssim> j" .
 qed
 
-lemma cardinal_mono: "i \<le> j ==> |i| \<le> |j|"
-apply (rule_tac i = "|i|" and j = "|j|" in Ord_linear_le)
-apply (safe intro!: Ord_cardinal le_eqI)
-apply (rule cardinal_eq_lemma)
-prefer 2 apply assumption
-apply (erule le_trans)
-apply (erule ltE)
-apply (erule Ord_cardinal_le)
-done
+lemma cardinal_mono: 
+  assumes ij: "i \<le> j" shows "|i| \<le> |j|"
+proof (cases rule: Ord_linear_le [OF Ord_cardinal Ord_cardinal])
+  assume "|i| \<le> |j|" thus ?thesis .
+next
+  assume cj: "|j| \<le> |i|"
+  have i: "Ord(i)" using ij
+    by (simp add: lt_Ord) 
+  have ci: "|i| \<le> j"  
+    by (blast intro: Ord_cardinal_le ij le_trans i) 
+  have "|i| = ||i||" 
+    by (auto simp add: Ord_cardinal_idem i) 
+  also have "... = |j|"
+    by (rule cardinal_eq_lemma [OF cj ci])
+  finally have "|i| = |j|" .
+  thus ?thesis by simp
+qed
 
 (*Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of cardinal_mono fails!*)
 lemma cardinal_lt_imp_lt: "[| |i| < |j|;  Ord(i);  Ord(j) |] ==> i < j"
@@ -458,8 +466,7 @@
 done
 
 lemma Card_lt_imp_lt: "[| |i| < K;  Ord(i);  Card(K) |] ==> i < K"
-apply (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
-done
+  by (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
 
 lemma Card_lt_iff: "[| Ord(i);  Card(K) |] ==> (|i| < K) \<longleftrightarrow> (i < K)"
 by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
@@ -532,8 +539,9 @@
 apply (rule mem_not_refl)+
 done
 
+
 lemma nat_lepoll_imp_le [rule_format]:
-     "m:nat ==> \<forall>n\<in>nat. m \<lesssim> n \<longrightarrow> m \<le> n"
+     "m \<in> nat ==> \<forall>n\<in>nat. m \<lesssim> n \<longrightarrow> m \<le> n"
 apply (induct_tac m)
 apply (blast intro!: nat_0_le)
 apply (rule ballI)
@@ -542,7 +550,7 @@
 apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
 done
 
-lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
+lemma nat_eqpoll_iff: "[| m \<in> nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
 apply (rule iffI)
 apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
 apply (simp add: eqpoll_refl)
@@ -564,7 +572,7 @@
 
 
 (*Part of Kunen's Lemma 10.6*)
-lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n;  n:nat |] ==> P"
+lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n;  n \<in> nat |] ==> P"
 by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
 
 lemma nat_lepoll_imp_ex_eqpoll_n:
@@ -580,27 +588,32 @@
 
 (** lepoll, \<prec> and natural numbers **)
 
+lemma lepoll_succ: "i \<lesssim> succ(i)"
+  by (blast intro: subset_imp_lepoll)
+
 lemma lepoll_imp_lesspoll_succ:
-     "[| A \<lesssim> m; m:nat |] ==> A \<prec> succ(m)"
-apply (unfold lesspoll_def)
-apply (rule conjI)
-apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans])
-apply (rule notI)
-apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
-apply (drule lepoll_trans, assumption)
-apply (erule succ_lepoll_natE, assumption)
+  assumes A: "A \<lesssim> m" and m: "m \<in> nat"
+  shows "A \<prec> succ(m)"
+proof -
+  { assume "A \<approx> succ(m)" 
+    hence "succ(m) \<approx> A" by (rule eqpoll_sym)
+    also have "... \<lesssim> m" by (rule A)
+    finally have "succ(m) \<lesssim> m" .
+    hence False by (rule succ_lepoll_natE) (rule m) }
+  moreover have "A \<lesssim> succ(m)" by (blast intro: lepoll_trans A lepoll_succ)
+  ultimately show ?thesis by (auto simp add: lesspoll_def) 
+qed
+
+lemma lesspoll_succ_imp_lepoll:
+     "[| A \<prec> succ(m); m \<in> nat |] ==> A \<lesssim> m"
+apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def)
+apply (auto dest: inj_not_surj_succ)
 done
 
-lemma lesspoll_succ_imp_lepoll:
-     "[| A \<prec> succ(m); m:nat |] ==> A \<lesssim> m"
-apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def, clarify)
-apply (blast intro!: inj_not_surj_succ)
-done
-
-lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m"
+lemma lesspoll_succ_iff: "m \<in> nat ==> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m"
 by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
 
-lemma lepoll_succ_disj: "[| A \<lesssim> succ(m);  m:nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
+lemma lepoll_succ_disj: "[| A \<lesssim> succ(m);  m \<in> nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
 apply (rule disjCI)
 apply (rule lesspoll_succ_imp_lepoll)
 prefer 2 apply assumption
@@ -618,32 +631,51 @@
 subsection{*The first infinite cardinal: Omega, or nat *}
 
 (*This implies Kunen's Lemma 10.6*)
-lemma lt_not_lepoll: "[| n<i;  n:nat |] ==> ~ i \<lesssim> n"
-apply (rule notI)
-apply (rule succ_lepoll_natE [of n])
-apply (rule lepoll_trans [of _ i])
-apply (erule ltE)
-apply (rule Ord_succ_subsetI [THEN subset_imp_lepoll], assumption+)
-done
+lemma lt_not_lepoll:
+  assumes n: "n<i" "n \<in> nat" shows "~ i \<lesssim> n"
+proof -
+  { assume i: "i \<lesssim> n"
+    have "succ(n) \<lesssim> i" using n
+      by (elim ltE, blast intro: Ord_succ_subsetI [THEN subset_imp_lepoll]) 
+    also have "... \<lesssim> n" by (rule i)
+    finally have "succ(n) \<lesssim> n" .
+    hence False  by (rule succ_lepoll_natE) (rule n) }
+  thus ?thesis by auto
+qed
 
-lemma Ord_nat_eqpoll_iff: "[| Ord(i);  n:nat |] ==> i \<approx> n \<longleftrightarrow> i=n"
-apply (rule iffI)
- prefer 2 apply (simp add: eqpoll_refl)
-apply (rule Ord_linear_lt [of i n])
-apply (simp_all add: nat_into_Ord)
-apply (erule lt_nat_in_nat [THEN nat_eqpoll_iff, THEN iffD1], assumption+)
-apply (rule lt_not_lepoll [THEN notE], assumption+)
-apply (erule eqpoll_imp_lepoll)
-done
+text{*A slightly weaker version of @{text nat_eqpoll_iff}*}
+lemma Ord_nat_eqpoll_iff:
+  assumes i: "Ord(i)" and n: "n \<in> nat" shows "i \<approx> n \<longleftrightarrow> i=n"
+proof (cases rule: Ord_linear_lt [OF i])
+  show "Ord(n)" using n by auto
+next
+  assume "i < n"
+  hence  "i \<in> nat" by (rule lt_nat_in_nat) (rule n)
+  thus ?thesis by (simp add: nat_eqpoll_iff n) 
+next
+  assume "i = n"
+  thus ?thesis by (simp add: eqpoll_refl) 
+next
+  assume "n < i"
+  hence  "~ i \<lesssim> n" using n  by (rule lt_not_lepoll) 
+  hence  "~ i \<approx> n" using n  by (blast intro: eqpoll_imp_lepoll)
+  moreover have "i \<noteq> n" using `n<i` by auto
+  ultimately show ?thesis by blast
+qed
 
 lemma Card_nat: "Card(nat)"
-apply (unfold Card_def cardinal_def)
-apply (subst Least_equality)
-apply (rule eqpoll_refl)
-apply (rule Ord_nat)
-apply (erule ltE)
-apply (simp_all add: eqpoll_iff lt_not_lepoll ltI)
-done
+proof -
+  { fix i
+    assume i: "i < nat" "i \<approx> nat" 
+    hence "~ nat \<lesssim> i" 
+      by (simp add: lt_def lt_not_lepoll) 
+    hence False using i 
+      by (simp add: eqpoll_iff)
+  }
+  hence "(\<mu> i. i \<approx> nat) = nat" by (blast intro: Least_equality eqpoll_refl) 
+  thus ?thesis
+    by (auto simp add: Card_def cardinal_def) 
+qed
 
 (*Allows showing that |i| is a limit cardinal*)
 lemma nat_le_cardinal: "nat \<le> i ==> nat \<le> |i|"
@@ -736,31 +768,35 @@
 
 (*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*)
 
-(*If A has at most n+1 elements and a:A then A-{a} has at most n.*)
+text{*If @{term A} has at most @{term"n+1"} elements and @{term"a \<in> A"} 
+      then @{term"A-{a}"} has at most @{term n}.*}
 lemma Diff_sing_lepoll:
-      "[| a:A;  A \<lesssim> succ(n) |] ==> A - {a} \<lesssim> n"
+      "[| a \<in> A;  A \<lesssim> succ(n) |] ==> A - {a} \<lesssim> n"
 apply (unfold succ_def)
 apply (rule cons_lepoll_consD)
 apply (rule_tac [3] mem_not_refl)
 apply (erule cons_Diff [THEN ssubst], safe)
 done
 
-(*If A has at least n+1 elements then A-{a} has at least n.*)
+text{*If @{term A} has at least @{term"n+1"} elements then @{term"A-{a}"} has at least @{term n}.*}
 lemma lepoll_Diff_sing:
-      "[| succ(n) \<lesssim> A |] ==> n \<lesssim> A - {a}"
-apply (unfold succ_def)
-apply (rule cons_lepoll_consD)
-apply (rule_tac [2] mem_not_refl)
-prefer 2 apply blast
-apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans])
-done
+  assumes A: "succ(n) \<lesssim> A" shows "n \<lesssim> A - {a}"
+proof -
+  have "cons(n,n) \<lesssim> A" using A
+    by (unfold succ_def)
+  also have "... \<lesssim> cons(a, A-{a})" 
+    by (blast intro: subset_imp_lepoll)
+  finally have "cons(n,n) \<lesssim> cons(a, A-{a})" .
+  thus ?thesis
+    by (blast intro: cons_lepoll_consD mem_irrefl) 
+qed
 
-lemma Diff_sing_eqpoll: "[| a:A; A \<approx> succ(n) |] ==> A - {a} \<approx> n"
+lemma Diff_sing_eqpoll: "[| a \<in> A; A \<approx> succ(n) |] ==> A - {a} \<approx> n"
 by (blast intro!: eqpollI
           elim!: eqpollE
           intro: Diff_sing_lepoll lepoll_Diff_sing)
 
-lemma lepoll_1_is_sing: "[| A \<lesssim> 1; a:A |] ==> A = {a}"
+lemma lepoll_1_is_sing: "[| A \<lesssim> 1; a \<in> A |] ==> A = {a}"
 apply (frule Diff_sing_lepoll, assumption)
 apply (drule lepoll_0_is_0)
 apply (blast elim: equalityE)
@@ -768,8 +804,8 @@
 
 lemma Un_lepoll_sum: "A \<union> B \<lesssim> A+B"
 apply (unfold lepoll_def)
-apply (rule_tac x = "\<lambda>x\<in>A \<union> B. if x:A then Inl (x) else Inr (x) " in exI)
-apply (rule_tac d = "%z. snd (z) " in lam_injective)
+apply (rule_tac x = "\<lambda>x\<in>A \<union> B. if x\<in>A then Inl (x) else Inr (x)" in exI)
+apply (rule_tac d = "%z. snd (z)" in lam_injective)
 apply force
 apply (simp add: Inl_def Inr_def)
 done
@@ -782,8 +818,8 @@
 (*Krzysztof Grabczewski*)
 lemma disj_Un_eqpoll_sum: "A \<inter> B = 0 ==> A \<union> B \<approx> A + B"
 apply (unfold eqpoll_def)
-apply (rule_tac x = "\<lambda>a\<in>A \<union> B. if a:A then Inl (a) else Inr (a) " in exI)
-apply (rule_tac d = "%z. case (%x. x, %x. x, z) " in lam_bijective)
+apply (rule_tac x = "\<lambda>a\<in>A \<union> B. if a \<in> A then Inl (a) else Inr (a)" in exI)
+apply (rule_tac d = "%z. case (%x. x, %x. x, z)" in lam_bijective)
 apply auto
 done
 
@@ -795,7 +831,7 @@
 apply (blast intro!: eqpoll_refl nat_0I)
 done
 
-lemma lepoll_nat_imp_Finite: "[| A \<lesssim> n;  n:nat |] ==> Finite(A)"
+lemma lepoll_nat_imp_Finite: "[| A \<lesssim> n;  n \<in> nat |] ==> Finite(A)"
 apply (unfold Finite_def)
 apply (erule rev_mp)
 apply (erule nat_induct)
@@ -811,12 +847,15 @@
 done
 
 lemma lepoll_Finite:
-     "[| Y \<lesssim> X;  Finite(X) |] ==> Finite(Y)"
-apply (unfold Finite_def)
-apply (blast elim!: eqpollE
-             intro: lepoll_trans [THEN lepoll_nat_imp_Finite
-                                       [unfolded Finite_def]])
-done
+  assumes Y: "Y \<lesssim> X" and X: "Finite(X)" shows "Finite(Y)"
+proof -
+  obtain n where n: "n \<in> nat" "X \<approx> n" using X 
+    by (auto simp add: Finite_def) 
+  have "Y \<lesssim> X"         by (rule Y)
+  also have "... \<approx> n"  by (rule n)
+  finally have "Y \<lesssim> n" .
+  thus ?thesis using n by (simp add: lepoll_nat_imp_Finite)
+qed
 
 lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite]
 
@@ -947,7 +986,7 @@
 (*Sidi Ehmety.  The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
 lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
 apply (unfold Finite_def)
-apply (case_tac "a:A")
+apply (case_tac "a \<in> A")
 apply (subgoal_tac [2] "A-{a}=A", auto)
 apply (rule_tac x = "succ (n) " in bexI)
 apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
@@ -1010,7 +1049,7 @@
 (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
   set is well-ordered.  Proofs simplified by lcp. *)
 
-lemma nat_wf_on_converse_Memrel: "n:nat ==> wf[n](converse(Memrel(n)))"
+lemma nat_wf_on_converse_Memrel: "n \<in> nat ==> wf[n](converse(Memrel(n)))"
 apply (erule nat_induct)
 apply (blast intro: wf_onI)
 apply (rule wf_onI)
@@ -1023,7 +1062,7 @@
 apply (drule_tac x = Z in spec, blast)
 done
 
-lemma nat_well_ord_converse_Memrel: "n:nat ==> well_ord(n,converse(Memrel(n)))"
+lemma nat_well_ord_converse_Memrel: "n \<in> nat ==> well_ord(n,converse(Memrel(n)))"
 apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
 apply (unfold well_ord_def)
 apply (blast intro!: tot_ord_converse nat_wf_on_converse_Memrel)
@@ -1040,13 +1079,16 @@
 done
 
 lemma ordertype_eq_n:
-     "[| well_ord(A,r);  A \<approx> n;  n:nat |] ==> ordertype(A,r)=n"
-apply (rule Ord_ordertype [THEN Ord_nat_eqpoll_iff, THEN iffD1], assumption+)
-apply (rule eqpoll_trans)
- prefer 2 apply assumption
-apply (unfold eqpoll_def)
-apply (blast intro!: ordermap_bij [THEN bij_converse_bij])
-done
+  assumes r: "well_ord(A,r)" and A: "A \<approx> n" and n: "n \<in> nat" 
+  shows "ordertype(A,r) = n"
+proof -
+  have "ordertype(A,r) \<approx> A" 
+    by (blast intro: bij_imp_eqpoll bij_converse_bij ordermap_bij r) 
+  also have "... \<approx> n" by (rule A)
+  finally have "ordertype(A,r) \<approx> n" .
+  thus ?thesis
+    by (simp add: Ord_nat_eqpoll_iff Ord_ordertype n r) 
+qed
 
 lemma Finite_well_ord_converse:
     "[| Finite(A);  well_ord(A,r) |] ==> well_ord(A,converse(r))"
@@ -1055,18 +1097,24 @@
 apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
 done
 
-lemma nat_into_Finite: "n:nat ==> Finite(n)"
+lemma nat_into_Finite: "n \<in> nat ==> Finite(n)"
 apply (unfold Finite_def)
 apply (fast intro!: eqpoll_refl)
 done
 
-lemma nat_not_Finite: "~Finite(nat)"
-apply (unfold Finite_def, clarify)
-apply (drule eqpoll_imp_lepoll [THEN lepoll_cardinal_le], simp)
-apply (insert Card_nat)
-apply (simp add: Card_def)
-apply (drule le_imp_subset)
-apply (blast elim: mem_irrefl)
-done
+lemma nat_not_Finite: "~ Finite(nat)"
+proof -
+  { fix n
+    assume n: "n \<in> nat" "nat \<approx> n"
+    have "n \<in> nat"    by (rule n) 
+    also have "... = n" using n
+      by (simp add: Ord_nat_eqpoll_iff Ord_nat) 
+    finally have "n \<in> n" .
+    hence False 
+      by (blast elim: mem_irrefl) 
+  }
+  thus ?thesis
+    by (auto simp add: Finite_def) 
+qed
 
 end