--- a/src/HOLCF/FOCUS/Buffer.ML Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Buffer.ML Tue Sep 06 21:51:17 2005 +0200
@@ -1,13 +1,13 @@
-(* Title: HOLCF/FOCUS/Buffer.ML
+(* Title: HOLCF/FOCUS/Buffer.ML
ID: $Id$
- Author: David von Oheimb, TU Muenchen
+ Author: David von Oheimb, TU Muenchen
*)
-val set_cong = prove_goal Set.thy "!!X. A = B ==> (x:A) = (x:B)" (K [
- etac subst 1, rtac refl 1]);
+val set_cong = prove_goal (theory "Set") "!!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 B_prover s tac eqs = prove_goal (the_context ()) 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;
@@ -15,74 +15,74 @@
(**** BufEq *******************************************************************)
-val mono_BufEq_F = prove_goalw thy [mono_def, BufEq_F_def]
- "mono BufEq_F" (K [Fast_tac 1]);
+val mono_BufEq_F = prove_goalw (the_context ()) [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 BufEq_unfold = prove_goal (the_context ()) "(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;
+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 mono_BufAC_Asm_F = prove_goalw (the_context ()) [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. \
+val BufAC_Asm_unfold = prove_goal (the_context ()) "(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]);
+ 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 [];
+ BufAC_Asm_unfold [];
val BufAC_Asm_prefix2 = prove_forw "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> s:BufAC_Asm"
- BufAC_Asm_unfold;
+ 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 mono_BufAC_Cmt_F = prove_goalw (the_context ()) [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. \
+val BufAC_Cmt_unfold = prove_goal (the_context ()) "((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]);
+ 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];
+ 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_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
+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
+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;
+ BufAC_Cmt_unfold;
-val BufAC_Cmt_d32 = prove_forw
+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_Cmt_unfold;
(**** BufAC *******************************************************************)
@@ -114,33 +114,33 @@
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 (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 mono_BufSt_F = prove_goalw (the_context ()) [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 & \
+val BufSt_P_unfold = prove_goal (the_context ()) "(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]);
+ 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_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;
+ 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;
+ \ h (Sd d)\\<cdot>(\\<bullet> \\<leadsto>x) = d\\<leadsto>(hh \\<currency> \\<cdot>x)"
+ BufSt_P_unfold;
(**** Buf_AC_imp_Eq ***********************************************************)
@@ -210,11 +210,11 @@
(**** 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]);
+val Buf_Eq_alt_imp_Eq = prove_goalw (the_context ()) [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 *)
@@ -224,10 +224,10 @@
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",
+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",
+bind_thm ("Buf_Eq_alt_eq",
subset_antisym OF [Buf_Eq_alt_imp_Eq, Buf_Eq_imp_Eq_alt]);
@@ -245,11 +245,11 @@
Goalw [BufSt_def, BufSt_P_def] "BufEq <= BufSt";
by Safe_tac;
-by (EVERY'[rename_tac "f", res_inst_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 (rewtac BufSt_F_def);
by (Simp_tac 1);
by Safe_tac;
by ( EVERY'[rename_tac "s", induct_tac "s"] 1);
@@ -262,6 +262,3 @@
qed "Buf_Eq_imp_St";
bind_thm ("Buf_Eq_eq_St", Buf_St_imp_Eq RS (Buf_Eq_imp_St RS subset_antisym));
-
-
-
--- a/src/HOLCF/FOCUS/Buffer.thy Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Buffer.thy Tue Sep 06 21:51:17 2005 +0200
@@ -1,6 +1,6 @@
-(* Title: HOLCF/FOCUS/Buffer.thy
+(* Title: HOLCF/FOCUS/Buffer.thy
ID: $Id$
- Author: David von Oheimb, TU Muenchen
+ Author: David von Oheimb, TU Muenchen
Formalization of section 4 of
@@ -20,65 +20,68 @@
*)
-Buffer = FOCUS +
+theory Buffer
+imports FOCUS
+begin
-types D
-arities D :: type
+typedecl D
datatype
- M = Md D | Mreq ("\\<bullet>")
+ M = Md D | Mreq ("\<bullet>")
datatype
- State = Sd D | Snil ("\\<currency>")
+ State = Sd D | Snil ("\<currency>")
types
- SPF11 = "M fstream \\<rightarrow> D fstream"
- SPEC11 = "SPF11 set"
- SPSF11 = "State \\<Rightarrow> SPF11"
- SPECS11 = "SPSF11 set"
+ 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"
+ 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"
+ 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"
+ 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"
+ 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}"
+ 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>}"
+ 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>}"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
--- a/src/HOLCF/FOCUS/Buffer_adm.ML Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML Tue Sep 06 21:51:17 2005 +0200
@@ -1,6 +1,6 @@
-(* Title: HOLCF/FOCUS/Buffer_adm.ML
+(* Title: HOLCF/FOCUS/Buffer_adm.ML
ID: $Id$
- Author: David von Oheimb, TU Muenchen
+ Author: David von Oheimb, TU Muenchen
*)
infixr 0 y;
@@ -10,30 +10,30 @@
Addsimps [thm "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
+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]
+val BufAC_Asm_F_def3 = prove_goalw (the_context ()) [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]);
+ 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]
+val BufAC_Cmt_F_def3 = prove_goalw (the_context ()) [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 [thm "surjectiv_scons" RS sym], simpset())]);
+ 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 [thm "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])]);
+val cont_BufAC_Cmt_F = prove_goal (the_context ()) "down_cont BufAC_Cmt_F" (K [
+ auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Cmt_F_def3])]);
(**** adm_BufAC_Asm ***********************************************************)
@@ -44,7 +44,7 @@
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 [
+val adm_BufAC_Asm = prove_goalw (the_context ()) [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]);
@@ -72,21 +72,21 @@
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 (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
+val BufAC_Cmt_d_req = prove_goal (the_context ())
"!!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,
- ftac Buf_f_d_req 1,
- auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
+ rtac (BufAC_Cmt_unfold RS iffD2) 1,
+ strip_tac 1,
+ ftac Buf_f_d_req 1,
+ auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
(*adm_BufAC_Asm*)
Goal "antitonP BufAC_Asm";
@@ -99,16 +99,16 @@
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;
+ 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;
+ 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";
+ \ (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. 2*i")] exI 1);
by (rtac allI 1);
by (induct_tac "i" 1);
@@ -137,12 +137,12 @@
*)
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, 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 ( 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 ( rotate_tac ~1 1);
+by ( Asm_full_simp_tac 1);
by (hyp_subst_tac 1);
(*
1. \\<And>i d xa ya t ff ffa.
@@ -272,6 +272,6 @@
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);
+by (eatac Buf_Eq_imp_AC_lemma 1 1);
(* this is what we originally aimed to show, using admissibilty :-( *)
qed "adm_BufAC'";
--- a/src/HOLCF/FOCUS/Buffer_adm.thy Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy Tue Sep 06 21:51:17 2005 +0200
@@ -1,9 +1,14 @@
-(* Title: HOLCF/FOCUS/Buffer_adm.thy
+(* Title: HOLCF/FOCUS/Buffer_adm.thy
ID: $Id$
- Author: David von Oheimb, TU Muenchen
-
-One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility
+ Author: David von Oheimb, TU Muenchen
*)
-Buffer_adm = Buffer + Stream_adm
+header {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
+theory Buffer_adm
+imports Buffer Stream_adm
+begin
+
+end
+
+
--- a/src/HOLCF/FOCUS/FOCUS.ML Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/FOCUS.ML Tue Sep 06 21:51:17 2005 +0200
@@ -1,11 +1,11 @@
-(* Title: HOLCF/FOCUS/FOCUS.ML
+(* Title: HOLCF/FOCUS/FOCUS.ML
ID: $Id$
- Author: David von Oheimb, TU Muenchen
+ Author: David von Oheimb, TU Muenchen
*)
-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]);
+val ex_eqI = prove_goal (the_context ()) "? xx. x = xx" (K [Auto_tac]);
+val ex2_eqI = prove_goal (the_context ()) "? xx yy. x = xx & y = yy" (K [Auto_tac]);
+val eq_UU_symf = prove_goal (the_context ()) "(UU = f x) = (f x = UU)" (K [Auto_tac]);
AddSIs [ex_eqI, ex2_eqI];
Addsimps[eq_UU_symf];
@@ -14,6 +14,6 @@
qed "fstream_exhaust_slen_eq";
Addsimps[thm "slen_less_1_eq", fstream_exhaust_slen_eq,
- thm "slen_fscons_eq", thm "slen_fscons_less_eq"];
+ thm "slen_fscons_eq", thm "slen_fscons_less_eq"];
Addsimps[thm "Suc_ile_eq"];
AddEs [strictI];
--- a/src/HOLCF/FOCUS/FOCUS.thy Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/FOCUS.thy Tue Sep 06 21:51:17 2005 +0200
@@ -1,8 +1,12 @@
-(* Title: HOLCF/FOCUS/FOCUS.thy
+(* Title: HOLCF/FOCUS/FOCUS.thy
ID: $Id$
- Author: David von Oheimb, TU Muenchen
-
-top level of FOCUS
+ Author: David von Oheimb, TU Muenchen
*)
-FOCUS = Fstream
+header {* Top level of FOCUS *}
+
+theory FOCUS
+imports Fstream
+begin
+
+end
--- a/src/HOLCF/FOCUS/Fstream.ML Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Fstream.ML Tue Sep 06 21:51:17 2005 +0200
@@ -1,6 +1,6 @@
-(* Title: HOLCF/FOCUS/Fstream.ML
+(* Title: HOLCF/FOCUS/Fstream.ML
ID: $Id$
- Author: David von Oheimb, TU Muenchen
+ Author: David von Oheimb, TU Muenchen
*)
Addsimps[eq_UU_iff RS sym];
@@ -19,60 +19,60 @@
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 [thm "stream.exhaust"] 1,
- fast_tac (claset() addDs [not_Undef_is_Def RS iffD1]) 1]);
+qed_goal "fstream_exhaust" (the_context ()) "x = UU | (? a y. x = a~> y)" (fn _ => [
+ simp_tac (simpset() addsimps [fscons_def2]) 1,
+ cut_facts_tac [thm "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"
+qed_goal "fstream_cases" (the_context ()) "[| 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]);
+ 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);
+ 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,thm "stream_exhaust_eq"]) 1,
- fast_tac (claset() addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
+qed_goal "fstream_exhaust_eq" (the_context ()) "(x ~= UU) = (? a y. x = a~> y)" (fn _ => [
+ simp_tac(simpset() addsimps [fscons_def2,thm "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,
+qed_goal "fscons_not_empty" (the_context ()) "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();*)
+qed_goal "fscons_inject" (the_context ()) "(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,
- res_inst_tac [("x","t")] (thm "stream.casedist") 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 (thm "stream_flat_prefix") 1,
- rtac Def_not_UU 1,
- fast_tac HOL_cs 1]);
+qed_goal "fstream_prefix" (the_context ()) "a~> s << t ==> ? tt. t = a~> tt & s << tt" (fn prems =>[
+ cut_facts_tac prems 1,
+ res_inst_tac [("x","t")] (thm "stream.casedist") 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 (thm "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 thm "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]);
+qed_goal "fstream_prefix'" (the_context ())
+ "x << a~> z = (x = <> | (? y. x = a~> y & y << z))" (fn _ => [
+ simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS thm "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'];
(* ------------------------------------------------------------------------- *)
@@ -80,22 +80,22 @@
section "ft & rt";
bind_thm("ft_empty",hd (thms "stream.sel_rews"));
-qed_goalw "ft_fscons" thy [fscons_def] "ft\\<cdot>(m~> s) = Def m" (fn _ => [
- (Simp_tac 1)]);
+qed_goalw "ft_fscons" (the_context ()) [fscons_def] "ft\\<cdot>(m~> s) = Def m" (fn _ => [
+ (Simp_tac 1)]);
Addsimps[ft_fscons];
bind_thm("rt_empty",hd (tl (thms "stream.sel_rews")));
-qed_goalw "rt_fscons" thy [fscons_def] "rt\\<cdot>(m~> s) = s" (fn _ => [
- (Simp_tac 1)]);
+qed_goalw "rt_fscons" (the_context ()) [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 (thm "surjectiv_scons" RS sym) 1,
- Simp_tac 1]);
+qed_goalw "ft_eq" (the_context ()) [fscons_def] "(ft\\<cdot>s = Def a) = (? t. s = a~> t)" (K [
+ Simp_tac 1,
+ Safe_tac,
+ etac subst 1,
+ rtac exI 1,
+ rtac (thm "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)";
@@ -110,95 +110,95 @@
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]);
+qed_goalw "fstream_take_Suc" (the_context ()) [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_goalw "slen_fscons" (the_context ()) [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, thm "slen_scons_eq"]) 1,
- fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
+qed_goal "slen_fscons_eq" (the_context ())
+ "(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)" (fn _ => [
+ simp_tac (HOL_ss addsimps [fscons_def2, thm "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, thm "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_eq_rev" (the_context ())
+ "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [
+ simp_tac (HOL_ss addsimps [fscons_def2, thm "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]);
+qed_goal "slen_fscons_less_eq" (the_context ())
+ "(#(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 (thm "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_ind" (the_context ())
+ "[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x" (fn prems => [
+ cut_facts_tac prems 1,
+ etac (thm "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
+qed_goal "fstream_ind2" (the_context ())
"[| 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 (thm "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]);
+ cut_facts_tac prems 1,
+ etac (thm "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 (thm "sfilter_empty") 1]);
+qed_goalw "fsfilter_empty" (the_context ()) [fsfilter_def] "A(C)UU = UU" (fn _ => [
+ rtac (thm "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,thm "sfilter_scons",If_and_if]) 1]);
+qed_goalw "fsfilter_fscons" (the_context ()) [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,thm "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_emptys" (the_context ()) "{}(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 [thm "fsfilter_fscons"]) 1]);
+qed_goal "fsfilter_insert" (the_context ()) "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" (fn _=> [
+ simp_tac (simpset() addsimps [thm "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_in" (the_context ()) "{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]);
+qed_goal "fsfilter_single_out" (the_context ()) "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);
@@ -235,5 +235,3 @@
by (atac 1);
by (Asm_simp_tac 1);
qed "fstream_lub_lemma";
-
-
--- a/src/HOLCF/FOCUS/Fstream.thy Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy Tue Sep 06 21:51:17 2005 +0200
@@ -1,45 +1,49 @@
-(* Title: HOLCF/FOCUS/Fstream.thy
+(* Title: HOLCF/FOCUS/Fstream.thy
ID: $Id$
- Author: David von Oheimb, TU Muenchen
+ Author: David von Oheimb, TU Muenchen
FOCUS streams (with lifted elements)
###TODO: integrate Fstreams.thy
*)
-(* FOCUS flat streams *)
-
-Fstream = Stream +
+header {* FOCUS flat streams *}
-default type
+theory Fstream
+imports Stream
+begin
-types 'a fstream = ('a lift) stream
+defaultsort type
+
+types 'a fstream = "'a lift stream"
consts
- fscons :: "'a \\<Rightarrow> 'a fstream \\<rightarrow> 'a fstream"
- fsfilter :: "'a set \\<Rightarrow> 'a fstream \\<rightarrow> 'a fstream"
+ 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)
+ "@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)
+ "@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"
+ "<>" => "\<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))"
+ fscons_def: "fscons a \<equiv> \<Lambda> s. Def a && s"
+ fsfilter_def: "fsfilter A \<equiv> sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
--- a/src/HOLCF/FOCUS/Stream_adm.ML Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.ML Tue Sep 06 21:51:17 2005 +0200
@@ -1,6 +1,6 @@
-(* Title: HOLCF/ex/Stream_adm.ML
+(* Title: HOLCF/ex/Stream_adm.ML
ID: $Id$
- Author: David von Oheimb, TU Muenchen
+ Author: David von Oheimb, TU Muenchen
*)
(* ----------------------------------------------------------------------- *)
@@ -77,66 +77,66 @@
by ( etac (thm "slen_rt_mult") 1);
by (dtac mp 1);
by (etac (thm "monofun_rt_mult") 1);
-by (mp_tac 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 (thm "ileI1") 1,
- dtac (thm "ile_trans") 1,
- rtac (thm "ile_iSuc") 1,
- dtac (thm "iSuc_ile_mono" RS iffD1) 1,
- atac 1,
- dtac mp 1,
- etac is_ub_thelub 1,
- Fast_tac 1];
+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 (thm "ileI1") 1,
+ dtac (thm "ile_trans") 1,
+ rtac (thm "ile_iSuc") 1,
+ dtac (thm "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]
+qed_goalw "stream_antiP2I" (the_context ()) [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,
- induct_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 i" 1,
- fast_tac HOL_cs 1,
- fold_goals_tac [thm "ile_def"],
- mp_tac 1,
- etac all_dupE 1 THEN dtac mp 1 THEN rtac refl_less 1,
- etac ssubst 1,
+ rtac allI 1,
+ induct_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 i" 1,
+ fast_tac HOL_cs 1,
+ fold_goals_tac [thm "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 (thm "slen_take_lemma3" RS ssubst) 1 THEN atac 1,
- atac 1,
- etac allE 1 THEN etac allE 1 THEN dtac mp 1 THEN etac (thm "monofun_rt_mult") 1,
- mp_tac 1,
- atac 1]);
+ dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1,
+ etac conjE 1 THEN rtac conjI 1,
+ etac (thm "slen_take_lemma3" RS ssubst) 1 THEN atac 1,
+ atac 1,
+ etac allE 1 THEN etac allE 1 THEN dtac mp 1 THEN etac (thm "monofun_rt_mult") 1,
+ mp_tac 1,
+ atac 1]);
-qed_goalw "stream_antiP2_non_gfp_admI" thy [adm_def]
+qed_goalw "stream_antiP2_non_gfp_admI" (the_context ()) [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]);
+ 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);
+bind_thm ("fstream_non_gfp_admI", stream_antiP2I RS
+ stream_antiP2_non_gfp_admI);
@@ -165,7 +165,7 @@
by (Fast_tac 1);
qed "def_gfp_adm_nonP";
-Goalw [adm_def]
+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";
--- a/src/HOLCF/FOCUS/Stream_adm.thy Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Tue Sep 06 21:51:17 2005 +0200
@@ -1,28 +1,29 @@
-(* Title: HOLCF/ex/Stream_adm.thy
+(* Title: HOLCF/ex/Stream_adm.thy
ID: $Id$
- Author: David von Oheimb, TU Muenchen
-
-Admissibility for streams
+ Author: David von Oheimb, TU Muenchen
*)
-Stream_adm = Stream + Continuity +
-
-consts
-
- stream_monoP,
- stream_antiP :: "(('a stream) set \\<Rightarrow> ('a stream) set) \\<Rightarrow> bool"
+header {* Admissibility for streams *}
-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)))"
+theory Stream_adm
+imports Stream Continuity
+begin
constdefs
+
+ stream_monoP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
+ "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 :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
+ "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)))"
+
antitonP :: "'a set => bool"
- "antitonP P \\<equiv> \\<forall>x y. x \\<sqsubseteq> y \\<longrightarrow> y\\<in>P \\<longrightarrow> x\\<in>P"
-
+ "antitonP P \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end