# HG changeset patch
# User huffman
# Date 1146620835 -7200
# Node ID ae77a20f6995aa0c8ba4c1bbfb78a269e15c5ef8
# Parent  a8ed346f86355fd8a6a355990761a1300c0f6118
update to reflect changes in inverts/injects lemmas

diff -r a8ed346f8635 -r ae77a20f6995 src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Wed May 03 03:46:25 2006 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Wed May 03 03:47:15 2006 +0200
@@ -175,15 +175,14 @@
 lemma fstreams_prefix: "<a> ooo s << t ==> EX tt. t = <a> ooo tt &  s << tt"
 apply (simp add: fsingleton_def2)
 apply (insert stream_prefix [of "Def a" s t], auto)
-by (drule stream.inverts, auto)
+by (auto simp add: stream.inverts)
 
 lemma fstreams_prefix': "x << <a> ooo z = (x = <> |  (EX y. x = <a> ooo y &  y << z))"
 apply (auto, case_tac "x=UU", auto)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (simp add: fsingleton_def2, auto)
-apply (drule stream.inverts, auto)
+apply (auto simp add: stream.inverts)
 apply (drule ax_flat [rule_format], simp)
-apply (drule stream.inverts, auto)
 by (erule sconc_mono)
 
 lemma ft_fstreams[simp]: "ft$(<a> ooo s) = Def a"
@@ -201,7 +200,7 @@
 
 lemma fstreams_mono: "<a> ooo b << <a> ooo c ==> b << c"
 apply (simp add: fsingleton_def2)
-by (drule stream.inverts, auto)
+by (auto simp add: stream.inverts)
 
 lemma fsmap_UU[simp]: "fsmap f$UU = UU"
 by (simp add: fsmap_def)
@@ -223,22 +222,20 @@
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (case_tac "y=UU", auto)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (drule stream.inverts, auto)
-apply (simp add: less_lift, auto)
-apply (rule monofun_cfun, auto)
+apply (auto simp add: stream.inverts)
+apply (simp add: less_lift)
 apply (case_tac "s=UU", auto)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (erule_tac x="ya" in allE)
 apply (drule stream_prefix, auto)
 apply (case_tac "y=UU",auto)
 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
-apply (drule stream.inverts, auto)
+apply (auto simp add: stream.inverts)
 apply (simp add: less_lift)
-apply (drule stream.inverts, auto)+
 apply (erule_tac x="tt" in allE)
 apply (erule_tac x="yb" in allE, auto)
 apply (simp add: less_lift)
-by (rule monofun_cfun, auto)
+by (simp add: less_lift)
 
 lemma fstreams_lub_lemma1: "[| chain Y; lub (range Y) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
 apply (subgoal_tac "lub(range Y) ~= UU")
diff -r a8ed346f8635 -r ae77a20f6995 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed May 03 03:46:25 2006 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed May 03 03:47:15 2006 +0200
@@ -680,7 +680,7 @@
 \ --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA";
 
 by (strip_tac 1);
-by (resolve_tac seq.take_lemmas 1);
+by (resolve_tac [seq.take_lemmas] 1);
 by (rtac mp 1);
 by (assume_tac 2);
 back();back();back();back();
@@ -920,7 +920,7 @@
 \ --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB";
 
 by (strip_tac 1);
-by (resolve_tac seq.take_lemmas 1);
+by (resolve_tac [seq.take_lemmas] 1);
 by (rtac mp 1);
 by (assume_tac 2);
 back();back();back();back();
