clean up and rename some profinite lemmas
authorhuffman
Fri Jun 20 22:51:50 2008 +0200 (2008-06-20)
changeset 27309c74270fd72a8
parent 27308 b915a10a616a
child 27310 d0229bc6c461
clean up and rename some profinite lemmas
src/HOLCF/Bifinite.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/Bifinite.thy	Fri Jun 20 22:41:41 2008 +0200
     1.2 +++ b/src/HOLCF/Bifinite.thy	Fri Jun 20 22:51:50 2008 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  apply (rule is_ub_thelub, simp)
     1.5  done
     1.6  
     1.7 -lemma approx_strict [simp]: "approx i\<cdot>(\<bottom>::'a::bifinite) = \<bottom>"
     1.8 +lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>"
     1.9  by (rule UU_I, rule approx_less)
    1.10  
    1.11  lemma approx_approx1:
    1.12 @@ -113,23 +113,12 @@
    1.13    thus "\<exists>j. approx n\<cdot>x \<sqsubseteq> Y j" ..
    1.14  qed
    1.15  
    1.16 -lemma bifinite_compact_eq_approx:
    1.17 -  assumes x: "compact x"
    1.18 -  shows "\<exists>i. approx i\<cdot>x = x"
    1.19 -proof -
    1.20 -  have chain: "chain (\<lambda>i. approx i\<cdot>x)" by simp
    1.21 -  have less: "x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by simp
    1.22 -  obtain i where i: "x \<sqsubseteq> approx i\<cdot>x"
    1.23 -    using compactD2 [OF x chain less] ..
    1.24 -  with approx_less have "approx i\<cdot>x = x"
    1.25 -    by (rule antisym_less)
    1.26 -  thus "\<exists>i. approx i\<cdot>x = x" ..
    1.27 -qed
    1.28 +lemma profinite_compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
    1.29 +by (rule admD2) simp_all
    1.30  
    1.31 -lemma bifinite_compact_iff:
    1.32 -  "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)"
    1.33 +lemma profinite_compact_iff: "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)"
    1.34   apply (rule iffI)
    1.35 -  apply (erule bifinite_compact_eq_approx)
    1.36 +  apply (erule profinite_compact_eq_approx)
    1.37   apply (erule exE)
    1.38   apply (erule subst)
    1.39   apply (rule compact_approx)
    1.40 @@ -144,7 +133,7 @@
    1.41    thus "P x" by simp
    1.42  qed
    1.43  
    1.44 -lemma bifinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
    1.45 +lemma profinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
    1.46  apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
    1.47  apply (rule lub_mono, simp, simp, simp)
    1.48  done
     2.1 --- a/src/HOLCF/CompactBasis.thy	Fri Jun 20 22:41:41 2008 +0200
     2.2 +++ b/src/HOLCF/CompactBasis.thy	Fri Jun 20 22:51:50 2008 +0200
     2.3 @@ -493,7 +493,7 @@
     2.4    show "\<exists>n. compact_approx n a = a"
     2.5      apply (simp add: Rep_compact_basis_inject [symmetric])
     2.6      apply (simp add: Rep_compact_approx)
     2.7 -    apply (rule bifinite_compact_eq_approx)
     2.8 +    apply (rule profinite_compact_eq_approx)
     2.9      apply (rule compact_Rep_compact_basis)
    2.10      done
    2.11  qed
    2.12 @@ -523,8 +523,8 @@
    2.13        apply simp
    2.14        apply (cut_tac a=x in compact_Rep_compact_basis)
    2.15        apply (cut_tac a=y in compact_Rep_compact_basis)
    2.16 -      apply (drule bifinite_compact_eq_approx)
    2.17 -      apply (drule bifinite_compact_eq_approx)
    2.18 +      apply (drule profinite_compact_eq_approx)
    2.19 +      apply (drule profinite_compact_eq_approx)
    2.20        apply (clarify, rename_tac i j)
    2.21        apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
    2.22        apply (simp add: compact_le_def)
     3.1 --- a/src/HOLCF/ConvexPD.thy	Fri Jun 20 22:41:41 2008 +0200
     3.2 +++ b/src/HOLCF/ConvexPD.thy	Fri Jun 20 22:51:50 2008 +0200
     3.3 @@ -327,7 +327,7 @@
     3.4  
     3.5  lemma convex_unit_less_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
     3.6   apply (rule iffI)
     3.7 -  apply (rule bifinite_less_ext)
     3.8 +  apply (rule profinite_less_ext)
     3.9    apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
    3.10    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
    3.11    apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
    3.12 @@ -346,7 +346,7 @@
    3.13  
    3.14  lemma compact_convex_unit_iff [simp]:
    3.15    "compact {x}\<natural> \<longleftrightarrow> compact x"
    3.16 -unfolding bifinite_compact_iff by simp
    3.17 +unfolding profinite_compact_iff by simp
    3.18  
    3.19  lemma compact_convex_plus [simp]:
    3.20    "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<natural> ys)"
    3.21 @@ -589,7 +589,7 @@
    3.22      (convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and>
    3.23       convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)"
    3.24   apply (safe elim!: monofun_cfun_arg)
    3.25 - apply (rule bifinite_less_ext)
    3.26 + apply (rule profinite_less_ext)
    3.27   apply (drule_tac f="approx i" in monofun_cfun_arg)
    3.28   apply (drule_tac f="approx i" in monofun_cfun_arg)
    3.29   apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
     4.1 --- a/src/HOLCF/LowerPD.thy	Fri Jun 20 22:41:41 2008 +0200
     4.2 +++ b/src/HOLCF/LowerPD.thy	Fri Jun 20 22:51:50 2008 +0200
     4.3 @@ -284,7 +284,7 @@
     4.4  
     4.5  lemma lower_unit_less_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
     4.6   apply (rule iffI)
     4.7 -  apply (rule bifinite_less_ext)
     4.8 +  apply (rule profinite_less_ext)
     4.9    apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
    4.10    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
    4.11    apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
    4.12 @@ -331,7 +331,7 @@
    4.13  done
    4.14  
    4.15  lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x"
    4.16 -unfolding bifinite_compact_iff by simp
    4.17 +unfolding profinite_compact_iff by simp
    4.18  
    4.19  lemma compact_lower_plus [simp]:
    4.20    "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"
     5.1 --- a/src/HOLCF/UpperPD.thy	Fri Jun 20 22:41:41 2008 +0200
     5.2 +++ b/src/HOLCF/UpperPD.thy	Fri Jun 20 22:51:50 2008 +0200
     5.3 @@ -282,7 +282,7 @@
     5.4  
     5.5  lemma upper_unit_less_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
     5.6   apply (rule iffI)
     5.7 -  apply (rule bifinite_less_ext)
     5.8 +  apply (rule profinite_less_ext)
     5.9    apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
    5.10    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
    5.11    apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
    5.12 @@ -321,7 +321,7 @@
    5.13  done
    5.14  
    5.15  lemma compact_upper_unit_iff [simp]: "compact {x}\<sharp> \<longleftrightarrow> compact x"
    5.16 -unfolding bifinite_compact_iff by simp
    5.17 +unfolding profinite_compact_iff by simp
    5.18  
    5.19  lemma compact_upper_plus [simp]:
    5.20    "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<sharp> ys)"