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