(* Title: HOL/HOLCF/FOCUS/Buffer.thy
Author: David von Oheimb, TU Muenchen
Formalization of section 4 of
@inproceedings {broy_mod94,
author = {Manfred Broy},
title = {{Specification and Refinement of a Buffer of Length One}},
booktitle = {Deductive Program Design},
year = {1994},
editor = {Manfred Broy},
volume = {152},
series = {ASI Series, Series F: Computer and System Sciences},
pages = {273 -- 304},
publisher = {Springer}
}
Slides available from http://ddvo.net/talks/1-Buffer.ps.gz
*)
theory Buffer
imports FOCUS
begin
typedecl D
datatype
M = Md D | Mreq ("\")
datatype
State = Sd D | Snil ("\")
type_synonym
SPF11 = "M fstream \ D fstream"
type_synonym
SPEC11 = "SPF11 set"
type_synonym
SPSF11 = "State \ SPF11"
type_synonym
SPECS11 = "SPSF11 set"
definition
BufEq_F :: "SPEC11 \ SPEC11" where
"BufEq_F B = {f. \d. f\(Md d\<>) = <> \
(\<forall>x. \<exists>ff\<in>B. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x)}"
definition
BufEq :: "SPEC11" where
"BufEq = gfp BufEq_F"
definition
BufEq_alt :: "SPEC11" where
"BufEq_alt = gfp (\B. {f. \d. f\(Md d\<> ) = <> \
(\<exists>ff\<in>B. (\<forall>x. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x))})"
definition
BufAC_Asm_F :: " (M fstream set) \ (M fstream set)" where
"BufAC_Asm_F A = {s. s = <> \
(\<exists>d x. s = Md d\<leadsto>x \<and> (x = <> \<or> (ft\<cdot>x = Def \<bullet> \<and> (rt\<cdot>x)\<in>A)))}"
definition
BufAC_Asm :: " (M fstream set)" where
"BufAC_Asm = gfp BufAC_Asm_F"
definition
BufAC_Cmt_F :: "((M fstream * D fstream) set) \
((M fstream * D fstream) set)" where
"BufAC_Cmt_F C = {(s,t). \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))}"
definition
BufAC_Cmt :: "((M fstream * D fstream) set)" where
"BufAC_Cmt = gfp BufAC_Cmt_F"
definition
BufAC :: "SPEC11" where
"BufAC = {f. \x. x\BufAC_Asm \ (x,f\x)\BufAC_Cmt}"
definition
BufSt_F :: "SPECS11 \ SPECS11" where
"BufSt_F H = {h. \s . h s \<> = <> \
(\<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)))}"
definition
BufSt_P :: "SPECS11" where
"BufSt_P = gfp BufSt_F"
definition
BufSt :: "SPEC11" where
"BufSt = {f. \h\BufSt_P. f = h \}"
lemma set_cong: "\X. A = B \ (x\A) = (x\B)"
by (erule subst, rule refl)
(**** 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 eq_reflection, THEN def_gfp_unfold]]
lemma BufEq_unfold: "(f\BufEq) = (\d. f\(Md d\<>) = <> \
(\<forall>x. \<exists>ff\<in>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 \ f\<> = <>"
by (drule BufEq_unfold [THEN iffD1], auto)
lemma Buf_f_d: "f\BufEq \ f\(Md d\<>) = <>"
by (drule BufEq_unfold [THEN iffD1], auto)
lemma Buf_f_d_req:
"f\BufEq \ \ff. ff\BufEq \ f\(Md d\\\x) = d\ff\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 eq_reflection, THEN def_gfp_unfold]]
lemma BufAC_Asm_unfold: "(s\BufAC_Asm) = (s = <> \ (\d x.
s = Md d\<leadsto>x \<and> (x = <> \<or> (ft\<cdot>x = Def \<bullet> \<and> (rt\<cdot>x)\<in>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\<> \ BufAC_Asm"
by (rule BufAC_Asm_unfold [THEN iffD2], auto)
lemma BufAC_Asm_d_req: "x \ BufAC_Asm \ Md d\\\x \ BufAC_Asm"
by (rule BufAC_Asm_unfold [THEN iffD2], auto)
lemma BufAC_Asm_prefix2: "a\b\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 eq_reflection, THEN def_gfp_unfold]]
lemma BufAC_Cmt_unfold: "((s,t) \ BufAC_Cmt) = (\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> 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\<>) \ BufAC_Cmt"
by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_empty)
lemma BufAC_Cmt_d: "f \ BufEq \ (a\\, f\(a\\)) \ BufAC_Cmt"
by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_d)
lemma BufAC_Cmt_d2:
"(Md d\\, f\(Md d\\)) \ BufAC_Cmt \ f\(Md d\\) = \"
by (drule BufAC_Cmt_unfold [THEN iffD1], auto)
lemma BufAC_Cmt_d3:
"(Md d\\\x, f\(Md d\\\x)) \ BufAC_Cmt \ (x, rt\(f\(Md d\\\x))) \ BufAC_Cmt"
by (drule BufAC_Cmt_unfold [THEN iffD1], auto)
lemma BufAC_Cmt_d32:
"(Md d\\\x, f\(Md d\\\x)) \ BufAC_Cmt \ ft\(f\(Md d\\\x)) = Def d"
by (drule BufAC_Cmt_unfold [THEN iffD1], auto)
(**** BufAC *******************************************************************)
lemma BufAC_f_d: "f \ BufAC \ f\(Md d\\) = \"
apply (unfold BufAC_def)
apply (fast intro: BufAC_Cmt_d2 BufAC_Asm_d)
done
lemma ex_elim_lemma: "(\ff\B. (\x. f\(a\b\x) = d\ff\x)) =
((\<forall>x. ft\<cdot>(f\<cdot>(a\<leadsto>b\<leadsto>x)) = Def d) \<and> (LAM x. rt\<cdot>(f\<cdot>(a\<leadsto>b\<leadsto>x)))\<in>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] cfun_eqI)
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\BufAC \ \ff\BufAC. \x. f\(Md d\\\x) = d\ff\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 eq_reflection, THEN def_gfp_unfold]]
lemma BufSt_P_unfold: "(h\BufSt_P) = (\s. h s\<> = <> \
(\<forall>d x. h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x \<and>
(\<exists>hh\<in>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 \ <> = <>"
by (drule BufSt_P_unfold [THEN iffD1], auto)
lemma BufSt_P_d: "h \ BufSt_P \ h \ \(Md d\x) = h (Sd d)\x"
by (drule BufSt_P_unfold [THEN iffD1], auto)
lemma BufSt_P_d_req: "h \ BufSt_P ==> \hh\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 \ 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]: "\s f ff. f\BufEq \ ff\BufEq \
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: "\f \ BufEq; ff \ BufEq; s \ BufAC_Asm\ \ f\s = ff\s"
apply (rule stream.take_lemma)
apply (erule (2) BufAC_Asm_cong_lemma)
done
lemma Buf_Eq_imp_AC_lemma: "\f \ BufEq; x \ BufAC_Asm\ \ (x, f\x) \ 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 \ 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 \ 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="\s. case s of Sd d => \ x. f\(Md d\x)| \ => 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
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
