src/HOL/HOLCF/Deflation.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 65380 ae93953746fc
child 67312 0d25e02759b7
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/HOLCF/Deflation.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section \<open>Continuous deflations and ep-pairs\<close>
     6 
     7 theory Deflation
     8 imports Cfun
     9 begin
    10 
    11 default_sort cpo
    12 
    13 subsection \<open>Continuous deflations\<close>
    14 
    15 locale deflation =
    16   fixes d :: "'a \<rightarrow> 'a"
    17   assumes idem: "\<And>x. d\<cdot>(d\<cdot>x) = d\<cdot>x"
    18   assumes below: "\<And>x. d\<cdot>x \<sqsubseteq> x"
    19 begin
    20 
    21 lemma below_ID: "d \<sqsubseteq> ID"
    22 by (rule cfun_belowI, simp add: below)
    23 
    24 text \<open>The set of fixed points is the same as the range.\<close>
    25 
    26 lemma fixes_eq_range: "{x. d\<cdot>x = x} = range (\<lambda>x. d\<cdot>x)"
    27 by (auto simp add: eq_sym_conv idem)
    28 
    29 lemma range_eq_fixes: "range (\<lambda>x. d\<cdot>x) = {x. d\<cdot>x = x}"
    30 by (auto simp add: eq_sym_conv idem)
    31 
    32 text \<open>
    33   The pointwise ordering on deflation functions coincides with
    34   the subset ordering of their sets of fixed-points.
    35 \<close>
    36 
    37 lemma belowI:
    38   assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
    39 proof (rule cfun_belowI)
    40   fix x
    41   from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
    42   also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
    43   finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" .
    44 qed
    45 
    46 lemma belowD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
    47 proof (rule below_antisym)
    48   from below show "d\<cdot>x \<sqsubseteq> x" .
    49 next
    50   assume "f \<sqsubseteq> d"
    51   hence "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
    52   also assume "f\<cdot>x = x"
    53   finally show "x \<sqsubseteq> d\<cdot>x" .
    54 qed
    55 
    56 end
    57 
    58 lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
    59 by (rule deflation.below [THEN bottomI])
    60 
    61 lemma adm_deflation: "adm (\<lambda>d. deflation d)"
    62 by (simp add: deflation_def)
    63 
    64 lemma deflation_ID: "deflation ID"
    65 by (simp add: deflation.intro)
    66 
    67 lemma deflation_bottom: "deflation \<bottom>"
    68 by (simp add: deflation.intro)
    69 
    70 lemma deflation_below_iff:
    71   "\<lbrakk>deflation p; deflation q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
    72  apply safe
    73   apply (simp add: deflation.belowD)
    74  apply (simp add: deflation.belowI)
    75 done
    76 
    77 text \<open>
    78   The composition of two deflations is equal to
    79   the lesser of the two (if they are comparable).
    80 \<close>
    81 
    82 lemma deflation_below_comp1:
    83   assumes "deflation f"
    84   assumes "deflation g"
    85   shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
    86 proof (rule below_antisym)
    87   interpret g: deflation g by fact
    88   from g.below show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
    89 next
    90   interpret f: deflation f by fact
    91   assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
    92   hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
    93   also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
    94   finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" .
    95 qed
    96 
    97 lemma deflation_below_comp2:
    98   "\<lbrakk>deflation f; deflation g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
    99 by (simp only: deflation.belowD deflation.idem)
   100 
   101 
   102 subsection \<open>Deflations with finite range\<close>
   103 
   104 lemma finite_range_imp_finite_fixes:
   105   "finite (range f) \<Longrightarrow> finite {x. f x = x}"
   106 proof -
   107   have "{x. f x = x} \<subseteq> range f"
   108     by (clarify, erule subst, rule rangeI)
   109   moreover assume "finite (range f)"
   110   ultimately show "finite {x. f x = x}"
   111     by (rule finite_subset)
   112 qed
   113 
   114 locale finite_deflation = deflation +
   115   assumes finite_fixes: "finite {x. d\<cdot>x = x}"
   116 begin
   117 
   118 lemma finite_range: "finite (range (\<lambda>x. d\<cdot>x))"
   119 by (simp add: range_eq_fixes finite_fixes)
   120 
   121 lemma finite_image: "finite ((\<lambda>x. d\<cdot>x) ` A)"
   122 by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])
   123 
   124 lemma compact: "compact (d\<cdot>x)"
   125 proof (rule compactI2)
   126   fix Y :: "nat \<Rightarrow> 'a"
   127   assume Y: "chain Y"
   128   have "finite_chain (\<lambda>i. d\<cdot>(Y i))"
   129   proof (rule finite_range_imp_finch)
   130     show "chain (\<lambda>i. d\<cdot>(Y i))"
   131       using Y by simp
   132     have "range (\<lambda>i. d\<cdot>(Y i)) \<subseteq> range (\<lambda>x. d\<cdot>x)"
   133       by clarsimp
   134     thus "finite (range (\<lambda>i. d\<cdot>(Y i)))"
   135       using finite_range by (rule finite_subset)
   136   qed
   137   hence "\<exists>j. (\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)"
   138     by (simp add: finite_chain_def maxinch_is_thelub Y)
   139   then obtain j where j: "(\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)" ..
   140 
   141   assume "d\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
   142   hence "d\<cdot>(d\<cdot>x) \<sqsubseteq> d\<cdot>(\<Squnion>i. Y i)"
   143     by (rule monofun_cfun_arg)
   144   hence "d\<cdot>x \<sqsubseteq> (\<Squnion>i. d\<cdot>(Y i))"
   145     by (simp add: contlub_cfun_arg Y idem)
   146   hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)"
   147     using j by simp
   148   hence "d\<cdot>x \<sqsubseteq> Y j"
   149     using below by (rule below_trans)
   150   thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
   151 qed
   152 
   153 end
   154 
   155 lemma finite_deflation_intro:
   156   "deflation d \<Longrightarrow> finite {x. d\<cdot>x = x} \<Longrightarrow> finite_deflation d"
   157 by (intro finite_deflation.intro finite_deflation_axioms.intro)
   158 
   159 lemma finite_deflation_imp_deflation:
   160   "finite_deflation d \<Longrightarrow> deflation d"
   161 unfolding finite_deflation_def by simp
   162 
   163 lemma finite_deflation_bottom: "finite_deflation \<bottom>"
   164 by standard simp_all
   165 
   166 
   167 subsection \<open>Continuous embedding-projection pairs\<close>
   168 
   169 locale ep_pair =
   170   fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a"
   171   assumes e_inverse [simp]: "\<And>x. p\<cdot>(e\<cdot>x) = x"
   172   and e_p_below: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
   173 begin
   174 
   175 lemma e_below_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
   176 proof
   177   assume "e\<cdot>x \<sqsubseteq> e\<cdot>y"
   178   hence "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
   179   thus "x \<sqsubseteq> y" by simp
   180 next
   181   assume "x \<sqsubseteq> y"
   182   thus "e\<cdot>x \<sqsubseteq> e\<cdot>y" by (rule monofun_cfun_arg)
   183 qed
   184 
   185 lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y"
   186 unfolding po_eq_conv e_below_iff ..
   187 
   188 lemma p_eq_iff:
   189   "\<lbrakk>e\<cdot>(p\<cdot>x) = x; e\<cdot>(p\<cdot>y) = y\<rbrakk> \<Longrightarrow> p\<cdot>x = p\<cdot>y \<longleftrightarrow> x = y"
   190 by (safe, erule subst, erule subst, simp)
   191 
   192 lemma p_inverse: "(\<exists>x. y = e\<cdot>x) = (e\<cdot>(p\<cdot>y) = y)"
   193 by (auto, rule exI, erule sym)
   194 
   195 lemma e_below_iff_below_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
   196 proof
   197   assume "e\<cdot>x \<sqsubseteq> y"
   198   then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>y" by (rule monofun_cfun_arg)
   199   then show "x \<sqsubseteq> p\<cdot>y" by simp
   200 next
   201   assume "x \<sqsubseteq> p\<cdot>y"
   202   then have "e\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>y)" by (rule monofun_cfun_arg)
   203   then show "e\<cdot>x \<sqsubseteq> y" using e_p_below by (rule below_trans)
   204 qed
   205 
   206 lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
   207 proof -
   208   assume "compact (e\<cdot>x)"
   209   hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (rule compactD)
   210   hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
   211   hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by simp
   212   thus "compact x" by (rule compactI)
   213 qed
   214 
   215 lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
   216 proof -
   217   assume "compact x"
   218   hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by (rule compactD)
   219   hence "adm (\<lambda>y. x \<notsqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
   220   hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (simp add: e_below_iff_below_p)
   221   thus "compact (e\<cdot>x)" by (rule compactI)
   222 qed
   223 
   224 lemma compact_e_iff: "compact (e\<cdot>x) \<longleftrightarrow> compact x"
   225 by (rule iffI [OF compact_e_rev compact_e])
   226 
   227 text \<open>Deflations from ep-pairs\<close>
   228 
   229 lemma deflation_e_p: "deflation (e oo p)"
   230 by (simp add: deflation.intro e_p_below)
   231 
   232 lemma deflation_e_d_p:
   233   assumes "deflation d"
   234   shows "deflation (e oo d oo p)"
   235 proof
   236   interpret deflation d by fact
   237   fix x :: 'b
   238   show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
   239     by (simp add: idem)
   240   show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
   241     by (simp add: e_below_iff_below_p below)
   242 qed
   243 
   244 lemma finite_deflation_e_d_p:
   245   assumes "finite_deflation d"
   246   shows "finite_deflation (e oo d oo p)"
   247 proof
   248   interpret finite_deflation d by fact
   249   fix x :: 'b
   250   show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
   251     by (simp add: idem)
   252   show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
   253     by (simp add: e_below_iff_below_p below)
   254   have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))"
   255     by (simp add: finite_image)
   256   hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
   257     by (simp add: image_image)
   258   thus "finite {x. (e oo d oo p)\<cdot>x = x}"
   259     by (rule finite_range_imp_finite_fixes)
   260 qed
   261 
   262 lemma deflation_p_d_e:
   263   assumes "deflation d"
   264   assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
   265   shows "deflation (p oo d oo e)"
   266 proof -
   267   interpret d: deflation d by fact
   268   {
   269     fix x
   270     have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
   271       by (rule d.below)
   272     hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)"
   273       by (rule monofun_cfun_arg)
   274     hence "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
   275       by simp
   276   }
   277   note p_d_e_below = this
   278   show ?thesis
   279   proof
   280     fix x
   281     show "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
   282       by (rule p_d_e_below)
   283   next
   284     fix x
   285     show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x"
   286     proof (rule below_antisym)
   287       show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) \<sqsubseteq> (p oo d oo e)\<cdot>x"
   288         by (rule p_d_e_below)
   289       have "p\<cdot>(d\<cdot>(d\<cdot>(d\<cdot>(e\<cdot>x)))) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
   290         by (intro monofun_cfun_arg d)
   291       hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
   292         by (simp only: d.idem)
   293       thus "(p oo d oo e)\<cdot>x \<sqsubseteq> (p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x)"
   294         by simp
   295     qed
   296   qed
   297 qed
   298 
   299 lemma finite_deflation_p_d_e:
   300   assumes "finite_deflation d"
   301   assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
   302   shows "finite_deflation (p oo d oo e)"
   303 proof -
   304   interpret d: finite_deflation d by fact
   305   show ?thesis
   306   proof (rule finite_deflation_intro)
   307     have "deflation d" ..
   308     thus "deflation (p oo d oo e)"
   309       using d by (rule deflation_p_d_e)
   310   next
   311     have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
   312       by (rule d.finite_image)
   313     hence "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
   314       by (rule finite_imageI)
   315     hence "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
   316       by (simp add: image_image)
   317     thus "finite {x. (p oo d oo e)\<cdot>x = x}"
   318       by (rule finite_range_imp_finite_fixes)
   319   qed
   320 qed
   321 
   322 end
   323 
   324 subsection \<open>Uniqueness of ep-pairs\<close>
   325 
   326 lemma ep_pair_unique_e_lemma:
   327   assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
   328   shows "e1 \<sqsubseteq> e2"
   329 proof (rule cfun_belowI)
   330   fix x
   331   have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
   332     by (rule ep_pair.e_p_below [OF 1])
   333   thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
   334     by (simp only: ep_pair.e_inverse [OF 2])
   335 qed
   336 
   337 lemma ep_pair_unique_e:
   338   "\<lbrakk>ep_pair e1 p; ep_pair e2 p\<rbrakk> \<Longrightarrow> e1 = e2"
   339 by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
   340 
   341 lemma ep_pair_unique_p_lemma:
   342   assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
   343   shows "p1 \<sqsubseteq> p2"
   344 proof (rule cfun_belowI)
   345   fix x
   346   have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
   347     by (rule ep_pair.e_p_below [OF 1])
   348   hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
   349     by (rule monofun_cfun_arg)
   350   thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
   351     by (simp only: ep_pair.e_inverse [OF 2])
   352 qed
   353 
   354 lemma ep_pair_unique_p:
   355   "\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
   356 by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
   357 
   358 subsection \<open>Composing ep-pairs\<close>
   359 
   360 lemma ep_pair_ID_ID: "ep_pair ID ID"
   361 by standard simp_all
   362 
   363 lemma ep_pair_comp:
   364   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   365   shows "ep_pair (e2 oo e1) (p1 oo p2)"
   366 proof
   367   interpret ep1: ep_pair e1 p1 by fact
   368   interpret ep2: ep_pair e2 p2 by fact
   369   fix x y
   370   show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
   371     by simp
   372   have "e1\<cdot>(p1\<cdot>(p2\<cdot>y)) \<sqsubseteq> p2\<cdot>y"
   373     by (rule ep1.e_p_below)
   374   hence "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)"
   375     by (rule monofun_cfun_arg)
   376   also have "e2\<cdot>(p2\<cdot>y) \<sqsubseteq> y"
   377     by (rule ep2.e_p_below)
   378   finally show "(e2 oo e1)\<cdot>((p1 oo p2)\<cdot>y) \<sqsubseteq> y"
   379     by simp
   380 qed
   381 
   382 locale pcpo_ep_pair = ep_pair e p
   383   for e :: "'a::pcpo \<rightarrow> 'b::pcpo"
   384   and p :: "'b::pcpo \<rightarrow> 'a::pcpo"
   385 begin
   386 
   387 lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
   388 proof -
   389   have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal)
   390   hence "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
   391   also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_below)
   392   finally show "e\<cdot>\<bottom> = \<bottom>" by simp
   393 qed
   394 
   395 lemma e_bottom_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
   396 by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
   397 
   398 lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
   399 by simp
   400 
   401 lemma p_strict [simp]: "p\<cdot>\<bottom> = \<bottom>"
   402 by (rule e_inverse [where x="\<bottom>", unfolded e_strict])
   403 
   404 lemmas stricts = e_strict p_strict
   405 
   406 end
   407 
   408 end