src/HOLCF/Sum_Cpo.thy
author huffman
Mon May 11 08:28:09 2009 -0700 (2009-05-11)
changeset 31095 b79d140f6d0b
parent 31076 99fe356cbbc2
child 35900 aa5dfb03eb1e
permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman@29534
     1
(*  Title:      HOLCF/Sum_Cpo.thy
huffman@29130
     2
    Author:     Brian Huffman
huffman@29130
     3
*)
huffman@29130
     4
huffman@29130
     5
header {* The cpo of disjoint sums *}
huffman@29130
     6
huffman@29534
     7
theory Sum_Cpo
huffman@29130
     8
imports Bifinite
huffman@29130
     9
begin
huffman@29130
    10
huffman@29130
    11
subsection {* Ordering on type @{typ "'a + 'b"} *}
huffman@29130
    12
huffman@31076
    13
instantiation "+" :: (below, below) below
huffman@29130
    14
begin
huffman@29130
    15
huffman@31076
    16
definition below_sum_def:
huffman@31076
    17
  "x \<sqsubseteq> y \<equiv> case x of
huffman@29130
    18
         Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
huffman@29130
    19
         Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
huffman@29130
    20
huffman@29130
    21
instance ..
huffman@29130
    22
end
huffman@29130
    23
huffman@31076
    24
lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
huffman@31076
    25
unfolding below_sum_def by simp
huffman@29130
    26
huffman@31076
    27
lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
huffman@31076
    28
unfolding below_sum_def by simp
huffman@29130
    29
huffman@31076
    30
lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
huffman@31076
    31
unfolding below_sum_def by simp
huffman@29130
    32
huffman@31076
    33
lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
huffman@31076
    34
unfolding below_sum_def by simp
huffman@29130
    35
huffman@29130
    36
lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
huffman@29130
    37
by simp
huffman@29130
    38
huffman@29130
    39
lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
huffman@29130
    40
by simp
huffman@29130
    41
huffman@31076
    42
lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
huffman@29130
    43
by (cases x, simp_all)
huffman@29130
    44
huffman@31076
    45
lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
huffman@29130
    46
by (cases x, simp_all)
huffman@29130
    47
huffman@31076
    48
lemmas sum_below_elims = Inl_belowE Inr_belowE
huffman@29130
    49
huffman@31076
    50
lemma sum_below_cases:
huffman@29130
    51
  "\<lbrakk>x \<sqsubseteq> y;
huffman@29130
    52
    \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
huffman@29130
    53
    \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
huffman@29130
    54
      \<Longrightarrow> R"
huffman@31076
    55
by (cases x, safe elim!: sum_below_elims, auto)
huffman@29130
    56
huffman@29130
    57
subsection {* Sum type is a complete partial order *}
huffman@29130
    58
huffman@29130
    59
instance "+" :: (po, po) po
huffman@29130
    60
proof
huffman@29130
    61
  fix x :: "'a + 'b"
huffman@29130
    62
  show "x \<sqsubseteq> x"
huffman@29130
    63
    by (induct x, simp_all)
huffman@29130
    64
next
huffman@29130
    65
  fix x y :: "'a + 'b"
huffman@29130
    66
  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
huffman@31076
    67
    by (induct x, auto elim!: sum_below_elims intro: below_antisym)
huffman@29130
    68
next
huffman@29130
    69
  fix x y z :: "'a + 'b"
huffman@29130
    70
  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
huffman@31076
    71
    by (induct x, auto elim!: sum_below_elims intro: below_trans)
huffman@29130
    72
qed
huffman@29130
    73
huffman@29130
    74
lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
huffman@31076
    75
by (rule monofunI, erule sum_below_cases, simp_all)
huffman@29130
    76
huffman@29130
    77
lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
huffman@31076
    78
by (rule monofunI, erule sum_below_cases, simp_all)
huffman@29130
    79
huffman@29130
    80
lemma sum_chain_cases:
huffman@29130
    81
  assumes Y: "chain Y"
huffman@29130
    82
  assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R"
huffman@29130
    83
  assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R"
huffman@29130
    84
  shows "R"
huffman@29130
    85
 apply (cases "Y 0")
huffman@29130
    86
  apply (rule A)
huffman@29130
    87
   apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
huffman@29130
    88
  apply (rule ext)
huffman@29130
    89
  apply (cut_tac j=i in chain_mono [OF Y le0], simp)
huffman@31076
    90
  apply (erule Inl_belowE, simp)
huffman@29130
    91
 apply (rule B)
huffman@29130
    92
  apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
huffman@29130
    93
 apply (rule ext)
huffman@29130
    94
 apply (cut_tac j=i in chain_mono [OF Y le0], simp)
huffman@31076
    95
 apply (erule Inr_belowE, simp)
huffman@29130
    96
done
huffman@29130
    97
