src/HOLCF/CompactBasis.thy
author huffman
Mon May 11 08:28:09 2009 -0700 (2009-05-11)
changeset 31095 b79d140f6d0b
parent 31076 99fe356cbbc2
child 35901 12f09bf2c77f
permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman@25904
     1
(*  Title:      HOLCF/CompactBasis.thy
huffman@25904
     2
    Author:     Brian Huffman
huffman@25904
     3
*)
huffman@25904
     4
huffman@25904
     5
header {* Compact bases of domains *}
huffman@25904
     6
huffman@25904
     7
theory CompactBasis
huffman@27404
     8
imports Completion
huffman@25904
     9
begin
huffman@25904
    10
huffman@25904
    11
subsection {* Compact bases of bifinite domains *}
huffman@25904
    12
huffman@26407
    13
defaultsort profinite
huffman@25904
    14
huffman@26407
    15
typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}"
huffman@25904
    16
by (fast intro: compact_approx)
huffman@25904
    17
huffman@27289
    18
lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
huffman@26927
    19
by (rule Rep_compact_basis [unfolded mem_Collect_eq])
huffman@25904
    20
huffman@31076
    21
instantiation compact_basis :: (profinite) below
huffman@26420
    22
begin
huffman@26420
    23
huffman@26420
    24
definition
huffman@26420
    25
  compact_le_def:
huffman@26420
    26
    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"
huffman@26420
    27
huffman@26420
    28
instance ..
huffman@26420
    29
huffman@26420
    30
end
huffman@26420
    31
huffman@26420
    32
instance compact_basis :: (profinite) po
huffman@26420
    33
by (rule typedef_po
huffman@26420
    34
    [OF type_definition_compact_basis compact_le_def])
huffman@25904
    35
huffman@27289
    36
text {* Take function for compact basis *}
huffman@25904
    37
huffman@25904
    38
definition
huffman@27406
    39
  compact_take :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where
huffman@27406
    40
  "compact_take = (\<lambda>n a. Abs_compact_basis (approx n\<cdot>(Rep_compact_basis a)))"
huffman@25904
    41
huffman@27406
    42
lemma Rep_compact_take:
huffman@27406
    43
  "Rep_compact_basis (compact_take n a) = approx n\<cdot>(Rep_compact_basis a)"
huffman@27406
    44
unfolding compact_take_def
huffman@25904
    45
by (simp add: Abs_compact_basis_inverse)
huffman@25904
    46
huffman@27406
    47
lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
huffman@25904
    48
wenzelm@30729
    49
interpretation compact_basis:
huffman@31076
    50
  basis_take below compact_take
huffman@27289
    51
proof
huffman@27289
    52
  fix n :: nat and a :: "'a compact_basis"
huffman@27406
    53
  show "compact_take n a \<sqsubseteq> a"
huffman@27289
    54
    unfolding compact_le_def
huffman@31076
    55
    by (simp add: Rep_compact_take approx_below)
huffman@27289
    56
next
huffman@27289
    57
  fix n :: nat and a :: "'a compact_basis"
huffman@27406
    58
  show "compact_take n (compact_take n a) = compact_take n a"
huffman@27406
    59
    by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_take)
huffman@27289
    60
next
huffman@27289
    61
  fix n :: nat and a b :: "'a compact_basis"
huffman@27406
    62
  assume "a \<sqsubseteq> b" thus "compact_take n a \<sqsubseteq> compact_take n b"
huffman@27406
    63
    unfolding compact_le_def Rep_compact_take
huffman@27289
    64
    by (rule monofun_cfun_arg)
huffman@27289
    65
next
huffman@27289
    66
  fix n :: nat and a :: "'a compact_basis"
huffman@27406
    67
  show "\<And>n a. compact_take n a \<sqsubseteq> compact_take (Suc n) a"
huffman@27406
    68
    unfolding compact_le_def Rep_compact_take
huffman@27289
    69
    by (rule chainE, simp)
huffman@27289
    70
next
huffman@27289
    71
  fix n :: nat
huffman@27406
    72
  show "finite (range (compact_take n))"
huffman@27289
    73
    apply (rule finite_imageD [where f="Rep_compact_basis"])
