src/HOL/BNF_Greatest_Fixpoint.thy
changeset 64413 c0d5e78eb647
parent 62905 52c5a25e0c96
child 66248 df85956228c2
     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Wed Oct 26 20:59:36 2016 +0200
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Wed Oct 26 22:40:28 2016 +0200
     1.3 @@ -136,8 +136,8 @@
     1.4  lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
     1.5    by simp
     1.6  
     1.7 -lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
     1.8 -lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
     1.9 +lemma fst_diag_id: "(fst \<circ> (\<lambda>x. (x, x))) z = id z" by simp
    1.10 +lemma snd_diag_id: "(snd \<circ> (\<lambda>x. (x, x))) z = id z" by simp
    1.11  
    1.12  lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto
    1.13  lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto
    1.14 @@ -201,16 +201,16 @@
    1.15  lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
    1.16    unfolding Field_card_of csum_def by auto
    1.17  
    1.18 -lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
    1.19 +lemma rec_nat_0_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
    1.20    by auto
    1.21  
    1.22 -lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
    1.23 +lemma rec_nat_Suc_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
    1.24    by auto
    1.25  
    1.26 -lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
    1.27 +lemma rec_list_Nil_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
    1.28    by auto
    1.29  
    1.30 -lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
    1.31 +lemma rec_list_Cons_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
    1.32    by auto
    1.33  
    1.34  lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
    1.35 @@ -235,40 +235,40 @@
    1.36  subsection \<open>Equivalence relations, quotients, and Hilbert's choice\<close>
    1.37  
    1.38  lemma equiv_Eps_in:
    1.39 -"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
    1.40 +"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (\<lambda>x. x \<in> X) \<in> X"
    1.41    apply (rule someI2_ex)
    1.42    using in_quotient_imp_non_empty by blast
    1.43  
    1.44  lemma equiv_Eps_preserves:
    1.45    assumes ECH: "equiv A r" and X: "X \<in> A//r"
    1.46 -  shows "Eps (%x. x \<in> X) \<in> A"
    1.47 +  shows "Eps (\<lambda>x. x \<in> X) \<in> A"
    1.48    apply (rule in_mono[rule_format])
    1.49     using assms apply (rule in_quotient_imp_subset)
    1.50    by (rule equiv_Eps_in) (rule assms)+
    1.51  
    1.52  lemma proj_Eps:
    1.53    assumes "equiv A r" and "X \<in> A//r"
    1.54 -  shows "proj r (Eps (%x. x \<in> X)) = X"
    1.55 +  shows "proj r (Eps (\<lambda>x. x \<in> X)) = X"
    1.56  unfolding proj_def
    1.57  proof auto
    1.58    fix x assume x: "x \<in> X"
    1.59 -  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
    1.60 +  thus "(Eps (\<lambda>x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
    1.61  next
    1.62 -  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
    1.63 +  fix x assume "(Eps (\<lambda>x. x \<in> X),x) \<in> r"
    1.64    thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
    1.65  qed
    1.66  
    1.67 -definition univ where "univ f X == f (Eps (%x. x \<in> X))"
    1.68 +definition univ where "univ f X == f (Eps (\<lambda>x. x \<in> X))"
    1.69  
    1.70  lemma univ_commute:
    1.71  assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
    1.72  shows "(univ f) (proj r x) = f x"
    1.73  proof (unfold univ_def)
    1.74    have prj: "proj r x \<in> A//r" using x proj_preserves by fast
    1.75 -  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
    1.76 -  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
    1.77 -  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
    1.78 -  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
    1.79 +  hence "Eps (\<lambda>y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
    1.80 +  moreover have "proj r (Eps (\<lambda>y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
    1.81 +  ultimately have "(x, Eps (\<lambda>y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
    1.82 +  thus "f (Eps (\<lambda>y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
    1.83  qed
    1.84  
    1.85  lemma univ_preserves: