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