src/HOLCF/CompactBasis.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 39986 38677db30cad
child 40497 d2e876d6da8c
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      HOLCF/CompactBasis.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* A compact basis for powerdomains *}
     6 
     7 theory CompactBasis
     8 imports Bifinite
     9 begin
    10 
    11 default_sort bifinite
    12 
    13 subsection {* A compact basis for powerdomains *}
    14 
    15 typedef 'a pd_basis =
    16   "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
    17 by (rule_tac x="{arbitrary}" in exI, simp)
    18 
    19 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
    20 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
    21 
    22 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
    23 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
    24 
    25 text {* The powerdomain basis type is countable. *}
    26 
    27 lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
    28 proof -
    29   obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
    30     using compact_basis.countable ..
    31   hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B"
    32     by (rule inj_image_eq_iff)
    33   have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))"
    34     by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
    35   thus ?thesis by - (rule exI)
    36   (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
    37 qed
    38 
    39 subsection {* Unit and plus constructors *}
    40 
    41 definition
    42   PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
    43   "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
    44 
    45 definition
    46   PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
    47   "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
    48 
    49 lemma Rep_PDUnit:
    50   "Rep_pd_basis (PDUnit x) = {x}"
    51 unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
    52 
    53 lemma Rep_PDPlus:
    54   "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
    55 unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
    56 
    57 lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
    58 unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
    59 
    60 lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
    61 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
    62 
    63 lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
    64 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
    65 
    66 lemma PDPlus_absorb: "PDPlus t t = t"
    67 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
    68 
    69 lemma pd_basis_induct1:
    70   assumes PDUnit: "\<And>a. P (PDUnit a)"
    71   assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
    72   shows "P x"
    73 apply (induct x, unfold pd_basis_def, clarify)
    74 apply (erule (1) finite_ne_induct)
    75 apply (cut_tac a=x in PDUnit)
    76 apply (simp add: PDUnit_def)
    77 apply (drule_tac a=x in PDPlus)
    78 apply (simp add: PDUnit_def PDPlus_def
    79   Abs_pd_basis_inverse [unfolded pd_basis_def])
    80 done
    81 
    82 lemma pd_basis_induct:
    83   assumes PDUnit: "\<And>a. P (PDUnit a)"
    84   assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
    85   shows "P x"
    86 apply (induct x rule: pd_basis_induct1)
    87 apply (rule PDUnit, erule PDPlus [OF PDUnit])
    88 done
    89 
    90 subsection {* Fold operator *}
    91 
    92 definition
    93   fold_pd ::
    94     "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
    95   where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
    96 
    97 lemma fold_pd_PDUnit:
    98   assumes "class.ab_semigroup_idem_mult f"
    99   shows "fold_pd g f (PDUnit x) = g x"
   100 unfolding fold_pd_def Rep_PDUnit by simp
   101 
   102 lemma fold_pd_PDPlus:
   103   assumes "class.ab_semigroup_idem_mult f"
   104   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
   105 proof -
   106   interpret ab_semigroup_idem_mult f by fact
   107   show ?thesis unfolding fold_pd_def Rep_PDPlus
   108     by (simp add: image_Un fold1_Un2)
   109 qed
   110 
   111 end