--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/Buffer.ML Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,268 @@
+(* Title: HOLCF/FOCUS/Buffer.ML
+ ID: $ $
+ Author: David von Oheimb, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+val set_cong = prove_goal Set.thy "!!X. A = B ==> (x:A) = (x:B)" (K [
+ etac subst 1, rtac refl 1]);
+
+fun B_prover s tac eqs = prove_goal thy s (fn prems => [cut_facts_tac prems 1,
+ tac 1, auto_tac (claset(), simpset() addsimps eqs)]);
+
+fun prove_forw s thm = B_prover s (dtac (thm RS iffD1)) [];
+fun prove_backw s thm eqs = B_prover s (rtac (thm RS iffD2)) eqs;
+
+
+(**** BufEq *******************************************************************)
+
+val mono_BufEq_F = prove_goalw thy [mono_def, BufEq_F_def]
+ "mono BufEq_F" (K [Fast_tac 1]);
+
+val BufEq_fix = mono_BufEq_F RS (BufEq_def RS def_gfp_unfold);
+
+val BufEq_unfold = prove_goal thy "f:BufEq = (!d. f\\<cdot>(Md d\\<leadsto><>) = <> & \
+ \(!x. ? ff:BufEq. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>(ff\\<cdot>x)))" (K [
+ stac (BufEq_fix RS set_cong) 1,
+ rewtac BufEq_F_def,
+ Asm_full_simp_tac 1]);
+
+val Buf_f_empty = prove_forw "f:BufEq \\<Longrightarrow> f\\<cdot><> = <>" BufEq_unfold;
+val Buf_f_d = prove_forw "f:BufEq \\<Longrightarrow> f\\<cdot>(Md d\\<leadsto><>) = <>" BufEq_unfold;
+val Buf_f_d_req = prove_forw
+ "f:BufEq \\<Longrightarrow> \\<exists>ff. ff:BufEq \\<and> f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x" BufEq_unfold;
+
+
+(**** BufAC_Asm ***************************************************************)
+
+val mono_BufAC_Asm_F = prove_goalw thy [mono_def, BufAC_Asm_F_def]
+ "mono BufAC_Asm_F" (K [Fast_tac 1]);
+
+val BufAC_Asm_fix = mono_BufAC_Asm_F RS (BufAC_Asm_def RS def_gfp_unfold);
+
+val BufAC_Asm_unfold = prove_goal thy "s:BufAC_Asm = (s = <> | (? d x. \
+\ s = Md d\\<leadsto>x & (x = <> | (ft\\<cdot>x = Def \\<bullet> & (rt\\<cdot>x):BufAC_Asm))))" (K [
+ stac (BufAC_Asm_fix RS set_cong) 1,
+ rewtac BufAC_Asm_F_def,
+ Asm_full_simp_tac 1]);
+
+val BufAC_Asm_empty = prove_backw "<> :BufAC_Asm" BufAC_Asm_unfold [];
+val BufAC_Asm_d = prove_backw "Md d\\<leadsto><>:BufAC_Asm" BufAC_Asm_unfold [];
+val BufAC_Asm_d_req = prove_backw "x:BufAC_Asm ==> Md d\\<leadsto>\\<bullet>\\<leadsto>x:BufAC_Asm"
+ BufAC_Asm_unfold [];
+val BufAC_Asm_prefix2 = prove_forw "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> s:BufAC_Asm"
+ BufAC_Asm_unfold;
+
+
+(**** BBufAC_Cmt **************************************************************)
+
+val mono_BufAC_Cmt_F = prove_goalw thy [mono_def, BufAC_Cmt_F_def]
+ "mono BufAC_Cmt_F" (K [Fast_tac 1]);
+
+val BufAC_Cmt_fix = mono_BufAC_Cmt_F RS (BufAC_Cmt_def RS def_gfp_unfold);
+
+val BufAC_Cmt_unfold = prove_goal thy "(s,t):BufAC_Cmt = (!d x. \
+ \(s = <> --> t = <>) & \
+ \(s = Md d\\<leadsto><> --> t = <>) & \
+ \(s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x, rt\\<cdot>t):BufAC_Cmt))" (K [
+ stac (BufAC_Cmt_fix RS set_cong) 1,
+ rewtac BufAC_Cmt_F_def,
+ Asm_full_simp_tac 1]);
+
+val BufAC_Cmt_empty = prove_backw "f:BufEq ==> (<>, f\\<cdot><>):BufAC_Cmt"
+ BufAC_Cmt_unfold [Buf_f_empty];
+
+val BufAC_Cmt_d = prove_backw "f:BufEq ==> (a\\<leadsto>\\<bottom>, f\\<cdot>(a\\<leadsto>\\<bottom>)):BufAC_Cmt"
+ BufAC_Cmt_unfold [Buf_f_d];
+
+val BufAC_Cmt_d2 = prove_forw
+ "(Md d\\<leadsto>\\<bottom>, f\\<cdot>(Md d\\<leadsto>\\<bottom>)):BufAC_Cmt ==> f\\<cdot>(Md d\\<leadsto>\\<bottom>) = \\<bottom>" BufAC_Cmt_unfold;
+val BufAC_Cmt_d3 = prove_forw
+"(Md d\\<leadsto>\\<bullet>\\<leadsto>x, f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)):BufAC_Cmt ==> (x, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x))):BufAC_Cmt"
+ BufAC_Cmt_unfold;
+
+val BufAC_Cmt_d32 = prove_forw
+"(Md d\\<leadsto>\\<bullet>\\<leadsto>x, f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)):BufAC_Cmt ==> ft\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)) = Def d"
+ BufAC_Cmt_unfold;
+
+(**** BufAC *******************************************************************)
+
+Goalw [BufAC_def] "f \\<in> BufAC \\<Longrightarrow> f\\<cdot>(Md d\\<leadsto>\\<bottom>) = \\<bottom>";
+by (fast_tac (claset() addIs [BufAC_Cmt_d2, BufAC_Asm_d]) 1);
+qed "BufAC_f_d";
+
+Goal "(? ff:B. (!x. f\\<cdot>(a\\<leadsto>b\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x)) = \
+ \((!x. ft\\<cdot>(f\\<cdot>(a\\<leadsto>b\\<leadsto>x)) = Def d) & (LAM x. rt\\<cdot>(f\\<cdot>(a\\<leadsto>b\\<leadsto>x))):B)";
+(* this is an instance (though unification cannot handle this) of
+Goal "(? ff:B. (!x. f\\<cdot>x = d\\<leadsto>ff\\<cdot>x)) = \
+ \((!x. ft\\<cdot>(f\\<cdot>x) = Def d) & (LAM x. rt\\<cdot>(f\\<cdot>x)):B)";*)
+by Safe_tac;
+by ( res_inst_tac [("P","(%x. x:B)")] ssubst 2);
+by ( atac 3);
+by ( rtac ext_cfun 2);
+by ( dtac spec 2);
+by ( dres_inst_tac [("f","rt")] cfun_arg_cong 2);
+by ( Asm_full_simp_tac 2);
+by ( Full_simp_tac 2);
+by (rtac bexI 2);
+by Auto_tac;
+by (dtac spec 1);
+by (etac exE 1);;
+by (etac ssubst 1);
+by (Simp_tac 1);
+qed "ex_elim_lemma";
+
+Goalw [BufAC_def] "f\\<in>BufAC \\<Longrightarrow> \\<exists>ff\\<in>BufAC. \\<forall>x. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x";
+by (rtac (ex_elim_lemma RS iffD2) 1);
+by Safe_tac;
+by (fast_tac (claset() addIs [BufAC_Cmt_d32 RS Def_maximal,
+ monofun_cfun_arg, BufAC_Asm_empty RS BufAC_Asm_d_req]) 1);
+by (auto_tac (claset() addIs [BufAC_Cmt_d3, BufAC_Asm_d_req],simpset()));
+qed "BufAC_f_d_req";
+
+
+(**** BufSt *******************************************************************)
+
+val mono_BufSt_F = prove_goalw thy [mono_def, BufSt_F_def]
+ "mono BufSt_F" (K [Fast_tac 1]);
+
+val BufSt_P_fix = mono_BufSt_F RS (BufSt_P_def RS def_gfp_unfold);
+
+val BufSt_P_unfold = prove_goal thy "h:BufSt_P = (!s. h s\\<cdot><> = <> & \
+ \ (!d x. h \\<currency> \\<cdot>(Md d\\<leadsto>x) = h (Sd d)\\<cdot>x & \
+ \ (? hh:BufSt_P. h (Sd d)\\<cdot>(\\<bullet>\\<leadsto>x) = d\\<leadsto>(hh \\<currency> \\<cdot>x))))" (K [
+ stac (BufSt_P_fix RS set_cong) 1,
+ rewtac BufSt_F_def,
+ Asm_full_simp_tac 1]);
+
+val BufSt_P_empty = prove_forw "h:BufSt_P ==> h s \\<cdot> <> = <>"
+ BufSt_P_unfold;
+val BufSt_P_d = prove_forw "h:BufSt_P ==> h \\<currency> \\<cdot>(Md d\\<leadsto>x) = h (Sd d)\\<cdot>x"
+ BufSt_P_unfold;
+val BufSt_P_d_req = prove_forw "h:BufSt_P ==> \\<exists>hh\\<in>BufSt_P. \
+ \ h (Sd d)\\<cdot>(\\<bullet> \\<leadsto>x) = d\\<leadsto>(hh \\<currency> \\<cdot>x)"
+ BufSt_P_unfold;
+
+
+(**** Buf_AC_imp_Eq ***********************************************************)
+
+Goalw [BufEq_def] "BufAC \\<subseteq> BufEq";
+by (rtac gfp_upperbound 1);
+by (rewtac BufEq_F_def);
+by Safe_tac;
+by (etac BufAC_f_d 1);
+by (dtac BufAC_f_d_req 1);
+by (Fast_tac 1);
+qed "Buf_AC_imp_Eq";
+
+
+(**** Buf_Eq_imp_AC by coinduction ********************************************)
+
+Goal "\\<forall>s f ff. f\\<in>BufEq \\<longrightarrow> ff\\<in>BufEq \\<longrightarrow> \
+\ s\\<in>BufAC_Asm \\<longrightarrow> stream_take n\\<cdot>(f\\<cdot>s) = stream_take n\\<cdot>(ff\\<cdot>s)";
+by (nat_ind_tac "n" 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (dtac (BufAC_Asm_unfold RS iffD1) 1);
+by Safe_tac;
+by (asm_simp_tac (simpset() addsimps [Buf_f_empty]) 1);
+by (asm_simp_tac (simpset() addsimps [Buf_f_d]) 1);
+by (dtac (ft_eq RS iffD1) 1);
+by (Clarsimp_tac 1);
+by (REPEAT(dtac Buf_f_d_req 1));
+by Safe_tac;
+by (REPEAT(etac ssubst 1));
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "BufAC_Asm_cong_lemma";
+Goal "\\<lbrakk>f \\<in> BufEq; ff \\<in> BufEq; s \\<in> BufAC_Asm\\<rbrakk> \\<Longrightarrow> f\\<cdot>s = ff\\<cdot>s";
+by (resolve_tac stream.take_lemmas 1);
+by (eatac BufAC_Asm_cong_lemma 2 1);
+qed "BufAC_Asm_cong";
+
+Goalw [BufAC_Cmt_def] "\\<lbrakk>f \\<in> BufEq; x \\<in> BufAC_Asm\\<rbrakk> \\<Longrightarrow> (x, f\\<cdot>x) \\<in> BufAC_Cmt";
+by (rotate_tac ~1 1);
+by (etac weak_coinduct_image 1);
+by (rewtac BufAC_Cmt_F_def);
+by Safe_tac;
+by (etac Buf_f_empty 1);
+by (etac Buf_f_d 1);
+by (dtac Buf_f_d_req 1);
+by (Clarsimp_tac 1);
+by (etac exI 1);
+by (dtac BufAC_Asm_prefix2 1);
+by (ftac Buf_f_d_req 1);
+by (Clarsimp_tac 1);
+by (etac ssubst 1);
+by (Simp_tac 1);
+by (datac BufAC_Asm_cong 2 1);
+by (etac subst 1);
+by (etac imageI 1);
+qed "Buf_Eq_imp_AC_lemma";
+Goalw [BufAC_def] "BufEq \\<subseteq> BufAC";
+by (Clarify_tac 1);
+by (eatac Buf_Eq_imp_AC_lemma 1 1);
+qed "Buf_Eq_imp_AC";
+
+(**** Buf_Eq_eq_AC ************************************************************)
+
+val Buf_Eq_eq_AC = Buf_AC_imp_Eq RS (Buf_Eq_imp_AC RS subset_antisym);
+
+
+(**** alternative (not strictly) stronger version of Buf_Eq *******************)
+
+val Buf_Eq_alt_imp_Eq = prove_goalw thy [BufEq_def,BufEq_alt_def]
+ "BufEq_alt \\<subseteq> BufEq" (K [
+ rtac gfp_mono 1,
+ rewtac BufEq_F_def,
+ Fast_tac 1]);
+
+(* direct proof of "BufEq \\<subseteq> BufEq_alt" seems impossible *)
+
+
+Goalw [BufEq_alt_def] "BufAC <= BufEq_alt";
+by (rtac gfp_upperbound 1);
+by (fast_tac (claset() addEs [BufAC_f_d, BufAC_f_d_req]) 1);
+qed "Buf_AC_imp_Eq_alt";
+
+bind_thm ("Buf_Eq_imp_Eq_alt",
+ subset_trans OF [Buf_Eq_imp_AC, Buf_AC_imp_Eq_alt]);
+
+bind_thm ("Buf_Eq_alt_eq",
+ subset_antisym OF [Buf_Eq_alt_imp_Eq, Buf_Eq_imp_Eq_alt]);
+
+
+(**** Buf_Eq_eq_St ************************************************************)
+
+Goalw [BufSt_def, BufEq_def] "BufSt <= BufEq";
+by (rtac gfp_upperbound 1);
+by (rewtac BufEq_F_def);
+by Safe_tac;
+by ( asm_simp_tac (simpset() addsimps [BufSt_P_d, BufSt_P_empty]) 1);
+by (asm_simp_tac (simpset() addsimps [BufSt_P_d]) 1);
+by (dtac BufSt_P_d_req 1);
+by (Force_tac 1);
+qed "Buf_St_imp_Eq";
+
+Goalw [BufSt_def, BufSt_P_def] "BufEq <= BufSt";
+by Safe_tac;
+by (EVERY'[rename_tac "f", res_inst_tac
+ [("x","\\<lambda>s. case s of Sd d => \\<Lambda>x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1);
+by ( Simp_tac 1);
+by (etac weak_coinduct_image 1);
+by (rewtac BufSt_F_def);
+by (Simp_tac 1);
+by Safe_tac;
+by ( EVERY'[rename_tac "s", induct_tac "s"] 1);
+by ( asm_simp_tac (simpset() addsimps [Buf_f_d]) 1);
+by ( asm_simp_tac (simpset() addsimps [Buf_f_empty]) 1);
+by ( Simp_tac 1);
+by (Simp_tac 1);
+by (EVERY'[rename_tac"f d x",dres_inst_tac[("d","d"),("x","x")] Buf_f_d_req] 1);
+by Auto_tac;
+qed "Buf_Eq_imp_St";
+
+bind_thm ("Buf_Eq_eq_St", Buf_St_imp_Eq RS (Buf_Eq_imp_St RS subset_antisym));
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/Buffer.thy Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,82 @@
+(* Title: HOLCF/FOCUS/Buffer.thy
+ ID: $ $
+ Author: David von Oheimb, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+Formalization of section 4 of
+
+@inproceedings{Broy95-SRBLO,
+ author = {Manfred Broy},
+ title = {Specification and ReFinement of a Buffer of Length One},
+ booktitle = {Working Material of Marktoberdorf Summer School},
+ year = {1994},
+ publisher = {},
+ editor = {},
+ note = {\url{http://www4.in.tum.de/papers/broy_mod94.html}}
+}
+
+Slides available from http://isabelle.in.tum.de/HOLCF/1-Buffer.ps.gz
+*)
+
+Buffer = FOCUS +
+
+types D
+arities D::term
+
+datatype
+
+ M = Md D | Mreq ("\\<bullet>")
+
+datatype
+
+ State = Sd D | Snil ("\\<currency>")
+
+types
+
+ SPF11 = "M fstream \\<rightarrow> D fstream"
+ SPEC11 = "SPF11 set"
+ SPSF11 = "State \\<Rightarrow> SPF11"
+ SPECS11 = "SPSF11 set"
+
+consts
+
+ BufEq_F :: "SPEC11 \\<Rightarrow> SPEC11"
+ BufEq :: "SPEC11"
+ BufEq_alt :: "SPEC11"
+
+ BufAC_Asm_F :: " (M fstream set) \\<Rightarrow> (M fstream set)"
+ BufAC_Asm :: " (M fstream set)"
+ BufAC_Cmt_F :: "((M fstream * D fstream) set) \\<Rightarrow> \
+\ ((M fstream * D fstream) set)"
+ BufAC_Cmt :: "((M fstream * D fstream) set)"
+ BufAC :: "SPEC11"
+
+ BufSt_F :: "SPECS11 \\<Rightarrow> SPECS11"
+ BufSt_P :: "SPECS11"
+ BufSt :: "SPEC11"
+
+defs
+
+ BufEq_F_def "BufEq_F B \\<equiv> {f. \\<forall>d. f\\<cdot>(Md d\\<leadsto><>) = <> \\<and>
+ (\\<forall>x. \\<exists>ff\\<in>B. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x)}"
+ BufEq_def "BufEq \\<equiv> gfp BufEq_F"
+ BufEq_alt_def "BufEq_alt \\<equiv> gfp (\\<lambda>B. {f. \\<forall>d. f\\<cdot>(Md d\\<leadsto><> ) = <> \\<and>
+ (\\<exists>ff\\<in>B. (\\<forall>x. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x))})"
+ BufAC_Asm_F_def "BufAC_Asm_F A \\<equiv> {s. s = <> \\<or>
+ (\\<exists>d x. s = Md d\\<leadsto>x \\<and> (x = <> \\<or> (ft\\<cdot>x = Def \\<bullet> \\<and> (rt\\<cdot>x)\\<in>A)))}"
+ BufAC_Asm_def "BufAC_Asm \\<equiv> gfp BufAC_Asm_F"
+
+ BufAC_Cmt_F_def "BufAC_Cmt_F C \\<equiv> {(s,t). \\<forall>d x.
+ (s = <> \\<longrightarrow> t = <> ) \\<and>
+ (s = Md d\\<leadsto><> \\<longrightarrow> t = <> ) \\<and>
+ (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x \\<longrightarrow> (ft\\<cdot>t = Def d \\<and> (x,rt\\<cdot>t)\\<in>C))}"
+ BufAC_Cmt_def "BufAC_Cmt \\<equiv> gfp BufAC_Cmt_F"
+ BufAC_def "BufAC \\<equiv> {f. \\<forall>x. x\\<in>BufAC_Asm \\<longrightarrow> (x,f\\<cdot>x)\\<in>BufAC_Cmt}"
+
+ BufSt_F_def "BufSt_F H \\<equiv> {h. \\<forall>s . h s \\<cdot><> = <> \\<and>
+ (\\<forall>d x. h \\<currency> \\<cdot>(Md d\\<leadsto>x) = h (Sd d)\\<cdot>x \\<and>
+ (\\<exists>hh\\<in>H. h (Sd d)\\<cdot>(\\<bullet> \\<leadsto>x) = d\\<leadsto>(hh \\<currency>\\<cdot>x)))}"
+ BufSt_P_def "BufSt_P \\<equiv> gfp BufSt_F"
+ BufSt_def "BufSt \\<equiv> {f. \\<exists>h\\<in>BufSt_P. f = h \\<currency>}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,278 @@
+(* Title: HOLCF/FOCUS/Buffer_adm.ML
+ ID: $ $
+ Author: David von Oheimb, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+infixr 0 y;
+fun _ y t = by t;
+val b=9999;
+
+Addsimps [Fin_0];
+
+val BufAC_Asm_d2 = prove_forw "a\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d" BufAC_Asm_unfold;
+val BufAC_Asm_d3 = prove_forw
+ "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\\<bullet> & s:BufAC_Asm" BufAC_Asm_unfold;
+
+val BufAC_Asm_F_def3 = prove_goalw thy [BufAC_Asm_F_def]
+ "s:BufAC_Asm_F A = (s=<> | \
+\ (? d. ft\\<cdot>s=Def(Md d)) & (rt\\<cdot>s=<> | ft\\<cdot>(rt\\<cdot>s)=Def \\<bullet> & rt\\<cdot>(rt\\<cdot>s):A))" (K [
+ Auto_tac]);
+
+Goal "down_cont BufAC_Asm_F";
+by (auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Asm_F_def3]));
+qed "cont_BufAC_Asm_F";
+
+val BufAC_Cmt_F_def3 = prove_goalw thy [BufAC_Cmt_F_def]
+ "(s,t):BufAC_Cmt_F C = (!d x.\
+\ (s = <> --> t = <> ) & \
+\ (s = Md d\\<leadsto><> --> t = <> ) & \
+\ (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C))" (fn _=> [
+ subgoal_tac "!d x. (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> (? y. t = d\\<leadsto>y & (x,y):C)) = \
+ \ (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C)" 1,
+ Asm_simp_tac 1,
+ auto_tac (claset() addIs [surjectiv_scons RS sym], simpset())]);
+
+val cont_BufAC_Cmt_F = prove_goal thy "down_cont BufAC_Cmt_F" (K [
+ auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Cmt_F_def3])]);
+
+
+(**** adm_BufAC_Asm ***********************************************************)
+
+Goalw [BufAC_Asm_F_def, stream_monoP_def] "stream_monoP BufAC_Asm_F";
+by (res_inst_tac [("x","{x. (? d. x = Md d\\<leadsto>\\<bullet>\\<leadsto><>)}")] exI 1);
+by (res_inst_tac [("x","2")] exI 1);
+by (Clarsimp_tac 1);
+qed "BufAC_Asm_F_stream_monoP";
+
+val adm_BufAC_Asm = prove_goalw thy [BufAC_Asm_def] "adm (%x. x:BufAC_Asm)" (K [
+rtac (cont_BufAC_Asm_F RS (BufAC_Asm_F_stream_monoP RS fstream_gfp_admI))1]);
+
+
+(**** adm_non_BufAC_Asm *******************************************************)
+
+Goalw [stream_antiP_def, BufAC_Asm_F_def] "stream_antiP BufAC_Asm_F";
+b y strip_tac 1;
+b y res_inst_tac [("x","{x. (? d. x = Md d\\<leadsto>\\<bullet>\\<leadsto><>)}")] exI 1;
+b y res_inst_tac [("x","2")] exI 1;
+b y rtac conjI 1;
+b y strip_tac 2;
+b y dtac slen_mono 2;
+b y datac ile_trans 1 2;
+b y ALLGOALS Force_tac;
+qed "BufAC_Asm_F_stream_antiP";
+
+Goalw [BufAC_Asm_def] "adm (%u. u~:BufAC_Asm)";
+by (rtac (cont_BufAC_Asm_F RS (BufAC_Asm_F_stream_antiP RS fstream_non_gfp_admI)) 1);
+qed "adm_non_BufAC_Asm";
+
+(**** adm_BufAC ***************************************************************)
+
+(*adm_non_BufAC_Asm*)
+Goal "!f ff. f:BufEq --> ff:BufEq --> s:BufAC_Asm --> f\\<cdot>s = ff\\<cdot>s";
+by (rtac fstream_ind2 1);
+by (simp_tac (simpset() addsimps [adm_non_BufAC_Asm]) 1);
+by (force_tac (claset() addDs [Buf_f_empty], simpset()) 1);
+by (force_tac (claset() addSDs [BufAC_Asm_d2]
+ addDs [Buf_f_d] addEs [ssubst], simpset()) 1);
+by (safe_tac (claset() addSDs [BufAC_Asm_d3]));
+by (REPEAT(dtac Buf_f_d_req 1));
+by (fast_tac (claset() addEs [ssubst]) 1);
+qed_spec_mp "BufAC_Asm_cong";
+
+(*adm_non_BufAC_Asm,BufAC_Asm_cong*)
+val BufAC_Cmt_d_req = prove_goal thy
+"!!X. [|f:BufEq; s:BufAC_Asm; (s, f\\<cdot>s):BufAC_Cmt|] ==> (a\\<leadsto>b\\<leadsto>s, f\\<cdot>(a\\<leadsto>b\\<leadsto>s)):BufAC_Cmt"
+ (K [
+ rtac (BufAC_Cmt_unfold RS iffD2) 1,
+ strip_tac 1,
+ forward_tac [Buf_f_d_req] 1,
+ auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
+
+(*adm_BufAC_Asm*)
+Goal "antitonP BufAC_Asm";
+b y rtac antitonPI 1;
+b y rtac allI 1;
+b y rtac fstream_ind2 1;
+b y REPEAT(resolve_tac adm_lemmas 1);
+b y rtac cont_id 1;
+b y rtac adm_BufAC_Asm 1;
+b y safe_tac HOL_cs;
+b y rtac BufAC_Asm_empty 1;
+b y force_tac (claset() addSDs [fstream_prefix]
+ addDs [BufAC_Asm_d2] addIs [BufAC_Asm_d],simpset()) 1;
+b y force_tac (claset() addSDs [fstream_prefix]
+ addDs [] addIs []
+ addDs [BufAC_Asm_d3] addSIs [BufAC_Asm_d_req],simpset()) 1;
+qed "BufAC_Asm_antiton";
+
+(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
+Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
+ \ (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
+ \ (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
+by (res_inst_tac [("x","%i. i+i")] exI 1);
+by (rtac allI 1);
+by (nat_ind_tac "i" 1);
+by ( Simp_tac 1);
+by (simp_tac (simpset() addsimps [add_commute]) 1);
+by (strip_tac 1);
+by (stac BufAC_Cmt_F_def3 1);
+by (dres_inst_tac [("P","%x. x")] (BufAC_Cmt_F_def3 RS subst) 1);
+by (Safe_tac);
+by ( etac Buf_f_empty 1);
+by ( etac Buf_f_d 1);
+by ( dtac Buf_f_d_req 1);
+by ( EVERY[safe_tac HOL_cs, etac ssubst 1, Simp_tac 1]);
+by (safe_tac (claset() addSDs [slen_fscons_eq RS iffD1] addSss simpset()));
+(*
+ 1. \\<And>i d xa ya t.
+ \\<lbrakk>f \\<in> BufEq;
+ \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
+ x \\<sqsubseteq> s \\<longrightarrow>
+ Fin (#2 * i) < #x \\<longrightarrow>
+ (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
+ (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
+ Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (#2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
+ (ya, t) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa\\<rbrakk>
+ \\<Longrightarrow> (xa, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>xa))) \\<in> down_iterate BufAC_Cmt_F i
+*)
+by (rotate_tac 2 1);
+by (dtac BufAC_Asm_prefix2 1);
+by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1, rotate_tac ~1 1,etac ssubst 1]);
+by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1]);
+by ( subgoal_tac "f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya" 1);
+by ( atac 2);
+by ( rotate_tac ~1 1);
+by ( Asm_full_simp_tac 1);
+by (hyp_subst_tac 1);
+(*
+ 1. \\<And>i d xa ya t ff ffa.
+ \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (#2 * i) < #ya;
+ (ya, ffa\\<cdot>ya) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa; f \\<in> BufEq;
+ \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
+ x \\<sqsubseteq> s \\<longrightarrow>
+ Fin (#2 * i) < #x \\<longrightarrow>
+ (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
+ (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
+ xa \\<in> BufAC_Asm; ff \\<in> BufEq; ffa \\<in> BufEq\\<rbrakk>
+ \\<Longrightarrow> (xa, ff\\<cdot>xa) \\<in> down_iterate BufAC_Cmt_F i
+*)
+by (smp_tac 2 1);
+by (mp_tac 1);
+by (mp_tac 1);
+by (etac impE 1);
+by ( EVERY[stac BufAC_Asm_cong 1, atac 1, atac 3, atac 1]);
+by ( eatac (BufAC_Asm_antiton RS antitonPD) 1 1);
+by (EVERY[stac BufAC_Asm_cong 1, atac 1, atac 3, atac 1, atac 1]);
+qed "BufAC_Cmt_2stream_monoP";
+
+Goalw [BufAC_Cmt_def] "x\\<in>BufAC_Cmt = (\\<forall>n. x\\<in>down_iterate BufAC_Cmt_F n)";
+by (stac (cont_BufAC_Cmt_F RS INTER_down_iterate_is_gfp) 1);
+by (Fast_tac 1);
+qed "BufAC_Cmt_iterate_all";
+
+(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
+ BufAC_Cmt_2stream_monoP*)
+Goal "f:BufEq ==> adm (%s. s:BufAC_Asm --> (s, f\\<cdot>s):BufAC_Cmt)";
+by (rtac flatstream_admI 1);
+by (stac BufAC_Cmt_iterate_all 1);
+by (dtac BufAC_Cmt_2stream_monoP 1);
+by Safe_tac;
+by (EVERY'[dtac spec, etac exE] 1);
+by (EVERY'[dtac spec, etac impE] 1);
+by (etac (BufAC_Asm_antiton RS antitonPD) 1);
+by (etac is_ub_thelub 1);
+by (smp_tac 3 1);
+by (dtac is_ub_thelub 1);
+by (mp_tac 1);
+by (mp_tac 1);
+by (etac mp 1);
+by (dtac (BufAC_Cmt_iterate_all RS iffD1) 1);
+by (etac spec 1);
+qed "adm_BufAC";
+
+
+
+(**** Buf_Eq_imp_AC by induction **********************************************)
+
+(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
+ BufAC_Cmt_2stream_monoP,adm_BufAC,BufAC_Cmt_d_req*)
+Goalw [BufAC_def] "BufEq <= BufAC";
+by (rtac subsetI 1);
+by (Simp_tac 1);
+by (rtac allI 1);
+by (rtac fstream_ind2 1);
+back();
+by ( etac adm_BufAC 1);
+by ( Safe_tac);
+by ( etac BufAC_Cmt_empty 1);
+by ( etac BufAC_Cmt_d 1);
+by ( dtac BufAC_Asm_prefix2 1);
+by ( contr_tac 1);
+by (fast_tac (claset() addIs [BufAC_Cmt_d_req, BufAC_Asm_prefix2]) 1);
+qed "Buf_Eq_imp_AC";
+
+(**** new approach for admissibility, reduces itself to absurdity *************)
+
+Goal "adm (\\<lambda>x. x\\<in>BufAC_Asm)";
+by(rtac def_gfp_admI 1);
+by(rtac BufAC_Asm_def 1);
+b y Safe_tac;
+b y rewtac BufAC_Asm_F_def;
+b y Safe_tac;
+b y etac swap 1;
+b y dtac (fstream_exhaust_eq RS iffD1) 1;
+b y Clarsimp_tac 1;
+b y datac fstream_lub_lemma 1 1;
+b y Clarify_tac 1;
+b y eres_inst_tac [("x","j")] all_dupE 1;
+b y Asm_full_simp_tac 1;
+b y dtac (BufAC_Asm_d2) 1;
+b y Clarify_tac 1;
+b y Simp_tac 1;
+b y rtac disjCI 1;
+b y etac swap 1;
+b y dtac (fstream_exhaust_eq RS iffD1) 1;
+b y Clarsimp_tac 1;
+b y datac fstream_lub_lemma 1 1;
+b y Clarsimp_tac 1;
+b y simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1;
+b y res_inst_tac [("x","Xa")] exI 1;
+br allI 1;
+b y rotate_tac ~1 1;
+b y eres_inst_tac [("x","i")] allE 1;
+b y Clarsimp_tac 1;
+b y eres_inst_tac [("x","jb")] allE 1;
+b y Clarsimp_tac 1;
+b y eres_inst_tac [("x","jc")] allE 1;
+by (clarsimp_tac (claset() addSDs [BufAC_Asm_d3], simpset()) 1);
+qed "adm_BufAC_Asm";
+
+Goal "adm (\\<lambda>u. u \\<notin> BufAC_Asm)"; (* uses antitonP *)
+by (rtac def_gfp_adm_nonP 1);
+by (rtac BufAC_Asm_def 1);
+b y rewtac BufAC_Asm_F_def;
+b y Safe_tac;
+b y etac swap 1;
+b y dtac (fstream_exhaust_eq RS iffD1) 1;
+b y Clarsimp_tac 1;
+b y ftac fstream_prefix 1;
+b y Clarsimp_tac 1;
+b y ftac BufAC_Asm_d2 1;
+b y Clarsimp_tac 1;
+b y rotate_tac ~1 1;
+b y etac contrapos_pp 1;
+b y dtac (fstream_exhaust_eq RS iffD1) 1;
+b y Clarsimp_tac 1;
+b y ftac fstream_prefix 1;
+b y Clarsimp_tac 1;
+b y ftac BufAC_Asm_d3 1;
+b y Force_tac 1;
+qed "adm_non_BufAC_Asm";
+
+Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
+by(rtac triv_admI 1);
+by(Clarify_tac 1);
+by(eatac Buf_Eq_imp_AC_lemma 1 1);
+ (* this is what we originally aimed to show, using admissibilty :-( *)
+qed "adm_BufAC";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,10 @@
+(* Title: HOLCF/FOCUS/Buffer_adm.thy
+ ID: $ $
+ Author: David von Oheimb, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility
+*)
+
+Buffer_adm = Buffer + Stream_adm
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/FOCUS.ML Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,22 @@
+(* Title: HOLCF/FOCUS/FOCUS.ML
+ ID: $ $
+ Author: David von Oheimb, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+open FOCUS;
+
+val ex_eqI = prove_goal thy "? xx. x = xx" (K [Auto_tac]);
+val ex2_eqI = prove_goal thy "? xx yy. x = xx & y = yy" (K [Auto_tac]);
+val eq_UU_symf = prove_goal thy "(UU = f x) = (f x = UU)" (K [Auto_tac]);
+
+AddSIs [ex_eqI, ex2_eqI];
+Addsimps[eq_UU_symf];
+Goal "(#x ~= 0) = (? a y. x = a~> y)";
+by (simp_tac (simpset() addsimps [slen_empty_eq, fstream_exhaust_eq]) 1);
+qed "fstream_exhaust_slen_eq";
+
+Addsimps[slen_less_1_eq, fstream_exhaust_slen_eq,
+ slen_fscons_eq, slen_fscons_less_eq];
+Addsimps[Suc_ile_eq];
+AddEs [strictI];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/FOCUS.thy Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,9 @@
+(* Title: HOLCF/FOCUS/FOCUS.thy
+ ID: $ $
+ Author: David von Oheimb, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+top level of FOCUS
+*)
+
+FOCUS = Fstream
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/Fstream.ML Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,238 @@
+(* Title: HOLCF/FOCUS/Fstream.ML
+ ID: $ $
+ Author: David von Oheimb, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+Goal "a = Def d \\<Longrightarrow> a\\<sqsubseteq>b \\<Longrightarrow> b = Def d";
+by (rtac (flat_eq RS iffD1 RS sym) 1);
+by (rtac Def_not_UU 1);
+by (dtac antisym_less_inverse 1);
+by (eatac (conjunct2 RS trans_less) 1 1);
+qed "Def_maximal";
+
+
+section "fscons";
+
+Goalw [fscons_def] "a~>s = Def a && s";
+by (Simp_tac 1);
+qed "fscons_def2";
+
+qed_goal "fstream_exhaust" thy "x = UU | (? a y. x = a~> y)" (fn _ => [
+ simp_tac (simpset() addsimps [fscons_def2]) 1,
+ cut_facts_tac [stream.exhaust] 1,
+ fast_tac (claset() addDs [not_Undef_is_Def RS iffD1]) 1]);
+
+qed_goal "fstream_cases" thy "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P"
+ (fn prems => [
+ cut_facts_tac [fstream_exhaust] 1,
+ etac disjE 1,
+ eresolve_tac prems 1,
+ REPEAT(etac exE 1),
+ eresolve_tac prems 1]);
+
+fun fstream_case_tac s i = res_inst_tac [("x",s)] fstream_cases i
+ THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
+
+qed_goal "fstream_exhaust_eq" thy "x ~= UU = (? a y. x = a~> y)" (fn _ => [
+ simp_tac(simpset() addsimps [fscons_def2,stream_exhaust_eq]) 1,
+ fast_tac (claset() addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
+
+
+qed_goal "fscons_not_empty" thy "a~> s ~= <>" (fn _ => [
+ stac fscons_def2 1,
+ Simp_tac 1]);
+Addsimps[fscons_not_empty];
+
+
+qed_goal "fscons_inject" thy "(a~> s = b~> t) = (a = b & s = t)" (fn _ => [
+ simp_tac (HOL_ss addsimps [fscons_def2]) 1,
+ stac (hd lift.inject RS sym) 1, (*2*back();*)
+ Simp_tac 1]);
+Addsimps[fscons_inject];
+
+qed_goal "fstream_prefix" thy "a~> s << t ==> ? tt. t = a~> tt & s << tt" (fn prems =>[
+ cut_facts_tac prems 1,
+ stream_case_tac "t" 1,
+ cut_facts_tac [fscons_not_empty] 1,
+ fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2]) 1,
+ asm_full_simp_tac (HOL_ss addsimps [fscons_def2]) 1,
+ dtac stream_flat_prefix 1,
+ rtac Def_not_UU 1,
+ fast_tac HOL_cs 1]);
+
+qed_goal "fstream_prefix'" thy
+ "x << a~> z = (x = <> | (? y. x = a~> y & y << z))" (fn _ => [
+ simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS stream_prefix'])1,
+ Step_tac 1,
+ ALLGOALS(etac swap),
+ fast_tac (HOL_cs addIs [refl_less] addEs [DefE]) 2,
+ rtac Lift_cases 1,
+ contr_tac 1,
+ Step_tac 1,
+ dtac (Def_inject_less_eq RS iffD1) 1,
+ Fast_tac 1]);
+Addsimps[fstream_prefix'];
+
+(* ------------------------------------------------------------------------- *)
+
+section "ft & rt";
+
+bind_thm("ft_empty",hd stream.sel_rews);
+qed_goalw "ft_fscons" thy [fscons_def] "ft\\<cdot>(m~> s) = Def m" (fn _ => [
+ (Simp_tac 1)]);
+Addsimps[ft_fscons];
+
+bind_thm("rt_empty",hd (tl stream.sel_rews));
+qed_goalw "rt_fscons" thy [fscons_def] "rt\\<cdot>(m~> s) = s" (fn _ => [
+ (Simp_tac 1)]);
+Addsimps[rt_fscons];
+
+qed_goalw "ft_eq" thy [fscons_def] "(ft\\<cdot>s = Def a) = (? t. s = a~> t)" (K [
+ Simp_tac 1,
+ Safe_tac,
+ etac subst 1,
+ rtac exI 1,
+ rtac (surjectiv_scons RS sym) 1,
+ Simp_tac 1]);
+Addsimps[ft_eq];
+
+Goal "(d\\<leadsto>y = x) = (ft\\<cdot>x = Def d & rt\\<cdot>x = y)";
+by Auto_tac;
+qed "surjective_fscons_lemma";
+Goal "ft\\<cdot>x = Def d \\<Longrightarrow> d\\<leadsto>rt\\<cdot>x = x";
+by (asm_simp_tac (simpset() addsimps [surjective_fscons_lemma]) 1);
+qed "surjective_fscons";
+
+
+(* ------------------------------------------------------------------------- *)
+
+section "take";
+
+qed_goalw "fstream_take_Suc" thy [fscons_def]
+ "stream_take (Suc n)\\<cdot>(a~> s) = a~> stream_take n\\<cdot>s" (K [
+ Simp_tac 1]);
+Addsimps[fstream_take_Suc];
+
+
+(* ------------------------------------------------------------------------- *)
+
+section "slen";
+
+(*bind_thm("slen_empty", slen_empty);*)
+
+qed_goalw "slen_fscons" thy [fscons_def] "#(m~> s) = iSuc (#s)" (fn _ => [
+ (Simp_tac 1)]);
+
+qed_goal "slen_fscons_eq" thy
+ "Fin (Suc n) < #x = (? a y. x = a~> y & Fin n < #y)" (fn _ => [
+ simp_tac (HOL_ss addsimps [fscons_def2, slen_scons_eq]) 1,
+ fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
+
+qed_goal "slen_fscons_eq_rev" thy
+ "#x < Fin (Suc (Suc n)) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [
+ simp_tac (HOL_ss addsimps [fscons_def2, slen_scons_eq_rev]) 1,
+ step_tac (HOL_cs addSEs [DefE]) 1,
+ step_tac (HOL_cs addSEs [DefE]) 1,
+ step_tac (HOL_cs addSEs [DefE]) 1,
+ step_tac (HOL_cs addSEs [DefE]) 1,
+ step_tac (HOL_cs addSEs [DefE]) 1,
+ step_tac (HOL_cs addSEs [DefE]) 1,
+ etac swap 1,
+ fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
+
+qed_goal "slen_fscons_less_eq" thy
+ "#(a~> y) < Fin (Suc (Suc n)) = (#y < Fin (Suc n))" (fn _ => [
+ stac slen_fscons_eq_rev 1,
+ fast_tac (HOL_cs addSDs [fscons_inject RS iffD1]) 1]);
+
+
+(* ------------------------------------------------------------------------- *)
+
+section "induction";
+
+qed_goal "fstream_ind" thy
+ "[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x" (fn prems => [
+ cut_facts_tac prems 1,
+ etac stream.ind 1,
+ atac 1,
+ fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]
+ addEs (tl (tl prems) RL [fscons_def2 RS subst])) 1]);
+
+qed_goal "fstream_ind2" thy
+ "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x" (fn prems => [
+ cut_facts_tac prems 1,
+ etac stream_ind2 1,
+ atac 1,
+ fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]
+ addIs ([hd(tl(tl prems))]RL[fscons_def2 RS subst]))1,
+ fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]
+ addEs [hd(tl(tl(tl prems))RL[fscons_def2 RS subst]
+ RL[fscons_def2 RS subst])])1]);
+
+
+(* ------------------------------------------------------------------------- *)
+
+section "fsfilter";
+
+qed_goalw "fsfilter_empty" thy [fsfilter_def] "A(C)UU = UU" (fn _ => [
+ rtac sfilter_empty 1]);
+
+qed_goalw "fsfilter_fscons" thy [fsfilter_def]
+ "A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" (fn _ => [
+ simp_tac (simpset() addsimps [fscons_def2,sfilter_scons,If_and_if]) 1]);
+
+qed_goal "fsfilter_emptys" thy "{}(C)x = UU" (fn _ => [
+ res_inst_tac [("x","x")] fstream_ind 1,
+ resolve_tac adm_lemmas 1,
+ cont_tacR 1,
+ rtac fsfilter_empty 1,
+ asm_simp_tac (simpset()addsimps [fsfilter_fscons]) 1]);
+
+qed_goal "fsfilter_insert" thy "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" (fn _=> [
+ simp_tac (simpset() addsimps [fsfilter_fscons]) 1]);
+
+qed_goal "fsfilter_single_in" thy "{a}(C)a~> x = a~> ({a}(C)x)" (fn _=> [
+ rtac fsfilter_insert 1]);
+
+qed_goal "fsfilter_single_out" thy "b ~= a ==> {a}(C)b~> x = ({a}(C)x)" (fn prems => [
+ cut_facts_tac prems 1,
+ asm_simp_tac (simpset() addsimps[fsfilter_fscons]) 1]);
+
+Goal "\\<lbrakk>chain Y; lub (range Y) = a\\<leadsto>s\\<rbrakk> \\<Longrightarrow> \\<exists>j t. Y j = a\\<leadsto>t";
+by (case_tac "max_in_chain i Y" 1);
+by (datac (lub_finch1 RS thelubI RS sym) 1 1);
+by (Force_tac 1);
+by (rewtac max_in_chain_def);
+by Auto_tac;
+by (fatac chain_mono3 1 1);
+by (res_inst_tac [("x","Y j")] fstream_cases 1);
+by (Force_tac 1);
+by (dres_inst_tac [("x","j")] is_ub_thelub 1);
+by (Force_tac 1);
+qed "fstream_lub_lemma1";
+
+Goal "\\<lbrakk>chain Y; lub (range Y) = a\\<leadsto>s\\<rbrakk> \\<Longrightarrow> (\\<exists>j t. Y j = a\\<leadsto>t) & (\\<exists>X. chain X & (!i. ? j. Y j = a\\<leadsto>X i) & lub (range X) = s)";
+by (fatac fstream_lub_lemma1 1 1);
+by (Clarsimp_tac 1);
+by (res_inst_tac [("x","%i. rt\\<cdot>(Y(i+j))")] exI 1);
+by (rtac conjI 1);
+by (etac (chain_shift RS chain_monofun) 1);
+by Safe_tac;
+by (dres_inst_tac [("x","j"),("y","i+j")] chain_mono3 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (res_inst_tac [("x","i+j")] exI 1);
+by (dtac fstream_prefix 1);
+by (Clarsimp_tac 1);
+by (stac (contlub_cfun RS sym) 1);
+by (rtac chainI 1);
+by (Fast_tac 1);
+by (etac chain_shift 1);
+by (stac (lub_const RS thelubI) 1);
+by (stac lub_range_shift 1);
+by (atac 1);
+by (Asm_simp_tac 1);
+qed "fstream_lub_lemma";
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/Fstream.thy Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,45 @@
+(* Title: HOLCF/FOCUS/Fstream.thy
+ ID: $ $
+ Author: David von Oheimb, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+FOCUS streams (with lifted elements)
+*)
+
+(* FOCUS flat streams *)
+
+Fstream = Stream +
+
+default term
+
+types 'a fstream = ('a lift) stream
+
+consts
+
+ fscons :: "'a \\<Rightarrow> 'a fstream \\<rightarrow> 'a fstream"
+ fsfilter :: "'a set \\<Rightarrow> 'a fstream \\<rightarrow> 'a fstream"
+
+syntax
+
+ "@emptystream":: "'a fstream" ("<>")
+ "@fscons" :: "'a \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream" ("(_~>_)" [66,65] 65)
+ "@fsfilter" :: "'a set \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63)
+
+syntax (xsymbols)
+
+ "@fscons" :: "'a \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream" ("(_\\<leadsto>_)"
+ [66,65] 65)
+ "@fsfilter" :: "'a set \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream" ("(_\\<copyright>_)"
+ [64,63] 63)
+translations
+
+ "<>" => "\\<bottom>"
+ "a~>s" == "fscons a\\<cdot>s"
+ "A(C)s" == "fsfilter A\\<cdot>s"
+
+defs
+
+ fscons_def "fscons a \\<equiv> \\<Lambda>s. Def a && s"
+ fsfilter_def "fsfilter A \\<equiv> sfilter\\<cdot>(flift2 (\\<lambda>x. x\\<in>A))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/ROOT.ML Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,15 @@
+(* Title: HOLCF/FOCUS/ROOT.ML
+ ID: $$
+ Author: David von Oheimb, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+ROOT file for the FOCUS extension of HOLCF.
+*)
+
+val banner = "HOLCF/FOCUS";
+writeln banner;
+
+path_add "~~/src/HOLCF/ex";
+
+use_thy "FOCUS";
+use_thy "Buffer_adm";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/Stream_adm.ML Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,179 @@
+(* Title: HOLCF/ex/Stream_adm.ML
+ ID: $ $
+ Author: David von Oheimb, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+(* ----------------------------------------------------------------------- *)
+
+val down_cont_def = thm "down_cont_def";
+val INTER_down_iterate_is_gfp = thm "INTER_down_iterate_is_gfp";
+
+section "admissibility";
+
+Goal "[| chain Y; !i. P (Y i);\
+\(!!Y. [| chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]\
+\ ==> P(lub (range Y))) |] ==> P(lub (range Y))";
+by (cut_facts_tac (premises()) 1);
+by (eatac increasing_chain_adm_lemma 1 1);
+by (etac thin_rl 1);
+by (EVERY'[eresolve_tac (premises()), atac, etac thin_rl] 1);
+by (rtac allI 1);
+by (case_tac "!j. stream_finite (Y j)" 1);
+by ( rtac chain_incr 1);
+by ( rtac allI 1);
+by ( dtac spec 1);
+by ( Safe_tac);
+by ( rtac exI 1);
+by ( rtac slen_strict_mono 1);
+by ( etac spec 1);
+by ( atac 1);
+by ( atac 1);
+by (dtac (not_ex RS iffD1) 1);
+by (stac slen_infinite 1);
+by (etac thin_rl 1);
+by (dtac spec 1);
+by (fold_goals_tac [ile_def]);
+by (etac (ile_iless_trans RS (Infty_eq RS iffD1)) 1);
+by (Simp_tac 1);
+qed "flatstream_adm_lemma";
+
+
+(* should be without reference to stream length? *)
+Goalw [adm_def] "[|(!!Y. [| chain Y; !i. P (Y i); \
+\!k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(lub (range Y)))|]==> adm P";
+by (strip_tac 1);
+by (eatac flatstream_adm_lemma 1 1);
+by (EVERY'[eresolve_tac (premises()), atac, atac] 1);
+qed "flatstream_admI";
+
+
+(* context (theory "Nat_InFinity");*)
+Goal "Fin (i + j) <= x ==> Fin i <= x";
+by (rtac ile_trans 1);
+by (atac 2);
+by (Simp_tac 1);
+qed "ile_lemma";
+
+Goalw [stream_monoP_def]
+"!!X. stream_monoP F ==> !i. ? l. !x y. \
+\ Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i";
+by (safe_tac HOL_cs);
+by (res_inst_tac [("x","i*ia")] exI 1);
+by (nat_ind_tac "ia" 1);
+by ( Simp_tac 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (etac allE 1 THEN etac all_dupE 1 THEN dtac mp 1 THEN etac ile_lemma 1);
+by (dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1);
+by (etac allE 1 THEN dtac mp 1 THEN rtac ile_lemma 1);
+by ( etac ile_trans 1);
+by ( etac slen_mono 1);
+by (etac ssubst 1);
+by (safe_tac HOL_cs);
+by ( eatac (ile_lemma RS slen_take_lemma3 RS subst) 2 1);
+by (etac allE 1);
+by (etac allE 1);
+by (dtac mp 1);
+by ( etac slen_rt_mult 1);
+by (dtac mp 1);
+by (etac monofun_rt_mult 1);
+by (mp_tac 1);
+by (atac 1);
+qed "stream_monoP2I";
+
+Goal "[| !i. ? l. !x y. \
+\Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;\
+\ down_cont F |] ==> adm (%x. x:gfp F)";
+byev[ etac (INTER_down_iterate_is_gfp RS ssubst) 1, (* cont *)
+ Simp_tac 1,
+ resolve_tac adm_lemmas 1,
+ rtac flatstream_admI 1,
+ etac allE 1,
+ etac exE 1,
+ etac allE 1 THEN etac exE 1,
+ etac allE 1 THEN etac allE 1 THEN dtac mp 1, (* stream_monoP *)
+ dtac ileI1 1,
+ dtac ile_trans 1,
+ rtac ile_iSuc 1,
+ dtac (iSuc_ile_mono RS iffD1) 1,
+ atac 1,
+ dtac mp 1,
+ etac is_ub_thelub 1,
+ Fast_tac 1];
+qed "stream_monoP2_gfp_admI";
+
+bind_thm("fstream_gfp_admI",stream_monoP2I RS stream_monoP2_gfp_admI);
+
+qed_goalw "stream_antiP2I" thy [stream_antiP_def]
+"!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]\
+\ ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i" (K [
+ rtac allI 1,
+ nat_ind_tac "i" 1,
+ Simp_tac 1,
+ Simp_tac 1,
+ strip_tac 1,
+ etac allE 1 THEN etac all_dupE 1 THEN etac exE 1 THEN etac exE 1,
+ etac conjE 1,
+ case_tac "#x < Fin ia" 1,
+ fast_tac HOL_cs 1,
+ fold_goals_tac [ile_def],
+ mp_tac 1,
+ etac all_dupE 1 THEN dtac mp 1 THEN rtac refl_less 1,
+ etac ssubst 1,
+ etac allE 1 THEN mp_tac 1,
+ dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1,
+ etac conjE 1 THEN rtac conjI 1,
+ etac (slen_take_lemma3 RS ssubst) 1 THEN atac 1,
+ atac 1,
+ etac allE 1 THEN etac allE 1 THEN dtac mp 1 THEN etac monofun_rt_mult 1,
+ mp_tac 1,
+ atac 1]);
+
+qed_goalw "stream_antiP2_non_gfp_admI" thy [adm_def]
+"!!X. [|!i x y. x << y --> y:down_iterate F i --> x:down_iterate F i; down_cont F |] \
+\ ==> adm (%u. ~ u:gfp F)" (K [
+ asm_simp_tac (simpset() addsimps [INTER_down_iterate_is_gfp]) 1,
+ fast_tac (claset() addSDs [is_ub_thelub]) 1]);
+
+bind_thm ("fstream_non_gfp_admI", stream_antiP2I RS
+ stream_antiP2_non_gfp_admI);
+
+
+
+(**new approach for adm********************************************************)
+
+section "antitonP";
+
+Goalw [antitonP_def] "[| antitonP P; y:P; x<<y |] ==> x:P";
+by Auto_tac;
+qed "antitonPD";
+
+Goalw [antitonP_def]"!x y. y:P --> x<<y --> x:P ==> antitonP P";
+by (Fast_tac 1);
+qed "antitonPI";
+
+Goalw [adm_def] "antitonP P ==> adm (%u. u~:P)";
+by (auto_tac (claset() addDs [antitonPD] addEs [is_ub_thelub],simpset()));
+qed "antitonP_adm_non_P";
+
+Goal "P \\<equiv> gfp F \\<Longrightarrow> {y. \\<exists>x::'a::pcpo. y \\<sqsubseteq> x \\<and> x \\<in> P} \\<subseteq> F {y. \\<exists>x. y \\<sqsubseteq> x \\<and> x \\<in> P} \\<Longrightarrow> \
+\ adm (\\<lambda>u. u\\<notin>P)";
+by (Asm_full_simp_tac 1);
+by (rtac antitonP_adm_non_P 1);
+by (rtac antitonPI 1);
+by (dtac gfp_upperbound 1);
+by (Fast_tac 1);
+qed "def_gfp_adm_nonP";
+
+Goalw [adm_def]
+"{lub (range Y) |Y. chain Y & (\\<forall>i. Y i \\<in> P)} \\<subseteq> P \\<Longrightarrow> adm (\\<lambda>x. x\\<in>P)";
+by (Fast_tac 1);
+qed "adm_set";
+
+Goal "P \\<equiv> gfp F \\<Longrightarrow> {lub (range Y) |Y. chain Y \\<and> (\\<forall>i. Y i \\<in> P)} \\<subseteq> \
+\ F {lub (range Y) |Y. chain Y \\<and> (\\<forall>i. Y i \\<in> P)} \\<Longrightarrow> adm (\\<lambda>x. x\\<in>P)";
+by (Asm_full_simp_tac 1);
+by (rtac adm_set 1);
+by (etac gfp_upperbound 1);
+qed "def_gfp_admI";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,29 @@
+(* Title: HOLCF/ex/Stream_adm.thy
+ ID: $ $
+ Author: David von Oheimb, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+Admissibility for streams
+*)
+
+Stream_adm = Stream + Continuity +
+
+consts
+
+ stream_monoP,
+ stream_antiP :: "(('a stream) set \\<Rightarrow> ('a stream) set) \\<Rightarrow> bool"
+
+defs
+
+ stream_monoP_def "stream_monoP F \\<equiv> \\<exists>Q i. \\<forall>P s. Fin i \\<le> #s \\<longrightarrow>
+ s \\<in> F P = (stream_take i\\<cdot>s \\<in> Q \\<and> iterate i rt s \\<in> P)"
+ stream_antiP_def "stream_antiP F \\<equiv> \\<forall>P x. \\<exists>Q i.
+ (#x < Fin i \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow> y \\<in> F P \\<longrightarrow> x \\<in> F P)) \\<and>
+ (Fin i <= #x \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow>
+ y \\<in> F P = (stream_take i\\<cdot>y \\<in> Q \\<and> iterate i rt y \\<in> P)))"
+
+constdefs
+ antitonP :: "'a set => bool"
+ "antitonP P \\<equiv> \\<forall>x y. x \\<sqsubseteq> y \\<longrightarrow> y\\<in>P \\<longrightarrow> x\\<in>P"
+
+end
--- a/src/HOLCF/IsaMakefile Thu May 31 16:52:54 2001 +0200
+++ b/src/HOLCF/IsaMakefile Thu May 31 16:53:00 2001 +0200
@@ -8,7 +8,8 @@
default: HOLCF
images: HOLCF IOA
-test: HOLCF-IMP HOLCF-ex IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex
+test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \
+ IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex
all: images test
@@ -58,10 +59,21 @@
$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.ML ex/Dagstuhl.thy \
ex/Dnat.ML ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \
ex/Focus_ex.thy ex/Hoare.ML ex/Hoare.thy ex/Loop.ML ex/Loop.thy \
- ex/ROOT.ML ex/Stream.ML ex/Stream.thy ex/loeckx.ML
+ ex/ROOT.ML ex/Stream.ML ex/Stream.thy ex/loeckx.ML \
+ ../HOL/Library/Nat_Infinity.thy
@$(ISATOOL) usedir $(OUT)/HOLCF ex
+## HOLCF-FOCUS
+
+HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
+
+$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstream.thy FOCUS/Fstream.ML \
+ FOCUS/FOCUS.thy FOCUS/FOCUS.ML \
+ FOCUS/Stream_adm.thy FOCUS/Stream_adm.ML ../HOL/Library/Continuity.thy \
+ FOCUS/Buffer.thy FOCUS/Buffer.ML FOCUS/Buffer_adm.thy FOCUS/Buffer_adm.ML
+ @$(ISATOOL) usedir $(OUT)/HOLCF FOCUS
+
## IOA
IOA: HOLCF $(OUT)/IOA
@@ -154,5 +166,6 @@
clean:
@rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \
- $(LOG)/HOLCF-ex.gz $(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \
+ $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz \
+ $(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \
$(LOG)/IOA-NTP.gz $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz