src/HOL/MicroJava/BV/Listn.thy
author haftmann
Tue Jul 28 13:37:08 2009 +0200 (2009-07-28)
changeset 32263 8bc0fd4a23a0
parent 29235 2d62b637fa80
permissions -rw-r--r--
explicit is better than implicit
kleing@12516
     1
(*  Title:      HOL/MicroJava/BV/Listn.thy
kleing@10496
     2
    Author:     Tobias Nipkow
kleing@10496
     3
    Copyright   2000 TUM
kleing@10496
     4
kleing@10496
     5
Lists of a fixed length
kleing@10496
     6
*)
kleing@10496
     7
kleing@12911
     8
header {* \isaheader{Fixed Length Lists} *}
kleing@10496
     9
haftmann@32263
    10
theory Listn
haftmann@32263
    11
imports Err
haftmann@32263
    12
begin
kleing@10496
    13
kleing@10496
    14
constdefs
kleing@10496
    15
kleing@13006
    16
 list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set"
kleing@10496
    17
"list n A == {xs. length xs = n & set xs <= A}"
kleing@10496
    18
kleing@13006
    19
 le :: "'a ord \<Rightarrow> ('a list)ord"
kleing@10496
    20
"le r == list_all2 (%x y. x <=_r y)"
kleing@10496
    21
kleing@13006
    22
syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
kleing@10496
    23
       ("(_ /<=[_] _)" [50, 0, 51] 50)
kleing@13006
    24
syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
kleing@10496
    25
       ("(_ /<[_] _)" [50, 0, 51] 50)
kleing@10496
    26
translations
kleing@10496
    27
 "x <=[r] y" == "x <=_(Listn.le r) y"
kleing@10496
    28
 "x <[r] y"  == "x <_(Listn.le r) y"
kleing@10496
    29
kleing@10496
    30
constdefs
kleing@13006
    31
 map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
kleing@10496
    32
"map2 f == (%xs ys. map (split f) (zip xs ys))"
kleing@10496
    33
kleing@13006
    34
syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
kleing@10496
    35
       ("(_ /+[_] _)" [65, 0, 66] 65)
kleing@10496
    36
translations  "x +[f] y" == "x +_(map2 f) y"
kleing@10496
    37
kleing@13006
    38
consts coalesce :: "'a err list \<Rightarrow> 'a list err"
kleing@10496
    39
primrec
kleing@10496
    40
"coalesce [] = OK[]"
kleing@10496
    41
"coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"
kleing@10496
    42
kleing@10496
    43
constdefs
kleing@13006
    44
 sl :: "nat \<Rightarrow> 'a sl \<Rightarrow> 'a list sl"
kleing@10496
    45
"sl n == %(A,r,f). (list n A, le r, map2 f)"
kleing@10496
    46
kleing@13006
    47
 sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list err"
kleing@10496
    48
"sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
kleing@10496
    49
kleing@13006
    50
 upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl"
kleing@10496
    51
"upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
kleing@10496
    52
kleing@10496
    53
lemmas [simp] = set_update_subsetI
kleing@10496
    54
kleing@10496
    55
lemma unfold_lesub_list:
kleing@10496
    56
  "xs <=[r] ys == Listn.le r xs ys"
kleing@10496
    57
  by (simp add: lesub_def)
kleing@10496
    58
kleing@10496
    59
lemma Nil_le_conv [iff]:
kleing@10496
    60
  "([] <=[r] ys) = (ys = [])"
kleing@10496
    61
apply (unfold lesub_def Listn.le_def)
kleing@10496
    62
apply simp
kleing@10496
    63
done
kleing@10496
    64
kleing@10496
    65
lemma Cons_notle_Nil [iff]: 
kleing@10496
    66
  "~ x#xs <=[r] []"
kleing@10496
    67
apply (unfold lesub_def Listn.le_def)
kleing@10496
    68
apply simp
kleing@10496
    69
done
kleing@10496
    70
