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