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