src/HOLCF/Library/List_Cpo.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 39968 d841744718fe
child 40771 1c6f7d4b110e
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
huffman@39143
     1
(*  Title:      HOLCF/Library/List_Cpo.thy
huffman@39143
     2
    Author:     Brian Huffman
huffman@39143
     3
*)
huffman@39143
     4
huffman@39143
     5
header {* Lists as a complete partial order *}
huffman@39143
     6
huffman@39143
     7
theory List_Cpo
huffman@39143
     8
imports HOLCF
huffman@39143
     9
begin
huffman@39143
    10
huffman@39143
    11
subsection {* Lists are a partial order *}
huffman@39143
    12
huffman@39143
    13
instantiation list :: (po) po
huffman@39143
    14
begin
huffman@39143
    15
huffman@39143
    16
definition
huffman@39143
    17
  "xs \<sqsubseteq> ys \<longleftrightarrow> list_all2 (op \<sqsubseteq>) xs ys"
huffman@39143
    18
huffman@39143
    19
instance proof
huffman@39143
    20
  fix xs :: "'a list"
huffman@39143
    21
  from below_refl show "xs \<sqsubseteq> xs"
huffman@39143
    22
    unfolding below_list_def
huffman@39143
    23
    by (rule list_all2_refl)
huffman@39143
    24
next
huffman@39143
    25
  fix xs ys zs :: "'a list"
huffman@39143
    26
  assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> zs"
huffman@39143
    27
  with below_trans show "xs \<sqsubseteq> zs"
huffman@39143
    28
    unfolding below_list_def
huffman@39143
    29
    by (rule list_all2_trans)
huffman@39143
    30
next
huffman@39143
    31
  fix xs ys zs :: "'a list"
huffman@39143
    32
  assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> xs"
huffman@39143
    33
  with below_antisym show "xs = ys"
huffman@39143
    34
    unfolding below_list_def
huffman@39143
    35
    by (rule list_all2_antisym)
huffman@39143
    36
qed
huffman@39143
    37
huffman@39143
    38
end
huffman@39143
    39
huffman@39143
    40
lemma below_list_simps [simp]:
huffman@39143
    41
  "[] \<sqsubseteq> []"
huffman@39143
    42
  "x # xs \<sqsubseteq> y # ys \<longleftrightarrow> x \<sqsubseteq> y \<and> xs \<sqsubseteq> ys"
huffman@39143
    43
  "\<not> [] \<sqsubseteq> y # ys"
huffman@39143
    44
  "\<not> x # xs \<sqsubseteq> []"
huffman@39143
    45
by (simp_all add: below_list_def)
huffman@39143
    46
huffman@39143
    47
lemma Nil_below_iff [simp]: "[] \<sqsubseteq> xs \<longleftrightarrow> xs = []"
huffman@39143
    48
by (cases xs, simp_all)
huffman@39143
    49
huffman@39143
    50
lemma below_Nil_iff [simp]: "xs \<sqsubseteq> [] \<longleftrightarrow> xs = []"
huffman@39143
    51
by (cases xs, simp_all)
huffman@39143
    52
huffman@39966
    53
lemma list_below_induct [consumes 1, case_names Nil Cons]:
huffman@39966
    54
  assumes "xs \<sqsubseteq> ys"
huffman@39966
    55
  assumes 1: "P [] []"
huffman@39966
    56
  assumes 2: "\<And>x y xs ys. \<lbrakk>x \<sqsubseteq> y; xs \<sqsubseteq> ys; P xs ys\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)"
huffman@39966
    57
  shows "P xs ys"
huffman@39966
    58
using `xs \<sqsubseteq> ys`
huffman@39966
    59
proof (induct xs arbitrary: ys)
huffman@39966
    60
  case Nil thus ?case by (simp add: 1)
huffman@39966
    61
next
huffman@39966
    62
  case (Cons x xs) thus ?case by (cases ys, simp_all add: 2)
huffman@39966
    63
qed
huffman@39966
    64
huffman@39966
    65
lemma list_below_cases:
huffman@39966
    66
  assumes "xs \<sqsubseteq> ys"
huffman@39966
    67
  obtains "xs = []" and "ys = []" |
huffman@39966
    68
    x y xs' ys' where "xs = x # xs'" and "ys = y # ys'"
huffman@39966
    69
using assms by (cases xs, simp, cases ys, auto)
huffman@39966
    70
huffman@39143
    71
text "Thanks to Joachim Breitner"
huffman@39143
    72
huffman@39143
    73
