--- a/src/HOLCF/Bifinite.thy Tue Oct 05 17:36:45 2010 -0700
+++ b/src/HOLCF/Bifinite.thy Tue Oct 05 17:53:00 2010 -0700
@@ -150,7 +150,7 @@
lemma finite_deflation_cprod_map:
assumes "finite_deflation d1" and "finite_deflation d2"
shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
@@ -283,7 +283,7 @@
lemma finite_deflation_cfun_map:
assumes "finite_deflation d1" and "finite_deflation d2"
shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
--- a/src/HOLCF/Deflation.thy Tue Oct 05 17:36:45 2010 -0700
+++ b/src/HOLCF/Deflation.thy Tue Oct 05 17:53:00 2010 -0700
@@ -152,6 +152,10 @@
end
+lemma finite_deflation_intro:
+ "deflation d \<Longrightarrow> finite {x. d\<cdot>x = x} \<Longrightarrow> finite_deflation d"
+by (intro finite_deflation.intro finite_deflation_axioms.intro)
+
lemma finite_deflation_imp_deflation:
"finite_deflation d \<Longrightarrow> deflation d"
unfolding finite_deflation_def by simp
@@ -299,22 +303,19 @@
proof -
interpret d: finite_deflation d by fact
show ?thesis
- proof (intro_locales)
+ proof (rule finite_deflation_intro)
have "deflation d" ..
thus "deflation (p oo d oo e)"
using d by (rule deflation_p_d_e)
next
- show "finite_deflation_axioms (p oo d oo e)"
- proof
- have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
- by (rule d.finite_image)
- hence "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
- by (rule finite_imageI)
- hence "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
- by (simp add: image_image)
- thus "finite {x. (p oo d oo e)\<cdot>x = x}"
- by (rule finite_range_imp_finite_fixes)
- qed
+ have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
+ by (rule d.finite_image)
+ hence "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
+ by (rule finite_imageI)
+ hence "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
+ by (simp add: image_image)
+ thus "finite {x. (p oo d oo e)\<cdot>x = x}"
+ by (rule finite_range_imp_finite_fixes)
qed
qed
--- a/src/HOLCF/Powerdomains.thy Tue Oct 05 17:36:45 2010 -0700
+++ b/src/HOLCF/Powerdomains.thy Tue Oct 05 17:53:00 2010 -0700
@@ -85,7 +85,7 @@
lemma finite_deflation_upper_map:
assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>d)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+proof (rule finite_deflation_intro)
interpret d: finite_deflation d by fact
have "deflation d" by fact
thus "deflation (upper_map\<cdot>d)" by (rule deflation_upper_map)
@@ -130,7 +130,7 @@
lemma finite_deflation_lower_map:
assumes "finite_deflation d" shows "finite_deflation (lower_map\<cdot>d)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+proof (rule finite_deflation_intro)
interpret d: finite_deflation d by fact
have "deflation d" by fact
thus "deflation (lower_map\<cdot>d)" by (rule deflation_lower_map)
@@ -175,7 +175,7 @@
lemma finite_deflation_convex_map:
assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>d)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+proof (rule finite_deflation_intro)
interpret d: finite_deflation d by fact
have "deflation d" by fact
thus "deflation (convex_map\<cdot>d)" by (rule deflation_convex_map)
--- a/src/HOLCF/Sprod.thy Tue Oct 05 17:36:45 2010 -0700
+++ b/src/HOLCF/Sprod.thy Tue Oct 05 17:53:00 2010 -0700
@@ -298,7 +298,7 @@
lemma finite_deflation_sprod_map:
assumes "finite_deflation d1" and "finite_deflation d2"
shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
--- a/src/HOLCF/Ssum.thy Tue Oct 05 17:36:45 2010 -0700
+++ b/src/HOLCF/Ssum.thy Tue Oct 05 17:53:00 2010 -0700
@@ -282,7 +282,7 @@
lemma finite_deflation_ssum_map:
assumes "finite_deflation d1" and "finite_deflation d2"
shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
--- a/src/HOLCF/Up.thy Tue Oct 05 17:36:45 2010 -0700
+++ b/src/HOLCF/Up.thy Tue Oct 05 17:53:00 2010 -0700
@@ -322,7 +322,7 @@
lemma finite_deflation_u_map:
assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+proof (rule finite_deflation_intro)
interpret d: finite_deflation d by fact
have "deflation d" by fact
thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map)