src/HOLCF/Pcpo.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40500 ee9c8d36318e
child 40771 1c6f7d4b110e
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
     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_below: "\<lbrakk>chain S; \<And>i. S i \<sqsubseteq> x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
    40   by (simp add: lub_below_iff)
    41 
    42 lemma below_lub: "\<lbrakk>chain S; x \<sqsubseteq> S i\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. S i)"
    43   by (erule below_trans, erule is_ub_thelub)
    44 
    45 lemma lub_range_mono:
    46   "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk>
    47     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
    48 apply (erule lub_below)
    49 apply (subgoal_tac "\<exists>j. X i = Y j")
    50 apply  clarsimp
    51 apply  (erule is_ub_thelub)
    52 apply auto
    53 done
    54 
    55 lemma lub_range_shift:
    56   "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)"
    57 apply (rule below_antisym)
    58 apply (rule lub_range_mono)
    59 apply    fast
    60 apply   assumption
    61 apply (erule chain_shift)
    62 apply (rule lub_below)
    63 apply assumption
    64 apply (rule_tac i="i" in below_lub)
    65 apply (erule chain_shift)
    66 apply (erule chain_mono)
    67 apply (rule le_add1)
    68 done
    69 
    70 lemma maxinch_is_thelub:
    71   "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)"
    72 apply (rule iffI)
    73 apply (fast intro!: thelubI lub_finch1)
    74 apply (unfold max_in_chain_def)
    75 apply (safe intro!: below_antisym)
    76 apply (fast elim!: chain_mono)
    77 apply (drule sym)
    78 apply (force elim!: is_ub_thelub)
    79 done
    80 
    81 text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *}
    82 
    83 lemma lub_mono:
    84   "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> 
    85     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
    86 by (fast elim: lub_below below_lub)
    87 
    88 text {* the = relation between two chains is preserved by their lubs *}
    89 
    90 lemma lub_eq:
    91   "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
    92   by simp
    93 
    94 lemma ch2ch_lub:
    95   assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
    96   assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
    97   shows "chain (\<lambda>i. \<Squnion>j. Y i j)"
    98 apply (rule chainI)
    99 apply (rule lub_mono [OF 2 2])
   100 apply (rule chainE [OF 1])
   101 done
   102 
   103 lemma diag_lub:
   104   assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
   105   assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
   106   shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)"
   107 proof (rule below_antisym)
   108   have 3: "chain (\<lambda>i. Y i i)"
   109     apply (rule chainI)
   110     apply (rule below_trans)
   111     apply (rule chainE [OF 1])
   112     apply (rule chainE [OF 2])
   113     done
   114   have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)"
   115     by (rule ch2ch_lub [OF 1 2])
   116   show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)"
   117     apply (rule lub_below [OF 4])
   118     apply (rule lub_below [OF 2])
   119     apply (rule below_lub [OF 3])
   120     apply (rule below_trans)
   121     apply (rule chain_mono [OF 1 le_maxI1])
   122     apply (rule chain_mono [OF 2 le_maxI2])
   123     done
   124   show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
   125     apply (rule lub_mono [OF 3 4])
   126     apply (rule is_ub_thelub [OF 2])
   127     done
   128 qed
   129 
   130 lemma ex_lub:
   131   assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
   132   assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
   133   shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>j. \<Squnion>i. Y i j)"
   134   by (simp add: diag_lub 1 2)
   135 
   136 end
   137 
   138 subsection {* Pointed cpos *}
   139 
   140 text {* The class pcpo of pointed cpos *}
   141 
   142 class pcpo = cpo +
   143   assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
   144 begin
   145 
   146 definition UU :: 'a where
   147   "UU = (THE x. \<forall>y. x \<sqsubseteq> y)"
   148 
   149 notation (xsymbols)
   150   UU  ("\<bottom>")
   151 
   152 text {* derive the old rule minimal *}
   153  
   154 lemma UU_least: "\<forall>z. \<bottom> \<sqsubseteq> z"
   155 apply (unfold UU_def)
   156 apply (rule theI')
   157 apply (rule ex_ex1I)
   158 apply (rule least)
   159 apply (blast intro: below_antisym)
   160 done
   161 
   162 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
   163 by (rule UU_least [THEN spec])
   164 
   165 end
   166 
   167 text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
   168 
   169 setup {*
   170   Reorient_Proc.add
   171     (fn Const(@{const_name UU}, _) => true | _ => false)
   172 *}
   173 
   174 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
   175 
   176 context pcpo
   177 begin
   178 
   179 text {* useful lemmas about @{term \<bottom>} *}
   180 
   181 lemma below_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
   182 by (simp add: po_eq_conv)
   183 
   184 lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
   185 by simp
   186 
   187 lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
   188 by (subst eq_UU_iff)
   189 
   190 lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)"
   191 by (simp only: eq_UU_iff lub_below_iff)
   192 
   193 lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>"
   194 by (simp add: lub_eq_bottom_iff)
   195 
   196 lemma chain_UU_I_inverse: "\<forall>i::nat. Y i = \<bottom> \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom>"
   197 by simp
   198 
   199 lemma chain_UU_I_inverse2: "(\<Squnion>i. Y i) \<noteq> \<bottom> \<Longrightarrow> \<exists>i::nat. Y i \<noteq> \<bottom>"
   200   by (blast intro: chain_UU_I_inverse)
   201 
   202 lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>"
   203   by (blast intro: UU_I)
   204 
   205 end
   206 
   207 subsection {* Chain-finite and flat cpos *}
   208 
   209 text {* further useful classes for HOLCF domains *}
   210 
   211 class chfin = po +
   212   assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
   213 begin
   214 
   215 subclass cpo
   216 apply default
   217 apply (frule chfin)
   218 apply (blast intro: lub_finch1)
   219 done
   220 
   221 lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y"
   222   by (simp add: chfin finite_chain_def)
   223 
   224 end
   225 
   226 class flat = pcpo +
   227   assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
   228 begin
   229 
   230 subclass chfin
   231 apply default
   232 apply (unfold max_in_chain_def)
   233 apply (case_tac "\<forall>i. Y i = \<bottom>")
   234 apply simp
   235 apply simp
   236 apply (erule exE)
   237 apply (rule_tac x="i" in exI)
   238 apply clarify
   239 apply (blast dest: chain_mono ax_flat)
   240 done
   241 
   242 lemma flat_below_iff:
   243   shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
   244   by (safe dest!: ax_flat)
   245 
   246 lemma flat_eq: "a \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
   247   by (safe dest!: ax_flat)
   248 
   249 end
   250 
   251 subsection {* Discrete cpos *}
   252 
   253 class discrete_cpo = below +
   254   assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
   255 begin
   256 
   257 subclass po
   258 proof qed simp_all
   259 
   260 text {* In a discrete cpo, every chain is constant *}
   261 
   262 lemma discrete_chain_const:
   263   assumes S: "chain S"
   264   shows "\<exists>x. S = (\<lambda>i. x)"
   265 proof (intro exI ext)
   266   fix i :: nat
   267   have "S 0 \<sqsubseteq> S i" using S le0 by (rule chain_mono)
   268   hence "S 0 = S i" by simp
   269   thus "S i = S 0" by (rule sym)
   270 qed
   271 
   272 subclass chfin
   273 proof
   274   fix S :: "nat \<Rightarrow> 'a"
   275   assume S: "chain S"
   276   hence "\<exists>x. S = (\<lambda>i. x)" by (rule discrete_chain_const)
   277   hence "max_in_chain 0 S"
   278     unfolding max_in_chain_def by auto
   279   thus "\<exists>i. max_in_chain i S" ..
   280 qed
   281 
   282 end
   283 
   284 end