# HG changeset patch
# User huffman
# Date 1213995669 -7200
# Node ID d0229bc6c46113cf6f4062cb803ad6408ad20093
# Parent  c74270fd72a8d35db12b8ace09f2b40ece7c4e5e
simplify profinite class axioms

diff -r c74270fd72a8 -r d0229bc6c461 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Fri Jun 20 22:51:50 2008 +0200
+++ b/src/HOLCF/Bifinite.thy	Fri Jun 20 23:01:09 2008 +0200
@@ -13,7 +13,7 @@
 
 class profinite = cpo +
   fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
-  assumes chain_approx_app: "chain (\<lambda>i. approx i\<cdot>x)"
+  assumes chain_approx [simp]: "chain approx"
   assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
   assumes approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   assumes finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
@@ -27,13 +27,6 @@
 apply (clarify, erule subst, rule exI, rule refl)
 done
 
-lemma chain_approx [simp]: "chain approx"
-apply (rule chainI)
-apply (rule less_cfun_ext)
-apply (rule chainE)
-apply (rule chain_approx_app)
-done
-
 lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda> x. x)"
 by (rule ext_cfun, simp add: contlub_cfun_fun)
 
diff -r c74270fd72a8 -r d0229bc6c461 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Fri Jun 20 22:51:50 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy	Fri Jun 20 23:01:09 2008 +0200
@@ -194,7 +194,7 @@
 
 instance
 apply (intro_classes, unfold approx_convex_pd_def)
-apply (simp add: convex_pd.chain_completion_approx)
+apply (rule convex_pd.chain_completion_approx)
 apply (rule convex_pd.lub_completion_approx)
 apply (rule convex_pd.completion_approx_idem)
 apply (rule convex_pd.finite_fixes_completion_approx)
diff -r c74270fd72a8 -r d0229bc6c461 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Fri Jun 20 22:51:50 2008 +0200
+++ b/src/HOLCF/Cprod.thy	Fri Jun 20 23:01:09 2008 +0200
@@ -351,7 +351,7 @@
 
 instance proof
   fix i :: nat and x :: "'a \<times> 'b"
-  show "chain (\<lambda>i. approx i\<cdot>x)"
+  show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)"
     unfolding approx_cprod_def by simp
   show "(\<Squnion>i. approx i\<cdot>x) = x"
     unfolding approx_cprod_def
diff -r c74270fd72a8 -r d0229bc6c461 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Fri Jun 20 22:51:50 2008 +0200
+++ b/src/HOLCF/Lift.thy	Fri Jun 20 23:01:09 2008 +0200
@@ -137,6 +137,13 @@
 apply (rule cont_lift_case1)
 done
 
+lemma FLIFT_mono:
+  "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
+apply (rule monofunE [where f=flift1])
+apply (rule cont2mono [OF cont_flift1])
+apply (simp add: less_fun_ext)
+done
+
 lemma cont2cont_flift1 [simp]:
   "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
 apply (rule cont_flift1 [THEN cont2cont_app3])
@@ -204,9 +211,9 @@
 
 instance proof
   fix x :: "'a lift"
-  show "chain (\<lambda>i. approx i\<cdot>x)"
+  show "chain (approx :: nat \<Rightarrow> 'a lift \<rightarrow> 'a lift)"
     unfolding approx_lift_def
-    by (rule chainI, cases x, simp_all)
+    by (rule chainI, simp add: FLIFT_mono)
 next
   fix x :: "'a lift"
   show "(\<Squnion>i. approx i\<cdot>x) = x"
diff -r c74270fd72a8 -r d0229bc6c461 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Fri Jun 20 22:51:50 2008 +0200
+++ b/src/HOLCF/LowerPD.thy	Fri Jun 20 23:01:09 2008 +0200
@@ -149,7 +149,7 @@
 
 instance
 apply (intro_classes, unfold approx_lower_pd_def)
-apply (simp add: lower_pd.chain_completion_approx)
+apply (rule lower_pd.chain_completion_approx)
 apply (rule lower_pd.lub_completion_approx)
 apply (rule lower_pd.completion_approx_idem)
 apply (rule lower_pd.finite_fixes_completion_approx)
diff -r c74270fd72a8 -r d0229bc6c461 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Fri Jun 20 22:51:50 2008 +0200
+++ b/src/HOLCF/Sprod.thy	Fri Jun 20 23:01:09 2008 +0200
@@ -73,7 +73,7 @@
   Rep_Sprod_inject [symmetric] less_Sprod_def
   Rep_Sprod_strict Rep_Sprod_spair
 
-lemma Exh_Sprod2:
+lemma Exh_Sprod:
   "z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)"
 apply (insert Rep_Sprod [of z])
 apply (simp add: Rep_Sprod_simps eq_cprod)
@@ -85,7 +85,7 @@
 
 lemma sprodE [cases type: **]:
   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-by (cut_tac z=p in Exh_Sprod2, auto)
