--- 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")
--- 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();
--- 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";
--- 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
--- 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);
--- 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 \
--- 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
--- 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"