src/HOLCF/ex/Stream.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 10230 5eb935d6cc69
child 11348 e08a0855af67
permissions -rw-r--r--
` -> $
paulson@9169
     1
(*  Title: 	HOLCF/ex//Stream.ML
paulson@9169
     2
    ID:         $Id$
oheimb@2570
     3
    Author: 	Franz Regensburger, David von Oheimb
oheimb@2570
     4
    Copyright   1993, 1995 Technische Universitaet Muenchen
oheimb@2570
     5
paulson@9169
     6
general Stream domain
oheimb@2570
     7
*)
oheimb@2570
     8
oheimb@4044
     9
fun stream_case_tac s i = res_inst_tac [("x",s)] stream.casedist i
oheimb@2570
    10
			  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
oheimb@2570
    11
oheimb@2570
    12
paulson@9169
    13
val [stream_con_rew1,stream_con_rew2] = stream.con_rews;
paulson@9169
    14
paulson@9248
    15
Addsimps stream.take_rews;
paulson@9248
    16
Addsimps stream.when_rews;
paulson@9248
    17
Addsimps stream.sel_rews;
paulson@9248
    18
oheimb@2570
    19
(* ----------------------------------------------------------------------- *)
oheimb@2570
    20
(* theorems about scons                                                    *)
oheimb@2570
    21
(* ----------------------------------------------------------------------- *)
oheimb@2570
    22
oheimb@2570
    23
section "scons";
oheimb@2570
    24
paulson@9248
    25
Goal "a && s = UU = (a = UU)";
paulson@9248
    26
by Safe_tac;
paulson@10230
    27
by (etac contrapos_pp 1);
paulson@9248
    28
by (safe_tac (claset() addSIs stream.con_rews));
paulson@9248
    29
qed "scons_eq_UU";
oheimb@2570
    30
paulson@9248
    31
Goal "[| a && x = UU; a ~= UU |] ==> R";
paulson@9248
    32
by (dresolve_tac [stream_con_rew2] 1);
paulson@9248
    33
by (contr_tac 1);
paulson@9248
    34
qed "scons_not_empty";
oheimb@2570
    35
paulson@9248
    36
Goal "x ~= UU = (EX a y. a ~= UU &  x = a && y)";
paulson@9248
    37
by (cut_facts_tac [stream.exhaust] 1);
paulson@9248
    38
by (best_tac (claset() addDs [stream_con_rew2]) 1);
paulson@9248
    39
qed "stream_exhaust_eq";
oheimb@2570
    40
paulson@9248
    41
Goal 
paulson@9248
    42
"[| a && s << t; a ~= UU  |] ==> EX b tt. t = b && tt &  b ~= UU &  s << tt";
paulson@9248
    43
by (stream_case_tac "t" 1);
paulson@9248
    44
by (fast_tac (claset() addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1);
paulson@9248
    45
by (fast_tac (claset() addDs stream.inverts) 1);
paulson@9248
    46
qed "stream_prefix";
oheimb@2570
    47
paulson@9248
    48
Goal "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys";
paulson@9248
    49
by (cut_inst_tac [("x1","x::'a::flat"), ("x","y::'a::flat")] 
paulson@9248
    50
                 (ax_flat RS spec RS spec) 1);
paulson@9248
    51
by (forward_tac stream.inverts 1);
paulson@9248
    52
by Safe_tac;
paulson@9248
    53
by (dtac (hd stream.con_rews RS subst) 1);
paulson@9248
    54
by (fast_tac (claset() addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1);
paulson@9248
    55
qed "stream_flat_prefix";
oheimb@2570
    56
paulson@9248
    57
Goal "b ~= UU ==> x << b && z = \
paulson@9248
    58
\           (x = UU |  (EX a y. x = a && y &  a ~= UU &  a << b &  y << z))";
paulson@9248
    59
by Safe_tac;
paulson@9248
    60
by (stream_case_tac "x" 1);
paulson@9248
    61
by (safe_tac (claset() addSDs stream.inverts 
paulson@9248
    62
                addSIs [minimal, monofun_cfun, monofun_cfun_arg]));
paulson@9248
    63
by (Fast_tac 1);
paulson@9248
    64
qed "stream_prefix'";
oheimb@2570
    65
paulson@9248
    66
Goal "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b &  s = t)";
paulson@9248
    67
by (best_tac (claset() addSEs stream.injects) 1);
paulson@9248
    68
qed "stream_inject_eq";	
oheimb@2570
    69
oheimb@2570
    70
oheimb@2570
    71
(* ----------------------------------------------------------------------- *)
oheimb@2570
    72
(* theorems about stream_when                                              *)
oheimb@2570
    73
(* ----------------------------------------------------------------------- *)
oheimb@2570
    74
oheimb@2570
    75
section "stream_when";
oheimb@2570
    76
nipkow@10835
    77
Goal "stream_when$UU$s=UU";
paulson@9248
    78
by (stream_case_tac "s" 1);
paulson@9248
    79
by (ALLGOALS(asm_simp_tac (simpset() addsimps [strict_Rep_CFun1])));
paulson@9248
    80
qed "stream_when_strictf";
oheimb@2570
    81
	
oheimb@2570
    82
oheimb@2570
    83
(* ----------------------------------------------------------------------- *)
oheimb@2570
    84
(* theorems about ft and rt                                                *)
oheimb@2570
    85
(* ----------------------------------------------------------------------- *)
oheimb@2570
    86
oheimb@2570
    87
section "ft & rt";
oheimb@2570
    88
oheimb@2570
    89
(*
nipkow@10835
    90
Goal "ft$s=UU --> s=UU";
paulson@9248
    91
by (stream_case_tac "s" 1);
paulson@9248
    92
by (REPEAT (asm_simp_tac (simpset() addsimps stream.rews) 1));
paulson@9248
    93
qed "stream_ft_lemma1";
oheimb@2570
    94
*)
oheimb@2570
    95
nipkow@10835
    96
Goal "s~=UU ==> ft$s~=UU";
paulson@9248
    97
by (stream_case_tac "s" 1);
paulson@9248
    98
by (Blast_tac 1);
paulson@9248
    99
by (asm_simp_tac (simpset() addsimps stream.rews) 1);
paulson@9248
   100
qed "ft_defin";
oheimb@2570
   101
nipkow@10835
   102
Goal "rt$s~=UU ==> s~=UU";
paulson@9248
   103
by Auto_tac;
paulson@9248
   104
qed "rt_strict_rev";
oheimb@2570
   105
nipkow@10835
   106
Goal "(ft$s)&&(rt$s)=s";
paulson@9248
   107
by (stream_case_tac "s" 1);
paulson@9248
   108
by (ALLGOALS (asm_simp_tac (simpset() addsimps stream.rews)));
paulson@9248
   109
qed "surjectiv_scons";
oheimb@2570
   110
paulson@9248
   111
Goal "ALL x s. x << s --> iterate i rt x << iterate i rt s";
paulson@9248
   112
by (induct_tac "i" 1);
paulson@9248
   113
by (Simp_tac 1);
paulson@9248
   114
by (strip_tac 1);
paulson@9248
   115
by (stream_case_tac "x" 1);
paulson@9248
   116
by (rtac (minimal RS (monofun_iterate2 RS monofunE RS spec RS spec RS mp))1);
paulson@9248
   117
by (dtac stream_prefix 1);
paulson@9248
   118
by Safe_tac;
paulson@9248
   119
by (asm_simp_tac (HOL_ss addsimps iterate_Suc2::stream.rews) 1);
paulson@9248
   120
qed_spec_mp "monofun_rt_mult";
paulson@9248
   121
oheimb@2570
   122
			
oheimb@2570
   123
oheimb@2570
   124
(* ----------------------------------------------------------------------- *)
oheimb@2570
   125
(* theorems about stream_take                                              *)
oheimb@2570
   126
(* ----------------------------------------------------------------------- *)
oheimb@2570
   127
oheimb@2570
   128
section "stream_take";
oheimb@2570
   129
nipkow@10835
   130
Goal  "(LUB i. stream_take i$s) = s";
nipkow@10835
   131
by (subgoal_tac "(LUB i. stream_take i$s) = fix$stream_copy$s" 1);
paulson@9248
   132
by (simp_tac (simpset() addsimps [fix_def2, stream.take_def,
paulson@9248
   133
                                  contlub_cfun_fun, chain_iterate]) 2);
paulson@9248
   134
by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
paulson@9248
   135
qed "stream_reach2";
oheimb@2570
   136
nipkow@10835
   137
Goal "chain (%i. stream_take i$s)";
paulson@9248
   138
by (rtac chainI 1);
nipkow@10835
   139
by (subgoal_tac "ALL i s. stream_take i$s << stream_take (Suc i)$s" 1);
paulson@9248
   140
by (Fast_tac 1);
paulson@9248
   141
by (rtac allI 1);
paulson@9248
   142
by (induct_tac "ia" 1);
paulson@9248
   143
by (Simp_tac 1);
paulson@9248
   144
by (rtac allI 1);
paulson@9248
   145
by (stream_case_tac "s" 1);
paulson@9248
   146
by (Simp_tac 1);
paulson@9248
   147
by (asm_simp_tac (simpset() addsimps [monofun_cfun_arg]) 1);
paulson@9248
   148
qed "chain_stream_take";
oheimb@2570
   149
paulson@9248
   150
paulson@9248
   151
Goalw [stream.take_def]
nipkow@10835
   152
	"stream_take n$x = x ==> stream_take (Suc n)$x = x";
paulson@9248
   153
by (rtac antisym_less 1);
nipkow@10835
   154
by (subgoal_tac "iterate (Suc n) stream_copy UU$x << fix$stream_copy$x" 1);
paulson@9248
   155
by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
paulson@9248
   156
by (rtac monofun_cfun_fun 1);
paulson@9248
   157
by (stac fix_def2 1);
paulson@9248
   158
by (rtac is_ub_thelub 1);
paulson@9248
   159
by (rtac chain_iterate 1);
paulson@9248
   160
by (etac subst 1 THEN rtac monofun_cfun_fun 1);
paulson@9248
   161
by (rtac (rewrite_rule [chain] chain_iterate RS spec) 1);
paulson@9248
   162
qed "stream_take_more";
oheimb@2570
   163
oheimb@2570
   164
(*
paulson@9248
   165
Goal 
nipkow@10835
   166
 "ALL  s2. stream_take n$s2 = s2 --> stream_take (Suc n)$s2=s2";
paulson@9248
   167
by (induct_tac "n" 1);
paulson@9248
   168
by (simp_tac (simpset() addsimps stream_rews) 1);
paulson@9248
   169
by (strip_tac 1);
paulson@9248
   170
by (hyp_subst_tac  1);
paulson@9248
   171
by (simp_tac (simpset() addsimps stream_rews) 1);
paulson@9248
   172
by (rtac allI 1);
paulson@9248
   173
by (res_inst_tac [("s","s2")] streamE 1);
paulson@9248
   174
by (asm_simp_tac (simpset() addsimps stream_rews) 1);
paulson@9248
   175
by (asm_simp_tac (simpset() addsimps stream_rews) 1);
paulson@9248
   176
by (strip_tac 1 );
nipkow@10835
   177
by (subgoal_tac "stream_take n1$xs = xs" 1);
paulson@9248
   178
by (rtac ((hd stream_inject) RS conjunct2) 2);
paulson@9248
   179
by (atac 4);
paulson@9248
   180
by (atac 2);
paulson@9248
   181
by (atac 2);
paulson@9248
   182
by (rtac cfun_arg_cong 1);
paulson@9248
   183
by (Blast_tac 1);
paulson@9248
   184
qed "stream_take_lemma2";
oheimb@2570
   185
*)
oheimb@2570
   186
paulson@9248
   187
Goal 
nipkow@10835
   188
 "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs";
paulson@9248
   189
by (induct_tac "n" 1);
paulson@9248
   190
by (Asm_simp_tac 1);
paulson@9248
   191
by (strip_tac 1);
paulson@9248
   192
by (res_inst_tac [("P","x && xs=UU")] notE 1);
paulson@9248
   193
by (eresolve_tac stream.con_rews 1);
paulson@9248
   194
by (etac sym 1);
paulson@9248
   195
by (strip_tac 1);
paulson@9248
   196
by (rtac stream_take_more 1);
paulson@9248
   197
by (res_inst_tac [("a1","x")] ((hd stream.injects) RS conjunct2) 1);
paulson@9248
   198
by (assume_tac 3);
paulson@9248
   199
by (etac (hd(tl(tl(stream.take_rews))) RS subst) 1);
paulson@9248
   200
by (atac 1);
paulson@9248
   201
qed_spec_mp "stream_take_lemma3";
oheimb@2570
   202
paulson@9248
   203
Goal 
nipkow@10835
   204
 "ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs";
paulson@9248
   205
by (induct_tac "n" 1);
paulson@9248
   206
by Auto_tac;  
paulson@9248
   207
qed_spec_mp "stream_take_lemma4";
oheimb@2570
   208
oheimb@2570
   209
oheimb@2570
   210
(* ------------------------------------------------------------------------- *)
oheimb@2570
   211
(* special induction rules                                                   *)
oheimb@2570
   212
(* ------------------------------------------------------------------------- *)
oheimb@2570
   213
oheimb@2570
   214
section "induction";
oheimb@2570
   215
oheimb@2570
   216
paulson@9248
   217
val prems = Goalw [stream.finite_def]
paulson@9248
   218
 "[| stream_finite x;  \
paulson@9248
   219
\    P UU; \
paulson@9248
   220
\    !!a s. [| a ~= UU; P s |] \
paulson@9248
   221
\ ==> P (a && s) |] ==> P x";
paulson@9248
   222
by (cut_facts_tac prems 1);
paulson@9248
   223
by (etac exE 1);
paulson@9248
   224
by (etac subst 1);
paulson@9248
   225
by (rtac stream.finite_ind 1);
paulson@9248
   226
by (atac 1);
paulson@9248
   227
by (eresolve_tac prems 1);
paulson@9248
   228
by (atac 1);
paulson@9248
   229
qed "stream_finite_ind";
paulson@9248
   230
paulson@9248
   231
val major::prems = Goal
oheimb@2570
   232
"[| P UU;\
oheimb@2570
   233
\   !! x    .    x ~= UU                  ==> P (x      && UU); \
oheimb@2570
   234
\   !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )  \
nipkow@10835
   235
\   |] ==> !s. P (stream_take n$s)";
paulson@9248
   236
by (res_inst_tac [("n","n")] nat_induct2 1);
paulson@9248
   237
by (asm_simp_tac (simpset() addsimps [major]) 1);
paulson@9248
   238
by (rtac allI 1);
paulson@9248
   239
by (stream_case_tac "s" 1);
paulson@9248
   240
by (asm_simp_tac (simpset() addsimps [major]) 1);
paulson@9248
   241
by (asm_simp_tac (simpset() addsimps prems) 1);
paulson@9248
   242
by (rtac allI 1);
paulson@9248
   243
by (stream_case_tac "s" 1);
paulson@9248
   244
by (asm_simp_tac (simpset() addsimps [major]) 1);
paulson@9248
   245
by (res_inst_tac [("x","sa")] stream.casedist 1);
paulson@9248
   246
by (asm_simp_tac (simpset() addsimps prems) 1);
paulson@9248
   247
by (asm_simp_tac (simpset() addsimps prems) 1);
paulson@9248
   248
qed "stream_finite_ind2";
oheimb@2570
   249
oheimb@2570
   250
paulson@9248
   251
val prems = Goal
oheimb@2570
   252
"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); \
oheimb@2570
   253
\   !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s)\
paulson@9248
   254
\ |] ==> P x";
paulson@9248
   255
by (rtac (stream.reach RS subst) 1);
paulson@9248
   256
by (rtac (adm_impl_admw RS wfix_ind) 1);
paulson@9248
   257
by (rtac adm_subst 1);
paulson@9248
   258
by (cont_tacR 1);
paulson@9248
   259
by (resolve_tac prems 1);
paulson@9248
   260
by (rtac allI 1);
paulson@9248
   261
by (rtac (rewrite_rule [stream.take_def] stream_finite_ind2 RS spec) 1);
paulson@9248
   262
by (resolve_tac prems 1);
paulson@9248
   263
by (eresolve_tac prems 1);
paulson@9248
   264
by (eresolve_tac prems 1);
paulson@9248
   265
by (atac 1);
paulson@9248
   266
by (atac 1);
paulson@9248
   267
qed "stream_ind2";
oheimb@2570
   268
oheimb@2570
   269
oheimb@2570
   270
(* ----------------------------------------------------------------------- *)
oheimb@2570
   271
(* simplify use of coinduction                                             *)
oheimb@2570
   272
(* ----------------------------------------------------------------------- *)
oheimb@2570
   273
oheimb@2570
   274
section "coinduction";
oheimb@2570
   275
paulson@9248
   276
paulson@9248
   277
Goalw [stream.bisim_def]
nipkow@10835
   278
"!s1 s2. R s1 s2 --> ft$s1 = ft$s2 &  R (rt$s1) (rt$s2) ==> stream_bisim R";
paulson@9248
   279
by (strip_tac 1);
paulson@9248
   280
by (etac allE 1);
paulson@9248
   281
by (etac allE 1);
paulson@9248
   282
by (dtac mp 1);
paulson@9248
   283
by (atac 1);
paulson@9248
   284
by (etac conjE 1);
paulson@9248
   285
by (case_tac "x = UU & x' = UU" 1);
paulson@9248
   286
by (rtac disjI1 1);
paulson@9248
   287
by (Blast_tac 1);
paulson@9248
   288
by (rtac disjI2 1);
paulson@9248
   289
by (rtac disjE 1);
paulson@9248
   290
by (etac (de_Morgan_conj RS subst) 1);
nipkow@10835
   291
by (res_inst_tac [("x","ft$x")] exI 1);
nipkow@10835
   292
by (res_inst_tac [("x","rt$x")] exI 1);
nipkow@10835
   293
by (res_inst_tac [("x","rt$x'")] exI 1);
paulson@9248
   294
by (rtac conjI 1);
paulson@9248
   295
by (etac ft_defin 1);
paulson@9248
   296
by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
nipkow@10835
   297
by (eres_inst_tac [("s","ft$x"),("t","ft$x'")] subst 1);
paulson@9248
   298
by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
nipkow@10835
   299
by (res_inst_tac [("x","ft$x'")] exI 1);
nipkow@10835
   300
by (res_inst_tac [("x","rt$x")] exI 1);
nipkow@10835
   301
by (res_inst_tac [("x","rt$x'")] exI 1);
paulson@9248
   302
by (rtac conjI 1);
paulson@9248
   303
by (etac ft_defin 1);
paulson@9248
   304
by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
nipkow@10835
   305
by (res_inst_tac [("s","ft$x"),("t","ft$x'")] ssubst 1);
paulson@9248
   306
by (etac sym 1);
paulson@9248
   307
by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
paulson@9248
   308
qed "stream_coind_lemma2";
oheimb@2570
   309
oheimb@2570
   310
(* ----------------------------------------------------------------------- *)
oheimb@2570
   311
(* theorems about stream_finite                                            *)
oheimb@2570
   312
(* ----------------------------------------------------------------------- *)
oheimb@2570
   313
oheimb@2570
   314
section "stream_finite";
oheimb@2570
   315
paulson@9248
   316
paulson@9248
   317
Goalw [stream.finite_def] "stream_finite UU";
paulson@9248
   318
by (rtac exI 1);
paulson@9248
   319
by (simp_tac (simpset() addsimps stream.rews) 1);
paulson@9248
   320
qed "stream_finite_UU";
oheimb@2570
   321
paulson@9248
   322
Goal  "~  stream_finite s ==> s ~= UU";
paulson@9248
   323
by (blast_tac (claset() addIs [stream_finite_UU]) 1);
paulson@9248
   324
qed "stream_finite_UU_rev";
oheimb@2570
   325
paulson@9248
   326
Goalw [stream.finite_def] "stream_finite xs ==> stream_finite (x && xs)";
paulson@9248
   327
by (blast_tac (claset() addIs [stream_take_lemma4]) 1);
paulson@9248
   328
qed "stream_finite_lemma1";
paulson@9248
   329
paulson@9248
   330
Goalw [stream.finite_def]
paulson@9248
   331
 "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs";
paulson@9248
   332
by (blast_tac (claset() addIs [stream_take_lemma3]) 1);
paulson@9248
   333
qed "stream_finite_lemma2";
oheimb@2570
   334
nipkow@10835
   335
Goal "stream_finite (rt$s) = stream_finite s";
paulson@9248
   336
by (stream_case_tac "s" 1);
paulson@9248
   337
by (simp_tac (simpset() addsimps [stream_finite_UU]) 1);
paulson@9248
   338
by (Asm_simp_tac 1);
paulson@9248
   339
by (fast_tac (claset() addIs [stream_finite_lemma1] 
paulson@9248
   340
                       addDs [stream_finite_lemma2]) 1);
paulson@9248
   341
qed "stream_finite_rt_eq";
oheimb@2570
   342
paulson@9248
   343
Goal "stream_finite s ==> !t. t<<s --> stream_finite t";
paulson@9248
   344
by (eres_inst_tac [("x","s")] stream_finite_ind 1);
paulson@9248
   345
by (strip_tac 1); 
paulson@9248
   346
by (dtac UU_I 1);
paulson@9248
   347
by (asm_simp_tac (simpset() addsimps [stream_finite_UU]) 1);
paulson@9248
   348
by (strip_tac 1);
paulson@9248
   349
by (asm_full_simp_tac (simpset() addsimps [stream_prefix']) 1);
paulson@9248
   350
by (fast_tac (claset() addSIs [stream_finite_UU, stream_finite_lemma1]) 1);
paulson@9248
   351
qed_spec_mp "stream_finite_less";
oheimb@2570
   352
paulson@9248
   353
Goal "adm (%x. ~  stream_finite x)";
paulson@9248
   354
by (rtac admI2 1);
paulson@9248
   355
by (best_tac (claset() addIs [stream_finite_less, is_ub_thelub]) 1);
paulson@9248
   356
qed "adm_not_stream_finite";