src/HOL/HOLCF/Domain_Aux.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (20 months ago) changeset 67022 49309fe530fd parent 62175 8ffc4d0e652d child 68383 93a42bd62ede permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
```     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
```