src/HOLCF/CompactBasis.thy
author huffman
Wed, 06 Oct 2010 10:49:27 -0700
changeset 39974 b525988432e9
parent 39967 1c6dce3ef477
child 39981 fdff0444fa7d
permissions -rw-r--r--
major reorganization/simplification of HOLCF type classes: removed profinite/bifinite classes and approx function; universal domain uses approx_chain locale instead of bifinite class; ideal_completion locale does not use 'take' functions, requires countable basis instead; replaced type 'udom alg_defl' with type 'sfp'; replaced class 'rep' with class 'sfp'; renamed REP('a) to SFP('a);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/CompactBasis.thy
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     3
*)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     4
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
     5
header {* A compact basis for powerdomains *}
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     6
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     7
theory CompactBasis
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
     8
imports Algebraic
26420
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
     9
begin
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    10
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    11
default_sort sfp
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    12
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    13
subsection {* A compact basis for powerdomains *}
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    14
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    15
typedef 'a pd_basis =
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    16
  "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    17
by (rule_tac x="{arbitrary}" in exI, simp)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    18
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    19
lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    20
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    21
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    22
lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    23
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    24
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    25
text {* The powerdomain basis type is countable. *}
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    26
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    27
lemma pd_basis_countable: "\<exists>f::'a::sfp pd_basis \<Rightarrow> nat. inj f"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    28
proof -
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    29
  obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    30
    using compact_basis.countable ..
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    31
  hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    32
    by (rule inj_image_eq_iff)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    33
  have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    34
    by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    35
  thus ?thesis by - (rule exI)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    36
  (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    37
qed
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    38
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    39
subsection {* Unit and plus constructors *}
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    40
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    41
definition
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    42
  PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    43
  "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    44
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    45
definition
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    46
  PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    47
  "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    48
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    49
lemma Rep_PDUnit:
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    50
  "Rep_pd_basis (PDUnit x) = {x}"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    51
unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    52
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    53
lemma Rep_PDPlus:
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    54
  "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    55
unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    56
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    57
lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    58
unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    59
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    60
lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    61
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    62
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    63
lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    64
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    65
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    66
lemma PDPlus_absorb: "PDPlus t t = t"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    67
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    68
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    69
lemma pd_basis_induct1:
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    70
  assumes PDUnit: "\<And>a. P (PDUnit a)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    71
  assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    72
  shows "P x"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    73
apply (induct x, unfold pd_basis_def, clarify)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    74
apply (erule (1) finite_ne_induct)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    75
apply (cut_tac a=x in PDUnit)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    76
apply (simp add: PDUnit_def)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    77
apply (drule_tac a=x in PDPlus)
35901
12f09bf2c77f fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents: 31076
diff changeset
    78
apply (simp add: PDUnit_def PDPlus_def
12f09bf2c77f fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents: 31076
diff changeset
    79
  Abs_pd_basis_inverse [unfolded pd_basis_def])
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    80
done
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    81
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    82
lemma pd_basis_induct:
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    83
  assumes PDUnit: "\<And>a. P (PDUnit a)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    84
  assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    85
  shows "P x"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    86
apply (induct x rule: pd_basis_induct1)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    87
apply (rule PDUnit, erule PDPlus [OF PDUnit])
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    88
done
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    89
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
    90
subsection {* Fold operator *}
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    91
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    92
definition
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    93
  fold_pd ::
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    94
    "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    95
  where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    96
26927
8684b5240f11 rename locales;
huffman
parents: 26806
diff changeset
    97
lemma fold_pd_PDUnit:
36635
080b755377c0 locale predicates of classes carry a mandatory "class" prefix
haftmann
parents: 36452
diff changeset
    98
  assumes "class.ab_semigroup_idem_mult f"
26927
8684b5240f11 rename locales;
huffman
parents: 26806
diff changeset
    99
  shows "fold_pd g f (PDUnit x) = g x"
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   100
unfolding fold_pd_def Rep_PDUnit by simp
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   101
26927
8684b5240f11 rename locales;
huffman
parents: 26806
diff changeset
   102
lemma fold_pd_PDPlus:
36635
080b755377c0 locale predicates of classes carry a mandatory "class" prefix
haftmann
parents: 36452
diff changeset
   103
  assumes "class.ab_semigroup_idem_mult f"
26927
8684b5240f11 rename locales;
huffman
parents: 26806
diff changeset
   104
  shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27406
diff changeset
   105
proof -
29511
7071b017cb35 migrated class package to new locale implementation
haftmann
parents: 29252
diff changeset
   106
  interpret ab_semigroup_idem_mult f by fact
35901
12f09bf2c77f fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents: 31076
diff changeset
   107
  show ?thesis unfolding fold_pd_def Rep_PDPlus
12f09bf2c77f fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents: 31076
diff changeset
   108
    by (simp add: image_Un fold1_Un2)
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27406
diff changeset
   109
qed
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   110
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   111
subsection {* Lemmas for proving if-and-only-if inequalities *}
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   112
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   113
lemma chain_max_below_iff:
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   114
  assumes Y: "chain Y" shows "Y (max i j) \<sqsubseteq> x \<longleftrightarrow> Y i \<sqsubseteq> x \<and> Y j \<sqsubseteq> x"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   115
apply auto
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   116
apply (erule below_trans [OF chain_mono [OF Y le_maxI1]])
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   117
apply (erule below_trans [OF chain_mono [OF Y le_maxI2]])
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   118
apply (simp add: max_def)
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   119
done
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   120
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   121
lemma all_ex_below_disj_iff:
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   122
  assumes "chain X" and "chain Y"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   123
  shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<or> Y i \<sqsubseteq> Z j) \<longleftrightarrow>
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   124
         (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<or> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   125
by (metis chain_max_below_iff assms)
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   126
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   127
lemma all_ex_below_conj_iff:
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   128
  assumes "chain X" and "chain Y" and "chain Z"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   129
  shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<and> Y i \<sqsubseteq> Z j) \<longleftrightarrow>
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   130
         (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<and> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39967
diff changeset
   131
oops
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   132
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   133
end