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