src/HOL/HOLCF/Algebraic.thy
author huffman
Sun Dec 19 05:15:31 2010 -0800 (2010-12-19)
changeset 41286 3d7685a4a5ff
parent 40888 28cd51cff70c
child 41287 029a6fc1bfb8
permissions -rw-r--r--
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
     1 (*  Title:      HOLCF/Algebraic.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Algebraic deflations *}
     6 
     7 theory Algebraic
     8 imports Universal Map_Functions
     9 begin
    10 
    11 subsection {* Type constructor for finite deflations *}
    12 
    13 typedef (open) fin_defl = "{d::udom \<rightarrow> udom. finite_deflation d}"
    14 by (fast intro: finite_deflation_UU)
    15 
    16 instantiation fin_defl :: below
    17 begin
    18 
    19 definition below_fin_defl_def:
    20     "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
    21 
    22 instance ..
    23 end
    24 
    25 instance fin_defl :: po
    26 using type_definition_fin_defl below_fin_defl_def
    27 by (rule typedef_po)
    28 
    29 lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
    30 using Rep_fin_defl by simp
    31 
    32 lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)"
    33 using finite_deflation_Rep_fin_defl
    34 by (rule finite_deflation_imp_deflation)
    35 
    36 interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
    37 by (rule finite_deflation_Rep_fin_defl)
    38 
    39 lemma fin_defl_belowI:
    40   "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
    41 unfolding below_fin_defl_def
    42 by (rule Rep_fin_defl.belowI)
    43 
    44 lemma fin_defl_belowD:
    45   "\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x"
    46 unfolding below_fin_defl_def
    47 by (rule Rep_fin_defl.belowD)
    48 
    49 lemma fin_defl_eqI:
    50   "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
    51 apply (rule below_antisym)
    52 apply (rule fin_defl_belowI, simp)
    53 apply (rule fin_defl_belowI, simp)
    54 done
    55 
    56 lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
    57 unfolding below_fin_defl_def .
    58 
    59 lemma Abs_fin_defl_mono:
    60   "\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk>
    61     \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
    62 unfolding below_fin_defl_def
    63 by (simp add: Abs_fin_defl_inverse)
    64 
    65 lemma (in finite_deflation) compact_belowI:
    66   assumes "\<And>x. compact x \<Longrightarrow> d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
    67 by (rule belowI, rule assms, erule subst, rule compact)
    68 
    69 lemma compact_Rep_fin_defl [simp]: "compact (Rep_fin_defl a)"
    70 using finite_deflation_Rep_fin_defl
    71 by (rule finite_deflation_imp_compact)
    72 
    73 subsection {* Defining algebraic deflations by ideal completion *}
    74 
    75 typedef (open) defl = "{S::fin_defl set. below.ideal S}"
    76 by (rule below.ex_ideal)
    77 
    78 instantiation defl :: below
    79 begin
    80 
    81 definition
    82   "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
    83 
    84 instance ..
    85 end
    86 
    87 instance defl :: po
    88 using type_definition_defl below_defl_def
    89 by (rule below.typedef_ideal_po)
    90 
    91 instance defl :: cpo
    92 using type_definition_defl below_defl_def
    93 by (rule below.typedef_ideal_cpo)
    94 
    95 definition
    96   defl_principal :: "fin_defl \<Rightarrow> defl" where
    97   "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
    98 
    99 lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
   100 proof -
   101   obtain f :: "udom compact_basis \<Rightarrow> nat" where inj_f: "inj f"
   102     using compact_basis.countable ..
   103   have *: "\<And>d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
   104     apply (rule finite_imageI)
   105     apply (rule finite_vimageI)
   106     apply (rule Rep_fin_defl.finite_fixes)
   107     apply (simp add: inj_on_def Rep_compact_basis_inject)
   108     done
   109   have range_eq: "range Rep_compact_basis = {x. compact x}"
   110     using type_definition_compact_basis by (rule type_definition.Rep_range)
   111   have "inj (\<lambda>d. set_encode
   112     (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
   113     apply (rule inj_onI)
   114     apply (simp only: set_encode_eq *)
   115     apply (simp only: inj_image_eq_iff inj_f)
   116     apply (drule_tac f="image Rep_compact_basis" in arg_cong)
   117     apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
   118     apply (rule Rep_fin_defl_inject [THEN iffD1])
   119     apply (rule below_antisym)
   120     apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
   121     apply (drule_tac x=z in spec, simp)
   122     apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
   123     apply (drule_tac x=z in spec, simp)
   124     done
   125   thus ?thesis by - (rule exI)
   126 qed
   127 
   128 interpretation defl: ideal_completion below defl_principal Rep_defl
   129 using type_definition_defl below_defl_def
   130 using defl_principal_def fin_defl_countable
   131 by (rule below.typedef_ideal_completion)
   132 
   133 text {* Algebraic deflations are pointed *}
   134 
   135 lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
   136 apply (induct x rule: defl.principal_induct, simp)
   137 apply (rule defl.principal_mono)
   138 apply (simp add: below_fin_defl_def)
   139 apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
   140 done
   141 
   142 instance defl :: pcpo
   143 by intro_classes (fast intro: defl_minimal)
   144 
   145 lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
   146 by (rule defl_minimal [THEN UU_I, symmetric])
   147 
   148 subsection {* Applying algebraic deflations *}
   149 
   150 definition
   151   cast :: "defl \<rightarrow> udom \<rightarrow> udom"
   152 where
   153   "cast = defl.basis_fun Rep_fin_defl"
   154 
   155 lemma cast_defl_principal:
   156   "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
   157 unfolding cast_def
   158 apply (rule defl.basis_fun_principal)
   159 apply (simp only: below_fin_defl_def)
   160 done
   161 
   162 lemma deflation_cast: "deflation (cast\<cdot>d)"
   163 apply (induct d rule: defl.principal_induct)
   164 apply (rule adm_subst [OF _ adm_deflation], simp)
   165 apply (simp add: cast_defl_principal)
   166 apply (rule finite_deflation_imp_deflation)
   167 apply (rule finite_deflation_Rep_fin_defl)
   168 done
   169 
   170 lemma finite_deflation_cast:
   171   "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
   172 apply (drule defl.compact_imp_principal, clarify)
   173 apply (simp add: cast_defl_principal)
   174 apply (rule finite_deflation_Rep_fin_defl)
   175 done
   176 
   177 interpretation cast: deflation "cast\<cdot>d"
   178 by (rule deflation_cast)
   179 
   180 declare cast.idem [simp]
   181 
   182 lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
   183 apply (rule finite_deflation_imp_compact)
   184 apply (erule finite_deflation_cast)
   185 done
   186 
   187 lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
   188 apply (induct A rule: defl.principal_induct, simp)
   189 apply (induct B rule: defl.principal_induct, simp)
   190 apply (simp add: cast_defl_principal below_fin_defl_def)
   191 done
   192 
   193 lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
   194 apply (rule iffI)
   195 apply (simp only: compact_def cast_below_cast [symmetric])
   196 apply (erule adm_subst [OF cont_Rep_cfun2])
   197 apply (erule compact_cast)
   198 done
   199 
   200 lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
   201 by (simp only: cast_below_cast)
   202 
   203 lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
   204 by (simp add: below_antisym cast_below_imp_below)
   205 
   206 lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
   207 apply (subst inst_defl_pcpo)
   208 apply (subst cast_defl_principal)
   209 apply (rule Abs_fin_defl_inverse)
   210 apply (simp add: finite_deflation_UU)
   211 done
   212 
   213 lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
   214 by (rule cast.below [THEN UU_I])
   215 
   216 end