src/HOLCF/IOA/meta_theory/Sequence.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 9877 b2a62260f8ac
child 12028 52aa183c15bb
permissions -rw-r--r--
` -> $
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/Sequence.ML
mueller@3275
     2
    ID:         $Id$
mueller@3071
     3
    Author:     Olaf M"uller
mueller@3071
     4
    Copyright   1996  TU Muenchen
mueller@3071
     5
mueller@3071
     6
Theorems about Sequences over flat domains with lifted elements
mueller@3071
     7
mueller@3071
     8
*)
mueller@3071
     9
mueller@3656
    10
mueller@3071
    11
Addsimps [andalso_and,andalso_or];
mueller@3071
    12
mueller@3071
    13
(* ----------------------------------------------------------------------------------- *)
mueller@3071
    14
mueller@3071
    15
section "recursive equations of operators";
mueller@3071
    16
mueller@3071
    17
(* ---------------------------------------------------------------- *)
mueller@3071
    18
(*                               Map                                *)
mueller@3071
    19
(* ---------------------------------------------------------------- *)
mueller@3071
    20
nipkow@10835
    21
Goal "Map f$UU =UU";
wenzelm@4098
    22
by (simp_tac (simpset() addsimps [Map_def]) 1);
mueller@3071
    23
qed"Map_UU";
mueller@3071
    24
nipkow@10835
    25
Goal "Map f$nil =nil";
wenzelm@4098
    26
by (simp_tac (simpset() addsimps [Map_def]) 1);
mueller@3071
    27
qed"Map_nil";
mueller@3071
    28
nipkow@10835
    29
Goal "Map f$(x>>xs)=(f x) >> Map f$xs";
wenzelm@7229
    30
by (simp_tac (simpset() addsimps [Map_def, Consq_def,flift2_def]) 1);
mueller@3071
    31
qed"Map_cons";
mueller@3071
    32
mueller@3071
    33
(* ---------------------------------------------------------------- *)
mueller@3071
    34
(*                               Filter                             *)
mueller@3071
    35
(* ---------------------------------------------------------------- *)
mueller@3071
    36
nipkow@10835
    37
Goal "Filter P$UU =UU";
wenzelm@4098
    38
by (simp_tac (simpset() addsimps [Filter_def]) 1);
mueller@3071
    39
qed"Filter_UU";
mueller@3071
    40
nipkow@10835
    41
Goal "Filter P$nil =nil";
wenzelm@4098
    42
by (simp_tac (simpset() addsimps [Filter_def]) 1);
mueller@3071
    43
qed"Filter_nil";
mueller@3071
    44
nipkow@10835
    45
Goal "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)"; 
wenzelm@7229
    46
by (simp_tac (simpset() addsimps [Filter_def, Consq_def,flift2_def,If_and_if]) 1);
mueller@3071
    47
qed"Filter_cons";
mueller@3071
    48
mueller@3071
    49
(* ---------------------------------------------------------------- *)
mueller@3071
    50
(*                               Forall                             *)
mueller@3071
    51
(* ---------------------------------------------------------------- *)
mueller@3071
    52
wenzelm@5068
    53
Goal "Forall P UU";
wenzelm@4098
    54
by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
mueller@3071
    55
qed"Forall_UU";
mueller@3071
    56
wenzelm@5068
    57
Goal "Forall P nil";
wenzelm@4098
    58
by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
mueller@3071
    59
qed"Forall_nil";
mueller@3071
    60
wenzelm@5068
    61
Goal "Forall P (x>>xs)= (P x & Forall P xs)";
wenzelm@4098
    62
by (simp_tac (simpset() addsimps [Forall_def, sforall_def,
wenzelm@7229
    63
                                 Consq_def,flift2_def]) 1);
mueller@3071
    64
qed"Forall_cons";
mueller@3071
    65
mueller@3071
    66
(* ---------------------------------------------------------------- *)
mueller@3071
    67
(*                               Conc                               *)
mueller@3071
    68
(* ---------------------------------------------------------------- *)
mueller@3071
    69
mueller@3071
    70
wenzelm@5068
    71
Goal "(x>>xs) @@ y = x>>(xs @@y)"; 
wenzelm@7229
    72
by (simp_tac (simpset() addsimps [Consq_def]) 1);
mueller@3071
    73
qed"Conc_cons";
mueller@3071
    74
mueller@3071
    75
(* ---------------------------------------------------------------- *)
mueller@3071
    76
(*                               Takewhile                          *)
mueller@3071
    77
(* ---------------------------------------------------------------- *)
mueller@3071
    78
nipkow@10835
    79
Goal "Takewhile P$UU =UU";
wenzelm@4098
    80
by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
mueller@3071
    81
qed"Takewhile_UU";
mueller@3071
    82
nipkow@10835
    83
Goal "Takewhile P$nil =nil";
wenzelm@4098
    84
by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
mueller@3071
    85
qed"Takewhile_nil";
mueller@3071
    86
nipkow@10835
    87
Goal "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)"; 
wenzelm@7229
    88
by (simp_tac (simpset() addsimps [Takewhile_def, Consq_def,flift2_def,If_and_if]) 1);
mueller@3071
    89
qed"Takewhile_cons";
mueller@3071
    90
mueller@3071
    91
(* ---------------------------------------------------------------- *)
mueller@3071
    92
(*                               Dropwhile                          *)
mueller@3071
    93
(* ---------------------------------------------------------------- *)
mueller@3071
    94
nipkow@10835
    95
Goal "Dropwhile P$UU =UU";
wenzelm@4098
    96
by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
mueller@3071
    97
qed"Dropwhile_UU";
mueller@3071
    98
nipkow@10835
    99
Goal "Dropwhile P$nil =nil";
wenzelm@4098
   100
by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
mueller@3071
   101
qed"Dropwhile_nil";
mueller@3071
   102
nipkow@10835
   103
Goal "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)"; 
wenzelm@7229
   104
by (simp_tac (simpset() addsimps [Dropwhile_def, Consq_def,flift2_def,If_and_if]) 1);
mueller@3071
   105
qed"Dropwhile_cons";
mueller@3071
   106
mueller@3071
   107
(* ---------------------------------------------------------------- *)
mueller@3071
   108
(*                               Last                               *)
mueller@3071
   109
(* ---------------------------------------------------------------- *)
mueller@3071
   110
mueller@3071
   111
nipkow@10835
   112
Goal "Last$UU =UU";
wenzelm@4098
   113
by (simp_tac (simpset() addsimps [Last_def]) 1);
mueller@3071
   114
qed"Last_UU";
mueller@3071
   115
nipkow@10835
   116
Goal "Last$nil =UU";
wenzelm@4098
   117
by (simp_tac (simpset() addsimps [Last_def]) 1);
mueller@3071
   118
qed"Last_nil";
mueller@3071
   119
nipkow@10835
   120
Goal "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"; 
wenzelm@7229
   121
by (simp_tac (simpset() addsimps [Last_def, Consq_def]) 1);
oheimb@4042
   122
by (res_inst_tac [("x","xs")] seq.casedist 1);
nipkow@4833
   123
by (Asm_simp_tac 1);
mueller@3071
   124
by (REPEAT (Asm_simp_tac 1));
mueller@3071
   125
qed"Last_cons";
mueller@3071
   126
mueller@3071
   127
mueller@3071
   128
(* ---------------------------------------------------------------- *)
mueller@3071
   129
(*                               Flat                               *)
mueller@3071
   130
(* ---------------------------------------------------------------- *)
mueller@3071
   131
nipkow@10835
   132
Goal "Flat$UU =UU";
wenzelm@4098
   133
by (simp_tac (simpset() addsimps [Flat_def]) 1);
mueller@3071
   134
qed"Flat_UU";
mueller@3071
   135
nipkow@10835
   136
Goal "Flat$nil =nil";
wenzelm@4098
   137
by (simp_tac (simpset() addsimps [Flat_def]) 1);
mueller@3071
   138
qed"Flat_nil";
mueller@3071
   139
nipkow@10835
   140
Goal "Flat$(x##xs)= x @@ (Flat$xs)"; 
wenzelm@7229
   141
by (simp_tac (simpset() addsimps [Flat_def, Consq_def]) 1);
mueller@3071
   142
qed"Flat_cons";
mueller@3071
   143
mueller@3071
   144
mueller@3071
   145
(* ---------------------------------------------------------------- *)
mueller@3071
   146
(*                               Zip                                *)
mueller@3071
   147
(* ---------------------------------------------------------------- *)
mueller@3071
   148
wenzelm@5068
   149
Goal "Zip = (LAM t1 t2. case t1 of \
mueller@3071
   150
\               nil   => nil \
mueller@3071
   151
\             | x##xs => (case t2 of \ 
mueller@3071
   152
\                          nil => UU  \
mueller@3071
   153
\                        | y##ys => (case x of \
mueller@3071
   154
\                                      Undef  => UU \
mueller@3071
   155
\                                    | Def a => (case y of \
mueller@3071
   156
\                                                  Undef => UU \
nipkow@10835
   157
\                                                | Def b => Def (a,b)##(Zip$xs$ys)))))";
mueller@3071
   158
by (rtac trans 1);
paulson@3457
   159
by (rtac fix_eq2 1);
paulson@3457
   160
by (rtac Zip_def 1);
paulson@3457
   161
by (rtac beta_cfun 1);
mueller@3071
   162
by (Simp_tac 1);
mueller@3071
   163
qed"Zip_unfold";
mueller@3071
   164
nipkow@10835
   165
Goal "Zip$UU$y =UU";
mueller@3071
   166
by (stac Zip_unfold 1);
mueller@3071
   167
by (Simp_tac 1);
mueller@3071
   168
qed"Zip_UU1";
mueller@3071
   169
nipkow@10835
   170
Goal "x~=nil ==> Zip$x$UU =UU";
mueller@3071
   171
by (stac Zip_unfold 1);
mueller@3071
   172
by (Simp_tac 1);
oheimb@4042
   173
by (res_inst_tac [("x","x")] seq.casedist 1);
mueller@3071
   174
by (REPEAT (Asm_full_simp_tac 1));
mueller@3071
   175
qed"Zip_UU2";
mueller@3071
   176
nipkow@10835
   177
Goal "Zip$nil$y =nil";
mueller@3071
   178
by (stac Zip_unfold 1);
mueller@3071
   179
by (Simp_tac 1);
mueller@3071
   180
qed"Zip_nil";
mueller@3071
   181
nipkow@10835
   182
Goal "Zip$(x>>xs)$nil= UU"; 
mueller@3071
   183
by (stac Zip_unfold 1);
wenzelm@7229
   184
by (simp_tac (simpset() addsimps [Consq_def]) 1);
mueller@3071
   185
qed"Zip_cons_nil";
mueller@3071
   186
nipkow@10835
   187
Goal "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys"; 
paulson@3457
   188
by (rtac trans 1);
mueller@3071
   189
by (stac Zip_unfold 1);
mueller@3071
   190
by (Simp_tac 1);
wenzelm@7229
   191
by (simp_tac (simpset() addsimps [Consq_def]) 1);
mueller@3071
   192
qed"Zip_cons";
mueller@3071
   193
mueller@3071
   194
mueller@3071
   195
Delsimps [sfilter_UU,sfilter_nil,sfilter_cons,
mueller@3071
   196
          smap_UU,smap_nil,smap_cons,
mueller@3071
   197
          sforall2_UU,sforall2_nil,sforall2_cons,
mueller@3071
   198
          slast_UU,slast_nil,slast_cons,
mueller@3071
   199
          stakewhile_UU, stakewhile_nil, stakewhile_cons, 
mueller@3071
   200
          sdropwhile_UU, sdropwhile_nil, sdropwhile_cons,
mueller@3071
   201
          sflat_UU,sflat_nil,sflat_cons,
mueller@3071
   202
          szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons];
mueller@3071
   203
mueller@3071
   204
mueller@3071
   205
Addsimps [Filter_UU,Filter_nil,Filter_cons,
mueller@3071
   206
          Map_UU,Map_nil,Map_cons,
mueller@3071
   207
          Forall_UU,Forall_nil,Forall_cons,
mueller@3071
   208
          Last_UU,Last_nil,Last_cons,
mueller@3275
   209
          Conc_cons,
mueller@3071
   210
          Takewhile_UU, Takewhile_nil, Takewhile_cons, 
mueller@3071
   211
          Dropwhile_UU, Dropwhile_nil, Dropwhile_cons,
mueller@3071
   212
          Zip_UU1,Zip_UU2,Zip_nil,Zip_cons_nil,Zip_cons];
mueller@3071
   213
mueller@3071
   214
mueller@3071
   215
mueller@3071
   216
(* ------------------------------------------------------------------------------------- *)
mueller@3071
   217
mueller@3071
   218
mueller@3071
   219
section "Cons";
mueller@3071
   220
wenzelm@5068
   221
Goal "a>>s = (Def a)##s";
wenzelm@7229
   222
by (simp_tac (simpset() addsimps [Consq_def]) 1);
wenzelm@7229
   223
qed"Consq_def2";
mueller@3071
   224
wenzelm@5068
   225
Goal "x = UU | x = nil | (? a s. x = a >> s)";
wenzelm@7229
   226
by (simp_tac (simpset() addsimps [Consq_def2]) 1);
mueller@3071
   227
by (cut_facts_tac [seq.exhaust] 1);
mueller@3071
   228
by (fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]) 1);
mueller@3071
   229
qed"Seq_exhaust";
mueller@3071
   230
mueller@3071
   231
wenzelm@5068
   232
Goal "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s  ==> P |] ==> P";
mueller@3071
   233
by (cut_inst_tac [("x","x")] Seq_exhaust 1);
paulson@3457
   234
by (etac disjE 1);
mueller@3071
   235
by (Asm_full_simp_tac 1);
paulson@3457
   236
by (etac disjE 1);
mueller@3071
   237
by (Asm_full_simp_tac 1);
mueller@3071
   238
by (REPEAT (etac exE 1));
mueller@3071
   239
by (Asm_full_simp_tac 1);
mueller@3071
   240
qed"Seq_cases";
mueller@3071
   241
mueller@3071
   242
fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i
mueller@3071
   243
	  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
mueller@3071
   244
mueller@3071
   245
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
mueller@3071
   246
fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2)
mueller@3071
   247
                                             THEN Asm_full_simp_tac (i+1)
mueller@3071
   248
                                             THEN Asm_full_simp_tac i;
mueller@3071
   249
wenzelm@5068
   250
Goal "a>>s ~= UU";
wenzelm@7229
   251
by (stac Consq_def2 1);
mueller@3071
   252
by (resolve_tac seq.con_rews 1);
paulson@3457
   253
by (rtac Def_not_UU 1);
mueller@3071
   254
qed"Cons_not_UU";
mueller@3071
   255
mueller@3275
   256
wenzelm@5068
   257
Goal "~(a>>x) << UU";
mueller@3071
   258
by (rtac notI 1);
mueller@3071
   259
by (dtac antisym_less 1);
mueller@3071
   260
by (Simp_tac 1);
wenzelm@4098
   261
by (asm_full_simp_tac (simpset() addsimps [Cons_not_UU]) 1);
mueller@3071
   262
qed"Cons_not_less_UU";
mueller@3071
   263
wenzelm@5068
   264
Goal "~a>>s << nil";
wenzelm@7229
   265
by (stac Consq_def2 1);
mueller@3071
   266
by (resolve_tac seq.rews 1);
paulson@3457
   267
by (rtac Def_not_UU 1);
mueller@3071
   268
qed"Cons_not_less_nil";
mueller@3071
   269
wenzelm@5068
   270
Goal "a>>s ~= nil";
wenzelm@7229
   271
by (stac Consq_def2 1);
mueller@3071
   272
by (resolve_tac seq.rews 1);
mueller@3071
   273
qed"Cons_not_nil";
mueller@3071
   274
wenzelm@5068
   275
Goal "nil ~= a>>s";
wenzelm@7229
   276
by (simp_tac (simpset() addsimps [Consq_def2]) 1);
mueller@3275
   277
qed"Cons_not_nil2";
mueller@3275
   278
wenzelm@5068
   279
Goal "(a>>s = b>>t) = (a = b & s = t)";
wenzelm@7229
   280
by (simp_tac (HOL_ss addsimps [Consq_def2]) 1);
mueller@3071
   281
by (stac (hd lift.inject RS sym) 1);
mueller@3071
   282
back(); back();
mueller@3071
   283
by (rtac scons_inject_eq 1);
mueller@3071
   284
by (REPEAT(rtac Def_not_UU 1));
mueller@3071
   285
qed"Cons_inject_eq";
mueller@3071
   286
wenzelm@5068
   287
Goal "(a>>s<<b>>t) = (a = b & s<<t)";
wenzelm@7229
   288
by (simp_tac (simpset() addsimps [Consq_def2]) 1);
mueller@3071
   289
by (stac (Def_inject_less_eq RS sym) 1);
mueller@3071
   290
back();
mueller@3071
   291
by (rtac iffI 1);
mueller@3071
   292
(* 1 *)
mueller@3071
   293
by (etac (hd seq.inverts) 1);
mueller@3071
   294
by (REPEAT(rtac Def_not_UU 1));
mueller@3071
   295
(* 2 *)
mueller@3071
   296
by (Asm_full_simp_tac 1);
mueller@3071
   297
by (etac conjE 1);
mueller@3071
   298
by (etac monofun_cfun_arg 1);
mueller@3071
   299
qed"Cons_inject_less_eq";
mueller@3071
   300
nipkow@10835
   301
Goal "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)";
wenzelm@7229
   302
by (simp_tac (simpset() addsimps [Consq_def]) 1);
mueller@3071
   303
qed"seq_take_Cons";
mueller@3071
   304
mueller@3275
   305
Addsimps [Cons_not_nil2,Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
mueller@3071
   306
          Cons_not_UU,Cons_not_less_UU,Cons_not_less_nil,Cons_not_nil];
mueller@3071
   307
mueller@3275
   308
(* Instead of adding UU_neq_Cons every equation UU~=x could be changed to x~=UU *)
wenzelm@5068
   309
Goal "UU ~= x>>xs";
mueller@3275
   310
by (res_inst_tac [("s1","UU"),("t1","x>>xs")]  (sym RS rev_contrapos) 1);
mueller@3275
   311
by (REPEAT (Simp_tac 1));
mueller@3275
   312
qed"UU_neq_Cons";
mueller@3275
   313
mueller@3275
   314
Addsimps [UU_neq_Cons];
mueller@3275
   315
mueller@3071
   316
mueller@3071
   317
(* ----------------------------------------------------------------------------------- *)
mueller@3071
   318
mueller@3071
   319
section "induction";
mueller@3071
   320
wenzelm@5068
   321
Goal "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x";
paulson@3457
   322
by (etac seq.ind 1);
mueller@3071
   323
by (REPEAT (atac 1));
mueller@3071
   324
by (def_tac 1);
wenzelm@7229
   325
by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
mueller@3071
   326
qed"Seq_induct";
mueller@3071
   327
wenzelm@5068
   328
Goal "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]  \
mueller@3071
   329
\               ==> seq_finite x --> P x";
paulson@3457
   330
by (etac seq_finite_ind 1);
mueller@3071
   331
by (REPEAT (atac 1));
mueller@3071
   332
by (def_tac 1);
wenzelm@7229
   333
by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
mueller@3071
   334
qed"Seq_FinitePartial_ind";
mueller@3071
   335
wenzelm@5068
   336
Goal "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
paulson@3457
   337
by (etac sfinite.induct 1);
paulson@3457
   338
by (assume_tac 1);
mueller@3071
   339
by (def_tac 1);
wenzelm@7229
   340
by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
mueller@3071
   341
qed"Seq_Finite_ind"; 
mueller@3071
   342
mueller@3071
   343
mueller@3071
   344
(* rws are definitions to be unfolded for admissibility check *)
mueller@3071
   345
fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
mueller@3071
   346
                         THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
wenzelm@4098
   347
                         THEN simp_tac (simpset() addsimps rws) i;
mueller@3071
   348
mueller@3071
   349
fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
mueller@3071
   350
                              THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
mueller@3071
   351
mueller@3071
   352
fun pair_tac s = res_inst_tac [("p",s)] PairE
mueller@3071
   353
			  THEN' hyp_subst_tac THEN' Asm_full_simp_tac;
mueller@3071
   354
mueller@3071
   355
(* induction on a sequence of pairs with pairsplitting and simplification *)
mueller@3071
   356
fun pair_induct_tac s rws i = 
mueller@3071
   357
           res_inst_tac [("x",s)] Seq_induct i 
mueller@3071
   358
           THEN pair_tac "a" (i+3) 
mueller@3071
   359
           THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1)))) 
wenzelm@4098
   360
           THEN simp_tac (simpset() addsimps rws) i;
mueller@3071
   361
mueller@3071
   362
mueller@3071
   363
mueller@3071
   364
(* ------------------------------------------------------------------------------------ *)
mueller@3071
   365
mueller@3071
   366
section "HD,TL";
mueller@3071
   367
nipkow@10835
   368
Goal "HD$(x>>y) = Def x";
wenzelm@7229
   369
by (simp_tac (simpset() addsimps [Consq_def]) 1);
mueller@3071
   370
qed"HD_Cons";
mueller@3071
   371
nipkow@10835
   372
Goal "TL$(x>>y) = y";
wenzelm@7229
   373
by (simp_tac (simpset() addsimps [Consq_def]) 1);
mueller@3071
   374
qed"TL_Cons";
mueller@3071
   375
mueller@3071
   376
Addsimps [HD_Cons,TL_Cons];
mueller@3071
   377
mueller@3071
   378
(* ------------------------------------------------------------------------------------ *)
mueller@3071
   379
mueller@3071
   380
section "Finite, Partial, Infinite";
mueller@3071
   381
wenzelm@5068
   382
Goal "Finite (a>>xs) = Finite xs";
wenzelm@7229
   383
by (simp_tac (simpset() addsimps [Consq_def2,Finite_cons]) 1);
mueller@3071
   384
qed"Finite_Cons";
mueller@3071
   385
mueller@3071
   386
Addsimps [Finite_Cons];
paulson@6161
   387
Goal "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
mueller@3275
   388
by (Seq_Finite_induct_tac 1);
mueller@3275
   389
qed"FiniteConc_1";
mueller@3275
   390
paulson@6161
   391
Goal "Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
mueller@3275
   392
by (Seq_Finite_induct_tac 1);
mueller@3275
   393
(* nil*)
mueller@3275
   394
by (strip_tac 1);
mueller@3275
   395
by (Seq_case_simp_tac "x" 1);
mueller@3275
   396
by (Asm_full_simp_tac 1);
mueller@3275
   397
(* cons *)
mueller@3275
   398
by (strip_tac 1);
mueller@3275
   399
by (Seq_case_simp_tac "x" 1);
mueller@3275
   400
by (Seq_case_simp_tac "y" 1);
wenzelm@4098
   401
by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
mueller@3275
   402
by (eres_inst_tac [("x","sa")] allE 1);
mueller@3275
   403
by (eres_inst_tac [("x","y")] allE 1);
mueller@3275
   404
by (Asm_full_simp_tac 1);
mueller@3275
   405
qed"FiniteConc_2";
mueller@3275
   406
wenzelm@5068
   407
Goal "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)";
mueller@3275
   408
by (rtac iffI 1);
paulson@3457
   409
by (etac (FiniteConc_2 RS spec RS spec RS mp) 1);
paulson@3457
   410
by (rtac refl 1);
paulson@3457
   411
by (rtac (FiniteConc_1 RS mp) 1);
paulson@4477
   412
by Auto_tac;
mueller@3275
   413
qed"FiniteConc";
mueller@3275
   414
mueller@3275
   415
Addsimps [FiniteConc];
mueller@3275
   416
mueller@3275
   417
nipkow@10835
   418
Goal "Finite s ==> Finite (Map f$s)";
mueller@3275
   419
by (Seq_Finite_induct_tac 1);
mueller@3275
   420
qed"FiniteMap1";
mueller@3275
   421
nipkow@10835
   422
Goal "Finite s ==> ! t. (s = Map f$t) --> Finite t";
mueller@3275
   423
by (Seq_Finite_induct_tac 1);
mueller@3275
   424
by (strip_tac 1);
mueller@3275
   425
by (Seq_case_simp_tac "t" 1);
mueller@3275
   426
by (Asm_full_simp_tac 1);
mueller@3275
   427
(* main case *)
paulson@4477
   428
by Auto_tac;
mueller@3275
   429
by (Seq_case_simp_tac "t" 1);
mueller@3275
   430
by (Asm_full_simp_tac 1);
mueller@3275
   431
qed"FiniteMap2";
mueller@3275
   432
nipkow@10835
   433
Goal "Finite (Map f$s) = Finite s";
paulson@4477
   434
by Auto_tac;
paulson@3457
   435
by (etac (FiniteMap2 RS spec RS mp) 1);
paulson@3457
   436
by (rtac refl 1);
paulson@3457
   437
by (etac FiniteMap1 1);
mueller@3275
   438
qed"Map2Finite";
mueller@3275
   439
mueller@3433
   440
nipkow@10835
   441
Goal "Finite s ==> Finite (Filter P$s)";
mueller@3433
   442
by (Seq_Finite_induct_tac 1);
mueller@3433
   443
qed"FiniteFilter";
mueller@3433
   444
mueller@3433
   445
mueller@3361
   446
(* ----------------------------------------------------------------------------------- *)
mueller@3361
   447
mueller@3361
   448
mueller@3361
   449
section "admissibility";
mueller@3361
   450
mueller@3361
   451
(* Finite x is proven to be adm: Finite_flat shows that there are only chains of length one.
nipkow@3461
   452
   Then the assumption that an _infinite_ chain exists (from admI2) is set to a contradiction 
mueller@3361
   453
   to Finite_flat *)
mueller@3361
   454
wenzelm@5068
   455
Goal "!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y";
mueller@3361
   456
by (Seq_Finite_induct_tac 1);
mueller@3361
   457
by (strip_tac 1);
paulson@3457
   458
by (etac conjE 1);
paulson@3457
   459
by (etac nil_less_is_nil 1);
mueller@3361
   460
(* main case *)
paulson@4477
   461
by Auto_tac;
mueller@3361
   462
by (Seq_case_simp_tac "y" 1);
paulson@4477
   463
by Auto_tac;
mueller@3361
   464
qed_spec_mp"Finite_flat";
mueller@3361
   465
mueller@3361
   466
wenzelm@5068
   467
Goal "adm(%(x:: 'a Seq).Finite x)";
nipkow@3461
   468
by (rtac admI2 1);
mueller@3361
   469
by (eres_inst_tac [("x","0")] allE 1);
mueller@3361
   470
back();
paulson@3457
   471
by (etac exE 1);
mueller@3361
   472
by (REPEAT (etac conjE 1));
mueller@3361
   473
by (res_inst_tac [("x","0")] allE 1);
paulson@3457
   474
by (assume_tac 1);
mueller@3361
   475
by (eres_inst_tac [("x","j")] allE 1);
mueller@3361
   476
by (cut_inst_tac [("x","Y 0"),("y","Y j")] Finite_flat 1);
mueller@3361
   477
(* Generates a contradiction in subgoal 3 *)
paulson@4477
   478
by Auto_tac;
mueller@3361
   479
qed"adm_Finite";
mueller@3361
   480
mueller@3361
   481
Addsimps [adm_Finite];
mueller@3361
   482
mueller@3071
   483
mueller@3071
   484
(* ------------------------------------------------------------------------------------ *)
mueller@3071
   485
mueller@3071
   486
section "Conc";
mueller@3071
   487
wenzelm@5068
   488
Goal "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)";
mueller@3071
   489
by (Seq_Finite_induct_tac 1);
mueller@3071
   490
qed"Conc_cong";
mueller@3071
   491
wenzelm@5068
   492
Goal "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z";
mueller@3275
   493
by (Seq_induct_tac "x" [] 1);
mueller@3275
   494
qed"Conc_assoc";
mueller@3275
   495
wenzelm@5068
   496
Goal "s@@ nil = s";
mueller@3275
   497
by (res_inst_tac[("x","s")] seq.ind 1);
mueller@3275
   498
by (Simp_tac 1);
mueller@3275
   499
by (Simp_tac 1);
mueller@3275
   500
by (Simp_tac 1);
mueller@3275
   501
by (Asm_full_simp_tac 1);
mueller@3275
   502
qed"nilConc";
mueller@3275
   503
mueller@3275
   504
Addsimps [nilConc];
mueller@3275
   505
mueller@5976
   506
(* should be same as nil_is_Conc2 when all nils are turned to right side !! *)
wenzelm@5068
   507
Goal "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
mueller@3361
   508
by (Seq_case_simp_tac "x" 1);
paulson@4477
   509
by Auto_tac;
mueller@3361
   510
qed"nil_is_Conc";
mueller@3361
   511
wenzelm@5068
   512
Goal "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)";
mueller@3361
   513
by (Seq_case_simp_tac "x" 1);
paulson@4477
   514
by Auto_tac;
mueller@3361
   515
qed"nil_is_Conc2";
mueller@3361
   516
mueller@3275
   517
mueller@3071
   518
(* ------------------------------------------------------------------------------------ *)
mueller@3071
   519
mueller@3071
   520
section "Last";
mueller@3071
   521
nipkow@10835
   522
Goal "Finite s ==> s~=nil --> Last$s~=UU";
mueller@3071
   523
by (Seq_Finite_induct_tac  1);
mueller@3071
   524
qed"Finite_Last1";
mueller@3071
   525
nipkow@10835
   526
Goal "Finite s ==> Last$s=UU --> s=nil";
mueller@3071
   527
by (Seq_Finite_induct_tac  1);
mueller@3071
   528
by (fast_tac HOL_cs 1);
mueller@3071
   529
qed"Finite_Last2";
mueller@3071
   530
mueller@3071
   531
mueller@3071
   532
(* ------------------------------------------------------------------------------------ *)
mueller@3071
   533
mueller@3071
   534
mueller@3071
   535
section "Filter, Conc";
mueller@3071
   536
mueller@3071
   537
nipkow@10835
   538
Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s";
mueller@3071
   539
by (Seq_induct_tac "s" [Filter_def] 1);
mueller@3071
   540
qed"FilterPQ";
mueller@3071
   541
nipkow@10835
   542
Goal "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)";
wenzelm@4098
   543
by (simp_tac (simpset() addsimps [Filter_def,sfiltersconc]) 1);
mueller@3071
   544
qed"FilterConc";
mueller@3071
   545
mueller@3071
   546
(* ------------------------------------------------------------------------------------ *)
mueller@3071
   547
mueller@3071
   548
section "Map";
mueller@3071
   549
nipkow@10835
   550
Goal "Map f$(Map g$s) = Map (f o g)$s";
mueller@3071
   551
by (Seq_induct_tac "s" [] 1);
mueller@3071
   552
qed"MapMap";
mueller@3071
   553
nipkow@10835
   554
Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)";
mueller@3071
   555
by (Seq_induct_tac "x" [] 1);
mueller@3071
   556
qed"MapConc";
mueller@3071
   557
nipkow@10835
   558
Goal "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)";
mueller@3071
   559
by (Seq_induct_tac "x" [] 1);
mueller@3071
   560
qed"MapFilter";
mueller@3071
   561
nipkow@10835
   562
Goal "nil = (Map f$s) --> s= nil";
mueller@3275
   563
by (Seq_case_simp_tac "s" 1);
mueller@3275
   564
qed"nilMap";
mueller@3275
   565
mueller@3361
   566
nipkow@10835
   567
Goal "Forall P (Map f$s) = Forall (P o f) s";
mueller@3275
   568
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
mueller@3361
   569
qed"ForallMap";
mueller@3275
   570
mueller@3275
   571
mueller@3275
   572
mueller@3071
   573
mueller@3071
   574
(* ------------------------------------------------------------------------------------ *)
mueller@3071
   575
mueller@3275
   576
section "Forall";
mueller@3071
   577
mueller@3071
   578
wenzelm@5068
   579
Goal "Forall P ys & (! x. P x --> Q x) \
mueller@3071
   580
\         --> Forall Q ys";
mueller@3071
   581
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
mueller@3071
   582
qed"ForallPForallQ1";
mueller@3071
   583
mueller@3071
   584
bind_thm ("ForallPForallQ",impI RSN (2,allI RSN (2,conjI RS (ForallPForallQ1 RS mp))));
mueller@3071
   585
wenzelm@5068
   586
Goal "(Forall P x & Forall P y) --> Forall P (x @@ y)";
mueller@3071
   587
by (Seq_induct_tac "x" [Forall_def,sforall_def] 1);
mueller@3071
   588
qed"Forall_Conc_impl";
mueller@3071
   589
paulson@6161
   590
Goal "Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
mueller@3071
   591
by (Seq_Finite_induct_tac  1);
mueller@3071
   592
qed"Forall_Conc";
mueller@3071
   593
mueller@3275
   594
Addsimps [Forall_Conc];
mueller@3275
   595
nipkow@10835
   596
Goal "Forall P s  --> Forall P (TL$s)";
mueller@3275
   597
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
mueller@3275
   598
qed"ForallTL1";
mueller@3275
   599
mueller@3275
   600
bind_thm ("ForallTL",ForallTL1 RS mp);
mueller@3275
   601
nipkow@10835
   602
Goal "Forall P s  --> Forall P (Dropwhile Q$s)";
mueller@3275
   603
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
mueller@3275
   604
qed"ForallDropwhile1";
mueller@3275
   605
mueller@3275
   606
bind_thm ("ForallDropwhile",ForallDropwhile1 RS mp);
mueller@3275
   607
mueller@3275
   608
mueller@3275
   609
(* only admissible in t, not if done in s *)
mueller@3275
   610
wenzelm@5068
   611
Goal "! s. Forall P s --> t<<s --> Forall P t";
mueller@3275
   612
by (Seq_induct_tac "t" [Forall_def,sforall_def] 1);
mueller@3275
   613
by (strip_tac 1); 
mueller@3275
   614
by (Seq_case_simp_tac "sa" 1);
mueller@3275
   615
by (Asm_full_simp_tac 1);
paulson@4477
   616
by Auto_tac;
mueller@3275
   617
qed"Forall_prefix";
nipkow@4681
   618
mueller@3275
   619
bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
mueller@3275
   620
mueller@3275
   621
paulson@6161
   622
Goal "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
paulson@4477
   623
by Auto_tac;
mueller@3275
   624
qed"Forall_postfixclosed";
mueller@3275
   625
mueller@3275
   626
nipkow@10835
   627
Goal "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr";
mueller@3275
   628
by (Seq_induct_tac "tr" [Forall_def,sforall_def] 1);
mueller@3275
   629
qed"ForallPFilterQR1";
mueller@3275
   630
mueller@3275
   631
bind_thm("ForallPFilterQR",allI RS (conjI RS (ForallPFilterQR1 RS mp)));
mueller@3275
   632
mueller@3071
   633
mueller@3071
   634
(* ------------------------------------------------------------------------------------- *)
mueller@3071
   635
mueller@3071
   636
section "Forall, Filter";
mueller@3071
   637
mueller@3071
   638
nipkow@10835
   639
Goal "Forall P (Filter P$x)";
wenzelm@4098
   640
by (simp_tac (simpset() addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
mueller@3071
   641
qed"ForallPFilterP";
mueller@3071
   642
mueller@3275
   643
(* holds also in other direction, then equal to forallPfilterP *)
nipkow@10835
   644
Goal "Forall P x --> Filter P$x = x";
mueller@3071
   645
by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);
mueller@3071
   646
qed"ForallPFilterPid1";
mueller@3071
   647
nipkow@4034
   648
bind_thm("ForallPFilterPid",ForallPFilterPid1 RS mp);
mueller@3071
   649
mueller@3071
   650
mueller@3275
   651
(* holds also in other direction *)
wenzelm@5068
   652
Goal "!! ys . Finite ys ==> \
nipkow@10835
   653
\   Forall (%x. ~P x) ys --> Filter P$ys = nil ";
mueller@3275
   654
by (Seq_Finite_induct_tac 1);
mueller@3071
   655
qed"ForallnPFilterPnil1";
mueller@3071
   656
mueller@3275
   657
bind_thm ("ForallnPFilterPnil",ForallnPFilterPnil1 RS mp);
mueller@3071
   658
mueller@3071
   659
mueller@3275
   660
(* holds also in other direction *)
paulson@6161
   661
Goal   "~Finite ys & Forall (%x. ~P x) ys \
nipkow@10835
   662
\                  --> Filter P$ys = UU ";
mueller@3361
   663
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
mueller@3071
   664
qed"ForallnPFilterPUU1";
mueller@3071
   665
mueller@3275
   666
bind_thm ("ForallnPFilterPUU",conjI RS (ForallnPFilterPUU1 RS mp));
mueller@3275
   667
mueller@3275
   668
mueller@3275
   669
(* inverse of ForallnPFilterPnil *)
mueller@3275
   670
nipkow@10835
   671
Goal "!! ys . Filter P$ys = nil --> \
mueller@3275
   672
\   (Forall (%x. ~P x) ys & Finite ys)";
mueller@3275
   673
by (res_inst_tac[("x","ys")] Seq_induct 1);
mueller@3275
   674
(* adm *)
mueller@3361
   675
(* FIX: not admissible, search other proof!! *)
paulson@3457
   676
by (rtac adm_all 1);
mueller@3275
   677
(* base cases *)
mueller@3275
   678
by (Simp_tac 1);
mueller@3275
   679
by (Simp_tac 1);
mueller@3275
   680
(* main case *)
nipkow@4833
   681
by (Asm_full_simp_tac 1);
mueller@3275
   682
qed"FilternPnilForallP1";
mueller@3275
   683
mueller@3275
   684
bind_thm ("FilternPnilForallP",FilternPnilForallP1 RS mp);
mueller@3275
   685
mueller@3361
   686
(* inverse of ForallnPFilterPUU. proved by 2 lemmas because of adm problems *)
mueller@3361
   687
nipkow@10835
   688
Goal "Finite ys ==> Filter P$ys ~= UU";
mueller@3361
   689
by (Seq_Finite_induct_tac 1);
mueller@3361
   690
qed"FilterUU_nFinite_lemma1";
mueller@3275
   691
nipkow@10835
   692
Goal "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU";
mueller@3361
   693
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
mueller@3361
   694
qed"FilterUU_nFinite_lemma2";
mueller@3361
   695
nipkow@10835
   696
Goal   "Filter P$ys = UU ==> \
mueller@3275
   697
\                (Forall (%x. ~P x) ys  & ~Finite ys)";
mueller@3361
   698
by (rtac conjI 1);
mueller@3361
   699
by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
paulson@4477
   700
by Auto_tac;
wenzelm@4098
   701
by (blast_tac (claset() addSDs [FilterUU_nFinite_lemma1]) 1);
mueller@3361
   702
qed"FilternPUUForallP";
mueller@3071
   703
mueller@3071
   704
wenzelm@5068
   705
Goal  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
nipkow@10835
   706
\   ==> Filter P$ys = nil";
paulson@3457
   707
by (etac ForallnPFilterPnil 1);
paulson@3457
   708
by (etac ForallPForallQ 1);
paulson@4477
   709
by Auto_tac;
mueller@3071
   710
qed"ForallQFilterPnil";
mueller@3071
   711
wenzelm@5068
   712
Goal "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|] \
nipkow@10835
   713
\   ==> Filter P$ys = UU ";
paulson@3457
   714
by (etac ForallnPFilterPUU 1);
paulson@3457
   715
by (etac ForallPForallQ 1);
paulson@4477
   716
by Auto_tac;
mueller@3071
   717
qed"ForallQFilterPUU";
mueller@3071
   718
mueller@3071
   719
mueller@3071
   720
mueller@3071
   721
(* ------------------------------------------------------------------------------------- *)
mueller@3071
   722
mueller@3071
   723
section "Takewhile, Forall, Filter";
mueller@3071
   724
mueller@3071
   725
nipkow@10835
   726
Goal "Forall P (Takewhile P$x)";
wenzelm@4098
   727
by (simp_tac (simpset() addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
mueller@3071
   728
qed"ForallPTakewhileP";
mueller@3071
   729
mueller@3071
   730
nipkow@10835
   731
Goal"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)";
paulson@3457
   732
by (rtac ForallPForallQ 1);
paulson@3457
   733
by (rtac ForallPTakewhileP 1);
paulson@4477
   734
by Auto_tac;
mueller@3071
   735
qed"ForallPTakewhileQ";
mueller@3071
   736
mueller@3071
   737
nipkow@10835
   738
Goal  "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |] \
nipkow@10835
   739
\   ==> Filter P$(Takewhile Q$ys) = nil";
paulson@3457
   740
by (etac ForallnPFilterPnil 1);
paulson@3457
   741
by (rtac ForallPForallQ 1);
paulson@3457
   742
by (rtac ForallPTakewhileP 1);
paulson@4477
   743
by Auto_tac;
mueller@3071
   744
qed"FilterPTakewhileQnil";
mueller@3071
   745
wenzelm@5068
   746
Goal "!! Q P. [| !!x. Q x ==> P x |] ==> \
nipkow@10835
   747
\            Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)";
paulson@3457
   748
by (rtac ForallPFilterPid 1);
paulson@3457
   749
by (rtac ForallPForallQ 1);
paulson@3457
   750
by (rtac ForallPTakewhileP 1);
paulson@4477
   751
by Auto_tac;
mueller@3071
   752
qed"FilterPTakewhileQid";
mueller@3071
   753
mueller@3071
   754
Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
mueller@3071
   755
          FilterPTakewhileQnil,FilterPTakewhileQid];
mueller@3071
   756
nipkow@10835
   757
Goal "Takewhile P$(Takewhile P$s) = Takewhile P$s";
mueller@3275
   758
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
mueller@3275
   759
qed"Takewhile_idempotent";
mueller@3071
   760
nipkow@10835
   761
Goal "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s";
mueller@3275
   762
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
mueller@3275
   763
qed"ForallPTakewhileQnP";
mueller@3275
   764
nipkow@10835
   765
Goal "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s";
mueller@3275
   766
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
mueller@3275
   767
qed"ForallPDropwhileQnP";
mueller@3275
   768
mueller@3275
   769
Addsimps [ForallPTakewhileQnP RS mp, ForallPDropwhileQnP RS mp];
mueller@3275
   770
mueller@3275
   771
nipkow@10835
   772
Goal "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)";
mueller@3275
   773
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
mueller@3275
   774
qed"TakewhileConc1";
mueller@3275
   775
mueller@3275
   776
bind_thm("TakewhileConc",TakewhileConc1 RS mp);
mueller@3275
   777
nipkow@10835
   778
Goal "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t";
mueller@3275
   779
by (Seq_Finite_induct_tac 1);
mueller@3275
   780
qed"DropwhileConc1";
mueller@3275
   781
mueller@3275
   782
bind_thm("DropwhileConc",DropwhileConc1 RS mp);
mueller@3071
   783
mueller@3071
   784
mueller@3071
   785
mueller@3071
   786
(* ----------------------------------------------------------------------------------- *)
mueller@3071
   787
mueller@3071
   788
section "coinductive characterizations of Filter";
mueller@3071
   789
mueller@3071
   790
nipkow@10835
   791
Goal "HD$(Filter P$y) = Def x \
nipkow@10835
   792
\         --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y)))  \
nipkow@10835
   793
\             & Finite (Takewhile (%x. ~ P x)$y)  & P x";
mueller@3071
   794
mueller@3071
   795
(* FIX: pay attention: is only admissible with chain-finite package to be added to 
mueller@3656
   796
        adm test and Finite f x admissibility *)
mueller@3071
   797
by (Seq_induct_tac "y" [] 1);
paulson@3457
   798
by (rtac adm_all 1);
mueller@3071
   799
by (Asm_full_simp_tac 1); 
mueller@3071
   800
by (case_tac "P a" 1);
nipkow@4681
   801
 by (Asm_full_simp_tac 1); 
nipkow@4681
   802
 by (Blast_tac 1);
mueller@3071
   803
(* ~ P a *)
mueller@3071
   804
by (Asm_full_simp_tac 1); 
mueller@3071
   805
qed"divide_Seq_lemma";
mueller@3071
   806
nipkow@10835
   807
Goal "(x>>xs) << Filter P$y  \
nipkow@10835
   808
\   ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) \
nipkow@10835
   809
\      & Finite (Takewhile (%a. ~ P a)$y)  & P x";
paulson@3457
   810
by (rtac (divide_Seq_lemma RS mp) 1);
mueller@3071
   811
by (dres_inst_tac [("fo","HD"),("xa","x>>xs")]  monofun_cfun_arg 1);
mueller@3071
   812
by (Asm_full_simp_tac 1); 
mueller@3071
   813
qed"divide_Seq";
mueller@3071
   814
mueller@3656
   815
 
nipkow@10835
   816
Goal "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)";
mueller@3656
   817
(* Pay attention: is only admissible with chain-finite package to be added to 
mueller@3071
   818
        adm test *)
mueller@3656
   819
by (Seq_induct_tac "y" [Forall_def,sforall_def] 1);
mueller@3071
   820
qed"nForall_HDFilter";
mueller@3071
   821
mueller@3071
   822
paulson@6161
   823
Goal "~Forall P y  \
nipkow@10835
   824
\  ==> ? x. y= (Takewhile P$y @@ (x >> TL$(Dropwhile P$y))) & \
nipkow@10835
   825
\      Finite (Takewhile P$y) & (~ P x)";
paulson@3457
   826
by (dtac (nForall_HDFilter RS mp) 1);
mueller@3071
   827
by (safe_tac set_cs);
mueller@3071
   828
by (res_inst_tac [("x","x")] exI 1);
mueller@3071
   829
by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1);
paulson@4477
   830
by Auto_tac;
mueller@3071
   831
qed"divide_Seq2";
mueller@3071
   832
mueller@3071
   833
paulson@6161
   834
Goal  "~Forall P y \
mueller@3071
   835
\  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
mueller@3071
   836
by (cut_inst_tac [] divide_Seq2 1);
paulson@4477
   837
(*Auto_tac no longer proves it*)
paulson@4477
   838
by (REPEAT (fast_tac (claset() addss (simpset())) 1));
mueller@3071
   839
qed"divide_Seq3";
mueller@3071
   840
mueller@3275
   841
Addsimps [FilterPQ,FilterConc,Conc_cong];
mueller@3071
   842
mueller@3071
   843
mueller@3071
   844
(* ------------------------------------------------------------------------------------- *)
mueller@3071
   845
mueller@3071
   846
mueller@3071
   847
section "take_lemma";
mueller@3071
   848
nipkow@10835
   849
Goal "(!n. seq_take n$x = seq_take n$x') = (x = x')";
mueller@3071
   850
by (rtac iffI 1);
oheimb@4042
   851
by (resolve_tac seq.take_lemmas 1);
paulson@4477
   852
by Auto_tac;
mueller@3071
   853
qed"seq_take_lemma";
mueller@3071
   854
wenzelm@5068
   855
Goal 
nipkow@10835
   856
"  ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2) \
nipkow@10835
   857
\   --> seq_take n$(x @@ (t>>y1)) =  seq_take n$(x @@ (t>>y2)))";
mueller@3275
   858
by (Seq_induct_tac "x" [] 1);
mueller@3275
   859
by (strip_tac 1);
wenzelm@8439
   860
by (case_tac "n" 1);
paulson@4477
   861
by Auto_tac;
wenzelm@8439
   862
by (case_tac "n" 1);
paulson@4477
   863
by Auto_tac;
mueller@3275
   864
qed"take_reduction1";
mueller@3071
   865
mueller@3071
   866
nipkow@10835
   867
Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|] \
nipkow@10835
   868
\ ==> seq_take n$(x @@ (s>>y1)) =  seq_take n$(y @@ (t>>y2))";
mueller@3071
   869
wenzelm@4098
   870
by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset()));
mueller@3071
   871
qed"take_reduction";
mueller@3275
   872
mueller@3361
   873
(* ------------------------------------------------------------------
mueller@3361
   874
          take-lemma and take_reduction for << instead of = 
mueller@3361
   875
   ------------------------------------------------------------------ *)
mueller@3361
   876
wenzelm@5068
   877
Goal 
nipkow@10835
   878
"  ! n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2) \
nipkow@10835
   879
\   --> seq_take n$(x @@ (t>>y1)) <<  seq_take n$(x @@ (t>>y2)))";
mueller@3361
   880
by (Seq_induct_tac "x" [] 1);
mueller@3361
   881
by (strip_tac 1);
wenzelm@8439
   882
by (case_tac "n" 1);
paulson@4477
   883
by Auto_tac;
wenzelm@8439
   884
by (case_tac "n" 1);
paulson@4477
   885
by Auto_tac;
mueller@3361
   886
qed"take_reduction_less1";
mueller@3361
   887
mueller@3361
   888
nipkow@10835
   889
Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|] \
nipkow@10835
   890
\ ==> seq_take n$(x @@ (s>>y1)) <<  seq_take n$(y @@ (t>>y2))";
wenzelm@4098
   891
by (auto_tac (claset() addSIs [take_reduction_less1 RS spec RS mp],simpset()));
mueller@3361
   892
qed"take_reduction_less";
mueller@3361
   893
mueller@3361
   894
mueller@3361
   895
val prems = goalw thy [seq.take_def]
nipkow@10835
   896
"(!! n. seq_take n$s1 << seq_take n$s2)  ==> s1<<s2";
mueller@3361
   897
mueller@3361
   898
by (res_inst_tac [("t","s1")] (seq.reach RS subst)  1);
mueller@3361
   899
by (res_inst_tac [("t","s2")] (seq.reach RS subst)  1);
mueller@3361
   900
by (rtac (fix_def2 RS ssubst ) 1);
paulson@3457
   901
by (stac contlub_cfun_fun 1);
oheimb@4721
   902
by (rtac chain_iterate 1);
paulson@3457
   903
by (stac contlub_cfun_fun 1);
oheimb@4721
   904
by (rtac chain_iterate 1);
mueller@3361
   905
by (rtac lub_mono 1);
slotosch@5291
   906
by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1);
slotosch@5291
   907
by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1);
mueller@3361
   908
by (rtac allI 1);
mueller@3361
   909
by (resolve_tac prems 1);
mueller@3361
   910
qed"take_lemma_less1";
mueller@3361
   911
mueller@3361
   912
nipkow@10835
   913
Goal "(!n. seq_take n$x << seq_take n$x') = (x << x')";
mueller@3361
   914
by (rtac iffI 1);
paulson@3457
   915
by (rtac take_lemma_less1 1);
paulson@4477
   916
by Auto_tac;
paulson@3457
   917
by (etac monofun_cfun_arg 1);
mueller@3361
   918
qed"take_lemma_less";
mueller@3361
   919
mueller@3361
   920
(* ------------------------------------------------------------------
mueller@3361
   921
          take-lemma proof principles
mueller@3361
   922
   ------------------------------------------------------------------ *)
mueller@3071
   923
wenzelm@5068
   924
Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
mueller@3071
   925
\           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
mueller@3071
   926
\                         ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |] \
mueller@3071
   927
\              ==> A x --> (f x)=(g x)";
mueller@3071
   928
by (case_tac "Forall Q x" 1);
wenzelm@4098
   929
by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
mueller@3071
   930
qed"take_lemma_principle1";
mueller@3071
   931
wenzelm@5068
   932
Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
mueller@3071
   933
\           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
nipkow@10835
   934
\                         ==> ! n. seq_take n$(f (s1 @@ y>>s2)) \
nipkow@10835
   935
\                                = seq_take n$(g (s1 @@ y>>s2)) |] \
mueller@3071
   936
\              ==> A x --> (f x)=(g x)";
mueller@3071
   937
by (case_tac "Forall Q x" 1);
wenzelm@4098
   938
by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
oheimb@4042
   939
by (resolve_tac seq.take_lemmas 1);
paulson@4477
   940
by Auto_tac;
mueller@3071
   941
qed"take_lemma_principle2";
mueller@3071
   942
mueller@3071
   943
mueller@3071
   944
(* Note: in the following proofs the ordering of proof steps is very 
mueller@3071
   945
         important, as otherwise either (Forall Q s1) would be in the IH as
mueller@3071
   946
         assumption (then rule useless) or it is not possible to strengthen 
mueller@3071
   947
         the IH by doing a forall closure of the sequence t (then rule also useless).
nipkow@9877
   948
         This is also the reason why the induction rule (nat_less_induct or nat_induct) has to 
mueller@3071
   949
         to be imbuilt into the rule, as induction has to be done early and the take lemma 
mueller@3071
   950
         has to be used in the trivial direction afterwards for the (Forall Q x) case.  *)
mueller@3071
   951
wenzelm@5068
   952
Goal 
mueller@3071
   953
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
nipkow@10835
   954
\        !! s1 s2 y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\
mueller@3071
   955
\                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
nipkow@10835
   956
\                         ==>   seq_take (Suc n)$(f (s1 @@ y>>s2)) \
nipkow@10835
   957
\                             = seq_take (Suc n)$(g (s1 @@ y>>s2)) |] \
mueller@3071
   958
\              ==> A x --> (f x)=(g x)";
paulson@3457
   959
by (rtac impI 1);
oheimb@4042
   960
by (resolve_tac seq.take_lemmas 1);
paulson@3457
   961
by (rtac mp 1);
paulson@3457
   962
by (assume_tac 2);
mueller@3071
   963
by (res_inst_tac [("x","x")] spec 1);
paulson@3457
   964
by (rtac nat_induct 1);
mueller@3071
   965
by (Simp_tac 1);
paulson@3457
   966
by (rtac allI 1);
mueller@3071
   967
by (case_tac "Forall Q xa" 1);
wenzelm@4098
   968
by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
wenzelm@4098
   969
                           simpset())) 1);
wenzelm@4098
   970
by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
mueller@3071
   971
qed"take_lemma_induct";
mueller@3071
   972
mueller@3071
   973
wenzelm@5068
   974
Goal 
mueller@3071
   975
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
nipkow@10835
   976
\        !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m$(f t) = seq_take m$(g t);\
mueller@3071
   977
\                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
nipkow@10835
   978
\                         ==>   seq_take n$(f (s1 @@ y>>s2)) \
nipkow@10835
   979
\                             = seq_take n$(g (s1 @@ y>>s2)) |] \
mueller@3071
   980
\              ==> A x --> (f x)=(g x)";
paulson@3457
   981
by (rtac impI 1);
oheimb@4042
   982
by (resolve_tac seq.take_lemmas 1);
paulson@3457
   983
by (rtac mp 1);
paulson@3457
   984
by (assume_tac 2);
mueller@3071
   985
by (res_inst_tac [("x","x")] spec 1);
nipkow@9877
   986
by (rtac nat_less_induct 1);
paulson@3457
   987
by (rtac allI 1);
mueller@3071
   988
by (case_tac "Forall Q xa" 1);
wenzelm@4098
   989
by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
wenzelm@4098
   990
                           simpset())) 1);
wenzelm@4098
   991
by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
mueller@3071
   992
qed"take_lemma_less_induct";
mueller@3071
   993
mueller@3275
   994
mueller@3275
   995
(*
mueller@3521
   996
local
mueller@3521
   997
mueller@3521
   998
fun qnt_tac i (tac, var) = tac THEN res_inst_tac [("x", var)] spec i;
mueller@3521
   999
mueller@3521
  1000
fun add_frees tsig =
mueller@3521
  1001
  let
mueller@3521
  1002
    fun add (Free (x, T), vars) =
mueller@3521
  1003
          if Type.of_sort tsig (T, HOLogic.termS) then x ins vars
mueller@3521
  1004
          else vars
mueller@3521
  1005
      | add (Abs (_, _, t), vars) = add (t, vars)
mueller@3521
  1006
      | add (t $ u, vars) = add (t, add (u, vars))
mueller@3521
  1007
      | add (_, vars) = vars;
mueller@3521
  1008
   in add end;
mueller@3521
  1009
mueller@3521
  1010
mueller@3521
  1011
in
mueller@3521
  1012
mueller@3521
  1013
(*Generalizes over all free variables, with the named var outermost.*)
mueller@3521
  1014
fun all_frees_tac x i thm =
mueller@3521
  1015
  let
mueller@3521
  1016
    val tsig = #tsig (Sign.rep_sg (#sign (rep_thm thm)));
mueller@3521
  1017
    val frees = add_frees tsig (nth_elem (i - 1, prems_of thm), [x]);
mueller@3521
  1018
    val frees' = sort (op >) (frees \ x) @ [x];
mueller@3521
  1019
  in
mueller@3521
  1020
    foldl (qnt_tac i) (all_tac, frees') thm
mueller@3521
  1021
  end;
mueller@3521
  1022
mueller@3521
  1023
end;
mueller@3521
  1024
mueller@3275
  1025
wenzelm@5068
  1026
Goal 
mueller@3275
  1027
"!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \
nipkow@10835
  1028
\  !! s1 s2 y n. [| ! t h1 h2 m. m < n --> (A t h1 h2) --> seq_take m$(f t h1 h2) = seq_take m$(g t h1 h2);\
mueller@3275
  1029
\                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) h1 h2|] \
nipkow@10835
  1030
\                         ==>   seq_take n$(f (s1 @@ y>>s2) h1 h2) \
nipkow@10835
  1031
\                             = seq_take n$(g (s1 @@ y>>s2) h1 h2) |] \
mueller@3275
  1032
\              ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)";
mueller@3275
  1033
by (strip_tac 1);
oheimb@4042
  1034
by (resolve_tac seq.take_lemmas 1);
paulson@3457
  1035
by (rtac mp 1);
paulson@3457
  1036
by (assume_tac 2);
mueller@3275
  1037
by (res_inst_tac [("x","h2a")] spec 1);
mueller@3275
  1038
by (res_inst_tac [("x","h1a")] spec 1);
mueller@3275
  1039
by (res_inst_tac [("x","x")] spec 1);
nipkow@9877
  1040
by (rtac nat_less_induct 1);
paulson@3457
  1041
by (rtac allI 1);
mueller@3275
  1042
by (case_tac "Forall Q xa" 1);
wenzelm@4098
  1043
by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
wenzelm@4098
  1044
                           simpset())) 1);
wenzelm@4098
  1045
by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
mueller@3275
  1046
qed"take_lemma_less_induct";
mueller@3275
  1047
mueller@3275
  1048
mueller@3275
  1049
wenzelm@5068
  1050
Goal 
mueller@3275
  1051
"!! Q. [|!! s. Forall Q s ==> P ((f s) = (g s)) ; \
nipkow@10835
  1052
\        !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m$(f t) = seq_take m$(g t));\
mueller@3275
  1053
\                         Forall Q s1; Finite s1; ~ Q y|] \
nipkow@10835
  1054
\                         ==>   P (seq_take n$(f (s1 @@ y>>s2)) \
nipkow@10835
  1055
\                                   = seq_take n$(g (s1 @@ y>>s2))) |] \
mueller@3275
  1056
\              ==> P ((f x)=(g x))";
mueller@3275
  1057
mueller@3275
  1058
by (res_inst_tac [("t","f x = g x"),
nipkow@10835
  1059
                  ("s","!n. seq_take n$(f x) = seq_take n$(g x)")] subst 1);
paulson@3457
  1060
by (rtac seq_take_lemma 1);
mueller@3275
  1061
mueller@3275
  1062
wie ziehe ich n durch P, d.h. evtl. ns in P muessen umbenannt werden.....
mueller@3275
  1063
mueller@3275
  1064
mueller@3275
  1065
FIX
mueller@3275
  1066
nipkow@9877
  1067
by (rtac nat_less_induct 1);
paulson@3457
  1068
by (rtac allI 1);
mueller@3275
  1069
by (case_tac "Forall Q xa" 1);
wenzelm@4098
  1070
by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
wenzelm@4098
  1071
                           simpset())) 1);
wenzelm@4098
  1072
by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
mueller@3275
  1073
qed"take_lemma_less_induct";
mueller@3275
  1074
mueller@3275
  1075
mueller@3275
  1076
*)
mueller@3275
  1077
mueller@3275
  1078
wenzelm@5068
  1079
Goal 
mueller@3071
  1080
"!! Q. [| A UU  ==> (f UU) = (g UU) ; \
mueller@3071
  1081
\         A nil ==> (f nil) = (g nil) ; \
nipkow@10835
  1082
\         !! s y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\
mueller@3071
  1083
\                    A (y>>s) |]   \
nipkow@10835
  1084
\                    ==>   seq_take (Suc n)$(f (y>>s)) \
nipkow@10835
  1085
\                        = seq_take (Suc n)$(g (y>>s)) |] \
mueller@3071
  1086
\              ==> A x --> (f x)=(g x)";
paulson@3457
  1087
by (rtac impI 1);
oheimb@4042
  1088
by (resolve_tac seq.take_lemmas 1);
paulson@3457
  1089
by (rtac mp 1);
paulson@3457
  1090
by (assume_tac 2);
mueller@3071
  1091
by (res_inst_tac [("x","x")] spec 1);
paulson@3457
  1092
by (rtac nat_induct 1);
mueller@3071
  1093
by (Simp_tac 1);
paulson@3457
  1094
by (rtac allI 1);
mueller@3071
  1095
by (Seq_case_simp_tac "xa" 1);
mueller@3071
  1096
qed"take_lemma_in_eq_out";
mueller@3071
  1097
mueller@3071
  1098
mueller@3071
  1099
(* ------------------------------------------------------------------------------------ *)
mueller@3071
  1100
mueller@3071
  1101
section "alternative take_lemma proofs";
mueller@3071
  1102
mueller@3071
  1103
mueller@3071
  1104
(* --------------------------------------------------------------- *)
mueller@3071
  1105
(*              Alternative Proof of FilterPQ                      *)
mueller@3071
  1106
(* --------------------------------------------------------------- *)
mueller@3071
  1107
mueller@3071
  1108
Delsimps [FilterPQ];
mueller@3071
  1109
mueller@3071
  1110
mueller@3071
  1111
(* In general: How to do this case without the same adm problems 
mueller@3071
  1112
   as for the entire proof ? *) 
wenzelm@5068
  1113
Goal "Forall (%x.~(P x & Q x)) s \
nipkow@10835
  1114
\         --> Filter P$(Filter Q$s) =\
nipkow@10835
  1115
\             Filter (%x. P x & Q x)$s";
mueller@3071
  1116
mueller@3071
  1117
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
mueller@3071
  1118
qed"Filter_lemma1";
mueller@3071
  1119
paulson@6161
  1120
Goal "Finite s ==>  \
mueller@3071
  1121
\         (Forall (%x. (~P x) | (~ Q x)) s  \
nipkow@10835
  1122
\         --> Filter P$(Filter Q$s) = nil)";
mueller@3071
  1123
by (Seq_Finite_induct_tac 1);
mueller@3071
  1124
qed"Filter_lemma2";
mueller@3071
  1125
paulson@6161
  1126
Goal "Finite s ==>  \
mueller@3071
  1127
\         Forall (%x. (~P x) | (~ Q x)) s  \
nipkow@10835
  1128
\         --> Filter (%x. P x & Q x)$s = nil";
mueller@3071
  1129
by (Seq_Finite_induct_tac 1);
mueller@3071
  1130
qed"Filter_lemma3";
mueller@3071
  1131
mueller@3071
  1132
nipkow@10835
  1133
Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s";
wenzelm@3842
  1134
by (res_inst_tac [("A1","%x. True") 
mueller@3275
  1135
                 ,("Q1","%x.~(P x & Q x)"),("x1","s")]
mueller@3071
  1136
                 (take_lemma_induct RS mp) 1);
mueller@5976
  1137
(* better support for A = %x. True *)
mueller@3071
  1138
by (Fast_tac 3);
wenzelm@4098
  1139
by (asm_full_simp_tac (simpset() addsimps [Filter_lemma1]) 1);
nipkow@4833
  1140
by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3]) 1);
mueller@3071
  1141
qed"FilterPQ_takelemma";
mueller@3071
  1142
mueller@3071
  1143
Addsimps [FilterPQ];
mueller@3071
  1144
mueller@3071
  1145
mueller@3071
  1146
(* --------------------------------------------------------------- *)
mueller@3071
  1147
(*              Alternative Proof of MapConc                       *)
mueller@3071
  1148
(* --------------------------------------------------------------- *)
mueller@3071
  1149
mueller@3275
  1150
mueller@3071
  1151
nipkow@10835
  1152
Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)";
paulson@4477
  1153
by (res_inst_tac [("A1","%x. True"), ("x1","x")]
paulson@4477
  1154
    (take_lemma_in_eq_out RS mp) 1);
paulson@4477
  1155
by Auto_tac;
mueller@3071
  1156
qed"MapConc_takelemma";
mueller@3071
  1157
mueller@3071
  1158