--- a/src/HOLCF/FOCUS/Buffer.ML Thu Jun 01 23:09:34 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,264 +0,0 @@
-(* Title: HOLCF/FOCUS/Buffer.ML
- ID: $Id$
- Author: David von Oheimb, TU Muenchen
-*)
-
-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 (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;
-
-
-(**** BufEq *******************************************************************)
-
-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 (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;
-
-
-(**** BufAC_Asm ***************************************************************)
-
-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 (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]);
-
-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 (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 (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]);
-
-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 (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 (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]);
-
-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 (induct_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 (thms "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 (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 *)
-
-
-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));
--- a/src/HOLCF/FOCUS/Buffer.thy Thu Jun 01 23:09:34 2006 +0200
+++ b/src/HOLCF/FOCUS/Buffer.thy Thu Jun 01 23:53:29 2006 +0200
@@ -84,4 +84,292 @@
ML {* use_legacy_bindings (the_context ()) *}
+lemma set_cong: "!!X. A = B ==> (x:A) = (x:B)"
+by (erule subst, rule refl)
+
+ML {*
+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;
+*}
+
+(**** BufEq *******************************************************************)
+
+lemma mono_BufEq_F: "mono BufEq_F"
+by (unfold mono_def BufEq_F_def, fast)
+
+lemmas BufEq_fix = mono_BufEq_F [THEN BufEq_def [THEN def_gfp_unfold]];
+
+lemma BufEq_unfold: "(f:BufEq) = (!d. f\<cdot>(Md d\<leadsto><>) = <> &
+ (!x. ? ff:BufEq. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>(ff\<cdot>x)))"
+apply (subst BufEq_fix [THEN set_cong])
+apply (unfold BufEq_F_def)
+apply (simp)
+done
+
+lemma Buf_f_empty: "f:BufEq \<Longrightarrow> f\<cdot><> = <>"
+by (drule BufEq_unfold [THEN iffD1], auto)
+
+lemma Buf_f_d: "f:BufEq \<Longrightarrow> f\<cdot>(Md d\<leadsto><>) = <>"
+by (drule BufEq_unfold [THEN iffD1], auto)
+
+lemma Buf_f_d_req:
+ "f:BufEq \<Longrightarrow> \<exists>ff. ff:BufEq \<and> f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x"
+by (drule BufEq_unfold [THEN iffD1], auto)
+
+
+(**** BufAC_Asm ***************************************************************)
+
+lemma mono_BufAC_Asm_F: "mono BufAC_Asm_F"
+by (unfold mono_def BufAC_Asm_F_def, fast)
+
+lemmas BufAC_Asm_fix = mono_BufAC_Asm_F [THEN BufAC_Asm_def [THEN def_gfp_unfold]]
+
+lemma BufAC_Asm_unfold: "(s:BufAC_Asm) = (s = <> | (? d x.
+ s = Md d\<leadsto>x & (x = <> | (ft\<cdot>x = Def \<bullet> & (rt\<cdot>x):BufAC_Asm))))"
+apply (subst BufAC_Asm_fix [THEN set_cong])
+apply (unfold BufAC_Asm_F_def)
+apply (simp)
+done
+
+lemma BufAC_Asm_empty: "<> :BufAC_Asm"
+by (rule BufAC_Asm_unfold [THEN iffD2], auto)
+
+lemma BufAC_Asm_d: "Md d\<leadsto><>:BufAC_Asm"
+by (rule BufAC_Asm_unfold [THEN iffD2], auto)
+lemma BufAC_Asm_d_req: "x:BufAC_Asm ==> Md d\<leadsto>\<bullet>\<leadsto>x:BufAC_Asm"
+by (rule BufAC_Asm_unfold [THEN iffD2], auto)
+lemma BufAC_Asm_prefix2: "a\<leadsto>b\<leadsto>s:BufAC_Asm ==> s:BufAC_Asm"
+by (drule BufAC_Asm_unfold [THEN iffD1], auto)
+
+
+(**** BBufAC_Cmt **************************************************************)
+
+lemma mono_BufAC_Cmt_F: "mono BufAC_Cmt_F"
+by (unfold mono_def BufAC_Cmt_F_def, fast)
+
+lemmas BufAC_Cmt_fix = mono_BufAC_Cmt_F [THEN BufAC_Cmt_def [THEN def_gfp_unfold]]
+
+lemma BufAC_Cmt_unfold: "((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))"
+apply (subst BufAC_Cmt_fix [THEN set_cong])
+apply (unfold BufAC_Cmt_F_def)
+apply (simp)
+done
+
+lemma BufAC_Cmt_empty: "f:BufEq ==> (<>, f\<cdot><>):BufAC_Cmt"
+by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_empty)
+
+lemma BufAC_Cmt_d: "f:BufEq ==> (a\<leadsto>\<bottom>, f\<cdot>(a\<leadsto>\<bottom>)):BufAC_Cmt"
+by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_d)
+
+lemma BufAC_Cmt_d2:
+ "(Md d\<leadsto>\<bottom>, f\<cdot>(Md d\<leadsto>\<bottom>)):BufAC_Cmt ==> f\<cdot>(Md d\<leadsto>\<bottom>) = \<bottom>"
+by (drule BufAC_Cmt_unfold [THEN iffD1], auto)
+
+lemma BufAC_Cmt_d3:
+"(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"
+by (drule BufAC_Cmt_unfold [THEN iffD1], auto)
+
+lemma BufAC_Cmt_d32:
+"(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"
+by (drule BufAC_Cmt_unfold [THEN iffD1], auto)
+
+(**** BufAC *******************************************************************)
+
+lemma BufAC_f_d: "f \<in> BufAC \<Longrightarrow> f\<cdot>(Md d\<leadsto>\<bottom>) = \<bottom>"
+apply (unfold BufAC_def)
+apply (fast intro: BufAC_Cmt_d2 BufAC_Asm_d)
+done
+
+lemma ex_elim_lemma: "(? 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
+lemma "(? 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)"*)
+apply safe
+apply ( rule_tac [2] P="(%x. x:B)" in ssubst)
+prefer 3
+apply ( assumption)
+apply ( rule_tac [2] ext_cfun)
+apply ( drule_tac [2] spec)
+apply ( drule_tac [2] f="rt" in cfun_arg_cong)
+prefer 2
+apply ( simp)
+prefer 2
+apply ( simp)
+apply (rule_tac bexI)
+apply auto
+apply (drule spec)
+apply (erule exE)
+apply (erule ssubst)
+apply (simp)
+done
+
+lemma BufAC_f_d_req: "f\<in>BufAC \<Longrightarrow> \<exists>ff\<in>BufAC. \<forall>x. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x"
+apply (unfold BufAC_def)
+apply (rule ex_elim_lemma [THEN iffD2])
+apply safe
+apply (fast intro: BufAC_Cmt_d32 [THEN Def_maximal]
+ monofun_cfun_arg BufAC_Asm_empty [THEN BufAC_Asm_d_req])
+apply (auto intro: BufAC_Cmt_d3 BufAC_Asm_d_req)
+done
+
+
+(**** BufSt *******************************************************************)
+
+lemma mono_BufSt_F: "mono BufSt_F"
+by (unfold mono_def BufSt_F_def, fast)
+
+lemmas BufSt_P_fix = mono_BufSt_F [THEN BufSt_P_def [THEN def_gfp_unfold]]
+
+lemma BufSt_P_unfold: "(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))))"
+apply (subst BufSt_P_fix [THEN set_cong])
+apply (unfold BufSt_F_def)
+apply (simp)
+done
+
+lemma BufSt_P_empty: "h:BufSt_P ==> h s \<cdot> <> = <>"
+by (drule BufSt_P_unfold [THEN iffD1], auto)
+lemma BufSt_P_d: "h:BufSt_P ==> h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x"
+by (drule BufSt_P_unfold [THEN iffD1], auto)
+lemma BufSt_P_d_req: "h:BufSt_P ==> \<exists>hh\<in>BufSt_P.
+ h (Sd d)\<cdot>(\<bullet> \<leadsto>x) = d\<leadsto>(hh \<currency> \<cdot>x)"
+by (drule BufSt_P_unfold [THEN iffD1], auto)
+
+
+(**** Buf_AC_imp_Eq ***********************************************************)
+
+lemma Buf_AC_imp_Eq: "BufAC \<subseteq> BufEq"
+apply (unfold BufEq_def)
+apply (rule gfp_upperbound)
+apply (unfold BufEq_F_def)
+apply safe
+apply (erule BufAC_f_d)
+apply (drule BufAC_f_d_req)
+apply (fast)
+done
+
+
+(**** Buf_Eq_imp_AC by coinduction ********************************************)
+
+lemma BufAC_Asm_cong_lemma [rule_format]: "\<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)"
+apply (induct_tac "n")
+apply (simp)
+apply (intro strip)
+apply (drule BufAC_Asm_unfold [THEN iffD1])
+apply safe
+apply (simp add: Buf_f_empty)
+apply (simp add: Buf_f_d)
+apply (drule ft_eq [THEN iffD1])
+apply (clarsimp)
+apply (drule Buf_f_d_req)+
+apply safe
+apply (erule ssubst)+
+apply (simp (no_asm))
+apply (fast)
+done
+
+lemma BufAC_Asm_cong: "\<lbrakk>f \<in> BufEq; ff \<in> BufEq; s \<in> BufAC_Asm\<rbrakk> \<Longrightarrow> f\<cdot>s = ff\<cdot>s"
+apply (rule stream.take_lemmas)
+apply (erule (2) BufAC_Asm_cong_lemma)
+done
+
+lemma Buf_Eq_imp_AC_lemma: "\<lbrakk>f \<in> BufEq; x \<in> BufAC_Asm\<rbrakk> \<Longrightarrow> (x, f\<cdot>x) \<in> BufAC_Cmt"
+apply (unfold BufAC_Cmt_def)
+apply (rotate_tac)
+apply (erule weak_coinduct_image)
+apply (unfold BufAC_Cmt_F_def)
+apply safe
+apply (erule Buf_f_empty)
+apply (erule Buf_f_d)
+apply (drule Buf_f_d_req)
+apply (clarsimp)
+apply (erule exI)
+apply (drule BufAC_Asm_prefix2)
+apply (frule Buf_f_d_req)
+apply (clarsimp)
+apply (erule ssubst)
+apply (simp)
+apply (drule (2) BufAC_Asm_cong)
+apply (erule subst)
+apply (erule imageI)
+done
+lemma Buf_Eq_imp_AC: "BufEq \<subseteq> BufAC"
+apply (unfold BufAC_def)
+apply (clarify)
+apply (erule (1) Buf_Eq_imp_AC_lemma)
+done
+
+(**** Buf_Eq_eq_AC ************************************************************)
+
+lemmas Buf_Eq_eq_AC = Buf_AC_imp_Eq [THEN Buf_Eq_imp_AC [THEN subset_antisym]]
+
+
+(**** alternative (not strictly) stronger version of Buf_Eq *******************)
+
+lemma Buf_Eq_alt_imp_Eq: "BufEq_alt \<subseteq> BufEq"
+apply (unfold BufEq_def BufEq_alt_def)
+apply (rule gfp_mono)
+apply (unfold BufEq_F_def)
+apply (fast)
+done
+
+(* direct proof of "BufEq \<subseteq> BufEq_alt" seems impossible *)
+
+
+lemma Buf_AC_imp_Eq_alt: "BufAC <= BufEq_alt"
+apply (unfold BufEq_alt_def)
+apply (rule gfp_upperbound)
+apply (fast elim: BufAC_f_d BufAC_f_d_req)
+done
+
+lemmas Buf_Eq_imp_Eq_alt = subset_trans [OF Buf_Eq_imp_AC Buf_AC_imp_Eq_alt]
+
+lemmas Buf_Eq_alt_eq = subset_antisym [OF Buf_Eq_alt_imp_Eq Buf_Eq_imp_Eq_alt]
+
+
+(**** Buf_Eq_eq_St ************************************************************)
+
+lemma Buf_St_imp_Eq: "BufSt <= BufEq"
+apply (unfold BufSt_def BufEq_def)
+apply (rule gfp_upperbound)
+apply (unfold BufEq_F_def)
+apply safe
+apply ( simp add: BufSt_P_d BufSt_P_empty)
+apply (simp add: BufSt_P_d)
+apply (drule BufSt_P_d_req)
+apply (force)
+done
+
+lemma Buf_Eq_imp_St: "BufEq <= BufSt"
+apply (unfold BufSt_def BufSt_P_def)
+apply safe
+apply (rename_tac f)
+apply (rule_tac x="\<lambda>s. case s of Sd d => \<Lambda> x. f\<cdot>(Md d\<leadsto>x)| \<currency> => f" in bexI)
+apply ( simp)
+apply (erule weak_coinduct_image)
+apply (unfold BufSt_F_def)
+apply (simp)
+apply safe
+apply ( rename_tac "s")
+apply ( induct_tac "s")
+apply ( simp add: Buf_f_d)
+apply ( simp add: Buf_f_empty)
+apply ( simp)
+apply (simp)
+apply (rename_tac f d x)
+apply (drule_tac d="d" and x="x" in Buf_f_d_req)
+apply auto
+done
+
+lemmas Buf_Eq_eq_St = Buf_St_imp_Eq [THEN Buf_Eq_imp_St [THEN subset_antisym]]
+
end
--- a/src/HOLCF/FOCUS/Buffer_adm.ML Thu Jun 01 23:09:34 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,277 +0,0 @@
-(* Title: HOLCF/FOCUS/Buffer_adm.ML
- ID: $Id$
- Author: David von Oheimb, TU Muenchen
-*)
-
-infixr 0 y;
-fun _ y t = by t;
-val b=9999;
-
-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
- "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 (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]);
-
-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 (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())]);
-
-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 ***********************************************************)
-
-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","Suc (Suc 0)")] exI 1);
-by (Clarsimp_tac 1);
-qed "BufAC_Asm_F_stream_monoP";
-
-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]);
-
-
-(**** 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","Suc (Suc 0)")] exI 1;
-b y rtac conjI 1;
-b y strip_tac 2;
-b y dtac (thm "slen_mono") 2;
-b y datac (thm "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 (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())]);
-
-(*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. 2*i")] exI 1);
-by (rtac allI 1);
-by (induct_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 contrapos_np 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 contrapos_np 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;
-by (rtac 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 contrapos_np 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'";
--- a/src/HOLCF/FOCUS/Buffer_adm.thy Thu Jun 01 23:09:34 2006 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy Thu Jun 01 23:53:29 2006 +0200
@@ -9,6 +9,293 @@
imports Buffer Stream_adm
begin
+declare Fin_0 [simp]
+
+lemma BufAC_Asm_d2: "a\<leadsto>s:BufAC_Asm ==> ? d. a=Md d"
+by (drule BufAC_Asm_unfold [THEN iffD1], auto)
+
+lemma BufAC_Asm_d3:
+ "a\<leadsto>b\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\<bullet> & s:BufAC_Asm"
+by (drule BufAC_Asm_unfold [THEN iffD1], auto)
+
+lemma BufAC_Asm_F_def3:
+ "(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))"
+by (unfold BufAC_Asm_F_def, auto)
+
+lemma cont_BufAC_Asm_F: "down_cont BufAC_Asm_F"
+by (auto simp add: down_cont_def BufAC_Asm_F_def3)
+
+lemma BufAC_Cmt_F_def3:
+ "((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))"
+apply (unfold BufAC_Cmt_F_def)
+apply (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)")
+apply (simp)
+apply (auto intro: surjectiv_scons [symmetric])
+done
+
+lemma cont_BufAC_Cmt_F: "down_cont BufAC_Cmt_F"
+by (auto simp add: down_cont_def BufAC_Cmt_F_def3)
+
+
+(**** adm_BufAC_Asm ***********************************************************)
+
+lemma BufAC_Asm_F_stream_monoP: "stream_monoP BufAC_Asm_F"
+apply (unfold BufAC_Asm_F_def stream_monoP_def)
+apply (rule_tac x="{x. (? d. x = Md d\<leadsto>\<bullet>\<leadsto><>)}" in exI)
+apply (rule_tac x="Suc (Suc 0)" in exI)
+apply (clarsimp)
+done
+
+lemma adm_BufAC_Asm: "adm (%x. x:BufAC_Asm)"
+apply (unfold BufAC_Asm_def)
+apply (rule cont_BufAC_Asm_F [THEN BufAC_Asm_F_stream_monoP [THEN fstream_gfp_admI]])
+done
+
+
+(**** adm_non_BufAC_Asm *******************************************************)
+
+lemma BufAC_Asm_F_stream_antiP: "stream_antiP BufAC_Asm_F"
+apply (unfold stream_antiP_def BufAC_Asm_F_def)
+apply (intro strip)
+apply (rule_tac x="{x. (? d. x = Md d\<leadsto>\<bullet>\<leadsto><>)}" in exI)
+apply (rule_tac x="Suc (Suc 0)" in exI)
+apply (rule conjI)
+prefer 2
+apply ( intro strip)
+apply ( drule slen_mono)
+apply ( drule (1) ile_trans)
+apply (force)+
+done
+
+lemma adm_non_BufAC_Asm: "adm (%u. u~:BufAC_Asm)"
+apply (unfold BufAC_Asm_def)
+apply (rule cont_BufAC_Asm_F [THEN BufAC_Asm_F_stream_antiP [THEN fstream_non_gfp_admI]])
+done
+
+(**** adm_BufAC ***************************************************************)
+
+(*adm_non_BufAC_Asm*)
+lemma BufAC_Asm_cong [rule_format]: "!f ff. f:BufEq --> ff:BufEq --> s:BufAC_Asm --> f\<cdot>s = ff\<cdot>s"
+apply (rule fstream_ind2)
+apply (simp add: adm_non_BufAC_Asm)
+apply (force dest: Buf_f_empty)
+apply (force dest!: BufAC_Asm_d2
+ dest: Buf_f_d elim: ssubst)
+apply (safe dest!: BufAC_Asm_d3)
+apply (drule Buf_f_d_req)+
+apply (fast elim: ssubst)
+done
+
+(*adm_non_BufAC_Asm,BufAC_Asm_cong*)
+lemma BufAC_Cmt_d_req:
+"!!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"
+apply (rule BufAC_Cmt_unfold [THEN iffD2])
+apply (intro strip)
+apply (frule Buf_f_d_req)
+apply (auto elim: BufAC_Asm_cong [THEN subst])
+done
+
+(*adm_BufAC_Asm*)
+lemma BufAC_Asm_antiton: "antitonP BufAC_Asm"
+apply (rule antitonPI)
+apply (rule allI)
+apply (rule fstream_ind2)
+apply ( rule adm_lemmas)+
+apply ( rule cont_id)
+apply ( rule adm_BufAC_Asm)
+apply ( safe)
+apply ( rule BufAC_Asm_empty)
+apply ( force dest!: fstream_prefix
+ dest: BufAC_Asm_d2 intro: BufAC_Asm_d)
+apply ( force dest!: fstream_prefix
+ dest: BufAC_Asm_d3 intro!: BufAC_Asm_d_req)
+done
+
+(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
+lemma BufAC_Cmt_2stream_monoP: "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"
+apply (rule_tac x="%i. 2*i" in exI)
+apply (rule allI)
+apply (induct_tac "i")
+apply ( simp)
+apply (simp add: add_commute)
+apply (intro strip)
+apply (subst BufAC_Cmt_F_def3)
+apply (drule_tac P="%x. x" in BufAC_Cmt_F_def3 [THEN subst])
+apply safe
+apply ( erule Buf_f_empty)
+apply ( erule Buf_f_d)
+apply ( drule Buf_f_d_req)
+apply ( safe, erule ssubst, simp)
+apply clarsimp
+apply (rename_tac i d xa ya t)
+(*
+ 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
+*)
+apply (rotate_tac 2)
+apply (drule BufAC_Asm_prefix2)
+apply (frule Buf_f_d_req, erule exE, erule conjE, rotate_tac -1, erule ssubst)
+apply (frule Buf_f_d_req, erule exE, erule conjE)
+apply ( subgoal_tac "f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya")
+prefer 2
+apply ( assumption)
+apply ( rotate_tac -1)
+apply ( simp)
+apply (erule subst)
+(*
+ 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
+*)
+apply (drule spec, drule spec, drule (1) mp)
+apply (drule (1) mp)
+apply (drule (1) mp)
+apply (erule impE)
+apply ( subst BufAC_Asm_cong, assumption)
+prefer 3 apply assumption
+apply assumption
+apply ( erule (1) BufAC_Asm_antiton [THEN antitonPD])
+apply (subst BufAC_Asm_cong, assumption)
+prefer 3 apply assumption
+apply assumption
+apply assumption
+done
+
+lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>down_iterate BufAC_Cmt_F n)"
+apply (unfold BufAC_Cmt_def)
+apply (subst cont_BufAC_Cmt_F [THEN INTER_down_iterate_is_gfp])
+apply (fast)
+done
+
+(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
+ BufAC_Cmt_2stream_monoP*)
+lemma adm_BufAC: "f:BufEq ==> adm (%s. s:BufAC_Asm --> (s, f\<cdot>s):BufAC_Cmt)"
+apply (rule flatstream_admI)
+apply (subst BufAC_Cmt_iterate_all)
+apply (drule BufAC_Cmt_2stream_monoP)
+apply safe
+apply (drule spec, erule exE)
+apply (drule spec, erule impE)
+apply (erule BufAC_Asm_antiton [THEN antitonPD])
+apply (erule is_ub_thelub)
+apply (tactic "smp_tac 3 1")
+apply (drule is_ub_thelub)
+apply (drule (1) mp)
+apply (drule (1) mp)
+apply (erule mp)
+apply (drule BufAC_Cmt_iterate_all [THEN iffD1])
+apply (erule spec)
+done
+
+
+
+(**** 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*)
+lemma Buf_Eq_imp_AC: "BufEq <= BufAC"
+apply (unfold BufAC_def)
+apply (rule subsetI)
+apply (simp)
+apply (rule allI)
+apply (rule fstream_ind2)
+back
+apply ( erule adm_BufAC)
+apply ( safe)
+apply ( erule BufAC_Cmt_empty)
+apply ( erule BufAC_Cmt_d)
+apply ( drule BufAC_Asm_prefix2)
+apply ( simp)
+apply (fast intro: BufAC_Cmt_d_req BufAC_Asm_prefix2)
+done
+
+(**** new approach for admissibility, reduces itself to absurdity *************)
+
+lemma adm_BufAC_Asm: "adm (\<lambda>x. x\<in>BufAC_Asm)"
+apply (rule def_gfp_admI)
+apply (rule BufAC_Asm_def)
+apply (safe)
+apply (unfold BufAC_Asm_F_def)
+apply (safe)
+apply (erule contrapos_np)
+apply (drule fstream_exhaust_eq [THEN iffD1])
+apply (clarsimp)
+apply (drule (1) fstream_lub_lemma)
+apply (clarify)
+apply (erule_tac x="j" in all_dupE)
+apply (simp)
+apply (drule BufAC_Asm_d2)
+apply (clarify)
+apply (simp)
+apply (rule disjCI)
+apply (erule contrapos_np)
+apply (drule fstream_exhaust_eq [THEN iffD1])
+apply (clarsimp)
+apply (drule (1) fstream_lub_lemma)
+apply (clarsimp)
+apply (tactic "simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1")
+apply (rule_tac x="Xa" in exI)
+apply (rule allI)
+apply (rotate_tac -1)
+apply (erule_tac x="i" in allE)
+apply (clarsimp)
+apply (erule_tac x="jb" in allE)
+apply (clarsimp)
+apply (erule_tac x="jc" in allE)
+apply (clarsimp dest!: BufAC_Asm_d3)
+done
+
+lemma adm_non_BufAC_Asm': "adm (\<lambda>u. u \<notin> BufAC_Asm)" (* uses antitonP *)
+apply (rule def_gfp_adm_nonP)
+apply (rule BufAC_Asm_def)
+apply (unfold BufAC_Asm_F_def)
+apply (safe)
+apply (erule contrapos_np)
+apply (drule fstream_exhaust_eq [THEN iffD1])
+apply (clarsimp)
+apply (frule fstream_prefix)
+apply (clarsimp)
+apply (frule BufAC_Asm_d2)
+apply (clarsimp)
+apply (rotate_tac -1)
+apply (erule contrapos_pp)
+apply (drule fstream_exhaust_eq [THEN iffD1])
+apply (clarsimp)
+apply (frule fstream_prefix)
+apply (clarsimp)
+apply (frule BufAC_Asm_d3)
+apply (force)
+done
+
+lemma adm_BufAC': "f \<in> BufEq \<Longrightarrow> adm (\<lambda>u. u \<in> BufAC_Asm \<longrightarrow> (u, f\<cdot>u) \<in> BufAC_Cmt)"
+apply (rule triv_admI)
+apply (clarify)
+apply (erule (1) Buf_Eq_imp_AC_lemma)
+ (* this is what we originally aimed to show, using admissibilty :-( *)
+done
+
end
--- a/src/HOLCF/FOCUS/FOCUS.ML Thu Jun 01 23:09:34 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: HOLCF/FOCUS/FOCUS.ML
- ID: $Id$
- Author: David von Oheimb, TU Muenchen
-*)
-
-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];
-Goal "(#x ~= 0) = (? a y. x = a~> y)";
-by (simp_tac (simpset() addsimps [thm "slen_empty_eq", fstream_exhaust_eq]) 1);
-qed "fstream_exhaust_slen_eq";
-
-Addsimps[thm "slen_less_1_eq", fstream_exhaust_slen_eq,
- thm "slen_fscons_eq", thm "slen_fscons_less_eq"];
-Addsimps[thm "Suc_ile_eq"];
-AddEs [strictI];
--- a/src/HOLCF/FOCUS/FOCUS.thy Thu Jun 01 23:09:34 2006 +0200
+++ b/src/HOLCF/FOCUS/FOCUS.thy Thu Jun 01 23:53:29 2006 +0200
@@ -9,4 +9,22 @@
imports Fstream
begin
+lemma ex_eqI [intro!]: "? xx. x = xx"
+by auto
+
+lemma ex2_eqI [intro!]: "? xx yy. x = xx & y = yy"
+by auto
+
+lemma eq_UU_symf: "(UU = f x) = (f x = UU)"
+by auto
+
+lemma fstream_exhaust_slen_eq: "(#x ~= 0) = (? a y. x = a~> y)"
+by (simp add: slen_empty_eq fstream_exhaust_eq)
+
+lemmas [simp] =
+ slen_less_1_eq fstream_exhaust_slen_eq
+ slen_fscons_eq slen_fscons_less_eq Suc_ile_eq
+
+declare strictI [elim]
+
end
--- a/src/HOLCF/FOCUS/Fstream.ML Thu Jun 01 23:09:34 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,237 +0,0 @@
-(* Title: HOLCF/FOCUS/Fstream.ML
- ID: $Id$
- Author: David von Oheimb, TU Muenchen
-*)
-
-Addsimps[eq_UU_iff RS sym];
-
-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" (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" (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]);
-
-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" (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" (the_context ()) "a~> s ~= <>" (fn _ => [
- stac fscons_def2 1,
- Simp_tac 1]);
-Addsimps[fscons_not_empty];
-
-
-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" (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'" (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 contrapos_np),
- 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 (thms "stream.sel_rews"));
-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" (the_context ()) [fscons_def] "rt\\<cdot>(m~> s) = s" (fn _ => [
- (Simp_tac 1)]);
-Addsimps[rt_fscons];
-
-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)";
-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" (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" (the_context ()) [fscons_def] "#(m~> s) = iSuc (#s)" (fn _ => [
- (Simp_tac 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" (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 contrapos_np 1,
- fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 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" (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" (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]);
-
-
-(* ------------------------------------------------------------------------- *)
-
-section "fsfilter";
-
-qed_goalw "fsfilter_empty" (the_context ()) [fsfilter_def] "A(C)UU = UU" (fn _ => [
- rtac (thm "sfilter_empty") 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" (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" (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" (the_context ()) "{a}(C)a~> x = a~> ({a}(C)x)" (fn _=> [
- rtac fsfilter_insert 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);
-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";
--- a/src/HOLCF/FOCUS/Fstream.thy Thu Jun 01 23:09:34 2006 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy Thu Jun 01 23:53:29 2006 +0200
@@ -46,4 +46,235 @@
ML {* use_legacy_bindings (the_context ()) *}
+lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
+apply (rule flat_eq [THEN iffD1, symmetric])
+apply (rule Def_not_UU)
+apply (drule antisym_less_inverse)
+apply (erule (1) conjunct2 [THEN trans_less])
+done
+
+
+section "fscons"
+
+lemma fscons_def2: "a~>s = Def a && s"
+apply (unfold fscons_def)
+apply (simp)
+done
+
+lemma fstream_exhaust: "x = UU | (? a y. x = a~> y)"
+apply (simp add: fscons_def2)
+apply (cut_tac stream.exhaust)
+apply (fast dest: not_Undef_is_Def [THEN iffD1])
+done
+
+lemma fstream_cases: "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P"
+apply (cut_tac fstream_exhaust)
+apply (erule disjE)
+apply fast
+apply fast
+done
+(*
+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);
+*)
+lemma fstream_exhaust_eq: "(x ~= UU) = (? a y. x = a~> y)"
+apply (simp add: fscons_def2 stream_exhaust_eq)
+apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
+done
+
+
+lemma fscons_not_empty [simp]: "a~> s ~= <>"
+by (simp add: fscons_def2)
+
+
+lemma fscons_inject [simp]: "(a~> s = b~> t) = (a = b & s = t)"
+by (simp add: fscons_def2)
+
+lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt & s << tt"
+apply (rule_tac x="t" in stream.casedist)
+apply (cut_tac fscons_not_empty)
+apply (fast dest: eq_UU_iff [THEN iffD2])
+apply (simp add: fscons_def2)
+apply (drule stream_flat_prefix)
+apply (rule Def_not_UU)
+apply (fast)
+done
+
+lemma fstream_prefix' [simp]:
+ "x << a~> z = (x = <> | (? y. x = a~> y & y << z))"
+apply (simp add: fscons_def2 Def_not_UU [THEN stream_prefix'])
+apply (safe)
+apply (erule_tac [!] contrapos_np)
+prefer 2 apply (fast elim: DefE)
+apply (rule Lift_cases)
+apply (erule (1) notE)
+apply (safe)
+apply (drule Def_inject_less_eq [THEN iffD1])
+apply fast
+done
+
+(* ------------------------------------------------------------------------- *)
+
+section "ft & rt"
+
+lemmas ft_empty = stream.sel_rews (1)
+lemma ft_fscons [simp]: "ft\<cdot>(m~> s) = Def m"
+by (simp add: fscons_def)
+
+lemmas rt_empty = stream.sel_rews (2)
+lemma rt_fscons [simp]: "rt\<cdot>(m~> s) = s"
+by (simp add: fscons_def)
+
+lemma ft_eq [simp]: "(ft\<cdot>s = Def a) = (? t. s = a~> t)"
+apply (unfold fscons_def)
+apply (simp)
+apply (safe)
+apply (erule subst)
+apply (rule exI)
+apply (rule surjectiv_scons [symmetric])
+apply (simp)
+done
+
+lemma surjective_fscons_lemma: "(d\<leadsto>y = x) = (ft\<cdot>x = Def d & rt\<cdot>x = y)"
+by auto
+
+lemma surjective_fscons: "ft\<cdot>x = Def d \<Longrightarrow> d\<leadsto>rt\<cdot>x = x"
+by (simp add: surjective_fscons_lemma)
+
+
+(* ------------------------------------------------------------------------- *)
+
+section "take"
+
+lemma fstream_take_Suc [simp]:
+ "stream_take (Suc n)\<cdot>(a~> s) = a~> stream_take n\<cdot>s"
+by (simp add: fscons_def)
+
+
+(* ------------------------------------------------------------------------- *)
+
+section "slen"
+
+(*bind_thm("slen_empty", slen_empty);*)
+
+lemma slen_fscons: "#(m~> s) = iSuc (#s)"
+by (simp add: fscons_def)
+
+lemma slen_fscons_eq:
+ "(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)"
+apply (simp add: fscons_def2 slen_scons_eq)
+apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
+done
+
+lemma slen_fscons_eq_rev:
+ "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))"
+apply (simp add: fscons_def2 slen_scons_eq_rev)
+apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1")
+apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1")
+apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1")
+apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1")
+apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1")
+apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1")
+apply (erule contrapos_np)
+apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
+done
+
+lemma slen_fscons_less_eq:
+ "(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))"
+apply (subst slen_fscons_eq_rev)
+apply (fast dest!: fscons_inject [THEN iffD1])
+done
+
+
+(* ------------------------------------------------------------------------- *)
+
+section "induction"
+
+lemma fstream_ind:
+ "[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x"
+apply (erule stream.ind)
+apply (assumption)
+apply (unfold fscons_def2)
+apply (fast dest: not_Undef_is_Def [THEN iffD1])
+done
+
+lemma fstream_ind2:
+ "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x"
+apply (erule stream_ind2)
+apply (assumption)
+apply (unfold fscons_def2)
+apply (fast dest: not_Undef_is_Def [THEN iffD1])
+apply (fast dest: not_Undef_is_Def [THEN iffD1])
+done
+
+
+(* ------------------------------------------------------------------------- *)
+
+section "fsfilter"
+
+lemma fsfilter_empty: "A(C)UU = UU"
+apply (unfold fsfilter_def)
+apply (rule sfilter_empty)
+done
+
+lemma fsfilter_fscons:
+ "A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)"
+apply (unfold fsfilter_def)
+apply (simp add: fscons_def2 sfilter_scons If_and_if)
+done
+
+lemma fsfilter_emptys: "{}(C)x = UU"
+apply (rule_tac x="x" in fstream_ind)
+apply (simp)
+apply (rule fsfilter_empty)
+apply (simp add: fsfilter_fscons)
+done
+
+lemma fsfilter_insert: "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)"
+by (simp add: fsfilter_fscons)
+
+lemma fsfilter_single_in: "{a}(C)a~> x = a~> ({a}(C)x)"
+by (rule fsfilter_insert)
+
+lemma fsfilter_single_out: "b ~= a ==> {a}(C)b~> x = ({a}(C)x)"
+by (simp add: fsfilter_fscons)
+
+lemma fstream_lub_lemma1:
+ "\<lbrakk>chain Y; lub (range Y) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
+apply (case_tac "max_in_chain i Y")
+apply (drule (1) lub_finch1 [THEN thelubI, THEN sym])
+apply (force)
+apply (unfold max_in_chain_def)
+apply auto
+apply (frule (1) chain_mono3)
+apply (rule_tac x="Y j" in fstream_cases)
+apply (force)
+apply (drule_tac x="j" in is_ub_thelub)
+apply (force)
+done
+
+lemma fstream_lub_lemma:
+ "\<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)"
+apply (frule (1) fstream_lub_lemma1)
+apply (clarsimp)
+apply (rule_tac x="%i. rt\<cdot>(Y(i+j))" in exI)
+apply (rule conjI)
+apply (erule chain_shift [THEN chain_monofun])
+apply safe
+apply (drule_tac x="j" and y="i+j" in chain_mono3)
+apply (simp)
+apply (simp)
+apply (rule_tac x="i+j" in exI)
+apply (drule fstream_prefix)
+apply (clarsimp)
+apply (subst contlub_cfun [symmetric])
+apply (rule chainI)
+apply (fast)
+apply (erule chain_shift)
+apply (subst lub_const [THEN thelubI])
+apply (subst lub_range_shift)
+apply (assumption)
+apply (simp)
+done
+
end
--- a/src/HOLCF/FOCUS/Stream_adm.ML Thu Jun 01 23:09:34 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,178 +0,0 @@
-(* Title: HOLCF/ex/Stream_adm.ML
- ID: $Id$
- Author: David von Oheimb, TU Muenchen
-*)
-
-(* ----------------------------------------------------------------------- *)
-
-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 (thm "chain_incr") 1);
-by ( rtac allI 1);
-by ( dtac spec 1);
-by ( Safe_tac);
-by ( rtac exI 1);
-by ( rtac (thm "slen_strict_mono") 1);
-by ( etac spec 1);
-by ( atac 1);
-by ( atac 1);
-by (dtac (not_ex RS iffD1) 1);
-by (stac (thm "slen_infinite") 1);
-by (etac thin_rl 1);
-by (dtac spec 1);
-by (fold_goals_tac [thm "ile_def"]);
-by (etac (thm "ile_iless_trans" RS (thm "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 (thm "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 (induct_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 (thm "ile_trans") 1);
-by ( etac (thm "slen_mono") 1);
-by (etac ssubst 1);
-by (safe_tac HOL_cs);
-by ( eatac (ile_lemma RS thm "slen_take_lemma3" RS subst) 2 1);
-by (etac allE 1);
-by (etac allE 1);
-by (dtac mp 1);
-by ( etac (thm "slen_rt_mult") 1);
-by (dtac mp 1);
-by (etac (thm "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)";
-by (EVERY [ 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" (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,
- 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]);
-
-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]);
-
-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";
--- a/src/HOLCF/FOCUS/Stream_adm.thy Thu Jun 01 23:09:34 2006 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Thu Jun 01 23:53:29 2006 +0200
@@ -26,4 +26,187 @@
ML {* use_legacy_bindings (the_context ()) *}
+(* ----------------------------------------------------------------------- *)
+
+section "admissibility"
+
+lemma flatstream_adm_lemma:
+ assumes 1: "chain Y"
+ assumes 2: "!i. P (Y i)"
+ assumes 3: "(!!Y. [| chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]
+ ==> P(lub (range Y)))"
+ shows "P(lub (range Y))"
+apply (rule increasing_chain_adm_lemma [OF 1 2])
+apply (erule 3, assumption)
+apply (erule thin_rl)
+apply (rule allI)
+apply (case_tac "!j. stream_finite (Y j)")
+apply ( rule chain_incr)
+apply ( rule allI)
+apply ( drule spec)
+apply ( safe)
+apply ( rule exI)
+apply ( rule slen_strict_mono)
+apply ( erule spec)
+apply ( assumption)
+apply ( assumption)
+apply (drule not_ex [THEN iffD1])
+apply (subst slen_infinite)
+apply (erule thin_rl)
+apply (drule spec)
+apply (fold ile_def)
+apply (erule ile_iless_trans [THEN Infty_eq [THEN iffD1]])
+apply (simp)
+done
+
+
+(* should be without reference to stream length? *)
+lemma flatstream_admI: "[|(!!Y. [| chain Y; !i. P (Y i);
+ !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(lub (range Y)))|]==> adm P"
+apply (unfold adm_def)
+apply (intro strip)
+apply (erule (1) flatstream_adm_lemma)
+apply (fast)
+done
+
+
+(* context (theory "Nat_InFinity");*)
+lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x"
+apply (rule ile_trans)
+prefer 2
+apply (assumption)
+apply (simp)
+done
+
+lemma stream_monoP2I:
+"!!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"
+apply (unfold stream_monoP_def)
+apply (safe)
+apply (rule_tac x="i*ia" in exI)
+apply (induct_tac "ia")
+apply ( simp)
+apply (simp)
+apply (intro strip)
+apply (erule allE, erule all_dupE, drule mp, erule ile_lemma)
+apply (drule_tac P="%x. x" in subst, assumption)
+apply (erule allE, drule mp, rule ile_lemma) back
+apply ( erule ile_trans)
+apply ( erule slen_mono)
+apply (erule ssubst)
+apply (safe)
+apply ( erule (2) ile_lemma [THEN slen_take_lemma3, THEN subst])
+apply (erule allE)
+apply (drule mp)
+apply ( erule slen_rt_mult)
+apply (erule allE)
+apply (drule mp)
+apply (erule monofun_rt_mult)
+apply (drule (1) mp)
+apply (assumption)
+done
+
+lemma stream_monoP2_gfp_admI: "[| !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)"
+apply (erule INTER_down_iterate_is_gfp [THEN ssubst]) (* cont *)
+apply (simp (no_asm))
+apply (rule adm_lemmas)
+apply (rule flatstream_admI)
+apply (erule allE)
+apply (erule exE)
+apply (erule allE, erule exE)
+apply (erule allE, erule allE, drule mp) (* stream_monoP *)
+apply ( drule ileI1)
+apply ( drule ile_trans)
+apply ( rule ile_iSuc)
+apply ( drule iSuc_ile_mono [THEN iffD1])
+apply ( assumption)
+apply (drule mp)
+apply ( erule is_ub_thelub)
+apply (fast)
+done
+
+lemmas fstream_gfp_admI = stream_monoP2I [THEN stream_monoP2_gfp_admI]
+
+lemma stream_antiP2I:
+"!!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"
+apply (unfold stream_antiP_def)
+apply (rule allI)
+apply (induct_tac "i")
+apply ( simp)
+apply (simp)
+apply (intro strip)
+apply (erule allE, erule all_dupE, erule exE, erule exE)
+apply (erule conjE)
+apply (case_tac "#x < Fin i")
+apply ( fast)
+apply (fold ile_def)
+apply (drule (1) mp)
+apply (erule all_dupE, drule mp, rule refl_less)
+apply (erule ssubst)
+apply (erule allE, drule (1) mp)
+apply (drule_tac P="%x. x" in subst, assumption)
+apply (erule conjE, rule conjI)
+apply ( erule slen_take_lemma3 [THEN ssubst], assumption)
+apply ( assumption)
+apply (erule allE, erule allE, drule mp, erule monofun_rt_mult)
+apply (drule (1) mp)
+apply (assumption)
+done
+
+lemma stream_antiP2_non_gfp_admI:
+"!!X. [|!i x y. x << y --> y:down_iterate F i --> x:down_iterate F i; down_cont F |]
+ ==> adm (%u. ~ u:gfp F)"
+apply (unfold adm_def)
+apply (simp add: INTER_down_iterate_is_gfp)
+apply (fast dest!: is_ub_thelub)
+done
+
+lemmas fstream_non_gfp_admI = stream_antiP2I [THEN stream_antiP2_non_gfp_admI]
+
+
+
+(**new approach for adm********************************************************)
+
+section "antitonP"
+
+lemma antitonPD: "[| antitonP P; y:P; x<<y |] ==> x:P"
+apply (unfold antitonP_def)
+apply auto
+done
+
+lemma antitonPI: "!x y. y:P --> x<<y --> x:P ==> antitonP P"
+apply (unfold antitonP_def)
+apply (fast)
+done
+
+lemma antitonP_adm_non_P: "antitonP P ==> adm (%u. u~:P)"
+apply (unfold adm_def)
+apply (auto dest: antitonPD elim: is_ub_thelub)
+done
+
+lemma def_gfp_adm_nonP: "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)"
+apply (simp)
+apply (rule antitonP_adm_non_P)
+apply (rule antitonPI)
+apply (drule gfp_upperbound)
+apply (fast)
+done
+
+lemma adm_set:
+"{lub (range Y) |Y. chain Y & (\<forall>i. Y i \<in> P)} \<subseteq> P \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
+apply (unfold adm_def)
+apply (fast)
+done
+
+lemma def_gfp_admI: "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)"
+apply (simp)
+apply (rule adm_set)
+apply (erule gfp_upperbound)
+done
+
end
--- a/src/HOLCF/IsaMakefile Thu Jun 01 23:09:34 2006 +0200
+++ b/src/HOLCF/IsaMakefile Thu Jun 01 23:53:29 2006 +0200
@@ -63,10 +63,9 @@
HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstreams.thy \
- 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
+ FOCUS/Fstream.thy FOCUS/FOCUS.thy \
+ FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \
+ FOCUS/Buffer.thy FOCUS/Buffer_adm.thy
@$(ISATOOL) usedir $(OUT)/HOLCF FOCUS
## IOA