huffman@29130
    98
lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
huffman@29130
    99
 apply (rule is_lubI)
huffman@29130
   100
  apply (rule ub_rangeI)
huffman@29130
   101
  apply (simp add: is_ub_lub)
huffman@29130
   102
 apply (frule ub_rangeD [where i=arbitrary])
huffman@31076
   103
 apply (erule Inl_belowE, simp)
huffman@29130
   104
 apply (erule is_lub_lub)
huffman@29130
   105
 apply (rule ub_rangeI)
huffman@29130
   106
 apply (drule ub_rangeD, simp)
huffman@29130
   107
done
huffman@29130
   108
huffman@29130
   109
lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
huffman@29130
   110
 apply (rule is_lubI)
huffman@29130
   111
  apply (rule ub_rangeI)
huffman@29130
   112
  apply (simp add: is_ub_lub)
huffman@29130
   113
 apply (frule ub_rangeD [where i=arbitrary])
huffman@31076
   114
 apply (erule Inr_belowE, simp)
huffman@29130
   115
 apply (erule is_lub_lub)
huffman@29130
   116
 apply (rule ub_rangeI)
huffman@29130
   117
 apply (drule ub_rangeD, simp)
huffman@29130
   118
done
huffman@29130
   119
huffman@29130
   120
instance "+" :: (cpo, cpo) cpo
huffman@29130
   121
 apply intro_classes
huffman@29130
   122
 apply (erule sum_chain_cases, safe)
huffman@29130
   123
  apply (rule exI)
huffman@29130
   124
  apply (rule is_lub_Inl)
huffman@29130
   125
  apply (erule cpo_lubI)
huffman@29130
   126
 apply (rule exI)
huffman@29130
   127
 apply (rule is_lub_Inr)
huffman@29130
   128
 apply (erule cpo_lubI)
huffman@29130
   129
done
huffman@29130
   130
huffman@29130
   131
subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
huffman@29130
   132
huffman@29130
   133
lemma cont_Inl: "cont Inl"
huffman@31041
   134
by (intro contI is_lub_Inl cpo_lubI)
huffman@29130
   135
huffman@29130
   136
lemma cont_Inr: "cont Inr"
huffman@31041
   137
by (intro contI is_lub_Inr cpo_lubI)
huffman@31041
   138
huffman@31041
   139
lemmas cont2cont_Inl [cont2cont] = cont_compose [OF cont_Inl]
huffman@31041
   140
lemmas cont2cont_Inr [cont2cont] = cont_compose [OF cont_Inr]
huffman@29130
   141
huffman@29130
   142
lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
huffman@29130
   143
lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
huffman@29130
   144
huffman@29130
   145
lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
huffman@29130
   146
lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
huffman@29130
   147
huffman@29130
   148
lemma cont_sum_case1:
huffman@29130
   149
  assumes f: "\<And>a. cont (\<lambda>x. f x a)"
huffman@29130
   150
  assumes g: "\<And>b. cont (\<lambda>x. g x b)"
huffman@29130
   151
  shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
huffman@29130
   152
by (induct y, simp add: f, simp add: g)
huffman@29130
   153
huffman@29130
   154
lemma cont_sum_case2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (sum_case f g)"
huffman@29130
   155
apply (rule contI)
huffman@29130
   156
apply (erule sum_chain_cases)
huffman@29130
   157
apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
huffman@29130
   158
apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
huffman@29130
   159
done
huffman@29130
   160
huffman@31041
   161
lemma cont2cont_sum_case:
huffman@29130
   162
  assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
huffman@29130
   163
  assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
huffman@29130
   164
  assumes h: "cont (\<lambda>x. h x)"
huffman@29130
   165
  shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
huffman@31041
   166
apply (rule cont_apply [OF h])
huffman@31041
   167
apply (rule cont_sum_case2 [OF f2 g2])
huffman@29130
   168
apply (rule cont_sum_case1 [OF f1 g1])
huffman@29130
   169
done
huffman@29130
   170
huffman@31041
   171
lemma cont2cont_sum_case' [cont2cont]:
huffman@31041
   172
  assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
huffman@31041
   173
  assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
huffman@31041
   174
  assumes h: "cont (\<lambda>x. h x)"
huffman@31041
   175
  shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
huffman@31041
   176
proof -
huffman@31041
   177
  note f1 = f [THEN cont_fst_snd_D1]
huffman@31041
   178
  note f2 = f [THEN cont_fst_snd_D2]
huffman@31041
   179
  note g1 = g [THEN cont_fst_snd_D1]
huffman@31041
   180
  note g2 = g [THEN cont_fst_snd_D2]
huffman@31041
   181
  show ?thesis
huffman@31041
   182
    apply (rule cont_apply [OF h])
huffman@31041
   183
    apply (rule cont_sum_case2 [OF f2 g2])
