src/HOLCF/Pcpo.thy
author haftmann
Fri Jun 19 21:08:07 2009 +0200 (2009-06-19)
changeset 31726 ffd2dc631d88
parent 31076 99fe356cbbc2
child 33523 96730ad673be
permissions -rw-r--r--
merged
     1 (*  Title:      HOLCF/Pcpo.thy
     2     Author:     Franz Regensburger
     3 *)
     4 
     5 header {* Classes cpo and pcpo *}
     6 
     7 theory Pcpo
     8 imports Porder
     9 begin
    10 
    11 subsection {* Complete partial orders *}
    12 
    13 text {* The class cpo of chain complete partial orders *}
    14 
    15 class cpo = po +
    16   assumes cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x"
    17 begin
    18 
    19 text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
    20 
    21 lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
    22   by (fast dest: cpo elim: lubI)
    23 
    24 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l"
    25   by (blast dest: cpo intro: lubI)
    26 
    27 text {* Properties of the lub *}
    28 
    29 lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
    30   by (blast dest: cpo intro: lubI [THEN is_ub_lub])
    31 
    32 lemma is_lub_thelub:
    33   "\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
    34   by (blast dest: cpo intro: lubI [THEN is_lub_lub])
    35 
    36 lemma lub_range_mono:
    37   "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk>
    38     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
    39 apply (erule is_lub_thelub)
    40 apply (rule ub_rangeI)
    41 apply (subgoal_tac "\<exists>j. X i = Y j")
    42 apply  clarsimp
    43 apply  (erule is_ub_thelub)
    44 apply auto
    45 done
    46 
    47 lemma lub_range_shift:
    48   "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)"
    49 apply (rule below_antisym)
    50 apply (rule lub_range_mono)
    51 apply    fast
    52 apply   assumption
    53 apply (erule chain_shift)
    54 apply (rule is_lub_thelub)
    55 apply assumption
    56 apply (rule ub_rangeI)
    57 apply (rule_tac y="Y (i + j)" in below_trans)
    58 apply (erule chain_mono)
    59 apply (rule le_add1)
    60 apply (rule is_ub_thelub)
    61 apply (erule chain_shift)
    62 done
    63 
    64 lemma maxinch_is_thelub:
    65   "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)"
    66 apply (rule iffI)
    67 apply (fast intro!: thelubI lub_finch1)
    68 apply (unfold max_in_chain_def)
    69 apply (safe intro!: below_antisym)
    70 apply (fast elim!: chain_mono)
    71 apply (drule sym)
    72 apply (force elim!: is_ub_thelub)
    73 done
    74 
    75 text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *}
    76 
    77 lemma lub_mono:
    78   "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> 
    79     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
    80 apply (erule is_lub_thelub)
    81 apply (rule ub_rangeI)
    82 apply (rule below_trans)
    83 apply (erule meta_spec)
    84 apply (erule is_ub_thelub)
    85 done
    86 
    87 text {* the = relation between two chains is preserved by their lubs *}
    88 
    89 lemma lub_equal:
    90   "\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk>
    91     \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
    92   by (simp only: expand_fun_eq [symmetric])
    93 
    94 text {* more results about mono and = of lubs of chains *}
    95 
    96 lemma lub_mono2:
    97   "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
    98     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
    99 apply (erule exE)
   100 apply (subgoal_tac "(\<Squnion>i. X (i + Suc j)) \<sqsubseteq> (\<Squnion>i. Y (i + Suc j))")
   101 apply (thin_tac "\<forall>i>j. X i = Y i")
   102 apply (simp only: lub_range_shift)
   103 apply simp
   104 done
   105 
   106 lemma lub_equal2:
   107   "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
   108     \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
   109   by (blast intro: below_antisym lub_mono2 sym)
   110 
   111 lemma lub_mono3:
   112   "\<lbrakk>chain Y; chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk>
   113     \<Longrightarrow> (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. X i)"
   114 apply (erule is_lub_thelub)
   115 apply (rule ub_rangeI)
   116 apply (erule allE)
   117 apply (erule exE)
   118 apply (erule below_trans)
   119 apply (erule is_ub_thelub)
   120 done
   121 
   122 lemma ch2ch_lub:
   123   assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
   124   assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
   125   shows "chain (\<lambda>i. \<Squnion>j. Y i j)"
   126 apply (rule chainI)
   127 apply (rule lub_mono [OF 2 2])
   128 apply (rule chainE [OF 1])
   129 done
   130 
   131 lemma diag_lub:
   132   assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
   133   assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
   134   shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)"
   135 proof (rule below_antisym)
   136   have 3: "chain (\<lambda>i. Y i i)"
   137     apply (rule chainI)
   138     apply (rule below_trans)
   139     apply (rule chainE [OF 1])
   140     apply (rule chainE [OF 2])
   141     done
   142   have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)"
   143     by (rule ch2ch_lub [OF 1 2])
   144   show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)"
   145     apply (rule is_lub_thelub [OF 4])
   146     apply (rule ub_rangeI)
   147     apply (rule lub_mono3 [rule_format, OF 2 3])
   148     apply (rule exI)
   149     apply (rule below_trans)
   150     apply (rule chain_mono [OF 1 le_maxI1])
   151     apply (rule chain_mono [OF 2 le_maxI2])
   152     done
   153   show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
   154     apply (rule lub_mono [OF 3 4])
   155     apply (rule is_ub_thelub [OF 2])
   156     done
   157 qed
   158 
   159 lemma ex_lub:
   160   assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
   161   assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
   162   shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>j. \<Squnion>i. Y i j)"
   163   by (simp add: diag_lub 1 2)
   164 
   165 end
   166 
   167 subsection {* Pointed cpos *}
   168 
   169 text {* The class pcpo of pointed cpos *}
   170 
   171 class pcpo = cpo +
   172   assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
   173 begin
   174 
   175 definition UU :: 'a where
   176   "UU = (THE x. \<forall>y. x \<sqsubseteq> y)"
   177 
   178 notation (xsymbols)
   179   UU  ("\<bottom>")
   180 
   181 text {* derive the old rule minimal *}
   182  
   183 lemma UU_least: "\<forall>z. \<bottom> \<sqsubseteq> z"
   184 apply (unfold UU_def)
   185 apply (rule theI')
   186 apply (rule ex_ex1I)
   187 apply (rule least)
   188 apply (blast intro: below_antisym)
   189 done
   190 
   191 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
   192 by (rule UU_least [THEN spec])
   193 
   194 end
   195 
   196 text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
   197 
   198 setup {*
   199   ReorientProc.add
   200     (fn Const(@{const_name UU}, _) => true | _ => false)
   201 *}
   202 
   203 simproc_setup reorient_bottom ("\<bottom> = x") = ReorientProc.proc
   204 
   205 context pcpo
   206 begin
   207 
   208 text {* useful lemmas about @{term \<bottom>} *}
   209 
   210 lemma below_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
   211 by (simp add: po_eq_conv)
   212 
   213 lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
   214 by simp
   215 
   216 lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
   217 by (subst eq_UU_iff)
   218 
   219 lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>"
   220 apply (rule allI)
   221 apply (rule UU_I)
   222 apply (erule subst)
   223 apply (erule is_ub_thelub)
   224 done
   225 
   226 lemma chain_UU_I_inverse: "\<forall>i::nat. Y i = \<bottom> \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom>"
   227 apply (rule lub_chain_maxelem)
   228 apply (erule spec)
   229 apply simp
   230 done
   231 
   232 lemma chain_UU_I_inverse2: "(\<Squnion>i. Y i) \<noteq> \<bottom> \<Longrightarrow> \<exists>i::nat. Y i \<noteq> \<bottom>"
   233   by (blast intro: chain_UU_I_inverse)
   234 
   235 lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>"
   236   by (blast intro: UU_I)
   237 
   238 lemma chain_mono2: "\<lbrakk>\<exists>j. Y j \<noteq> \<bottom>; chain Y\<rbrakk> \<Longrightarrow> \<exists>j. \<forall>i>j. Y i \<noteq> \<bottom>"
   239   by (blast dest: notUU_I chain_mono_less)
   240 
   241 end
   242 
   243 subsection {* Chain-finite and flat cpos *}
   244 
   245 text {* further useful classes for HOLCF domains *}
   246 
   247 class chfin = po +
   248   assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
   249 begin
   250 
   251 subclass cpo
   252 apply default
   253 apply (frule chfin)
   254 apply (blast intro: lub_finch1)
   255 done
   256 
   257 lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y"
   258   by (simp add: chfin finite_chain_def)
   259 
   260 end
   261 
   262 class finite_po = finite + po
   263 begin
   264 
   265 subclass chfin
   266 apply default
   267 apply (drule finite_range_imp_finch)
   268 apply (rule finite)
   269 apply (simp add: finite_chain_def)
   270 done
   271 
   272 end
   273 
   274 class flat = pcpo +
   275   assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
   276 begin
   277 
   278 subclass chfin
   279 apply default
   280 apply (unfold max_in_chain_def)
   281 apply (case_tac "\<forall>i. Y i = \<bottom>")
   282 apply simp
   283 apply simp
   284 apply (erule exE)
   285 apply (rule_tac x="i" in exI)
   286 apply clarify
   287 apply (blast dest: chain_mono ax_flat)
   288 done
   289 
   290 lemma flat_below_iff:
   291   shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
   292   by (safe dest!: ax_flat)
   293 
   294 lemma flat_eq: "a \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
   295   by (safe dest!: ax_flat)
   296 
   297 end
   298 
   299 text {* Discrete cpos *}
   300 
   301 class discrete_cpo = below +
   302   assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
   303 begin
   304 
   305 subclass po
   306 proof qed simp_all
   307 
   308 text {* In a discrete cpo, every chain is constant *}
   309 
   310 lemma discrete_chain_const:
   311   assumes S: "chain S"
   312   shows "\<exists>x. S = (\<lambda>i. x)"
   313 proof (intro exI ext)
   314   fix i :: nat
   315   have "S 0 \<sqsubseteq> S i" using S le0 by (rule chain_mono)
   316   hence "S 0 = S i" by simp
   317   thus "S i = S 0" by (rule sym)
   318 qed
   319 
   320 subclass cpo
   321 proof
   322   fix S :: "nat \<Rightarrow> 'a"
   323   assume S: "chain S"
   324   hence "\<exists>x. S = (\<lambda>i. x)"
   325     by (rule discrete_chain_const)
   326   thus "\<exists>x. range S <<| x"
   327     by (fast intro: lub_const)
   328 qed
   329 
   330 end
   331 
   332 end