src/HOLCF/Algebraic.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 39989 ad60d7311f43
child 40038 9d061b3d8f46
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      HOLCF/Algebraic.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Algebraic deflations *}
     6 
     7 theory Algebraic
     8 imports Universal
     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 (fast intro: below.ideal_principal)
    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   have *: "\<And>d. finite (approx_chain.place udom_approx `
   102                Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
   103     apply (rule finite_imageI)
   104     apply (rule finite_vimageI)
   105     apply (rule Rep_fin_defl.finite_fixes)
   106     apply (simp add: inj_on_def Rep_compact_basis_inject)
   107     done
   108   have range_eq: "range Rep_compact_basis = {x. compact x}"
   109     using type_definition_compact_basis by (rule type_definition.Rep_range)
   110   show "inj (\<lambda>d. set_encode
   111     (approx_chain.place udom_approx ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
   112     apply (rule inj_onI)
   113     apply (simp only: set_encode_eq *)
   114     apply (simp only: inj_image_eq_iff approx_chain.inj_place [OF udom_approx])
   115     apply (drule_tac f="image Rep_compact_basis" in arg_cong)
   116     apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
   117     apply (rule Rep_fin_defl_inject [THEN iffD1])
   118     apply (rule below_antisym)
   119     apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
   120     apply (drule_tac x=z in spec, simp)
   121     apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
   122     apply (drule_tac x=z in spec, simp)
   123     done
   124 qed
   125 
   126 interpretation defl: ideal_completion below defl_principal Rep_defl
   127 using type_definition_defl below_defl_def
   128 using defl_principal_def fin_defl_countable
   129 by (rule below.typedef_ideal_completion)
   130 
   131 text {* Algebraic deflations are pointed *}
   132 
   133 lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
   134 apply (induct x rule: defl.principal_induct, simp)
   135 apply (rule defl.principal_mono)
   136 apply (simp add: below_fin_defl_def)
   137 apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
   138 done
   139 
   140 instance defl :: pcpo
   141 by intro_classes (fast intro: defl_minimal)
   142 
   143 lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
   144 by (rule defl_minimal [THEN UU_I, symmetric])
   145 
   146 subsection {* Applying algebraic deflations *}
   147 
   148 definition
   149   cast :: "defl \<rightarrow> udom \<rightarrow> udom"
   150 where
   151   "cast = defl.basis_fun Rep_fin_defl"
   152 
   153 lemma cast_defl_principal:
   154   "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
   155 unfolding cast_def
   156 apply (rule defl.basis_fun_principal)
   157 apply (simp only: below_fin_defl_def)
   158 done
   159 
   160 lemma deflation_cast: "deflation (cast\<cdot>d)"
   161 apply (induct d rule: defl.principal_induct)
   162 apply (rule adm_subst [OF _ adm_deflation], simp)
   163 apply (simp add: cast_defl_principal)
   164 apply (rule finite_deflation_imp_deflation)
   165 apply (rule finite_deflation_Rep_fin_defl)
   166 done
   167 
   168 lemma finite_deflation_cast:
   169   "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
   170 apply (drule defl.compact_imp_principal, clarify)
   171 apply (simp add: cast_defl_principal)
   172 apply (rule finite_deflation_Rep_fin_defl)
   173 done
   174 
   175 interpretation cast: deflation "cast\<cdot>d"
   176 by (rule deflation_cast)
   177 
   178 declare cast.idem [simp]
   179 
   180 lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
   181 apply (rule finite_deflation_imp_compact)
   182 apply (erule finite_deflation_cast)
   183 done
   184 
   185 lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
   186 apply (induct A rule: defl.principal_induct, simp)
   187 apply (induct B rule: defl.principal_induct, simp)
   188 apply (simp add: cast_defl_principal below_fin_defl_def)
   189 done
   190 
   191 lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
   192 apply (rule iffI)
   193 apply (simp only: compact_def cast_below_cast [symmetric])
   194 apply (erule adm_subst [OF cont_Rep_CFun2])
   195 apply (erule compact_cast)
   196 done
   197 
   198 lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
   199 by (simp only: cast_below_cast)
   200 
   201 lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
   202 by (simp add: below_antisym cast_below_imp_below)
   203 
   204 lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
   205 apply (subst inst_defl_pcpo)
   206 apply (subst cast_defl_principal)
   207 apply (rule Abs_fin_defl_inverse)
   208 apply (simp add: finite_deflation_UU)
   209 done
   210 
   211 lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
   212 by (rule cast.below [THEN UU_I])
   213 
   214 subsection {* Deflation membership relation *}
   215 
   216 definition
   217   in_defl :: "udom \<Rightarrow> defl \<Rightarrow> bool" (infixl ":::" 50)
   218 where
   219   "x ::: A \<longleftrightarrow> cast\<cdot>A\<cdot>x = x"
   220 
   221 lemma adm_in_defl: "adm (\<lambda>x. x ::: A)"
   222 unfolding in_defl_def by simp
   223 
   224 lemma in_deflI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
   225 unfolding in_defl_def .
   226 
   227 lemma cast_fixed: "x ::: A \<Longrightarrow> cast\<cdot>A\<cdot>x = x"
   228 unfolding in_defl_def .
   229 
   230 lemma cast_in_defl [simp]: "cast\<cdot>A\<cdot>x ::: A"
   231 unfolding in_defl_def by (rule cast.idem)
   232 
   233 lemma bottom_in_defl [simp]: "\<bottom> ::: A"
   234 unfolding in_defl_def by (rule cast_strict2)
   235 
   236 lemma defl_belowD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
   237 unfolding in_defl_def
   238  apply (rule deflation.belowD)
   239    apply (rule deflation_cast)
   240   apply (erule monofun_cfun_arg)
   241  apply assumption
   242 done
   243 
   244 lemma rev_defl_belowD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
   245 by (rule defl_belowD)
   246 
   247 lemma defl_belowI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
   248 apply (rule cast_below_imp_below)
   249 apply (rule cast.belowI)
   250 apply (simp add: in_defl_def)
   251 done
   252 
   253 end