# HG changeset patch
# User huffman
# Date 1146628571 -7200
# Node ID 4103954f3668c60afc014a58a7dcb7295af85d70
# Parent  ae77a20f6995aa0c8ba4c1bbfb78a269e15c5ef8
converted to isar theory; removed unsound adm_all axiom

diff -r ae77a20f6995 -r 4103954f3668 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed May 03 03:47:15 2006 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed May 03 05:56:11 2006 +0200
@@ -3,237 +3,8 @@
     Author:     Olaf Mller
 *)
 
-Addsimps [andalso_and,andalso_or];
-
 (* ----------------------------------------------------------------------------------- *)
 
-section "recursive equations of operators";
-
-(* ---------------------------------------------------------------- *)
-(*                               Map                                *)
-(* ---------------------------------------------------------------- *)
-
-Goal "Map f$UU =UU";
-by (simp_tac (simpset() addsimps [Map_def]) 1);
-qed"Map_UU";
-
-Goal "Map f$nil =nil";
-by (simp_tac (simpset() addsimps [Map_def]) 1);
-qed"Map_nil";
-
-Goal "Map f$(x>>xs)=(f x) >> Map f$xs";
-by (simp_tac (simpset() addsimps [Map_def, Consq_def,flift2_def]) 1);
-qed"Map_cons";
-
-(* ---------------------------------------------------------------- *)
-(*                               Filter                             *)
-(* ---------------------------------------------------------------- *)
-
-Goal "Filter P$UU =UU";
-by (simp_tac (simpset() addsimps [Filter_def]) 1);
-qed"Filter_UU";
-
-Goal "Filter P$nil =nil";
-by (simp_tac (simpset() addsimps [Filter_def]) 1);
-qed"Filter_nil";
-
-Goal "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)";
-by (simp_tac (simpset() addsimps [Filter_def, Consq_def,flift2_def,If_and_if]) 1);
-qed"Filter_cons";
-
-(* ---------------------------------------------------------------- *)
-(*                               Forall                             *)
-(* ---------------------------------------------------------------- *)
-
-Goal "Forall P UU";
-by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
-qed"Forall_UU";
-
-Goal "Forall P nil";
-by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
-qed"Forall_nil";
-
-Goal "Forall P (x>>xs)= (P x & Forall P xs)";
-by (simp_tac (simpset() addsimps [Forall_def, sforall_def,
-                                 Consq_def,flift2_def]) 1);
-qed"Forall_cons";
-
-(* ---------------------------------------------------------------- *)
-(*                               Conc                               *)
-(* ---------------------------------------------------------------- *)
-
-
-Goal "(x>>xs) @@ y = x>>(xs @@y)";
-by (simp_tac (simpset() addsimps [Consq_def]) 1);
-qed"Conc_cons";
-
-(* ---------------------------------------------------------------- *)
-(*                               Takewhile                          *)
-(* ---------------------------------------------------------------- *)
-
-Goal "Takewhile P$UU =UU";
-by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
-qed"Takewhile_UU";
-
-Goal "Takewhile P$nil =nil";
-by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
-qed"Takewhile_nil";
-
-Goal "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)";
-by (simp_tac (simpset() addsimps [Takewhile_def, Consq_def,flift2_def,If_and_if]) 1);
-qed"Takewhile_cons";
-
-(* ---------------------------------------------------------------- *)
-(*                               Dropwhile                          *)
-(* ---------------------------------------------------------------- *)
-
-Goal "Dropwhile P$UU =UU";
-by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
-qed"Dropwhile_UU";
-
-Goal "Dropwhile P$nil =nil";
-by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
-qed"Dropwhile_nil";
-
-Goal "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)";
-by (simp_tac (simpset() addsimps [Dropwhile_def, Consq_def,flift2_def,If_and_if]) 1);
-qed"Dropwhile_cons";
-
-(* ---------------------------------------------------------------- *)
-(*                               Last                               *)
-(* ---------------------------------------------------------------- *)
-
-
-Goal "Last$UU =UU";
-by (simp_tac (simpset() addsimps [Last_def]) 1);
-qed"Last_UU";
-
-Goal "Last$nil =UU";
-by (simp_tac (simpset() addsimps [Last_def]) 1);
-qed"Last_nil";
-
-Goal "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)";
-by (simp_tac (simpset() addsimps [Last_def, Consq_def]) 1);
-by (res_inst_tac [("x","xs")] seq.casedist 1);
-by (Asm_simp_tac 1);
-by (REPEAT (Asm_simp_tac 1));
-qed"Last_cons";
-
-
-(* ---------------------------------------------------------------- *)
-(*                               Flat                               *)
-(* ---------------------------------------------------------------- *)
-
-Goal "Flat$UU =UU";
-by (simp_tac (simpset() addsimps [Flat_def]) 1);
-qed"Flat_UU";
-
-Goal "Flat$nil =nil";
-by (simp_tac (simpset() addsimps [Flat_def]) 1);
-qed"Flat_nil";
-
-Goal "Flat$(x##xs)= x @@ (Flat$xs)";
-by (simp_tac (simpset() addsimps [Flat_def, Consq_def]) 1);
-qed"Flat_cons";
-
-
-(* ---------------------------------------------------------------- *)
-(*                               Zip                                *)
-(* ---------------------------------------------------------------- *)
-
-Goal "Zip = (LAM t1 t2. case t1 of \
-\               nil   => nil \
-\             | x##xs => (case t2 of \
-\                          nil => UU  \
-\                        | y##ys => (case x of \
-\                                      UU  => UU \
-\                                    | Def a => (case y of \
-\                                                  UU => UU \
-\                                                | Def b => Def (a,b)##(Zip$xs$ys)))))";
-by (rtac trans 1);
-by (rtac fix_eq2 1);
-by (rtac Zip_def 1);
-by (rtac beta_cfun 1);
-by (Simp_tac 1);
-qed"Zip_unfold";
-
-Goal "Zip$UU$y =UU";
-by (stac Zip_unfold 1);
-by (Simp_tac 1);
-qed"Zip_UU1";
-
-Goal "x~=nil ==> Zip$x$UU =UU";
-by (stac Zip_unfold 1);
-by (Simp_tac 1);
-by (res_inst_tac [("x","x")] seq.casedist 1);
-by (REPEAT (Asm_full_simp_tac 1));
-qed"Zip_UU2";
-
-Goal "Zip$nil$y =nil";
-by (stac Zip_unfold 1);
-by (Simp_tac 1);
-qed"Zip_nil";
-
-Goal "Zip$(x>>xs)$nil= UU";
-by (stac Zip_unfold 1);
-by (simp_tac (simpset() addsimps [Consq_def]) 1);
-qed"Zip_cons_nil";
-
-Goal "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys";
-by (rtac trans 1);
-by (stac Zip_unfold 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsimps [Consq_def]) 1);
-qed"Zip_cons";
-
-
-Delsimps [sfilter_UU,sfilter_nil,sfilter_cons,
-          smap_UU,smap_nil,smap_cons,
-          sforall2_UU,sforall2_nil,sforall2_cons,
-          slast_UU,slast_nil,slast_cons,
-          stakewhile_UU, stakewhile_nil, stakewhile_cons,
-          sdropwhile_UU, sdropwhile_nil, sdropwhile_cons,
-          sflat_UU,sflat_nil,sflat_cons,
-          szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons];
-
-
-Addsimps [Filter_UU,Filter_nil,Filter_cons,
-          Map_UU,Map_nil,Map_cons,
-          Forall_UU,Forall_nil,Forall_cons,
-          Last_UU,Last_nil,Last_cons,
-          Conc_cons,
-          Takewhile_UU, Takewhile_nil, Takewhile_cons,
-          Dropwhile_UU, Dropwhile_nil, Dropwhile_cons,
-          Zip_UU1,Zip_UU2,Zip_nil,Zip_cons_nil,Zip_cons];
-
-
-
-(* ------------------------------------------------------------------------------------- *)
-
-
-section "Cons";
-
-Goal "a>>s = (Def a)##s";
-by (simp_tac (simpset() addsimps [Consq_def]) 1);
-qed"Consq_def2";
-
-Goal "x = UU | x = nil | (? a s. x = a >> s)";
-by (simp_tac (simpset() addsimps [Consq_def2]) 1);
-by (cut_facts_tac [seq.exhaust] 1);
-by (fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]) 1);
-qed"Seq_exhaust";
-
-
-Goal "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s  ==> P |] ==> P";
-by (cut_inst_tac [("x","x")] Seq_exhaust 1);
-by (etac disjE 1);
-by (Asm_full_simp_tac 1);
-by (etac disjE 1);
-by (Asm_full_simp_tac 1);
-by (REPEAT (etac exE 1));
-by (Asm_full_simp_tac 1);
-qed"Seq_cases";
-
 fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i
           THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
 
