src/HOL/HOLCF/Up.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 63040 eb4ddd18d635
child 67312 0d25e02759b7
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Up.thy
huffman@40502
     2
    Author:     Franz Regensburger
huffman@40502
     3
    Author:     Brian Huffman
huffman@15576
     4
*)
huffman@15576
     5
wenzelm@62175
     6
section \<open>The type of lifted values\<close>
huffman@15576
     7
huffman@15577
     8
theory Up
huffman@40502
     9
imports Cfun
huffman@15577
    10
begin
huffman@15576
    11
wenzelm@36452
    12
default_sort cpo
huffman@15599
    13
wenzelm@62175
    14
subsection \<open>Definition of new type for lifting\<close>
huffman@15576
    15
wenzelm@61998
    16
datatype 'a u  ("(_\<^sub>\<bottom>)" [1000] 999) = Ibottom | Iup 'a
huffman@18290
    17
haftmann@34941
    18
primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
haftmann@34941
    19
    "Ifup f Ibottom = \<bottom>"
haftmann@34941
    20
 |  "Ifup f (Iup x) = f\<cdot>x"
huffman@15576
    21
wenzelm@62175
    22
subsection \<open>Ordering on lifted cpo\<close>
huffman@15593
    23
huffman@31076
    24
instantiation u :: (cpo) below
huffman@25787
    25
begin
huffman@15576
    26
huffman@25787
    27
definition
huffman@31076
    28
  below_up_def:
huffman@16753
    29
    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
huffman@16753
    30
      (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
huffman@15576
    31
huffman@25787
    32
instance ..
huffman@25787
    33
end
huffman@25787
    34
huffman@16753
    35
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
huffman@31076
    36
by (simp add: below_up_def)
huffman@15576
    37
huffman@41182
    38
lemma not_Iup_below [iff]: "Iup x \<notsqsubseteq> Ibottom"
huffman@31076
    39
by (simp add: below_up_def)
huffman@15576
    40
huffman@31076
    41
lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
huffman@31076
    42
by (simp add: below_up_def)
huffman@15576
    43
wenzelm@62175
    44
subsection \<open>Lifted cpo is a partial order\<close>
huffman@15576
    45
huffman@15599
    46
instance u :: (cpo) po
huffman@25787
    47
proof
huffman@25787
    48
  fix x :: "'a u"
huffman@25787
    49
  show "x \<sqsubseteq> x"
huffman@31076
    50
    unfolding below_up_def by (simp split: u.split)
huffman@25787
    51
next
huffman@25787
    52
  fix x y :: "'a u"
huffman@25787
    53
  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
huffman@31076
    54
    unfolding below_up_def
huffman@31076
    55
    by (auto split: u.split_asm intro: below_antisym)
huffman@25787
    56
next
huffman@25787
    57
  fix x y z :: "'a u"
huffman@25787
    58
  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
huffman@31076
    59
    unfolding below_up_def
huffman@31076
    60
    by (auto split: u.split_asm intro: below_trans)
huffman@25787
    61
qed
huffman@15576
    62
wenzelm@62175
    63
subsection \<open>Lifted cpo is a cpo\<close>
huffman@15593
    64
huffman@16319
    65
lemma is_lub_Iup:
huffman@16319
    66
  "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
huffman@40084
    67
unfolding is_lub_def is_ub_def ball_simps
huffman@40084
    68
by (auto simp add: below_up_def split: u.split)
huffman@15599
    69
huffman@17838
    70
lemma up_chain_lemma:
huffman@40084
    71
  assumes Y: "chain Y" obtains "\<forall>i. Y i = Ibottom"
huffman@40084
    72
  | A k where "\<forall>i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
huffman@40084
    73
proof (cases "\<exists>k. Y k \<noteq> Ibottom")
huffman@40084
    74
  case True
huffman@40084
    75
  then obtain k where k: "Y k \<noteq> Ibottom" ..
wenzelm@63040
    76
  define A where "A i = (THE a. Iup a = Y (i + k))" for i
huffman@40084
    77
  have Iup_A: "\<forall>i. Iup (A i) = Y (i + k)"
huffman@40084
    78
  proof
huffman@40084
    79
    fix i :: nat
huffman@40084
    80
    from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono)
huffman@40084
    81
    with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k", auto)
huffman@40084
    82
    thus "Iup (A i) = Y (i + k)"
huffman@40084
    83
      by (cases "Y (i + k)", simp_all add: A_def)
huffman@40084
    84
  qed
huffman@40084
    85
  from Y have chain_A: "chain A"