kleing@10496
    71
kleing@10496
    72
lemma Cons_le_Cons [iff]:
kleing@10496
    73
  "x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)"
kleing@10496
    74
apply (unfold lesub_def Listn.le_def)
kleing@10496
    75
apply simp
kleing@10496
    76
done
kleing@10496
    77
kleing@10496
    78
lemma Cons_less_Conss [simp]:
kleing@13006
    79
  "order r \<Longrightarrow> 
kleing@10496
    80
  x#xs <_(Listn.le r) y#ys = 
kleing@10496
    81
  (x <_r y & xs <=[r] ys  |  x = y & xs <_(Listn.le r) ys)"
kleing@10496
    82
apply (unfold lesssub_def)
kleing@10496
    83
apply blast
kleing@10496
    84
done  
kleing@10496
    85
kleing@10496
    86
lemma list_update_le_cong:
kleing@13006
    87
  "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]";
kleing@10496
    88
apply (unfold unfold_lesub_list)
kleing@10496
    89
apply (unfold Listn.le_def)
kleing@10496
    90
apply (simp add: list_all2_conv_all_nth nth_list_update)
kleing@10496
    91
done
kleing@10496
    92
kleing@10496
    93
kleing@10496
    94
lemma le_listD:
kleing@13006
    95
  "\<lbrakk> xs <=[r] ys; p < size xs \<rbrakk> \<Longrightarrow> xs!p <=_r ys!p"
kleing@10496
    96
apply (unfold Listn.le_def lesub_def)
kleing@10496
    97
apply (simp add: list_all2_conv_all_nth)
kleing@10496
    98
done
kleing@10496
    99
kleing@10496
   100
lemma le_list_refl:
kleing@13006
   101
  "!x. x <=_r x \<Longrightarrow> xs <=[r] xs"
kleing@10496
   102
apply (unfold unfold_lesub_list)
kleing@10496
   103
apply (simp add: Listn.le_def list_all2_conv_all_nth)
kleing@10496
   104
done
kleing@10496
   105
kleing@10496
   106
lemma le_list_trans:
kleing@13006
   107
  "\<lbrakk> order r; xs <=[r] ys; ys <=[r] zs \<rbrakk> \<Longrightarrow> xs <=[r] zs"
kleing@10496
   108
apply (unfold unfold_lesub_list)
kleing@10496
   109
apply (simp add: Listn.le_def list_all2_conv_all_nth)
kleing@10496
   110
apply clarify
kleing@10496
   111
apply simp
kleing@10496
   112
apply (blast intro: order_trans)
kleing@10496
   113
done
kleing@10496
   114
kleing@10496
   115
lemma le_list_antisym:
kleing@13006
   116
  "\<lbrakk> order r; xs <=[r] ys; ys <=[r] xs \<rbrakk> \<Longrightarrow> xs = ys"
kleing@10496
   117
apply (unfold unfold_lesub_list)
kleing@10496
   118
apply (simp add: Listn.le_def list_all2_conv_all_nth)
kleing@10496
   119
apply (rule nth_equalityI)
kleing@10496
   120
 apply blast
kleing@10496
   121
apply clarify
kleing@10496
   122
apply simp
kleing@10496
   123
apply (blast intro: order_antisym)
kleing@10496
   124
done
kleing@10496
   125
kleing@10496
   126
lemma order_listI [simp, intro!]:
kleing@13006
   127
  "order r \<Longrightarrow> order(Listn.le r)"
haftmann@22068
   128
apply (subst Semilat.order_def)
kleing@10496
   129
apply (blast intro: le_list_refl le_list_trans le_list_antisym
kleing@10496
   130
             dest: order_refl)
kleing@10496
   131
done
kleing@10496
   132
kleing@10496
   133
kleing@10496
   134
lemma lesub_list_impl_same_size [simp]:
kleing@13006
   135
  "xs <=[r] ys \<Longrightarrow> size ys = size xs"  
kleing@10496
   136
