src/HOL/Inductive.thy
changeset 63540 f8652d0534fa
parent 63400 249fa34faba2
child 63561 fba08009ff3e
     1.1 --- a/src/HOL/Inductive.thy	Fri Jul 22 08:02:37 2016 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Fri Jul 22 11:00:43 2016 +0200
     1.3 @@ -270,10 +270,10 @@
     1.4    show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
     1.5    proof (rule lfp_greatest)
     1.6      fix u
     1.7 -    assume "g (f u) \<le> u"
     1.8 -    moreover then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
     1.9 +    assume u: "g (f u) \<le> u"
    1.10 +    then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
    1.11        by (intro assms[THEN monoD] lfp_lowerbound)
    1.12 -    ultimately show "g (lfp (\<lambda>x. f (g x))) \<le> u"
    1.13 +    with u show "g (lfp (\<lambda>x. f (g x))) \<le> u"
    1.14        by auto
    1.15    qed
    1.16  qed
    1.17 @@ -307,10 +307,11 @@
    1.18      by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
    1.19    show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
    1.20    proof (rule gfp_least)
    1.21 -    fix u assume "u \<le> g (f u)"
    1.22 -    moreover then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
    1.23 +    fix u
    1.24 +    assume u: "u \<le> g (f u)"
    1.25 +    then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
    1.26        by (intro assms[THEN monoD] gfp_upperbound)
    1.27 -    ultimately show "u \<le> g (gfp (\<lambda>x. f (g x)))"
    1.28 +    with u show "u \<le> g (gfp (\<lambda>x. f (g x)))"
    1.29        by auto
    1.30    qed
    1.31  qed