huffman@40084
    86
    unfolding chain_def Iup_below [symmetric]
huffman@40084
    87
    by (simp add: Iup_A)
huffman@40084
    88
  hence "range A <<| (\<Squnion>i. A i)"
huffman@40084
    89
    by (rule cpo_lubI)
huffman@40084
    90
  hence "range (\<lambda>i. Iup (A i)) <<| Iup (\<Squnion>i. A i)"
huffman@40084
    91
    by (rule is_lub_Iup)
huffman@40084
    92
  hence "range (\<lambda>i. Y (i + k)) <<| Iup (\<Squnion>i. A i)"
huffman@40084
    93
    by (simp only: Iup_A)
huffman@40084
    94
  hence "range (\<lambda>i. Y i) <<| Iup (\<Squnion>i. A i)"
huffman@40084
    95
    by (simp only: is_lub_range_shift [OF Y])
huffman@40084
    96
  with Iup_A chain_A show ?thesis ..
huffman@40084
    97
next
huffman@40084
    98
  case False
huffman@40084
    99
  then have "\<forall>i. Y i = Ibottom" by simp
huffman@40084
   100
  then show ?thesis ..
huffman@40084
   101
qed
huffman@15576
   102
huffman@15599
   103
instance u :: (cpo) cpo
huffman@40084
   104
proof
huffman@40084
   105
  fix S :: "nat \<Rightarrow> 'a u"
huffman@40084
   106
  assume S: "chain S"
huffman@40084
   107
  thus "\<exists>x. range (\<lambda>i. S i) <<| x"
huffman@40084
   108
  proof (rule up_chain_lemma)
huffman@40084
   109
    assume "\<forall>i. S i = Ibottom"
huffman@40084
   110
    hence "range (\<lambda>i. S i) <<| Ibottom"
huffman@40771
   111
      by (simp add: is_lub_const)
huffman@40084
   112
    thus ?thesis ..
huffman@40084
   113
  next
huffman@40085
   114
    fix A :: "nat \<Rightarrow> 'a"
huffman@40085
   115
    assume "range S <<| Iup (\<Squnion>i. A i)"
huffman@40084
   116
    thus ?thesis ..
huffman@40084
   117
  qed
huffman@40084
   118
qed
huffman@15593
   119
wenzelm@62175
   120
subsection \<open>Lifted cpo is pointed\<close>
huffman@15576
   121
huffman@15599
   122
instance u :: (cpo) pcpo
huffman@40084
   123
by intro_classes fast
huffman@15593
   124
wenzelm@62175
   125
text \<open>for compatibility with old HOLCF-Version\<close>
huffman@16753
   126
lemma inst_up_pcpo: "\<bottom> = Ibottom"
huffman@41430
   127
by (rule minimal_up [THEN bottomI, symmetric])
huffman@15593
   128
wenzelm@62175
   129
subsection \<open>Continuity of \emph{Iup} and \emph{Ifup}\<close>
huffman@15593
   130
wenzelm@62175
   131
text \<open>continuity for @{term Iup}\<close>
huffman@15576
   132
huffman@16319
   133
lemma cont_Iup: "cont Iup"
huffman@16215
   134
apply (rule contI)
huffman@15599
   135
apply (rule is_lub_Iup)
huffman@26027
   136
apply (erule cpo_lubI)
huffman@15576
   137
done
huffman@15576
   138
wenzelm@62175
   139
text \<open>continuity for @{term Ifup}\<close>
huffman@15576
   140
huffman@16319
   141
lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
huffman@16753
   142
by (induct x, simp_all)
huffman@15576
   143
huffman@16319
   144
lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
huffman@16319
   145
apply (rule monofunI)
huffman@16753
   146
apply (case_tac x, simp)
huffman@16753
   147
apply (case_tac y, simp)
huffman@16319
   148
apply (simp add: monofun_cfun_arg)
huffman@15576
   149
done
huffman@15576
   150
huffman@16319
   151
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
huffman@40084
   152
proof (rule contI2)
huffman@40084
   153
  fix Y assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))"
huffman@40084
   154
  from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))"
huffman@40084
   155
  proof (rule up_chain_lemma)
huffman@40084
   156
    fix A and k
huffman@40084
   157
    assume A: "\<forall>i. Iup (A i) = Y (i + k)"
huffman@40084
   158
    assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
huffman@40084
   159
    hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
huffman@40771
   160
      by (simp add: lub_eqI contlub_cfun_arg)
huffman@40084
   161
    also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
huffman@40084
   162
      by (simp add: A)
