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