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