src/HOL/BNF_Cardinal_Order_Relation.thy
 changeset 67091 1393c2340eec parent 63980 f8e556c8ad6f child 67613 ce654b0e6d69
```     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Nov 26 13:19:52 2017 +0100
1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Nov 26 21:08:32 2017 +0100
1.3 @@ -387,8 +387,8 @@
1.4  lemma card_of_image:
1.5  "|f ` A| <=o |A|"
1.6  proof(cases "A = {}", simp add: card_of_empty)
1.7 -  assume "A ~= {}"
1.8 -  hence "f ` A ~= {}" by auto
1.9 +  assume "A \<noteq> {}"
1.10 +  hence "f ` A \<noteq> {}" by auto
1.11    thus "|f ` A| \<le>o |A|"
1.12    using card_of_ordLeq2[of "f ` A" A] by auto
1.13  qed
1.14 @@ -886,7 +886,7 @@
1.15    moreover have "under r a \<le> Field r"
1.16    using under_Field .
1.17    ultimately have "under r a < Field r" by blast
1.18 -  then obtain b where 1: "b : Field r \<and> ~ (b,a) : r"
1.19 +  then obtain b where 1: "b \<in> Field r \<and> \<not> (b,a) \<in> r"
1.20    unfolding under_def by blast
1.21    moreover have ba: "b \<noteq> a"
1.22    using 1 r unfolding card_order_on_def well_order_on_def
1.23 @@ -1100,7 +1100,7 @@
1.24      using 3 infinite_imp_bij_betw2[of "?Inl ` A"] by auto
1.25      moreover have "?A' = A <+> B" using Case1 by blast
1.26      ultimately have "bij_betw g (?Inl ` A) (A <+> B)" by simp
1.27 -    hence "bij_betw (g o ?Inl) A (A <+> B)"
1.28 +    hence "bij_betw (g \<circ> ?Inl) A (A <+> B)"
1.29      using 2 by (auto simp add: bij_betw_trans)
1.30      thus ?thesis using card_of_ordIso ordIso_symmetric by blast
1.31    next
1.32 @@ -1510,11 +1510,11 @@
1.33
1.34  definition regularCard where
1.35  "regularCard r \<equiv>
1.36 - ALL K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r"
1.37 + \<forall>K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r"
1.38
1.39  definition relChain where
1.40  "relChain r As \<equiv>
1.41 - ALL i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j"
1.42 + \<forall>i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j"
1.43
1.44  lemma regularCard_UNION:
1.45  assumes r: "Card_order r"   "regularCard r"
1.46 @@ -1523,17 +1523,17 @@
1.47  and cardB: "|B| <o r"
1.48  shows "EX i : Field r. B \<le> As i"
1.49  proof-
1.50 -  let ?phi = "%b j. j : Field r \<and> b : As j"
1.51 -  have "ALL b : B. EX j. ?phi b j" using Bsub by blast
1.52 +  let ?phi = "\<lambda>b j. j \<in> Field r \<and> b \<in> As j"
1.53 +  have "\<forall>b\<in>B. \<exists>j. ?phi b j" using Bsub by blast
1.54    then obtain f where f: "!! b. b : B \<Longrightarrow> ?phi b (f b)"
1.55    using bchoice[of B ?phi] by blast
1.56    let ?K = "f ` B"
1.57 -  {assume 1: "!! i. i : Field r \<Longrightarrow> ~ B \<le> As i"
1.58 +  {assume 1: "\<And>i. i \<in> Field r \<Longrightarrow> \<not> B \<le> As i"
1.59     have 2: "cofinal ?K r"
1.60     unfolding cofinal_def proof auto
1.61       fix i assume i: "i : Field r"
1.62       with 1 obtain b where b: "b : B \<and> b \<notin> As i" by blast
1.63 -     hence "i \<noteq> f b \<and> ~ (f b,i) : r"
1.64 +     hence "i \<noteq> f b \<and> \<not> (f b,i) \<in> r"
1.65       using As f unfolding relChain_def by auto
1.66       hence "i \<noteq> f b \<and> (i, f b) : r" using r
1.67       unfolding card_order_on_def well_order_on_def linear_order_on_def
```