lemma list_Cons_below:
huffman@39143
    74
  assumes "a # as \<sqsubseteq> xs"
huffman@39143
    75
  obtains b and bs where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = b # bs"
huffman@39143
    76
  using assms by (cases xs, auto)
huffman@39143
    77
huffman@39143
    78
lemma list_below_Cons:
huffman@39143
    79
  assumes "xs \<sqsubseteq> b # bs"
huffman@39143
    80
  obtains a and as where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = a # as"
huffman@39143
    81
  using assms by (cases xs, auto)
huffman@39143
    82
huffman@39143
    83
lemma hd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> hd xs \<sqsubseteq> hd ys"
huffman@39143
    84
by (cases xs, simp, cases ys, simp, simp)
huffman@39143
    85
huffman@39143
    86
lemma tl_mono: "xs \<sqsubseteq> ys \<Longrightarrow> tl xs \<sqsubseteq> tl ys"
huffman@39143
    87
by (cases xs, simp, cases ys, simp, simp)
huffman@39143
    88
huffman@39143
    89
lemma ch2ch_hd [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. hd (S i))"
huffman@39143
    90
by (rule chainI, rule hd_mono, erule chainE)
huffman@39143
    91
huffman@39143
    92
lemma ch2ch_tl [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. tl (S i))"
huffman@39143
    93
by (rule chainI, rule tl_mono, erule chainE)
huffman@39143
    94
huffman@39143
    95
lemma below_same_length: "xs \<sqsubseteq> ys \<Longrightarrow> length xs = length ys"
huffman@39143
    96
unfolding below_list_def by (rule list_all2_lengthD)
huffman@39143
    97
huffman@39966
    98
lemma list_chain_induct [consumes 1, case_names Nil Cons]:
huffman@39966
    99
  assumes "chain S"
huffman@39966
   100
  assumes 1: "P (\<lambda>i. [])"
huffman@39966
   101
  assumes 2: "\<And>A B. chain A \<Longrightarrow> chain B \<Longrightarrow> P B \<Longrightarrow> P (\<lambda>i. A i # B i)"
huffman@39966
   102
  shows "P S"
huffman@39966
   103
using `chain S`
huffman@39966
   104
proof (induct "S 0" arbitrary: S)
huffman@39966
   105
  case Nil
huffman@39966
   106
  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`])
huffman@39966
   107
  with Nil have "\<forall>i. S i = []" by simp
huffman@39966
   108
  thus ?case by (simp add: 1)
huffman@39966
   109
next
huffman@39966
   110
  case (Cons x xs)
huffman@39966
   111
  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`])
huffman@39966
   112
  hence *: "\<forall>i. S i \<noteq> []" by (rule all_forward, insert Cons) auto
huffman@39966
   113
  have "chain (\<lambda>i. hd (S i))" and "chain (\<lambda>i. tl (S i))"
huffman@39966
   114
    using `chain S` by simp_all
huffman@39966
   115
  moreover have "P (\<lambda>i. tl (S i))"
huffman@39966
   116
    using `chain S` and `x # xs = S 0` [symmetric]
huffman@39966
   117
    by (simp add: Cons(1))
huffman@39966
   118
  ultimately have "P (\<lambda>i. hd (S i) # tl (S i))"
huffman@39966
   119
    by (rule 2)
huffman@39966
   120
  thus "P S" by (simp add: *)
huffman@39966
   121
qed
huffman@39966
   122
huffman@39143
   123
lemma list_chain_cases:
huffman@39143
   124
  assumes S: "chain S"
huffman@39966
   125
  obtains "S = (\<lambda>i. [])" |
huffman@39966
   126
    A B where "chain A" and "chain B" and "S = (\<lambda>i. A i # B i)"
huffman@39966
   127
using S by (induct rule: list_chain_induct) simp_all
huffman@39143
   128
huffman@39143
   129
subsection {* Lists are a complete partial order *}
huffman@39143
   130
huffman@39143
   131
lemma is_lub_Cons:
huffman@39143
   132
  assumes A: "range A <<| x"
huffman@39143
   133
  assumes B: "range B <<| xs"
huffman@39143
   134
  shows "range (\<lambda>i. A i # B i) <<| x # xs"
huffman@39143
   135
using assms
huffman@39968
   136
unfolding is_lub_def is_ub_def
huffman@39143
   137
by (clarsimp, case_tac u, simp_all)
huffman@39143
   138
huffman@39143
   139
instance list :: (cpo) cpo
huffman@39143
   140
