src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 63040 eb4ddd18d635
parent 62390 842917225d56
child 63980 f8e556c8ad6f
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -470,10 +470,15 @@
     1.4  fixes A :: "'a set" and B :: "'b set" and C :: "'c set"
     1.5  shows "|(A <+> B) <+> C| =o |A <+> B <+> C|"
     1.6  proof -
     1.7 -  def f \<equiv> "\<lambda>(k::('a + 'b) + 'c).
     1.8 -  case k of Inl ab \<Rightarrow> (case ab of Inl a \<Rightarrow> Inl a
     1.9 -                                 |Inr b \<Rightarrow> Inr (Inl b))
    1.10 -           |Inr c \<Rightarrow> Inr (Inr c)"
    1.11 +  define f :: "('a + 'b) + 'c \<Rightarrow> 'a + 'b + 'c"
    1.12 +    where [abs_def]: "f k =
    1.13 +      (case k of
    1.14 +        Inl ab \<Rightarrow>
    1.15 +          (case ab of
    1.16 +            Inl a \<Rightarrow> Inl a
    1.17 +          | Inr b \<Rightarrow> Inr (Inl b))
    1.18 +      | Inr c \<Rightarrow> Inr (Inr c))"
    1.19 +    for k
    1.20    have "A <+> B <+> C \<subseteq> f ` ((A <+> B) <+> C)"
    1.21    proof
    1.22      fix x assume x: "x \<in> A <+> B <+> C"
    1.23 @@ -499,7 +504,7 @@
    1.24      qed
    1.25    qed
    1.26    hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)"
    1.27 -  unfolding bij_betw_def inj_on_def f_def by fastforce
    1.28 +    unfolding bij_betw_def inj_on_def f_def by fastforce
    1.29    thus ?thesis using card_of_ordIso by blast
    1.30  qed
    1.31  
    1.32 @@ -1626,8 +1631,8 @@
    1.33  lemma card_of_Pow_Func:
    1.34  "|Pow A| =o |Func A (UNIV::bool set)|"
    1.35  proof-
    1.36 -  def F \<equiv> "\<lambda> A' a. if a \<in> A then (if a \<in> A' then True else False)
    1.37 -                            else undefined"
    1.38 +  define F where [abs_def]: "F A' a =
    1.39 +    (if a \<in> A then (if a \<in> A' then True else False) else undefined)" for A' a
    1.40    have "bij_betw F (Pow A) (Func A (UNIV::bool set))"
    1.41    unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI)
    1.42      fix A1 A2 assume "A1 \<in> Pow A" "A2 \<in> Pow A" "F A1 = F A2"
    1.43 @@ -1638,8 +1643,9 @@
    1.44        fix f assume f: "f \<in> Func A (UNIV::bool set)"
    1.45        show "f \<in> F ` Pow A" unfolding image_def mem_Collect_eq proof(intro bexI)
    1.46          let ?A1 = "{a \<in> A. f a = True}"
    1.47 -        show "f = F ?A1" unfolding F_def apply(rule ext)
    1.48 -        using f unfolding Func_def mem_Collect_eq by auto
    1.49 +        show "f = F ?A1"
    1.50 +          unfolding F_def apply(rule ext)
    1.51 +          using f unfolding Func_def mem_Collect_eq by auto
    1.52        qed auto
    1.53      qed(unfold Func_def mem_Collect_eq F_def, auto)
    1.54    qed