src/HOL/HOLCF/Algebraic.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62175 8ffc4d0e652d
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 (*  Title:      HOL/HOLCF/Algebraic.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section \<open>Algebraic deflations\<close>
     6 
     7 theory Algebraic
     8 imports Universal Map_Functions
     9 begin
    10 
    11 default_sort bifinite
    12 
    13 subsection \<open>Type constructor for finite deflations\<close>
    14 
    15 typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
    16 by (fast intro: finite_deflation_bottom)
    17 
    18 instantiation fin_defl :: (bifinite) below
    19 begin
    20 
    21 definition below_fin_defl_def:
    22   "below \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
    23 
    24 instance ..
    25 end
    26 
    27 instance fin_defl :: (bifinite) po
    28 using type_definition_fin_defl below_fin_defl_def
    29 by (rule typedef_po)
    30 
    31 lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
    32 using Rep_fin_defl by simp
    33 
    34 lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)"
    35 using finite_deflation_Rep_fin_defl
    36 by (rule finite_deflation_imp_deflation)
    37 
    38 interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
    39 by (rule finite_deflation_Rep_fin_defl)
    40 
    41 lemma fin_defl_belowI:
    42   "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
    43 unfolding below_fin_defl_def
    44 by (rule Rep_fin_defl.belowI)
    45 
    46 lemma fin_defl_belowD:
    47   "\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x"
    48 unfolding below_fin_defl_def
    49 by (rule Rep_fin_defl.belowD)
    50 
    51 lemma fin_defl_eqI:
    52   "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
    53 apply (rule below_antisym)
    54 apply (rule fin_defl_belowI, simp)
    55 apply (rule fin_defl_belowI, simp)
    56 done
    57 
    58 lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
    59 unfolding below_fin_defl_def .
    60 
    61 lemma Abs_fin_defl_mono:
    62   "\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk>
    63     \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
    64 unfolding below_fin_defl_def
    65 by (simp add: Abs_fin_defl_inverse)
    66 
    67 lemma (in finite_deflation) compact_belowI:
    68   assumes "\<And>x. compact x \<Longrightarrow> d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
    69 by (rule belowI, rule assms, erule subst, rule compact)
    70 
    71 lemma compact_Rep_fin_defl [simp]: "compact (Rep_fin_defl a)"
    72 using finite_deflation_Rep_fin_defl
    73 by (rule finite_deflation_imp_compact)
    74 
    75 subsection \<open>Defining algebraic deflations by ideal completion\<close>
    76 
    77 typedef 'a defl = "{S::'a fin_defl set. below.ideal S}"
    78 by (rule below.ex_ideal)
    79 
    80 instantiation defl :: (bifinite) below
    81 begin
    82 
    83 definition
    84   "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
    85 
    86 instance ..
    87 end
    88 
    89 instance defl :: (bifinite) po
    90 using type_definition_defl below_defl_def
    91 by (rule below.typedef_ideal_po)
    92 
    93 instance defl :: (bifinite) cpo
    94 using type_definition_defl below_defl_def
    95 by (rule below.typedef_ideal_cpo)
    96 
    97 definition
    98   defl_principal :: "'a fin_defl \<Rightarrow> 'a defl" where
    99   "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
   100 
   101 lemma fin_defl_countable: "\<exists>f::'a fin_defl \<Rightarrow> nat. inj f"
   102 proof -
   103   obtain f :: "'a compact_basis \<Rightarrow> nat" where inj_f: "inj f"
   104     using compact_basis.countable ..
   105   have *: "\<And>d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
   106     apply (rule finite_imageI)
   107     apply (rule finite_vimageI)
   108     apply (rule Rep_fin_defl.finite_fixes)
   109     apply (simp add: inj_on_def Rep_compact_basis_inject)
   110     done
   111   have range_eq: "range Rep_compact_basis = {x. compact x}"
   112     using type_definition_compact_basis by (rule type_definition.Rep_range)
   113   have "inj (\<lambda>d. set_encode
   114     (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
   115     apply (rule inj_onI)
   116     apply (simp only: set_encode_eq *)
   117     apply (simp only: inj_image_eq_iff inj_f)
   118     apply (drule_tac f="image Rep_compact_basis" in arg_cong)
   119     apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
   120     apply (rule Rep_fin_defl_inject [THEN iffD1])
   121     apply (rule below_antisym)
   122     apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
   123     apply (drule_tac x=z in spec, simp)
   124     apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
   125     apply (drule_tac x=z in spec, simp)
   126     done
   127   thus ?thesis by - (rule exI)
   128 qed
   129 
   130 interpretation defl: ideal_completion below defl_principal Rep_defl
   131 using type_definition_defl below_defl_def
   132 using defl_principal_def fin_defl_countable
   133 by (rule below.typedef_ideal_completion)
   134 
   135 text \<open>Algebraic deflations are pointed\<close>
   136 
   137 lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
   138 apply (induct x rule: defl.principal_induct, simp)
   139 apply (rule defl.principal_mono)
   140 apply (simp add: below_fin_defl_def)
   141 apply (simp add: Abs_fin_defl_inverse finite_deflation_bottom)
   142 done
   143 
   144 instance defl :: (bifinite) pcpo
   145 by intro_classes (fast intro: defl_minimal)
   146 
   147 lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
   148 by (rule defl_minimal [THEN bottomI, symmetric])
   149 
   150 subsection \<open>Applying algebraic deflations\<close>
   151 
   152 definition
   153   cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
   154 where
   155   "cast = defl.extension Rep_fin_defl"
   156 
   157 lemma cast_defl_principal:
   158   "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
   159 unfolding cast_def
   160 apply (rule defl.extension_principal)
   161 apply (simp only: below_fin_defl_def)
   162 done
   163 
   164 lemma deflation_cast: "deflation (cast\<cdot>d)"
   165 apply (induct d rule: defl.principal_induct)
   166 apply (rule adm_subst [OF _ adm_deflation], simp)
   167 apply (simp add: cast_defl_principal)
   168 apply (rule finite_deflation_imp_deflation)
   169 apply (rule finite_deflation_Rep_fin_defl)
   170 done
   171 
   172 lemma finite_deflation_cast:
   173   "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
   174 apply (drule defl.compact_imp_principal, clarify)
   175 apply (simp add: cast_defl_principal)
   176 apply (rule finite_deflation_Rep_fin_defl)
   177 done
   178 
   179 interpretation cast: deflation "cast\<cdot>d"
   180 by (rule deflation_cast)
   181 
   182 declare cast.idem [simp]
   183 
   184 lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
   185 apply (rule finite_deflation_imp_compact)
   186 apply (erule finite_deflation_cast)
   187 done
   188 
   189 lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
   190 apply (induct A rule: defl.principal_induct, simp)
   191 apply (induct B rule: defl.principal_induct, simp)
   192 apply (simp add: cast_defl_principal below_fin_defl_def)
   193 done
   194 
   195 lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
   196 apply (rule iffI)
   197 apply (simp only: compact_def cast_below_cast [symmetric])
   198 apply (erule adm_subst [OF cont_Rep_cfun2])
   199 apply (erule compact_cast)
   200 done
   201 
   202 lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
   203 by (simp only: cast_below_cast)
   204 
   205 lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
   206 by (simp add: below_antisym cast_below_imp_below)
   207 
   208 lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
   209 apply (subst inst_defl_pcpo)
   210 apply (subst cast_defl_principal)
   211 apply (rule Abs_fin_defl_inverse)
   212 apply (simp add: finite_deflation_bottom)
   213 done
   214 
   215 lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
   216 by (rule cast.below [THEN bottomI])
   217 
   218 subsection \<open>Deflation combinators\<close>
   219 
   220 definition
   221   "defl_fun1 e p f =
   222     defl.extension (\<lambda>a.
   223       defl_principal (Abs_fin_defl
   224         (e oo f\<cdot>(Rep_fin_defl a) oo p)))"
   225 
   226 definition
   227   "defl_fun2 e p f =
   228     defl.extension (\<lambda>a.
   229       defl.extension (\<lambda>b.
   230         defl_principal (Abs_fin_defl
   231           (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p))))"
   232 
   233 lemma cast_defl_fun1:
   234   assumes ep: "ep_pair e p"
   235   assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
   236   shows "cast\<cdot>(defl_fun1 e p f\<cdot>A) = e oo f\<cdot>(cast\<cdot>A) oo p"
   237 proof -
   238   have 1: "\<And>a. finite_deflation (e oo f\<cdot>(Rep_fin_defl a) oo p)"
   239     apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
   240     apply (rule f, rule finite_deflation_Rep_fin_defl)
   241     done
   242   show ?thesis
   243     by (induct A rule: defl.principal_induct, simp)
   244        (simp only: defl_fun1_def
   245                    defl.extension_principal
   246                    defl.extension_mono
   247                    defl.principal_mono
   248                    Abs_fin_defl_mono [OF 1 1]
   249                    monofun_cfun below_refl
   250                    Rep_fin_defl_mono
   251                    cast_defl_principal
   252                    Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
   253 qed
   254 
   255 lemma cast_defl_fun2:
   256   assumes ep: "ep_pair e p"
   257   assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
   258                 finite_deflation (f\<cdot>a\<cdot>b)"
   259   shows "cast\<cdot>(defl_fun2 e p f\<cdot>A\<cdot>B) = e oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo p"
   260 proof -
   261   have 1: "\<And>a b. finite_deflation
   262       (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p)"
   263     apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
   264     apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
   265     done
   266   show ?thesis
   267     apply (induct A rule: defl.principal_induct, simp)
   268     apply (induct B rule: defl.principal_induct, simp)
   269     by (simp only: defl_fun2_def
   270                    defl.extension_principal
   271                    defl.extension_mono
   272                    defl.principal_mono
   273                    Abs_fin_defl_mono [OF 1 1]
   274                    monofun_cfun below_refl
   275                    Rep_fin_defl_mono
   276                    cast_defl_principal
   277                    Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
   278 qed
   279 
   280 end