apply (unfold Listn.le_def lesub_def)
kleing@10496
   137
apply (simp add: list_all2_conv_all_nth)
kleing@10496
   138
done 
kleing@10496
   139
kleing@10496
   140
lemma lesssub_list_impl_same_size:
kleing@13006
   141
  "xs <_(Listn.le r) ys \<Longrightarrow> size ys = size xs"
kleing@10496
   142
apply (unfold lesssub_def)
kleing@10496
   143
apply auto
kleing@10496
   144
done  
kleing@10496
   145
kleing@13066
   146
lemma le_list_appendI:
kleing@13066
   147
  "\<And>b c d. a <=[r] b \<Longrightarrow> c <=[r] d \<Longrightarrow> a@c <=[r] b@d"
kleing@13066
   148
apply (induct a)
kleing@13066
   149
 apply simp
kleing@13066
   150
apply (case_tac b)
kleing@13066
   151
apply auto
kleing@13066
   152
done
kleing@13066
   153
kleing@13066
   154
lemma le_listI:
kleing@13066
   155
  "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> a!n <=_r b!n) \<Longrightarrow> a <=[r] b"
kleing@13066
   156
  apply (unfold lesub_def Listn.le_def)
kleing@13066
   157
  apply (simp add: list_all2_conv_all_nth)
kleing@13066
   158
  done
kleing@13066
   159
kleing@10496
   160
lemma listI:
kleing@13006
   161
  "\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
kleing@10496
   162
apply (unfold list_def)
kleing@10496
   163
apply blast
kleing@10496
   164
done
kleing@10496
   165
kleing@10496
   166
lemma listE_length [simp]:
kleing@13006
   167
   "xs : list n A \<Longrightarrow> length xs = n"
kleing@10496
   168
apply (unfold list_def)
kleing@10496
   169
apply blast
kleing@10496
   170
done 
kleing@10496
   171
kleing@10496
   172
lemma less_lengthI:
kleing@13006
   173
  "\<lbrakk> xs : list n A; p < n \<rbrakk> \<Longrightarrow> p < length xs"
kleing@10496
   174
  by simp
kleing@10496
   175
kleing@10496
   176
lemma listE_set [simp]:
kleing@13006
   177
  "xs : list n A \<Longrightarrow> set xs <= A"
kleing@10496
   178
apply (unfold list_def)
kleing@10496
   179
apply blast
kleing@10496
   180
done 
kleing@10496
   181
kleing@10496
   182
lemma list_0 [simp]:
kleing@10496
   183
  "list 0 A = {[]}"
kleing@10496
   184
apply (unfold list_def)
kleing@10496
   185
apply auto
kleing@10496
   186
done 
kleing@10496
   187
kleing@10496
   188
lemma in_list_Suc_iff: 
paulson@15341
   189
  "(xs : list (Suc n) A) = (\<exists>y\<in> A. \<exists>ys\<in> list n A. xs = y#ys)"
kleing@10496
   190
apply (unfold list_def)
kleing@10496
   191
apply (case_tac "xs")
kleing@10496
   192
apply auto
kleing@10496
   193
done 
kleing@10496
   194
kleing@10496
   195
lemma Cons_in_list_Suc [iff]:
paulson@15341
   196
  "(x#xs : list (Suc n) A) = (x\<in> A & xs : list n A)";
kleing@10496
   197
apply (simp add: in_list_Suc_iff)
kleing@10496
   198
done 
kleing@10496
   199
kleing@10496
   200
lemma list_not_empty:
paulson@15341
   201
  "\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs : list n A";
kleing@10496
   202
apply (induct "n")
kleing@10496
   203
 apply simp
kleing@10496
   204
apply (simp add: in_list_Suc_iff)
kleing@10496
   205
apply blast
kleing@10496
   206
done
kleing@10496
   207
kleing@10496
   208
kleing@10496
   209
