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