src/HOLCF/Deflation.thy
changeset 39973 c62b4ff97bfc
parent 39971 2949af5e6b9c
child 39985 310f98585107
     1.1 --- a/src/HOLCF/Deflation.thy	Tue Oct 05 17:36:45 2010 -0700
     1.2 +++ b/src/HOLCF/Deflation.thy	Tue Oct 05 17:53:00 2010 -0700
     1.3 @@ -152,6 +152,10 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma finite_deflation_intro:
     1.8 +  "deflation d \<Longrightarrow> finite {x. d\<cdot>x = x} \<Longrightarrow> finite_deflation d"
     1.9 +by (intro finite_deflation.intro finite_deflation_axioms.intro)
    1.10 +
    1.11  lemma finite_deflation_imp_deflation:
    1.12    "finite_deflation d \<Longrightarrow> deflation d"
    1.13  unfolding finite_deflation_def by simp
    1.14 @@ -299,22 +303,19 @@
    1.15  proof -
    1.16    interpret d: finite_deflation d by fact
    1.17    show ?thesis
    1.18 -  proof (intro_locales)
    1.19 +  proof (rule finite_deflation_intro)
    1.20      have "deflation d" ..
    1.21      thus "deflation (p oo d oo e)"
    1.22        using d by (rule deflation_p_d_e)
    1.23    next
    1.24 -    show "finite_deflation_axioms (p oo d oo e)"
    1.25 -    proof
    1.26 -      have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
    1.27 -        by (rule d.finite_image)
    1.28 -      hence "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
    1.29 -        by (rule finite_imageI)
    1.30 -      hence "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
    1.31 -        by (simp add: image_image)
    1.32 -      thus "finite {x. (p oo d oo e)\<cdot>x = x}"
    1.33 -        by (rule finite_range_imp_finite_fixes)
    1.34 -    qed
    1.35 +    have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
    1.36 +      by (rule d.finite_image)
    1.37 +    hence "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
    1.38 +      by (rule finite_imageI)
    1.39 +    hence "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
    1.40 +      by (simp add: image_image)
    1.41 +    thus "finite {x. (p oo d oo e)\<cdot>x = x}"
    1.42 +      by (rule finite_range_imp_finite_fixes)
    1.43    qed
    1.44  qed
    1.45