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