huffman@27289
    74
    apply (rule finite_subset [where B="range (\<lambda>x. approx n\<cdot>x)"])
huffman@27406
    75
    apply (clarsimp simp add: Rep_compact_take)
huffman@27289
    76
    apply (rule finite_range_approx)
huffman@27289
    77
    apply (rule inj_onI, simp add: Rep_compact_basis_inject)
huffman@27289
    78
    done
huffman@27289
    79
next
huffman@27289
    80
  fix a :: "'a compact_basis"
huffman@27406
    81
  show "\<exists>n. compact_take n a = a"
huffman@27289
    82
    apply (simp add: Rep_compact_basis_inject [symmetric])
huffman@27406
    83
    apply (simp add: Rep_compact_take)
huffman@27309
    84
    apply (rule profinite_compact_eq_approx)
huffman@27289
    85
    apply (rule compact_Rep_compact_basis)
huffman@27289
    86
    done
huffman@27289
    87
qed
huffman@25904
    88
huffman@27289
    89
text {* Ideal completion *}
huffman@25904
    90
huffman@27289
    91
definition
huffman@28890
    92
  approximants :: "'a \<Rightarrow> 'a compact_basis set" where
huffman@28890
    93
  "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
huffman@25904
    94
wenzelm@30729
    95
interpretation compact_basis:
huffman@31076
    96
  ideal_completion below compact_take Rep_compact_basis approximants
huffman@27289
    97
proof
huffman@27289
    98
  fix w :: 'a
huffman@31076
    99
  show "preorder.ideal below (approximants w)"
huffman@31076
   100
  proof (rule below.idealI)
huffman@28890
   101
    show "\<exists>x. x \<in> approximants w"
huffman@28890
   102
      unfolding approximants_def
huffman@27289
   103
      apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
huffman@31076
   104
      apply (simp add: Abs_compact_basis_inverse approx_below)
huffman@27289
   105
      done
huffman@27289
   106
  next
huffman@27289
   107
    fix x y :: "'a compact_basis"
huffman@28890
   108
    assume "x \<in> approximants w" "y \<in> approximants w"
huffman@28890
   109
    thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
huffman@28890
   110
      unfolding approximants_def
huffman@27289
   111
      apply simp
huffman@27289
   112
      apply (cut_tac a=x in compact_Rep_compact_basis)
huffman@27289
   113
      apply (cut_tac a=y in compact_Rep_compact_basis)
huffman@27309
   114
      apply (drule profinite_compact_eq_approx)
huffman@27309
   115
      apply (drule profinite_compact_eq_approx)
huffman@27289
   116
      apply (clarify, rename_tac i j)
huffman@27289
   117
      apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
huffman@27289
   118
      apply (simp add: compact_le_def)
huffman@31076
   119
      apply (simp add: Abs_compact_basis_inverse approx_below)
huffman@27289
   120
      apply (erule subst, erule subst)
huffman@27289
   121
      apply (simp add: monofun_cfun chain_mono [OF chain_approx])
huffman@27289
   122
      done
huffman@27289
   123
  next
huffman@27289
   124
    fix x y :: "'a compact_basis"
huffman@28890
   125
    assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w"
huffman@28890
   126
      unfolding approximants_def
huffman@27289
   127
      apply simp
huffman@27289
   128
      apply (simp add: compact_le_def)
huffman@31076
   129
      apply (erule (1) below_trans)
huffman@27289
   130
      done
huffman@27289
   131
  qed
huffman@27289
   132
next
huffman@27297
   133
  fix Y :: "nat \<Rightarrow> 'a"
huffman@27297
   134
  assume Y: "chain Y"
huffman@28890
   135
  show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
huffman@28890
   136
    unfolding approximants_def
huffman@27297
   137
    apply safe
huffman@27297
   138
    apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
huffman@31076
   139
    apply (erule below_trans, rule is_ub_thelub [OF Y])
huffman@27289
   140
    done
huffman@26420
   141
next
huffman@27289
   142
  fix a :: "'a compact_basis"
huffman@28890
   143
  show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
huffman@28890
   144
    unfolding approximants_def compact_le_def ..