lemma nth_in [rule_format, simp]:
kleing@13006
   210
  "!i n. length xs = n \<longrightarrow> set xs <= A \<longrightarrow> i < n \<longrightarrow> (xs!i) : A"
kleing@10496
   211
apply (induct "xs")
kleing@10496
   212
 apply simp
kleing@10496
   213
apply (simp add: nth_Cons split: nat.split)
kleing@10496
   214
done
kleing@10496
   215
kleing@10496
   216
lemma listE_nth_in:
kleing@13006
   217
  "\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
kleing@10496
   218
  by auto
kleing@10496
   219
kleing@13066
   220
kleing@13066
   221
lemma listn_Cons_Suc [elim!]:
kleing@13066
   222
  "l#xs \<in> list n A \<Longrightarrow> (\<And>n'. n = Suc n' \<Longrightarrow> l \<in> A \<Longrightarrow> xs \<in> list n' A \<Longrightarrow> P) \<Longrightarrow> P"
kleing@13066
   223
  by (cases n) auto
kleing@13066
   224
kleing@13066
   225
lemma listn_appendE [elim!]:
kleing@13066
   226
  "a@b \<in> list n A \<Longrightarrow> (\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P) \<Longrightarrow> P" 
kleing@13066
   227
proof -
kleing@13066
   228
  have "\<And>n. a@b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n=n1+n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A"
