src/HOL/BNF_Wellorder_Constructions.thy
changeset 63040 eb4ddd18d635
parent 61943 7fba644ed827
child 63092 a949b2a5f51d
     1.1 --- a/src/HOL/BNF_Wellorder_Constructions.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/BNF_Wellorder_Constructions.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -1616,7 +1616,7 @@
     1.4    show ?thesis
     1.5    proof safe
     1.6      fix h assume h: "h \<in> Func B2 B1"
     1.7 -    def j1 \<equiv> "inv_into A1 f1"
     1.8 +    define j1 where "j1 = inv_into A1 f1"
     1.9      have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast
    1.10      then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2"
    1.11        by atomize_elim (rule bchoice)
    1.12 @@ -1626,11 +1626,11 @@
    1.13       ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast
    1.14      } note kk = this
    1.15      obtain b22 where b22: "b22 \<in> B2" using B2 by auto
    1.16 -    def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2 ` B2 then k a2 else b22"
    1.17 +    define j2 where [abs_def]: "j2 a2 = (if a2 \<in> f2 ` B2 then k a2 else b22)" for a2
    1.18      have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto
    1.19      have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2"
    1.20      using kk unfolding j2_def by auto
    1.21 -    def g \<equiv> "Func_map A2 j1 j2 h"
    1.22 +    define g where "g = Func_map A2 j1 j2 h"
    1.23      have "Func_map B2 f1 f2 g = h"
    1.24      proof (rule ext)
    1.25        fix b2 show "Func_map B2 f1 f2 g b2 = h b2"