proof
huffman@39143
   141
  fix S :: "nat \<Rightarrow> 'a list"
huffman@39966
   142
  assume "chain S" thus "\<exists>x. range S <<| x"
huffman@39966
   143
  proof (induct rule: list_chain_induct)
huffman@39966
   144
    case Nil thus ?case by (auto intro: lub_const)
huffman@39966
   145
  next
huffman@39966
   146
    case (Cons A B) thus ?case by (auto intro: is_lub_Cons cpo_lubI)
huffman@39966
   147
  qed
huffman@39143
   148
qed
huffman@39143
   149
huffman@39143
   150
subsection {* Continuity of list operations *}
huffman@39143
   151
huffman@39143
   152
lemma cont2cont_Cons [simp, cont2cont]:
huffman@39143
   153
  assumes f: "cont (\<lambda>x. f x)"
huffman@39143
   154
  assumes g: "cont (\<lambda>x. g x)"
huffman@39143
   155
  shows "cont (\<lambda>x. f x # g x)"
huffman@39143
   156
apply (rule contI)
huffman@39143
   157
apply (rule is_lub_Cons)
huffman@39143
   158
apply (erule contE [OF f])
huffman@39143
   159
apply (erule contE [OF g])
huffman@39143
   160
done
huffman@39143
   161
huffman@39143
   162
lemma lub_Cons:
huffman@39143
   163
  fixes A :: "nat \<Rightarrow> 'a::cpo"
huffman@39143
   164
  assumes A: "chain A" and B: "chain B"
huffman@39143
   165
  shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)"
huffman@39143
   166
by (intro thelubI is_lub_Cons cpo_lubI A B)
huffman@39143
   167
huffman@39143
   168
lemma cont2cont_list_case:
huffman@39143
   169
  assumes f: "cont (\<lambda>x. f x)"
huffman@39143
   170
  assumes g: "cont (\<lambda>x. g x)"
huffman@39143
   171
  assumes h1: "\<And>y ys. cont (\<lambda>x. h x y ys)"
huffman@39143
   172
  assumes h2: "\<And>x ys. cont (\<lambda>y. h x y ys)"
huffman@39143
   173
  assumes h3: "\<And>x y. cont (\<lambda>ys. h x y ys)"
huffman@39143
   174
  shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
huffman@39143
   175
apply (rule cont_apply [OF f])
huffman@39143
   176
apply (rule contI)
huffman@39143
   177
apply (erule list_chain_cases)
huffman@39143
   178
apply (simp add: lub_const)
huffman@39143
   179
apply (simp add: lub_Cons)
huffman@39143
   180
apply (simp add: cont2contlubE [OF h2])
huffman@39143
   181
apply (simp add: cont2contlubE [OF h3])
huffman@39143
   182
apply (simp add: diag_lub ch2ch_cont [OF h2] ch2ch_cont [OF h3])
huffman@39143
   183
apply (rule cpo_lubI, rule chainI, rule below_trans)
huffman@39143
   184
apply (erule cont2monofunE [OF h2 chainE])
huffman@39143
   185
apply (erule cont2monofunE [OF h3 chainE])
huffman@39143
   186
apply (case_tac y, simp_all add: g h1)
huffman@39143
   187
done
huffman@39143
   188
huffman@39143
   189
lemma cont2cont_list_case' [simp, cont2cont]:
huffman@39143
   190
  assumes f: "cont (\<lambda>x. f x)"
huffman@39143
   191
  assumes g: "cont (\<lambda>x. g x)"
huffman@39143
   192
  assumes h: "cont (\<lambda>p. h (fst p) (fst (snd p)) (snd (snd p)))"
huffman@39143
   193
  shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
huffman@39808
   194
using assms by (simp add: cont2cont_list_case prod_cont_iff)
huffman@39143
   195
huffman@39143
   196
text {* The simple version (due to Joachim Breitner) is needed if the
huffman@39143
   197
  element type of the list is not a cpo. *}
huffman@39143
   198
huffman@39143
   199
lemma cont2cont_list_case_simple [simp, cont2cont]:
huffman@39143
   200
  assumes "cont (\<lambda>x. f1 x)"
huffman@39143
   201
  assumes "\<And>y ys. cont (\<lambda>x. f2 x y ys)"
huffman@39143
   202
  shows "cont (\<lambda>x. case l of [] \<Rightarrow> f1 x | y # ys \<Rightarrow> f2 x y ys)"
huffman@39143
   203
using assms by (cases l) auto
huffman@39143
   204
huffman@39966
   205
