# HG changeset patch
# User Brian Huffman <brianh@cs.pdx.edu>
# Date 1286326380 25200
# Node ID c62b4ff97bfca5242701f7d1cdef4bdc29080a4d
# Parent  4244ff4f964919346b28861c0926acb227aaf205
add lemma finite_deflation_intro

diff -r 4244ff4f9649 -r c62b4ff97bfc src/HOLCF/Bifinite.thy
--- 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+
diff -r 4244ff4f9649 -r c62b4ff97bfc src/HOLCF/Deflation.thy
--- 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
 
diff -r 4244ff4f9649 -r c62b4ff97bfc src/HOLCF/Powerdomains.thy
--- 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)
diff -r 4244ff4f9649 -r c62b4ff97bfc src/HOLCF/Sprod.thy
--- 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+
diff -r 4244ff4f9649 -r c62b4ff97bfc src/HOLCF/Ssum.thy
--- 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+
diff -r 4244ff4f9649 -r c62b4ff97bfc src/HOLCF/Up.thy
--- 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)