huffman@26420
   145
next
huffman@26420
   146
  fix x y :: "'a"
huffman@28890
   147
  assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y"
huffman@27289
   148
    apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
huffman@27289
   149
    apply (rule admD, simp, simp)
huffman@27289
   150
    apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
huffman@31076
   151
    apply (simp add: approximants_def Abs_compact_basis_inverse approx_below)
huffman@28890
   152
    apply (simp add: approximants_def Abs_compact_basis_inverse)
huffman@27289
   153
    done
huffman@26420
   154
qed
huffman@25904
   155
huffman@27289
   156
text {* minimal compact element *}
huffman@27289
   157
huffman@27289
   158
definition
huffman@27289
   159
  compact_bot :: "'a::bifinite compact_basis" where
huffman@27289
   160
  "compact_bot = Abs_compact_basis \<bottom>"
huffman@27289
   161
huffman@27289
   162
lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
huffman@27289
   163
unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
huffman@27289
   164
huffman@28890
   165
lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a"
huffman@27289
   166
unfolding compact_le_def Rep_compact_bot by simp
huffman@27289
   167
huffman@25904
   168
huffman@25904
   169
subsection {* A compact basis for powerdomains *}
huffman@25904
   170
huffman@25904
   171
typedef 'a pd_basis =
huffman@26407
   172
  "{S::'a::profinite compact_basis set. finite S \<and> S \<noteq> {}}"
huffman@25904
   173
by (rule_tac x="{arbitrary}" in exI, simp)
huffman@25904
   174
huffman@25904
   175
lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
huffman@25904
   176
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
huffman@25904
   177
huffman@25904
   178
lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
huffman@25904
   179
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
huffman@25904
   180
huffman@25904
   181
text {* unit and plus *}
huffman@25904
   182
huffman@25904
   183
definition
huffman@25904
   184
  PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
huffman@25904
   185
  "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
huffman@25904
   186
huffman@25904
   187
definition
huffman@25904
   188
  PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
huffman@25904
   189
  "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
huffman@25904
   190
huffman@25904
   191
lemma Rep_PDUnit:
huffman@25904
   192
  "Rep_pd_basis (PDUnit x) = {x}"
huffman@25904
   193
unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
huffman@25904
   194
huffman@25904
   195
lemma Rep_PDPlus:
huffman@25904
   196
  "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
huffman@25904
   197
unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
huffman@25904
   198
huffman@25904
   199
lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
huffman@25904
   200
unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
huffman@25904
   201
huffman@25904
   202
lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
huffman@25904
   203
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
huffman@25904
   204
huffman@25904
   205
lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
huffman@25904
   206
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
huffman@25904
   207
huffman@25904
   208
lemma PDPlus_absorb: "PDPlus t t = t"
huffman@25904
   209
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
huffman@25904
   210
huffman@25904
   211
lemma pd_basis_induct1:
huffman@25904
   212
  assumes PDUnit: "\<And>a. P (PDUnit a)"
huffman@25904
   213
  assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
huffman@25904
   214
  shows "P x"
huffman@25904
   215
apply (induct x, unfold pd_basis_def, clarify)
huffman@25904
   216
apply (erule (1) finite_ne_induct)
huffman@25904
   217
apply (cut_tac a=x in PDUnit)
huffman@25904
   218
apply (simp add: PDUnit_def)
huffman@25904
   219
apply (drule_tac a=x in PDPlus)
huffman@25904
   220
apply (simp add: PDUnit_def PDPlus_def Abs_pd_basis_inverse [unfolded pd_basis_def])
huffman@25904
   221
done
huffman@25904
   222
huffman@25904
   223
lemma pd_basis_induct:
huffman@25904
   224
  assumes PDUnit: "\<And>a. P (PDUnit a)"
huffman@25904
   225
  assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
huffman@25904
   226
  shows "P x"
huffman@25904
   227
apply (induct x rule: pd_basis_induct1)
huffman@25904
   228
apply (rule PDUnit, erule PDPlus [OF PDUnit])
huffman@25904
   229
done
huffman@25904
   230
huffman@25904
   231
text {* fold-pd *}
huffman@25904
   232
