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