huffman@40084
   163
    also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
huffman@40084
   164
      using Y' by (rule lub_range_shift)
huffman@40084
   165
    finally show ?thesis by simp
huffman@40084
   166
  qed simp
huffman@40084
   167
qed (rule monofun_Ifup2)
huffman@15576
   168
wenzelm@62175
   169
subsection \<open>Continuous versions of constants\<close>
huffman@15576
   170
wenzelm@25131
   171
definition
wenzelm@25131
   172
  up  :: "'a \<rightarrow> 'a u" where
wenzelm@25131
   173
  "up = (\<Lambda> x. Iup x)"
huffman@16319
   174
wenzelm@25131
   175
definition
wenzelm@25131
   176
  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
wenzelm@25131
   177
  "fup = (\<Lambda> f p. Ifup f p)"
huffman@15593
   178
huffman@15593
   179
translations
huffman@26046
   180
  "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
wenzelm@46125
   181
  "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
huffman@26046
   182
  "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
huffman@15593
   183
wenzelm@62175
   184
text \<open>continuous versions of lemmas for @{typ "('a)u"}\<close>
huffman@15576
   185
huffman@16753
   186
lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
huffman@16753
   187
apply (induct z)
huffman@16319
   188
apply (simp add: inst_up_pcpo)
huffman@16319
   189
apply (simp add: up_def cont_Iup)
huffman@15576
   190
done
huffman@15576
   191
huffman@16753
   192
lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
huffman@16319
   193
by (simp add: up_def cont_Iup)
huffman@15576
   194
huffman@16753
   195
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
huffman@16753
   196
by simp
huffman@16319
   197
huffman@17838
   198
lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
huffman@16319
   199
by (simp add: up_def cont_Iup inst_up_pcpo)
huffman@15576
   200
huffman@41182
   201
lemma not_up_less_UU: "up\<cdot>x \<notsqsubseteq> \<bottom>"
huffman@31076
   202
by simp (* FIXME: remove? *)
huffman@15576
   203
huffman@31076
   204
lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
huffman@16319
   205
by (simp add: up_def cont_Iup)
huffman@16319
   206
huffman@35783
   207
lemma upE [case_names bottom up, cases type: u]:
huffman@35783
   208
  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
huffman@25788
   209
apply (cases p)
huffman@16319
   210
apply (simp add: inst_up_pcpo)
huffman@16319
   211
apply (simp add: up_def cont_Iup)
huffman@15576
   212
done
huffman@15576
   213
huffman@35783
   214
lemma up_induct [case_names bottom up, induct type: u]:
huffman@35783
   215
  "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
huffman@25788
   216
by (cases x, simp_all)
huffman@25788
   217
wenzelm@62175
   218
text \<open>lifting preserves chain-finiteness\<close>
huffman@25827
   219
huffman@17838
   220
lemma up_chain_cases:
huffman@40084
   221
  assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
huffman@40084
   222
  | A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)"
huffman@40084
   223
apply (rule up_chain_lemma [OF Y])
huffman@40771
   224
apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
huffman@40084
   225
done
huffman@17838
   226
huffman@25879
   227
lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
huffman@25879
   228
apply (rule compactI2)
huffman@40084
   229
apply (erule up_chain_cases)
huffman@40084
   230
apply simp
huffman@25879
   231
apply (drule (1) compactD2, simp)
huffman@40084
   232
apply (erule exE)
huffman@40084
   233
apply (drule_tac f="up" and x="x" in monofun_cfun_arg)
huffman@40084
   234
apply (simp, erule exI)
huffman@25879
   235
done
huffman@25879
   236
huffman@25879
   237
lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
huffman@25879
   238
unfolding compact_def
huffman@40327
   239
by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp)
huffman@25879
   240
huffman@25879
   241
lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
huffman@25879
   242
by (safe elim!: compact_up compact_upD)
huffman@25879
   243
huffman@25827
   244
instance u :: (chfin) chfin
huffman@25921
   245
apply intro_classes
huffman@25879
   246
apply (erule compact_imp_max_in_chain)
huffman@25898
   247
apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
huffman@17838
   248
done
huffman@17838
   249
wenzelm@62175
   250
text \<open>properties of fup\<close>
huffman@17838
   251
huffman@16319
   252
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
huffman@29530
   253
by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)
huffman@15576
   254
huffman@16319
   255
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
huffman@29530
   256
by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM)
huffman@15576
   257
huffman@16553
   258
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
huffman@25788
   259
by (cases x, simp_all)
huffman@15576
   260
huffman@26962
   261
end