src/HOLCF/LowerPD.thy
changeset 27289 c49d427867aa
parent 27267 5ebfb7f25ebb
child 27297 2c42b1505f25
     1.1 --- a/src/HOLCF/LowerPD.thy	Thu Jun 19 22:43:59 2008 +0200
     1.2 +++ b/src/HOLCF/LowerPD.thy	Thu Jun 19 22:50:58 2008 +0200
     1.3 @@ -72,23 +72,23 @@
     1.4  apply (simp add: lower_le_PDPlus_iff 3)
     1.5  done
     1.6  
     1.7 -lemma approx_pd_lower_mono1:
     1.8 -  "i \<le> j \<Longrightarrow> approx_pd i t \<le>\<flat> approx_pd j t"
     1.9 +lemma approx_pd_lower_chain:
    1.10 +  "approx_pd n t \<le>\<flat> approx_pd (Suc n) t"
    1.11  apply (induct t rule: pd_basis_induct)
    1.12 -apply (simp add: compact_approx_mono1)
    1.13 +apply (simp add: compact_basis.take_chain)
    1.14  apply (simp add: PDPlus_lower_mono)
    1.15  done
    1.16  
    1.17  lemma approx_pd_lower_le: "approx_pd i t \<le>\<flat> t"
    1.18  apply (induct t rule: pd_basis_induct)
    1.19 -apply (simp add: compact_approx_le)
    1.20 +apply (simp add: compact_basis.take_less)
    1.21  apply (simp add: PDPlus_lower_mono)
    1.22  done
    1.23  
    1.24  lemma approx_pd_lower_mono:
    1.25    "t \<le>\<flat> u \<Longrightarrow> approx_pd n t \<le>\<flat> approx_pd n u"
    1.26  apply (erule lower_le_induct)
    1.27 -apply (simp add: compact_approx_mono)
    1.28 +apply (simp add: compact_basis.take_mono)
    1.29  apply (simp add: lower_le_PDUnit_PDPlus_iff)
    1.30  apply (simp add: lower_le_PDPlus_iff)
    1.31  done
    1.32 @@ -122,29 +122,16 @@
    1.33  apply (rule approx_pd_lower_le)
    1.34  apply (rule approx_pd_idem)
    1.35  apply (erule approx_pd_lower_mono)
    1.36 -apply (rule approx_pd_lower_mono1, simp)
    1.37 +apply (rule approx_pd_lower_chain)
    1.38  apply (rule finite_range_approx_pd)
    1.39 -apply (rule ex_approx_pd_eq)
    1.40 +apply (rule approx_pd_covers)
    1.41  apply (rule ideal_Rep_lower_pd)
    1.42  apply (rule cont_Rep_lower_pd)
    1.43  apply (rule Rep_lower_principal)
    1.44  apply (simp only: less_lower_pd_def less_set_eq)
    1.45  done
    1.46  
    1.47 -lemma lower_principal_less_iff [simp]:
    1.48 -  "lower_principal t \<sqsubseteq> lower_principal u \<longleftrightarrow> t \<le>\<flat> u"
    1.49 -by (rule lower_pd.principal_less_iff)
    1.50 -
    1.51 -lemma lower_principal_eq_iff:
    1.52 -  "lower_principal t = lower_principal u \<longleftrightarrow> t \<le>\<flat> u \<and> u \<le>\<flat> t"
    1.53 -by (rule lower_pd.principal_eq_iff)
    1.54 -
    1.55 -lemma lower_principal_mono:
    1.56 -  "t \<le>\<flat> u \<Longrightarrow> lower_principal t \<sqsubseteq> lower_principal u"
    1.57 -by (rule lower_pd.principal_mono)
    1.58 -
    1.59 -lemma compact_lower_principal: "compact (lower_principal t)"
    1.60 -by (rule lower_pd.compact_principal)
    1.61 +text {* Lower powerdomain is pointed *}
    1.62  
    1.63  lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
    1.64  by (induct ys rule: lower_pd.principal_induct, simp, simp)
    1.65 @@ -155,8 +142,7 @@
    1.66  lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
    1.67  by (rule lower_pd_minimal [THEN UU_I, symmetric])
    1.68  
    1.69 -
    1.70 -subsection {* Approximation *}
    1.71 +text {* Lower powerdomain is profinite *}
    1.72  
    1.73  instantiation lower_pd :: (profinite) profinite
    1.74  begin
    1.75 @@ -186,24 +172,6 @@
    1.76  unfolding approx_lower_pd_def
    1.77  by (rule lower_pd.completion_approx_eq_principal)
    1.78  
    1.79 -lemma compact_imp_lower_principal:
    1.80 -  "compact xs \<Longrightarrow> \<exists>t. xs = lower_principal t"
    1.81 -by (rule lower_pd.compact_imp_principal)
    1.82 -
    1.83 -lemma lower_principal_induct:
    1.84 -  "\<lbrakk>adm P; \<And>t. P (lower_principal t)\<rbrakk> \<Longrightarrow> P xs"
    1.85 -by (rule lower_pd.principal_induct)
    1.86 -
    1.87 -lemma lower_principal_induct2:
    1.88 -  "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
    1.89 -    \<And>t u. P (lower_principal t) (lower_principal u)\<rbrakk> \<Longrightarrow> P xs ys"
    1.90 -apply (rule_tac x=ys in spec)
    1.91 -apply (rule_tac xs=xs in lower_principal_induct, simp)
    1.92 -apply (rule allI, rename_tac ys)
    1.93 -apply (rule_tac xs=ys in lower_principal_induct, simp)
    1.94 -apply simp
    1.95 -done
    1.96 -
    1.97  
    1.98  subsection {* Monadic unit and plus *}
    1.99  
   1.100 @@ -231,8 +199,7 @@
   1.101  lemma lower_unit_Rep_compact_basis [simp]:
   1.102    "{Rep_compact_basis a}\<flat> = lower_principal (PDUnit a)"
   1.103  unfolding lower_unit_def
   1.104 -by (simp add: compact_basis.basis_fun_principal
   1.105 -    lower_principal_mono PDUnit_lower_mono)
   1.106 +by (simp add: compact_basis.basis_fun_principal PDUnit_lower_mono)
   1.107  
   1.108  lemma lower_plus_principal [simp]:
   1.109    "lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
   1.110 @@ -242,27 +209,27 @@
   1.111  
   1.112  lemma approx_lower_unit [simp]:
   1.113    "approx n\<cdot>{x}\<flat> = {approx n\<cdot>x}\<flat>"
   1.114 -apply (induct x rule: compact_basis_induct, simp)
   1.115 +apply (induct x rule: compact_basis.principal_induct, simp)
   1.116  apply (simp add: approx_Rep_compact_basis)
   1.117  done
   1.118  
   1.119  lemma approx_lower_plus [simp]:
   1.120    "approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)"
   1.121 -by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
   1.122 +by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
   1.123  
   1.124  lemma lower_plus_assoc: "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
   1.125 -apply (induct xs ys arbitrary: zs rule: lower_principal_induct2, simp, simp)
   1.126 -apply (rule_tac xs=zs in lower_principal_induct, simp)
   1.127 +apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
   1.128 +apply (rule_tac x=zs in lower_pd.principal_induct, simp)
   1.129  apply (simp add: PDPlus_assoc)
   1.130  done
   1.131  
   1.132  lemma lower_plus_commute: "xs +\<flat> ys = ys +\<flat> xs"
   1.133 -apply (induct xs ys rule: lower_principal_induct2, simp, simp)
   1.134 +apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
   1.135  apply (simp add: PDPlus_commute)
   1.136  done
   1.137  
   1.138  lemma lower_plus_absorb: "xs +\<flat> xs = xs"
   1.139 -apply (induct xs rule: lower_principal_induct, simp)
   1.140 +apply (induct xs rule: lower_pd.principal_induct, simp)
   1.141  apply (simp add: PDPlus_absorb)
   1.142  done
   1.143  
   1.144 @@ -279,7 +246,7 @@
   1.145  lemmas lower_plus_aci = aci_lower_plus.mult_ac_idem
   1.146  
   1.147  lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
   1.148 -apply (induct xs ys rule: lower_principal_induct2, simp, simp)
   1.149 +apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
   1.150  apply (simp add: PDPlus_lower_less)
   1.151  done
   1.152  
   1.153 @@ -306,9 +273,9 @@
   1.154      "adm (\<lambda>f. f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>zs)")
   1.155     apply (drule admD, rule chain_approx)
   1.156      apply (drule_tac f="approx i" in monofun_cfun_arg)
   1.157 -    apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   1.158 -    apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_lower_principal, simp)
   1.159 -    apply (cut_tac xs="approx i\<cdot>zs" in compact_imp_lower_principal, simp)
   1.160 +    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   1.161 +    apply (cut_tac x="approx i\<cdot>ys" in lower_pd.compact_imp_principal, simp)
   1.162 +    apply (cut_tac x="approx i\<cdot>zs" in lower_pd.compact_imp_principal, simp)
   1.163      apply (clarify, simp add: lower_le_PDUnit_PDPlus_iff)
   1.164     apply simp
   1.165    apply simp
   1.166 @@ -321,9 +288,9 @@
   1.167   apply (rule iffI)
   1.168    apply (rule bifinite_less_ext)
   1.169    apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   1.170 -  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   1.171 -  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   1.172 -  apply (clarify, simp add: compact_le_def)
   1.173 +  apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   1.174 +  apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
   1.175 +  apply clarsimp
   1.176   apply (erule monofun_cfun_arg)
   1.177  done
   1.178  
   1.179 @@ -332,8 +299,14 @@
   1.180    lower_plus_less_iff
   1.181    lower_unit_less_plus_iff
   1.182  
   1.183 +lemma fooble:
   1.184 +  fixes f :: "'a::po \<Rightarrow> 'b::po"
   1.185 +  assumes f: "\<And>x y. f x \<sqsubseteq> f y \<longleftrightarrow> x \<sqsubseteq> y"
   1.186 +  shows "f x = f y \<longleftrightarrow> x = y"
   1.187 +unfolding po_eq_conv by (simp add: f)
   1.188 +
   1.189  lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
   1.190 -unfolding po_eq_conv by simp
   1.191 +by (rule lower_unit_less_iff [THEN fooble])
   1.192  
   1.193  lemma lower_unit_strict [simp]: "{\<bottom>}\<flat> = \<bottom>"
   1.194  unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
   1.195 @@ -364,9 +337,7 @@
   1.196  
   1.197  lemma compact_lower_plus [simp]:
   1.198    "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"
   1.199 -apply (drule compact_imp_lower_principal)+
   1.200 -apply (auto simp add: compact_lower_principal)
   1.201 -done
   1.202 +by (auto dest!: lower_pd.compact_imp_principal)
   1.203  
   1.204  
   1.205  subsection {* Induction rules *}
   1.206 @@ -377,8 +348,8 @@
   1.207    assumes insert:
   1.208      "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> +\<flat> ys)"
   1.209    shows "P (xs::'a lower_pd)"
   1.210 -apply (induct xs rule: lower_principal_induct, rule P)
   1.211 -apply (induct_tac t rule: pd_basis_induct1)
   1.212 +apply (induct xs rule: lower_pd.principal_induct, rule P)
   1.213 +apply (induct_tac a rule: pd_basis_induct1)
   1.214  apply (simp only: lower_unit_Rep_compact_basis [symmetric])
   1.215  apply (rule unit)
   1.216  apply (simp only: lower_unit_Rep_compact_basis [symmetric]
   1.217 @@ -391,8 +362,8 @@
   1.218    assumes unit: "\<And>x. P {x}\<flat>"
   1.219    assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<flat> ys)"
   1.220    shows "P (xs::'a lower_pd)"
   1.221 -apply (induct xs rule: lower_principal_induct, rule P)
   1.222 -apply (induct_tac t rule: pd_basis_induct)
   1.223 +apply (induct xs rule: lower_pd.principal_induct, rule P)
   1.224 +apply (induct_tac a rule: pd_basis_induct)
   1.225  apply (simp only: lower_unit_Rep_compact_basis [symmetric] unit)
   1.226  apply (simp only: lower_plus_principal [symmetric] plus)
   1.227  done
   1.228 @@ -430,7 +401,7 @@
   1.229    "t \<le>\<flat> u \<Longrightarrow> lower_bind_basis t \<sqsubseteq> lower_bind_basis u"
   1.230  unfolding expand_cfun_less
   1.231  apply (erule lower_le_induct, safe)
   1.232 -apply (simp add: compact_le_def monofun_cfun)
   1.233 +apply (simp add: monofun_cfun)
   1.234  apply (simp add: rev_trans_less [OF lower_plus_less1])
   1.235  apply (simp add: lower_plus_less_iff)
   1.236  done
   1.237 @@ -448,11 +419,11 @@
   1.238  
   1.239  lemma lower_bind_unit [simp]:
   1.240    "lower_bind\<cdot>{x}\<flat>\<cdot>f = f\<cdot>x"
   1.241 -by (induct x rule: compact_basis_induct, simp, simp)
   1.242 +by (induct x rule: compact_basis.principal_induct, simp, simp)
   1.243  
   1.244  lemma lower_bind_plus [simp]:
   1.245    "lower_bind\<cdot>(xs +\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f +\<flat> lower_bind\<cdot>ys\<cdot>f"
   1.246 -by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
   1.247 +by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
   1.248  
   1.249  lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   1.250  unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit)