src/HOLCF/CompactBasis.thy
author huffman
Mon May 11 08:28:09 2009 -0700 (2009-05-11)
changeset 31095 b79d140f6d0b
parent 31076 99fe356cbbc2
child 35901 12f09bf2c77f
permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
     1 (*  Title:      HOLCF/CompactBasis.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Compact bases of domains *}
     6 
     7 theory CompactBasis
     8 imports Completion
     9 begin
    10 
    11 subsection {* Compact bases of bifinite domains *}
    12 
    13 defaultsort profinite
    14 
    15 typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}"
    16 by (fast intro: compact_approx)
    17 
    18 lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
    19 by (rule Rep_compact_basis [unfolded mem_Collect_eq])
    20 
    21 instantiation compact_basis :: (profinite) below
    22 begin
    23 
    24 definition
    25   compact_le_def:
    26     "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"
    27 
    28 instance ..
    29 
    30 end
    31 
    32 instance compact_basis :: (profinite) po
    33 by (rule typedef_po
    34     [OF type_definition_compact_basis compact_le_def])
    35 
    36 text {* Take function for compact basis *}
    37 
    38 definition
    39   compact_take :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where
    40   "compact_take = (\<lambda>n a. Abs_compact_basis (approx n\<cdot>(Rep_compact_basis a)))"
    41 
    42 lemma Rep_compact_take:
    43   "Rep_compact_basis (compact_take n a) = approx n\<cdot>(Rep_compact_basis a)"
    44 unfolding compact_take_def
    45 by (simp add: Abs_compact_basis_inverse)
    46 
    47 lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
    48 
    49 interpretation compact_basis:
    50   basis_take below compact_take
    51 proof
    52   fix n :: nat and a :: "'a compact_basis"
    53   show "compact_take n a \<sqsubseteq> a"
    54     unfolding compact_le_def
    55     by (simp add: Rep_compact_take approx_below)
    56 next
    57   fix n :: nat and a :: "'a compact_basis"
    58   show "compact_take n (compact_take n a) = compact_take n a"
    59     by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_take)
    60 next
    61   fix n :: nat and a b :: "'a compact_basis"
    62   assume "a \<sqsubseteq> b" thus "compact_take n a \<sqsubseteq> compact_take n b"
    63     unfolding compact_le_def Rep_compact_take
    64     by (rule monofun_cfun_arg)
    65 next
    66   fix n :: nat and a :: "'a compact_basis"
    67   show "\<And>n a. compact_take n a \<sqsubseteq> compact_take (Suc n) a"
    68     unfolding compact_le_def Rep_compact_take
    69     by (rule chainE, simp)
    70 next
    71   fix n :: nat
    72   show "finite (range (compact_take n))"
    73     apply (rule finite_imageD [where f="Rep_compact_basis"])
    74     apply (rule finite_subset [where B="range (\<lambda>x. approx n\<cdot>x)"])
    75     apply (clarsimp simp add: Rep_compact_take)
    76     apply (rule finite_range_approx)
    77     apply (rule inj_onI, simp add: Rep_compact_basis_inject)
    78     done
    79 next
    80   fix a :: "'a compact_basis"
    81   show "\<exists>n. compact_take n a = a"
    82     apply (simp add: Rep_compact_basis_inject [symmetric])
    83     apply (simp add: Rep_compact_take)
    84     apply (rule profinite_compact_eq_approx)
    85     apply (rule compact_Rep_compact_basis)
    86     done
    87 qed
    88 
    89 text {* Ideal completion *}
    90 
    91 definition
    92   approximants :: "'a \<Rightarrow> 'a compact_basis set" where
    93   "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
    94 
    95 interpretation compact_basis:
    96   ideal_completion below compact_take Rep_compact_basis approximants
    97 proof
    98   fix w :: 'a
    99   show "preorder.ideal below (approximants w)"
   100   proof (rule below.idealI)
   101     show "\<exists>x. x \<in> approximants w"
   102       unfolding approximants_def
   103       apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
   104       apply (simp add: Abs_compact_basis_inverse approx_below)
   105       done
   106   next
   107     fix x y :: "'a compact_basis"
   108     assume "x \<in> approximants w" "y \<in> approximants w"
   109     thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
   110       unfolding approximants_def
   111       apply simp
   112       apply (cut_tac a=x in compact_Rep_compact_basis)
   113       apply (cut_tac a=y in compact_Rep_compact_basis)
   114       apply (drule profinite_compact_eq_approx)
   115       apply (drule profinite_compact_eq_approx)
   116       apply (clarify, rename_tac i j)
   117       apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
   118       apply (simp add: compact_le_def)
   119       apply (simp add: Abs_compact_basis_inverse approx_below)
   120       apply (erule subst, erule subst)
   121       apply (simp add: monofun_cfun chain_mono [OF chain_approx])
   122       done
   123   next
   124     fix x y :: "'a compact_basis"
   125     assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w"
   126       unfolding approximants_def
   127       apply simp
   128       apply (simp add: compact_le_def)
   129       apply (erule (1) below_trans)
   130       done
   131   qed
   132 next
   133   fix Y :: "nat \<Rightarrow> 'a"
   134   assume Y: "chain Y"
   135   show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
   136     unfolding approximants_def
   137     apply safe
   138     apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
   139     apply (erule below_trans, rule is_ub_thelub [OF Y])
   140     done
   141 next
   142   fix a :: "'a compact_basis"
   143   show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
   144     unfolding approximants_def compact_le_def ..
   145 next
   146   fix x y :: "'a"
   147   assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y"
   148     apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
   149     apply (rule admD, simp, simp)
   150     apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
   151     apply (simp add: approximants_def Abs_compact_basis_inverse approx_below)
   152     apply (simp add: approximants_def Abs_compact_basis_inverse)
   153     done
   154 qed
   155 
   156 text {* minimal compact element *}
   157 
   158 definition
   159   compact_bot :: "'a::bifinite compact_basis" where
   160   "compact_bot = Abs_compact_basis \<bottom>"
   161 
   162 lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
   163 unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
   164 
   165 lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a"
   166 unfolding compact_le_def Rep_compact_bot by simp
   167 
   168 
   169 subsection {* A compact basis for powerdomains *}
   170 
   171 typedef 'a pd_basis =
   172   "{S::'a::profinite compact_basis set. finite S \<and> S \<noteq> {}}"
   173 by (rule_tac x="{arbitrary}" in exI, simp)
   174 
   175 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
   176 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
   177 
   178 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
   179 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
   180 
   181 text {* unit and plus *}
   182 
   183 definition
   184   PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
   185   "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
   186 
   187 definition
   188   PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
   189   "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
   190 
   191 lemma Rep_PDUnit:
   192   "Rep_pd_basis (PDUnit x) = {x}"
   193 unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
   194 
   195 lemma Rep_PDPlus:
   196   "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
   197 unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
   198 
   199 lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
   200 unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
   201 
   202 lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
   203 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
   204 
   205 lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
   206 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
   207 
   208 lemma PDPlus_absorb: "PDPlus t t = t"
   209 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
   210 
   211 lemma pd_basis_induct1:
   212   assumes PDUnit: "\<And>a. P (PDUnit a)"
   213   assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
   214   shows "P x"
   215 apply (induct x, unfold pd_basis_def, clarify)
   216 apply (erule (1) finite_ne_induct)
   217 apply (cut_tac a=x in PDUnit)
   218 apply (simp add: PDUnit_def)
   219 apply (drule_tac a=x in PDPlus)
   220 apply (simp add: PDUnit_def PDPlus_def Abs_pd_basis_inverse [unfolded pd_basis_def])
   221 done
   222 
   223 lemma pd_basis_induct:
   224   assumes PDUnit: "\<And>a. P (PDUnit a)"
   225   assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
   226   shows "P x"
   227 apply (induct x rule: pd_basis_induct1)
   228 apply (rule PDUnit, erule PDPlus [OF PDUnit])
   229 done
   230 
   231 text {* fold-pd *}
   232 
   233 definition
   234   fold_pd ::
   235     "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
   236   where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
   237 
   238 lemma fold_pd_PDUnit:
   239   assumes "ab_semigroup_idem_mult f"
   240   shows "fold_pd g f (PDUnit x) = g x"
   241 unfolding fold_pd_def Rep_PDUnit by simp
   242 
   243 lemma fold_pd_PDPlus:
   244   assumes "ab_semigroup_idem_mult f"
   245   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
   246 proof -
   247   interpret ab_semigroup_idem_mult f by fact
   248   show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
   249 qed
   250 
   251 text {* Take function for powerdomain basis *}
   252 
   253 definition
   254   pd_take :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
   255   "pd_take n = (\<lambda>t. Abs_pd_basis (compact_take n ` Rep_pd_basis t))"
   256 
   257 lemma Rep_pd_take:
   258   "Rep_pd_basis (pd_take n t) = compact_take n ` Rep_pd_basis t"
   259 unfolding pd_take_def
   260 apply (rule Abs_pd_basis_inverse)
   261 apply (simp add: pd_basis_def)
   262 done
   263 
   264 lemma pd_take_simps [simp]:
   265   "pd_take n (PDUnit a) = PDUnit (compact_take n a)"
   266   "pd_take n (PDPlus t u) = PDPlus (pd_take n t) (pd_take n u)"
   267 apply (simp_all add: Rep_pd_basis_inject [symmetric])
   268 apply (simp_all add: Rep_pd_take Rep_PDUnit Rep_PDPlus image_Un)
   269 done
   270 
   271 lemma pd_take_idem: "pd_take n (pd_take n t) = pd_take n t"
   272 apply (induct t rule: pd_basis_induct)
   273 apply (simp add: compact_basis.take_take)
   274 apply simp
   275 done
   276 
   277 lemma finite_range_pd_take: "finite (range (pd_take n))"
   278 apply (rule finite_imageD [where f="Rep_pd_basis"])
   279 apply (rule finite_subset [where B="Pow (range (compact_take n))"])
   280 apply (clarsimp simp add: Rep_pd_take)
   281 apply (simp add: compact_basis.finite_range_take)
   282 apply (rule inj_onI, simp add: Rep_pd_basis_inject)
   283 done
   284 
   285 lemma pd_take_covers: "\<exists>n. pd_take n t = t"
   286 apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. pd_take m t = t", fast)
   287 apply (induct t rule: pd_basis_induct)
   288 apply (cut_tac a=a in compact_basis.take_covers)
   289 apply (clarify, rule_tac x=n in exI)
   290 apply (clarify, simp)
   291 apply (rule below_antisym)
   292 apply (rule compact_basis.take_less)
   293 apply (drule_tac a=a in compact_basis.take_chain_le)
   294 apply simp
   295 apply (clarify, rename_tac i j)
   296 apply (rule_tac x="max i j" in exI, simp)
   297 done
   298 
   299 end