src/HOLCF/explicit_domains/Dnat.ML
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/explicit_domains/Dnat.ML	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,534 +0,0 @@
     1.4 -(*  Title:      HOLCF/Dnat.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Franz Regensburger
     1.7 -    Copyright   1993 Technische Universitaet Muenchen
     1.8 -
     1.9 -Lemmas for dnat.thy 
    1.10 -*)
    1.11 -
    1.12 -open Dnat;
    1.13 -
    1.14 -(* ------------------------------------------------------------------------*)
    1.15 -(* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict               *)
    1.16 -(* ------------------------------------------------------------------------*)
    1.17 -
    1.18 -val dnat_iso_strict = dnat_rep_iso RS (dnat_abs_iso RS 
    1.19 -        (allI  RSN (2,allI RS iso_strict)));
    1.20 -
    1.21 -val dnat_rews = [dnat_iso_strict RS conjunct1,
    1.22 -                dnat_iso_strict RS conjunct2];
    1.23 -
    1.24 -(* ------------------------------------------------------------------------*)
    1.25 -(* Properties of dnat_copy                                                 *)
    1.26 -(* ------------------------------------------------------------------------*)
    1.27 -
    1.28 -fun prover defs thm =  prove_goalw Dnat.thy defs thm
    1.29 - (fn prems =>
    1.30 -        [
    1.31 -        (cut_facts_tac prems 1),
    1.32 -        (asm_simp_tac (!simpset addsimps 
    1.33 -                (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
    1.34 -        ]);
    1.35 -
    1.36 -val dnat_copy = 
    1.37 -        [
    1.38 -        prover [dnat_copy_def] "dnat_copy`f`UU=UU",
    1.39 -        prover [dnat_copy_def,dzero_def] "dnat_copy`f`dzero= dzero",
    1.40 -        prover [dnat_copy_def,dsucc_def] 
    1.41 -                "n~=UU ==> dnat_copy`f`(dsucc`n) = dsucc`(f`n)"
    1.42 -        ];
    1.43 -
    1.44 -val dnat_rews =  dnat_copy @ dnat_rews; 
    1.45 -
    1.46 -(* ------------------------------------------------------------------------*)
    1.47 -(* Exhaustion and elimination for dnat                                     *)
    1.48 -(* ------------------------------------------------------------------------*)
    1.49 -
    1.50 -qed_goalw "Exh_dnat" Dnat.thy [dsucc_def,dzero_def]
    1.51 -        "n = UU | n = dzero | (? x . x~=UU & n = dsucc`x)"
    1.52 - (fn prems =>
    1.53 -        [
    1.54 -        (Simp_tac  1),
    1.55 -        (rtac (dnat_rep_iso RS subst) 1),
    1.56 -        (res_inst_tac [("p","dnat_rep`n")] ssumE 1),
    1.57 -        (rtac disjI1 1),
    1.58 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
    1.59 -        (rtac (disjI1 RS disjI2) 1),
    1.60 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
    1.61 -        (res_inst_tac [("p","x")] oneE 1),
    1.62 -        (contr_tac 1),
    1.63 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
    1.64 -        (rtac (disjI2 RS disjI2) 1),
    1.65 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
    1.66 -        (fast_tac HOL_cs 1)
    1.67 -        ]);
    1.68 -
    1.69 -qed_goal "dnatE" Dnat.thy 
    1.70 - "[| n=UU ==> Q; n=dzero ==> Q; !!x.[|n=dsucc`x;x~=UU|]==>Q|]==>Q"
    1.71 - (fn prems =>
    1.72 -        [
    1.73 -        (rtac (Exh_dnat RS disjE) 1),
    1.74 -        (eresolve_tac prems 1),
    1.75 -        (etac disjE 1),
    1.76 -        (eresolve_tac prems 1),
    1.77 -        (REPEAT (etac exE 1)),
    1.78 -        (resolve_tac prems 1),
    1.79 -        (fast_tac HOL_cs 1),
    1.80 -        (fast_tac HOL_cs 1)
    1.81 -        ]);
    1.82 -
    1.83 -(* ------------------------------------------------------------------------*)
    1.84 -(* Properties of dnat_when                                                 *)
    1.85 -(* ------------------------------------------------------------------------*)
    1.86 -
    1.87 -fun prover defs thm =  prove_goalw Dnat.thy defs thm
    1.88 - (fn prems =>
    1.89 -        [
    1.90 -        (cut_facts_tac prems 1),
    1.91 -        (asm_simp_tac (!simpset addsimps 
    1.92 -                (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
    1.93 -        ]);
    1.94 -
    1.95 -
    1.96 -val dnat_when = [
    1.97 -        prover [dnat_when_def] "dnat_when`c`f`UU=UU",
    1.98 -        prover [dnat_when_def,dzero_def] "dnat_when`c`f`dzero=c",
    1.99 -        prover [dnat_when_def,dsucc_def] 
   1.100 -                "n~=UU ==> dnat_when`c`f`(dsucc`n)=f`n"
   1.101 -        ];
   1.102 -
   1.103 -val dnat_rews = dnat_when @ dnat_rews;
   1.104 -
   1.105 -(* ------------------------------------------------------------------------*)
   1.106 -(* Rewrites for  discriminators and  selectors                             *)
   1.107 -(* ------------------------------------------------------------------------*)
   1.108 -
   1.109 -fun prover defs thm = prove_goalw Dnat.thy defs thm
   1.110 - (fn prems =>
   1.111 -        [
   1.112 -        (simp_tac (!simpset addsimps dnat_rews) 1)
   1.113 -        ]);
   1.114 -
   1.115 -val dnat_discsel = [
   1.116 -        prover [is_dzero_def] "is_dzero`UU=UU",
   1.117 -        prover [is_dsucc_def] "is_dsucc`UU=UU",
   1.118 -        prover [dpred_def] "dpred`UU=UU"
   1.119 -        ];
   1.120 -
   1.121 -
   1.122 -fun prover defs thm = prove_goalw Dnat.thy defs thm
   1.123 - (fn prems =>
   1.124 -        [
   1.125 -        (cut_facts_tac prems 1),
   1.126 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   1.127 -        ]);
   1.128 -
   1.129 -val dnat_discsel = [
   1.130 -        prover [is_dzero_def] "is_dzero`dzero=TT",
   1.131 -        prover [is_dzero_def] "n~=UU ==>is_dzero`(dsucc`n)=FF",
   1.132 -        prover [is_dsucc_def] "is_dsucc`dzero=FF",
   1.133 -        prover [is_dsucc_def] "n~=UU ==> is_dsucc`(dsucc`n)=TT",
   1.134 -        prover [dpred_def] "dpred`dzero=UU",
   1.135 -        prover [dpred_def] "n~=UU ==> dpred`(dsucc`n)=n"
   1.136 -        ] @ dnat_discsel;
   1.137 -
   1.138 -val dnat_rews = dnat_discsel @ dnat_rews;
   1.139 -
   1.140 -(* ------------------------------------------------------------------------*)
   1.141 -(* Definedness and strictness                                              *)
   1.142 -(* ------------------------------------------------------------------------*)
   1.143 -
   1.144 -fun prover contr thm = prove_goal Dnat.thy thm
   1.145 - (fn prems =>
   1.146 -        [
   1.147 -        (res_inst_tac [("P1",contr)] classical2 1),
   1.148 -        (simp_tac (!simpset addsimps dnat_rews) 1),
   1.149 -        (dtac sym 1),
   1.150 -        (Asm_simp_tac  1),
   1.151 -        (simp_tac (!simpset addsimps (prems @ dnat_rews)) 1)
   1.152 -        ]);
   1.153 -
   1.154 -val dnat_constrdef = [
   1.155 -        prover "is_dzero`UU ~= UU" "dzero~=UU",
   1.156 -        prover "is_dsucc`UU ~= UU" "n~=UU ==> dsucc`n~=UU"
   1.157 -        ]; 
   1.158 -
   1.159 -
   1.160 -fun prover defs thm = prove_goalw Dnat.thy defs thm
   1.161 - (fn prems =>
   1.162 -        [
   1.163 -        (simp_tac (!simpset addsimps dnat_rews) 1)
   1.164 -        ]);
   1.165 -
   1.166 -val dnat_constrdef = [
   1.167 -        prover [dsucc_def] "dsucc`UU=UU"
   1.168 -        ] @ dnat_constrdef;
   1.169 -
   1.170 -val dnat_rews = dnat_constrdef @ dnat_rews;
   1.171 -
   1.172 -
   1.173 -(* ------------------------------------------------------------------------*)
   1.174 -(* Distinctness wrt. << and =                                              *)
   1.175 -(* ------------------------------------------------------------------------*)
   1.176 -
   1.177 -val temp = prove_goal Dnat.thy  "~dzero << dsucc`n"
   1.178 - (fn prems =>
   1.179 -        [
   1.180 -        (res_inst_tac [("P1","TT << FF")] classical2 1),
   1.181 -        (resolve_tac dist_less_tr 1),
   1.182 -        (dres_inst_tac [("fo","is_dzero")] monofun_cfun_arg 1),
   1.183 -        (etac box_less 1),
   1.184 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.185 -        (case_tac "n=UU" 1),
   1.186 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.187 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   1.188 -        ]);
   1.189 -
   1.190 -val dnat_dist_less = [temp];
   1.191 -
   1.192 -val temp = prove_goal Dnat.thy  "n~=UU ==> ~dsucc`n << dzero"
   1.193 - (fn prems =>
   1.194 -        [
   1.195 -        (cut_facts_tac prems 1),
   1.196 -        (res_inst_tac [("P1","TT << FF")] classical2 1),
   1.197 -        (resolve_tac dist_less_tr 1),
   1.198 -        (dres_inst_tac [("fo","is_dsucc")] monofun_cfun_arg 1),
   1.199 -        (etac box_less 1),
   1.200 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.201 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   1.202 -        ]);
   1.203 -
   1.204 -val dnat_dist_less = temp::dnat_dist_less;
   1.205 -
   1.206 -val temp = prove_goal Dnat.thy   "dzero ~= dsucc`n"
   1.207 - (fn prems =>
   1.208 -        [
   1.209 -        (case_tac "n=UU" 1),
   1.210 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.211 -        (res_inst_tac [("P1","TT = FF")] classical2 1),
   1.212 -        (resolve_tac dist_eq_tr 1),
   1.213 -        (dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
   1.214 -        (etac box_equals 1),
   1.215 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.216 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   1.217 -        ]);
   1.218 -
   1.219 -val dnat_dist_eq = [temp, temp RS not_sym];
   1.220 -
   1.221 -val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews;
   1.222 -
   1.223 -(* ------------------------------------------------------------------------*)
   1.224 -(* Invertibility                                                           *)
   1.225 -(* ------------------------------------------------------------------------*)
   1.226 -
   1.227 -val dnat_invert = 
   1.228 -        [
   1.229 -prove_goal Dnat.thy 
   1.230 -"[|x1~=UU; y1~=UU; dsucc`x1 << dsucc`y1 |] ==> x1<< y1"
   1.231 - (fn prems =>
   1.232 -        [
   1.233 -        (cut_facts_tac prems 1),
   1.234 -        (dres_inst_tac [("fo","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
   1.235 -        (etac box_less 1),
   1.236 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.237 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   1.238 -        ])
   1.239 -        ];
   1.240 -
   1.241 -(* ------------------------------------------------------------------------*)
   1.242 -(* Injectivity                                                             *)
   1.243 -(* ------------------------------------------------------------------------*)
   1.244 -
   1.245 -val dnat_inject = 
   1.246 -        [
   1.247 -prove_goal Dnat.thy 
   1.248 -"[|x1~=UU; y1~=UU; dsucc`x1 = dsucc`y1 |] ==> x1= y1"
   1.249 - (fn prems =>
   1.250 -        [
   1.251 -        (cut_facts_tac prems 1),
   1.252 -        (dres_inst_tac [("f","dnat_when`c`(LAM x.x)")] cfun_arg_cong 1),
   1.253 -        (etac box_equals 1),
   1.254 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.255 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   1.256 -        ])
   1.257 -        ];
   1.258 -
   1.259 -(* ------------------------------------------------------------------------*)
   1.260 -(* definedness for  discriminators and  selectors                          *)
   1.261 -(* ------------------------------------------------------------------------*)
   1.262 -
   1.263 -
   1.264 -fun prover thm = prove_goal Dnat.thy thm
   1.265 - (fn prems =>
   1.266 -        [
   1.267 -        (cut_facts_tac prems 1),
   1.268 -        (rtac dnatE 1),
   1.269 -        (contr_tac 1),
   1.270 -        (REPEAT (asm_simp_tac (!simpset addsimps dnat_rews) 1))
   1.271 -        ]);
   1.272 -
   1.273 -val dnat_discsel_def = 
   1.274 -        [
   1.275 -        prover  "n~=UU ==> is_dzero`n ~= UU",
   1.276 -        prover  "n~=UU ==> is_dsucc`n ~= UU"
   1.277 -        ];
   1.278 -
   1.279 -val dnat_rews = dnat_discsel_def @ dnat_rews;
   1.280 -
   1.281 - 
   1.282 -(* ------------------------------------------------------------------------*)
   1.283 -(* Properties dnat_take                                                    *)
   1.284 -(* ------------------------------------------------------------------------*)
   1.285 -val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take n`UU = UU"
   1.286 - (fn prems =>
   1.287 -        [
   1.288 -        (res_inst_tac [("n","n")] natE 1),
   1.289 -        (Asm_simp_tac 1),
   1.290 -        (Asm_simp_tac 1),
   1.291 -        (simp_tac (!simpset addsimps dnat_rews) 1)
   1.292 -        ]);
   1.293 -
   1.294 -val dnat_take = [temp];
   1.295 -
   1.296 -val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take 0`xs = UU"
   1.297 - (fn prems =>
   1.298 -        [
   1.299 -        (Asm_simp_tac 1)
   1.300 -        ]);
   1.301 -
   1.302 -val dnat_take = temp::dnat_take;
   1.303 -
   1.304 -val temp = prove_goalw Dnat.thy [dnat_take_def]
   1.305 -        "dnat_take (Suc n)`dzero=dzero"
   1.306 - (fn prems =>
   1.307 -        [
   1.308 -        (Asm_simp_tac 1),
   1.309 -        (simp_tac (!simpset addsimps dnat_rews) 1)
   1.310 -        ]);
   1.311 -
   1.312 -val dnat_take = temp::dnat_take;
   1.313 -
   1.314 -val temp = prove_goalw Dnat.thy [dnat_take_def]
   1.315 -  "dnat_take (Suc n)`(dsucc`xs)=dsucc`(dnat_take n ` xs)"
   1.316 - (fn prems =>
   1.317 -        [
   1.318 -        (case_tac "xs=UU" 1),
   1.319 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.320 -        (Asm_simp_tac 1),
   1.321 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.322 -        (res_inst_tac [("n","n")] natE 1),
   1.323 -        (Asm_simp_tac 1),
   1.324 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.325 -        (Asm_simp_tac 1),
   1.326 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.327 -        (Asm_simp_tac 1),
   1.328 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   1.329 -        ]);
   1.330 -
   1.331 -val dnat_take = temp::dnat_take;
   1.332 -
   1.333 -val dnat_rews = dnat_take @ dnat_rews;
   1.334 -
   1.335 -
   1.336 -(* ------------------------------------------------------------------------*)
   1.337 -(* take lemma for dnats                                                  *)
   1.338 -(* ------------------------------------------------------------------------*)
   1.339 -
   1.340 -fun prover reach defs thm  = prove_goalw Dnat.thy defs thm
   1.341 - (fn prems =>
   1.342 -        [
   1.343 -        (res_inst_tac [("t","s1")] (reach RS subst) 1),
   1.344 -        (res_inst_tac [("t","s2")] (reach RS subst) 1),
   1.345 -        (stac fix_def2 1),
   1.346 -        (stac contlub_cfun_fun 1),
   1.347 -        (rtac is_chain_iterate 1),
   1.348 -        (stac contlub_cfun_fun 1),
   1.349 -        (rtac is_chain_iterate 1),
   1.350 -        (rtac lub_equal 1),
   1.351 -        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
   1.352 -        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
   1.353 -        (rtac allI 1),
   1.354 -        (resolve_tac prems 1)
   1.355 -        ]);
   1.356 -
   1.357 -val dnat_take_lemma = prover dnat_reach  [dnat_take_def]
   1.358 -        "(!!n.dnat_take n`s1 = dnat_take n`s2) ==> s1=s2";
   1.359 -
   1.360 -
   1.361 -(* ------------------------------------------------------------------------*)
   1.362 -(* Co -induction for dnats                                                 *)
   1.363 -(* ------------------------------------------------------------------------*)
   1.364 -
   1.365 -qed_goalw "dnat_coind_lemma" Dnat.thy [dnat_bisim_def] 
   1.366 -"dnat_bisim R ==> ! p q. R p q --> dnat_take n`p = dnat_take n`q"
   1.367 - (fn prems =>
   1.368 -        [
   1.369 -        (cut_facts_tac prems 1),
   1.370 -        (nat_ind_tac "n" 1),
   1.371 -        (simp_tac (!simpset addsimps dnat_take) 1),
   1.372 -        (strip_tac 1),
   1.373 -        ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
   1.374 -        (atac 1),
   1.375 -        (asm_simp_tac (!simpset addsimps dnat_take) 1),
   1.376 -        (etac disjE 1),
   1.377 -        (asm_simp_tac (!simpset addsimps dnat_take) 1),
   1.378 -        (etac exE 1),
   1.379 -        (etac exE 1),
   1.380 -        (asm_simp_tac (!simpset addsimps dnat_take) 1),
   1.381 -        (REPEAT (etac conjE 1)),
   1.382 -        (rtac cfun_arg_cong 1),
   1.383 -        (fast_tac HOL_cs 1)
   1.384 -        ]);
   1.385 -
   1.386 -qed_goal "dnat_coind" Dnat.thy "[|dnat_bisim R;R p q|] ==> p = q"
   1.387 - (fn prems =>
   1.388 -        [
   1.389 -        (rtac dnat_take_lemma 1),
   1.390 -        (rtac (dnat_coind_lemma RS spec RS spec RS mp) 1),
   1.391 -        (resolve_tac prems 1),
   1.392 -        (resolve_tac prems 1)
   1.393 -        ]);
   1.394 -
   1.395 -
   1.396 -(* ------------------------------------------------------------------------*)
   1.397 -(* structural induction for admissible predicates                          *)
   1.398 -(* ------------------------------------------------------------------------*)
   1.399 -
   1.400 -(* not needed any longer
   1.401 -qed_goal "dnat_ind" Dnat.thy
   1.402 -"[| adm(P);\
   1.403 -\   P(UU);\
   1.404 -\   P(dzero);\
   1.405 -\   !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc`s1)|] ==> P(s)"
   1.406 - (fn prems =>
   1.407 -        [
   1.408 -        (rtac (dnat_reach RS subst) 1),
   1.409 -        (res_inst_tac [("x","s")] spec 1),
   1.410 -        (rtac fix_ind 1),
   1.411 -        (rtac adm_all2 1),
   1.412 -        (rtac adm_subst 1),
   1.413 -        (cont_tacR 1),
   1.414 -        (resolve_tac prems 1),
   1.415 -        (Simp_tac 1),
   1.416 -        (resolve_tac prems 1),
   1.417 -        (strip_tac 1),
   1.418 -        (res_inst_tac [("n","xa")] dnatE 1),
   1.419 -        (asm_simp_tac (!simpset addsimps dnat_copy) 1),
   1.420 -        (resolve_tac prems 1),
   1.421 -        (asm_simp_tac (!simpset addsimps dnat_copy) 1),
   1.422 -        (resolve_tac prems 1),
   1.423 -        (asm_simp_tac (!simpset addsimps dnat_copy) 1),
   1.424 -        (case_tac "x`xb=UU" 1),
   1.425 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.426 -        (resolve_tac prems 1),
   1.427 -        (eresolve_tac prems 1),
   1.428 -        (etac spec 1)
   1.429 -        ]);
   1.430 -*)
   1.431 -
   1.432 -qed_goal "dnat_finite_ind" Dnat.thy
   1.433 -"[|P(UU);P(dzero);\
   1.434 -\  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\
   1.435 -\  |] ==> !s.P(dnat_take n`s)"
   1.436 - (fn prems =>
   1.437 -        [
   1.438 -        (nat_ind_tac "n" 1),
   1.439 -        (simp_tac (!simpset addsimps dnat_rews) 1),
   1.440 -        (resolve_tac prems 1),
   1.441 -        (rtac allI 1),
   1.442 -        (res_inst_tac [("n","s")] dnatE 1),
   1.443 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.444 -        (resolve_tac prems 1),
   1.445 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.446 -        (resolve_tac prems 1),
   1.447 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.448 -        (case_tac "dnat_take n1`x=UU" 1),
   1.449 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.450 -        (resolve_tac prems 1),
   1.451 -        (resolve_tac prems 1),
   1.452 -        (atac 1),
   1.453 -        (etac spec 1)
   1.454 -        ]);
   1.455 -
   1.456 -qed_goal "dnat_all_finite_lemma1" Dnat.thy
   1.457 -"!s.dnat_take n`s=UU |dnat_take n`s=s"
   1.458 - (fn prems =>
   1.459 -        [
   1.460 -        (nat_ind_tac "n" 1),
   1.461 -        (simp_tac (!simpset addsimps dnat_rews) 1),
   1.462 -        (rtac allI 1),
   1.463 -        (res_inst_tac [("n","s")] dnatE 1),
   1.464 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.465 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.466 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.467 -        (eres_inst_tac [("x","x")] allE 1),
   1.468 -        (etac disjE 1),
   1.469 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.470 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   1.471 -        ]);
   1.472 -
   1.473 -qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take n`s=s"
   1.474 - (fn prems =>
   1.475 -        [
   1.476 -        (case_tac "s=UU" 1),
   1.477 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.478 -        (subgoal_tac "(!n.dnat_take(n)`s=UU) |(? n.dnat_take(n)`s=s)" 1),
   1.479 -        (etac disjE 1),
   1.480 -        (eres_inst_tac [("P","s=UU")] notE 1),
   1.481 -        (rtac dnat_take_lemma 1),
   1.482 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.483 -        (atac 1),
   1.484 -        (subgoal_tac "!n.!s.dnat_take(n)`s=UU |dnat_take(n)`s=s" 1),
   1.485 -        (fast_tac HOL_cs 1),
   1.486 -        (rtac allI 1),
   1.487 -        (rtac dnat_all_finite_lemma1 1)
   1.488 -        ]);
   1.489 -
   1.490 -
   1.491 -qed_goal "dnat_ind" Dnat.thy
   1.492 -"[|P(UU);P(dzero);\
   1.493 -\  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\
   1.494 -\  |] ==> P(s)"
   1.495 - (fn prems =>
   1.496 -        [
   1.497 -        (rtac (dnat_all_finite_lemma2 RS exE) 1),
   1.498 -        (etac subst 1),
   1.499 -        (rtac (dnat_finite_ind RS spec) 1),
   1.500 -        (REPEAT (resolve_tac prems 1)),
   1.501 -        (REPEAT (atac 1))
   1.502 -        ]);
   1.503 -
   1.504 -
   1.505 -qed_goalw "dnat_flat" Dnat.thy [flat_def] "flat(dzero)"
   1.506 - (fn prems =>
   1.507 -        [
   1.508 -        (rtac allI 1),
   1.509 -        (res_inst_tac [("s","x")] dnat_ind 1),
   1.510 -        (fast_tac HOL_cs 1),
   1.511 -        (rtac allI 1),
   1.512 -        (res_inst_tac [("n","y")] dnatE 1),
   1.513 -        (fast_tac (HOL_cs addSIs [UU_I]) 1),
   1.514 -        (Asm_simp_tac 1),
   1.515 -        (asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
   1.516 -        (rtac allI 1),
   1.517 -        (res_inst_tac [("n","y")] dnatE 1),
   1.518 -        (fast_tac (HOL_cs addSIs [UU_I]) 1),
   1.519 -        (asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
   1.520 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   1.521 -        (strip_tac 1),
   1.522 -        (subgoal_tac "s1<<xa" 1),
   1.523 -        (etac allE 1),
   1.524 -        (dtac mp 1),
   1.525 -        (atac 1),
   1.526 -        (etac disjE 1),
   1.527 -        (contr_tac 1),
   1.528 -        (Asm_simp_tac 1),
   1.529 -        (resolve_tac  dnat_invert 1),
   1.530 -        (REPEAT (atac 1))
   1.531 -        ]);
   1.532 -
   1.533 -
   1.534 -
   1.535 -
   1.536 -
   1.537 -