# HG changeset patch
# User huffman
# Date 1289228289 28800
# Node ID 768f7e264e2b0be1e50008b40eef7269cefe89d5
# Parent  61176a1f9cd3a92ad0f8755fbf9c16968aa791f1
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances

diff -r 61176a1f9cd3 -r 768f7e264e2b src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Mon Nov 08 05:07:18 2010 -0800
+++ b/src/HOLCF/Bifinite.thy	Mon Nov 08 06:58:09 2010 -0800
@@ -71,6 +71,58 @@
   show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
 qed
 
+subsection {* Chains of approx functions *}
+
+definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
+  where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
+
+definition cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
+  where "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+definition prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
+  where "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+definition sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
+  where "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+definition ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
+  where "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+lemma approx_chain_lemma1:
+  assumes "m\<cdot>ID = ID"
+  assumes "\<And>d. finite_deflation d \<Longrightarrow> finite_deflation (m\<cdot>d)"
+  shows "approx_chain (\<lambda>i. m\<cdot>(udom_approx i))"
+by (rule approx_chain.intro)
+   (simp_all add: lub_distribs finite_deflation_udom_approx assms)
+
+lemma approx_chain_lemma2:
+  assumes "m\<cdot>ID\<cdot>ID = ID"
+  assumes "\<And>a b. \<lbrakk>finite_deflation a; finite_deflation b\<rbrakk>
+    \<Longrightarrow> finite_deflation (m\<cdot>a\<cdot>b)"
+  shows "approx_chain (\<lambda>i. m\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+by (rule approx_chain.intro)
+   (simp_all add: lub_distribs finite_deflation_udom_approx assms)
+
+lemma u_approx: "approx_chain u_approx"
+using u_map_ID finite_deflation_u_map
+unfolding u_approx_def by (rule approx_chain_lemma1)
+
+lemma cfun_approx: "approx_chain cfun_approx"
+using cfun_map_ID finite_deflation_cfun_map
+unfolding cfun_approx_def by (rule approx_chain_lemma2)
+
+lemma prod_approx: "approx_chain prod_approx"
+using cprod_map_ID finite_deflation_cprod_map
+unfolding prod_approx_def by (rule approx_chain_lemma2)
+
+lemma sprod_approx: "approx_chain sprod_approx"
+using sprod_map_ID finite_deflation_sprod_map
+unfolding sprod_approx_def by (rule approx_chain_lemma2)
+
+lemma ssum_approx: "approx_chain ssum_approx"
+using ssum_map_ID finite_deflation_ssum_map
+unfolding ssum_approx_def by (rule approx_chain_lemma2)
+
 subsection {* Type combinators *}
 
 definition
@@ -144,6 +196,53 @@
                    Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
 qed
 
+definition u_defl :: "defl \<rightarrow> defl"
+  where "u_defl = defl_fun1 u_approx u_map"
+
+definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+  where "cfun_defl = defl_fun2 cfun_approx cfun_map"
+
+definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+  where "prod_defl = defl_fun2 prod_approx cprod_map"
+
+definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+  where "sprod_defl = defl_fun2 sprod_approx sprod_map"
+
+definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "ssum_defl = defl_fun2 ssum_approx ssum_map"
+
+lemma cast_u_defl:
+  "cast\<cdot>(u_defl\<cdot>A) =
+    udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
+using u_approx finite_deflation_u_map
+unfolding u_defl_def by (rule cast_defl_fun1)
+
+lemma cast_cfun_defl:
+  "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) =
+    udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
+using cfun_approx finite_deflation_cfun_map
+unfolding cfun_defl_def by (rule cast_defl_fun2)
+
+lemma cast_prod_defl:
+  "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
+    cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
+using prod_approx finite_deflation_cprod_map
+unfolding prod_defl_def by (rule cast_defl_fun2)
+
+lemma cast_sprod_defl:
+  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
+    udom_emb sprod_approx oo
+      sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
+        udom_prj sprod_approx"
+using sprod_approx finite_deflation_sprod_map
+unfolding sprod_defl_def by (rule cast_defl_fun2)
+
+lemma cast_ssum_defl:
+  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
+    udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
+using ssum_approx finite_deflation_ssum_map
+unfolding ssum_defl_def by (rule cast_defl_fun2)
+
 subsection {* The universal domain is bifinite *}
 
 instantiation udom :: bifinite
@@ -161,7 +260,6 @@
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> udom)"
     by (simp add: ep_pair.intro)
-next
   show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"
     unfolding defl_udom_def
     apply (subst contlub_cfun_arg)
@@ -180,34 +278,6 @@
 
 subsection {* Continuous function space is a bifinite domain *}
 
