src/HOL/Zorn.thy
changeset 55811 aa1acc25126b
parent 55018 2a526bd279ed
child 58184 db1381d811ab
     1.1 --- a/src/HOL/Zorn.thy	Fri Feb 28 22:00:13 2014 +0100
     1.2 +++ b/src/HOL/Zorn.thy	Fri Feb 28 17:54:52 2014 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4  
     1.5  lemma suc_not_equals:
     1.6    "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> suc C \<noteq> C"
     1.7 -  by (auto simp: suc_def) (metis (no_types) less_irrefl not_maxchain_Some)
     1.8 +  using not_maxchain_Some by (auto simp: suc_def)
     1.9  
    1.10  lemma subset_suc:
    1.11    assumes "X \<subseteq> Y" shows "X \<subseteq> suc Y"
    1.12 @@ -257,7 +257,7 @@
    1.13    shows "chain X"
    1.14  using assms
    1.15  proof (induct)
    1.16 -  case (suc X) then show ?case by (simp add: suc_def) (metis (no_types) not_maxchain_Some)
    1.17 +  case (suc X) then show ?case using not_maxchain_Some by (simp add: suc_def)
    1.18  next
    1.19    case (Union X)
    1.20    then have "\<Union>X \<subseteq> A" by (auto dest: suc_Union_closed_in_carrier)
    1.21 @@ -377,7 +377,7 @@
    1.22          using `subset.maxchain A M` by (auto simp: subset.maxchain_def)
    1.23      qed
    1.24    qed
    1.25 -  ultimately show ?thesis by metis
    1.26 +  ultimately show ?thesis by blast
    1.27  qed
    1.28  
    1.29  text{*Alternative version of Zorn's lemma for the subset relation.*}
    1.30 @@ -440,8 +440,7 @@
    1.31  lemma Chains_alt_def:
    1.32    assumes "refl r"
    1.33    shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
    1.34 -  using assms
    1.35 -  by (metis Chains_subset Chains_subset' subset_antisym)
    1.36 +  using assms Chains_subset Chains_subset' by blast
    1.37  
    1.38  lemma Zorn_Lemma:
    1.39    "\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
    1.40 @@ -534,16 +533,28 @@
    1.41    by (auto simp: init_seg_of_def Ball_def Chains_def) blast
    1.42  
    1.43  lemma chain_subset_trans_Union:
    1.44 -  "chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans (\<Union>R)"
    1.45 -apply (auto simp add: chain_subset_def)
    1.46 -apply (simp (no_asm_use) add: trans_def)
    1.47 -by (metis subsetD)
    1.48 +  assumes "chain\<^sub>\<subseteq> R" "\<forall>r\<in>R. trans r"
    1.49 +  shows "trans (\<Union>R)"
    1.50 +proof (intro transI, elim UnionE)
    1.51 +  fix  S1 S2 :: "'a rel" and x y z :: 'a
    1.52 +  assume "S1 \<in> R" "S2 \<in> R"
    1.53 +  with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1" unfolding chain_subset_def by blast
    1.54 +  moreover assume "(x, y) \<in> S1" "(y, z) \<in> S2"
    1.55 +  ultimately have "((x, y) \<in> S1 \<and> (y, z) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, z) \<in> S2)" by blast
    1.56 +  with `S1 \<in> R` `S2 \<in> R` assms(2) show "(x, z) \<in> \<Union>R" by (auto elim: transE)
    1.57 +qed
    1.58  
    1.59  lemma chain_subset_antisym_Union:
    1.60 -  "chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym (\<Union>R)"
    1.61 -unfolding chain_subset_def antisym_def
    1.62 -apply simp
    1.63 -by (metis (no_types) subsetD)
    1.64 +  assumes "chain\<^sub>\<subseteq> R" "\<forall>r\<in>R. antisym r"
    1.65 +  shows "antisym (\<Union>R)"
    1.66 +proof (intro antisymI, elim UnionE)
    1.67 +  fix  S1 S2 :: "'a rel" and x y :: 'a
    1.68 +  assume "S1 \<in> R" "S2 \<in> R"
    1.69 +  with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1" unfolding chain_subset_def by blast
    1.70 +  moreover assume "(x, y) \<in> S1" "(y, x) \<in> S2"
    1.71 +  ultimately have "((x, y) \<in> S1 \<and> (y, x) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, x) \<in> S2)" by blast
    1.72 +  with `S1 \<in> R` `S2 \<in> R` assms(2) show "x = y" unfolding antisym_def by auto
    1.73 +qed
    1.74  
    1.75  lemma chain_subset_Total_Union:
    1.76    assumes "chain\<^sub>\<subseteq> R" and "\<forall>r\<in>R. Total r"
    1.77 @@ -554,12 +565,12 @@
    1.78      by (auto simp add: chain_subset_def)
    1.79    thus "(\<exists>r\<in>R. (a, b) \<in> r) \<or> (\<exists>r\<in>R. (b, a) \<in> r)"
    1.80    proof
    1.81 -    assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A
    1.82 -      by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
    1.83 +    assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A mono_Field[of r s]
    1.84 +      by (auto simp add: total_on_def)
    1.85      thus ?thesis using `s \<in> R` by blast
    1.86    next
    1.87 -    assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A
    1.88 -      by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
    1.89 +    assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A mono_Field[of s r]
    1.90 +      by (fastforce simp add: total_on_def)
    1.91      thus ?thesis using `r \<in> R` by blast
    1.92    qed
    1.93  qed
    1.94 @@ -633,8 +644,8 @@
    1.95      moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris
    1.96        by(simp add: Chains_init_seg_of_Union)
    1.97      ultimately have "\<Union>R \<in> ?WO \<and> (\<forall>r\<in>R. (r, \<Union>R) \<in> I)"
    1.98 -      using mono_Chains [OF I_init] and `R \<in> Chains I`
    1.99 -      by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo)
   1.100 +      using mono_Chains [OF I_init] Chains_wo[of R] and `R \<in> Chains I`
   1.101 +      unfolding I_def by blast
   1.102    }
   1.103    hence 1: "\<forall>R \<in> Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast
   1.104  --{*Zorn's Lemma yields a maximal well-order m:*}
   1.105 @@ -671,8 +682,8 @@
   1.106      moreover have "Total ?m" using `Total m` and Fm by (auto simp: total_on_def)
   1.107      moreover have "wf (?m - Id)"
   1.108      proof -
   1.109 -      have "wf ?s" using `x \<notin> Field m`
   1.110 -        by (auto simp add: wf_eq_minimal Field_def) metis
   1.111 +      have "wf ?s" using `x \<notin> Field m` unfolding wf_eq_minimal Field_def
   1.112 +        by (auto simp: Bex_def)
   1.113        thus ?thesis using `wf (m - Id)` and `x \<notin> Field m`
   1.114          wf_subset [OF `wf ?s` Diff_subset]
   1.115          unfolding Un_Diff Field_def by (auto intro: wf_Un)