src/HOLCF/dlist.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 298 3a0485439396
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/dlist.ML
     2     Author: 	Franz Regensburger
     3     ID:         $ $
     4     Copyright   1994 Technische Universitaet Muenchen
     5 
     6 Lemmas for dlist.thy
     7 *)
     8 
     9 open Dlist;
    10 
    11 (* ------------------------------------------------------------------------*)
    12 (* The isomorphisms dlist_rep_iso and dlist_abs_iso are strict             *)
    13 (* ------------------------------------------------------------------------*)
    14 
    15 val dlist_iso_strict= dlist_rep_iso RS (dlist_abs_iso RS 
    16 	(allI  RSN (2,allI RS iso_strict)));
    17 
    18 val dlist_rews = [dlist_iso_strict RS conjunct1,
    19 		dlist_iso_strict RS conjunct2];
    20 
    21 (* ------------------------------------------------------------------------*)
    22 (* Properties of dlist_copy                                                *)
    23 (* ------------------------------------------------------------------------*)
    24 
    25 val temp = prove_goalw Dlist.thy  [dlist_copy_def] "dlist_copy[f][UU]=UU"
    26  (fn prems =>
    27 	[
    28 	(asm_simp_tac (HOLCF_ss addsimps 
    29 		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
    30 	]);
    31 
    32 val dlist_copy = [temp];
    33 
    34 
    35 val temp = prove_goalw Dlist.thy  [dlist_copy_def,dnil_def] 
    36     "dlist_copy[f][dnil]=dnil"
    37  (fn prems =>
    38 	[
    39 	(asm_simp_tac (HOLCF_ss addsimps 
    40 		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
    41 	]);
    42 
    43 val dlist_copy = temp :: dlist_copy;
    44 
    45 
    46 val temp = prove_goalw Dlist.thy  [dlist_copy_def,dcons_def] 
    47 	"xl~=UU ==> dlist_copy[f][dcons[x][xl]]= dcons[x][f[xl]]"
    48  (fn prems =>
    49 	[
    50 	(cut_facts_tac prems 1),
    51 	(asm_simp_tac (HOLCF_ss addsimps 
    52 		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
    53 	(res_inst_tac [("Q","x=UU")] classical2 1),
    54 	(asm_simp_tac HOLCF_ss  1),
    55 	(asm_simp_tac (HOLCF_ss addsimps [defined_spair]) 1)
    56 	]);
    57 
    58 val dlist_copy = temp :: dlist_copy;
    59 
    60 val dlist_rews =  dlist_copy @ dlist_rews; 
    61 
    62 (* ------------------------------------------------------------------------*)
    63 (* Exhaustion and elimination for dlists                                   *)
    64 (* ------------------------------------------------------------------------*)
    65 
    66 val Exh_dlist = prove_goalw Dlist.thy [dcons_def,dnil_def]
    67 	"l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons[x][xl])"
    68  (fn prems =>
    69 	[
    70 	(simp_tac HOLCF_ss  1),
    71 	(rtac (dlist_rep_iso RS subst) 1),
    72 	(res_inst_tac [("p","dlist_rep[l]")] ssumE 1),
    73 	(rtac disjI1 1),
    74 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
    75 	(rtac disjI2 1),
    76 	(rtac disjI1 1),
    77 	(res_inst_tac [("p","x")] oneE 1),
    78 	(contr_tac 1),
    79 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
    80 	(rtac disjI2 1),
    81 	(rtac disjI2 1),
    82 	(res_inst_tac [("p","y")] sprodE 1),
    83 	(contr_tac 1),
    84 	(rtac exI 1),
    85 	(rtac exI 1),
    86 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
    87 	(fast_tac HOL_cs 1)
    88 	]);
    89 
    90 
    91 val dlistE = prove_goal Dlist.thy 
    92 "[| l=UU ==> Q; l=dnil ==> Q;!!x xl.[|l=dcons[x][xl];x~=UU;xl~=UU|]==>Q|]==>Q"
    93  (fn prems =>
    94 	[
    95 	(rtac (Exh_dlist RS disjE) 1),
    96 	(eresolve_tac prems 1),
    97 	(etac disjE 1),
    98 	(eresolve_tac prems 1),
    99 	(etac exE 1),
   100 	(etac exE 1),
   101 	(resolve_tac prems 1),
   102 	(fast_tac HOL_cs 1),
   103 	(fast_tac HOL_cs 1),
   104 	(fast_tac HOL_cs 1)
   105 	]);
   106 
   107 (* ------------------------------------------------------------------------*)
   108 (* Properties of dlist_when                                                *)
   109 (* ------------------------------------------------------------------------*)
   110 
   111 val temp = prove_goalw  Dlist.thy  [dlist_when_def] "dlist_when[f1][f2][UU]=UU"
   112  (fn prems =>
   113 	[
   114 	(asm_simp_tac (HOLCF_ss addsimps [dlist_iso_strict]) 1)
   115 	]);
   116 
   117 val dlist_when = [temp];
   118 
   119 val temp = prove_goalw  Dlist.thy [dlist_when_def,dnil_def]
   120  "dlist_when[f1][f2][dnil]= f1"
   121  (fn prems =>
   122 	[
   123 	(asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso]) 1)
   124 	]);
   125 
   126 val dlist_when = temp::dlist_when;
   127 
   128 val temp = prove_goalw  Dlist.thy [dlist_when_def,dcons_def]
   129  "[|x~=UU;xl~=UU|] ==> dlist_when[f1][f2][dcons[x][xl]]= f2[x][xl]"
   130  (fn prems =>
   131 	[
   132 	(cut_facts_tac prems 1),
   133 	(asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso,defined_spair]) 1)
   134 	]);
   135 
   136 val dlist_when = temp::dlist_when;
   137 
   138 val dlist_rews = dlist_when @ dlist_rews;
   139 
   140 (* ------------------------------------------------------------------------*)
   141 (* Rewrites for  discriminators and  selectors                             *)
   142 (* ------------------------------------------------------------------------*)
   143 
   144 fun prover defs thm = prove_goalw Dlist.thy defs thm
   145  (fn prems =>
   146 	[
   147 	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   148 	]);
   149 
   150 val dlist_discsel = [
   151 	prover [is_dnil_def] "is_dnil[UU]=UU",
   152 	prover [is_dcons_def] "is_dcons[UU]=UU",
   153 	prover [dhd_def] "dhd[UU]=UU",
   154 	prover [dtl_def] "dtl[UU]=UU"
   155 	];
   156 
   157 fun prover defs thm = prove_goalw Dlist.thy defs thm
   158  (fn prems =>
   159 	[
   160 	(cut_facts_tac prems 1),
   161 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   162 	]);
   163 
   164 val dlist_discsel = [
   165 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   166   "is_dnil[dnil]=TT",
   167 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   168   "[|x~=UU;xl~=UU|] ==> is_dnil[dcons[x][xl]]=FF",
   169 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   170   "is_dcons[dnil]=FF",
   171 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   172   "[|x~=UU;xl~=UU|] ==> is_dcons[dcons[x][xl]]=TT",
   173 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   174   "dhd[dnil]=UU",
   175 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   176   "[|x~=UU;xl~=UU|] ==> dhd[dcons[x][xl]]=x",
   177 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   178   "dtl[dnil]=UU",
   179 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   180   "[|x~=UU;xl~=UU|] ==> dtl[dcons[x][xl]]=xl"] @ dlist_discsel;
   181 
   182 val dlist_rews = dlist_discsel @ dlist_rews;
   183 
   184 (* ------------------------------------------------------------------------*)
   185 (* Definedness and strictness                                              *)
   186 (* ------------------------------------------------------------------------*)
   187 
   188 fun prover contr thm = prove_goal Dlist.thy thm
   189  (fn prems =>
   190 	[
   191 	(res_inst_tac [("P1",contr)] classical3 1),
   192 	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   193 	(dtac sym 1),
   194 	(asm_simp_tac HOLCF_ss  1),
   195 	(simp_tac (HOLCF_ss addsimps (prems @ dlist_rews)) 1)
   196 	]);
   197 
   198 
   199 val dlist_constrdef = [
   200 prover "is_dnil[UU] ~= UU" "dnil~=UU",
   201 prover "is_dcons[UU] ~= UU" "[|x~=UU;xl~=UU|] ==> dcons[x][xl]~=UU"
   202  ];
   203 
   204 
   205 fun prover defs thm = prove_goalw Dlist.thy defs thm
   206  (fn prems =>
   207 	[
   208 	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   209 	]);
   210 
   211 val dlist_constrdef = [
   212 	prover [dcons_def] "dcons[UU][xl]=UU",
   213 	prover [dcons_def] "dcons[x][UU]=UU"
   214 	] @ dlist_constrdef;
   215 
   216 val dlist_rews = dlist_constrdef @ dlist_rews;
   217 
   218 
   219 (* ------------------------------------------------------------------------*)
   220 (* Distinctness wrt. << and =                                              *)
   221 (* ------------------------------------------------------------------------*)
   222 
   223 val temp = prove_goal Dlist.thy  "~dnil << dcons[x][xl]"
   224  (fn prems =>
   225 	[
   226 	(res_inst_tac [("P1","TT << FF")] classical3 1),
   227 	(resolve_tac dist_less_tr 1),
   228 	(dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
   229 	(etac box_less 1),
   230 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   231 	(res_inst_tac [("Q","x=UU")] classical2 1),
   232 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   233 	(res_inst_tac [("Q","xl=UU")] classical2 1),
   234 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   235 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   236 	]);
   237 
   238 val dlist_dist_less = [temp];
   239 
   240 val temp = prove_goal Dlist.thy  "[|x~=UU;xl~=UU|]==>~dcons[x][xl] << dnil"
   241  (fn prems =>
   242 	[
   243 	(cut_facts_tac prems 1),
   244 	(res_inst_tac [("P1","TT << FF")] classical3 1),
   245 	(resolve_tac dist_less_tr 1),
   246 	(dres_inst_tac [("fo5","is_dcons")] monofun_cfun_arg 1),
   247 	(etac box_less 1),
   248 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   249 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   250 	]);
   251 
   252 val dlist_dist_less = temp::dlist_dist_less;
   253 
   254 val temp = prove_goal Dlist.thy  "dnil ~= dcons[x][xl]"
   255  (fn prems =>
   256 	[
   257 	(res_inst_tac [("Q","x=UU")] classical2 1),
   258 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   259 	(res_inst_tac [("Q","xl=UU")] classical2 1),
   260 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   261 	(res_inst_tac [("P1","TT = FF")] classical3 1),
   262 	(resolve_tac dist_eq_tr 1),
   263 	(dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1),
   264 	(etac box_equals 1),
   265 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   266 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   267 	]);
   268 
   269 val dlist_dist_eq = [temp,temp RS not_sym];
   270 
   271 val dlist_rews = dlist_dist_less @ dlist_dist_eq @ dlist_rews;
   272 
   273 (* ------------------------------------------------------------------------*)
   274 (* Invertibility                                                           *)
   275 (* ------------------------------------------------------------------------*)
   276 
   277 val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
   278 \ dcons[x1][x2] << dcons[y1][y2]|] ==> x1<< y1 & x2 << y2"
   279  (fn prems =>
   280 	[
   281 	(cut_facts_tac prems 1),
   282 	(rtac conjI 1),
   283 	(dres_inst_tac [("fo5","dlist_when[UU][LAM x l.x]")] monofun_cfun_arg 1),
   284 	(etac box_less 1),
   285 	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   286 	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   287 	(dres_inst_tac [("fo5","dlist_when[UU][LAM x l.l]")] monofun_cfun_arg 1),
   288 	(etac box_less 1),
   289 	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   290 	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
   291 	]);
   292 
   293 val dlist_invert =[temp];
   294 
   295 (* ------------------------------------------------------------------------*)
   296 (* Injectivity                                                             *)
   297 (* ------------------------------------------------------------------------*)
   298 
   299 val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
   300 \ dcons[x1][x2] = dcons[y1][y2]|] ==> x1= y1 & x2 = y2"
   301  (fn prems =>
   302 	[
   303 	(cut_facts_tac prems 1),
   304 	(rtac conjI 1),
   305 	(dres_inst_tac [("f","dlist_when[UU][LAM x l.x]")] cfun_arg_cong 1),
   306 	(etac box_equals 1),
   307 	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   308 	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   309 	(dres_inst_tac [("f","dlist_when[UU][LAM x l.l]")] cfun_arg_cong 1),
   310 	(etac box_equals 1),
   311 	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
   312 	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
   313 	]);
   314 
   315 val dlist_inject = [temp];
   316  
   317 
   318 (* ------------------------------------------------------------------------*)
   319 (* definedness for  discriminators and  selectors                          *)
   320 (* ------------------------------------------------------------------------*)
   321 
   322 fun prover thm = prove_goal Dlist.thy thm
   323  (fn prems =>
   324 	[
   325 	(cut_facts_tac prems 1),
   326 	(rtac dlistE 1),
   327 	(contr_tac 1),
   328 	(REPEAT (asm_simp_tac (HOLCF_ss addsimps dlist_discsel) 1))
   329 	]);
   330 
   331 val dlist_discsel_def = 
   332 	[
   333 	prover "l~=UU ==> is_dnil[l]~=UU", 
   334 	prover "l~=UU ==> is_dcons[l]~=UU" 
   335 	];
   336 
   337 val dlist_rews = dlist_discsel_def @ dlist_rews;
   338 
   339 (* ------------------------------------------------------------------------*)
   340 (* enhance the simplifier                                                  *)
   341 (* ------------------------------------------------------------------------*)
   342 
   343 val dhd2 = prove_goal Dlist.thy "xl~=UU ==> dhd[dcons[x][xl]]=x"
   344  (fn prems =>
   345 	[
   346 	(cut_facts_tac prems 1),
   347 	(res_inst_tac [("Q","x=UU")] classical2 1),
   348 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   349 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   350 	]);
   351 
   352 val dtl2 = prove_goal Dlist.thy "x~=UU ==> dtl[dcons[x][xl]]=xl"
   353  (fn prems =>
   354 	[
   355 	(cut_facts_tac prems 1),
   356 	(res_inst_tac [("Q","xl=UU")] classical2 1),
   357 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   358 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   359 	]);
   360 
   361 val dlist_rews = dhd2 :: dtl2 :: dlist_rews;
   362 
   363 (* ------------------------------------------------------------------------*)
   364 (* Properties dlist_take                                                   *)
   365 (* ------------------------------------------------------------------------*)
   366 
   367 val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take(n)[UU]=UU"
   368  (fn prems =>
   369 	[
   370 	(res_inst_tac [("n","n")] natE 1),
   371 	(asm_simp_tac iterate_ss 1),
   372 	(asm_simp_tac iterate_ss 1),
   373 	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   374 	]);
   375 
   376 val dlist_take = [temp];
   377 
   378 val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take(0)[xs]=UU"
   379  (fn prems =>
   380 	[
   381 	(asm_simp_tac iterate_ss 1)
   382 	]);
   383 
   384 val dlist_take = temp::dlist_take;
   385 
   386 val temp = prove_goalw Dlist.thy [dlist_take_def]
   387 	"dlist_take(Suc(n))[dnil]=dnil"
   388  (fn prems =>
   389 	[
   390 	(asm_simp_tac iterate_ss 1),
   391 	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   392 	]);
   393 
   394 val dlist_take = temp::dlist_take;
   395 
   396 val temp = prove_goalw Dlist.thy [dlist_take_def]
   397   "dlist_take(Suc(n))[dcons[x][xl]]=dcons[x][dlist_take(n)[xl]]"
   398  (fn prems =>
   399 	[
   400 	(res_inst_tac [("Q","x=UU")] classical2 1),
   401 	(asm_simp_tac iterate_ss 1),
   402 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   403 	(res_inst_tac [("Q","xl=UU")] classical2 1),
   404 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   405 	(asm_simp_tac iterate_ss 1),
   406 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   407 	(res_inst_tac [("n","n")] natE 1),
   408 	(asm_simp_tac iterate_ss 1),
   409 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   410 	(asm_simp_tac iterate_ss 1),
   411 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   412 	(asm_simp_tac iterate_ss 1),
   413 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   414 	]);
   415 
   416 val dlist_take = temp::dlist_take;
   417 
   418 val dlist_rews = dlist_take @ dlist_rews;
   419 
   420 (* ------------------------------------------------------------------------*)
   421 (* take lemma for dlists                                                  *)
   422 (* ------------------------------------------------------------------------*)
   423 
   424 fun prover reach defs thm  = prove_goalw Dlist.thy defs thm
   425  (fn prems =>
   426 	[
   427 	(res_inst_tac [("t","l1")] (reach RS subst) 1),
   428 	(res_inst_tac [("t","l2")] (reach RS subst) 1),
   429 	(rtac (fix_def2 RS ssubst) 1),
   430 	(rtac (contlub_cfun_fun RS ssubst) 1),
   431 	(rtac is_chain_iterate 1),
   432 	(rtac (contlub_cfun_fun RS ssubst) 1),
   433 	(rtac is_chain_iterate 1),
   434 	(rtac lub_equal 1),
   435 	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
   436 	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
   437 	(rtac allI 1),
   438 	(resolve_tac prems 1)
   439 	]);
   440 
   441 val dlist_take_lemma = prover dlist_reach  [dlist_take_def]
   442 	"(!!n.dlist_take(n)[l1]=dlist_take(n)[l2]) ==> l1=l2";
   443 
   444 
   445 (* ------------------------------------------------------------------------*)
   446 (* Co -induction for dlists                                               *)
   447 (* ------------------------------------------------------------------------*)
   448 
   449 val dlist_coind_lemma = prove_goalw Dlist.thy [dlist_bisim_def] 
   450 "dlist_bisim(R) ==> ! p q.R(p,q) --> dlist_take(n)[p]=dlist_take(n)[q]"
   451  (fn prems =>
   452 	[
   453 	(cut_facts_tac prems 1),
   454 	(nat_ind_tac "n" 1),
   455 	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   456 	(strip_tac 1),
   457 	((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
   458 	(atac 1),
   459 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   460 	(etac disjE 1),
   461 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   462 	(etac exE 1),
   463 	(etac exE 1),
   464 	(etac exE 1),
   465 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   466 	(REPEAT (etac conjE 1)),
   467 	(rtac cfun_arg_cong 1),
   468 	(fast_tac HOL_cs 1)
   469 	]);
   470 
   471 val dlist_coind = prove_goal Dlist.thy "[|dlist_bisim(R);R(p,q)|] ==> p = q"
   472  (fn prems =>
   473 	[
   474 	(rtac dlist_take_lemma 1),
   475 	(rtac (dlist_coind_lemma RS spec RS spec RS mp) 1),
   476 	(resolve_tac prems 1),
   477 	(resolve_tac prems 1)
   478 	]);
   479 
   480 (* ------------------------------------------------------------------------*)
   481 (* structural induction                                                    *)
   482 (* ------------------------------------------------------------------------*)
   483 
   484 val dlist_finite_ind = prove_goal Dlist.thy
   485 "[|P(UU);P(dnil);\
   486 \  !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons[x][l1])\
   487 \  |] ==> !l.P(dlist_take(n)[l])"
   488  (fn prems =>
   489 	[
   490 	(nat_ind_tac "n" 1),
   491 	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   492 	(resolve_tac prems 1),
   493 	(rtac allI 1),
   494 	(res_inst_tac [("l","l")] dlistE 1),
   495 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   496 	(resolve_tac prems 1),
   497 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   498 	(resolve_tac prems 1),
   499 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   500 	(res_inst_tac [("Q","dlist_take(n1)[xl]=UU")] classical2 1),
   501 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   502 	(resolve_tac prems 1),
   503 	(resolve_tac prems 1),
   504 	(atac 1),
   505 	(atac 1),
   506 	(etac spec 1)
   507 	]);
   508 
   509 val dlist_all_finite_lemma1 = prove_goal Dlist.thy
   510 "!l.dlist_take(n)[l]=UU |dlist_take(n)[l]=l"
   511  (fn prems =>
   512 	[
   513 	(nat_ind_tac "n" 1),
   514 	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   515 	(rtac allI 1),
   516 	(res_inst_tac [("l","l")] dlistE 1),
   517 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   518 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   519 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   520 	(eres_inst_tac [("x","xl")] allE 1),
   521 	(etac disjE 1),
   522 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   523 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
   524 	]);
   525 
   526 val dlist_all_finite_lemma2 = prove_goal Dlist.thy "? n.dlist_take(n)[l]=l"
   527  (fn prems =>
   528 	[
   529 	(res_inst_tac [("Q","l=UU")] classical2 1),
   530 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   531 	(subgoal_tac "(!n.dlist_take(n)[l]=UU) |(? n.dlist_take(n)[l]=l)" 1),
   532 	(etac disjE 1),
   533 	(eres_inst_tac [("P","l=UU")] notE 1),
   534 	(rtac dlist_take_lemma 1),
   535 	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
   536 	(atac 1),
   537 	(subgoal_tac "!n.!l.dlist_take(n)[l]=UU |dlist_take(n)[l]=l" 1),
   538 	(fast_tac HOL_cs 1),
   539 	(rtac allI 1),
   540 	(rtac dlist_all_finite_lemma1 1)
   541 	]);
   542 
   543 val dlist_all_finite= prove_goalw Dlist.thy [dlist_finite_def] "dlist_finite(l)"
   544  (fn prems =>
   545 	[
   546 	(rtac  dlist_all_finite_lemma2 1)
   547 	]);
   548 
   549 val dlist_ind = prove_goal Dlist.thy
   550 "[|P(UU);P(dnil);\
   551 \  !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons[x][l1])|] ==> P(l)"
   552  (fn prems =>
   553 	[
   554 	(rtac (dlist_all_finite_lemma2 RS exE) 1),
   555 	(etac subst 1),
   556 	(rtac (dlist_finite_ind RS spec) 1),
   557 	(REPEAT (resolve_tac prems 1)),
   558 	(REPEAT (atac 1))
   559 	]);
   560 
   561 
   562 
   563