huffman@25904
   233
definition
huffman@25904
   234
  fold_pd ::
huffman@25904
   235
    "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
huffman@25904
   236
  where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
huffman@25904
   237
huffman@26927
   238
lemma fold_pd_PDUnit:
ballarin@28611
   239
  assumes "ab_semigroup_idem_mult f"
huffman@26927
   240
  shows "fold_pd g f (PDUnit x) = g x"
huffman@25904
   241
unfolding fold_pd_def Rep_PDUnit by simp
huffman@25904
   242
huffman@26927
   243
lemma fold_pd_PDPlus:
ballarin@28611
   244
  assumes "ab_semigroup_idem_mult f"
huffman@26927
   245
  shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
ballarin@28611
   246
proof -
haftmann@29511
   247
  interpret ab_semigroup_idem_mult f by fact
ballarin@28611
   248
  show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
ballarin@28611
   249
qed
huffman@25904
   250
huffman@27405
   251
text {* Take function for powerdomain basis *}
huffman@25904
   252
huffman@25904
   253
definition
huffman@27405
   254
  pd_take :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
huffman@27406
   255
  "pd_take n = (\<lambda>t. Abs_pd_basis (compact_take n ` Rep_pd_basis t))"
huffman@25904
   256
huffman@27405
   257
lemma Rep_pd_take:
huffman@27406
   258
  "Rep_pd_basis (pd_take n t) = compact_take n ` Rep_pd_basis t"
huffman@27405
   259
unfolding pd_take_def
huffman@25904
   260
apply (rule Abs_pd_basis_inverse)
huffman@25904
   261
apply (simp add: pd_basis_def)
huffman@25904
   262
done
huffman@25904
   263
huffman@27405
   264
lemma pd_take_simps [simp]:
huffman@27406
   265
  "pd_take n (PDUnit a) = PDUnit (compact_take n a)"
huffman@27405
   266
  "pd_take n (PDPlus t u) = PDPlus (pd_take n t) (pd_take n u)"
huffman@25904
   267
apply (simp_all add: Rep_pd_basis_inject [symmetric])
huffman@27405
   268
apply (simp_all add: Rep_pd_take Rep_PDUnit Rep_PDPlus image_Un)
huffman@25904
   269
done
huffman@25904
   270
huffman@27405
   271
lemma pd_take_idem: "pd_take n (pd_take n t) = pd_take n t"
huffman@25904
   272
apply (induct t rule: pd_basis_induct)
huffman@27289
   273
apply (simp add: compact_basis.take_take)
huffman@25904
   274
apply simp
huffman@25904
   275
done
huffman@25904
   276
huffman@27405
   277
lemma finite_range_pd_take: "finite (range (pd_take n))"
huffman@27289
   278
apply (rule finite_imageD [where f="Rep_pd_basis"])
huffman@27406
   279
apply (rule finite_subset [where B="Pow (range (compact_take n))"])
huffman@27405
   280
apply (clarsimp simp add: Rep_pd_take)
huffman@27289
   281
apply (simp add: compact_basis.finite_range_take)
huffman@25904
   282
apply (rule inj_onI, simp add: Rep_pd_basis_inject)
huffman@25904
   283
done
huffman@25904
   284
huffman@27405
   285
lemma pd_take_covers: "\<exists>n. pd_take n t = t"
huffman@27405
   286
apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. pd_take m t = t", fast)
huffman@25904
   287
apply (induct t rule: pd_basis_induct)
huffman@27289
   288
apply (cut_tac a=a in compact_basis.take_covers)
huffman@25904
   289
apply (clarify, rule_tac x=n in exI)
huffman@25904
   290
apply (clarify, simp)
huffman@31076
   291
apply (rule below_antisym)
huffman@27289
   292
apply (rule compact_basis.take_less)
huffman@27289
   293
apply (drule_tac a=a in compact_basis.take_chain_le)
huffman@25904
   294
apply simp
huffman@25904
   295
apply (clarify, rename_tac i j)
huffman@25904
   296
apply (rule_tac x="max i j" in exI, simp)
huffman@25904
   297
done
huffman@25904
   298
huffman@25904
   299
end