simplify profinite class axioms
authorhuffman
Fri Jun 20 23:01:09 2008 +0200 (2008-06-20)
changeset 27310d0229bc6c461
parent 27309 c74270fd72a8
child 27311 aa28b1d33866
simplify profinite class axioms
src/HOLCF/Bifinite.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/Cprod.thy
src/HOLCF/Lift.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Up.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/Bifinite.thy	Fri Jun 20 22:51:50 2008 +0200
     1.2 +++ b/src/HOLCF/Bifinite.thy	Fri Jun 20 23:01:09 2008 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  class profinite = cpo +
     1.6    fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
     1.7 -  assumes chain_approx_app: "chain (\<lambda>i. approx i\<cdot>x)"
     1.8 +  assumes chain_approx [simp]: "chain approx"
     1.9    assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
    1.10    assumes approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    1.11    assumes finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
    1.12 @@ -27,13 +27,6 @@
    1.13  apply (clarify, erule subst, rule exI, rule refl)
    1.14  done
    1.15  
    1.16 -lemma chain_approx [simp]: "chain approx"
    1.17 -apply (rule chainI)
    1.18 -apply (rule less_cfun_ext)
    1.19 -apply (rule chainE)
    1.20 -apply (rule chain_approx_app)
    1.21 -done
    1.22 -
    1.23  lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda> x. x)"
    1.24  by (rule ext_cfun, simp add: contlub_cfun_fun)
    1.25  
     2.1 --- a/src/HOLCF/ConvexPD.thy	Fri Jun 20 22:51:50 2008 +0200
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Fri Jun 20 23:01:09 2008 +0200
     2.3 @@ -194,7 +194,7 @@
     2.4  
     2.5  instance
     2.6  apply (intro_classes, unfold approx_convex_pd_def)
     2.7 -apply (simp add: convex_pd.chain_completion_approx)
     2.8 +apply (rule convex_pd.chain_completion_approx)
     2.9  apply (rule convex_pd.lub_completion_approx)
    2.10  apply (rule convex_pd.completion_approx_idem)
    2.11  apply (rule convex_pd.finite_fixes_completion_approx)
     3.1 --- a/src/HOLCF/Cprod.thy	Fri Jun 20 22:51:50 2008 +0200
     3.2 +++ b/src/HOLCF/Cprod.thy	Fri Jun 20 23:01:09 2008 +0200
     3.3 @@ -351,7 +351,7 @@
     3.4  
     3.5  instance proof
     3.6    fix i :: nat and x :: "'a \<times> 'b"
     3.7 -  show "chain (\<lambda>i. approx i\<cdot>x)"
     3.8 +  show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)"
     3.9      unfolding approx_cprod_def by simp
    3.10    show "(\<Squnion>i. approx i\<cdot>x) = x"
    3.11      unfolding approx_cprod_def
     4.1 --- a/src/HOLCF/Lift.thy	Fri Jun 20 22:51:50 2008 +0200
     4.2 +++ b/src/HOLCF/Lift.thy	Fri Jun 20 23:01:09 2008 +0200
     4.3 @@ -137,6 +137,13 @@
     4.4  apply (rule cont_lift_case1)
     4.5  done
     4.6  
     4.7 +lemma FLIFT_mono:
     4.8 +  "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
     4.9 +apply (rule monofunE [where f=flift1])
    4.10 +apply (rule cont2mono [OF cont_flift1])
    4.11 +apply (simp add: less_fun_ext)
    4.12 +done
    4.13 +
    4.14  lemma cont2cont_flift1 [simp]:
    4.15    "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
    4.16  apply (rule cont_flift1 [THEN cont2cont_app3])
    4.17 @@ -204,9 +211,9 @@
    4.18  
    4.19  instance proof
    4.20    fix x :: "'a lift"
    4.21 -  show "chain (\<lambda>i. approx i\<cdot>x)"
    4.22 +  show "chain (approx :: nat \<Rightarrow> 'a lift \<rightarrow> 'a lift)"
    4.23      unfolding approx_lift_def
    4.24 -    by (rule chainI, cases x, simp_all)
    4.25 +    by (rule chainI, simp add: FLIFT_mono)
    4.26  next
    4.27    fix x :: "'a lift"
    4.28    show "(\<Squnion>i. approx i\<cdot>x) = x"
     5.1 --- a/src/HOLCF/LowerPD.thy	Fri Jun 20 22:51:50 2008 +0200
     5.2 +++ b/src/HOLCF/LowerPD.thy	Fri Jun 20 23:01:09 2008 +0200
     5.3 @@ -149,7 +149,7 @@
     5.4  
     5.5  instance
     5.6  apply (intro_classes, unfold approx_lower_pd_def)
     5.7 -apply (simp add: lower_pd.chain_completion_approx)
     5.8 +apply (rule lower_pd.chain_completion_approx)
     5.9  apply (rule lower_pd.lub_completion_approx)
    5.10  apply (rule lower_pd.completion_approx_idem)
    5.11  apply (rule lower_pd.finite_fixes_completion_approx)
     6.1 --- a/src/HOLCF/Sprod.thy	Fri Jun 20 22:51:50 2008 +0200
     6.2 +++ b/src/HOLCF/Sprod.thy	Fri Jun 20 23:01:09 2008 +0200
     6.3 @@ -73,7 +73,7 @@
     6.4    Rep_Sprod_inject [symmetric] less_Sprod_def
     6.5    Rep_Sprod_strict Rep_Sprod_spair
     6.6  
     6.7 -lemma Exh_Sprod2:
     6.8 +lemma Exh_Sprod:
     6.9    "z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)"
    6.10  apply (insert Rep_Sprod [of z])
    6.11  apply (simp add: Rep_Sprod_simps eq_cprod)
    6.12 @@ -85,7 +85,7 @@
    6.13  
    6.14  lemma sprodE [cases type: **]:
    6.15    "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    6.16 -by (cut_tac z=p in Exh_Sprod2, auto)
    6.17 +by (cut_tac z=p in Exh_Sprod, auto)
    6.18  
    6.19  lemma sprod_induct [induct type: **]:
    6.20    "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
    6.21 @@ -222,11 +222,14 @@
    6.22  subsection {* Strict product preserves flatness *}
    6.23  
    6.24  instance "**" :: (flat, flat) flat
    6.25 -apply (intro_classes, clarify)
    6.26 -apply (rule_tac p=x in sprodE, simp)
    6.27 -apply (rule_tac p=y in sprodE, simp)
    6.28 -apply (simp add: flat_less_iff spair_less)
    6.29 -done
    6.30 +proof
    6.31 +  fix x y :: "'a \<otimes> 'b"
    6.32 +  assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
    6.33 +    apply (induct x, simp)
    6.34 +    apply (induct y, simp)
    6.35 +    apply (simp add: spair_less_iff flat_less_iff)
    6.36 +    done
    6.37 +qed
    6.38  
    6.39  subsection {* Strict product is a bifinite domain *}
    6.40  
    6.41 @@ -239,7 +242,7 @@
    6.42  
    6.43  instance proof
    6.44    fix i :: nat and x :: "'a \<otimes> 'b"
    6.45 -  show "chain (\<lambda>i. approx i\<cdot>x)"
    6.46 +  show "chain (approx :: nat \<Rightarrow> 'a \<otimes> 'b \<rightarrow> 'a \<otimes> 'b)"
    6.47      unfolding approx_sprod_def by simp
    6.48    show "(\<Squnion>i. approx i\<cdot>x) = x"
    6.49      unfolding approx_sprod_def
    6.50 @@ -249,7 +252,7 @@
    6.51      by (simp add: ssplit_def strictify_conv_if)
    6.52    have "Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x} \<subseteq> {x. approx i\<cdot>x = x}"
    6.53      unfolding approx_sprod_def
    6.54 -    apply (clarify, rule_tac p=x in sprodE)
    6.55 +    apply (clarify, case_tac x)
    6.56       apply (simp add: Rep_Sprod_strict)
    6.57      apply (simp add: Rep_Sprod_spair spair_eq_iff)
    6.58      done
     7.1 --- a/src/HOLCF/Ssum.thy	Fri Jun 20 22:51:50 2008 +0200
     7.2 +++ b/src/HOLCF/Ssum.thy	Fri Jun 20 23:01:09 2008 +0200
     7.3 @@ -231,7 +231,7 @@
     7.4  
     7.5  instance proof
     7.6    fix i :: nat and x :: "'a \<oplus> 'b"
     7.7 -  show "chain (\<lambda>i. approx i\<cdot>x)"
     7.8 +  show "chain (approx :: nat \<Rightarrow> 'a \<oplus> 'b \<rightarrow> 'a \<oplus> 'b)"
     7.9      unfolding approx_ssum_def by simp
    7.10    show "(\<Squnion>i. approx i\<cdot>x) = x"
    7.11      unfolding approx_ssum_def
    7.12 @@ -241,7 +241,7 @@
    7.13    have "{x::'a \<oplus> 'b. approx i\<cdot>x = x} \<subseteq>
    7.14          (\<lambda>x. sinl\<cdot>x) ` {x. approx i\<cdot>x = x} \<union>
    7.15          (\<lambda>x. sinr\<cdot>x) ` {x. approx i\<cdot>x = x}"
    7.16 -    by (rule subsetI, rule_tac p=x in ssumE2, simp, simp)
    7.17 +    by (rule subsetI, case_tac x rule: ssumE2, simp, simp)
    7.18    thus "finite {x::'a \<oplus> 'b. approx i\<cdot>x = x}"
    7.19      by (rule finite_subset,
    7.20          intro finite_UnI finite_imageI finite_fixes_approx)
     8.1 --- a/src/HOLCF/Up.thy	Fri Jun 20 22:51:50 2008 +0200
     8.2 +++ b/src/HOLCF/Up.thy	Fri Jun 20 23:01:09 2008 +0200
     8.3 @@ -320,7 +320,7 @@
     8.4  
     8.5  instance proof
     8.6    fix i :: nat and x :: "'a u"
     8.7 -  show "chain (\<lambda>i. approx i\<cdot>x)"
     8.8 +  show "chain (approx :: nat \<Rightarrow> 'a u \<rightarrow> 'a u)"
     8.9      unfolding approx_up_def by simp
    8.10    show "(\<Squnion>i. approx i\<cdot>x) = x"
    8.11      unfolding approx_up_def
    8.12 @@ -331,7 +331,7 @@
    8.13    have "{x::'a u. approx i\<cdot>x = x} \<subseteq>
    8.14          insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x::'a. approx i\<cdot>x = x})"
    8.15      unfolding approx_up_def
    8.16 -    by (rule subsetI, rule_tac p=x in upE, simp_all)
    8.17 +    by (rule subsetI, case_tac x, simp_all)
    8.18    thus "finite {x::'a u. approx i\<cdot>x = x}"
    8.19      by (rule finite_subset, simp add: finite_fixes_approx)
    8.20  qed
     9.1 --- a/src/HOLCF/UpperPD.thy	Fri Jun 20 22:51:50 2008 +0200
     9.2 +++ b/src/HOLCF/UpperPD.thy	Fri Jun 20 23:01:09 2008 +0200
     9.3 @@ -147,7 +147,7 @@
     9.4  
     9.5  instance
     9.6  apply (intro_classes, unfold approx_upper_pd_def)
     9.7 -apply (simp add: upper_pd.chain_completion_approx)
     9.8 +apply (rule upper_pd.chain_completion_approx)
     9.9  apply (rule upper_pd.lub_completion_approx)
    9.10  apply (rule upper_pd.completion_approx_idem)
    9.11  apply (rule upper_pd.finite_fixes_completion_approx)