# HG changeset patch # User oheimb # Date 991320780 -7200 # Node ID 4c55b020d6ee3ff5ad7a52dd6148ac6fbc9f74b3 # Parent fcb507c945c3832faf0d10daf37015269c54e76c added FOCUS including the One-Element Buffer by Manfred Broy diff -r fcb507c945c3 -r 4c55b020d6ee src/HOLCF/FOCUS/Buffer.ML --- /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\\(Md d\\<>) = <> & \ + \(!x. ? ff:BufEq. f\\(Md d\\\\\\x) = d\\(ff\\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 \\ f\\<> = <>" BufEq_unfold; +val Buf_f_d = prove_forw "f:BufEq \\ f\\(Md d\\<>) = <>" BufEq_unfold; +val Buf_f_d_req = prove_forw + "f:BufEq \\ \\ff. ff:BufEq \\ f\\(Md d\\\\\\x) = d\\ff\\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\\x & (x = <> | (ft\\x = Def \\ & (rt\\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\\<>:BufAC_Asm" BufAC_Asm_unfold []; +val BufAC_Asm_d_req = prove_backw "x:BufAC_Asm ==> Md d\\\\\\x:BufAC_Asm" + BufAC_Asm_unfold []; +val BufAC_Asm_prefix2 = prove_forw "a\\b\\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\\<> --> t = <>) & \ + \(s = Md d\\\\\\x --> ft\\t = Def d & (x, rt\\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\\<>):BufAC_Cmt" + BufAC_Cmt_unfold [Buf_f_empty]; + +val BufAC_Cmt_d = prove_backw "f:BufEq ==> (a\\\\, f\\(a\\\$):BufAC_Cmt" + BufAC_Cmt_unfold [Buf_f_d]; + +val BufAC_Cmt_d2 = prove_forw + "(Md d\\\\, f\$Md d\\\$):BufAC_Cmt ==> f\$Md d\\\$ = \\" BufAC_Cmt_unfold; +val BufAC_Cmt_d3 = prove_forw +"(Md d\\\\\\x, f\$Md d\\\\\\x)):BufAC_Cmt ==> (x, rt\\(f\\(Md d\\\\\\x))):BufAC_Cmt" + BufAC_Cmt_unfold; + +val BufAC_Cmt_d32 = prove_forw +"(Md d\\\\\\x, f\\(Md d\\\\\\x)):BufAC_Cmt ==> ft\\(f\\(Md d\\\\\\x)) = Def d" + BufAC_Cmt_unfold; + +(**** BufAC *******************************************************************) + +Goalw [BufAC_def] "f \\ BufAC \\ f\\(Md d\\\$ = \\"; +by (fast_tac (claset() addIs [BufAC_Cmt_d2, BufAC_Asm_d]) 1); +qed "BufAC_f_d"; + +Goal "(? ff:B. (!x. f\\(a\\b\\x) = d\\ff\\x)) = \ + \((!x. ft\\(f\\(a\\b\\x)) = Def d) & (LAM x. rt\\(f\\(a\\b\\x))):B)"; +(* this is an instance (though unification cannot handle this) of +Goal "(? ff:B. (!x. f\\x = d\\ff\\x)) = \ + \((!x. ft\\(f\\x) = Def d) & (LAM x. rt\\(f\\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\\BufAC \\ \\ff\\BufAC. \\x. f\\(Md d\\\\\\x) = d\\ff\\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\\<> = <> & \ + \ (!d x. h \\ \\(Md d\\x) = h (Sd d)\\x & \ + \ (? hh:BufSt_P. h (Sd d)\\(\\\\x) = d\\(hh \\ \\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 \\ <> = <>" + BufSt_P_unfold; +val BufSt_P_d = prove_forw "h:BufSt_P ==> h \\ \\(Md d\\x) = h (Sd d)\\x" + BufSt_P_unfold; +val BufSt_P_d_req = prove_forw "h:BufSt_P ==> \\hh\\BufSt_P. \ + \ h (Sd d)\\(\\ \\x) = d\\(hh \\ \\x)" + BufSt_P_unfold; + + +(**** Buf_AC_imp_Eq ***********************************************************) + +Goalw [BufEq_def] "BufAC \\ 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 "\\s f ff. f\\BufEq \\ ff\\BufEq \\ \ +\ s\\BufAC_Asm \\ stream_take n\\(f\\s) = stream_take n\\(ff\\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 "\\f \\ BufEq; ff \\ BufEq; s \\ BufAC_Asm\\ \\ f\\s = ff\\s"; +by (resolve_tac stream.take_lemmas 1); +by (eatac BufAC_Asm_cong_lemma 2 1); +qed "BufAC_Asm_cong"; + +Goalw [BufAC_Cmt_def] "\\f \\ BufEq; x \\ BufAC_Asm\\ \\ (x, f\\x) \\ 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 \\ 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 \\ BufEq" (K [ + rtac gfp_mono 1, + rewtac BufEq_F_def, + Fast_tac 1]); + +(* direct proof of "BufEq \\ 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","\\s. case s of Sd d => \\x. f\\(Md d\\x)| \\ => 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)); + + + diff -r fcb507c945c3 -r 4c55b020d6ee src/HOLCF/FOCUS/Buffer.thy --- /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 ("\\") + +datatype + + State = Sd D | Snil ("\\") + +types + + SPF11 = "M fstream \\ D fstream" + SPEC11 = "SPF11 set" + SPSF11 = "State \\ SPF11" + SPECS11 = "SPSF11 set" + +consts + + BufEq_F :: "SPEC11 \\ SPEC11" + BufEq :: "SPEC11" + BufEq_alt :: "SPEC11" + + BufAC_Asm_F :: " (M fstream set) \\ (M fstream set)" + BufAC_Asm :: " (M fstream set)" + BufAC_Cmt_F :: "((M fstream * D fstream) set) \\ \ +\ ((M fstream * D fstream) set)" + BufAC_Cmt :: "((M fstream * D fstream) set)" + BufAC :: "SPEC11" + + BufSt_F :: "SPECS11 \\ SPECS11" + BufSt_P :: "SPECS11" + BufSt :: "SPEC11" + +defs + + BufEq_F_def "BufEq_F B \\ {f. \\d. f\\(Md d\\<>) = <> \\ + (\\x. \\ff\\B. f\\(Md d\\\\\\x) = d\\ff\\x)}" + BufEq_def "BufEq \\ gfp BufEq_F" + BufEq_alt_def "BufEq_alt \\ gfp (\\B. {f. \\d. f\\(Md d\\<> ) = <> \\ + (\\ff\\B. (\\x. f\\(Md d\\\\\\x) = d\\ff\\x))})" + BufAC_Asm_F_def "BufAC_Asm_F A \\ {s. s = <> \\ + (\\d x. s = Md d\\x \\ (x = <> \\ (ft\\x = Def \\ \\ (rt\\x)\\A)))}" + BufAC_Asm_def "BufAC_Asm \\ gfp BufAC_Asm_F" + + BufAC_Cmt_F_def "BufAC_Cmt_F C \\ {(s,t). \\d x. + (s = <> \\ t = <> ) \\ + (s = Md d\\<> \\ t = <> ) \\ + (s = Md d\\\\\\x \\ (ft\\t = Def d \\ (x,rt\\t)\\C))}" + BufAC_Cmt_def "BufAC_Cmt \\ gfp BufAC_Cmt_F" + BufAC_def "BufAC \\ {f. \\x. x\\BufAC_Asm \\ (x,f\\x)\\BufAC_Cmt}" + + BufSt_F_def "BufSt_F H \\ {h. \\s . h s \\<> = <> \\ + (\\d x. h \\ \\(Md d\\x) = h (Sd d)\\x \\ + (\\hh\\H. h (Sd d)\\(\\ \\x) = d\\(hh \\\\x)))}" + BufSt_P_def "BufSt_P \\ gfp BufSt_F" + BufSt_def "BufSt \\ {f. \\h\\BufSt_P. f = h \\}" + +end diff -r fcb507c945c3 -r 4c55b020d6ee src/HOLCF/FOCUS/Buffer_adm.ML --- /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\\s:BufAC_Asm ==> ? d. a=Md d" BufAC_Asm_unfold; +val BufAC_Asm_d3 = prove_forw + "a\\b\\s:BufAC_Asm ==> ? d. a=Md d & b=\\ & 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\\s=Def(Md d)) & (rt\\s=<> | ft\\(rt\\s)=Def \\ & rt\\(rt\\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\\<> --> t = <> ) & \ +\ (s = Md d\\\\\\x --> ft\\t = Def d & (x,rt\\t):C))" (fn _=> [ + subgoal_tac "!d x. (s = Md d\\\\\\x --> (? y. t = d\\y & (x,y):C)) = \ + \ (s = Md d\\\\\\x --> ft\\t = Def d & (x,rt\\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\\\\\\<>)}")] 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\\\\\\<>)}")] 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\\s = ff\\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\\s):BufAC_Cmt|] ==> (a\\b\\s, f\\(a\\b\\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\\x):down_iterate BufAC_Cmt_F i --> \ + \ (s,f\\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. \\i d xa ya t. + \\f \\ BufEq; + \\x s. s \\ BufAC_Asm \\ + x \\ s \\ + Fin (#2 * i) < #x \\ + (x, f\\x) \\ down_iterate BufAC_Cmt_F i \\ + (s, f\\s) \\ down_iterate BufAC_Cmt_F i; + Md d\\\\\\xa \\ BufAC_Asm; Fin (#2 * i) < #ya; f\\(Md d\\\\\\ya) = d\\t; + (ya, t) \\ down_iterate BufAC_Cmt_F i; ya \\ xa\\ + \\ (xa, rt\\(f\\(Md d\\\\\\xa))) \\ 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\\(Md d\\\\\\ya) = d\\ffa\\ya" 1); +by ( atac 2); +by ( rotate_tac ~1 1); +by ( Asm_full_simp_tac 1); +by (hyp_subst_tac 1); +(* + 1. \\i d xa ya t ff ffa. + \\f\\(Md d\\\\\\ya) = d\\ffa\\ya; Fin (#2 * i) < #ya; + (ya, ffa\\ya) \\ down_iterate BufAC_Cmt_F i; ya \\ xa; f \\ BufEq; + \\x s. s \\ BufAC_Asm \\ + x \\ s \\ + Fin (#2 * i) < #x \\ + (x, f\\x) \\ down_iterate BufAC_Cmt_F i \\ + (s, f\\s) \\ down_iterate BufAC_Cmt_F i; + xa \\ BufAC_Asm; ff \\ BufEq; ffa \\ BufEq\\ + \\ (xa, ff\\xa) \\ 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\\BufAC_Cmt = (\\n. x\\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\\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 (\\x. x\\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 (\\u. u \\ 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 \\ BufEq \\ adm (\\u. u \\ BufAC_Asm \\ (u, f\\u) \\ 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"; diff -r fcb507c945c3 -r 4c55b020d6ee src/HOLCF/FOCUS/Buffer_adm.thy --- /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 + diff -r fcb507c945c3 -r 4c55b020d6ee src/HOLCF/FOCUS/FOCUS.ML --- /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]; diff -r fcb507c945c3 -r 4c55b020d6ee src/HOLCF/FOCUS/FOCUS.thy --- /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 diff -r fcb507c945c3 -r 4c55b020d6ee src/HOLCF/FOCUS/Fstream.ML --- /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 \\ a\\b \\ 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\\(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\\(m~> s) = s" (fn _ => [ + (Simp_tac 1)]); +Addsimps[rt_fscons]; + +qed_goalw "ft_eq" thy [fscons_def] "(ft\\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\\