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