-definition
-  cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
-where
-  "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma cfun_approx: "approx_chain cfun_approx"
-proof (rule approx_chain.intro)
-  show "chain (\<lambda>i. cfun_approx i)"
-    unfolding cfun_approx_def by simp
-  show "(\<Squnion>i. cfun_approx i) = ID"
-    unfolding cfun_approx_def
-    by (simp add: lub_distribs cfun_map_ID)
-  show "\<And>i. finite_deflation (cfun_approx i)"
-    unfolding cfun_approx_def
-    by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
-qed
-
-definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
-where "cfun_defl = defl_fun2 cfun_approx cfun_map"
-
-lemma cast_cfun_defl:
-  "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) =
-    udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
-unfolding cfun_defl_def
-apply (rule cast_defl_fun2 [OF cfun_approx])
-apply (erule (1) finite_deflation_cfun_map)
-done
-
 instantiation cfun :: (bifinite, bifinite) bifinite
 begin
 
@@ -239,34 +309,6 @@
 
 subsection {* Cartesian product is a bifinite domain *}
 
-definition
-  prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
-where
-  "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma prod_approx: "approx_chain prod_approx"
-proof (rule approx_chain.intro)
-  show "chain (\<lambda>i. prod_approx i)"
-    unfolding prod_approx_def by simp
-  show "(\<Squnion>i. prod_approx i) = ID"
-    unfolding prod_approx_def
-    by (simp add: lub_distribs cprod_map_ID)
-  show "\<And>i. finite_deflation (prod_approx i)"
-    unfolding prod_approx_def
-    by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
-qed
-
-definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
-where "prod_defl = defl_fun2 prod_approx cprod_map"
-
-lemma cast_prod_defl:
-  "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
-    cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
-unfolding prod_defl_def
-apply (rule cast_defl_fun2 [OF prod_approx])
-apply (erule (1) finite_deflation_cprod_map)
-done
-
 instantiation prod :: (bifinite, bifinite) bifinite
 begin
 
@@ -298,36 +340,6 @@
 
 subsection {* Strict product is a bifinite domain *}
 
-definition
-  sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
-where
-  "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma sprod_approx: "approx_chain sprod_approx"
-proof (rule approx_chain.intro)
-  show "chain (\<lambda>i. sprod_approx i)"
-    unfolding sprod_approx_def by simp
-  show "(\<Squnion>i. sprod_approx i) = ID"
-    unfolding sprod_approx_def
-    by (simp add: lub_distribs sprod_map_ID)
-  show "\<And>i. finite_deflation (sprod_approx i)"
-    unfolding sprod_approx_def
-    by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
-qed
-
-definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
-where "sprod_defl = defl_fun2 sprod_approx sprod_map"
-
-lemma cast_sprod_defl:
-  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
-    udom_emb sprod_approx oo
-      sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
-        udom_prj sprod_approx"
-unfolding sprod_defl_def
-apply (rule cast_defl_fun2 [OF sprod_approx])
-apply (erule (1) finite_deflation_sprod_map)
-done
-
 instantiation sprod :: (bifinite, bifinite) bifinite
 begin
 
@@ -359,32 +371,6 @@
 
 subsection {* Lifted cpo is a bifinite domain *}
 
-definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
-where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
-
-lemma u_approx: "approx_chain u_approx"
-proof (rule approx_chain.intro)
-  show "chain (\<lambda>i. u_approx i)"
-    unfolding u_approx_def by simp
-  show "(\<Squnion>i. u_approx i) = ID"
-    unfolding u_approx_def
-    by (simp add: lub_distribs u_map_ID)
-  show "\<And>i. finite_deflation (u_approx i)"
-    unfolding u_approx_def
-    by (intro finite_deflation_u_map finite_deflation_udom_approx)
-qed
-
-definition u_defl :: "defl \<rightarrow> defl"
-where "u_defl = defl_fun1 u_approx u_map"
-
-lemma cast_u_defl:
-  "cast\<cdot>(u_defl\<cdot>A) =
-    udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
-unfolding u_defl_def
-apply (rule cast_defl_fun1 [OF u_approx])
-apply (erule finite_deflation_u_map)
-done
-
 instantiation u :: (bifinite) bifinite
 begin
 
@@ -500,34 +486,6 @@
 
 subsection {* Strict sum is a bifinite domain *}
 
-definition
-  ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
-where
-  "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma ssum_approx: "approx_chain ssum_approx"
-proof (rule approx_chain.intro)
-  show "chain (\<lambda>i. ssum_approx i)"
-    unfolding ssum_approx_def by simp
-  show "(\<Squnion>i. ssum_approx i) = ID"
-    unfolding ssum_approx_def
-    by (simp add: lub_distribs ssum_map_ID)
-  show "\<And>i. finite_deflation (ssum_approx i)"
-    unfolding ssum_approx_def
-    by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
-qed
-
-definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
-where "ssum_defl = defl_fun2 ssum_approx ssum_map"
-
-lemma cast_ssum_defl:
-  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
-    udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
-unfolding ssum_defl_def
-apply (rule cast_defl_fun2 [OF ssum_approx])
-apply (erule (1) finite_deflation_ssum_map)
-done
-
 instantiation ssum :: (bifinite, bifinite) bifinite
 begin
 
