src/HOL/HOLCF/Domain_Aux.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62175 8ffc4d0e652d
child 68383 93a42bd62ede
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/HOLCF/Domain_Aux.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section \<open>Domain package support\<close>
     6 
     7 theory Domain_Aux
     8 imports Map_Functions Fixrec
     9 begin
    10 
    11 subsection \<open>Continuous isomorphisms\<close>
    12 
    13 text \<open>A locale for continuous isomorphisms\<close>
    14 
    15 locale iso =
    16   fixes abs :: "'a \<rightarrow> 'b"
    17   fixes rep :: "'b \<rightarrow> 'a"
    18   assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x"
    19   assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y"
    20 begin
    21 
    22 lemma swap: "iso rep abs"
    23   by (rule iso.intro [OF rep_iso abs_iso])
    24 
    25 lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
    26 proof
    27   assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y"
    28   then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg)
    29   then show "x \<sqsubseteq> y" by simp
    30 next
    31   assume "x \<sqsubseteq> y"
    32   then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg)
    33 qed
    34 
    35 lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
    36   by (rule iso.abs_below [OF swap])
    37 
    38 lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)"
    39   by (simp add: po_eq_conv abs_below)
    40 
    41 lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)"
    42   by (rule iso.abs_eq [OF swap])
    43 
    44 lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>"
    45 proof -
    46   have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
    47   then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
    48   then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
    49   then show ?thesis by (rule bottomI)
    50 qed
    51 
    52 lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"
    53   by (rule iso.abs_strict [OF swap])
    54 
    55 lemma abs_defin': "abs\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>"
    56 proof -
    57   have "x = rep\<cdot>(abs\<cdot>x)" by simp
    58   also assume "abs\<cdot>x = \<bottom>"
    59   also note rep_strict
    60   finally show "x = \<bottom>" .
    61 qed
    62 
    63 lemma rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"
    64   by (rule iso.abs_defin' [OF swap])
    65 
    66 lemma abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>"
    67   by (erule contrapos_nn, erule abs_defin')
    68 
    69 lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
    70   by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)
    71 
    72 lemma abs_bottom_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
    73   by (auto elim: abs_defin' intro: abs_strict)
    74 
    75 lemma rep_bottom_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
    76   by (rule iso.abs_bottom_iff [OF iso.swap]) (rule iso_axioms)
    77 
    78 lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P"
    79   by (simp add: rep_bottom_iff)
    80 
    81 lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
    82 proof (unfold compact_def)
    83   assume "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> y)"
    84   with cont_Rep_cfun2
    85   have "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> abs\<cdot>y)" by (rule adm_subst)
    86   then show "adm (\<lambda>y. x \<notsqsubseteq> y)" using abs_below by simp
    87 qed
    88 
    89 lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
    90   by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms)
    91 
    92 lemma compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)"
    93   by (rule compact_rep_rev) simp
    94 
    95 lemma compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)"
    96   by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms)
    97 
    98 lemma iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)"
    99 proof
   100   assume "x = abs\<cdot>y"
   101   then have "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp
   102   then show "rep\<cdot>x = y" by simp
   103 next
   104   assume "rep\<cdot>x = y"
   105   then have "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp
   106   then show "x = abs\<cdot>y" by simp
   107 qed
   108 
   109 end
   110 
   111 subsection \<open>Proofs about take functions\<close>
   112 
   113 text \<open>
   114   This section contains lemmas that are used in a module that supports
   115   the domain isomorphism package; the module contains proofs related
   116   to take functions and the finiteness predicate.
   117 \<close>
   118 
   119 lemma deflation_abs_rep:
   120   fixes abs and rep and d
   121   assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
   122   assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
   123   shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
   124 by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
   125 
   126 lemma deflation_chain_min:
   127   assumes chain: "chain d"
   128   assumes defl: "\<And>n. deflation (d n)"
   129   shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
   130 proof (rule linorder_le_cases)
   131   assume "m \<le> n"
   132   with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
   133   then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
   134     by (rule deflation_below_comp1 [OF defl defl])
   135   moreover from \<open>m \<le> n\<close> have "min m n = m" by simp
   136   ultimately show ?thesis by simp
   137 next
   138   assume "n \<le> m"
   139   with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
   140   then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
   141     by (rule deflation_below_comp2 [OF defl defl])
   142   moreover from \<open>n \<le> m\<close> have "min m n = n" by simp
   143   ultimately show ?thesis by simp
   144 qed
   145 
   146 lemma lub_ID_take_lemma:
   147   assumes "chain t" and "(\<Squnion>n. t n) = ID"
   148   assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y"
   149 proof -
   150   have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)"
   151     using assms(3) by simp
   152   then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y"
   153     using assms(1) by (simp add: lub_distribs)
   154   then show "x = y"
   155     using assms(2) by simp
   156 qed
   157 
   158 lemma lub_ID_reach:
   159   assumes "chain t" and "(\<Squnion>n. t n) = ID"
   160   shows "(\<Squnion>n. t n\<cdot>x) = x"
   161 using assms by (simp add: lub_distribs)
   162 
   163 lemma lub_ID_take_induct:
   164   assumes "chain t" and "(\<Squnion>n. t n) = ID"
   165   assumes "adm P" and "\<And>n. P (t n\<cdot>x)" shows "P x"
   166 proof -
   167   from \<open>chain t\<close> have "chain (\<lambda>n. t n\<cdot>x)" by simp
   168   from \<open>adm P\<close> this \<open>\<And>n. P (t n\<cdot>x)\<close> have "P (\<Squnion>n. t n\<cdot>x)" by (rule admD)
   169   with \<open>chain t\<close> \<open>(\<Squnion>n. t n) = ID\<close> show "P x" by (simp add: lub_distribs)
   170 qed
   171 
   172 subsection \<open>Finiteness\<close>
   173 
   174 text \<open>
   175   Let a ``decisive'' function be a deflation that maps every input to
   176   either itself or bottom.  Then if a domain's take functions are all
   177   decisive, then all values in the domain are finite.
   178 \<close>
   179 
   180 definition
   181   decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool"
   182 where
   183   "decisive d \<longleftrightarrow> (\<forall>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>)"
   184 
   185 lemma decisiveI: "(\<And>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>) \<Longrightarrow> decisive d"
   186   unfolding decisive_def by simp
   187 
   188 lemma decisive_cases:
   189   assumes "decisive d" obtains "d\<cdot>x = x" | "d\<cdot>x = \<bottom>"
   190 using assms unfolding decisive_def by auto
   191 
   192 lemma decisive_bottom: "decisive \<bottom>"
   193   unfolding decisive_def by simp
   194 
   195 lemma decisive_ID: "decisive ID"
   196   unfolding decisive_def by simp
   197 
   198 lemma decisive_ssum_map:
   199   assumes f: "decisive f"
   200   assumes g: "decisive g"
   201   shows "decisive (ssum_map\<cdot>f\<cdot>g)"
   202 apply (rule decisiveI, rename_tac s)
   203 apply (case_tac s, simp_all)
   204 apply (rule_tac x=x in decisive_cases [OF f], simp_all)
   205 apply (rule_tac x=y in decisive_cases [OF g], simp_all)
   206 done
   207 
   208 lemma decisive_sprod_map:
   209   assumes f: "decisive f"
   210   assumes g: "decisive g"
   211   shows "decisive (sprod_map\<cdot>f\<cdot>g)"
   212 apply (rule decisiveI, rename_tac s)
   213 apply (case_tac s, simp_all)
   214 apply (rule_tac x=x in decisive_cases [OF f], simp_all)
   215 apply (rule_tac x=y in decisive_cases [OF g], simp_all)
   216 done
   217 
   218 lemma decisive_abs_rep:
   219   fixes abs rep
   220   assumes iso: "iso abs rep"
   221   assumes d: "decisive d"
   222   shows "decisive (abs oo d oo rep)"
   223 apply (rule decisiveI)
   224 apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
   225 apply (simp add: iso.rep_iso [OF iso])
   226 apply (simp add: iso.abs_strict [OF iso])
   227 done
   228 
   229 lemma lub_ID_finite:
   230   assumes chain: "chain d"
   231   assumes lub: "(\<Squnion>n. d n) = ID"
   232   assumes decisive: "\<And>n. decisive (d n)"
   233   shows "\<exists>n. d n\<cdot>x = x"
   234 proof -
   235   have 1: "chain (\<lambda>n. d n\<cdot>x)" using chain by simp
   236   have 2: "(\<Squnion>n. d n\<cdot>x) = x" using chain lub by (rule lub_ID_reach)
   237   have "\<forall>n. d n\<cdot>x = x \<or> d n\<cdot>x = \<bottom>"
   238     using decisive unfolding decisive_def by simp
   239   hence "range (\<lambda>n. d n\<cdot>x) \<subseteq> {x, \<bottom>}"
   240     by auto
   241   hence "finite (range (\<lambda>n. d n\<cdot>x))"
   242     by (rule finite_subset, simp)
   243   with 1 have "finite_chain (\<lambda>n. d n\<cdot>x)"
   244     by (rule finite_range_imp_finch)
   245   then have "\<exists>n. (\<Squnion>n. d n\<cdot>x) = d n\<cdot>x"
   246     unfolding finite_chain_def by (auto simp add: maxinch_is_thelub)
   247   with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym)
   248 qed
   249 
   250 lemma lub_ID_finite_take_induct:
   251   assumes "chain d" and "(\<Squnion>n. d n) = ID" and "\<And>n. decisive (d n)"
   252   shows "(\<And>n. P (d n\<cdot>x)) \<Longrightarrow> P x"
   253 using lub_ID_finite [OF assms] by metis
   254 
   255 subsection \<open>Proofs about constructor functions\<close>
   256 
   257 text \<open>Lemmas for proving nchotomy rule:\<close>
   258 
   259 lemma ex_one_bottom_iff:
   260   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
   261 by simp
   262 
   263 lemma ex_up_bottom_iff:
   264   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
   265 by (safe, case_tac x, auto)
   266 
   267 lemma ex_sprod_bottom_iff:
   268  "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
   269   (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
   270 by (safe, case_tac y, auto)
   271 
   272 lemma ex_sprod_up_bottom_iff:
   273  "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
   274   (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
   275 by (safe, case_tac y, simp, case_tac x, auto)
   276 
   277 lemma ex_ssum_bottom_iff:
   278  "(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
   279  ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
   280   (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
   281 by (safe, case_tac x, auto)
   282 
   283 lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
   284   by auto
   285 
   286 lemmas ex_bottom_iffs =
   287    ex_ssum_bottom_iff
   288    ex_sprod_up_bottom_iff
   289    ex_sprod_bottom_iff
   290    ex_up_bottom_iff
   291    ex_one_bottom_iff
   292 
   293 text \<open>Rules for turning nchotomy into exhaust:\<close>
   294 
   295 lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *)
   296   by auto
   297 
   298 lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)"
   299   by rule auto
   300 
   301 lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
   302   by rule auto
   303 
   304 lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
   305   by rule auto
   306 
   307 lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
   308 
   309 text \<open>Rules for proving constructor properties\<close>
   310 
   311 lemmas con_strict_rules =
   312   sinl_strict sinr_strict spair_strict1 spair_strict2
   313 
   314 lemmas con_bottom_iff_rules =
   315   sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined
   316 
   317 lemmas con_below_iff_rules =
   318   sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules
   319 
   320 lemmas con_eq_iff_rules =
   321   sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules
   322 
   323 lemmas sel_strict_rules =
   324   cfcomp2 sscase1 sfst_strict ssnd_strict fup1
   325 
   326 lemma sel_app_extra_rules:
   327   "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinr\<cdot>x) = \<bottom>"
   328   "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinl\<cdot>x) = x"
   329   "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinl\<cdot>x) = \<bottom>"
   330   "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinr\<cdot>x) = x"
   331   "fup\<cdot>ID\<cdot>(up\<cdot>x) = x"
   332 by (cases "x = \<bottom>", simp, simp)+
   333 
   334 lemmas sel_app_rules =
   335   sel_strict_rules sel_app_extra_rules
   336   ssnd_spair sfst_spair up_defined spair_defined
   337 
   338 lemmas sel_bottom_iff_rules =
   339   cfcomp2 sfst_bottom_iff ssnd_bottom_iff
   340 
   341 lemmas take_con_rules =
   342   ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
   343   deflation_strict deflation_ID ID1 cfcomp2
   344 
   345 subsection \<open>ML setup\<close>
   346 
   347 named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
   348   and domain_map_ID "theorems like foo_map$ID = ID"
   349 
   350 ML_file "Tools/Domain/domain_take_proofs.ML"
   351 ML_file "Tools/cont_consts.ML"
   352 ML_file "Tools/cont_proc.ML"
   353 ML_file "Tools/Domain/domain_constructors.ML"
   354 ML_file "Tools/Domain/domain_induction.ML"
   355 
   356 end