kleing@13066
   229
    (is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2")
kleing@13066
   230
  proof (induct a)
kleing@13066
   231
    fix n assume "?list [] n"
kleing@13066
   232
    hence "?P [] n 0 n" by simp
kleing@13066
   233
    thus "\<exists>n1 n2. ?P [] n n1 n2" by fast
kleing@13066
   234
  next
kleing@13066
   235
    fix n l ls
kleing@13066
   236
    assume "?list (l#ls) n"
wenzelm@23464
   237
    then obtain n' where n: "n = Suc n'" "l \<in> A" and list_n': "ls@b \<in> list n' A" by fastsimp
kleing@13066
   238
    assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
wenzelm@23464
   239
    hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" by this (rule list_n')
kleing@13066
   240
    then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
kleing@13066
   241
    with n have "?P (l#ls) n (n1+1) n2" by simp
kleing@13066
   242
    thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
kleing@13066
   243
  qed
kleing@13066
   244
  moreover
kleing@13066
   245
  assume "a@b \<in> list n A" "\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P"
kleing@13066
   246
  ultimately
kleing@13066
   247
  show ?thesis by blast
kleing@13066
   248
qed
kleing@13066
   249
kleing@13066
   250
kleing@10496
   251
lemma listt_update_in_list [simp, intro!]:
paulson@15341
   252
  "\<lbrakk> xs : list n A; x\<in> A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
kleing@10496
   253
apply (unfold list_def)
kleing@10496
   254
apply simp
kleing@10496
   255
done 
kleing@10496
   256
kleing@10496
   257
lemma plus_list_Nil [simp]:
kleing@10496
   258
  "[] +[f] xs = []"
kleing@10496
   259
apply (unfold plussub_def map2_def)
kleing@10496
   260
apply simp
kleing@10496
   261
done 
kleing@10496
   262
kleing@10496
   263
lemma plus_list_Cons [simp]:
kleing@13006
   264
  "(x#xs) +[f] ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x +_f y)#(xs +[f] ys))"
kleing@10496
   265
  by (simp add: plussub_def map2_def split: list.split)
kleing@10496
   266
kleing@10496
   267
lemma length_plus_list [rule_format, simp]:
kleing@10496
   268
  "!ys. length(xs +[f] ys) = min(length xs) (length ys)"
kleing@10496
   269
apply (induct xs)
kleing@10496
   270
 apply simp
kleing@10496
   271
apply clarify
kleing@10496
   272
apply (simp (no_asm_simp) split: list.split)
kleing@10496
   273
done
kleing@10496
   274
kleing@10496
   275
lemma nth_plus_list [rule_format, simp]:
kleing@13006
   276
  "!xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i<n \<longrightarrow> 
kleing@10496
   277
  (xs +[f] ys)!i = (xs!i) +_f (ys!i)"
kleing@10496
   278
apply (induct n)
kleing@10496
   279
 apply simp
kleing@10496
   280
apply clarify
kleing@10496
   281
apply (case_tac xs)
kleing@10496
   282
 apply simp
kleing@10496
   283
apply (force simp add: nth_Cons split: list.split nat.split)
kleing@10496
   284
done
kleing@10496
   285
kleing@10496
   286
haftmann@27681
   287
lemma (in Semilat) plus_list_ub1 [rule_format]:
nipkow@13074
   288
 "\<lbrakk> set xs <= A; set ys <= A; size xs = size ys \<rbrakk> 
kleing@13006
   289
  \<Longrightarrow> xs <=[r] xs +[f] ys"
kleing@10496
   290
apply (unfold unfold_lesub_list)
kleing@10496
   291
apply (simp add: Listn.le_def list_all2_conv_all_nth)
kleing@10496
   292
done
kleing@10496
   293
haftmann@27681
   294
lemma (in Semilat) plus_list_ub2:
nipkow@13074
   295
 "\<lbrakk>set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
kleing@13006
   296
  \<Longrightarrow> ys <=[r] xs +[f] ys"
kleing@10496
   297
apply (unfold unfold_lesub_list)
kleing@10496
   298
apply (simp add: Listn.le_def list_all2_conv_all_nth)
nipkow@13074
   299
done
kleing@10496
   300
haftmann@27681
   301
lemma (in Semilat) plus_list_lub [rule_format]:
nipkow@13074
   302
shows "!xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A 
kleing@13006
   303
  \<longrightarrow> size xs = n & size ys = n \<longrightarrow> 
kleing@13006
   304
  xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
kleing@10496
   305
apply (unfold unfold_lesub_list)
kleing@10496
   306
apply (simp add: Listn.le_def list_all2_conv_all_nth)
nipkow@13074
   307
done
kleing@10496
   308
haftmann@27681
   309
lemma (in Semilat) list_update_incr [rule_format]:
paulson@15341
   310
 "x\<in> A \<Longrightarrow> set xs <= A \<longrightarrow> 
kleing@13006
   311
  (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
kleing@10496
   312
apply (unfold unfold_lesub_list)
kleing@10496
   313
apply (simp add: Listn.le_def list_all2_conv_all_nth)
kleing@10496
   314
apply (induct xs)
kleing@10496
   315
 apply simp
kleing@10496
   316
apply (simp add: in_list_Suc_iff)
kleing@10496
   317
apply clarify
kleing@10496
   318
apply (simp add: nth_Cons split: nat.split)
nipkow@13074
   319
done
kleing@10496
   320
haftmann@32263
   321
lemma equals0I_aux:
haftmann@32263
   322
  "(\<And>y. A y \<Longrightarrow> False) \<Longrightarrow> A = bot_class.bot"
haftmann@32263
   323
  by (rule equals0I) (auto simp add: mem_def)
haftmann@32263
   324
kleing@10496
   325
lemma acc_le_listI [intro!]:
kleing@13006
   326
  "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
kleing@10496
   327
apply (unfold acc_def)
kleing@10496
   328
apply (subgoal_tac
berghofe@22271
   329
 "wfP (SUP n. (\<lambda>ys xs. size xs = n & size ys = n & xs <_(Listn.le r) ys))")
berghofe@22271
   330
 apply (erule wfP_subset)
kleing@10496
   331
 apply (blast intro: lesssub_list_impl_same_size)
berghofe@22271
   332
apply (rule wfP_SUP)
kleing@10496
   333
 prefer 2
kleing@10496
   334
 apply clarify
kleing@10496
   335
 apply (rename_tac m n)
kleing@10496
   336
 apply (case_tac "m=n")
kleing@10496
   337
  apply simp
haftmann@32263
   338
 apply (fast intro!: equals0I_aux dest: not_sym)
kleing@10496
   339
apply clarify
kleing@10496
   340
apply (rename_tac n)
kleing@10496
   341
apply (induct_tac n)
kleing@10496
   342
 apply (simp add: lesssub_def cong: conj_cong)
kleing@10496
   343
apply (rename_tac k)
berghofe@22271
   344
apply (simp add: wfP_eq_minimal)
kleing@10496
   345
apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
kleing@10496
   346
apply clarify
kleing@10496
   347
apply (rename_tac M m)
paulson@15341
   348
apply (case_tac "\<exists>x xs. size xs = k & x#xs : M")
kleing@10496
   349
 prefer 2
kleing@10496
   350
 apply (erule thin_rl)
kleing@10496
   351
 apply (erule thin_rl)
kleing@10496
   352
 apply blast
paulson@15341
   353
apply (erule_tac x = "{a. \<exists>xs. size xs = k & a#xs:M}" in allE)
kleing@10496
   354
apply (erule impE)
kleing@10496
   355
 apply blast
paulson@15341
   356
apply (thin_tac "\<exists>x xs. ?P x xs")
kleing@10496
   357
apply clarify
kleing@10496
   358
apply (rename_tac maxA xs)
kleing@10496
   359
apply (erule_tac x = "{ys. size ys = size xs & maxA#ys : M}" in allE)
kleing@10496
   360
apply (erule impE)
kleing@10496
   361
 apply blast
kleing@10496
   362
apply clarify
kleing@10496
   363
apply (thin_tac "m : M")
kleing@10496
   364
apply (thin_tac "maxA#xs : M")
kleing@10496
   365
apply (rule bexI)
kleing@10496
   366
 prefer 2
kleing@10496
   367
 apply assumption
kleing@10496
   368
apply clarify
kleing@10496
   369
apply simp
kleing@10496
   370
apply blast
kleing@10496
   371
done 
kleing@10496
   372
kleing@10496
   373
lemma closed_listI:
kleing@13006
   374
  "closed S f \<Longrightarrow> closed (list n S) (map2 f)"
kleing@10496
   375
apply (unfold closed_def)
kleing@10496
   376
apply (induct n)
kleing@10496
   377
 apply simp
kleing@10496
   378
apply clarify
kleing@10496
   379
apply (simp add: in_list_Suc_iff)
kleing@10496
   380
apply clarify
kleing@10496
   381
apply simp
nipkow@13074
   382
done
kleing@10496
   383
kleing@10496
   384
nipkow@13074
   385
lemma Listn_sl_aux:
ballarin@27611
   386
assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))"
ballarin@27611
   387
