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