# HG changeset patch # User wenzelm # Date 1192976862 -7200 # Node ID 4f8176c940cfb46312a3be410d20884aa86629b1 # Parent 3d4953e8844951e995905f4ca80d79840cf3989f modernized specifications ('definition', 'axiomatization'); diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/Cfun.thy --- a/src/HOLCF/Cfun.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/Cfun.thy Sun Oct 21 16:27:42 2007 +0200 @@ -435,18 +435,18 @@ subsection {* Identity and composition *} -consts - ID :: "'a \ 'a" - cfcomp :: "('b \ 'c) \ ('a \ 'b) \ 'a \ 'c" +definition + ID :: "'a \ 'a" where + "ID = (\ x. x)" + +definition + cfcomp :: "('b \ 'c) \ ('a \ 'b) \ 'a \ 'c" where + oo_def: "cfcomp = (\ f g x. f\(g\x))" abbreviation cfcomp_syn :: "['b \ 'c, 'a \ 'b] \ 'a \ 'c" (infixr "oo" 100) where "f oo g == cfcomp\f\g" -defs - ID_def: "ID \ (\ x. x)" - oo_def: "cfcomp \ (\ f g x. f\(g\x))" - lemma ID1 [simp]: "ID\x = x" by (simp add: ID_def) diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/ABP/Abschannel.thy --- a/src/HOLCF/IOA/ABP/Abschannel.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/ABP/Abschannel.thy Sun Oct 21 16:27:42 2007 +0200 @@ -12,90 +12,79 @@ datatype 'a abs_action = S 'a | R 'a -consts - -ch_asig :: "'a abs_action signature" -ch_trans :: "('a abs_action, 'a list)transition set" -ch_ioa :: "('a abs_action, 'a list)ioa" - -rsch_actions :: "'m action => bool abs_action option" -srch_actions :: "'m action =>(bool * 'm) abs_action option" - -srch_asig :: "'m action signature" -rsch_asig :: "'m action signature" - -srch_trans :: "('m action, 'm packet list)transition set" -rsch_trans :: "('m action, bool list)transition set" - -srch_ioa :: "('m action, 'm packet list)ioa" -rsch_ioa :: "('m action, bool list)ioa" - - -defs - -srch_asig_def: "srch_asig == asig_of(srch_ioa)" -rsch_asig_def: "rsch_asig == asig_of(rsch_ioa)" - -srch_trans_def: "srch_trans == trans_of(srch_ioa)" -rsch_trans_def: "rsch_trans == trans_of(rsch_ioa)" - -srch_ioa_def: "srch_ioa == rename ch_ioa srch_actions" -rsch_ioa_def: "rsch_ioa == rename ch_ioa rsch_actions" - - (********************************************************** G e n e r i c C h a n n e l *********************************************************) -ch_asig_def: "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})" +definition + ch_asig :: "'a abs_action signature" where + "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})" -ch_trans_def: "ch_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in - case fst(snd(tr)) - of S(b) => ((t = s) | (t = s @ [b])) | - R(b) => s ~= [] & - b = hd(s) & - ((t = s) | (t = tl(s))) }" +definition + ch_trans :: "('a abs_action, 'a list)transition set" where + "ch_trans = + {tr. let s = fst(tr); + t = snd(snd(tr)) + in + case fst(snd(tr)) + of S(b) => ((t = s) | (t = s @ [b])) | + R(b) => s ~= [] & + b = hd(s) & + ((t = s) | (t = tl(s)))}" -ch_ioa_def: "ch_ioa == (ch_asig, {[]}, ch_trans,{},{})" +definition + ch_ioa :: "('a abs_action, 'a list)ioa" where + "ch_ioa = (ch_asig, {[]}, ch_trans,{},{})" + (********************************************************** C o n c r e t e C h a n n e l s b y R e n a m i n g *********************************************************) -rsch_actions_def: "rsch_actions (akt) == - case akt of +definition + rsch_actions :: "'m action => bool abs_action option" where + "rsch_actions (akt) = + (case akt of Next => None | S_msg(m) => None | R_msg(m) => None | S_pkt(packet) => None | R_pkt(packet) => None | S_ack(b) => Some(S(b)) | - R_ack(b) => Some(R(b))" + R_ack(b) => Some(R(b)))" -srch_actions_def: "srch_actions (akt) == - case akt of +definition + srch_actions :: "'m action =>(bool * 'm) abs_action option" where + "srch_actions akt = + (case akt of Next => None | S_msg(m) => None | R_msg(m) => None | S_pkt(p) => Some(S(p)) | R_pkt(p) => Some(R(p)) | S_ack(b) => None | - R_ack(b) => None" + R_ack(b) => None)" + +definition + srch_ioa :: "('m action, 'm packet list)ioa" where + "srch_ioa = rename ch_ioa srch_actions" +definition + rsch_ioa :: "('m action, bool list)ioa" where + "rsch_ioa = rename ch_ioa rsch_actions" + +definition + srch_asig :: "'m action signature" where + "srch_asig = asig_of(srch_ioa)" + +definition + rsch_asig :: "'m action signature" where + "rsch_asig = asig_of(rsch_ioa)" + +definition + srch_trans :: "('m action, 'm packet list)transition set" where + "srch_trans = trans_of(srch_ioa)" +definition + rsch_trans :: "('m action, bool list)transition set" where + "rsch_trans = trans_of(rsch_ioa)" end - - - - - - - - - - - - - diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/ABP/Abschannel_finite.thy --- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy Sun Oct 21 16:27:42 2007 +0200 @@ -9,54 +9,54 @@ imports Abschannel IOA Action Lemmas begin -consts - -ch_fin_asig :: "'a abs_action signature" - -ch_fin_trans :: "('a abs_action, 'a list)transition set" - -ch_fin_ioa :: "('a abs_action, 'a list)ioa" - -srch_fin_asig :: "'m action signature" -rsch_fin_asig :: "'m action signature" - -srch_fin_trans :: "('m action, 'm packet list)transition set" -rsch_fin_trans :: "('m action, bool list)transition set" - -srch_fin_ioa :: "('m action, 'm packet list)ioa" -rsch_fin_ioa :: "('m action, bool list)ioa" - -reverse :: "'a list => 'a list" - +consts reverse :: "'a list => 'a list" primrec reverse_Nil: "reverse([]) = []" reverse_Cons: "reverse(x#xs) = reverse(xs)@[x]" -defs - -srch_fin_asig_def: "srch_fin_asig == asig_of(srch_fin_ioa)" -rsch_fin_asig_def: "rsch_fin_asig == asig_of(rsch_fin_ioa)" +definition + ch_fin_asig :: "'a abs_action signature" where + "ch_fin_asig = ch_asig" -srch_fin_trans_def: "srch_fin_trans == trans_of(srch_fin_ioa)" -rsch_fin_trans_def: "rsch_fin_trans == trans_of(rsch_fin_ioa)" +definition + ch_fin_trans :: "('a abs_action, 'a list)transition set" where + "ch_fin_trans = + {tr. let s = fst(tr); + t = snd(snd(tr)) + in + case fst(snd(tr)) + of S(b) => ((t = s) | + (if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) | + R(b) => s ~= [] & + b = hd(s) & + ((t = s) | (t = tl(s)))}" -srch_fin_ioa_def: "srch_fin_ioa == rename ch_fin_ioa srch_actions" -rsch_fin_ioa_def: "rsch_fin_ioa == rename ch_fin_ioa rsch_actions" - +definition + ch_fin_ioa :: "('a abs_action, 'a list)ioa" where + "ch_fin_ioa = (ch_fin_asig, {[]}, ch_fin_trans,{},{})" -ch_fin_asig_def: "ch_fin_asig == ch_asig" +definition + srch_fin_ioa :: "('m action, 'm packet list)ioa" where + "srch_fin_ioa = rename ch_fin_ioa srch_actions" + +definition + rsch_fin_ioa :: "('m action, bool list)ioa" where + "rsch_fin_ioa = rename ch_fin_ioa rsch_actions" + +definition + srch_fin_asig :: "'m action signature" where + "srch_fin_asig = asig_of(srch_fin_ioa)" -ch_fin_trans_def: "ch_fin_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in - case fst(snd(tr)) - of S(b) => ((t = s) | - (if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) | - R(b) => s ~= [] & - b = hd(s) & - ((t = s) | (t = tl(s))) }" +definition + rsch_fin_asig :: "'m action signature" where + "rsch_fin_asig = asig_of(rsch_fin_ioa)" -ch_fin_ioa_def: "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans,{},{})" +definition + srch_fin_trans :: "('m action, 'm packet list)transition set" where + "srch_fin_trans = trans_of(srch_fin_ioa)" + +definition + rsch_fin_trans :: "('m action, bool list)transition set" where + "rsch_fin_trans = trans_of(rsch_fin_ioa)" end diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/ABP/Spec.thy --- a/src/HOLCF/IOA/ABP/Spec.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/ABP/Spec.thy Sun Oct 21 16:27:42 2007 +0200 @@ -9,32 +9,30 @@ imports IOA Action begin -consts - -spec_sig :: "'m action signature" -spec_trans :: "('m action, 'm list)transition set" -spec_ioa :: "('m action, 'm list)ioa" - -defs - -sig_def: "spec_sig == (UN m.{S_msg(m)}, - UN m.{R_msg(m)} Un {Next}, - {})" +definition + spec_sig :: "'m action signature" where + sig_def: "spec_sig = (UN m.{S_msg(m)}, + UN m.{R_msg(m)} Un {Next}, + {})" -trans_def: "spec_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in - case fst(snd(tr)) - of - Next => t=s | (* Note that there is condition as in Sender *) - S_msg(m) => t = s@[m] | - R_msg(m) => s = (m#t) | - S_pkt(pkt) => False | - R_pkt(pkt) => False | - S_ack(b) => False | - R_ack(b) => False}" +definition + spec_trans :: "('m action, 'm list)transition set" where + trans_def: "spec_trans = + {tr. let s = fst(tr); + t = snd(snd(tr)) + in + case fst(snd(tr)) + of + Next => t=s | (* Note that there is condition as in Sender *) + S_msg(m) => t = s@[m] | + R_msg(m) => s = (m#t) | + S_pkt(pkt) => False | + R_pkt(pkt) => False | + S_ack(b) => False | + R_ack(b) => False}" -ioa_def: "spec_ioa == (spec_sig, {[]}, spec_trans)" +definition + spec_ioa :: "('m action, 'm list)ioa" where + ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans)" end diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/ex/TrivEx.thy --- a/src/HOLCF/IOA/ex/TrivEx.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/ex/TrivEx.thy Sun Oct 21 16:27:42 2007 +0200 @@ -11,53 +11,42 @@ datatype action = INC -consts - -C_asig :: "action signature" -C_trans :: "(action, nat)transition set" -C_ioa :: "(action, nat)ioa" - -A_asig :: "action signature" -A_trans :: "(action, bool)transition set" -A_ioa :: "(action, bool)ioa" - -h_abs :: "nat => bool" - -defs - -C_asig_def: - "C_asig == ({},{INC},{})" - -C_trans_def: "C_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - INC => t = Suc(s)}" +definition + C_asig :: "action signature" where + "C_asig = ({},{INC},{})" +definition + C_trans :: "(action, nat)transition set" where + "C_trans = + {tr. let s = fst(tr); + t = snd(snd(tr)) + in case fst(snd(tr)) + of + INC => t = Suc(s)}" +definition + C_ioa :: "(action, nat)ioa" where + "C_ioa = (C_asig, {0}, C_trans,{},{})" -C_ioa_def: "C_ioa == - (C_asig, {0}, C_trans,{},{})" - -A_asig_def: - "A_asig == ({},{INC},{})" +definition + A_asig :: "action signature" where + "A_asig = ({},{INC},{})" +definition + A_trans :: "(action, bool)transition set" where + "A_trans = + {tr. let s = fst(tr); + t = snd(snd(tr)) + in case fst(snd(tr)) + of + INC => t = True}" +definition + A_ioa :: "(action, bool)ioa" where + "A_ioa = (A_asig, {False}, A_trans,{},{})" -A_trans_def: "A_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - INC => t = True}" +definition + h_abs :: "nat => bool" where + "h_abs n = (n~=0)" -A_ioa_def: "A_ioa == - (A_asig, {False}, A_trans,{},{})" - -h_abs_def: - "h_abs n == n~=0" - -axioms - -MC_result: - "validIOA A_ioa (<>[] <%(b,a,c). b>)" +axiomatization where + MC_result: "validIOA A_ioa (<>[] <%(b,a,c). b>)" lemma h_abs_is_abstraction: "is_abstraction h_abs C_ioa A_ioa" diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/ex/TrivEx2.thy --- a/src/HOLCF/IOA/ex/TrivEx2.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/ex/TrivEx2.thy Sun Oct 21 16:27:42 2007 +0200 @@ -11,62 +11,48 @@ datatype action = INC -consts - -C_asig :: "action signature" -C_trans :: "(action, nat)transition set" -C_ioa :: "(action, nat)ioa" -C_live_ioa :: "(action, nat)live_ioa" - -A_asig :: "action signature" -A_trans :: "(action, bool)transition set" -A_ioa :: "(action, bool)ioa" -A_live_ioa :: "(action, bool)live_ioa" - -h_abs :: "nat => bool" - -defs - -C_asig_def: - "C_asig == ({},{INC},{})" - -C_trans_def: "C_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - INC => t = Suc(s)}" +definition + C_asig :: "action signature" where + "C_asig = ({},{INC},{})" +definition + C_trans :: "(action, nat)transition set" where + "C_trans = + {tr. let s = fst(tr); + t = snd(snd(tr)) + in case fst(snd(tr)) + of + INC => t = Suc(s)}" +definition + C_ioa :: "(action, nat)ioa" where + "C_ioa = (C_asig, {0}, C_trans,{},{})" +definition + C_live_ioa :: "(action, nat)live_ioa" where + "C_live_ioa = (C_ioa, WF C_ioa {INC})" -C_ioa_def: "C_ioa == - (C_asig, {0}, C_trans,{},{})" - -C_live_ioa_def: - "C_live_ioa == (C_ioa, WF C_ioa {INC})" - -A_asig_def: - "A_asig == ({},{INC},{})" +definition + A_asig :: "action signature" where + "A_asig = ({},{INC},{})" +definition + A_trans :: "(action, bool)transition set" where + "A_trans = + {tr. let s = fst(tr); + t = snd(snd(tr)) + in case fst(snd(tr)) + of + INC => t = True}" +definition + A_ioa :: "(action, bool)ioa" where + "A_ioa = (A_asig, {False}, A_trans,{},{})" +definition + A_live_ioa :: "(action, bool)live_ioa" where + "A_live_ioa = (A_ioa, WF A_ioa {INC})" -A_trans_def: "A_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - INC => t = True}" - -A_ioa_def: "A_ioa == - (A_asig, {False}, A_trans,{},{})" +definition + h_abs :: "nat => bool" where + "h_abs n = (n~=0)" -A_live_ioa_def: - "A_live_ioa == (A_ioa, WF A_ioa {INC})" - - -h_abs_def: - "h_abs n == n~=0" - -axioms - -MC_result: - "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)" +axiomatization where + MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)" lemma h_abs_is_abstraction: diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/meta_theory/Abstraction.thy --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Oct 21 16:27:42 2007 +0200 @@ -12,69 +12,57 @@ defaultsort type -consts +definition + cex_abs :: "('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" where + "cex_abs f ex = (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))" +definition + -- {* equals cex_abs on Sequences -- after ex2seq application *} + cex_absSeq :: "('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq" where + "cex_absSeq f = (%s. Map (%(s,a,t). (f s,a,f t))$s)" - cex_abs ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" - cex_absSeq ::"('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq" - - is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" +definition + is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where + "is_abstraction f C A = + ((!s:starts_of(C). f(s):starts_of(A)) & + (!s t a. reachable C s & s -a--C-> t + --> (f s) -a--A-> (f t)))" - weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" - temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" - temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" +definition + weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" where + "weakeningIOA A C h = (!ex. ex : executions C --> cex_abs h ex : executions A)" +definition + temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where + "temp_strengthening Q P h = (!ex. (cex_abs h ex |== Q) --> (ex |== P))" +definition + temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where + "temp_weakening Q P h = temp_strengthening (.~ Q) (.~ P) h" - state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" - state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" +definition + state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where + "state_strengthening Q P h = (!s t a. Q (h(s),a,h(t)) --> P (s,a,t))" +definition + state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where + "state_weakening Q P h = state_strengthening (.~Q) (.~P) h" - is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" +definition + is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where + "is_live_abstraction h CL AM = + (is_abstraction h (fst CL) (fst AM) & + temp_weakening (snd AM) (snd CL) h)" -defs - -is_abstraction_def: - "is_abstraction f C A == - (!s:starts_of(C). f(s):starts_of(A)) & - (!s t a. reachable C s & s -a--C-> t - --> (f s) -a--A-> (f t))" - -is_live_abstraction_def: - "is_live_abstraction h CL AM == - is_abstraction h (fst CL) (fst AM) & - temp_weakening (snd AM) (snd CL) h" - -cex_abs_def: - "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))" - -(* equals cex_abs on Sequneces -- after ex2seq application -- *) -cex_absSeq_def: - "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s" - -weakeningIOA_def: - "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A" - -temp_weakening_def: - "temp_weakening Q P h == temp_strengthening (.~ Q) (.~ P) h" - -temp_strengthening_def: - "temp_strengthening Q P h == ! ex. (cex_abs h ex |== Q) --> (ex |== P)" - -state_weakening_def: - "state_weakening Q P h == state_strengthening (.~Q) (.~P) h" - -state_strengthening_def: - "state_strengthening Q P h == ! s t a. Q (h(s),a,h(t)) --> P (s,a,t)" - -axioms - +axiomatization where (* thm about ex2seq which is not provable by induction as ex2seq is not continous *) ex2seq_abs_cex: "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" +axiomatization where (* analog to the proved thm strength_Box - proof skipped as trivial *) weak_Box: "temp_weakening P Q h ==> temp_weakening ([] P) ([] Q) h" +axiomatization where (* analog to the proved thm strength_Next - proof skipped as trivial *) weak_Next: "temp_weakening P Q h @@ -82,7 +70,7 @@ subsection "cex_abs" - + lemma cex_abs_UU: "cex_abs f (s,UU) = (f s, UU)" by (simp add: cex_abs_def) @@ -94,7 +82,7 @@ declare cex_abs_UU [simp] cex_abs_nil [simp] cex_abs_cons [simp] - + subsection "lemmas" lemma temp_weakening_def2: "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))" @@ -110,9 +98,9 @@ subsection "Abstraction Rules for Properties" -lemma exec_frag_abstraction [rule_format]: - "[| is_abstraction h C A |] ==> - !s. reachable C s & is_exec_frag C (s,xs) +lemma exec_frag_abstraction [rule_format]: + "[| is_abstraction h C A |] ==> + !s. reachable C s & is_exec_frag C (s,xs) --> is_exec_frag A (cex_abs h (s,xs))" apply (unfold cex_abs_def) apply simp @@ -139,7 +127,7 @@ done -lemma AbsRuleT1: "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] +lemma AbsRuleT1: "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] ==> validIOA C P" apply (drule abs_is_weakening) apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def) @@ -165,9 +153,9 @@ declare IMPLIES_temp_sat [simp] AND_temp_sat [simp] OR_temp_sat [simp] NOT_temp_sat [simp] -lemma AbsRuleT2: - "[|is_live_abstraction h (C,L) (A,M); - validLIOA (A,M) Q; temp_strengthening Q P h |] +lemma AbsRuleT2: + "[|is_live_abstraction h (C,L) (A,M); + validLIOA (A,M) Q; temp_strengthening Q P h |] ==> validLIOA (C,L) P" apply (unfold is_live_abstraction_def) apply auto @@ -178,10 +166,10 @@ done -lemma AbsRuleTImprove: - "[|is_live_abstraction h (C,L) (A,M); - validLIOA (A,M) (H1 .--> Q); temp_strengthening Q P h; - temp_weakening H1 H2 h; validLIOA (C,L) H2 |] +lemma AbsRuleTImprove: + "[|is_live_abstraction h (C,L) (A,M); + validLIOA (A,M) (H1 .--> Q); temp_strengthening Q P h; + temp_weakening H1 H2 h; validLIOA (C,L) H2 |] ==> validLIOA (C,L) P" apply (unfold is_live_abstraction_def) apply auto @@ -194,7 +182,7 @@ subsection "Correctness of safe abstraction" -lemma abstraction_is_ref_map: +lemma abstraction_is_ref_map: "is_abstraction h C A ==> is_ref_map h C A" apply (unfold is_abstraction_def is_ref_map_def) apply (tactic "safe_tac set_cs") @@ -203,8 +191,8 @@ done -lemma abs_safety: "[| inp(C)=inp(A); out(C)=out(A); - is_abstraction h C A |] +lemma abs_safety: "[| inp(C)=inp(A); out(C)=out(A); + is_abstraction h C A |] ==> C =<| A" apply (simp add: ioa_implements_def) apply (rule trace_inclusion) @@ -218,8 +206,8 @@ (* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x), that is to special Map Lemma *) -lemma traces_coincide_abs: - "ext C = ext A +lemma traces_coincide_abs: + "ext C = ext A ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))" apply (unfold cex_abs_def mk_trace_def filter_act_def) apply simp @@ -231,8 +219,8 @@ is_live_abstraction includes temp_strengthening which is necessarily based on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific way for cex_abs *) -lemma abs_liveness: "[| inp(C)=inp(A); out(C)=out(A); - is_live_abstraction h (C,M) (A,L) |] +lemma abs_liveness: "[| inp(C)=inp(A); out(C)=out(A); + is_live_abstraction h (C,M) (A,L) |] ==> live_implements (C,M) (A,L)" apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def) apply (tactic "safe_tac set_cs") @@ -243,25 +231,25 @@ apply (rule traces_coincide_abs) apply (simp (no_asm) add: externals_def) apply (auto)[1] - + (* cex_abs is execution *) apply (tactic {* pair_tac "ex" 1 *}) apply (simp add: executions_def) - (* start state *) + (* start state *) apply (rule conjI) apply (simp add: is_abstraction_def cex_abs_def) (* is-execution-fragment *) apply (erule exec_frag_abstraction) apply (simp add: reachable.reachable_0) - (* Liveness *) + (* Liveness *) apply (simp add: temp_weakening_def2) apply (tactic {* pair_tac "ex" 1 *}) done (* FIX: NAch Traces.ML bringen *) -lemma implements_trans: +lemma implements_trans: "[| A =<| B; B =<| C|] ==> A =<| C" apply (unfold ioa_implements_def) apply auto @@ -270,11 +258,11 @@ subsection "Abstraction Rules for Automata" -lemma AbsRuleA1: "[| inp(C)=inp(A); out(C)=out(A); - inp(Q)=inp(P); out(Q)=out(P); - is_abstraction h1 C A; - A =<| Q ; - is_abstraction h2 Q P |] +lemma AbsRuleA1: "[| inp(C)=inp(A); out(C)=out(A); + inp(Q)=inp(P); out(Q)=out(P); + is_abstraction h1 C A; + A =<| Q ; + is_abstraction h2 Q P |] ==> C =<| P" apply (drule abs_safety) apply assumption+ @@ -286,11 +274,11 @@ done -lemma AbsRuleA2: "!!LC. [| inp(C)=inp(A); out(C)=out(A); - inp(Q)=inp(P); out(Q)=out(P); - is_live_abstraction h1 (C,LC) (A,LA); - live_implements (A,LA) (Q,LQ) ; - is_live_abstraction h2 (Q,LQ) (P,LP) |] +lemma AbsRuleA2: "!!LC. [| inp(C)=inp(A); out(C)=out(A); + inp(Q)=inp(P); out(Q)=out(P); + is_live_abstraction h1 (C,LC) (A,LA); + live_implements (A,LA) (Q,LQ) ; + is_live_abstraction h2 (Q,LQ) (P,LP) |] ==> live_implements (C,LC) (P,LP)" apply (drule abs_liveness) apply assumption+ @@ -307,64 +295,64 @@ subsection "Localizing Temporal Strengthenings and Weakenings" -lemma strength_AND: -"[| temp_strengthening P1 Q1 h; - temp_strengthening P2 Q2 h |] +lemma strength_AND: +"[| temp_strengthening P1 Q1 h; + temp_strengthening P2 Q2 h |] ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h" apply (unfold temp_strengthening_def) apply auto done -lemma strength_OR: -"[| temp_strengthening P1 Q1 h; - temp_strengthening P2 Q2 h |] +lemma strength_OR: +"[| temp_strengthening P1 Q1 h; + temp_strengthening P2 Q2 h |] ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h" apply (unfold temp_strengthening_def) apply auto done -lemma strength_NOT: -"[| temp_weakening P Q h |] +lemma strength_NOT: +"[| temp_weakening P Q h |] ==> temp_strengthening (.~ P) (.~ Q) h" apply (unfold temp_strengthening_def) apply (simp add: temp_weakening_def2) apply auto done -lemma strength_IMPLIES: -"[| temp_weakening P1 Q1 h; - temp_strengthening P2 Q2 h |] +lemma strength_IMPLIES: +"[| temp_weakening P1 Q1 h; + temp_strengthening P2 Q2 h |] ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h" apply (unfold temp_strengthening_def) apply (simp add: temp_weakening_def2) done -lemma weak_AND: -"[| temp_weakening P1 Q1 h; - temp_weakening P2 Q2 h |] +lemma weak_AND: +"[| temp_weakening P1 Q1 h; + temp_weakening P2 Q2 h |] ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h" apply (simp add: temp_weakening_def2) done -lemma weak_OR: -"[| temp_weakening P1 Q1 h; - temp_weakening P2 Q2 h |] +lemma weak_OR: +"[| temp_weakening P1 Q1 h; + temp_weakening P2 Q2 h |] ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h" apply (simp add: temp_weakening_def2) done -lemma weak_NOT: -"[| temp_strengthening P Q h |] +lemma weak_NOT: +"[| temp_strengthening P Q h |] ==> temp_weakening (.~ P) (.~ Q) h" apply (unfold temp_strengthening_def) apply (simp add: temp_weakening_def2) apply auto done -lemma weak_IMPLIES: -"[| temp_strengthening P1 Q1 h; - temp_weakening P2 Q2 h |] +lemma weak_IMPLIES: +"[| temp_strengthening P1 Q1 h; + temp_weakening P2 Q2 h |] ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h" apply (unfold temp_strengthening_def) apply (simp add: temp_weakening_def2) @@ -379,7 +367,7 @@ done lemma ex2seqConc [rule_format]: -"Finite s1 --> +"Finite s1 --> (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))" apply (rule impI) apply (tactic {* Seq_Finite_induct_tac 1 *}) @@ -399,7 +387,7 @@ (* important property of ex2seq: can be shiftet, as defined "pointwise" *) -lemma ex2seq_tsuffix: +lemma ex2seq_tsuffix: "tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')" apply (unfold tsuffix_def suffix_def) apply auto @@ -419,10 +407,10 @@ done -(* important property of cex_absSeq: As it is a 1to1 correspondence, +(* important property of cex_absSeq: As it is a 1to1 correspondence, properties carry over *) -lemma cex_absSeq_tsuffix: +lemma cex_absSeq_tsuffix: "tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)" apply (unfold tsuffix_def suffix_def cex_absSeq_def) apply auto @@ -433,8 +421,8 @@ done -lemma strength_Box: -"[| temp_strengthening P Q h |] +lemma strength_Box: +"[| temp_strengthening P Q h |] ==> temp_strengthening ([] P) ([] Q) h" apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def) apply (tactic "clarify_tac set_cs 1") @@ -447,10 +435,10 @@ subsubsection {* Init *} -lemma strength_Init: -"[| state_strengthening P Q h |] +lemma strength_Init: +"[| state_strengthening P Q h |] ==> temp_strengthening (Init P) (Init Q) h" -apply (unfold temp_strengthening_def state_strengthening_def +apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Init_def unlift_def) apply (tactic "safe_tac set_cs") apply (tactic {* pair_tac "ex" 1 *}) @@ -461,7 +449,7 @@ subsubsection {* Next *} -lemma TL_ex2seq_UU: +lemma TL_ex2seq_UU: "(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)" apply (tactic {* pair_tac "ex" 1 *}) apply (tactic {* Seq_case_simp_tac "y" 1 *}) @@ -470,7 +458,7 @@ apply (tactic {* pair_tac "a" 1 *}) done -lemma TL_ex2seq_nil: +lemma TL_ex2seq_nil: "(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)" apply (tactic {* pair_tac "ex" 1 *}) apply (tactic {* Seq_case_simp_tac "y" 1 *}) @@ -484,10 +472,10 @@ apply (tactic {* Seq_induct_tac "s" [] 1 *}) done -(* important property of cex_absSeq: As it is a 1to1 correspondence, +(* important property of cex_absSeq: As it is a 1to1 correspondence, properties carry over *) -lemma cex_absSeq_TL: +lemma cex_absSeq_TL: "cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))" apply (unfold cex_absSeq_def) apply (simp add: MapTL) @@ -502,7 +490,7 @@ apply auto done - + lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)" apply (tactic {* pair_tac "ex" 1 *}) apply (tactic {* Seq_case_simp_tac "y" 1 *}) @@ -512,8 +500,8 @@ done -lemma strength_Next: -"[| temp_strengthening P Q h |] +lemma strength_Next: +"[| temp_strengthening P Q h |] ==> temp_strengthening (Next P) (Next Q) h" apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def) apply simp @@ -533,8 +521,8 @@ text {* Localizing Temporal Weakenings - 2 *} -lemma weak_Init: -"[| state_weakening P Q h |] +lemma weak_Init: +"[| state_weakening P Q h |] ==> temp_weakening (Init P) (Init Q) h" apply (simp add: temp_weakening_def2 state_weakening_def2 temp_sat_def satisfies_def Init_def unlift_def) @@ -547,8 +535,8 @@ text {* Localizing Temproal Strengthenings - 3 *} -lemma strength_Diamond: -"[| temp_strengthening P Q h |] +lemma strength_Diamond: +"[| temp_strengthening P Q h |] ==> temp_strengthening (<> P) (<> Q) h" apply (unfold Diamond_def) apply (rule strength_NOT) @@ -556,9 +544,9 @@ apply (erule weak_NOT) done -lemma strength_Leadsto: -"[| temp_weakening P1 P2 h; - temp_strengthening Q1 Q2 h |] +lemma strength_Leadsto: +"[| temp_weakening P1 P2 h; + temp_strengthening Q1 Q2 h |] ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h" apply (unfold Leadsto_def) apply (rule strength_Box) @@ -569,8 +557,8 @@ text {* Localizing Temporal Weakenings - 3 *} -lemma weak_Diamond: -"[| temp_weakening P Q h |] +lemma weak_Diamond: +"[| temp_weakening P Q h |] ==> temp_weakening (<> P) (<> Q) h" apply (unfold Diamond_def) apply (rule weak_NOT) @@ -578,9 +566,9 @@ apply (erule strength_NOT) done -lemma weak_Leadsto: -"[| temp_strengthening P1 P2 h; - temp_weakening Q1 Q2 h |] +lemma weak_Leadsto: +"[| temp_strengthening P1 P2 h; + temp_weakening Q1 Q2 h |] ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h" apply (unfold Leadsto_def) apply (rule weak_Box) @@ -588,8 +576,8 @@ apply (erule weak_Diamond) done -lemma weak_WF: - " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] +lemma weak_WF: + " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] ==> temp_weakening (WF A acts) (WF C acts) h" apply (unfold WF_def) apply (rule weak_IMPLIES) @@ -603,8 +591,8 @@ xt2_def plift_def option_lift_def NOT_def) done -lemma weak_SF: - " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] +lemma weak_SF: + " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] ==> temp_weakening (SF A acts) (SF C acts) h" apply (unfold SF_def) apply (rule weak_IMPLIES) @@ -626,18 +614,10 @@ strength_Diamond strength_Leadsto weak_WF weak_SF ML {* - -local - val weak_strength_lemmas = thms "weak_strength_lemmas" - val state_strengthening_def = thm "state_strengthening_def" - val state_weakening_def = thm "state_weakening_def" -in - -fun abstraction_tac i = +fun abstraction_tac i = SELECT_GOAL (CLASIMPSET (fn (cs, ss) => - auto_tac (cs addSIs weak_strength_lemmas, - ss addsimps [state_strengthening_def, state_weakening_def]))) i -end + auto_tac (cs addSIs @{thms weak_strength_lemmas}, + ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))) i *} use "ioa_package.ML" diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/meta_theory/Asig.thy --- a/src/HOLCF/IOA/meta_theory/Asig.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/meta_theory/Asig.thy Sun Oct 21 16:27:42 2007 +0200 @@ -12,47 +12,47 @@ types 'a signature = "('a set * 'a set * 'a set)" -consts - actions :: "'action signature => 'action set" - inputs :: "'action signature => 'action set" - outputs :: "'action signature => 'action set" - internals :: "'action signature => 'action set" - externals :: "'action signature => 'action set" - locals :: "'action signature => 'action set" - is_asig ::"'action signature => bool" - mk_ext_asig ::"'action signature => 'action signature" +definition + inputs :: "'action signature => 'action set" where + asig_inputs_def: "inputs = fst" -defs +definition + outputs :: "'action signature => 'action set" where + asig_outputs_def: "outputs = (fst o snd)" + +definition + internals :: "'action signature => 'action set" where + asig_internals_def: "internals = (snd o snd)" -asig_inputs_def: "inputs == fst" -asig_outputs_def: "outputs == (fst o snd)" -asig_internals_def: "internals == (snd o snd)" +definition + actions :: "'action signature => 'action set" where + "actions(asig) = (inputs(asig) Un outputs(asig) Un internals(asig))" -actions_def: - "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" +definition + externals :: "'action signature => 'action set" where + "externals(asig) = (inputs(asig) Un outputs(asig))" -externals_def: - "externals(asig) == (inputs(asig) Un outputs(asig))" +definition + locals :: "'action signature => 'action set" where + "locals asig = ((internals asig) Un (outputs asig))" -locals_def: - "locals asig == ((internals asig) Un (outputs asig))" - -is_asig_def: - "is_asig(triple) == - ((inputs(triple) Int outputs(triple) = {}) & +definition + is_asig :: "'action signature => bool" where + "is_asig(triple) = + ((inputs(triple) Int outputs(triple) = {}) & (outputs(triple) Int internals(triple) = {}) & (inputs(triple) Int internals(triple) = {}))" - -mk_ext_asig_def: - "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})" +definition + mk_ext_asig :: "'action signature => 'action signature" where + "mk_ext_asig(triple) = (inputs(triple), outputs(triple), {})" lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def -lemma asig_triple_proj: - "(outputs (a,b,c) = b) & - (inputs (a,b,c) = a) & +lemma asig_triple_proj: + "(outputs (a,b,c) = b) & + (inputs (a,b,c) = a) & (internals (a,b,c) = c)" apply (simp add: asig_projections) done @@ -91,7 +91,7 @@ apply blast done -lemma int_is_not_ext: +lemma int_is_not_ext: "[| is_asig (S); x:internals S |] ==> x~:externals S" apply (unfold externals_def actions_def is_asig_def) apply simp diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/meta_theory/CompoExecs.thy --- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Sun Oct 21 16:27:42 2007 +0200 @@ -9,49 +9,33 @@ imports Traces begin -consts +definition + ProjA2 :: "('a,'s * 't)pairs -> ('a,'s)pairs" where + "ProjA2 = Map (%x.(fst x,fst(snd x)))" - ProjA ::"('a,'s * 't)execution => ('a,'s)execution" - ProjA2 ::"('a,'s * 't)pairs -> ('a,'s)pairs" - ProjB ::"('a,'s * 't)execution => ('a,'t)execution" - ProjB2 ::"('a,'s * 't)pairs -> ('a,'t)pairs" - Filter_ex ::"'a signature => ('a,'s)execution => ('a,'s)execution" - Filter_ex2 ::"'a signature => ('a,'s)pairs -> ('a,'s)pairs" - stutter ::"'a signature => ('a,'s)execution => bool" - stutter2 ::"'a signature => ('a,'s)pairs -> ('s => tr)" +definition + ProjA :: "('a,'s * 't)execution => ('a,'s)execution" where + "ProjA ex = (fst (fst ex), ProjA2$(snd ex))" - par_execs ::"[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module" - - -defs - - -ProjA_def: - "ProjA ex == (fst (fst ex), ProjA2$(snd ex))" +definition + ProjB2 :: "('a,'s * 't)pairs -> ('a,'t)pairs" where + "ProjB2 = Map (%x.(fst x,snd(snd x)))" -ProjB_def: - "ProjB ex == (snd (fst ex), ProjB2$(snd ex))" - +definition + ProjB :: "('a,'s * 't)execution => ('a,'t)execution" where + "ProjB ex = (snd (fst ex), ProjB2$(snd ex))" -ProjA2_def: - "ProjA2 == Map (%x.(fst x,fst(snd x)))" - -ProjB2_def: - "ProjB2 == Map (%x.(fst x,snd(snd x)))" - +definition + Filter_ex2 :: "'a signature => ('a,'s)pairs -> ('a,'s)pairs" where + "Filter_ex2 sig = Filter (%x. fst x:actions sig)" -Filter_ex_def: - "Filter_ex sig ex == (fst ex,Filter_ex2 sig$(snd ex))" - +definition + Filter_ex :: "'a signature => ('a,'s)execution => ('a,'s)execution" where + "Filter_ex sig ex = (fst ex,Filter_ex2 sig$(snd ex))" -Filter_ex2_def: - "Filter_ex2 sig == Filter (%x. fst x:actions sig)" - -stutter_def: - "stutter sig ex == ((stutter2 sig$(snd ex)) (fst ex) ~= FF)" - -stutter2_def: - "stutter2 sig ==(fix$(LAM h ex. (%s. case ex of +definition + stutter2 :: "'a signature => ('a,'s)pairs -> ('s => tr)" where + "stutter2 sig = (fix$(LAM h ex. (%s. case ex of nil => TT | x##xs => (flift1 (%p.(If Def ((fst p)~:actions sig) @@ -61,9 +45,14 @@ $x) )))" -par_execs_def: - "par_execs ExecsA ExecsB == - let exA = fst ExecsA; sigA = snd ExecsA; +definition + stutter :: "'a signature => ('a,'s)execution => bool" where + "stutter sig ex = ((stutter2 sig$(snd ex)) (fst ex) ~= FF)" + +definition + par_execs :: "[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module" where + "par_execs ExecsA ExecsB = + (let exA = fst ExecsA; sigA = snd ExecsA; exB = fst ExecsB; sigB = snd ExecsB in ( {ex. Filter_ex sigA (ProjA ex) : exA} @@ -71,8 +60,7 @@ Int {ex. stutter sigA (ProjA ex)} Int {ex. stutter sigB (ProjB ex)} Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)}, - asig_comp sigA sigB)" - + asig_comp sigA sigB))" lemmas [simp del] = ex_simps all_simps split_paired_All @@ -131,9 +119,9 @@ apply (simp add: Filter_ex2_def) done -lemma Filter_ex2_cons: "Filter_ex2 sig$(at >> xs) = - (if (fst at:actions sig) - then at >> (Filter_ex2 sig$xs) +lemma Filter_ex2_cons: "Filter_ex2 sig$(at >> xs) = + (if (fst at:actions sig) + then at >> (Filter_ex2 sig$xs) else Filter_ex2 sig$xs)" apply (simp add: Filter_ex2_def) @@ -145,18 +133,18 @@ (* ---------------------------------------------------------------- *) -lemma stutter2_unfold: "stutter2 sig = (LAM ex. (%s. case ex of - nil => TT - | x##xs => (flift1 - (%p.(If Def ((fst p)~:actions sig) - then Def (s=(snd p)) - else TT fi) - andalso (stutter2 sig$xs) (snd p)) - $x) +lemma stutter2_unfold: "stutter2 sig = (LAM ex. (%s. case ex of + nil => TT + | x##xs => (flift1 + (%p.(If Def ((fst p)~:actions sig) + then Def (s=(snd p)) + else TT fi) + andalso (stutter2 sig$xs) (snd p)) + $x) ))" apply (rule trans) apply (rule fix_eq2) -apply (rule stutter2_def) +apply (simp only: stutter2_def) apply (rule beta_cfun) apply (simp add: flift1_def) done @@ -171,8 +159,8 @@ apply simp done -lemma stutter2_cons: "(stutter2 sig$(at>>xs)) s = - ((if (fst at)~:actions sig then Def (s=snd at) else TT) +lemma stutter2_cons: "(stutter2 sig$(at>>xs)) s = + ((if (fst at)~:actions sig then Def (s=snd at) else TT) andalso (stutter2 sig$xs) (snd at))" apply (rule trans) apply (subst stutter2_unfold) @@ -196,7 +184,7 @@ apply (simp add: stutter_def) done -lemma stutter_cons: "stutter sig (s, (a,t)>>ex) = +lemma stutter_cons: "stutter sig (s, (a,t)>>ex) = ((a~:actions sig --> (s=t)) & stutter sig (t,ex))" apply (simp add: stutter_def) done @@ -224,8 +212,8 @@ (* Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B *) (* --------------------------------------------------------------------- *) -lemma lemma_1_1a: "!s. is_exec_frag (A||B) (s,xs) - --> is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) & +lemma lemma_1_1a: "!s. is_exec_frag (A||B) (s,xs) + --> is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) & is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))" apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *}) @@ -240,8 +228,8 @@ (* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *) (* --------------------------------------------------------------------- *) -lemma lemma_1_1b: "!s. is_exec_frag (A||B) (s,xs) - --> stutter (asig_of A) (fst s,ProjA2$xs) & +lemma lemma_1_1b: "!s. is_exec_frag (A||B) (s,xs) + --> stutter (asig_of A) (fst s,ProjA2$xs) & stutter (asig_of B) (snd s,ProjB2$xs)" apply (tactic {* pair_induct_tac "xs" [thm "stutter_def", thm "is_exec_frag_def"] 1 *}) @@ -255,7 +243,7 @@ (* Lemma_1_1c : Executions of A||B have only A- or B-actions *) (* --------------------------------------------------------------------- *) -lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs) +lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs) --> Forall (%x. fst x:act (A||B)) xs)" apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def", @@ -270,12 +258,12 @@ (* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *) (* ----------------------------------------------------------------------- *) -lemma lemma_1_2: -"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) & - is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) & - stutter (asig_of A) (fst s,(ProjA2$xs)) & - stutter (asig_of B) (snd s,(ProjB2$xs)) & - Forall (%x. fst x:act (A||B)) xs +lemma lemma_1_2: +"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) & + is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) & + stutter (asig_of A) (fst s,(ProjA2$xs)) & + stutter (asig_of B) (snd s,(ProjB2$xs)) & + Forall (%x. fst x:act (A||B)) xs --> is_exec_frag (A||B) (s,xs)" apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def", @@ -289,11 +277,11 @@ subsection {* COMPOSITIONALITY on EXECUTION Level -- Main Theorem *} -lemma compositionality_ex: -"(ex:executions(A||B)) = - (Filter_ex (asig_of A) (ProjA ex) : executions A & - Filter_ex (asig_of B) (ProjB ex) : executions B & - stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) & +lemma compositionality_ex: +"(ex:executions(A||B)) = + (Filter_ex (asig_of A) (ProjA ex) : executions A & + Filter_ex (asig_of B) (ProjB ex) : executions B & + stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) & Forall (%x. fst x:act (A||B)) (snd ex))" apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par) @@ -310,7 +298,7 @@ subsection {* COMPOSITIONALITY on EXECUTION Level -- for Modules *} -lemma compositionality_ex_modules: +lemma compositionality_ex_modules: "Execs (A||B) = par_execs (Execs A) (Execs B)" apply (unfold Execs_def par_execs_def) apply (simp add: asig_of_par) diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/meta_theory/CompoScheds.thy --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Sun Oct 21 16:27:42 2007 +0200 @@ -9,25 +9,11 @@ imports CompoExecs begin -consts - - mkex ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq => - ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" - mkex2 ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> +definition + mkex2 :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq -> ('a,'s)pairs -> ('a,'t)pairs -> - ('s => 't => ('a,'s*'t)pairs)" - par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module" - - -defs - -mkex_def: - "mkex A B sch exA exB == - ((fst exA,fst exB), - (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))" - -mkex2_def: - "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of + ('s => 't => ('a,'s*'t)pairs)" where + "mkex2 A B = (fix$(LAM h sch exA exB. (%s t. case sch of nil => nil | x##xs => (case x of @@ -60,15 +46,23 @@ ) ))))" -par_scheds_def: - "par_scheds SchedsA SchedsB == - let schA = fst SchedsA; sigA = snd SchedsA; +definition + mkex :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq => + ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" where + "mkex A B sch exA exB = + ((fst exA,fst exB), + (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))" + +definition + par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module" where + "par_scheds SchedsA SchedsB = + (let schA = fst SchedsA; sigA = snd SchedsA; schB = fst SchedsB; sigB = snd SchedsB in ( {sch. Filter (%a. a:actions sigA)$sch : schA} Int {sch. Filter (%a. a:actions sigB)$sch : schB} Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch}, - asig_comp sigA sigB)" + asig_comp sigA sigB))" declare surjective_pairing [symmetric, simp] @@ -78,41 +72,41 @@ lemma mkex2_unfold: -"mkex2 A B = (LAM sch exA exB. (%s t. case sch of - nil => nil - | x##xs => - (case x of - UU => UU - | Def y => - (if y:act A then - (if y:act B then - (case HD$exA of - UU => UU - | Def a => (case HD$exB of - UU => UU - | Def b => - (y,(snd a,snd b))>> - (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b))) - else - (case HD$exA of - UU => UU - | Def a => - (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t) - ) - else - (if y:act B then - (case HD$exB of - UU => UU - | Def b => - (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b)) - else - UU - ) - ) +"mkex2 A B = (LAM sch exA exB. (%s t. case sch of + nil => nil + | x##xs => + (case x of + UU => UU + | Def y => + (if y:act A then + (if y:act B then + (case HD$exA of + UU => UU + | Def a => (case HD$exB of + UU => UU + | Def b => + (y,(snd a,snd b))>> + (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b))) + else + (case HD$exA of + UU => UU + | Def a => + (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t) + ) + else + (if y:act B then + (case HD$exB of + UU => UU + | Def b => + (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b)) + else + UU + ) + ) )))" apply (rule trans) apply (rule fix_eq2) -apply (rule mkex2_def) +apply (simp only: mkex2_def) apply (rule beta_cfun) apply simp done @@ -127,8 +121,8 @@ apply simp done -lemma mkex2_cons_1: "[| x:act A; x~:act B; HD$exA=Def a|] - ==> (mkex2 A B$(x>>sch)$exA$exB) s t = +lemma mkex2_cons_1: "[| x:act A; x~:act B; HD$exA=Def a|] + ==> (mkex2 A B$(x>>sch)$exA$exB) s t = (x,snd a,t) >> (mkex2 A B$sch$(TL$exA)$exB) (snd a) t" apply (rule trans) apply (subst mkex2_unfold) @@ -136,8 +130,8 @@ apply (simp add: Consq_def) done -lemma mkex2_cons_2: "[| x~:act A; x:act B; HD$exB=Def b|] - ==> (mkex2 A B$(x>>sch)$exA$exB) s t = +lemma mkex2_cons_2: "[| x~:act A; x:act B; HD$exB=Def b|] + ==> (mkex2 A B$(x>>sch)$exA$exB) s t = (x,s,snd b) >> (mkex2 A B$sch$exA$(TL$exB)) s (snd b)" apply (rule trans) apply (subst mkex2_unfold) @@ -145,9 +139,9 @@ apply (simp add: Consq_def) done -lemma mkex2_cons_3: "[| x:act A; x:act B; HD$exA=Def a;HD$exB=Def b|] - ==> (mkex2 A B$(x>>sch)$exA$exB) s t = - (x,snd a,snd b) >> +lemma mkex2_cons_3: "[| x:act A; x:act B; HD$exA=Def a;HD$exB=Def b|] + ==> (mkex2 A B$(x>>sch)$exA$exB) s t = + (x,snd a,snd b) >> (mkex2 A B$sch$(TL$exA)$(TL$exB)) (snd a) (snd b)" apply (rule trans) apply (subst mkex2_unfold) @@ -169,24 +163,24 @@ apply (simp add: mkex_def) done -lemma mkex_cons_1: "[| x:act A; x~:act B |] - ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) = +lemma mkex_cons_1: "[| x:act A; x~:act B |] + ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) = ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))" apply (simp (no_asm) add: mkex_def) apply (cut_tac exA = "a>>exA" in mkex2_cons_1) apply auto done -lemma mkex_cons_2: "[| x~:act A; x:act B |] - ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) = +lemma mkex_cons_2: "[| x~:act A; x:act B |] + ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) = ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))" apply (simp (no_asm) add: mkex_def) apply (cut_tac exB = "b>>exB" in mkex2_cons_2) apply auto done -lemma mkex_cons_3: "[| x:act A; x:act B |] - ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = +lemma mkex_cons_3: "[| x:act A; x:act B |] + ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))" apply (simp (no_asm) add: mkex_def) apply (cut_tac exB = "b>>exB" and exA = "a>>exA" in mkex2_cons_3) @@ -209,8 +203,8 @@ (* Lemma_2_1 : tfilter(ex) and filter_act are commutative *) (* --------------------------------------------------------------------- *) -lemma lemma_2_1a: - "filter_act$(Filter_ex2 (asig_of A)$xs)= +lemma lemma_2_1a: + "filter_act$(Filter_ex2 (asig_of A)$xs)= Filter (%a. a:act A)$(filter_act$xs)" apply (unfold filter_act_def Filter_ex2_def) @@ -222,8 +216,8 @@ (* Lemma_2_2 : State-projections do not affect filter_act *) (* --------------------------------------------------------------------- *) -lemma lemma_2_1b: - "filter_act$(ProjA2$xs) =filter_act$xs & +lemma lemma_2_1b: + "filter_act$(ProjA2$xs) =filter_act$xs & filter_act$(ProjB2$xs) =filter_act$xs" apply (tactic {* pair_induct_tac "xs" [] 1 *}) done @@ -237,7 +231,7 @@ an ex is in A or B, but after projecting it onto the action schedule. Of course, this is the same proposition, but we cannot change this one, when then rather lemma_1_1c *) -lemma sch_actions_in_AorB: "!s. is_exec_frag (A||B) (s,xs) +lemma sch_actions_in_AorB: "!s. is_exec_frag (A||B) (s,xs) --> Forall (%x. x:act (A||B)) (filter_act$xs)" apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def", thm "Forall_def", @@ -255,10 +249,10 @@ structural induction --------------------------------------------------------------------------- *) -lemma Mapfst_mkex_is_sch: "! exA exB s t. - Forall (%x. x:act (A||B)) sch & - Filter (%a. a:act A)$sch << filter_act$exA & - Filter (%a. a:act B)$sch << filter_act$exB +lemma Mapfst_mkex_is_sch: "! exA exB s t. + Forall (%x. x:act (A||B)) sch & + Filter (%a. a:act A)$sch << filter_act$exA & + Filter (%a. a:act B)$sch << filter_act$exB --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch" apply (tactic {* Seq_induct_tac "sch" [thm "Filter_def", thm "Forall_def", @@ -327,20 +321,20 @@ structural induction --------------------------------------------------------------------------- *) -lemma stutterA_mkex: "! exA exB s t. - Forall (%x. x:act (A||B)) sch & - Filter (%a. a:act A)$sch << filter_act$exA & - Filter (%a. a:act B)$sch << filter_act$exB +lemma stutterA_mkex: "! exA exB s t. + Forall (%x. x:act (A||B)) sch & + Filter (%a. a:act A)$sch << filter_act$exA & + Filter (%a. a:act B)$sch << filter_act$exB --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))" apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *}) done -lemma stutter_mkex_on_A: "[| - Forall (%x. x:act (A||B)) sch ; - Filter (%a. a:act A)$sch << filter_act$(snd exA) ; - Filter (%a. a:act B)$sch << filter_act$(snd exB) |] +lemma stutter_mkex_on_A: "[| + Forall (%x. x:act (A||B)) sch ; + Filter (%a. a:act A)$sch << filter_act$(snd exA) ; + Filter (%a. a:act B)$sch << filter_act$(snd exB) |] ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))" apply (cut_tac stutterA_mkex) @@ -357,19 +351,19 @@ structural induction --------------------------------------------------------------------------- *) -lemma stutterB_mkex: "! exA exB s t. - Forall (%x. x:act (A||B)) sch & - Filter (%a. a:act A)$sch << filter_act$exA & - Filter (%a. a:act B)$sch << filter_act$exB +lemma stutterB_mkex: "! exA exB s t. + Forall (%x. x:act (A||B)) sch & + Filter (%a. a:act A)$sch << filter_act$exA & + Filter (%a. a:act B)$sch << filter_act$exB --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))" apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *}) done -lemma stutter_mkex_on_B: "[| - Forall (%x. x:act (A||B)) sch ; - Filter (%a. a:act A)$sch << filter_act$(snd exA) ; - Filter (%a. a:act B)$sch << filter_act$(snd exB) |] +lemma stutter_mkex_on_B: "[| + Forall (%x. x:act (A||B)) sch ; + Filter (%a. a:act A)$sch << filter_act$(snd exA) ; + Filter (%a. a:act B)$sch << filter_act$(snd exB) |] ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))" apply (cut_tac stutterB_mkex) apply (simp add: stutter_def ProjB_def mkex_def) @@ -387,11 +381,11 @@ structural induction --------------------------------------------------------------------------- *) -lemma filter_mkex_is_exA_tmp: "! exA exB s t. - Forall (%x. x:act (A||B)) sch & - Filter (%a. a:act A)$sch << filter_act$exA & - Filter (%a. a:act B)$sch << filter_act$exB - --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) = +lemma filter_mkex_is_exA_tmp: "! exA exB s t. + Forall (%x. x:act (A||B)) sch & + Filter (%a. a:act A)$sch << filter_act$exA & + Filter (%a. a:act B)$sch << filter_act$exB + --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) = Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)" apply (tactic {* mkex_induct_tac "sch" "exB" "exA" *}) done @@ -411,8 +405,8 @@ lemma for eliminating non admissible equations in assumptions --------------------------------------------------------------------------- *) -lemma trick_against_eq_in_ass: "!! sch ex. - Filter (%a. a:act AB)$sch = filter_act$ex +lemma trick_against_eq_in_ass: "!! sch ex. + Filter (%a. a:act AB)$sch = filter_act$ex ==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)" apply (simp add: filter_act_def) apply (rule Zip_Map_fst_snd [symmetric]) @@ -424,10 +418,10 @@ --------------------------------------------------------------------------- *) -lemma filter_mkex_is_exA: "!!sch exA exB. - [| Forall (%a. a:act (A||B)) sch ; - Filter (%a. a:act A)$sch = filter_act$(snd exA) ; - Filter (%a. a:act B)$sch = filter_act$(snd exB) |] +lemma filter_mkex_is_exA: "!!sch exA exB. + [| Forall (%a. a:act (A||B)) sch ; + Filter (%a. a:act A)$sch = filter_act$(snd exA) ; + Filter (%a. a:act B)$sch = filter_act$(snd exB) |] ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA" apply (simp add: ProjA_def Filter_ex_def) apply (tactic {* pair_tac "exA" 1 *}) @@ -448,11 +442,11 @@ structural induction --------------------------------------------------------------------------- *) -lemma filter_mkex_is_exB_tmp: "! exA exB s t. - Forall (%x. x:act (A||B)) sch & - Filter (%a. a:act A)$sch << filter_act$exA & - Filter (%a. a:act B)$sch << filter_act$exB - --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) = +lemma filter_mkex_is_exB_tmp: "! exA exB s t. + Forall (%x. x:act (A||B)) sch & + Filter (%a. a:act A)$sch << filter_act$exA & + Filter (%a. a:act B)$sch << filter_act$exB + --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) = Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)" (* notice necessary change of arguments exA and exB *) @@ -466,10 +460,10 @@ --------------------------------------------------------------------------- *) -lemma filter_mkex_is_exB: "!!sch exA exB. - [| Forall (%a. a:act (A||B)) sch ; - Filter (%a. a:act A)$sch = filter_act$(snd exA) ; - Filter (%a. a:act B)$sch = filter_act$(snd exB) |] +lemma filter_mkex_is_exB: "!!sch exA exB. + [| Forall (%a. a:act (A||B)) sch ; + Filter (%a. a:act A)$sch = filter_act$(snd exA) ; + Filter (%a. a:act B)$sch = filter_act$(snd exB) |] ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB" apply (simp add: ProjB_def Filter_ex_def) apply (tactic {* pair_tac "exA" 1 *}) @@ -487,11 +481,11 @@ (* --------------------------------------------------------------------- *) -lemma mkex_actions_in_AorB: "!s t exA exB. - Forall (%x. x : act (A || B)) sch & - Filter (%a. a:act A)$sch << filter_act$exA & - Filter (%a. a:act B)$sch << filter_act$exB - --> Forall (%x. fst x : act (A ||B)) +lemma mkex_actions_in_AorB: "!s t exA exB. + Forall (%x. x : act (A || B)) sch & + Filter (%a. a:act A)$sch << filter_act$exA & + Filter (%a. a:act B)$sch << filter_act$exB + --> Forall (%x. fst x : act (A ||B)) (snd (mkex A B sch (s,exA) (t,exB)))" apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *}) done @@ -502,10 +496,10 @@ (* Main Theorem *) (* ------------------------------------------------------------------ *) -lemma compositionality_sch: -"(sch : schedules (A||B)) = - (Filter (%a. a:act A)$sch : schedules A & - Filter (%a. a:act B)$sch : schedules B & +lemma compositionality_sch: +"(sch : schedules (A||B)) = + (Filter (%a. a:act A)$sch : schedules A & + Filter (%a. a:act B)$sch : schedules B & Forall (%x. x:act (A||B)) sch)" apply (simp (no_asm) add: schedules_def has_schedule_def) apply (tactic "safe_tac set_cs") @@ -545,7 +539,7 @@ subsection {* COMPOSITIONALITY on SCHEDULE Level -- for Modules *} -lemma compositionality_sch_modules: +lemma compositionality_sch_modules: "Scheds (A||B) = par_scheds (Scheds A) (Scheds B)" apply (unfold Scheds_def par_scheds_def) diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/meta_theory/LiveIOA.thy --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Sun Oct 21 16:27:42 2007 +0200 @@ -14,54 +14,40 @@ types ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp" -consts - -validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool" - -WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" -SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" +definition + validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool" where + "validLIOA AL P = validIOA (fst AL) ((snd AL) .--> P)" -liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" -livetraces :: "('a,'s)live_ioa => 'a trace set" -live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" -is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" - - -defs - -validLIOA_def: - "validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)" - +definition + WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where + "WF A acts = (<> [] <%(s,a,t) . Enabled A acts s> .--> [] <> )" +definition + SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where + "SF A acts = ([] <> <%(s,a,t) . Enabled A acts s> .--> [] <> )" -WF_def: - "WF A acts == <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> " - -SF_def: - "SF A acts == [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> " - - -liveexecutions_def: - "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}" - -livetraces_def: - "livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}" - -live_implements_def: - "live_implements CL AM == (inp (fst CL) = inp (fst AM)) & +definition + liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where + "liveexecutions AP = {exec. exec : executions (fst AP) & (exec |== (snd AP))}" +definition + livetraces :: "('a,'s)live_ioa => 'a trace set" where + "livetraces AP = {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}" +definition + live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where + "live_implements CL AM = ((inp (fst CL) = inp (fst AM)) & (out (fst CL) = out (fst AM)) & - livetraces CL <= livetraces AM" - -is_live_ref_map_def: - "is_live_ref_map f CL AM == - is_ref_map f (fst CL ) (fst AM) & + livetraces CL <= livetraces AM)" +definition + is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where + "is_live_ref_map f CL AM = + (is_ref_map f (fst CL ) (fst AM) & (! exec : executions (fst CL). (exec |== (snd CL)) --> - ((corresp_ex (fst AM) f exec) |== (snd AM)))" + ((corresp_ex (fst AM) f exec) |== (snd AM))))" declare split_paired_Ex [simp del] -lemma live_implements_trans: -"!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] +lemma live_implements_trans: +"!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] ==> live_implements (A,LA) (C,LC)" apply (unfold live_implements_def) apply auto @@ -69,9 +55,9 @@ subsection "Correctness of live refmap" - -lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A); - is_live_ref_map f (C,M) (A,L) |] + +lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A); + is_live_ref_map f (C,M) (A,L) |] ==> live_implements (C,M) (A,L)" apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def) apply (tactic "safe_tac set_cs") @@ -83,11 +69,11 @@ apply (simp (no_asm) add: externals_def) apply (auto)[1] apply (simp add: executions_def reachable.reachable_0) - + (* corresp_ex is execution, Lemma 2 *) apply (tactic {* pair_tac "ex" 1 *}) apply (simp add: executions_def) - (* start state *) + (* start state *) apply (rule conjI) apply (simp add: is_ref_map_def corresp_ex_def) (* is-execution-fragment *) diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/meta_theory/RefCorrectness.thy --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Sun Oct 21 16:27:42 2007 +0200 @@ -9,48 +9,42 @@ imports RefMappings begin -consts - - corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) => - ('a,'s1)execution => ('a,'s2)execution" - corresp_exC ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs - -> ('s1 => ('a,'s2)pairs)" - is_fair_ref_map :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool" - -defs - -corresp_ex_def: - "corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))" - - -corresp_exC_def: - "corresp_exC A f == (fix$(LAM h ex. (%s. case ex of +definition + corresp_exC :: "('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs + -> ('s1 => ('a,'s2)pairs)" where + "corresp_exC A f = (fix$(LAM h ex. (%s. case ex of nil => nil | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr))) @@ ((h$xs) (snd pr))) $x) )))" +definition + corresp_ex :: "('a,'s2)ioa => ('s1 => 's2) => + ('a,'s1)execution => ('a,'s2)execution" where + "corresp_ex A f ex = (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))" -is_fair_ref_map_def: - "is_fair_ref_map f C A == - is_ref_map f C A & - (! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex))" +definition + is_fair_ref_map :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool" where + "is_fair_ref_map f C A = + (is_ref_map f C A & + (! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex)))" - - -axioms (* Axioms for fair trace inclusion proof support, not for the correctness proof of refinement mappings! Note: Everything is superseded by LiveIOA.thy! *) +axiomatization where corresp_laststate: "Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))" +axiomatization where corresp_Finite: "Finite (snd (corresp_ex A f (s,ex))) = Finite ex" +axiomatization where FromAtoC: "fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex" +axiomatization where FromCtoA: "inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))" @@ -59,10 +53,12 @@ an index i from which on no W in ex. But W inf enabled, ie at least once after i W is enabled. As W does not occur after i and W is enabling_persistent, W keeps enabled until infinity, ie. indefinitely *) +axiomatization where persistent: "[|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W|] ==> inf_often (%x. fst x :W) ex | fin_often (%x. ~Enabled A W (snd x)) ex" +axiomatization where infpostcond: "[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|] ==> inf_often (% x. set_was_enabled A W (snd x)) ex" @@ -70,14 +66,14 @@ subsection "corresp_ex" -lemma corresp_exC_unfold: "corresp_exC A f = (LAM ex. (%s. case ex of - nil => nil - | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr))) - @@ ((corresp_exC A f $xs) (snd pr))) +lemma corresp_exC_unfold: "corresp_exC A f = (LAM ex. (%s. case ex of + nil => nil + | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr))) + @@ ((corresp_exC A f $xs) (snd pr))) $x) ))" apply (rule trans) apply (rule fix_eq2) -apply (rule corresp_exC_def) +apply (simp only: corresp_exC_def) apply (rule beta_cfun) apply (simp add: flift1_def) done @@ -92,8 +88,8 @@ apply simp done -lemma corresp_exC_cons: "(corresp_exC A f$(at>>xs)) s = - (@cex. move A cex (f s) (fst at) (f (snd at))) +lemma corresp_exC_cons: "(corresp_exC A f$(at>>xs)) s = + (@cex. move A cex (f s) (fst at) (f (snd at))) @@ ((corresp_exC A f$xs) (snd at))" apply (rule trans) apply (subst corresp_exC_unfold) @@ -108,8 +104,8 @@ subsection "properties of move" -lemma move_is_move: - "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> +lemma move_is_move: + "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> move A (@x. move A x (f s) a (f t)) (f s) a (f t)" apply (unfold is_ref_map_def) apply (subgoal_tac "? ex. move A ex (f s) a (f t) ") @@ -120,8 +116,8 @@ apply assumption done -lemma move_subprop1: - "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> +lemma move_subprop1: + "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> is_exec_frag A (f s,@x. move A x (f s) a (f t))" apply (cut_tac move_is_move) defer @@ -129,8 +125,8 @@ apply (simp add: move_def) done -lemma move_subprop2: - "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> +lemma move_subprop2: + "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> Finite ((@x. move A x (f s) a (f t)))" apply (cut_tac move_is_move) defer @@ -138,8 +134,8 @@ apply (simp add: move_def) done -lemma move_subprop3: - "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> +lemma move_subprop3: + "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> laststate (f s,@x. move A x (f s) a (f t)) = (f t)" apply (cut_tac move_is_move) defer @@ -147,9 +143,9 @@ apply (simp add: move_def) done -lemma move_subprop4: - "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> - mk_trace A$((@x. move A x (f s) a (f t))) = +lemma move_subprop4: + "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> + mk_trace A$((@x. move A x (f s) a (f t))) = (if a:ext A then a>>nil else nil)" apply (cut_tac move_is_move) defer @@ -180,9 +176,9 @@ ------------------------------------------------------- *) declare split_if [split del] -lemma lemma_1: - "[|is_ref_map f C A; ext C = ext A|] ==> - !s. reachable C s & is_exec_frag C (s,xs) --> +lemma lemma_1: + "[|is_ref_map f C A; ext C = ext A|] ==> + !s. reachable C s & is_exec_frag C (s,xs) --> mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))" apply (unfold corresp_ex_def) apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *}) @@ -209,10 +205,10 @@ (* Lemma 2.1 *) (* -------------------------------------------------- *) -lemma lemma_2_1 [rule_format (no_asm)]: -"Finite xs --> - (!s .is_exec_frag A (s,xs) & is_exec_frag A (t,ys) & - t = laststate (s,xs) +lemma lemma_2_1 [rule_format (no_asm)]: +"Finite xs --> + (!s .is_exec_frag A (s,xs) & is_exec_frag A (t,ys) & + t = laststate (s,xs) --> is_exec_frag A (s,xs @@ ys))" apply (rule impI) @@ -229,9 +225,9 @@ -lemma lemma_2: - "[| is_ref_map f C A |] ==> - !s. reachable C s & is_exec_frag C (s,xs) +lemma lemma_2: + "[| is_ref_map f C A |] ==> + !s. reachable C s & is_exec_frag C (s,xs) --> is_exec_frag A (corresp_ex A f (s,xs))" apply (unfold corresp_ex_def) @@ -267,8 +263,8 @@ subsection "Main Theorem: TRACE - INCLUSION" -lemma trace_inclusion: - "[| ext C = ext A; is_ref_map f C A |] +lemma trace_inclusion: + "[| ext C = ext A; is_ref_map f C A |] ==> traces C <= traces A" apply (unfold traces_def) @@ -305,14 +301,14 @@ done -lemma WF_alt: "is_wfair A W (s,ex) = +lemma WF_alt: "is_wfair A W (s,ex) = (fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)" apply (simp add: is_wfair_def fin_often_def) apply auto done -lemma WF_persistent: "[|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; - en_persistent A W|] +lemma WF_persistent: "[|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; + en_persistent A W|] ==> inf_often (%x. fst x :W) ex" apply (drule persistent) apply assumption @@ -321,9 +317,9 @@ done -lemma fair_trace_inclusion: "!! C A. - [| is_ref_map f C A; ext C = ext A; - !! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |] +lemma fair_trace_inclusion: "!! C A. + [| is_ref_map f C A; ext C = ext A; + !! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |] ==> fairtraces C <= fairtraces A" apply (simp (no_asm) add: fairtraces_def fairexecutions_def) apply (tactic "safe_tac set_cs") @@ -350,9 +346,9 @@ apply auto done -lemma fair_trace_inclusion2: "!! C A. - [| inp(C) = inp(A); out(C)=out(A); - is_fair_ref_map f C A |] +lemma fair_trace_inclusion2: "!! C A. + [| inp(C) = inp(A); out(C)=out(A); + is_fair_ref_map f C A |] ==> fair_implements C A" apply (simp add: is_fair_ref_map_def fair_implements_def fairtraces_def fairexecutions_def) apply (tactic "safe_tac set_cs") diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/meta_theory/RefMappings.thy --- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Sun Oct 21 16:27:42 2007 +0200 @@ -11,35 +11,30 @@ defaultsort type -consts - move ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" - is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" - is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" - - -defs - -move_def: - "move ioa ex s a t == +definition + move :: "[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" where + "move ioa ex s a t = (is_exec_frag ioa (s,ex) & Finite ex & laststate (s,ex)=t & mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))" -is_ref_map_def: - "is_ref_map f C A == - (!s:starts_of(C). f(s):starts_of(A)) & +definition + is_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where + "is_ref_map f C A = + ((!s:starts_of(C). f(s):starts_of(A)) & (!s t a. reachable C s & s -a--C-> t - --> (? ex. move A ex (f s) a (f t)))" + --> (? ex. move A ex (f s) a (f t))))" -is_weak_ref_map_def: - "is_weak_ref_map f C A == - (!s:starts_of(C). f(s):starts_of(A)) & +definition + is_weak_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where + "is_weak_ref_map f C A = + ((!s:starts_of(C). f(s):starts_of(A)) & (!s t a. reachable C s & s -a--C-> t --> (if a:ext(C) then (f s) -a--A-> (f t) - else (f s)=(f t)))" + else (f s)=(f t))))" subsection "transitions and moves" diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/meta_theory/ShortExecutions.thy --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Sun Oct 21 16:27:42 2007 +0200 @@ -14,28 +14,9 @@ that has the same trace as ex, but its schedule ends with an external action. *} -consts - -(* LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool"*) - LastActExtsch ::"('a,'s)ioa => 'a Seq => bool" - - Cut ::"('a => bool) => 'a Seq => 'a Seq" - - oraclebuild ::"('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" - -defs - -LastActExtsch_def: - "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)" - -(* LastActExtex_def: - "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *) - -Cut_def: - "Cut P s == oraclebuild P$s$(Filter P$s)" - -oraclebuild_def: - "oraclebuild P == (fix$(LAM h s t. case t of +definition + oraclebuild :: "('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" where + "oraclebuild P = (fix$(LAM h s t. case t of nil => nil | x##xs => (case x of @@ -45,18 +26,26 @@ ) ))" - -axioms +definition + Cut :: "('a => bool) => 'a Seq => 'a Seq" where + "Cut P s = oraclebuild P$s$(Filter P$s)" -Cut_prefixcl_Finite: - "Finite s ==> (? y. s = Cut P s @@ y)" +definition + LastActExtsch :: "('a,'s)ioa => 'a Seq => bool" where + "LastActExtsch A sch = (Cut (%x. x: ext A) sch = sch)" -LastActExtsmall1: - "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))" +(* LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool"*) +(* LastActExtex_def: + "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *) -LastActExtsmall2: - "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2" +axiomatization where + Cut_prefixcl_Finite: "Finite s ==> (? y. s = Cut P s @@ y)" +axiomatization where + LastActExtsmall1: "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))" + +axiomatization where + LastActExtsmall2: "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2" ML {* @@ -71,9 +60,9 @@ lemma oraclebuild_unfold: -"oraclebuild P = (LAM s t. case t of +"oraclebuild P = (LAM s t. case t of nil => nil - | x##xs => + | x##xs => (case x of UU => UU | Def y => (Takewhile (%a.~ P a)$s) @@ -82,7 +71,7 @@ )" apply (rule trans) apply (rule fix_eq2) -apply (rule oraclebuild_def) +apply (simp only: oraclebuild_def) apply (rule beta_cfun) apply simp done @@ -97,8 +86,8 @@ apply simp done -lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) = - (Takewhile (%a.~ P a)$s) +lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) = + (Takewhile (%a.~ P a)$s) @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))" apply (rule trans) apply (subst oraclebuild_unfold) @@ -109,8 +98,8 @@ subsection "Cut rewrite rules" -lemma Cut_nil: -"[| Forall (%a.~ P a) s; Finite s|] +lemma Cut_nil: +"[| Forall (%a.~ P a) s; Finite s|] ==> Cut P s =nil" apply (unfold Cut_def) apply (subgoal_tac "Filter P$s = nil") @@ -119,8 +108,8 @@ apply assumption+ done -lemma Cut_UU: -"[| Forall (%a.~ P a) s; ~Finite s|] +lemma Cut_UU: +"[| Forall (%a.~ P a) s; ~Finite s|] ==> Cut P s =UU" apply (unfold Cut_def) apply (subgoal_tac "Filter P$s= UU") @@ -129,9 +118,9 @@ apply assumption+ done -lemma Cut_Cons: -"[| P t; Forall (%x.~ P x) ss; Finite ss|] - ==> Cut P (ss @@ (t>> rs)) +lemma Cut_Cons: +"[| P t; Forall (%x.~ P x) ss; Finite ss|] + ==> Cut P (ss @@ (t>> rs)) = ss @@ (t >> Cut P rs)" apply (unfold Cut_def) apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc) @@ -227,10 +216,10 @@ subsection "Main Cut Theorem" -lemma exists_LastActExtsch: - "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|] - ==> ? sch. sch : schedules A & - tr = Filter (%a. a:ext A)$sch & +lemma exists_LastActExtsch: + "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|] + ==> ? sch. sch : schedules A & + tr = Filter (%a. a:ext A)$sch & LastActExtsch A sch" apply (unfold schedules_def has_schedule_def) @@ -265,8 +254,8 @@ subsection "Further Cut lemmas" -lemma LastActExtimplnil: - "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |] +lemma LastActExtimplnil: + "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |] ==> sch=nil" apply (unfold LastActExtsch_def) apply (drule FilternPnilForallP) @@ -276,8 +265,8 @@ apply simp done -lemma LastActExtimplUU: - "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |] +lemma LastActExtimplUU: + "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |] ==> sch=UU" apply (unfold LastActExtsch_def) apply (drule FilternPUUForallP) diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/meta_theory/SimCorrectness.thy --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Sun Oct 21 16:27:42 2007 +0200 @@ -9,25 +9,11 @@ imports Simulations begin -consts - - corresp_ex_sim ::"('a,'s2)ioa => (('s1 *'s2)set) => - ('a,'s1)execution => ('a,'s2)execution" +definition (* Note: s2 instead of s1 in last argument type !! *) - corresp_ex_simC ::"('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs - -> ('s2 => ('a,'s2)pairs)" - - -defs - -corresp_ex_sim_def: - "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A) - in - (S',(corresp_ex_simC A R$(snd ex)) S')" - - -corresp_ex_simC_def: - "corresp_ex_simC A R == (fix$(LAM h ex. (%s. case ex of + corresp_ex_simC :: "('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs + -> ('s2 => ('a,'s2)pairs)" where + "corresp_ex_simC A R = (fix$(LAM h ex. (%s. case ex of nil => nil | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr); T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' @@ -36,20 +22,27 @@ @@ ((h$xs) T')) $x) )))" +definition + corresp_ex_sim :: "('a,'s2)ioa => (('s1 *'s2)set) => + ('a,'s1)execution => ('a,'s2)execution" where + "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A) + in + (S',(corresp_ex_simC A R$(snd ex)) S')" + subsection "corresp_ex_sim" -lemma corresp_ex_simC_unfold: "corresp_ex_simC A R = (LAM ex. (%s. case ex of - nil => nil - | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr); - T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' - in - (@cex. move A cex s a T') - @@ ((corresp_ex_simC A R $xs) T')) +lemma corresp_ex_simC_unfold: "corresp_ex_simC A R = (LAM ex. (%s. case ex of + nil => nil + | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr); + T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' + in + (@cex. move A cex s a T') + @@ ((corresp_ex_simC A R $xs) T')) $x) ))" apply (rule trans) apply (rule fix_eq2) -apply (rule corresp_ex_simC_def) +apply (simp only: corresp_ex_simC_def) apply (rule beta_cfun) apply (simp add: flift1_def) done @@ -64,10 +57,10 @@ apply simp done -lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)>>xs)) s = - (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' - in - (@cex. move A cex s a T') +lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)>>xs)) s = + (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' + in + (@cex. move A cex s a T') @@ ((corresp_ex_simC A R$xs) T'))" apply (rule trans) apply (subst corresp_ex_simC_unfold) @@ -83,9 +76,9 @@ declare Let_def [simp del] -lemma move_is_move_sim: - "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==> - let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in +lemma move_is_move_sim: + "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==> + let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'" apply (unfold is_simulation_def) @@ -113,9 +106,9 @@ declare Let_def [simp] -lemma move_subprop1_sim: - "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> - let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in +lemma move_subprop1_sim: + "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> + let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in is_exec_frag A (s',@x. move A x s' a T')" apply (cut_tac move_is_move_sim) defer @@ -123,9 +116,9 @@ apply (simp add: move_def) done -lemma move_subprop2_sim: - "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> - let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in +lemma move_subprop2_sim: + "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> + let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in Finite (@x. move A x s' a T')" apply (cut_tac move_is_move_sim) defer @@ -133,9 +126,9 @@ apply (simp add: move_def) done -lemma move_subprop3_sim: - "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> - let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in +lemma move_subprop3_sim: + "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> + let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in laststate (s',@x. move A x s' a T') = T'" apply (cut_tac move_is_move_sim) defer @@ -143,10 +136,10 @@ apply (simp add: move_def) done -lemma move_subprop4_sim: - "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> - let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in - mk_trace A$((@x. move A x s' a T')) = +lemma move_subprop4_sim: + "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> + let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in + mk_trace A$((@x. move A x s' a T')) = (if a:ext A then a>>nil else nil)" apply (cut_tac move_is_move_sim) defer @@ -154,9 +147,9 @@ apply (simp add: move_def) done -lemma move_subprop5_sim: - "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> - let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in +lemma move_subprop5_sim: + "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> + let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in (t,T'):R" apply (cut_tac move_is_move_sim) defer @@ -174,9 +167,9 @@ ------------------------------------------------------- *) declare split_if [split del] -lemma traces_coincide_sim [rule_format (no_asm)]: - "[|is_simulation R C A; ext C = ext A|] ==> - !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> +lemma traces_coincide_sim [rule_format (no_asm)]: + "[|is_simulation R C A; ext C = ext A|] ==> + !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')" apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *}) @@ -200,9 +193,9 @@ (* ----------------------------------------------------------- *) -lemma correspsim_is_execution [rule_format (no_asm)]: - "[| is_simulation R C A |] ==> - !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R +lemma correspsim_is_execution [rule_format (no_asm)]: + "[| is_simulation R C A |] ==> + !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')" apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *}) @@ -244,9 +237,9 @@ traces_coincide_sim, the second for the start state case. S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C *) -lemma simulation_starts: -"[| is_simulation R C A; s:starts_of C |] - ==> let S' = @s'. (s,s'):R & s':starts_of A in +lemma simulation_starts: +"[| is_simulation R C A; s:starts_of C |] + ==> let S' = @s'. (s,s'):R & s':starts_of A in (s,S'):R & S':starts_of A" apply (simp add: is_simulation_def corresp_ex_sim_def Int_non_empty Image_def) apply (erule conjE)+ @@ -262,8 +255,8 @@ lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2, standard] -lemma trace_inclusion_for_simulations: - "[| ext C = ext A; is_simulation R C A |] +lemma trace_inclusion_for_simulations: + "[| ext C = ext A; is_simulation R C A |] ==> traces C <= traces A" apply (unfold traces_def) diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/IOA/meta_theory/Simulations.thy --- a/src/HOLCF/IOA/meta_theory/Simulations.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/IOA/meta_theory/Simulations.thy Sun Oct 21 16:27:42 2007 +0200 @@ -11,56 +11,51 @@ defaultsort type -consts - - is_simulation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" - is_backward_simulation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" - is_forw_back_simulation ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" - is_back_forw_simulation ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" - is_history_relation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" - is_prophecy_relation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" - -defs - -is_simulation_def: - "is_simulation R C A == - (!s:starts_of C. R``{s} Int starts_of A ~= {}) & +definition + is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where + "is_simulation R C A = + ((!s:starts_of C. R``{s} Int starts_of A ~= {}) & (!s s' t a. reachable C s & s -a--C-> t & (s,s') : R - --> (? t' ex. (t,t'):R & move A ex s' a t'))" + --> (? t' ex. (t,t'):R & move A ex s' a t')))" -is_backward_simulation_def: - "is_backward_simulation R C A == - (!s:starts_of C. R``{s} <= starts_of A) & +definition + is_backward_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where + "is_backward_simulation R C A = + ((!s:starts_of C. R``{s} <= starts_of A) & (!s t t' a. reachable C s & s -a--C-> t & (t,t') : R - --> (? ex s'. (s,s'):R & move A ex s' a t'))" + --> (? ex s'. (s,s'):R & move A ex s' a t')))" -is_forw_back_simulation_def: - "is_forw_back_simulation R C A == - (!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) & +definition + is_forw_back_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where + "is_forw_back_simulation R C A = + ((!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) & (!s S' t a. reachable C s & s -a--C-> t & (s,S') : R - --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t')))" + --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t'))))" -is_back_forw_simulation_def: - "is_back_forw_simulation R C A == - (!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) & +definition + is_back_forw_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where + "is_back_forw_simulation R C A = + ((!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) & (!s t T' a. reachable C s & s -a--C-> t & (t,T') : R - --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t')))" + --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t'))))" -is_history_relation_def: - "is_history_relation R C A == is_simulation R C A & - is_ref_map (%x.(@y. (x,y):(R^-1))) A C" +definition + is_history_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where + "is_history_relation R C A = (is_simulation R C A & + is_ref_map (%x.(@y. (x,y):(R^-1))) A C)" -is_prophecy_relation_def: - "is_prophecy_relation R C A == is_backward_simulation R C A & - is_ref_map (%x.(@y. (x,y):(R^-1))) A C" +definition + is_prophecy_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where + "is_prophecy_relation R C A = (is_backward_simulation R C A & + is_ref_map (%x.(@y. (x,y):(R^-1))) A C)" lemma set_non_empty: "(A~={}) = (? x. x:A)" @@ -72,7 +67,7 @@ done -lemma Sim_start_convert: +lemma Sim_start_convert: "(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)" apply (unfold Image_def) apply (simp add: Int_non_empty) @@ -81,7 +76,7 @@ declare Sim_start_convert [simp] -lemma ref_map_is_simulation: +lemma ref_map_is_simulation: "!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A" apply (unfold is_ref_map_def is_simulation_def) diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/Sprod.thy --- a/src/HOLCF/Sprod.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/Sprod.thy Sun Oct 21 16:27:42 2007 +0200 @@ -30,22 +30,25 @@ subsection {* Definitions of constants *} -consts - sfst :: "('a ** 'b) \ 'a" - ssnd :: "('a ** 'b) \ 'b" - spair :: "'a \ 'b \ ('a ** 'b)" - ssplit :: "('a \ 'b \ 'c) \ ('a ** 'b) \ 'c" +definition + sfst :: "('a ** 'b) \ 'a" where + "sfst = (\ p. cfst\(Rep_Sprod p))" + +definition + ssnd :: "('a ** 'b) \ 'b" where + "ssnd = (\ p. csnd\(Rep_Sprod p))" -defs - sfst_def: "sfst \ \ p. cfst\(Rep_Sprod p)" - ssnd_def: "ssnd \ \ p. csnd\(Rep_Sprod p)" - spair_def: "spair \ \ a b. Abs_Sprod - (\ b. a)\b, strictify\(\ a. b)\a>" - ssplit_def: "ssplit \ \ f. strictify\(\ p. f\(sfst\p)\(ssnd\p))" +definition + spair :: "'a \ 'b \ ('a ** 'b)" where + "spair = (\ a b. Abs_Sprod + (\ b. a)\b, strictify\(\ a. b)\a>)" -syntax +definition + ssplit :: "('a \ 'b \ 'c) \ ('a ** 'b) \ 'c" where + "ssplit = (\ f. strictify\(\ p. f\(sfst\p)\(ssnd\p)))" + +syntax "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") - translations "(:x, y, z:)" == "(:x, (:y, z:):)" "(:x, y:)" == "CONST spair\x\y" @@ -53,6 +56,7 @@ translations "\(CONST spair\x\y). t" == "CONST ssplit\(\ x y. t)" + subsection {* Case analysis *} lemma spair_Abs_Sprod: @@ -92,7 +96,7 @@ lemma spair_strict_rev: "(:x, y:) \ \ \ x \ \ \ y \ \" by (erule contrapos_np, auto) -lemma spair_defined [simp]: +lemma spair_defined [simp]: "\x \ \; y \ \\ \ (:x, y:) \ \" by (simp add: spair_Abs_Sprod Abs_Sprod_defined Sprod_def) diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/Tr.thy --- a/src/HOLCF/Tr.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/Tr.thy Sun Oct 21 16:27:42 2007 +0200 @@ -17,47 +17,55 @@ tr = "bool lift" translations - "tr" <= (type) "bool lift" + "tr" <= (type) "bool lift" + +definition + TT :: "tr" where + "TT = Def True" -consts - TT :: "tr" - FF :: "tr" - trifte :: "'c \ 'c \ tr \ 'c" - trand :: "tr \ tr \ tr" - tror :: "tr \ tr \ tr" - neg :: "tr \ tr" - If2 :: "[tr, 'c, 'c] \ 'c" +definition + FF :: "tr" where + "FF = Def False" +definition + trifte :: "'c \ 'c \ tr \ 'c" where + ifte_def: "trifte = (\ t e. FLIFT b. if b then t else e)" abbreviation cifte_syn :: "[tr, 'c, 'c] \ 'c" ("(3If _/ (then _/ else _) fi)" 60) where "If b then e1 else e2 fi == trifte\e1\e2\b" +definition + trand :: "tr \ tr \ tr" where + andalso_def: "trand = (\ x y. If x then y else FF fi)" abbreviation andalso_syn :: "tr \ tr \ tr" ("_ andalso _" [36,35] 35) where "x andalso y == trand\x\y" +definition + tror :: "tr \ tr \ tr" where + orelse_def: "tror = (\ x y. If x then TT else y fi)" abbreviation orelse_syn :: "tr \ tr \ tr" ("_ orelse _" [31,30] 30) where "x orelse y == tror\x\y" - -translations - "\ TT. t" == "trifte\t\\" - "\ FF. t" == "trifte\\\t" + +definition + neg :: "tr \ tr" where + "neg = flift2 Not" -defs - TT_def: "TT \ Def True" - FF_def: "FF \ Def False" - neg_def: "neg \ flift2 Not" - ifte_def: "trifte \ \ t e. FLIFT b. if b then t else e" - andalso_def: "trand \ \ x y. If x then y else FF fi" - orelse_def: "tror \ \ x y. If x then TT else y fi" - If2_def: "If2 Q x y \ If Q then x else y fi" +definition + If2 :: "[tr, 'c, 'c] \ 'c" where + "If2 Q x y = (If Q then x else y fi)" + +translations + "\ (CONST TT). t" == "CONST trifte\t\\" + "\ (CONST FF). t" == "CONST trifte\\\t" + text {* Exhaustion and Elimination for type @{typ tr} *} lemma Exh_tr: "t = \ \ t = TT \ t = FF" apply (unfold FF_def TT_def) -apply (induct_tac "t") +apply (induct t) apply fast apply fast done @@ -78,7 +86,7 @@ (fn prems => [ (res_inst_tac [("p","y")] trE 1), - (REPEAT(asm_simp_tac (simpset() addsimps + (REPEAT(asm_simp_tac (simpset() addsimps [o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1)) ]) *) @@ -129,8 +137,8 @@ by (simp_all add: neg_def TT_def FF_def) text {* split-tac for If via If2 because the constant has to be a constant *} - -lemma split_If2: + +lemma split_If2: "P (If2 Q x y) = ((Q = \ \ P \) \ (Q = TT \ P x) \ (Q = FF \ P y))" apply (unfold If2_def) apply (rule_tac p = "Q" in trE) @@ -139,13 +147,13 @@ ML {* val split_If_tac = - simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")]) - THEN' (split_tac [thm "split_If2"]) + simp_tac (HOL_basic_ss addsimps [@{thm If2_def} RS sym]) + THEN' (split_tac [@{thm split_If2}]) *} subsection "Rewriting of HOLCF operations to HOL functions" -lemma andalso_or: +lemma andalso_or: "t \ \ \ ((t andalso s) = FF) = (t = FF \ s = FF)" apply (rule_tac p = "t" in trE) apply simp_all @@ -169,7 +177,7 @@ lemma Def_bool4 [simp]: "(Def x \ TT) = (\ x)" by (simp add: TT_def) -lemma If_and_if: +lemma If_and_if: "(If Def P then A else B fi) = (if P then A else B)" apply (rule_tac p = "Def P" in trE) apply (auto simp add: TT_def[symmetric] FF_def[symmetric]) diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/ex/Dagstuhl.thy --- a/src/HOLCF/ex/Dagstuhl.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/ex/Dagstuhl.thy Sun Oct 21 16:27:42 2007 +0200 @@ -4,7 +4,7 @@ imports Stream begin -consts +axiomatization y :: "'a" definition diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/ex/Fix2.thy --- a/src/HOLCF/ex/Fix2.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/ex/Fix2.thy Sun Oct 21 16:27:42 2007 +0200 @@ -10,11 +10,9 @@ imports HOLCF begin -consts - gix :: "('a->'a)->'a" - -axioms - gix1_def: "F$(gix$F) = gix$F" +axiomatization + gix :: "('a->'a)->'a" where + gix1_def: "F$(gix$F) = gix$F" and gix2_def: "F$y=y ==> gix$F << y" diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/ex/Focus_ex.thy --- a/src/HOLCF/ex/Focus_ex.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/ex/Focus_ex.thy Sun Oct 21 16:27:42 2007 +0200 @@ -107,7 +107,7 @@ typedecl ('a, 'b) tc arities tc:: (pcpo, pcpo) pcpo -consts +axiomatization Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool" definition diff -r 3d4953e88449 -r 4f8176c940cf src/HOLCF/ex/Hoare.thy --- a/src/HOLCF/ex/Hoare.thy Sun Oct 21 14:53:44 2007 +0200 +++ b/src/HOLCF/ex/Hoare.thy Sun Oct 21 16:27:42 2007 +0200 @@ -24,9 +24,9 @@ imports HOLCF begin -consts - b1 :: "'a -> tr" - b2 :: "'a -> tr" +axiomatization + b1 :: "'a -> tr" and + b2 :: "'a -> tr" and g :: "'a -> 'a" definition