proof -
ballarin@29235
   388
  interpret Semilat A r f using assms by (rule Semilat.intro)
ballarin@27611
   389
show ?thesis
kleing@10496
   390
apply (unfold Listn.sl_def)
wenzelm@10918
   391
apply (simp (no_asm) only: semilat_Def split_conv)
kleing@10496
   392
apply (rule conjI)
kleing@10496
   393
 apply simp
kleing@10496
   394
apply (rule conjI)
nipkow@13074
   395
 apply (simp only: closedI closed_listI)
kleing@10496
   396
apply (simp (no_asm) only: list_def)
kleing@10496
   397
apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
nipkow@13074
   398
done
ballarin@27611
   399
qed
kleing@10496
   400
nipkow@13074
   401
lemma Listn_sl: "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
nipkow@13074
   402
 by(simp add: Listn_sl_aux split_tupled_all)
kleing@10496
   403
kleing@10496
   404
lemma coalesce_in_err_list [rule_format]:
kleing@13006
   405
  "!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)"
kleing@10496
   406
apply (induct n)
kleing@10496
   407
 apply simp
kleing@10496
   408
apply clarify
kleing@10496
   409
apply (simp add: in_list_Suc_iff)
kleing@10496
   410
apply clarify
kleing@10496
   411
apply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split)
kleing@10496
   412