diff -r a8ed346f8635 -r ae77a20f6995 src/HOLCF/IOA/meta_theory/Seq.ML
--- a/src/HOLCF/IOA/meta_theory/Seq.ML	Wed May 03 03:46:25 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,457 +0,0 @@
-(*  Title:      HOLCF/IOA/meta_theory/Seq.ML
-    ID:         $Id$
-    Author:     Olaf Mller
-*)
-
-Addsimps (sfinite.intros @ seq.rews);
-
-
-(* Instead of adding UU_neq_nil every equation UU~=x could be changed to x~=UU *)
-(*
-Goal "UU ~=nil";
-by (res_inst_tac [("s1","UU"),("t1","nil")]  (sym RS rev_contrapos) 1);
-by (REPEAT (Simp_tac 1));
-qed"UU_neq_nil";
-
-Addsimps [UU_neq_nil];
-*)
-
-
-
-(* ------------------------------------------------------------------------------------- *)
-
-
-(* ----------------------------------------------------  *)
-       section "recursive equations of operators";
-(* ----------------------------------------------------  *)
-
-
-(* ----------------------------------------------------------- *)
-(*                        smap                                 *)
-(* ----------------------------------------------------------- *)
-
-bind_thm ("smap_unfold", fix_prover2 (the_context ()) smap_def
-   "smap = (LAM f tr. case tr of  \
- \                         nil  => nil \
- \                       | x##xs => f$x ## smap$f$xs)");
-
-Goal "smap$f$nil=nil";
-by (stac smap_unfold 1);
-by (Simp_tac 1);
-qed"smap_nil";
-
-Goal "smap$f$UU=UU";
-by (stac smap_unfold 1);
-by (Simp_tac 1);
-qed"smap_UU";
-
-Goal
-"[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs";
-by (rtac trans 1);
-by (stac smap_unfold 1);
-by (Asm_full_simp_tac 1);
-by (rtac refl 1);
-qed"smap_cons";
-
-(* ----------------------------------------------------------- *)
-(*                        sfilter                              *)
-(* ----------------------------------------------------------- *)
-
-bind_thm ("sfilter_unfold", fix_prover2 (the_context ()) sfilter_def
-  "sfilter = (LAM P tr. case tr of  \
- \         nil   => nil \
- \       | x##xs => If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)");
-
-Goal "sfilter$P$nil=nil";
-by (stac sfilter_unfold 1);
-by (Simp_tac 1);
-qed"sfilter_nil";
-
-Goal "sfilter$P$UU=UU";
-by (stac sfilter_unfold 1);
-by (Simp_tac 1);
-qed"sfilter_UU";
-
-Goal
-"x~=UU ==> sfilter$P$(x##xs)=   \
-\             (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)";
-by (rtac trans 1);
-by (stac sfilter_unfold 1);
-by (Asm_full_simp_tac 1);
-by (rtac refl 1);
-qed"sfilter_cons";
-
-(* ----------------------------------------------------------- *)
-(*                        sforall2                             *)
-(* ----------------------------------------------------------- *)
-
-bind_thm ("sforall2_unfold", fix_prover2 (the_context ()) sforall2_def
-   "sforall2 = (LAM P tr. case tr of  \
- \                         nil   => TT \
- \                       | x##xs => (P$x andalso sforall2$P$xs))");
-
-Goal "sforall2$P$nil=TT";
-by (stac sforall2_unfold 1);
-by (Simp_tac 1);
-qed"sforall2_nil";
-
-Goal "sforall2$P$UU=UU";
-by (stac sforall2_unfold 1);
-by (Simp_tac 1);
-qed"sforall2_UU";
-
-Goal
-"x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)";
-by (rtac trans 1);
-by (stac sforall2_unfold 1);
-by (Asm_full_simp_tac 1);
-by (rtac refl 1);
-qed"sforall2_cons";
-
-
-(* ----------------------------------------------------------- *)
-(*                        stakewhile                           *)
-(* ----------------------------------------------------------- *)
-
-
-bind_thm ("stakewhile_unfold", fix_prover2 (the_context ()) stakewhile_def
-   "stakewhile = (LAM P tr. case tr of  \
- \                         nil   => nil \
- \                       | x##xs => (If P$x then x##(stakewhile$P$xs) else nil fi))");
-
-Goal "stakewhile$P$nil=nil";
-by (stac stakewhile_unfold 1);
-by (Simp_tac 1);
-qed"stakewhile_nil";
-
-Goal "stakewhile$P$UU=UU";
-by (stac stakewhile_unfold 1);
-by (Simp_tac 1);
-qed"stakewhile_UU";
-
-Goal
-"x~=UU ==> stakewhile$P$(x##xs) =   \
-\             (If P$x then x##(stakewhile$P$xs) else nil fi)";
-by (rtac trans 1);
-by (stac stakewhile_unfold 1);
-by (Asm_full_simp_tac 1);
-by (rtac refl 1);
-qed"stakewhile_cons";
-
-(* ----------------------------------------------------------- *)
-(*                        sdropwhile                           *)
-(* ----------------------------------------------------------- *)
-
-
-bind_thm ("sdropwhile_unfold", fix_prover2 (the_context ()) sdropwhile_def
-   "sdropwhile = (LAM P tr. case tr of  \
- \                         nil   => nil \
- \                       | x##xs => (If P$x then sdropwhile$P$xs else tr fi))");
-
-Goal "sdropwhile$P$nil=nil";
-by (stac sdropwhile_unfold 1);
-by (Simp_tac 1);
-qed"sdropwhile_nil";
-
-Goal "sdropwhile$P$UU=UU";
-by (stac sdropwhile_unfold 1);
-by (Simp_tac 1);
-qed"sdropwhile_UU";
-
-Goal
-"x~=UU ==> sdropwhile$P$(x##xs) =   \
-\             (If P$x then sdropwhile$P$xs else x##xs fi)";
-by (rtac trans 1);
-by (stac sdropwhile_unfold 1);
-by (Asm_full_simp_tac 1);
-by (rtac refl 1);
-qed"sdropwhile_cons";
-
-
-(* ----------------------------------------------------------- *)
-(*                        slast                                 *)
-(* ----------------------------------------------------------- *)
-
-
-bind_thm ("slast_unfold", fix_prover2 (the_context ()) slast_def
-   "slast = (LAM tr. case tr of  \
- \                         nil   => UU \
- \                       | x##xs => (If is_nil$xs then x else slast$xs fi))");
-
-
-Goal "slast$nil=UU";
-by (stac slast_unfold 1);
-by (Simp_tac 1);
-qed"slast_nil";
-
-Goal "slast$UU=UU";
-by (stac slast_unfold 1);
-by (Simp_tac 1);
-qed"slast_UU";
-
-Goal
-"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)";
-by (rtac trans 1);
-by (stac slast_unfold 1);
-by (Asm_full_simp_tac 1);
-by (rtac refl 1);
-qed"slast_cons";
-
-
-(* ----------------------------------------------------------- *)
-(*                        sconc                                 *)
-(* ----------------------------------------------------------- *)
-
-bind_thm ("sconc_unfold", fix_prover2 (the_context ()) sconc_def
-   "sconc = (LAM t1 t2. case t1 of  \
- \                         nil   => t2 \
- \                       | x##xs => x ## (xs @@ t2))");
-
-
-Goal "nil @@ y = y";
-by (stac sconc_unfold 1);
-by (Simp_tac 1);
-qed"sconc_nil";
-
-Goal "UU @@ y=UU";
-by (stac sconc_unfold 1);
-by (Simp_tac 1);
-qed"sconc_UU";
-
-Goal "(x##xs) @@ y=x##(xs @@ y)";
-by (rtac trans 1);
-by (stac sconc_unfold 1);
-by (Asm_full_simp_tac 1);
-by (case_tac "x=UU" 1);
-by (REPEAT (Asm_full_simp_tac 1));
-qed"sconc_cons";
-
-Addsimps [sconc_nil,sconc_UU,sconc_cons];
-
-
-(* ----------------------------------------------------------- *)
-(*                        sflat                                 *)
-(* ----------------------------------------------------------- *)
-
-bind_thm ("sflat_unfold", fix_prover2 (the_context ()) sflat_def
-   "sflat = (LAM tr. case tr of  \
- \                         nil   => nil \
- \                       | x##xs => x @@ sflat$xs)");
-
-Goal "sflat$nil=nil";
-by (stac sflat_unfold 1);
-by (Simp_tac 1);
-qed"sflat_nil";
-
-Goal "sflat$UU=UU";
-by (stac sflat_unfold 1);
-by (Simp_tac 1);
-qed"sflat_UU";
-
-Goal "sflat$(x##xs)= x@@(sflat$xs)";
-by (rtac trans 1);
-by (stac sflat_unfold 1);
-by (Asm_full_simp_tac 1);
-by (case_tac "x=UU" 1);
-by (REPEAT (Asm_full_simp_tac 1));
-qed"sflat_cons";
-
-
-
-
-(* ----------------------------------------------------------- *)
-(*                        szip                                 *)
-(* ----------------------------------------------------------- *)
-
-bind_thm ("szip_unfold", fix_prover2 (the_context ()) szip_def
-   "szip = (LAM t1 t2. case t1 of \
-\               nil   => nil    \
-\             | x##xs => (case t2 of     \
-\                          nil => UU    \
-\                        | y##ys => <x,y>##(szip$xs$ys)))");
-
-Goal "szip$nil$y=nil";
-by (stac szip_unfold 1);
-by (Simp_tac 1);
-qed"szip_nil";
-
-Goal "szip$UU$y=UU";
-by (stac szip_unfold 1);
-by (Simp_tac 1);
-qed"szip_UU1";
-
-Goal "x~=nil ==> szip$x$UU=UU";
-by (stac szip_unfold 1);
-by (Asm_full_simp_tac 1);
-by (res_inst_tac [("x","x")] seq.casedist 1);
-by (REPEAT (Asm_full_simp_tac 1));
-qed"szip_UU2";
-
-Goal "x~=UU ==> szip$(x##xs)$nil=UU";
-by (rtac trans 1);
-by (stac szip_unfold 1);
-by (REPEAT (Asm_full_simp_tac 1));
-qed"szip_cons_nil";
-
-Goal "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys";
-by (rtac trans 1);
-by (stac szip_unfold 1);
-by (REPEAT (Asm_full_simp_tac 1));
-qed"szip_cons";
-
-
-Addsimps [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];
-
-
-
-(* ------------------------------------------------------------------------------------- *)
-
-section "scons, nil";
-
-Goal
- "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
-by (rtac iffI 1);
-by (etac (hd seq.injects) 1);
-by Auto_tac;
-qed"scons_inject_eq";
-
-Goal "nil<<x ==> nil=x";
-by (res_inst_tac [("x","x")] seq.casedist 1);
-by (hyp_subst_tac 1);
-by (etac antisym_less 1);
-by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
-qed"nil_less_is_nil";
-
-(* ------------------------------------------------------------------------------------- *)
-
-section "sfilter, sforall, sconc";
-
-
-Goal  "(if b then tr1 else tr2) @@ tr \
-        \= (if b then tr1 @@ tr else tr2 @@ tr)";
-by (res_inst_tac [("P","b"),("Q","b")] impCE 1);
-by (fast_tac HOL_cs 1);
-by (REPEAT (Asm_full_simp_tac 1));
-qed"if_and_sconc";
-
-Addsimps [if_and_sconc];
-
-
-Goal "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)";
-
-by (res_inst_tac[("x","x")] seq.ind 1);
-(* adm *)
-by (Simp_tac 1);
-(* base cases *)
-by (Simp_tac 1);
-by (Simp_tac 1);
-(* main case *)
-by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
-qed"sfiltersconc";
-
-Goal "sforall P (stakewhile$P$x)";
-by (simp_tac (simpset() addsimps [sforall_def]) 1);
-by (res_inst_tac[("x","x")] seq.ind 1);
-(* adm *)
-by (simp_tac (simpset() (*addsimps [adm_trick_1]*)) 1);
-(* base cases *)
-by (Simp_tac 1);
-by (Simp_tac 1);
-(* main case *)
-by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
-qed"sforallPstakewhileP";
-
-Goal "sforall P (sfilter$P$x)";
-by (simp_tac (simpset() addsimps [sforall_def]) 1);
-by (res_inst_tac[("x","x")] seq.ind 1);
-(* adm *)
-by (simp_tac (simpset() (*addsimps [adm_trick_1]*)) 1);
-(* base cases *)
-by (Simp_tac 1);
-by (Simp_tac 1);
-(* main case *)
-by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
-qed"forallPsfilterP";
-
-
-
-(* ------------------------------------------------------------------------------------- *)
-
-section "Finite";
-
-(* ----------------------------------------------------  *)
-(* Proofs of rewrite rules for Finite:                  *)
-(* 1. Finite(nil),   (by definition)                    *)
-(* 2. ~Finite(UU),                                      *)
-(* 3. a~=UU==> Finite(a##x)=Finite(x)                  *)
-(* ----------------------------------------------------  *)
-
-Goal "Finite x --> x~=UU";
-by (rtac impI 1);
-by (etac sfinite.induct 1);
- by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-qed"Finite_UU_a";
-
-Goal "~(Finite UU)";
-by (cut_inst_tac [("x","UU")]Finite_UU_a  1);
-by (fast_tac HOL_cs 1);
-qed"Finite_UU";
-
-Goal "Finite x --> a~=UU --> x=a##xs --> Finite xs";
-by (strip_tac 1);
-by (etac sfinite.elim 1);
-by (fast_tac (HOL_cs addss simpset()) 1);
-by (fast_tac (HOL_cs addSDs seq.injects) 1);
-qed"Finite_cons_a";
-
-Goal "a~=UU ==>(Finite (a##x)) = (Finite x)";
-by (rtac iffI 1);
-by (rtac (Finite_cons_a RS mp RS mp RS mp) 1);
-by (REPEAT (assume_tac 1));
-by (fast_tac HOL_cs 1);
-by (Asm_full_simp_tac 1);
-qed"Finite_cons";
-
-Addsimps [Finite_UU];
-
-
-(* ------------------------------------------------------------------------------------- *)
-
-section "induction";
-
-
-(*--------------------------------   *)
-(* Extensions to Induction Theorems  *)
-(*--------------------------------   *)
-
-
-qed_goalw "seq_finite_ind_lemma" (the_context ())  [seq.finite_def]
-"(!!n. P(seq_take n$s)) ==>  seq_finite(s) -->P(s)"
- (fn prems =>
-        [
-        (strip_tac 1),
-        (etac exE 1),
-        (etac subst 1),
-        (resolve_tac prems 1)
-        ]);
-
-
-Goal "!!P.[|P(UU);P(nil);\
-\  !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\
-\  |] ==> seq_finite(s) --> P(s)";
-by (rtac seq_finite_ind_lemma 1);
-by (etac seq.finite_ind 1);
- by (assume_tac 1);
-by (Asm_full_simp_tac 1);
-qed"seq_finite_ind";
diff -r a8ed346f8635 -r ae77a20f6995 src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Wed May 03 03:46:25 2006 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Wed May 03 03:47:15 2006 +0200
@@ -132,4 +132,382 @@
 end
 *}
 
+declare sfinite.intros [simp]
+declare seq.rews [simp]
+
+subsection {* recursive equations of operators *}
+
+subsubsection {* smap *}
+
+lemma smap_unfold:
+  "smap = (LAM f tr. case tr of nil  => nil | x##xs => f$x ## smap$f$xs)"
+by (subst fix_eq2 [OF smap_def], simp)
+
+lemma smap_nil [simp]: "smap$f$nil=nil"
+by (subst smap_unfold, simp)
+
+lemma smap_UU [simp]: "smap$f$UU=UU"
+by (subst smap_unfold, simp)
+
+lemma smap_cons [simp]: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"
+apply (rule trans)
+apply (subst smap_unfold)
+apply simp
+apply (rule refl)
+done
+
+subsubsection {* sfilter *}
+
+lemma sfilter_unfold:
+  "sfilter = (LAM P tr. case tr of
+           nil   => nil
+         | x##xs => If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"
+by (subst fix_eq2 [OF sfilter_def], simp)
+
+lemma sfilter_nil [simp]: "sfilter$P$nil=nil"
+by (subst sfilter_unfold, simp)
+
+lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
+by (subst sfilter_unfold, simp)
+
+lemma sfilter_cons [simp]:
+"x~=UU ==> sfilter$P$(x##xs)=
+              (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"
+apply (rule trans)
+apply (subst sfilter_unfold)
+apply simp
+apply (rule refl)
+done
+
+subsubsection {* sforall2 *}
+
+lemma sforall2_unfold:
+   "sforall2 = (LAM P tr. case tr of
+                           nil   => TT
+                         | x##xs => (P$x andalso sforall2$P$xs))"
+by (subst fix_eq2 [OF sforall2_def], simp)
+
+lemma sforall2_nil [simp]: "sforall2$P$nil=TT"
+by (subst sforall2_unfold, simp)
+
+lemma sforall2_UU [simp]: "sforall2$P$UU=UU"
+by (subst sforall2_unfold, simp)
+
+lemma sforall2_cons [simp]:
+"x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)"
+apply (rule trans)
+apply (subst sforall2_unfold)
+apply simp
+apply (rule refl)
+done
+
+
+subsubsection {* stakewhile *}
+
+lemma stakewhile_unfold:
+  "stakewhile = (LAM P tr. case tr of
+     nil   => nil
+   | x##xs => (If P$x then x##(stakewhile$P$xs) else nil fi))"
+by (subst fix_eq2 [OF stakewhile_def], simp)
+
+lemma stakewhile_nil [simp]: "stakewhile$P$nil=nil"
+apply (subst stakewhile_unfold)
+apply simp
+done
+
+lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
+apply (subst stakewhile_unfold)
+apply simp
+done
+
+lemma stakewhile_cons [simp]:
+"x~=UU ==> stakewhile$P$(x##xs) =
+              (If P$x then x##(stakewhile$P$xs) else nil fi)"
+apply (rule trans)
+apply (subst stakewhile_unfold)
+apply simp
+apply (rule refl)
+done
+
+subsubsection {* sdropwhile *}
+
+lemma sdropwhile_unfold:
+   "sdropwhile = (LAM P tr. case tr of
+                           nil   => nil
+                         | x##xs => (If P$x then sdropwhile$P$xs else tr fi))"
+by (subst fix_eq2 [OF sdropwhile_def], simp)
+
+lemma sdropwhile_nil [simp]: "sdropwhile$P$nil=nil"
+apply (subst sdropwhile_unfold)
+apply simp
+done
+
+lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
+apply (subst sdropwhile_unfold)
+apply simp
+done
+
+lemma sdropwhile_cons [simp]:
+"x~=UU ==> sdropwhile$P$(x##xs) =
+              (If P$x then sdropwhile$P$xs else x##xs fi)"
+apply (rule trans)
+apply (subst sdropwhile_unfold)
+apply simp
+apply (rule refl)
+done
+
+
+subsubsection {* slast *}
+
+lemma slast_unfold:
+   "slast = (LAM tr. case tr of
+                           nil   => UU
+                         | x##xs => (If is_nil$xs then x else slast$xs fi))"
+by (subst fix_eq2 [OF slast_def], simp)
+
+lemma slast_nil [simp]: "slast$nil=UU"
+apply (subst slast_unfold)
+apply simp
+done
+
+lemma slast_UU [simp]: "slast$UU=UU"
+apply (subst slast_unfold)
+apply simp
+done
+
+lemma slast_cons [simp]:
+"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)"
+apply (rule trans)
+apply (subst slast_unfold)
+apply simp
+apply (rule refl)
+done
+
+
+subsubsection {* sconc *}
+
+lemma sconc_unfold:
+   "sconc = (LAM t1 t2. case t1 of
+                           nil   => t2
+                         | x##xs => x ## (xs @@ t2))"
+by (subst fix_eq2 [OF sconc_def], simp)
+
+lemma sconc_nil [simp]: "nil @@ y = y"
+apply (subst sconc_unfold)
+apply simp
+done
+
+lemma sconc_UU [simp]: "UU @@ y=UU"
+apply (subst sconc_unfold)
+apply simp
+done
+
+lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)"
+apply (rule trans)
+apply (subst sconc_unfold)
+apply simp
+apply (case_tac "x=UU")
+apply simp_all
+done
+
+
+subsubsection {* sflat *}
+
+lemma sflat_unfold:
+   "sflat = (LAM tr. case tr of
+                           nil   => nil
+                         | x##xs => x @@ sflat$xs)"
+by (subst fix_eq2 [OF sflat_def], simp)
+
+lemma sflat_nil [simp]: "sflat$nil=nil"
+apply (subst sflat_unfold)
+apply simp
+done
+
+lemma sflat_UU [simp]: "sflat$UU=UU"
+apply (subst sflat_unfold)
+apply simp
+done
+
+lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)"
+apply (rule trans)
+apply (subst sflat_unfold)
+apply simp
+apply (case_tac "x=UU")
+apply simp_all
+done
+
+
+subsubsection {* szip *}
+
+lemma szip_unfold:
+   "szip = (LAM t1 t2. case t1 of
+                nil   => nil
+              | x##xs => (case t2 of
+                           nil => UU
+                         | y##ys => <x,y>##(szip$xs$ys)))"
+by (subst fix_eq2 [OF szip_def], simp)
+
+lemma szip_nil [simp]: "szip$nil$y=nil"
+apply (subst szip_unfold)
+apply simp
+done
+
+lemma szip_UU1 [simp]: "szip$UU$y=UU"
+apply (subst szip_unfold)
+apply simp
+done
+
+lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU"
+apply (subst szip_unfold)
+apply simp
+apply (rule_tac x="x" in seq.casedist)
+apply simp_all
+done
+
+lemma szip_cons_nil [simp]: "x~=UU ==> szip$(x##xs)$nil=UU"
+apply (rule trans)
+apply (subst szip_unfold)
+apply simp_all
+done
+
+lemma szip_cons [simp]:
+"[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys"
+apply (rule trans)
+apply (subst szip_unfold)
+apply simp_all
+done
+
+
+subsection "scons, nil"
+
+lemma scons_inject_eq:
+ "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)"
+by (simp add: seq.injects)
+
+lemma nil_less_is_nil: "nil<<x ==> nil=x"
+apply (rule_tac x="x" in seq.casedist)
+apply simp
+apply simp
+apply simp
+done
+
+subsection "sfilter, sforall, sconc"
+
+lemma if_and_sconc [simp]: "(if b then tr1 else tr2) @@ tr
+        = (if b then tr1 @@ tr else tr2 @@ tr)"
+by simp
+
+
+lemma sfiltersconc: "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)"
+apply (rule_tac x="x" in seq.ind)
+(* adm *)
+apply simp
+(* base cases *)
+apply simp
+apply simp
+(* main case *)
+apply (rule_tac p="P$a" in trE)
+apply simp
+apply simp
+apply simp
+done
+
+lemma sforallPstakewhileP: "sforall P (stakewhile$P$x)"
+apply (simp add: sforall_def)
+apply (rule_tac x="x" in seq.ind)
+(* adm *)
+apply simp
+(* base cases *)
+apply simp
+apply simp
+(* main case *)
+apply (rule_tac p="P$a" in trE)
+apply simp
+apply simp
+apply simp
+done
+
+lemma forallPsfilterP: "sforall P (sfilter$P$x)"
+apply (simp add: sforall_def)
+apply (rule_tac x="x" in seq.ind)
+(* adm *)
+apply simp
+(* base cases *)
+apply simp
+apply simp
+(* main case *)
+apply (rule_tac p="P$a" in trE)
+apply simp
+apply simp
+apply simp
+done
+
+
+subsection "Finite"
+
+(* ----------------------------------------------------  *)
+(* Proofs of rewrite rules for Finite:                  *)
+(* 1. Finite(nil),   (by definition)                    *)
+(* 2. ~Finite(UU),                                      *)
+(* 3. a~=UU==> Finite(a##x)=Finite(x)                  *)
+(* ----------------------------------------------------  *)
+
+lemma Finite_UU_a: "Finite x --> x~=UU"
+apply (rule impI)
+apply (erule sfinite.induct)
+ apply simp
+apply simp
+done
+
+lemma Finite_UU [simp]: "~(Finite UU)"
+apply (cut_tac x="UU" in Finite_UU_a)
+apply fast
+done
+
+lemma Finite_cons_a: "Finite x --> a~=UU --> x=a##xs --> Finite xs"
+apply (intro strip)
+apply (erule sfinite.elims)
+apply fastsimp
+apply (simp add: seq.injects)
+done
+
+lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)"
+apply (rule iffI)
+apply (erule (1) Finite_cons_a [rule_format])
+apply fast
+apply simp
+done
+
+
+subsection "induction"
+
+
+(*--------------------------------   *)
+(* Extensions to Induction Theorems  *)
+(*--------------------------------   *)
+
+
+lemma seq_finite_ind_lemma:
+  assumes "(!!n. P(seq_take n$s))"
+  shows "seq_finite(s) -->P(s)"
+apply (unfold seq.finite_def)
+apply (intro strip)
+apply (erule exE)
+apply (erule subst)
+apply (rule prems)
+done
+
+
+lemma seq_finite_ind: "!!P.[|P(UU);P(nil);
+   !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)
+   |] ==> seq_finite(s) --> P(s)"
+apply (rule seq_finite_ind_lemma)
+apply (erule seq.finite_ind)
+ apply assumption
+apply simp
+done
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
diff -r a8ed346f8635 -r ae77a20f6995 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed May 03 03:46:25 2006 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed May 03 03:47:15 2006 +0200
@@ -281,16 +281,15 @@
 
 Goal "(a>>s<<b>>t) = (a = b & s<<t)";
 by (simp_tac (simpset() addsimps [Consq_def2]) 1);
-by (stac (Def_inject_less_eq RS sym) 1);
+by (simp_tac (simpset() addsimps [seq.inverts]) 1);
+(*by (stac (Def_inject_less_eq RS sym) 1);
 back();
 by (rtac iffI 1);
-(* 1 *)
 by (etac (hd seq.inverts) 1);
 by (REPEAT(rtac Def_not_UU 1));
-(* 2 *)
 by (Asm_full_simp_tac 1);
 by (etac conjE 1);
-by (etac monofun_cfun_arg 1);
+by (etac monofun_cfun_arg 1);*)
 qed"Cons_inject_less_eq";
 
 Goal "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)";
@@ -844,7 +843,7 @@
 
 Goal "(!n. seq_take n$x = seq_take n$x') = (x = x')";
 by (rtac iffI 1);
-by (resolve_tac seq.take_lemmas 1);
+by (resolve_tac [seq.take_lemmas] 1);
 by Auto_tac;
 qed"seq_take_lemma";
 
@@ -932,7 +931,7 @@
 \              ==> 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 (resolve_tac [seq.take_lemmas] 1);
 by Auto_tac;
 qed"take_lemma_principle2";
 
@@ -953,7 +952,7 @@
 \                             = 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 (resolve_tac [seq.take_lemmas] 1);
 by (rtac mp 1);
 by (assume_tac 2);
 by (res_inst_tac [("x","x")] spec 1);
@@ -975,7 +974,7 @@
 \                             = 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 (resolve_tac [seq.take_lemmas] 1);
 by (rtac mp 1);
 by (assume_tac 2);
 by (res_inst_tac [("x","x")] spec 1);
@@ -998,7 +997,7 @@
 \                        = 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 (resolve_tac [seq.take_lemmas] 1);
 by (rtac mp 1);
 by (assume_tac 2);
 by (res_inst_tac [("x","x")] spec 1);
diff -r a8ed346f8635 -r ae77a20f6995 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Wed May 03 03:46:25 2006 +0200
+++ b/src/HOLCF/IsaMakefile	Wed May 03 03:47:15 2006 +0200
@@ -82,7 +82,7 @@
   IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \
   IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \
   IOA/meta_theory/Automata.thy IOA/meta_theory/Traces.ML \
-  IOA/meta_theory/Seq.ML IOA/meta_theory/RefMappings.ML \
+  IOA/meta_theory/RefMappings.ML \
   IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/ShortExecutions.ML \
   IOA/meta_theory/IOA.thy \
   IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \
diff -r a8ed346f8635 -r ae77a20f6995 src/HOLCF/ex/Dnat.thy
--- a/src/HOLCF/ex/Dnat.thy	Wed May 03 03:46:25 2006 +0200
+++ b/src/HOLCF/ex/Dnat.thy	Wed May 03 03:47:15 2006 +0200
@@ -53,23 +53,17 @@
     apply fast
    apply (rule allI)
    apply (rule_tac x = y in dnat.casedist)
-     apply (fast intro!: UU_I)
+     apply simp
     apply simp
    apply (simp add: dnat.dist_les)
   apply (rule allI)
   apply (rule_tac x = y in dnat.casedist)
     apply (fast intro!: UU_I)
+   apply (thin_tac "ALL y. d << y --> d = UU | d = y")
    apply (simp add: dnat.dist_les)
-  apply (simp (no_asm_simp) add: dnat.rews)
-  apply (intro strip)
-  apply (subgoal_tac "d << da")
-   apply (erule allE)
-   apply (drule mp)
-    apply assumption
-   apply (erule disjE)
-    apply (tactic "contr_tac 1")
-   apply simp
-  apply (erule (1) dnat.inverts)
+  apply (simp (no_asm_simp) add: dnat.rews dnat.injects dnat.inverts)
+  apply (drule_tac x="da" in spec)
+  apply simp
   done
 
 end
diff -r a8ed346f8635 -r ae77a20f6995 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Wed May 03 03:46:25 2006 +0200
+++ b/src/HOLCF/ex/Stream.thy	Wed May 03 03:47:15 2006 +0200
@@ -81,15 +81,15 @@
 lemma stream_prefix:
   "[| a && s << t; a ~= UU  |] ==> EX b tt. t = b && tt &  b ~= UU &  s << tt"
 apply (insert stream.exhaust [of t], auto)
-by (drule stream.inverts, auto)
+by (auto simp add: stream.inverts)
 
 lemma stream_prefix':
   "b ~= UU ==> x << b && z =
    (x = UU |  (EX a y. x = a && y &  a ~= UU &  a << b &  y << z))"
 apply (case_tac "x=UU",auto)
 apply (drule stream_exhaust_eq [THEN iffD1],auto)
-apply (drule stream.inverts,auto)
-by (intro monofun_cfun,auto)
+by (auto simp add: stream.inverts)
+
 
 (*
 lemma stream_prefix1: "[| x<<y; xs<<ys |] ==> x&&xs << y&&ys"
@@ -99,9 +99,9 @@
 lemma stream_flat_prefix:
   "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
 apply (case_tac "y=UU",auto)
-apply (drule stream.inverts,auto)
-apply (drule ax_flat [rule_format],simp)
-by (drule stream.inverts,auto)
+apply (auto simp add: stream.inverts)
+by (drule ax_flat [rule_format],simp)
+
 
 
 
@@ -324,7 +324,7 @@
 apply (erule stream_finite_ind [of s], auto)
 apply (case_tac "t=UU", auto)
 apply (drule stream_exhaust_eq [THEN iffD1],auto)
-apply (drule stream.inverts, auto)
+apply (auto simp add: stream.inverts)
 apply (erule_tac x="y" in allE, simp)
 by (rule stream_finite_lemma1, simp)
 
@@ -456,7 +456,7 @@
 apply (case_tac "t=UU", auto)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (erule_tac x="y" in allE, auto)
-by (drule stream.inverts, auto)
+by (auto simp add: stream.inverts)
 
 lemma slen_mono: "s << t ==> #s <= #t"
 apply (case_tac "stream_finite t")
@@ -486,7 +486,7 @@
 apply (case_tac "y=UU", clarsimp)
 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
 apply (erule_tac x="ya" in allE, simp)
-apply (drule stream.inverts,auto)
+apply (auto simp add: stream.inverts)
 by (drule ax_flat [rule_format], simp)
 
 lemma slen_strict_mono_lemma:
@@ -494,7 +494,7 @@
 apply (erule stream_finite_ind, auto)
 apply (case_tac "sa=UU", auto)
 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
-apply (drule stream.inverts, simp, simp, clarsimp)
+apply (simp add: stream.inverts, clarsimp)
 by (drule ax_flat [rule_format], simp)
 
 lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"