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