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