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