text {* Lemma for proving continuity of recursive list functions: *}
huffman@39966
   206
huffman@39966
   207
lemma list_contI:
huffman@39966
   208
  fixes f :: "'a::cpo list \<Rightarrow> 'b::cpo"
huffman@39966
   209
  assumes f: "\<And>x xs. f (x # xs) = g x xs (f xs)"
huffman@39966
   210
  assumes g1: "\<And>xs y. cont (\<lambda>x. g x xs y)"
huffman@39966
   211
  assumes g2: "\<And>x y. cont (\<lambda>xs. g x xs y)"
huffman@39966
   212
  assumes g3: "\<And>x xs. cont (\<lambda>y. g x xs y)"
huffman@39966
   213
  shows "cont f"
huffman@39966
   214
proof (rule contI2)
huffman@39966
   215
  obtain h where h: "\<And>x xs y. g x xs y = h\<cdot>x\<cdot>xs\<cdot>y"
huffman@39966
   216
  proof
huffman@39966
   217
    fix x xs y show "g x xs y = (\<Lambda> x xs y. g x xs y)\<cdot>x\<cdot>xs\<cdot>y"
huffman@39966
   218
    by (simp add: cont2cont_LAM g1 g2 g3)
huffman@39966
   219
  qed
huffman@39966
   220
  show mono: "monofun f"
huffman@39966
   221
    apply (rule monofunI)
huffman@39966
   222
    apply (erule list_below_induct)
huffman@39966
   223
    apply simp
huffman@39966
   224
    apply (simp add: f h monofun_cfun)
huffman@39966
   225
    done
huffman@39966
   226
  fix Y :: "nat \<Rightarrow> 'a list"
huffman@39966
   227
  assume "chain Y" thus "f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
huffman@39966
   228
    apply (induct rule: list_chain_induct)
huffman@39966
   229
    apply simp
huffman@39966
   230
    apply (simp add: lub_Cons f h)
huffman@39966
   231
    apply (simp add: contlub_cfun [symmetric] ch2ch_monofun [OF mono])
huffman@39966
   232
    apply (simp add: monofun_cfun)
huffman@39966
   233
    done
huffman@39966
   234
qed
huffman@39966
   235
huffman@39143
   236
text {* There are probably lots of other list operations that also
huffman@39143
   237
deserve to have continuity lemmas.  I'll add more as they are
huffman@39143
   238
needed. *}
huffman@39143
   239
huffman@39212
   240
subsection {* Using lists with fixrec *}
huffman@39212
   241
huffman@39212
   242
definition
huffman@39212
   243
  match_Nil :: "'a::cpo list \<rightarrow> 'b match \<rightarrow> 'b match"
huffman@39212
   244
where
huffman@39212
   245
  "match_Nil = (\<Lambda> xs k. case xs of [] \<Rightarrow> k | y # ys \<Rightarrow> Fixrec.fail)"
huffman@39212
   246
huffman@39212
   247
definition
huffman@39212
   248
  match_Cons :: "'a::cpo list \<rightarrow> ('a \<rightarrow> 'a list \<rightarrow> 'b match) \<rightarrow> 'b match"
huffman@39212
   249
where
huffman@39212
   250
  "match_Cons = (\<Lambda> xs k. case xs of [] \<Rightarrow> Fixrec.fail | y # ys \<Rightarrow> k\<cdot>y\<cdot>ys)"
huffman@39212
   251
huffman@39212
   252
lemma match_Nil_simps [simp]:
huffman@39212
   253
  "match_Nil\<cdot>[]\<cdot>k = k"
huffman@39212
   254
  "match_Nil\<cdot>(x # xs)\<cdot>k = Fixrec.fail"
huffman@39212
   255
unfolding match_Nil_def by simp_all
huffman@39212
   256
huffman@39212
   257
lemma match_Cons_simps [simp]:
huffman@39212
   258
  "match_Cons\<cdot>[]\<cdot>k = Fixrec.fail"
huffman@39212
   259
  "match_Cons\<cdot>(x # xs)\<cdot>k = k\<cdot>x\<cdot>xs"
huffman@39212
   260
unfolding match_Cons_def by simp_all
huffman@39212
   261
huffman@39212
   262
setup {*
huffman@39212
   263
  Fixrec.add_matchers
huffman@39212
   264
    [ (@{const_name Nil}, @{const_name match_Nil}),
huffman@39212
   265
      (@{const_name Cons}, @{const_name match_Cons}) ]
huffman@39212
   266
*}
huffman@39212
   267
huffman@39143
   268
end