@@ -242,100 +13,6 @@
                                              THEN Asm_full_simp_tac (i+1)
                                              THEN Asm_full_simp_tac i;
 
-Goal "a>>s ~= UU";
-by (stac Consq_def2 1);
-by (resolve_tac seq.con_rews 1);
-by (rtac Def_not_UU 1);
-qed"Cons_not_UU";
-
-
-Goal "~(a>>x) << UU";
-by (rtac notI 1);
-by (dtac antisym_less 1);
-by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_not_UU]) 1);
-qed"Cons_not_less_UU";
-
-Goal "~a>>s << nil";
-by (stac Consq_def2 1);
-by (resolve_tac seq.rews 1);
-by (rtac Def_not_UU 1);
-qed"Cons_not_less_nil";
-
-Goal "a>>s ~= nil";
-by (stac Consq_def2 1);
-by (resolve_tac seq.rews 1);
-qed"Cons_not_nil";
-
-Goal "nil ~= a>>s";
-by (simp_tac (simpset() addsimps [Consq_def2]) 1);
-qed"Cons_not_nil2";
-
-Goal "(a>>s = b>>t) = (a = b & s = t)";
-by (simp_tac (HOL_ss addsimps [Consq_def2]) 1);
-by (stac (hd lift.inject RS sym) 1);
-back(); back();
-by (rtac scons_inject_eq 1);
-by (REPEAT(rtac Def_not_UU 1));
-qed"Cons_inject_eq";
-
-Goal "(a>>s<<b>>t) = (a = b & s<<t)";
-by (simp_tac (simpset() addsimps [Consq_def2]) 1);
-by (simp_tac (simpset() addsimps [seq.inverts]) 1);
-(*by (stac (Def_inject_less_eq RS sym) 1);
-back();
-by (rtac iffI 1);
-by (etac (hd seq.inverts) 1);
-by (REPEAT(rtac Def_not_UU 1));
-by (Asm_full_simp_tac 1);
-by (etac conjE 1);
-by (etac monofun_cfun_arg 1);*)
-qed"Cons_inject_less_eq";
-
-Goal "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)";
-by (simp_tac (simpset() addsimps [Consq_def]) 1);
-qed"seq_take_Cons";
-
-Addsimps [Cons_not_nil2,Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
-          Cons_not_UU,Cons_not_less_UU,Cons_not_less_nil,Cons_not_nil];
-
-(* Instead of adding UU_neq_Cons every equation UU~=x could be changed to x~=UU *)
-(*
-Goal "UU ~= x>>xs";
-by (res_inst_tac [("s1","UU"),("t1","x>>xs")]  (sym RS rev_contrapos) 1);
-by (REPEAT (Simp_tac 1));
-qed"UU_neq_Cons";
-
-Addsimps [UU_neq_Cons];
-*)
-
-(* ----------------------------------------------------------------------------------- *)
-
-section "induction";
-
-Goal "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x";
-by (etac seq.ind 1);
-by (REPEAT (atac 1));
-by (def_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
-qed"Seq_induct";
-
-Goal "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]  \
-\               ==> seq_finite x --> P x";
-by (etac seq_finite_ind 1);
-by (REPEAT (atac 1));
-by (def_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
-qed"Seq_FinitePartial_ind";
-
-Goal "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
-by (etac sfinite.induct 1);
-by (assume_tac 1);
-by (def_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
-qed"Seq_Finite_ind";
-
-
 (* rws are definitions to be unfolded for admissibility check *)
 fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
                          THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
@@ -353,718 +30,3 @@
            THEN pair_tac "a" (i+3)
            THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1))))
            THEN simp_tac (simpset() addsimps rws) i;