diff -r 61176a1f9cd3 -r 768f7e264e2b src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Mon Nov 08 05:07:18 2010 -0800
+++ b/src/HOLCF/ConvexPD.thy	Mon Nov 08 06:58:09 2010 -0800
@@ -448,16 +448,8 @@
   "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))"
 
 lemma convex_approx: "approx_chain convex_approx"
-proof (rule approx_chain.intro)
-  show "chain (\<lambda>i. convex_approx i)"
-    unfolding convex_approx_def by simp
-  show "(\<Squnion>i. convex_approx i) = ID"
-    unfolding convex_approx_def
-    by (simp add: lub_distribs convex_map_ID)
-  show "\<And>i. finite_deflation (convex_approx i)"
-    unfolding convex_approx_def
-    by (intro finite_deflation_convex_map finite_deflation_udom_approx)
-qed
+using convex_map_ID finite_deflation_convex_map
+unfolding convex_approx_def by (rule approx_chain_lemma1)
 
 definition convex_defl :: "defl \<rightarrow> defl"
 where "convex_defl = defl_fun1 convex_approx convex_map"
@@ -465,10 +457,8 @@
 lemma cast_convex_defl:
   "cast\<cdot>(convex_defl\<cdot>A) =
     udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx"
-unfolding convex_defl_def
-apply (rule cast_defl_fun1 [OF convex_approx])
-apply (erule finite_deflation_convex_map)
-done
+using convex_approx finite_deflation_convex_map
+unfolding convex_defl_def by (rule cast_defl_fun1)
 
 instantiation convex_pd :: (bifinite) bifinite
 begin
diff -r 61176a1f9cd3 -r 768f7e264e2b src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Mon Nov 08 05:07:18 2010 -0800
+++ b/src/HOLCF/LowerPD.thy	Mon Nov 08 06:58:09 2010 -0800
@@ -441,16 +441,8 @@
   "lower_approx = (\<lambda>i. lower_map\<cdot>(udom_approx i))"
 
 lemma lower_approx: "approx_chain lower_approx"
-proof (rule approx_chain.intro)
-  show "chain (\<lambda>i. lower_approx i)"
-    unfolding lower_approx_def by simp
-  show "(\<Squnion>i. lower_approx i) = ID"
-    unfolding lower_approx_def
-    by (simp add: lub_distribs lower_map_ID)
-  show "\<And>i. finite_deflation (lower_approx i)"
-    unfolding lower_approx_def
-    by (intro finite_deflation_lower_map finite_deflation_udom_approx)
-qed
+using lower_map_ID finite_deflation_lower_map
+unfolding lower_approx_def by (rule approx_chain_lemma1)
 
 definition lower_defl :: "defl \<rightarrow> defl"
 where "lower_defl = defl_fun1 lower_approx lower_map"
@@ -458,10 +450,8 @@
 lemma cast_lower_defl:
   "cast\<cdot>(lower_defl\<cdot>A) =
     udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx"
-unfolding lower_defl_def
-apply (rule cast_defl_fun1 [OF lower_approx])
-apply (erule finite_deflation_lower_map)
-done
+using lower_approx finite_deflation_lower_map
+unfolding lower_defl_def by (rule cast_defl_fun1)
 
 instantiation lower_pd :: (bifinite) bifinite
 begin
diff -r 61176a1f9cd3 -r 768f7e264e2b src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Mon Nov 08 05:07:18 2010 -0800
+++ b/src/HOLCF/UpperPD.thy	Mon Nov 08 06:58:09 2010 -0800
@@ -436,16 +436,8 @@
   "upper_approx = (\<lambda>i. upper_map\<cdot>(udom_approx i))"
 
 lemma upper_approx: "approx_chain upper_approx"
-proof (rule approx_chain.intro)
-  show "chain (\<lambda>i. upper_approx i)"
-    unfolding upper_approx_def by simp
-  show "(\<Squnion>i. upper_approx i) = ID"
-    unfolding upper_approx_def
-    by (simp add: lub_distribs upper_map_ID)
-  show "\<And>i. finite_deflation (upper_approx i)"
-    unfolding upper_approx_def
-    by (intro finite_deflation_upper_map finite_deflation_udom_approx)
-qed
+using upper_map_ID finite_deflation_upper_map
+unfolding upper_approx_def by (rule approx_chain_lemma1)
 
 definition upper_defl :: "defl \<rightarrow> defl"
 where "upper_defl = defl_fun1 upper_approx upper_map"
@@ -453,10 +445,8 @@
 lemma cast_upper_defl:
   "cast\<cdot>(upper_defl\<cdot>A) =
     udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
-unfolding upper_defl_def
-apply (rule cast_defl_fun1 [OF upper_approx])
-apply (erule finite_deflation_upper_map)
-done
+using upper_approx finite_deflation_upper_map
+unfolding upper_defl_def by (rule cast_defl_fun1)
 
 instantiation upper_pd :: (bifinite) bifinite
 begin