apply force
kleing@10496
   413
done 
kleing@10496
   414
kleing@13006
   415
lemma lem: "\<And>x xs. x +_(op #) xs = x#xs"
kleing@10496
   416
  by (simp add: plussub_def)
kleing@10496
   417
kleing@10496
   418
lemma coalesce_eq_OK1_D [rule_format]:
kleing@13006
   419
  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
kleing@13006
   420
  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
kleing@13006
   421
  (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> xs <=[r] zs))"
kleing@10496
   422
apply (induct n)
kleing@10496
   423
  apply simp
kleing@10496
   424
apply clarify
kleing@10496
   425
apply (simp add: in_list_Suc_iff)
kleing@10496
   426
apply clarify
kleing@10496
   427
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
kleing@10496
   428
apply (force simp add: semilat_le_err_OK1)
kleing@10496
   429
done
kleing@10496
   430
kleing@10496
   431
lemma coalesce_eq_OK2_D [rule_format]:
kleing@13006
   432
  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
kleing@13006
   433
  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
kleing@13006
   434
  (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> ys <=[r] zs))"
kleing@10496
   435
apply (induct n)
kleing@10496
   436
 apply simp
kleing@10496
   437
apply clarify
kleing@10496
   438
apply (simp add: in_list_Suc_iff)
kleing@10496
   439
apply clarify
kleing@10496
   440
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
kleing@10496
   441
apply (force simp add: semilat_le_err_OK2)
kleing@10496
   442
done 
kleing@10496
   443
kleing@10496
   444
lemma lift2_le_ub:
paulson@15341
   445
  "\<lbrakk> semilat(err A, Err.le r, lift2 f); x\<in> A; y\<in> A; x +_f y = OK z; 
paulson@15341
   446
      u\<in> A; x <=_r u; y <=_r u \<rbrakk> \<Longrightarrow> z <=_r u"
kleing@10496
   447
apply (unfold semilat_Def plussub_def err_def)
kleing@10496
   448
apply (simp add: lift2_def)
kleing@10496
   449
apply clarify
kleing@10496
   450
apply (rotate_tac -3)
kleing@10496
   451
apply (erule thin_rl)
kleing@10496
   452
apply (erule thin_rl)
kleing@10496
   453
apply force
nipkow@13074
   454
done
kleing@10496
   455
kleing@10496
   456
lemma coalesce_eq_OK_ub_D [rule_format]:
kleing@13006
   457
  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
kleing@13006
   458
  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
kleing@10496
   459
  (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us 
kleing@13006
   460
           & us : list n A \<longrightarrow> zs <=[r] us))"
kleing@10496
   461
apply (induct n)
kleing@10496
   462
 apply simp
kleing@10496
   463
apply clarify
kleing@10496
   464
apply (simp add: in_list_Suc_iff)
kleing@10496
   465
apply clarify
kleing@10496
   466
apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def)
kleing@10496
   467
apply clarify
kleing@10496
   468
apply (rule conjI)
kleing@10496
   469
 apply (blast intro: lift2_le_ub)
kleing@10496
   470
apply blast
kleing@10496
   471
done 
kleing@10496
   472
kleing@10496
   473
lemma lift2_eq_ErrD:
paulson@15341
   474
  "\<lbrakk> x +_f y = Err; semilat(err A, Err.le r, lift2 f); x\<in> A; y\<in> A \<rbrakk> 
paulson@15341
   475
  \<Longrightarrow> ~(\<exists>u\<in> A. x <=_r u & y <=_r u)"
kleing@10496
   476
  by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])
kleing@10496
   477
kleing@10496
   478
kleing@10496
   479
lemma coalesce_eq_Err_D [rule_format]:
kleing@13006
   480
  "\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk> 