-
-
-
-(* ------------------------------------------------------------------------------------ *)
-
-section "HD,TL";
-
-Goal "HD$(x>>y) = Def x";
-by (simp_tac (simpset() addsimps [Consq_def]) 1);
-qed"HD_Cons";
-
-Goal "TL$(x>>y) = y";
-by (simp_tac (simpset() addsimps [Consq_def]) 1);
-qed"TL_Cons";
-
-Addsimps [HD_Cons,TL_Cons];
-
-(* ------------------------------------------------------------------------------------ *)
-
-section "Finite, Partial, Infinite";
-
-Goal "Finite (a>>xs) = Finite xs";
-by (simp_tac (simpset() addsimps [Consq_def2,Finite_cons]) 1);
-qed"Finite_Cons";
-
-Addsimps [Finite_Cons];
-Goal "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
-by (Seq_Finite_induct_tac 1);
-qed"FiniteConc_1";
-
-Goal "Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
-by (Seq_Finite_induct_tac 1);
-(* nil*)
-by (strip_tac 1);
-by (Seq_case_simp_tac "x" 1);
-by (Asm_full_simp_tac 1);
-(* cons *)
-by (strip_tac 1);
-by (Seq_case_simp_tac "x" 1);
-by (Seq_case_simp_tac "y" 1);
-by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
-by (eres_inst_tac [("x","sa")] allE 1);
-by (eres_inst_tac [("x","y")] allE 1);
-by (Asm_full_simp_tac 1);
-qed"FiniteConc_2";
-
-Goal "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)";
-by (rtac iffI 1);
-by (etac (FiniteConc_2 RS spec RS spec RS mp) 1);
-by (rtac refl 1);
-by (rtac (FiniteConc_1 RS mp) 1);
-by Auto_tac;
-qed"FiniteConc";
-
-Addsimps [FiniteConc];
-
-
-Goal "Finite s ==> Finite (Map f$s)";
-by (Seq_Finite_induct_tac 1);
-qed"FiniteMap1";
-
-Goal "Finite s ==> ! t. (s = Map f$t) --> Finite t";
-by (Seq_Finite_induct_tac 1);
-by (strip_tac 1);
-by (Seq_case_simp_tac "t" 1);
-by (Asm_full_simp_tac 1);
-(* main case *)
-by Auto_tac;
-by (Seq_case_simp_tac "t" 1);
-by (Asm_full_simp_tac 1);
-qed"FiniteMap2";
-
-Goal "Finite (Map f$s) = Finite s";
-by Auto_tac;
-by (etac (FiniteMap2 RS spec RS mp) 1);
-by (rtac refl 1);
-by (etac FiniteMap1 1);
-qed"Map2Finite";
-
-
-Goal "Finite s ==> Finite (Filter P$s)";
-by (Seq_Finite_induct_tac 1);
-qed"FiniteFilter";
-
-
-(* ----------------------------------------------------------------------------------- *)
-
-
-section "admissibility";
-
-(* Finite x is proven to be adm: Finite_flat shows that there are only chains of length one.
-   Then the assumption that an _infinite_ chain exists (from admI2) is set to a contradiction
-   to Finite_flat *)
-
-Goal "!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y";
-by (Seq_Finite_induct_tac 1);
-by (strip_tac 1);
-by (etac conjE 1);
-by (etac nil_less_is_nil 1);
-(* main case *)
-by Auto_tac;
-by (Seq_case_simp_tac "y" 1);
-by Auto_tac;
-qed_spec_mp"Finite_flat";
-
-
-Goal "adm(%(x:: 'a Seq).Finite x)";
-by (rtac admI2 1);
-by (eres_inst_tac [("x","0")] allE 1);
-back();
-by (etac exE 1);
-by (REPEAT (etac conjE 1));
-by (res_inst_tac [("x","0")] allE 1);
-by (assume_tac 1);
-by (eres_inst_tac [("x","j")] allE 1);
-by (cut_inst_tac [("x","Y 0"),("y","Y j")] Finite_flat 1);
-(* Generates a contradiction in subgoal 3 *)
-by Auto_tac;
-qed"adm_Finite";
-
-Addsimps [adm_Finite];
-
-
-(* ------------------------------------------------------------------------------------ *)
-
-section "Conc";
-
-Goal "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)";
-by (Seq_Finite_induct_tac 1);
-qed"Conc_cong";
-
-Goal "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z";
-by (Seq_induct_tac "x" [] 1);
-qed"Conc_assoc";
-
-Goal "s@@ nil = s";
-by (res_inst_tac[("x","s")] seq.ind 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (Asm_full_simp_tac 1);
-qed"nilConc";
-
-Addsimps [nilConc];
-
-(* should be same as nil_is_Conc2 when all nils are turned to right side !! *)
-Goal "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
-by (Seq_case_simp_tac "x" 1);
-by Auto_tac;
-qed"nil_is_Conc";
-
-Goal "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)";
-by (Seq_case_simp_tac "x" 1);
-by Auto_tac;
-qed"nil_is_Conc2";
-
-
-(* ------------------------------------------------------------------------------------ *)
-
-section "Last";
-
-Goal "Finite s ==> s~=nil --> Last$s~=UU";
-by (Seq_Finite_induct_tac  1);
-qed"Finite_Last1";
-
-Goal "Finite s ==> Last$s=UU --> s=nil";
-by (Seq_Finite_induct_tac  1);
-by (fast_tac HOL_cs 1);
-qed"Finite_Last2";
-
-
-(* ------------------------------------------------------------------------------------ *)
-
-
-section "Filter, Conc";
-
-
-Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s";
-by (Seq_induct_tac "s" [Filter_def] 1);
-qed"FilterPQ";
-
-Goal "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)";
-by (simp_tac (simpset() addsimps [Filter_def,sfiltersconc]) 1);
-qed"FilterConc";
-
-(* ------------------------------------------------------------------------------------ *)
-
-section "Map";
-
-Goal "Map f$(Map g$s) = Map (f o g)$s";
-by (Seq_induct_tac "s" [] 1);
-qed"MapMap";
-
-Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)";
-by (Seq_induct_tac "x" [] 1);
-qed"MapConc";
-
-Goal "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)";
-by (Seq_induct_tac "x" [] 1);
-qed"MapFilter";
-
-Goal "nil = (Map f$s) --> s= nil";
-by (Seq_case_simp_tac "s" 1);
-qed"nilMap";
-
-
-Goal "Forall P (Map f$s) = Forall (P o f) s";
-by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-qed"ForallMap";
-
-
-
-
-(* ------------------------------------------------------------------------------------ *)
-
-section "Forall";
-
-
-Goal "Forall P ys & (! x. P x --> Q x) \
-\         --> Forall Q ys";
-by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
-qed"ForallPForallQ1";
-
-bind_thm ("ForallPForallQ",impI RSN (2,allI RSN (2,conjI RS (ForallPForallQ1 RS mp))));
-
-Goal "(Forall P x & Forall P y) --> Forall P (x @@ y)";
-by (Seq_induct_tac "x" [Forall_def,sforall_def] 1);
-qed"Forall_Conc_impl";
-
-Goal "Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
-by (Seq_Finite_induct_tac  1);
-qed"Forall_Conc";
-
-Addsimps [Forall_Conc];
-
-Goal "Forall P s  --> Forall P (TL$s)";
-by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-qed"ForallTL1";
-
-bind_thm ("ForallTL",ForallTL1 RS mp);
-
-Goal "Forall P s  --> Forall P (Dropwhile Q$s)";
-by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-qed"ForallDropwhile1";
-
-bind_thm ("ForallDropwhile",ForallDropwhile1 RS mp);
-
-
-(* only admissible in t, not if done in s *)
-
-Goal "! s. Forall P s --> t<<s --> Forall P t";
-by (Seq_induct_tac "t" [Forall_def,sforall_def] 1);
-by (strip_tac 1);
-by (Seq_case_simp_tac "sa" 1);
-by (Asm_full_simp_tac 1);
-by Auto_tac;
-qed"Forall_prefix";
-
-bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
-
-
-Goal "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
-by Auto_tac;
-qed"Forall_postfixclosed";
-
-
-Goal "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr";
-by (Seq_induct_tac "tr" [Forall_def,sforall_def] 1);
-qed"ForallPFilterQR1";
-
-bind_thm("ForallPFilterQR",allI RS (conjI RS (ForallPFilterQR1 RS mp)));
-
-
-(* ------------------------------------------------------------------------------------- *)
-
-section "Forall, Filter";
-
-
-Goal "Forall P (Filter P$x)";
-by (simp_tac (simpset() addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
-qed"ForallPFilterP";
-
-(* holds also in other direction, then equal to forallPfilterP *)
-Goal "Forall P x --> Filter P$x = x";
-by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);
-qed"ForallPFilterPid1";
-
-bind_thm("ForallPFilterPid",ForallPFilterPid1 RS mp);
-
-
-(* holds also in other direction *)
-Goal "!! ys . Finite ys ==> \
-\   Forall (%x. ~P x) ys --> Filter P$ys = nil ";
-by (Seq_Finite_induct_tac 1);
-qed"ForallnPFilterPnil1";
-
-bind_thm ("ForallnPFilterPnil",ForallnPFilterPnil1 RS mp);
-
-
-(* holds also in other direction *)
-Goal   "~Finite ys & Forall (%x. ~P x) ys \
-\                  --> Filter P$ys = UU ";
-by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
-qed"ForallnPFilterPUU1";
-
-bind_thm ("ForallnPFilterPUU",conjI RS (ForallnPFilterPUU1 RS mp));
-
-
-(* inverse of ForallnPFilterPnil *)
-
-Goal "!! ys . Filter P$ys = nil --> \
-\   (Forall (%x. ~P x) ys & Finite ys)";
-by (res_inst_tac[("x","ys")] Seq_induct 1);
-(* adm *)
-(* FIX: not admissible, search other proof!! *)
-by (rtac adm_all 1);
-(* base cases *)
-by (Simp_tac 1);
-by (Simp_tac 1);
-(* main case *)
-by (Asm_full_simp_tac 1);
-qed"FilternPnilForallP1";
-
-bind_thm ("FilternPnilForallP",FilternPnilForallP1 RS mp);
-
-(* inverse of ForallnPFilterPUU. proved by 2 lemmas because of adm problems *)
-
-Goal "Finite ys ==> Filter P$ys ~= UU";
-by (Seq_Finite_induct_tac 1);
-qed"FilterUU_nFinite_lemma1";
-
-Goal "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU";
-by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
-qed"FilterUU_nFinite_lemma2";
-
-Goal   "Filter P$ys = UU ==> \
-\                (Forall (%x. ~P x) ys  & ~Finite ys)";
-by (rtac conjI 1);
-by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
-by Auto_tac;
-by (blast_tac (claset() addSDs [FilterUU_nFinite_lemma1]) 1);
-qed"FilternPUUForallP";
-
-
-Goal  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
-\   ==> Filter P$ys = nil";
-by (etac ForallnPFilterPnil 1);
-by (etac ForallPForallQ 1);
-by Auto_tac;
-qed"ForallQFilterPnil";
-
-Goal "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|] \
-\   ==> Filter P$ys = UU ";
-by (etac ForallnPFilterPUU 1);
-by (etac ForallPForallQ 1);
-by Auto_tac;
-qed"ForallQFilterPUU";
-
-
-
-(* ------------------------------------------------------------------------------------- *)
-
-section "Takewhile, Forall, Filter";
-
-
-Goal "Forall P (Takewhile P$x)";
-by (simp_tac (simpset() addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
-qed"ForallPTakewhileP";
-
-
-Goal"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)";
-by (rtac ForallPForallQ 1);
-by (rtac ForallPTakewhileP 1);
-by Auto_tac;
-qed"ForallPTakewhileQ";
-
-
-Goal  "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |] \
-\   ==> Filter P$(Takewhile Q$ys) = nil";
-by (etac ForallnPFilterPnil 1);
-by (rtac ForallPForallQ 1);
-by (rtac ForallPTakewhileP 1);
-by Auto_tac;
-qed"FilterPTakewhileQnil";
-
-Goal "!! Q P. [| !!x. Q x ==> P x |] ==> \
-\            Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)";
-by (rtac ForallPFilterPid 1);
-by (rtac ForallPForallQ 1);
-by (rtac ForallPTakewhileP 1);
-by Auto_tac;
-qed"FilterPTakewhileQid";
-
-Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
-          FilterPTakewhileQnil,FilterPTakewhileQid];
-
-Goal "Takewhile P$(Takewhile P$s) = Takewhile P$s";
-by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-qed"Takewhile_idempotent";
-
-Goal "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s";
-by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-qed"ForallPTakewhileQnP";
-
-Goal "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s";
-by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-qed"ForallPDropwhileQnP";
-
-Addsimps [ForallPTakewhileQnP RS mp, ForallPDropwhileQnP RS mp];
-
-
-Goal "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)";
-by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-qed"TakewhileConc1";
-
-bind_thm("TakewhileConc",TakewhileConc1 RS mp);
-
-Goal "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t";
-by (Seq_Finite_induct_tac 1);
-qed"DropwhileConc1";
-
-bind_thm("DropwhileConc",DropwhileConc1 RS mp);
-
-
-
-(* ----------------------------------------------------------------------------------- *)
-
-section "coinductive characterizations of Filter";
-
-
-Goal "HD$(Filter P$y) = Def x \
-\         --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y)))  \
-\             & Finite (Takewhile (%x. ~ P x)$y)  & P x";
-
-(* FIX: pay attention: is only admissible with chain-finite package to be added to
-        adm test and Finite f x admissibility *)
-by (Seq_induct_tac "y" [] 1);
-by (rtac adm_all 1);
-by (Asm_full_simp_tac 1);
-by (case_tac "P a" 1);
- by (Asm_full_simp_tac 1);
- by (Blast_tac 1);
-(* ~ P a *)
-by (Asm_full_simp_tac 1);
-qed"divide_Seq_lemma";
-
-Goal "(x>>xs) << Filter P$y  \
-\   ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) \
-\      & Finite (Takewhile (%a. ~ P a)$y)  & P x";
-by (rtac (divide_Seq_lemma RS mp) 1);
-by (dres_inst_tac [("f","HD"),("x","x>>xs")]  monofun_cfun_arg 1);
-by (Asm_full_simp_tac 1);
-qed"divide_Seq";
-
-
-Goal "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)";
-(* Pay attention: is only admissible with chain-finite package to be added to
-        adm test *)
-by (Seq_induct_tac "y" [Forall_def,sforall_def] 1);
-qed"nForall_HDFilter";
-
-
-Goal "~Forall P y  \
-\  ==> ? x. y= (Takewhile P$y @@ (x >> TL$(Dropwhile P$y))) & \
-\      Finite (Takewhile P$y) & (~ P x)";
-by (dtac (nForall_HDFilter RS mp) 1);
-by (safe_tac set_cs);
-by (res_inst_tac [("x","x")] exI 1);
-by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1);
-by Auto_tac;
-qed"divide_Seq2";
-
-
-Goal  "~Forall P y \
-\  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
-by (cut_inst_tac [] divide_Seq2 1);
-(*Auto_tac no longer proves it*)
-by (REPEAT (fast_tac (claset() addss (simpset())) 1));
-qed"divide_Seq3";
-
-Addsimps [FilterPQ,FilterConc,Conc_cong];
-
-
-(* ------------------------------------------------------------------------------------- *)
-
-
-section "take_lemma";
-
-Goal "(!n. seq_take n$x = seq_take n$x') = (x = x')";
-by (rtac iffI 1);
-by (resolve_tac [seq.take_lemmas] 1);
-by Auto_tac;
-qed"seq_take_lemma";
-
-Goal
-"  ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2) \
-\   --> seq_take n$(x @@ (t>>y1)) =  seq_take n$(x @@ (t>>y2)))";
-by (Seq_induct_tac "x" [] 1);
-by (strip_tac 1);
-by (case_tac "n" 1);
-by Auto_tac;
-by (case_tac "n" 1);
-by Auto_tac;
-qed"take_reduction1";
-
-
-Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|] \
-\ ==> seq_take n$(x @@ (s>>y1)) =  seq_take n$(y @@ (t>>y2))";
-
-by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset()));
-qed"take_reduction";
-
-(* ------------------------------------------------------------------
-          take-lemma and take_reduction for << instead of =
-   ------------------------------------------------------------------ *)
-
-Goal
-"  ! n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2) \
-\   --> seq_take n$(x @@ (t>>y1)) <<  seq_take n$(x @@ (t>>y2)))";
-by (Seq_induct_tac "x" [] 1);
-by (strip_tac 1);
-by (case_tac "n" 1);
-by Auto_tac;
-by (case_tac "n" 1);
-by Auto_tac;
-qed"take_reduction_less1";
-
-
-Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|] \
-\ ==> seq_take n$(x @@ (s>>y1)) <<  seq_take n$(y @@ (t>>y2))";
-by (auto_tac (claset() addSIs [take_reduction_less1 RS spec RS mp],simpset()));
-qed"take_reduction_less";
-
-
-val prems = goalw (the_context ()) [seq.take_def]
-"(!! n. seq_take n$s1 << seq_take n$s2)  ==> s1<<s2";
-
-by (res_inst_tac [("t","s1")] (seq.reach RS subst)  1);
-by (res_inst_tac [("t","s2")] (seq.reach RS subst)  1);
-by (rtac (fix_def2 RS ssubst ) 1);
-by (stac contlub_cfun_fun 1);
-by (rtac chain_iterate 1);
-by (stac contlub_cfun_fun 1);
-by (rtac chain_iterate 1);
-by (rtac lub_mono 1);
-by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1);
-by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1);
-by (rtac allI 1);
-by (resolve_tac prems 1);
-qed"take_lemma_less1";
-
-
-Goal "(!n. seq_take n$x << seq_take n$x') = (x << x')";
-by (rtac iffI 1);
-by (rtac take_lemma_less1 1);
-by Auto_tac;
-by (etac monofun_cfun_arg 1);
-qed"take_lemma_less";
-
-(* ------------------------------------------------------------------
-          take-lemma proof principles
-   ------------------------------------------------------------------ *)
-
-Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
-\           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
-\                         ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |] \
-\              ==> A x --> (f x)=(g x)";
-by (case_tac "Forall Q x" 1);
-by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
-qed"take_lemma_principle1";
-
-Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
-\           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
-\                         ==> ! n. seq_take n$(f (s1 @@ y>>s2)) \
-\                                = seq_take n$(g (s1 @@ y>>s2)) |] \
-\              ==> A x --> (f x)=(g x)";
-by (case_tac "Forall Q x" 1);
-by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
-by (resolve_tac [seq.take_lemmas] 1);
-by Auto_tac;
-qed"take_lemma_principle2";
-
-
-(* Note: in the following proofs the ordering of proof steps is very
-         important, as otherwise either (Forall Q s1) would be in the IH as
-         assumption (then rule useless) or it is not possible to strengthen
-         the IH by doing a forall closure of the sequence t (then rule also useless).
-         This is also the reason why the induction rule (nat_less_induct or nat_induct) has to
-         to be imbuilt into the rule, as induction has to be done early and the take lemma
-         has to be used in the trivial direction afterwards for the (Forall Q x) case.  *)
-
-Goal
-"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
-\        !! s1 s2 y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\
-\                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
-\                         ==>   seq_take (Suc n)$(f (s1 @@ y>>s2)) \
-\                             = seq_take (Suc n)$(g (s1 @@ y>>s2)) |] \
-\              ==> A x --> (f x)=(g x)";
-by (rtac impI 1);
-by (resolve_tac [seq.take_lemmas] 1);
-by (rtac mp 1);
-by (assume_tac 2);
-by (res_inst_tac [("x","x")] spec 1);
-by (rtac nat_induct 1);
-by (Simp_tac 1);
-by (rtac allI 1);
-by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
-                           simpset())) 1);
-by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
-qed"take_lemma_induct";
-
-
-Goal
-"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
-\        !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m$(f t) = seq_take m$(g t);\
-\                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
-\                         ==>   seq_take n$(f (s1 @@ y>>s2)) \
-\                             = seq_take n$(g (s1 @@ y>>s2)) |] \
-\              ==> A x --> (f x)=(g x)";
-by (rtac impI 1);
-by (resolve_tac [seq.take_lemmas] 1);
-by (rtac mp 1);
-by (assume_tac 2);
-by (res_inst_tac [("x","x")] spec 1);
-by (rtac nat_less_induct 1);
-by (rtac allI 1);
-by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
-                           simpset())) 1);
-by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
-qed"take_lemma_less_induct";
-
-
-
-Goal
-"!! Q. [| A UU  ==> (f UU) = (g UU) ; \
-\         A nil ==> (f nil) = (g nil) ; \
-\         !! s y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\
-\                    A (y>>s) |]   \
-\                    ==>   seq_take (Suc n)$(f (y>>s)) \
-\                        = seq_take (Suc n)$(g (y>>s)) |] \
-\              ==> A x --> (f x)=(g x)";
-by (rtac impI 1);
-by (resolve_tac [seq.take_lemmas] 1);
-by (rtac mp 1);
-by (assume_tac 2);
-by (res_inst_tac [("x","x")] spec 1);
-by (rtac nat_induct 1);
-by (Simp_tac 1);
-by (rtac allI 1);
-by (Seq_case_simp_tac "xa" 1);
-qed"take_lemma_in_eq_out";
-
-
-(* ------------------------------------------------------------------------------------ *)
-
-section "alternative take_lemma proofs";
-
-
-(* --------------------------------------------------------------- *)
-(*              Alternative Proof of FilterPQ                      *)
-(* --------------------------------------------------------------- *)
-
-Delsimps [FilterPQ];
-
-
-(* In general: How to do this case without the same adm problems
-   as for the entire proof ? *)
-Goal "Forall (%x.~(P x & Q x)) s \
-\         --> Filter P$(Filter Q$s) =\
-\             Filter (%x. P x & Q x)$s";
-
-by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-qed"Filter_lemma1";
-
-Goal "Finite s ==>  \
-\         (Forall (%x. (~P x) | (~ Q x)) s  \
-\         --> Filter P$(Filter Q$s) = nil)";
-by (Seq_Finite_induct_tac 1);
-qed"Filter_lemma2";
-
-Goal "Finite s ==>  \
-\         Forall (%x. (~P x) | (~ Q x)) s  \
-\         --> Filter (%x. P x & Q x)$s = nil";
-by (Seq_Finite_induct_tac 1);
-qed"Filter_lemma3";
-
-
-Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s";
-by (res_inst_tac [("A1","%x. True")
-                 ,("Q1","%x.~(P x & Q x)"),("x1","s")]
-                 (take_lemma_induct RS mp) 1);
-(* better support for A = %x. True *)
-by (Fast_tac 3);
-by (asm_full_simp_tac (simpset() addsimps [Filter_lemma1]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3]) 1);
-qed"FilterPQ_takelemma";
-
-Addsimps [FilterPQ];
-
-
-(* --------------------------------------------------------------- *)
-(*              Alternative Proof of MapConc                       *)
-(* --------------------------------------------------------------- *)
-
-
-
-Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)";
-by (res_inst_tac [("A1","%x. True"), ("x1","x")]
-    (take_lemma_in_eq_out RS mp) 1);
-by Auto_tac;
-qed"MapConc_takelemma";
-
-
diff -r ae77a20f6995 -r 4103954f3668 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed May 03 03:47:15 2006 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed May 03 05:56:11 2006 +0200
@@ -81,8 +81,1048 @@
                      then x##(h$xs)
                      else     h$xs))))"
 