+by (cut_tac z=p in Exh_Sprod, auto)
 
 lemma sprod_induct [induct type: **]:
   "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
@@ -222,11 +222,14 @@
 subsection {* Strict product preserves flatness *}
 
 instance "**" :: (flat, flat) flat
-apply (intro_classes, clarify)
-apply (rule_tac p=x in sprodE, simp)
-apply (rule_tac p=y in sprodE, simp)
-apply (simp add: flat_less_iff spair_less)
-done
+proof
+  fix x y :: "'a \<otimes> 'b"
+  assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
+    apply (induct x, simp)
+    apply (induct y, simp)
+    apply (simp add: spair_less_iff flat_less_iff)
+    done
+qed
 
 subsection {* Strict product is a bifinite domain *}
 
@@ -239,7 +242,7 @@
 
 instance proof
   fix i :: nat and x :: "'a \<otimes> 'b"
-  show "chain (\<lambda>i. approx i\<cdot>x)"
+  show "chain (approx :: nat \<Rightarrow> 'a \<otimes> 'b \<rightarrow> 'a \<otimes> 'b)"
     unfolding approx_sprod_def by simp
   show "(\<Squnion>i. approx i\<cdot>x) = x"
     unfolding approx_sprod_def
@@ -249,7 +252,7 @@
     by (simp add: ssplit_def strictify_conv_if)
   have "Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x} \<subseteq> {x. approx i\<cdot>x = x}"
     unfolding approx_sprod_def
-    apply (clarify, rule_tac p=x in sprodE)
+    apply (clarify, case_tac x)
      apply (simp add: Rep_Sprod_strict)
     apply (simp add: Rep_Sprod_spair spair_eq_iff)
     done
diff -r c74270fd72a8 -r d0229bc6c461 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Fri Jun 20 22:51:50 2008 +0200
+++ b/src/HOLCF/Ssum.thy	Fri Jun 20 23:01:09 2008 +0200
@@ -231,7 +231,7 @@
 
 instance proof
   fix i :: nat and x :: "'a \<oplus> 'b"
-  show "chain (\<lambda>i. approx i\<cdot>x)"
+  show "chain (approx :: nat \<Rightarrow> 'a \<oplus> 'b \<rightarrow> 'a \<oplus> 'b)"
     unfolding approx_ssum_def by simp
   show "(\<Squnion>i. approx i\<cdot>x) = x"
     unfolding approx_ssum_def
@@ -241,7 +241,7 @@
   have "{x::'a \<oplus> 'b. approx i\<cdot>x = x} \<subseteq>
         (\<lambda>x. sinl\<cdot>x) ` {x. approx i\<cdot>x = x} \<union>
         (\<lambda>x. sinr\<cdot>x) ` {x. approx i\<cdot>x = x}"
-    by (rule subsetI, rule_tac p=x in ssumE2, simp, simp)
+    by (rule subsetI, case_tac x rule: ssumE2, simp, simp)
   thus "finite {x::'a \<oplus> 'b. approx i\<cdot>x = x}"
     by (rule finite_subset,
         intro finite_UnI finite_imageI finite_fixes_approx)
diff -r c74270fd72a8 -r d0229bc6c461 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Fri Jun 20 22:51:50 2008 +0200
+++ b/src/HOLCF/Up.thy	Fri Jun 20 23:01:09 2008 +0200
@@ -320,7 +320,7 @@
 
 instance proof
   fix i :: nat and x :: "'a u"
-  show "chain (\<lambda>i. approx i\<cdot>x)"
+  show "chain (approx :: nat \<Rightarrow> 'a u \<rightarrow> 'a u)"
     unfolding approx_up_def by simp
   show "(\<Squnion>i. approx i\<cdot>x) = x"
     unfolding approx_up_def
@@ -331,7 +331,7 @@
   have "{x::'a u. approx i\<cdot>x = x} \<subseteq>
         insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x::'a. approx i\<cdot>x = x})"
     unfolding approx_up_def
-    by (rule subsetI, rule_tac p=x in upE, simp_all)
+    by (rule subsetI, case_tac x, simp_all)
   thus "finite {x::'a u. approx i\<cdot>x = x}"
     by (rule finite_subset, simp add: finite_fixes_approx)
 qed
diff -r c74270fd72a8 -r d0229bc6c461 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Fri Jun 20 22:51:50 2008 +0200
+++ b/src/HOLCF/UpperPD.thy	Fri Jun 20 23:01:09 2008 +0200
@@ -147,7 +147,7 @@
 
 instance
 apply (intro_classes, unfold approx_upper_pd_def)
-apply (simp add: upper_pd.chain_completion_approx)
+apply (rule upper_pd.chain_completion_approx)
 apply (rule upper_pd.lub_completion_approx)
 apply (rule upper_pd.completion_approx_idem)
 apply (rule upper_pd.finite_fixes_completion_approx)