paulson@15341
   481
  \<Longrightarrow> !xs. xs\<in> list n A \<longrightarrow> (!ys. ys\<in> list n A \<longrightarrow> 
kleing@13006
   482
      coalesce (xs +[f] ys) = Err \<longrightarrow> 
paulson@15341
   483
      ~(\<exists>zs\<in> list n A. xs <=[r] zs & ys <=[r] zs))"
kleing@10496
   484
apply (induct n)
kleing@10496
   485
 apply simp
kleing@10496
   486
apply clarify
kleing@10496
   487
apply (simp add: in_list_Suc_iff)
kleing@10496
   488
apply clarify
kleing@10496
   489
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
kleing@10496
   490
 apply (blast dest: lift2_eq_ErrD)
kleing@10496
   491
done 
kleing@10496
   492
kleing@10496
   493
lemma closed_err_lift2_conv:
paulson@15341
   494
  "closed (err A) (lift2 f) = (\<forall>x\<in> A. \<forall>y\<in> A. x +_f y : err A)"
kleing@10496
   495
apply (unfold closed_def)
kleing@10496
   496
apply (simp add: err_def)
kleing@10496
   497
done 
kleing@10496
   498
kleing@10496
   499
lemma closed_map2_list [rule_format]:
kleing@13006
   500
  "closed (err A) (lift2 f) \<Longrightarrow> 
paulson@15341
   501
  \<forall>xs. xs : list n A \<longrightarrow> (\<forall>ys. ys : list n A \<longrightarrow> 
kleing@10496
   502
  map2 f xs ys : list n (err A))"
kleing@10496
   503
apply (unfold map2_def)
kleing@10496
   504
apply (induct n)
kleing@10496
   505
 apply simp
kleing@10496
   506
apply clarify
kleing@10496
   507
apply (simp add: in_list_Suc_iff)
kleing@10496
   508
apply clarify
kleing@10496
   509
apply (simp add: plussub_def closed_err_lift2_conv)
nipkow@13074
   510
done
kleing@10496
   511
kleing@10496
   512
lemma closed_lift2_sup:
kleing@13006
   513
  "closed (err A) (lift2 f) \<Longrightarrow> 
kleing@10496
   514
  closed (err (list n A)) (lift2 (sup f))"
kleing@10496
   515
  by (fastsimp  simp add: closed_def plussub_def sup_def lift2_def
kleing@10496
   516
                          coalesce_in_err_list closed_map2_list
kleing@10496
   517
                split: err.split)
kleing@10496
   518
kleing@10496
   519
lemma err_semilat_sup:
kleing@13006
   520
  "err_semilat (A,r,f) \<Longrightarrow> 
kleing@10496
   521
  err_semilat (list n A, Listn.le r, sup f)"
kleing@10496
   522
apply (unfold Err.sl_def)
wenzelm@10918
   523
apply (simp only: split_conv)
kleing@10496
   524
apply (simp (no_asm) only: semilat_Def plussub_def)
haftmann@27681
   525
apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup)
kleing@10496
   526
apply (rule conjI)
haftmann@27681
   527
 apply (drule Semilat.orderI [OF Semilat.intro])
kleing@10496
   528
 apply simp
kleing@10496
   529
apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)
kleing@10496
   530
apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)
kleing@10496
   531
apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D)
kleing@10496
   532
done 
kleing@10496
   533
kleing@10496
   534
lemma err_semilat_upto_esl:
kleing@13006
   535
  "\<And>L. err_semilat L \<Longrightarrow> err_semilat(upto_esl m L)"
kleing@10496
   536
apply (unfold Listn.upto_esl_def)
kleing@10496
   537
apply (simp (no_asm_simp) only: split_tupled_all)
kleing@10496
   538
apply simp
kleing@10496
   539
apply (fastsimp intro!: err_semilat_UnionI err_semilat_sup
kleing@10496
   540
                dest: lesub_list_impl_same_size 
kleing@10496
   541
                simp add: plussub_def Listn.sup_def)
kleing@10496
   542
done
kleing@10496
   543
kleing@10496
   544
end