-axioms  -- {* for test purposes should be deleted FIX !! *}  (* FIXME *)
-  adm_all: "adm f"
+declare andalso_and [simp]
+declare andalso_or [simp]
+
+subsection "recursive equations of operators"
+
+subsubsection "Map"
+
+lemma Map_UU: "Map f$UU =UU"
+by (simp add: Map_def)
+
+lemma Map_nil: "Map f$nil =nil"
+by (simp add: Map_def)
+
+lemma Map_cons: "Map f$(x>>xs)=(f x) >> Map f$xs"
+by (simp add: Map_def Consq_def flift2_def)
+
+
+subsubsection {* Filter *}
+
+lemma Filter_UU: "Filter P$UU =UU"
+by (simp add: Filter_def)
+
+lemma Filter_nil: "Filter P$nil =nil"
+by (simp add: Filter_def)
+
+lemma Filter_cons:
+  "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)"
+by (simp add: Filter_def Consq_def flift2_def If_and_if)
+
+
+subsubsection {* Forall *}
+
+lemma Forall_UU: "Forall P UU"
+by (simp add: Forall_def sforall_def)
+
+lemma Forall_nil: "Forall P nil"
+by (simp add: Forall_def sforall_def)
+
+lemma Forall_cons: "Forall P (x>>xs)= (P x & Forall P xs)"
+by (simp add: Forall_def sforall_def Consq_def flift2_def)
+
+
+subsubsection {* Conc *}
+
+lemma Conc_cons: "(x>>xs) @@ y = x>>(xs @@y)"
+by (simp add: Consq_def)
+
+
+subsubsection {* Takewhile *}
+
+lemma Takewhile_UU: "Takewhile P$UU =UU"
+by (simp add: Takewhile_def)
+
+lemma Takewhile_nil: "Takewhile P$nil =nil"
+by (simp add: Takewhile_def)
+
+lemma Takewhile_cons:
+  "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)"
+by (simp add: Takewhile_def Consq_def flift2_def If_and_if)
+
+
+subsubsection {* DropWhile *}
+
+lemma Dropwhile_UU: "Dropwhile P$UU =UU"
+by (simp add: Dropwhile_def)
+
+lemma Dropwhile_nil: "Dropwhile P$nil =nil"
+by (simp add: Dropwhile_def)
+
+lemma Dropwhile_cons:
+  "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)"
+by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)
+
+
+subsubsection {* Last *}
+
+lemma Last_UU: "Last$UU =UU"
+by (simp add: Last_def)
+
+lemma Last_nil: "Last$nil =UU"
+by (simp add: Last_def)
+
+lemma Last_cons: "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"
+apply (simp add: Last_def Consq_def)
+apply (rule_tac x="xs" in seq.casedist)
+apply simp
+apply simp_all
+done
+
+
+subsubsection {* Flat *}
+
+lemma Flat_UU: "Flat$UU =UU"
+by (simp add: Flat_def)
+
+lemma Flat_nil: "Flat$nil =nil"
+by (simp add: Flat_def)
+
+lemma Flat_cons: "Flat$(x##xs)= x @@ (Flat$xs)"
+by (simp add: Flat_def Consq_def)
+
+
+subsubsection {* Zip *}
+
+lemma Zip_unfold:
+"Zip = (LAM t1 t2. case t1 of
+                nil   => nil
+              | x##xs => (case t2 of
+                           nil => UU
+                         | y##ys => (case x of
+                                       UU  => UU
+                                     | Def a => (case y of
+                                                   UU => UU
+                                                 | Def b => Def (a,b)##(Zip$xs$ys)))))"
+apply (rule trans)
+apply (rule fix_eq2)
+apply (rule Zip_def)
+apply (rule beta_cfun)
+apply simp
+done
+
+lemma Zip_UU1: "Zip$UU$y =UU"
+apply (subst Zip_unfold)
+apply simp
+done
+
+lemma Zip_UU2: "x~=nil ==> Zip$x$UU =UU"
+apply (subst Zip_unfold)
+apply simp
+apply (rule_tac x="x" in seq.casedist)
+apply simp_all
+done
+
+lemma Zip_nil: "Zip$nil$y =nil"
+apply (subst Zip_unfold)
+apply simp
+done
+
+lemma Zip_cons_nil: "Zip$(x>>xs)$nil= UU"
+apply (subst Zip_unfold)
+apply (simp add: Consq_def)
+done
+
+lemma Zip_cons: "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys"
+apply (rule trans)
+apply (subst Zip_unfold)
+apply simp
+apply (simp add: Consq_def)
+done
+
+lemmas [simp del] =
+  sfilter_UU sfilter_nil sfilter_cons
+  smap_UU smap_nil smap_cons
+  sforall2_UU sforall2_nil sforall2_cons
+  slast_UU slast_nil slast_cons
+  stakewhile_UU  stakewhile_nil  stakewhile_cons
+  sdropwhile_UU  sdropwhile_nil  sdropwhile_cons
+  sflat_UU sflat_nil sflat_cons
+  szip_UU1 szip_UU2 szip_nil szip_cons_nil szip_cons
+
+lemmas [simp] =
+  Filter_UU Filter_nil Filter_cons
+  Map_UU Map_nil Map_cons
+  Forall_UU Forall_nil Forall_cons
+  Last_UU Last_nil Last_cons
+  Conc_cons
+  Takewhile_UU Takewhile_nil Takewhile_cons
+  Dropwhile_UU Dropwhile_nil Dropwhile_cons
+  Zip_UU1 Zip_UU2 Zip_nil Zip_cons_nil Zip_cons
+
+
+
+section "Cons"
+
+lemma Consq_def2: "a>>s = (Def a)##s"
+apply (simp add: Consq_def)
+done
+
+lemma Seq_exhaust: "x = UU | x = nil | (? a s. x = a >> s)"
+apply (simp add: Consq_def2)
+apply (cut_tac seq.exhaust)
+apply (fast dest: not_Undef_is_Def [THEN iffD1])
+done
+
+
+lemma Seq_cases:
+"!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s  ==> P |] ==> P"
+apply (cut_tac x="x" in Seq_exhaust)
+apply (erule disjE)
+apply simp
+apply (erule disjE)
+apply simp
+apply (erule exE)+
+apply simp
+done
+
+(*
+fun Seq_case_tac s i = rule_tac x",s)] Seq_cases i
+          THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
+*)
+(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
+(*
+fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2)
+                                             THEN Asm_full_simp_tac (i+1)
+                                             THEN Asm_full_simp_tac i;
+*)
+
+lemma Cons_not_UU: "a>>s ~= UU"
+apply (subst Consq_def2)
+apply (rule seq.con_rews)
+apply (rule Def_not_UU)
+done
+
+
+lemma Cons_not_less_UU: "~(a>>x) << UU"
+apply (rule notI)
+apply (drule antisym_less)
+apply simp
+apply (simp add: Cons_not_UU)
+done
+
+lemma Cons_not_less_nil: "~a>>s << nil"
+apply (subst Consq_def2)
+apply (rule seq.rews)
+apply (rule Def_not_UU)
+done
+
+lemma Cons_not_nil: "a>>s ~= nil"
+apply (subst Consq_def2)
+apply (rule seq.rews)
+done
+
+lemma Cons_not_nil2: "nil ~= a>>s"
+apply (simp add: Consq_def2)
+done
+
+lemma Cons_inject_eq: "(a>>s = b>>t) = (a = b & s = t)"
+apply (simp only: Consq_def2)
+apply (simp add: scons_inject_eq)
+done
+
+lemma Cons_inject_less_eq: "(a>>s<<b>>t) = (a = b & s<<t)"
+apply (simp add: Consq_def2)
+apply (simp add: seq.inverts)
+done
+
+lemma seq_take_Cons: "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)"
+apply (simp add: Consq_def)
+done
+
+lemmas [simp] =
+  Cons_not_nil2 Cons_inject_eq Cons_inject_less_eq seq_take_Cons
+  Cons_not_UU Cons_not_less_UU Cons_not_less_nil Cons_not_nil
+
+
+subsection "induction"
+
+lemma Seq_induct:
+"!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x"
+apply (erule (2) seq.ind)
+apply (tactic {* def_tac 1 *})
+apply (simp add: Consq_def)
+done
+
+lemma Seq_FinitePartial_ind:
+"!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]
+                ==> seq_finite x --> P x"
+apply (erule (1) seq_finite_ind)
+apply (tactic {* def_tac 1 *})
+apply (simp add: Consq_def)
+done
+
+lemma Seq_Finite_ind:
+"!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x"
+apply (erule (1) sfinite.induct)
+apply (tactic {* def_tac 1 *})
+apply (simp add: Consq_def)
+done
+
+
+(* rws are definitions to be unfolded for admissibility check *)
+(*
+fun Seq_induct_tac s rws i = rule_tac x",s)] Seq_induct i
+                         THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
+                         THEN simp add: rws) i;
+
+fun Seq_Finite_induct_tac i = erule Seq_Finite_ind i
+                              THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
+
+fun pair_tac s = rule_tac p",s)] PairE
+                          THEN' hyp_subst_tac THEN' Simp_tac;
+*)
+(* induction on a sequence of pairs with pairsplitting and simplification *)
+(*
+fun pair_induct_tac s rws i =
+           rule_tac x",s)] Seq_induct i
+           THEN pair_tac "a" (i+3)
+           THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1))))
+           THEN simp add: rws) i;
+*)
+
+
+(* ------------------------------------------------------------------------------------ *)
+
+subsection "HD,TL"
+
+lemma HD_Cons [simp]: "HD$(x>>y) = Def x"
+apply (simp add: Consq_def)
+done
+
+lemma TL_Cons [simp]: "TL$(x>>y) = y"
+apply (simp add: Consq_def)
+done
+
+(* ------------------------------------------------------------------------------------ *)
+
+subsection "Finite, Partial, Infinite"
+
+lemma Finite_Cons [simp]: "Finite (a>>xs) = Finite xs"
+apply (simp add: Consq_def2 Finite_cons)
+done
+
+lemma FiniteConc_1: "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)"
+apply (erule Seq_Finite_ind, simp_all)
+done
+
+lemma FiniteConc_2:
+"Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)"
+apply (erule Seq_Finite_ind)
+(* nil*)
+apply (intro strip)
+apply (rule_tac x="x" in Seq_cases, simp_all)
+(* cons *)
+apply (intro strip)
+apply (rule_tac x="x" in Seq_cases, simp_all)
+apply (rule_tac x="y" in Seq_cases, simp_all)
+done
+
+lemma FiniteConc [simp]: "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)"
+apply (rule iffI)
+apply (erule FiniteConc_2 [rule_format])
+apply (rule refl)
+apply (rule FiniteConc_1 [rule_format])
+apply auto
+done
+
+
+lemma FiniteMap1: "Finite s ==> Finite (Map f$s)"
+apply (erule Seq_Finite_ind, simp_all)
+done
+
+lemma FiniteMap2: "Finite s ==> ! t. (s = Map f$t) --> Finite t"
+apply (erule Seq_Finite_ind)
+apply (intro strip)
+apply (rule_tac x="t" in Seq_cases, simp_all)
+(* main case *)
+apply auto
+apply (rule_tac x="t" in Seq_cases, simp_all)
+done
+
+lemma Map2Finite: "Finite (Map f$s) = Finite s"
+apply auto
+apply (erule FiniteMap2 [rule_format])
+apply (rule refl)
+apply (erule FiniteMap1)
+done
+
+
+lemma FiniteFilter: "Finite s ==> Finite (Filter P$s)"
+apply (erule Seq_Finite_ind, simp_all)
+done
+
+
+(* ----------------------------------------------------------------------------------- *)
+
+
+subsection "admissibility"
+
+(* Finite x is proven to be adm: Finite_flat shows that there are only chains of length one.
+   Then the assumption that an _infinite_ chain exists (from admI2) is set to a contradiction
+   to Finite_flat *)
+
+lemma Finite_flat [rule_format]:
+"!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y"
+apply (erule Seq_Finite_ind)
+apply (intro strip)
+apply (erule conjE)
+apply (erule nil_less_is_nil)
+(* main case *)
+apply auto
+apply (rule_tac x="y" in Seq_cases)
+apply auto
+done
+
+
+lemma adm_Finite [simp]: "adm(%(x:: 'a Seq).Finite x)"
+apply (rule admI2)
+apply (erule_tac x="0" in allE)
+back
+apply (erule exE)
+apply (erule conjE)+
+apply (rule_tac x="0" in allE)
+apply assumption
+apply (erule_tac x="j" in allE)
+apply (cut_tac x="Y 0" and y="Y j" in Finite_flat)
+(* Generates a contradiction in subgoal 3 *)
+apply auto
+done
+
+
+(* ------------------------------------------------------------------------------------ *)
+
+subsection "Conc"
+
+lemma Conc_cong: "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)"
+apply (erule Seq_Finite_ind, simp_all)
+done
+
+lemma Conc_assoc: "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z"
+apply (rule_tac x="x" in Seq_induct, simp_all)
+done
+
+lemma nilConc [simp]: "s@@ nil = s"
+apply (rule_tac x="s" in seq.ind)
+apply simp
+apply simp
+apply simp
+apply simp
+done
+
+
+(* should be same as nil_is_Conc2 when all nils are turned to right side !! *)
+lemma nil_is_Conc: "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)"
+apply (rule_tac x="x" in Seq_cases)
+apply auto
+done
+
+lemma nil_is_Conc2: "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)"
+apply (rule_tac x="x" in Seq_cases)
+apply auto
+done
+
+
+(* ------------------------------------------------------------------------------------ *)
+
+subsection "Last"
+
+lemma Finite_Last1: "Finite s ==> s~=nil --> Last$s~=UU"
+apply (erule Seq_Finite_ind, simp_all)
+done
+
+lemma Finite_Last2: "Finite s ==> Last$s=UU --> s=nil"
+apply (erule Seq_Finite_ind, simp_all)
+apply fast
+done
+
+
+(* ------------------------------------------------------------------------------------ *)
+
+
+subsection "Filter, Conc"
+
+
+lemma FilterPQ: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
+apply (rule_tac x="s" in Seq_induct, simp_all)
+done
+
+lemma FilterConc: "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)"
+apply (simp add: Filter_def sfiltersconc)
+done
+
+(* ------------------------------------------------------------------------------------ *)
+
+subsection "Map"
+
+lemma MapMap: "Map f$(Map g$s) = Map (f o g)$s"
+apply (rule_tac x="s" in Seq_induct, simp_all)
+done
+
+lemma MapConc: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
+apply (rule_tac x="x" in Seq_induct, simp_all)
+done
+
+lemma MapFilter: "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)"
+apply (rule_tac x="x" in Seq_induct, simp_all)
+done
+
+lemma nilMap: "nil = (Map f$s) --> s= nil"
+apply (rule_tac x="s" in Seq_cases, simp_all)
+done
+
+
+lemma ForallMap: "Forall P (Map f$s) = Forall (P o f) s"
+apply (rule_tac x="s" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+
+
+
+(* ------------------------------------------------------------------------------------ *)
+
+subsection "Forall"
+
+
+lemma ForallPForallQ1: "Forall P ys & (! x. P x --> Q x) \
+\         --> Forall Q ys"
+apply (rule_tac x="ys" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+lemmas ForallPForallQ =
+  ForallPForallQ1 [THEN mp, OF conjI, OF _ allI, OF _ impI]
+
+lemma Forall_Conc_impl: "(Forall P x & Forall P y) --> Forall P (x @@ y)"
+apply (rule_tac x="x" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+lemma Forall_Conc [simp]:
+  "Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)"
+apply (erule Seq_Finite_ind, simp_all)
+done
+
+lemma ForallTL1: "Forall P s  --> Forall P (TL$s)"
+apply (rule_tac x="s" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+lemmas ForallTL = ForallTL1 [THEN mp]
+
+lemma ForallDropwhile1: "Forall P s  --> Forall P (Dropwhile Q$s)"
+apply (rule_tac x="s" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+lemmas ForallDropwhile = ForallDropwhile1 [THEN mp]
+
+
+(* only admissible in t, not if done in s *)
+
+lemma Forall_prefix: "! s. Forall P s --> t<<s --> Forall P t"
+apply (rule_tac x="t" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+apply (intro strip)
+apply (rule_tac x="sa" in Seq_cases)
+apply simp
+apply auto
+done
+
+lemmas Forall_prefixclosed = Forall_prefix [rule_format]
+
+lemma Forall_postfixclosed:
+  "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t"
+apply auto
+done
+
+
+lemma ForallPFilterQR1:
+  "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr"
+apply (rule_tac x="tr" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+lemmas ForallPFilterQR = ForallPFilterQR1 [THEN mp, OF conjI, OF allI]
+
+
+(* ------------------------------------------------------------------------------------- *)
+
+subsection "Forall, Filter"
+
+
+lemma ForallPFilterP: "Forall P (Filter P$x)"
+apply (simp add: Filter_def Forall_def forallPsfilterP)
+done
+
+(* holds also in other direction, then equal to forallPfilterP *)
+lemma ForallPFilterPid1: "Forall P x --> Filter P$x = x"
+apply (rule_tac x="x" in Seq_induct)
+apply (simp add: Forall_def sforall_def Filter_def)
+apply simp_all
+done
+
+lemmas ForallPFilterPid = ForallPFilterPid1 [THEN mp]
+
+
+(* holds also in other direction *)
+lemma ForallnPFilterPnil1: "!! ys . Finite ys ==>
+   Forall (%x. ~P x) ys --> Filter P$ys = nil "
+apply (erule Seq_Finite_ind, simp_all)
+done
+
+lemmas ForallnPFilterPnil = ForallnPFilterPnil1 [THEN mp]
+
+
+(* holds also in other direction *)
+lemma ForallnPFilterPUU1: "~Finite ys & Forall (%x. ~P x) ys \
+\                  --> Filter P$ys = UU "
+apply (rule_tac x="ys" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+lemmas ForallnPFilterPUU = ForallnPFilterPUU1 [THEN mp, OF conjI]
+
+
+(* inverse of ForallnPFilterPnil *)
+
+lemma FilternPnilForallP1: "!! ys . Filter P$ys = nil -->
+   (Forall (%x. ~P x) ys & Finite ys)"
+apply (rule_tac x="ys" in Seq_induct)
+(* adm *)
+apply (simp add: seq.compacts Forall_def sforall_def)
+(* base cases *)
+apply simp
+apply simp
+(* main case *)
+apply simp
+done
+
+lemmas FilternPnilForallP = FilternPnilForallP1 [THEN mp]
+
+(* inverse of ForallnPFilterPUU. proved apply 2 lemmas because of adm problems *)
+
+lemma FilterUU_nFinite_lemma1: "Finite ys ==> Filter P$ys ~= UU"
+apply (erule Seq_Finite_ind, simp_all)
+done
+
+lemma FilterUU_nFinite_lemma2: "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU"
+apply (rule_tac x="ys" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+lemma FilternPUUForallP:
+  "Filter P$ys = UU ==> (Forall (%x. ~P x) ys  & ~Finite ys)"
+apply (rule conjI)
+apply (cut_tac FilterUU_nFinite_lemma2 [THEN mp, COMP rev_contrapos])
+apply auto
+apply (blast dest!: FilterUU_nFinite_lemma1)
+done
+
+
+lemma ForallQFilterPnil:
+  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|]
+    ==> Filter P$ys = nil"
+apply (erule ForallnPFilterPnil)
+apply (erule ForallPForallQ)
+apply auto
+done
+
+lemma ForallQFilterPUU:
+ "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|]
+    ==> Filter P$ys = UU "
+apply (erule ForallnPFilterPUU)
+apply (erule ForallPForallQ)
+apply auto
+done
+
+
+
+(* ------------------------------------------------------------------------------------- *)
+
+subsection "Takewhile, Forall, Filter"
+
+
+lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P$x)"
+apply (simp add: Forall_def Takewhile_def sforallPstakewhileP)
+done
+
+
+lemma ForallPTakewhileQ [simp]:
+"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)"
+apply (rule ForallPForallQ)
+apply (rule ForallPTakewhileP)
+apply auto
+done
+
+
+lemma FilterPTakewhileQnil [simp]:
+  "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |] \
+\   ==> Filter P$(Takewhile Q$ys) = nil"
+apply (erule ForallnPFilterPnil)
+apply (rule ForallPForallQ)
+apply (rule ForallPTakewhileP)
+apply auto
+done
+
+lemma FilterPTakewhileQid [simp]:
+ "!! Q P. [| !!x. Q x ==> P x |] ==> \
+\            Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)"
+apply (rule ForallPFilterPid)
+apply (rule ForallPForallQ)
+apply (rule ForallPTakewhileP)
+apply auto
+done
+
+
+lemma Takewhile_idempotent: "Takewhile P$(Takewhile P$s) = Takewhile P$s"
+apply (rule_tac x="s" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+lemma ForallPTakewhileQnP [simp]:
+ "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s"
+apply (rule_tac x="s" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+lemma ForallPDropwhileQnP [simp]:
+ "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s"
+apply (rule_tac x="s" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+
+lemma TakewhileConc1:
+ "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)"
+apply (rule_tac x="s" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+lemmas TakewhileConc = TakewhileConc1 [THEN mp]
+
+lemma DropwhileConc1:
+ "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t"
+apply (erule Seq_Finite_ind, simp_all)
+done
+
+lemmas DropwhileConc = DropwhileConc1 [THEN mp]
+
+
+
+(* ----------------------------------------------------------------------------------- *)
+
+subsection "coinductive characterizations of Filter"
+
+
+lemma divide_Seq_lemma:
+ "HD$(Filter P$y) = Def x
+    --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) 
+             & Finite (Takewhile (%x. ~ P x)$y)  & P x"
+
+(* FIX: pay attention: is only admissible with chain-finite package to be added to
+        adm test and Finite f x admissibility *)
+apply (rule_tac x="y" in Seq_induct)
+apply (simp add: adm_subst [OF _ adm_Finite])
+apply simp
+apply simp
+apply (case_tac "P a")
+ apply simp
+ apply blast
+(* ~ P a *)
+apply simp
+done
+
+lemma divide_Seq: "(x>>xs) << Filter P$y 
+   ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y)))
+      & Finite (Takewhile (%a. ~ P a)$y)  & P x"
+apply (rule divide_Seq_lemma [THEN mp])
+apply (drule_tac f="HD" and x="x>>xs" in  monofun_cfun_arg)
+apply simp
+done
+
+
+lemma nForall_HDFilter:
+ "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"
+(* Pay attention: is only admissible with chain-finite package to be added to
+        adm test *)
+apply (rule_tac x="y" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+
+lemma divide_Seq2: "~Forall P y
+  ==> ? x. y= (Takewhile P$y @@ (x >> TL$(Dropwhile P$y))) &
+      Finite (Takewhile P$y) & (~ P x)"
+apply (drule nForall_HDFilter [THEN mp])
+apply safe
+apply (rule_tac x="x" in exI)
+apply (cut_tac P1="%x. ~ P x" in divide_Seq_lemma [THEN mp])
+apply auto
+done
+
+
+lemma divide_Seq3: "~Forall P y
+  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)"
+apply (drule divide_Seq2)
+(*Auto_tac no longer proves it*)
+apply fastsimp
+done
+
+lemmas [simp] = FilterPQ FilterConc Conc_cong
+
+
+(* ------------------------------------------------------------------------------------- *)
+
+
+subsection "take_lemma"
+
+lemma seq_take_lemma: "(!n. seq_take n$x = seq_take n$x') = (x = x')"
+apply (rule iffI)
+apply (rule seq.take_lemmas)
+apply auto
+done
+
+lemma take_reduction1:
+"  ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2)
+    --> seq_take n$(x @@ (t>>y1)) =  seq_take n$(x @@ (t>>y2)))"
+apply (rule_tac x="x" in Seq_induct)
+apply simp_all
+apply (intro strip)
+apply (case_tac "n")
+apply auto
+apply (case_tac "n")
+apply auto
+done
+
+
+lemma take_reduction:
+ "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|]
+  ==> seq_take n$(x @@ (s>>y1)) =  seq_take n$(y @@ (t>>y2))"
+apply (auto intro!: take_reduction1 [rule_format])
+done
+
+(* ------------------------------------------------------------------
+          take-lemma and take_reduction for << instead of =
+   ------------------------------------------------------------------ *)
+
+lemma take_reduction_less1:
+"  ! n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2)
+    --> seq_take n$(x @@ (t>>y1)) <<  seq_take n$(x @@ (t>>y2)))"
+apply (rule_tac x="x" in Seq_induct)
+apply simp_all
+apply (intro strip)
+apply (case_tac "n")
+apply auto
+apply (case_tac "n")
+apply auto
+done
+
+
+lemma take_reduction_less:
+ "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|]
+  ==> seq_take n$(x @@ (s>>y1)) <<  seq_take n$(y @@ (t>>y2))"
+apply (auto intro!: take_reduction_less1 [rule_format])
+done
+
+lemma take_lemma_less1:
+  assumes "!! n. seq_take n$s1 << seq_take n$s2"
+  shows "s1<<s2"
+apply (rule_tac t="s1" in seq.reach [THEN subst])
+apply (rule_tac t="s2" in seq.reach [THEN subst])
+apply (rule fix_def2 [THEN ssubst])
+apply (subst contlub_cfun_fun)
+apply (rule chain_iterate)
+apply (subst contlub_cfun_fun)
+apply (rule chain_iterate)
+apply (rule lub_mono)
+apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
+apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
+apply (rule allI)
+apply (rule prems [unfolded seq.take_def])
+done
+
+
+lemma take_lemma_less: "(!n. seq_take n$x << seq_take n$x') = (x << x')"
+apply (rule iffI)
+apply (rule take_lemma_less1)
+apply auto
+apply (erule monofun_cfun_arg)
+done
+
+(* ------------------------------------------------------------------
+          take-lemma proof principles
+   ------------------------------------------------------------------ *)
+
+lemma take_lemma_principle1:
+ "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
+            !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|]
+                          ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |]
+               ==> A x --> (f x)=(g x)"
+apply (case_tac "Forall Q x")
+apply (auto dest!: divide_Seq3)
+done
+
+lemma take_lemma_principle2:
+  "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
+           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|]
+                          ==> ! n. seq_take n$(f (s1 @@ y>>s2))
+                                 = seq_take n$(g (s1 @@ y>>s2)) |]
+               ==> A x --> (f x)=(g x)"
+apply (case_tac "Forall Q x")
+apply (auto dest!: divide_Seq3)
+apply (rule seq.take_lemmas)
+apply auto
+done
+
+
+(* Note: in the following proofs the ordering of proof steps is very
+         important, as otherwise either (Forall Q s1) would be in the IH as
+         assumption (then rule useless) or it is not possible to strengthen
+         the IH apply doing a forall closure of the sequence t (then rule also useless).
+         This is also the reason why the induction rule (nat_less_induct or nat_induct) has to
+         to be imbuilt into the rule, as induction has to be done early and the take lemma
+         has to be used in the trivial direction afterwards for the (Forall Q x) case.  *)
+
+lemma take_lemma_induct:
+"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
+         !! s1 s2 y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);
+                          Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |]
+                          ==>   seq_take (Suc n)$(f (s1 @@ y>>s2))
+                              = seq_take (Suc n)$(g (s1 @@ y>>s2)) |]
+               ==> A x --> (f x)=(g x)"
+apply (rule impI)
+apply (rule seq.take_lemmas)
+apply (rule mp)
+prefer 2 apply assumption
+apply (rule_tac x="x" in spec)
+apply (rule nat_induct)
+apply simp
+apply (rule allI)
+apply (case_tac "Forall Q xa")
+apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
+apply (auto dest!: divide_Seq3)
+done
+
+
+lemma take_lemma_less_induct:
+"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
+        !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m$(f t) = seq_take m$(g t);
+                          Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |]
+                          ==>   seq_take n$(f (s1 @@ y>>s2))
+                              = seq_take n$(g (s1 @@ y>>s2)) |]
+               ==> A x --> (f x)=(g x)"
+apply (rule impI)
+apply (rule seq.take_lemmas)
+apply (rule mp)
+prefer 2 apply assumption
+apply (rule_tac x="x" in spec)
+apply (rule nat_less_induct)
+apply (rule allI)
+apply (case_tac "Forall Q xa")
+apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
+apply (auto dest!: divide_Seq3)
+done
+
+
+
+lemma take_lemma_in_eq_out:
+"!! Q. [| A UU  ==> (f UU) = (g UU) ;
+          A nil ==> (f nil) = (g nil) ;
+          !! s y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);
+                     A (y>>s) |]
+                     ==>   seq_take (Suc n)$(f (y>>s))
+                         = seq_take (Suc n)$(g (y>>s)) |]
+               ==> A x --> (f x)=(g x)"
+apply (rule impI)
+apply (rule seq.take_lemmas)
+apply (rule mp)
+prefer 2 apply assumption
+apply (rule_tac x="x" in spec)
+apply (rule nat_induct)
+apply simp
+apply (rule allI)
+apply (rule_tac x="xa" in Seq_cases)
+apply simp_all
+done
+
+
+(* ------------------------------------------------------------------------------------ *)
+
+subsection "alternative take_lemma proofs"
+
+
+(* --------------------------------------------------------------- *)
+(*              Alternative Proof of FilterPQ                      *)
+(* --------------------------------------------------------------- *)
+
+declare FilterPQ [simp del]
+
+
+(* In general: How to do this case without the same adm problems
+   as for the entire proof ? *)
+lemma Filter_lemma1: "Forall (%x.~(P x & Q x)) s
+          --> Filter P$(Filter Q$s) =
+              Filter (%x. P x & Q x)$s"
+
+apply (rule_tac x="s" in Seq_induct)
+apply (simp add: Forall_def sforall_def)
+apply simp_all
+done
+
+lemma Filter_lemma2: "Finite s ==>
+          (Forall (%x. (~P x) | (~ Q x)) s
+          --> Filter P$(Filter Q$s) = nil)"
+apply (erule Seq_Finite_ind, simp_all)
+done
+
+lemma Filter_lemma3: "Finite s ==>
+          Forall (%x. (~P x) | (~ Q x)) s
+          --> Filter (%x. P x & Q x)$s = nil"
+apply (erule Seq_Finite_ind, simp_all)
+done
+
+
+lemma FilterPQ_takelemma: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
+apply (rule_tac A1="%x. True" and
+                 Q1="%x.~(P x & Q x)" and x1="s" in
+                 take_lemma_induct [THEN mp])
+(* better support for A = %x. True *)
+apply (simp add: Filter_lemma1)
+apply (simp add: Filter_lemma2 Filter_lemma3)
+apply simp
+done
+
+declare FilterPQ [simp]
+
+
+(* --------------------------------------------------------------- *)
+(*              Alternative Proof of MapConc                       *)
+(* --------------------------------------------------------------- *)
+
+
+
+lemma MapConc_takelemma: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
+apply (rule_tac A1="%x. True" and x1="x" in
+    take_lemma_in_eq_out [THEN mp])
+apply auto
+done
 
 ML {* use_legacy_bindings (the_context ()) *}