src/HOLCF/Domain_Aux.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40327 1dfdbd66093a
child 40503 4094d788b904
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
     1 (*  Title:      HOLCF/Domain_Aux.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Domain package support *}
     6 
     7 theory Domain_Aux
     8 imports Map_Functions Fixrec
     9 uses
    10   ("Tools/Domain/domain_take_proofs.ML")
    11 begin
    12 
    13 subsection {* Continuous isomorphisms *}
    14 
    15 text {* A locale for continuous isomorphisms *}
    16 
    17 locale iso =
    18   fixes abs :: "'a \<rightarrow> 'b"
    19   fixes rep :: "'b \<rightarrow> 'a"
    20   assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x"
    21   assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y"
    22 begin
    23 
    24 lemma swap: "iso rep abs"
    25   by (rule iso.intro [OF rep_iso abs_iso])
    26 
    27 lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
    28 proof
    29   assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y"
    30   then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg)
    31   then show "x \<sqsubseteq> y" by simp
    32 next
    33   assume "x \<sqsubseteq> y"
    34   then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg)
    35 qed
    36 
    37 lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
    38   by (rule iso.abs_below [OF swap])
    39 
    40 lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)"
    41   by (simp add: po_eq_conv abs_below)
    42 
    43 lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)"
    44   by (rule iso.abs_eq [OF swap])
    45 
    46 lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>"
    47 proof -
    48   have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
    49   then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
    50   then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
    51   then show ?thesis by (rule UU_I)
    52 qed
    53 
    54 lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"
    55   by (rule iso.abs_strict [OF swap])
    56 
    57 lemma abs_defin': "abs\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>"
    58 proof -
    59   have "x = rep\<cdot>(abs\<cdot>x)" by simp
    60   also assume "abs\<cdot>x = \<bottom>"
    61   also note rep_strict
    62   finally show "x = \<bottom>" .
    63 qed
    64 
    65 lemma rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"
    66   by (rule iso.abs_defin' [OF swap])
    67 
    68 lemma abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>"
    69   by (erule contrapos_nn, erule abs_defin')
    70 
    71 lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
    72   by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)
    73 
    74 lemma abs_bottom_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
    75   by (auto elim: abs_defin' intro: abs_strict)
    76 
    77 lemma rep_bottom_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
    78   by (rule iso.abs_bottom_iff [OF iso.swap]) (rule iso_axioms)
    79 
    80 lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P"
    81   by (simp add: rep_bottom_iff)
    82 
    83 lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
    84 proof (unfold compact_def)
    85   assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
    86   with cont_Rep_cfun2
    87   have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
    88   then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
    89 qed
    90 
    91 lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
    92   by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms)
    93 
    94 lemma compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)"
    95   by (rule compact_rep_rev) simp
    96 
    97 lemma compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)"
    98   by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms)
    99 
   100 lemma iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)"
   101 proof
   102   assume "x = abs\<cdot>y"
   103   then have "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp
   104   then show "rep\<cdot>x = y" by simp
   105 next
   106   assume "rep\<cdot>x = y"
   107   then have "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp
   108   then show "x = abs\<cdot>y" by simp
   109 qed
   110 
   111 end
   112 
   113 
   114 subsection {* Proofs about take functions *}
   115 
   116 text {*
   117   This section contains lemmas that are used in a module that supports
   118   the domain isomorphism package; the module contains proofs related
   119   to take functions and the finiteness predicate.
   120 *}
   121 
   122 lemma deflation_abs_rep:
   123   fixes abs and rep and d
   124   assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
   125   assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
   126   shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
   127 by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
   128 
   129 lemma deflation_chain_min:
   130   assumes chain: "chain d"
   131   assumes defl: "\<And>n. deflation (d n)"
   132   shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
   133 proof (rule linorder_le_cases)
   134   assume "m \<le> n"
   135   with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
   136   then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
   137     by (rule deflation_below_comp1 [OF defl defl])
   138   moreover from `m \<le> n` have "min m n = m" by simp
   139   ultimately show ?thesis by simp
   140 next
   141   assume "n \<le> m"
   142   with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
   143   then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
   144     by (rule deflation_below_comp2 [OF defl defl])
   145   moreover from `n \<le> m` have "min m n = n" by simp
   146   ultimately show ?thesis by simp
   147 qed
   148 
   149 lemma lub_ID_take_lemma:
   150   assumes "chain t" and "(\<Squnion>n. t n) = ID"
   151   assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y"
   152 proof -
   153   have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)"
   154     using assms(3) by simp
   155   then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y"
   156     using assms(1) by (simp add: lub_distribs)
   157   then show "x = y"
   158     using assms(2) by simp
   159 qed
   160 
   161 lemma lub_ID_reach:
   162   assumes "chain t" and "(\<Squnion>n. t n) = ID"
   163   shows "(\<Squnion>n. t n\<cdot>x) = x"
   164 using assms by (simp add: lub_distribs)
   165 
   166 lemma lub_ID_take_induct:
   167   assumes "chain t" and "(\<Squnion>n. t n) = ID"
   168   assumes "adm P" and "\<And>n. P (t n\<cdot>x)" shows "P x"
   169 proof -
   170   from `chain t` have "chain (\<lambda>n. t n\<cdot>x)" by simp
   171   from `adm P` this `\<And>n. P (t n\<cdot>x)` have "P (\<Squnion>n. t n\<cdot>x)" by (rule admD)
   172   with `chain t` `(\<Squnion>n. t n) = ID` show "P x" by (simp add: lub_distribs)
   173 qed
   174 
   175 
   176 subsection {* Finiteness *}
   177 
   178 text {*
   179   Let a ``decisive'' function be a deflation that maps every input to
   180   either itself or bottom.  Then if a domain's take functions are all
   181   decisive, then all values in the domain are finite.
   182 *}
   183 
   184 definition
   185   decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool"
   186 where
   187   "decisive d \<longleftrightarrow> (\<forall>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>)"
   188 
   189 lemma decisiveI: "(\<And>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>) \<Longrightarrow> decisive d"
   190   unfolding decisive_def by simp
   191 
   192 lemma decisive_cases:
   193   assumes "decisive d" obtains "d\<cdot>x = x" | "d\<cdot>x = \<bottom>"
   194 using assms unfolding decisive_def by auto
   195 
   196 lemma decisive_bottom: "decisive \<bottom>"
   197   unfolding decisive_def by simp
   198 
   199 lemma decisive_ID: "decisive ID"
   200   unfolding decisive_def by simp
   201 
   202 lemma decisive_ssum_map:
   203   assumes f: "decisive f"
   204   assumes g: "decisive g"
   205   shows "decisive (ssum_map\<cdot>f\<cdot>g)"
   206 apply (rule decisiveI, rename_tac s)
   207 apply (case_tac s, simp_all)
   208 apply (rule_tac x=x in decisive_cases [OF f], simp_all)
   209 apply (rule_tac x=y in decisive_cases [OF g], simp_all)
   210 done
   211 
   212 lemma decisive_sprod_map:
   213   assumes f: "decisive f"
   214   assumes g: "decisive g"
   215   shows "decisive (sprod_map\<cdot>f\<cdot>g)"
   216 apply (rule decisiveI, rename_tac s)
   217 apply (case_tac s, simp_all)
   218 apply (rule_tac x=x in decisive_cases [OF f], simp_all)
   219 apply (rule_tac x=y in decisive_cases [OF g], simp_all)
   220 done
   221 
   222 lemma decisive_abs_rep:
   223   fixes abs rep
   224   assumes iso: "iso abs rep"
   225   assumes d: "decisive d"
   226   shows "decisive (abs oo d oo rep)"
   227 apply (rule decisiveI)
   228 apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
   229 apply (simp add: iso.rep_iso [OF iso])
   230 apply (simp add: iso.abs_strict [OF iso])
   231 done
   232 
   233 lemma lub_ID_finite:
   234   assumes chain: "chain d"
   235   assumes lub: "(\<Squnion>n. d n) = ID"
   236   assumes decisive: "\<And>n. decisive (d n)"
   237   shows "\<exists>n. d n\<cdot>x = x"
   238 proof -
   239   have 1: "chain (\<lambda>n. d n\<cdot>x)" using chain by simp
   240   have 2: "(\<Squnion>n. d n\<cdot>x) = x" using chain lub by (rule lub_ID_reach)
   241   have "\<forall>n. d n\<cdot>x = x \<or> d n\<cdot>x = \<bottom>"
   242     using decisive unfolding decisive_def by simp
   243   hence "range (\<lambda>n. d n\<cdot>x) \<subseteq> {x, \<bottom>}"
   244     by auto
   245   hence "finite (range (\<lambda>n. d n\<cdot>x))"
   246     by (rule finite_subset, simp)
   247   with 1 have "finite_chain (\<lambda>n. d n\<cdot>x)"
   248     by (rule finite_range_imp_finch)
   249   then have "\<exists>n. (\<Squnion>n. d n\<cdot>x) = d n\<cdot>x"
   250     unfolding finite_chain_def by (auto simp add: maxinch_is_thelub)
   251   with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym)
   252 qed
   253 
   254 lemma lub_ID_finite_take_induct:
   255   assumes "chain d" and "(\<Squnion>n. d n) = ID" and "\<And>n. decisive (d n)"
   256   shows "(\<And>n. P (d n\<cdot>x)) \<Longrightarrow> P x"
   257 using lub_ID_finite [OF assms] by metis
   258 
   259 subsection {* ML setup *}
   260 
   261 use "Tools/Domain/domain_take_proofs.ML"
   262 
   263 setup Domain_Take_Proofs.setup
   264 
   265 end