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