huffman@31041
   184
    apply (rule cont_sum_case1 [OF f1 g1])
huffman@31041
   185
    done
huffman@31041
   186
qed
huffman@31041
   187
huffman@29130
   188
subsection {* Compactness and chain-finiteness *}
huffman@29130
   189
huffman@29130
   190
lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
huffman@29130
   191
apply (rule compactI2)
huffman@29130
   192
apply (erule sum_chain_cases, safe)
huffman@29130
   193
apply (simp add: lub_Inl)
huffman@29130
   194
apply (erule (2) compactD2)
huffman@29130
   195
apply (simp add: lub_Inr)
huffman@29130
   196
done
huffman@29130
   197
huffman@29130
   198
lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)"
huffman@29130
   199
apply (rule compactI2)
huffman@29130
   200
apply (erule sum_chain_cases, safe)
huffman@29130
   201
apply (simp add: lub_Inl)
huffman@29130
   202
apply (simp add: lub_Inr)
huffman@29130
   203
apply (erule (2) compactD2)
huffman@29130
   204
done
huffman@29130
   205
huffman@29130
   206
lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a"
huffman@29130
   207
unfolding compact_def
huffman@29130
   208
by (drule adm_subst [OF cont_Inl], simp)
huffman@29130
   209
huffman@29130
   210
lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a"
huffman@29130
   211
unfolding compact_def
huffman@29130
   212
by (drule adm_subst [OF cont_Inr], simp)
huffman@29130
   213
huffman@29130
   214
lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a"
huffman@29130
   215
by (safe elim!: compact_Inl compact_Inl_rev)
huffman@29130
   216
huffman@29130
   217
lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
huffman@29130
   218
by (safe elim!: compact_Inr compact_Inr_rev)
huffman@29130
   219
huffman@29130
   220
instance "+" :: (chfin, chfin) chfin
huffman@29130
   221
apply intro_classes
huffman@29130
   222
apply (erule compact_imp_max_in_chain)
huffman@29130
   223
apply (case_tac "\<Squnion>i. Y i", simp_all)
huffman@29130
   224
done
huffman@29130
   225
huffman@29130
   226
instance "+" :: (finite_po, finite_po) finite_po ..
huffman@29130
   227
huffman@29130
   228
instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
huffman@31076
   229
by intro_classes (simp add: below_sum_def split: sum.split)
huffman@29130
   230
huffman@29130
   231
subsection {* Sum type is a bifinite domain *}
huffman@29130
   232
huffman@29130
   233
instantiation "+" :: (profinite, profinite) profinite
huffman@29130
   234
begin
huffman@29130
   235
huffman@29130
   236
definition
huffman@29130
   237
  approx_sum_def: "approx =
huffman@29130
   238
    (\<lambda>n. \<Lambda> x. case x of Inl a \<Rightarrow> Inl (approx n\<cdot>a) | Inr b \<Rightarrow> Inr (approx n\<cdot>b))"
huffman@29130
   239
huffman@29130
   240
lemma approx_Inl [simp]: "approx n\<cdot>(Inl x) = Inl (approx n\<cdot>x)"
huffman@29130
   241
  unfolding approx_sum_def by simp
huffman@29130
   242
huffman@29130
   243
lemma approx_Inr [simp]: "approx n\<cdot>(Inr x) = Inr (approx n\<cdot>x)"
huffman@29130
   244
  unfolding approx_sum_def by simp
huffman@29130
   245
huffman@29130
   246
instance proof
huffman@29130
   247
  fix i :: nat and x :: "'a + 'b"
huffman@29130
   248
  show "chain (approx :: nat \<Rightarrow> 'a + 'b \<rightarrow> 'a + 'b)"
huffman@29130
   249
    unfolding approx_sum_def
huffman@29130
   250
    by (rule ch2ch_LAM, case_tac x, simp_all)
huffman@29130
   251
  show "(\<Squnion>i. approx i\<cdot>x) = x"
huffman@29130
   252
    by (induct x, simp_all add: lub_Inl lub_Inr)
huffman@29130
   253
  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
huffman@29130
   254
    by (induct x, simp_all)
huffman@29130
   255
  have "{x::'a + 'b. approx i\<cdot>x = x} \<subseteq>
huffman@29130
   256
        {x::'a. approx i\<cdot>x = x} <+> {x::'b. approx i\<cdot>x = x}"
huffman@29130
   257
    by (rule subsetI, case_tac x, simp_all add: InlI InrI)
huffman@29130
   258
  thus "finite {x::'a + 'b. approx i\<cdot>x = x}"
huffman@29130
   259
    by (rule finite_subset,
huffman@29130
   260
        intro finite_Plus finite_fixes_approx)
huffman@29130
   261
qed
huffman@29130
   262
huffman@29130
   263
end
huffman@29130
   264
huffman@29130
   265
end