src/HOLCF/dnat.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 297 5ef75ff3baeb
permissions -rw-r--r--
tidying
     1 (*  Title: 	HOLCF/dnat.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for dnat.thy 
     7 *)
     8 
     9 open Dnat;
    10 
    11 (* ------------------------------------------------------------------------*)
    12 (* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict               *)
    13 (* ------------------------------------------------------------------------*)
    14 
    15 val dnat_iso_strict= dnat_rep_iso RS (dnat_abs_iso RS 
    16 	(allI  RSN (2,allI RS iso_strict)));
    17 
    18 val dnat_rews = [dnat_iso_strict RS conjunct1,
    19 		dnat_iso_strict RS conjunct2];
    20 
    21 (* ------------------------------------------------------------------------*)
    22 (* Properties of dnat_copy                                                 *)
    23 (* ------------------------------------------------------------------------*)
    24 
    25 fun prover defs thm =  prove_goalw Dnat.thy defs thm
    26  (fn prems =>
    27 	[
    28 	(cut_facts_tac prems 1),
    29 	(asm_simp_tac (HOLCF_ss addsimps 
    30 		(dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
    31 	]);
    32 
    33 val dnat_copy = 
    34 	[
    35 	prover [dnat_copy_def] "dnat_copy[f][UU]=UU",
    36 	prover [dnat_copy_def,dzero_def] "dnat_copy[f][dzero]= dzero",
    37 	prover [dnat_copy_def,dsucc_def] 
    38 		"n~=UU ==> dnat_copy[f][dsucc[n]] = dsucc[f[n]]"
    39 	];
    40 
    41 val dnat_rews =  dnat_copy @ dnat_rews; 
    42 
    43 (* ------------------------------------------------------------------------*)
    44 (* Exhaustion and elimination for dnat                                     *)
    45 (* ------------------------------------------------------------------------*)
    46 
    47 val Exh_dnat = prove_goalw Dnat.thy [dsucc_def,dzero_def]
    48 	"n = UU | n = dzero | (? x . x~=UU & n = dsucc[x])"
    49  (fn prems =>
    50 	[
    51 	(simp_tac HOLCF_ss  1),
    52 	(rtac (dnat_rep_iso RS subst) 1),
    53 	(res_inst_tac [("p","dnat_rep[n]")] ssumE 1),
    54 	(rtac disjI1 1),
    55 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    56 	(rtac (disjI1 RS disjI2) 1),
    57 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    58 	(res_inst_tac [("p","x")] oneE 1),
    59 	(contr_tac 1),
    60 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    61 	(rtac (disjI2 RS disjI2) 1),
    62 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    63 	(fast_tac HOL_cs 1)
    64 	]);
    65 
    66 val dnatE = prove_goal Dnat.thy 
    67  "[| n=UU ==> Q; n=dzero ==> Q; !!x.[|n=dsucc[x];x~=UU|]==>Q|]==>Q"
    68  (fn prems =>
    69 	[
    70 	(rtac (Exh_dnat RS disjE) 1),
    71 	(eresolve_tac prems 1),
    72 	(etac disjE 1),
    73 	(eresolve_tac prems 1),
    74 	(REPEAT (etac exE 1)),
    75 	(resolve_tac prems 1),
    76 	(fast_tac HOL_cs 1),
    77 	(fast_tac HOL_cs 1)
    78 	]);
    79 
    80 (* ------------------------------------------------------------------------*)
    81 (* Properties of dnat_when                                                 *)
    82 (* ------------------------------------------------------------------------*)
    83 
    84 fun prover defs thm =  prove_goalw Dnat.thy defs thm
    85  (fn prems =>
    86 	[
    87 	(cut_facts_tac prems 1),
    88 	(asm_simp_tac (HOLCF_ss addsimps 
    89 		(dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
    90 	]);
    91 
    92 
    93 val dnat_when = [
    94 	prover [dnat_when_def] "dnat_when[c][f][UU]=UU",
    95 	prover [dnat_when_def,dzero_def] "dnat_when[c][f][dzero]=c",
    96 	prover [dnat_when_def,dsucc_def] 
    97 		"n~=UU ==> dnat_when[c][f][dsucc[n]]=f[n]"
    98 	];
    99 
   100 val dnat_rews = dnat_when @ dnat_rews;
   101 
   102 (* ------------------------------------------------------------------------*)
   103 (* Rewrites for  discriminators and  selectors                             *)
   104 (* ------------------------------------------------------------------------*)
   105 
   106 fun prover defs thm = prove_goalw Dnat.thy defs thm
   107  (fn prems =>
   108 	[
   109 	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   110 	]);
   111 
   112 val dnat_discsel = [
   113 	prover [is_dzero_def] "is_dzero[UU]=UU",
   114 	prover [is_dsucc_def] "is_dsucc[UU]=UU",
   115 	prover [dpred_def] "dpred[UU]=UU"
   116 	];
   117 
   118 
   119 fun prover defs thm = prove_goalw Dnat.thy defs thm
   120  (fn prems =>
   121 	[
   122 	(cut_facts_tac prems 1),
   123 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   124 	]);
   125 
   126 val dnat_discsel = [
   127 	prover [is_dzero_def] "is_dzero[dzero]=TT",
   128 	prover [is_dzero_def] "n~=UU ==>is_dzero[dsucc[n]]=FF",
   129 	prover [is_dsucc_def] "is_dsucc[dzero]=FF",
   130 	prover [is_dsucc_def] "n~=UU ==> is_dsucc[dsucc[n]]=TT",
   131 	prover [dpred_def] "dpred[dzero]=UU",
   132 	prover [dpred_def] "n~=UU ==> dpred[dsucc[n]]=n"
   133 	] @ dnat_discsel;
   134 
   135 val dnat_rews = dnat_discsel @ dnat_rews;
   136 
   137 (* ------------------------------------------------------------------------*)
   138 (* Definedness and strictness                                              *)
   139 (* ------------------------------------------------------------------------*)
   140 
   141 fun prover contr thm = prove_goal Dnat.thy thm
   142  (fn prems =>
   143 	[
   144 	(res_inst_tac [("P1",contr)] classical3 1),
   145 	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   146 	(dtac sym 1),
   147 	(asm_simp_tac HOLCF_ss  1),
   148 	(simp_tac (HOLCF_ss addsimps (prems @ dnat_rews)) 1)
   149 	]);
   150 
   151 val dnat_constrdef = [
   152 	prover "is_dzero[UU] ~= UU" "dzero~=UU",
   153 	prover "is_dsucc[UU] ~= UU" "n~=UU ==> dsucc[n]~=UU"
   154 	]; 
   155 
   156 
   157 fun prover defs thm = prove_goalw Dnat.thy defs thm
   158  (fn prems =>
   159 	[
   160 	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   161 	]);
   162 
   163 val dnat_constrdef = [
   164 	prover [dsucc_def] "dsucc[UU]=UU"
   165 	] @ dnat_constrdef;
   166 
   167 val dnat_rews = dnat_constrdef @ dnat_rews;
   168 
   169 
   170 (* ------------------------------------------------------------------------*)
   171 (* Distinctness wrt. << and =                                              *)
   172 (* ------------------------------------------------------------------------*)
   173 
   174 val temp = prove_goal Dnat.thy  "~dzero << dsucc[n]"
   175  (fn prems =>
   176 	[
   177 	(res_inst_tac [("P1","TT << FF")] classical3 1),
   178 	(resolve_tac dist_less_tr 1),
   179 	(dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
   180 	(etac box_less 1),
   181 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   182 	(res_inst_tac [("Q","n=UU")] classical2 1),
   183 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   184 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   185 	]);
   186 
   187 val dnat_dist_less = [temp];
   188 
   189 val temp = prove_goal Dnat.thy  "n~=UU ==> ~dsucc[n] << dzero"
   190  (fn prems =>
   191 	[
   192 	(cut_facts_tac prems 1),
   193 	(res_inst_tac [("P1","TT << FF")] classical3 1),
   194 	(resolve_tac dist_less_tr 1),
   195 	(dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1),
   196 	(etac box_less 1),
   197 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   198 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   199 	]);
   200 
   201 val dnat_dist_less = temp::dnat_dist_less;
   202 
   203 val temp = prove_goal Dnat.thy   "dzero ~= dsucc[n]"
   204  (fn prems =>
   205 	[
   206 	(res_inst_tac [("Q","n=UU")] classical2 1),
   207 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   208 	(res_inst_tac [("P1","TT = FF")] classical3 1),
   209 	(resolve_tac dist_eq_tr 1),
   210 	(dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
   211 	(etac box_equals 1),
   212 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   213 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   214 	]);
   215 
   216 val dnat_dist_eq = [temp, temp RS not_sym];
   217 
   218 val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews;
   219 
   220 (* ------------------------------------------------------------------------*)
   221 (* Invertibility                                                           *)
   222 (* ------------------------------------------------------------------------*)
   223 
   224 val dnat_invert = 
   225 	[
   226 prove_goal Dnat.thy 
   227 "[|x1~=UU; y1~=UU; dsucc[x1] << dsucc[y1] |] ==> x1<< y1"
   228  (fn prems =>
   229 	[
   230 	(cut_facts_tac prems 1),
   231 	(dres_inst_tac [("fo5","dnat_when[c][LAM x.x]")] monofun_cfun_arg 1),
   232 	(etac box_less 1),
   233 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   234 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   235 	])
   236 	];
   237 
   238 (* ------------------------------------------------------------------------*)
   239 (* Injectivity                                                             *)
   240 (* ------------------------------------------------------------------------*)
   241 
   242 val dnat_inject = 
   243 	[
   244 prove_goal Dnat.thy 
   245 "[|x1~=UU; y1~=UU; dsucc[x1] = dsucc[y1] |] ==> x1= y1"
   246  (fn prems =>
   247 	[
   248 	(cut_facts_tac prems 1),
   249 	(dres_inst_tac [("f","dnat_when[c][LAM x.x]")] cfun_arg_cong 1),
   250 	(etac box_equals 1),
   251 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   252 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   253 	])
   254 	];
   255 
   256 (* ------------------------------------------------------------------------*)
   257 (* definedness for  discriminators and  selectors                          *)
   258 (* ------------------------------------------------------------------------*)
   259 
   260 
   261 fun prover thm = prove_goal Dnat.thy thm
   262  (fn prems =>
   263 	[
   264 	(cut_facts_tac prems 1),
   265 	(rtac dnatE 1),
   266 	(contr_tac 1),
   267 	(REPEAT (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1))
   268 	]);
   269 
   270 val dnat_discsel_def = 
   271 	[
   272 	prover  "n~=UU ==> is_dzero[n]~=UU",
   273 	prover  "n~=UU ==> is_dsucc[n]~=UU"
   274 	];
   275 
   276 val dnat_rews = dnat_discsel_def @ dnat_rews;
   277 
   278  
   279 (* ------------------------------------------------------------------------*)
   280 (* Properties dnat_take                                                    *)
   281 (* ------------------------------------------------------------------------*)
   282 val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take(n)[UU]=UU"
   283  (fn prems =>
   284 	[
   285 	(res_inst_tac [("n","n")] natE 1),
   286 	(asm_simp_tac iterate_ss 1),
   287 	(asm_simp_tac iterate_ss 1),
   288 	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   289 	]);
   290 
   291 val dnat_take = [temp];
   292 
   293 val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take(0)[xs]=UU"
   294  (fn prems =>
   295 	[
   296 	(asm_simp_tac iterate_ss 1)
   297 	]);
   298 
   299 val dnat_take = temp::dnat_take;
   300 
   301 val temp = prove_goalw Dnat.thy [dnat_take_def]
   302 	"dnat_take(Suc(n))[dzero]=dzero"
   303  (fn prems =>
   304 	[
   305 	(asm_simp_tac iterate_ss 1),
   306 	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   307 	]);
   308 
   309 val dnat_take = temp::dnat_take;
   310 
   311 val temp = prove_goalw Dnat.thy [dnat_take_def]
   312   "dnat_take(Suc(n))[dsucc[xs]]=dsucc[dnat_take(n)[xs]]"
   313  (fn prems =>
   314 	[
   315 	(res_inst_tac [("Q","xs=UU")] classical2 1),
   316 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   317 	(asm_simp_tac iterate_ss 1),
   318 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   319 	(res_inst_tac [("n","n")] natE 1),
   320 	(asm_simp_tac iterate_ss 1),
   321 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   322 	(asm_simp_tac iterate_ss 1),
   323 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   324 	(asm_simp_tac iterate_ss 1),
   325 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   326 	]);
   327 
   328 val dnat_take = temp::dnat_take;
   329 
   330 val dnat_rews = dnat_take @ dnat_rews;
   331 
   332 
   333 (* ------------------------------------------------------------------------*)
   334 (* take lemma for dnats                                                  *)
   335 (* ------------------------------------------------------------------------*)
   336 
   337 fun prover reach defs thm  = prove_goalw Dnat.thy defs thm
   338  (fn prems =>
   339 	[
   340 	(res_inst_tac [("t","s1")] (reach RS subst) 1),
   341 	(res_inst_tac [("t","s2")] (reach RS subst) 1),
   342 	(rtac (fix_def2 RS ssubst) 1),
   343 	(rtac (contlub_cfun_fun RS ssubst) 1),
   344 	(rtac is_chain_iterate 1),
   345 	(rtac (contlub_cfun_fun RS ssubst) 1),
   346 	(rtac is_chain_iterate 1),
   347 	(rtac lub_equal 1),
   348 	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
   349 	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
   350 	(rtac allI 1),
   351 	(resolve_tac prems 1)
   352 	]);
   353 
   354 val dnat_take_lemma = prover dnat_reach  [dnat_take_def]
   355 	"(!!n.dnat_take(n)[s1]=dnat_take(n)[s2]) ==> s1=s2";
   356 
   357 
   358 (* ------------------------------------------------------------------------*)
   359 (* Co -induction for dnats                                                 *)
   360 (* ------------------------------------------------------------------------*)
   361 
   362 val dnat_coind_lemma = prove_goalw Dnat.thy [dnat_bisim_def] 
   363 "dnat_bisim(R) ==> ! p q.R(p,q) --> dnat_take(n)[p]=dnat_take(n)[q]"
   364  (fn prems =>
   365 	[
   366 	(cut_facts_tac prems 1),
   367 	(nat_ind_tac "n" 1),
   368 	(simp_tac (HOLCF_ss addsimps dnat_take) 1),
   369 	(strip_tac 1),
   370 	((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
   371 	(atac 1),
   372 	(asm_simp_tac (HOLCF_ss addsimps dnat_take) 1),
   373 	(etac disjE 1),
   374 	(asm_simp_tac (HOLCF_ss addsimps dnat_take) 1),
   375 	(etac exE 1),
   376 	(etac exE 1),
   377 	(asm_simp_tac (HOLCF_ss addsimps dnat_take) 1),
   378 	(REPEAT (etac conjE 1)),
   379 	(rtac cfun_arg_cong 1),
   380 	(fast_tac HOL_cs 1)
   381 	]);
   382 
   383 val dnat_coind = prove_goal Dnat.thy "[|dnat_bisim(R);R(p,q)|] ==> p = q"
   384  (fn prems =>
   385 	[
   386 	(rtac dnat_take_lemma 1),
   387 	(rtac (dnat_coind_lemma RS spec RS spec RS mp) 1),
   388 	(resolve_tac prems 1),
   389 	(resolve_tac prems 1)
   390 	]);
   391 
   392 
   393 (* ------------------------------------------------------------------------*)
   394 (* structural induction for admissible predicates                          *)
   395 (* ------------------------------------------------------------------------*)
   396 
   397 (* not needed any longer
   398 val dnat_ind = prove_goal Dnat.thy
   399 "[| adm(P);\
   400 \   P(UU);\
   401 \   P(dzero);\
   402 \   !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc[s1])|] ==> P(s)"
   403  (fn prems =>
   404 	[
   405 	(rtac (dnat_reach RS subst) 1),
   406 	(res_inst_tac [("x","s")] spec 1),
   407 	(rtac fix_ind 1),
   408 	(rtac adm_all2 1),
   409 	(rtac adm_subst 1),
   410 	(contX_tacR 1),
   411 	(resolve_tac prems 1),
   412 	(simp_tac HOLCF_ss 1),
   413 	(resolve_tac prems 1),
   414 	(strip_tac 1),
   415 	(res_inst_tac [("n","xa")] dnatE 1),
   416 	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
   417 	(resolve_tac prems 1),
   418 	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
   419 	(resolve_tac prems 1),
   420 	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
   421 	(res_inst_tac [("Q","x[xb]=UU")] classical2 1),
   422 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   423 	(resolve_tac prems 1),
   424 	(eresolve_tac prems 1),
   425 	(etac spec 1)
   426 	]);
   427 *)
   428 
   429 val dnat_finite_ind = prove_goal Dnat.thy
   430 "[|P(UU);P(dzero);\
   431 \  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
   432 \  |] ==> !s.P(dnat_take(n)[s])"
   433  (fn prems =>
   434 	[
   435 	(nat_ind_tac "n" 1),
   436 	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   437 	(resolve_tac prems 1),
   438 	(rtac allI 1),
   439 	(res_inst_tac [("n","s")] dnatE 1),
   440 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   441 	(resolve_tac prems 1),
   442 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   443 	(resolve_tac prems 1),
   444 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   445 	(res_inst_tac [("Q","dnat_take(n1)[x]=UU")] classical2 1),
   446 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   447 	(resolve_tac prems 1),
   448 	(resolve_tac prems 1),
   449 	(atac 1),
   450 	(etac spec 1)
   451 	]);
   452 
   453 val dnat_all_finite_lemma1 = prove_goal Dnat.thy
   454 "!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s"
   455  (fn prems =>
   456 	[
   457 	(nat_ind_tac "n" 1),
   458 	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   459 	(rtac allI 1),
   460 	(res_inst_tac [("n","s")] dnatE 1),
   461 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   462 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   463 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   464 	(eres_inst_tac [("x","x")] allE 1),
   465 	(etac disjE 1),
   466 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   467 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   468 	]);
   469 
   470 val dnat_all_finite_lemma2 = prove_goal Dnat.thy "? n.dnat_take(n)[s]=s"
   471  (fn prems =>
   472 	[
   473 	(res_inst_tac [("Q","s=UU")] classical2 1),
   474 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   475 	(subgoal_tac "(!n.dnat_take(n)[s]=UU) |(? n.dnat_take(n)[s]=s)" 1),
   476 	(etac disjE 1),
   477 	(eres_inst_tac [("P","s=UU")] notE 1),
   478 	(rtac dnat_take_lemma 1),
   479 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   480 	(atac 1),
   481 	(subgoal_tac "!n.!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s" 1),
   482 	(fast_tac HOL_cs 1),
   483 	(rtac allI 1),
   484 	(rtac dnat_all_finite_lemma1 1)
   485 	]);
   486 
   487 
   488 val dnat_ind = prove_goal Dnat.thy
   489 "[|P(UU);P(dzero);\
   490 \  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
   491 \  |] ==> P(s)"
   492  (fn prems =>
   493 	[
   494 	(rtac (dnat_all_finite_lemma2 RS exE) 1),
   495 	(etac subst 1),
   496 	(rtac (dnat_finite_ind RS spec) 1),
   497 	(REPEAT (resolve_tac prems 1)),
   498 	(REPEAT (atac 1))
   499 	]);
   500 
   501 
   502 val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(dzero)"
   503  (fn prems =>
   504 	[
   505 	(rtac allI 1),
   506 	(res_inst_tac [("s","x")] dnat_ind 1),
   507 	(fast_tac HOL_cs 1),
   508 	(rtac allI 1),
   509 	(res_inst_tac [("n","y")] dnatE 1),
   510 	(fast_tac (HOL_cs addSIs [UU_I]) 1),
   511 	(asm_simp_tac HOLCF_ss 1),
   512 	(asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1),
   513 	(rtac allI 1),
   514 	(res_inst_tac [("n","y")] dnatE 1),
   515 	(fast_tac (HOL_cs addSIs [UU_I]) 1),
   516 	(asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1),
   517 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   518 	(strip_tac 1),
   519 	(subgoal_tac "s1<<xa" 1),
   520 	(etac allE 1),
   521 	(dtac mp 1),
   522 	(atac 1),
   523 	(etac disjE 1),
   524 	(contr_tac 1),
   525 	(asm_simp_tac HOLCF_ss 1),
   526 	(resolve_tac  dnat_invert 1),
   527 	(REPEAT (atac 1))
   528 	]);
   529 
   530 
   531 
   532