src/HOL/HOLCF/Pcpo.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62175 8ffc4d0e652d
child 67312 0d25e02759b7
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 (*  Title:      HOL/HOLCF/Pcpo.thy
     2     Author:     Franz Regensburger
     3 *)
     4 
     5 section \<open>Classes cpo and pcpo\<close>
     6 
     7 theory Pcpo
     8 imports Porder
     9 begin
    10 
    11 subsection \<open>Complete partial orders\<close>
    12 
    13 text \<open>The class cpo of chain complete partial orders\<close>
    14 
    15 class cpo = po +
    16   assumes cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x"
    17 begin
    18 
    19 text \<open>in cpo's everthing equal to THE lub has lub properties for every chain\<close>
    20 
    21 lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
    22   by (fast dest: cpo elim: is_lub_lub)
    23 
    24 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l"
    25   by (blast dest: cpo intro: is_lub_lub)
    26 
    27 text \<open>Properties of the lub\<close>
    28 
    29 lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
    30   by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1])
    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: is_lub_lub [THEN is_lubD2])
    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!: lub_eqI 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 \<open>the \<open>\<sqsubseteq>\<close> relation between two chains is preserved by their lubs\<close>
    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 \<open>the = relation between two chains is preserved by their lubs\<close>
    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 max.cobounded1])
   122     apply (rule chain_mono [OF 2 max.cobounded2])
   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 \<open>Pointed cpos\<close>
   139 
   140 text \<open>The class pcpo of pointed cpos\<close>
   141 
   142 class pcpo = cpo +
   143   assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
   144 begin
   145 
   146 definition bottom :: "'a"  ("\<bottom>")
   147   where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)"
   148 
   149 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
   150 unfolding bottom_def
   151 apply (rule the1I2)
   152 apply (rule ex_ex1I)
   153 apply (rule least)
   154 apply (blast intro: below_antisym)
   155 apply simp
   156 done
   157 
   158 end
   159 
   160 text \<open>Old "UU" syntax:\<close>
   161 
   162 syntax UU :: logic
   163 
   164 translations "UU" => "CONST bottom"
   165 
   166 text \<open>Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}.\<close>
   167 
   168 setup \<open>
   169   Reorient_Proc.add
   170     (fn Const(@{const_name bottom}, _) => true | _ => false)
   171 \<close>
   172 
   173 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
   174 
   175 text \<open>useful lemmas about @{term \<bottom>}\<close>
   176 
   177 lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
   178 by (simp add: po_eq_conv)
   179 
   180 lemma eq_bottom_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
   181 by simp
   182 
   183 lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
   184 by (subst eq_bottom_iff)
   185 
   186 lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)"
   187 by (simp only: eq_bottom_iff lub_below_iff)
   188 
   189 subsection \<open>Chain-finite and flat cpos\<close>
   190 
   191 text \<open>further useful classes for HOLCF domains\<close>
   192 
   193 class chfin = po +
   194   assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
   195 begin
   196 
   197 subclass cpo
   198 apply standard
   199 apply (frule chfin)
   200 apply (blast intro: lub_finch1)
   201 done
   202 
   203 lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y"
   204   by (simp add: chfin finite_chain_def)
   205 
   206 end
   207 
   208 class flat = pcpo +
   209   assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
   210 begin
   211 
   212 subclass chfin
   213 apply standard
   214 apply (unfold max_in_chain_def)
   215 apply (case_tac "\<forall>i. Y i = \<bottom>")
   216 apply simp
   217 apply simp
   218 apply (erule exE)
   219 apply (rule_tac x="i" in exI)
   220 apply clarify
   221 apply (blast dest: chain_mono ax_flat)
   222 done
   223 
   224 lemma flat_below_iff:
   225   shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
   226   by (safe dest!: ax_flat)
   227 
   228 lemma flat_eq: "a \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
   229   by (safe dest!: ax_flat)
   230 
   231 end
   232 
   233 subsection \<open>Discrete cpos\<close>
   234 
   235 class discrete_cpo = below +
   236   assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
   237 begin
   238 
   239 subclass po
   240 proof qed simp_all
   241 
   242 text \<open>In a discrete cpo, every chain is constant\<close>
   243 
   244 lemma discrete_chain_const:
   245   assumes S: "chain S"
   246   shows "\<exists>x. S = (\<lambda>i. x)"
   247 proof (intro exI ext)
   248   fix i :: nat
   249   have "S 0 \<sqsubseteq> S i" using S le0 by (rule chain_mono)
   250   hence "S 0 = S i" by simp
   251   thus "S i = S 0" by (rule sym)
   252 qed
   253 
   254 subclass chfin
   255 proof
   256   fix S :: "nat \<Rightarrow> 'a"
   257   assume S: "chain S"
   258   hence "\<exists>x. S = (\<lambda>i. x)" by (rule discrete_chain_const)
   259   hence "max_in_chain 0 S"
   260     unfolding max_in_chain_def by auto
   261   thus "\<exists>i. max_in_chain i S" ..
   262 qed
   263 
   264 end
   265 
   266 end