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
```