# HG changeset patch # User wenzelm # Date 1214421951 -7200 # Node ID 24ec32bee347f14680d5a9b59958f3a2b5dccab6 # Parent a0189ff58b7ce5a8162b094cf8950409935c2ded modernized specifications; diff -r a0189ff58b7c -r 24ec32bee347 src/HOLCF/IOA/ABP/Abschannel_finite.thy --- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy Wed Jun 25 18:23:50 2008 +0200 +++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy Wed Jun 25 21:25:51 2008 +0200 @@ -9,10 +9,10 @@ imports Abschannel IOA Action Lemmas begin -consts reverse :: "'a list => 'a list" -primrec +primrec reverse :: "'a list => 'a list" +where reverse_Nil: "reverse([]) = []" - reverse_Cons: "reverse(x#xs) = reverse(xs)@[x]" +| reverse_Cons: "reverse(x#xs) = reverse(xs)@[x]" definition ch_fin_asig :: "'a abs_action signature" where diff -r a0189ff58b7c -r 24ec32bee347 src/HOLCF/IOA/ABP/Correctness.thy --- a/src/HOLCF/IOA/ABP/Correctness.thy Wed Jun 25 18:23:50 2008 +0200 +++ b/src/HOLCF/IOA/ABP/Correctness.thy Wed Jun 25 21:25:51 2008 +0200 @@ -9,11 +9,10 @@ imports IOA Env Impl Impl_finite begin -consts - reduce :: "'a list => 'a list" -primrec +primrec reduce :: "'a list => 'a list" +where reduce_Nil: "reduce [] = []" - reduce_Cons: "reduce(x#xs) = +| reduce_Cons: "reduce(x#xs) = (case xs of [] => [x] | y#ys => (if (x=y) diff -r a0189ff58b7c -r 24ec32bee347 src/HOLCF/IOA/NTP/Abschannel.thy --- a/src/HOLCF/IOA/NTP/Abschannel.thy Wed Jun 25 18:23:50 2008 +0200 +++ b/src/HOLCF/IOA/NTP/Abschannel.thy Wed Jun 25 21:25:51 2008 +0200 @@ -11,65 +11,28 @@ datatype 'a abs_action = S 'a | R 'a -consts - -ch_asig :: "'a abs_action signature" - -ch_trans :: "('a abs_action, 'a multiset)transition set" - -ch_ioa :: "('a abs_action, 'a multiset)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_wfair :: "('m action)set set" -srch_sfair :: "('m action)set set" -rsch_sfair :: "('m action)set set" -rsch_wfair :: "('m action)set set" - -srch_trans :: "('m action, 'm packet multiset)transition set" -rsch_trans :: "('m action, bool multiset)transition set" - -srch_ioa :: "('m action, 'm packet multiset)ioa" -rsch_ioa :: "('m action, bool multiset)ioa" - - -defs +definition + ch_asig :: "'a abs_action signature" where + "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})" -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_wfair_def: "srch_wfair == wfair_of(srch_ioa)" -rsch_wfair_def: "rsch_wfair == wfair_of(rsch_ioa)" - -srch_sfair_def: "srch_sfair == sfair_of(srch_ioa)" -rsch_sfair_def: "rsch_sfair == sfair_of(rsch_ioa)" - -srch_ioa_def: "srch_ioa == rename ch_ioa srch_actions" -rsch_ioa_def: "rsch_ioa == rename ch_ioa rsch_actions" - +definition + ch_trans :: "('a abs_action, 'a multiset)transition set" where + "ch_trans = + {tr. let s = fst(tr); + t = snd(snd(tr)) + in + case fst(snd(tr)) + of S(b) => t = addm s b | + R(b) => count s b ~= 0 & t = delm s b}" -ch_asig_def: "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})" +definition + ch_ioa :: "('a abs_action, 'a multiset)ioa" where + "ch_ioa = (ch_asig, {{|}}, ch_trans,{},{})" -ch_trans_def: "ch_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in - case fst(snd(tr)) - of S(b) => t = addm s b | - R(b) => count s b ~= 0 & t = delm s b}" - -ch_ioa_def: "ch_ioa == (ch_asig, {{|}}, ch_trans,{},{})" - - -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 S_msg(m) => None | R_msg(m) => None | S_pkt(packet) => None | @@ -79,10 +42,12 @@ C_m_s => None | C_m_r => None | C_r_s => None | - C_r_r(m) => None" + C_r_r(m) => None)" -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 S_msg(m) => None | R_msg(m) => None | S_pkt(p) => Some(S(p)) | @@ -92,7 +57,44 @@ C_m_s => None | C_m_r => None | C_r_s => None | - C_r_r(m) => None" + C_r_r(m) => None)" + +definition + srch_ioa :: "('m action, 'm packet multiset)ioa" where + "srch_ioa = rename ch_ioa srch_actions" + +definition + rsch_ioa :: "('m action, bool multiset)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_wfair :: "('m action)set set" where + "srch_wfair = wfair_of(srch_ioa)" +definition + srch_sfair :: "('m action)set set" where + "srch_sfair = sfair_of(srch_ioa)" +definition + rsch_sfair :: "('m action)set set" where + "rsch_sfair = sfair_of(rsch_ioa)" +definition + rsch_wfair :: "('m action)set set" where + "rsch_wfair = wfair_of(rsch_ioa)" + +definition + srch_trans :: "('m action, 'm packet multiset)transition set" where + "srch_trans = trans_of(srch_ioa)" +definition + rsch_trans :: "('m action, bool multiset)transition set" where + "rsch_trans = trans_of(rsch_ioa)" + lemmas unfold_renaming = srch_asig_def rsch_asig_def rsch_ioa_def srch_ioa_def ch_ioa_def @@ -110,7 +112,6 @@ C_m_s ~: actions(srch_asig) & C_m_r ~: actions(srch_asig) & C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)" - by (simp add: unfold_renaming) lemma in_rsch_asig: diff -r a0189ff58b7c -r 24ec32bee347 src/HOLCF/IOA/NTP/Impl.thy --- a/src/HOLCF/IOA/NTP/Impl.thy Wed Jun 25 18:23:50 2008 +0200 +++ b/src/HOLCF/IOA/NTP/Impl.thy Wed Jun 25 21:25:51 2008 +0200 @@ -14,39 +14,29 @@ (* sender_state * receiver_state * srch_state * rsch_state *) -consts - impl_ioa :: "('m action, 'm impl_state)ioa" - sen :: "'m impl_state => 'm sender_state" - rec :: "'m impl_state => 'm receiver_state" - srch :: "'m impl_state => 'm packet multiset" - rsch :: "'m impl_state => bool multiset" - inv1 :: "'m impl_state => bool" - inv2 :: "'m impl_state => bool" - inv3 :: "'m impl_state => bool" - inv4 :: "'m impl_state => bool" - hdr_sum :: "'m packet multiset => bool => nat" +definition + impl_ioa :: "('m action, 'm impl_state)ioa" where + impl_def: "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" -defs - impl_def: - "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" +definition sen :: "'m impl_state => 'm sender_state" where "sen = fst" +definition rec :: "'m impl_state => 'm receiver_state" where "rec = fst o snd" +definition srch :: "'m impl_state => 'm packet multiset" where "srch = fst o snd o snd" +definition rsch :: "'m impl_state => bool multiset" where "rsch = snd o snd o snd" - sen_def: "sen == fst" - rec_def: "rec == fst o snd" - srch_def: "srch == fst o snd o snd" - rsch_def: "rsch == snd o snd o snd" - -hdr_sum_def: - "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)" +definition + hdr_sum :: "'m packet multiset => bool => nat" where + "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)" (* Lemma 5.1 *) -inv1_def: +definition "inv1(s) == (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) & (!b. count (ssent(sen s)) b = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)" (* Lemma 5.2 *) - inv2_def: "inv2(s) == +definition + "inv2(s) == (rbit(rec(s)) = sbit(sen(s)) & ssending(sen(s)) & count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) & @@ -58,7 +48,8 @@ count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))" (* Lemma 5.3 *) - inv3_def: "inv3(s) == +definition + "inv3(s) == rbit(rec(s)) = sbit(sen(s)) --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s))) --> count (rrcvd(rec s)) (sbit(sen(s)),m) @@ -66,7 +57,7 @@ <= count (rsent(rec s)) (~sbit(sen s)))" (* Lemma 5.4 *) - inv4_def: "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []" +definition "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []" subsection {* Invariants *} @@ -229,7 +220,8 @@ (@{thm raw_inv1} RS @{thm invariantE})] 1 *}) apply (tactic "tac2 1") - apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *}) + apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}] + (@{thm Impl.hdr_sum_def})] *}) apply arith txt {* 2 *} diff -r a0189ff58b7c -r 24ec32bee347 src/HOLCF/IOA/NTP/Receiver.thy --- a/src/HOLCF/IOA/NTP/Receiver.thy Wed Jun 25 18:23:50 2008 +0200 +++ b/src/HOLCF/IOA/NTP/Receiver.thy Wed Jun 25 21:25:51 2008 +0200 @@ -15,31 +15,22 @@ = "'m list * bool multiset * 'm packet multiset * bool * bool" (* messages #replies #received header mode *) -consts - - receiver_asig :: "'m action signature" - receiver_trans:: "('m action, 'm receiver_state)transition set" - receiver_ioa :: "('m action, 'm receiver_state)ioa" - rq :: "'m receiver_state => 'm list" - rsent :: "'m receiver_state => bool multiset" - rrcvd :: "'m receiver_state => 'm packet multiset" - rbit :: "'m receiver_state => bool" - rsending :: "'m receiver_state => bool" - -defs +definition rq :: "'m receiver_state => 'm list" where "rq == fst" +definition rsent :: "'m receiver_state => bool multiset" where "rsent == fst o snd" +definition rrcvd :: "'m receiver_state => 'm packet multiset" where "rrcvd == fst o snd o snd" +definition rbit :: "'m receiver_state => bool" where "rbit == fst o snd o snd o snd" +definition rsending :: "'m receiver_state => bool" where "rsending == snd o snd o snd o snd" -rq_def: "rq == fst" -rsent_def: "rsent == fst o snd" -rrcvd_def: "rrcvd == fst o snd o snd" -rbit_def: "rbit == fst o snd o snd o snd" -rsending_def: "rsending == snd o snd o snd o snd" +definition + receiver_asig :: "'m action signature" where + "receiver_asig = + (UN pkt. {R_pkt(pkt)}, + (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), + insert C_m_r (UN m. {C_r_r(m)}))" -receiver_asig_def: "receiver_asig == - (UN pkt. {R_pkt(pkt)}, - (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), - insert C_m_r (UN m. {C_r_r(m)}))" - -receiver_trans_def: "receiver_trans == +definition + receiver_trans:: "('m action, 'm receiver_state)transition set" where +"receiver_trans = {tr. let s = fst(tr); t = snd(snd(tr)) in @@ -83,9 +74,10 @@ ~rsending(s) & rsending(t)}" - -receiver_ioa_def: "receiver_ioa == - (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})" +definition + receiver_ioa :: "('m action, 'm receiver_state)ioa" where + "receiver_ioa = + (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})" lemma in_receiver_asig: "S_msg(m) ~: actions(receiver_asig)" diff -r a0189ff58b7c -r 24ec32bee347 src/HOLCF/IOA/NTP/Sender.thy --- a/src/HOLCF/IOA/NTP/Sender.thy Wed Jun 25 18:23:50 2008 +0200 +++ b/src/HOLCF/IOA/NTP/Sender.thy Wed Jun 25 21:25:51 2008 +0200 @@ -13,31 +13,21 @@ 'm sender_state = "'m list * bool multiset * bool multiset * bool * bool" (* messages #sent #received header mode *) -consts - -sender_asig :: "'m action signature" -sender_trans :: "('m action, 'm sender_state)transition set" -sender_ioa :: "('m action, 'm sender_state)ioa" -sq :: "'m sender_state => 'm list" -ssent :: "'m sender_state => bool multiset" -srcvd :: "'m sender_state => bool multiset" -sbit :: "'m sender_state => bool" -ssending :: "'m sender_state => bool" - -defs +definition sq :: "'m sender_state => 'm list" where "sq = fst" +definition ssent :: "'m sender_state => bool multiset" where "ssent = fst o snd" +definition srcvd :: "'m sender_state => bool multiset" where "srcvd = fst o snd o snd" +definition sbit :: "'m sender_state => bool" where "sbit = fst o snd o snd o snd" +definition ssending :: "'m sender_state => bool" where "ssending = snd o snd o snd o snd" -sq_def: "sq == fst" -ssent_def: "ssent == fst o snd" -srcvd_def: "srcvd == fst o snd o snd" -sbit_def: "sbit == fst o snd o snd o snd" -ssending_def: "ssending == snd o snd o snd o snd" +definition + sender_asig :: "'m action signature" where + "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), + UN pkt. {S_pkt(pkt)}, + {C_m_s,C_r_s})" -sender_asig_def: - "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), - UN pkt. {S_pkt(pkt)}, - {C_m_s,C_r_s})" - -sender_trans_def: "sender_trans == +definition + sender_trans :: "('m action, 'm sender_state)transition set" where + "sender_trans = {tr. let s = fst(tr); t = snd(snd(tr)) in case fst(snd(tr)) @@ -80,8 +70,10 @@ ssending(t) | C_r_r(m) => False}" -sender_ioa_def: "sender_ioa == - (sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})" +definition + sender_ioa :: "('m action, 'm sender_state)ioa" where + "sender_ioa = + (sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})" lemma in_sender_asig: "S_msg(m) : actions(sender_asig)" diff -r a0189ff58b7c -r 24ec32bee347 src/HOLCF/IOA/NTP/Spec.thy --- a/src/HOLCF/IOA/NTP/Spec.thy Wed Jun 25 18:23:50 2008 +0200 +++ b/src/HOLCF/IOA/NTP/Spec.thy Wed Jun 25 21:25:51 2008 +0200 @@ -9,35 +9,33 @@ 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)}, - {})" +definition + spec_sig :: "'m action signature" where + sig_def: "spec_sig = (UN m.{S_msg(m)}, + UN m.{R_msg(m)}, + {})" -trans_def: "spec_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in - case fst(snd(tr)) - of - 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 | - C_m_s => False | - C_m_r => False | - C_r_s => False | - C_r_r(m) => 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 + 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 | + C_m_s => False | + C_m_r => False | + C_r_s => False | + C_r_r(m) => 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 a0189ff58b7c -r 24ec32bee347 src/HOLCF/IOA/Storage/Correctness.thy --- a/src/HOLCF/IOA/Storage/Correctness.thy Wed Jun 25 18:23:50 2008 +0200 +++ b/src/HOLCF/IOA/Storage/Correctness.thy Wed Jun 25 21:25:51 2008 +0200 @@ -35,30 +35,30 @@ txt {* start states *} apply (auto)[1] apply (rule_tac x = " ({},False) " in exI) -apply (simp add: sim_relation_def starts_of_def Spec.ioa_def Impl.ioa_def) +apply (simp add: sim_relation_def starts_of_def spec_ioa_def impl_ioa_def) txt {* main-part *} apply (rule allI)+ apply (rule imp_conj_lemma) apply (rename_tac k b used c k' b' a) apply (induct_tac "a") -apply (simp_all (no_asm) add: sim_relation_def Impl.ioa_def Impl.trans_def trans_of_def) +apply (simp_all (no_asm) add: sim_relation_def impl_ioa_def impl_trans_def trans_of_def) apply auto txt {* NEW *} apply (rule_tac x = "(used,True)" in exI) apply simp apply (rule transition_is_ex) -apply (simp (no_asm) add: Spec.ioa_def Spec.trans_def trans_of_def) +apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) txt {* LOC *} apply (rule_tac x = " (used Un {k},False) " in exI) apply (simp add: less_SucI) apply (rule transition_is_ex) -apply (simp (no_asm) add: Spec.ioa_def Spec.trans_def trans_of_def) +apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) apply fast txt {* FREE *} apply (rule_tac x = " (used - {nat},c) " in exI) apply simp apply (rule transition_is_ex) -apply (simp (no_asm) add: Spec.ioa_def Spec.trans_def trans_of_def) +apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) done @@ -66,10 +66,10 @@ "impl_ioa =<| spec_ioa" apply (unfold ioa_implements_def) apply (rule conjI) -apply (simp (no_asm) add: Impl.sig_def Spec.sig_def Impl.ioa_def Spec.ioa_def +apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def asig_outputs_def asig_of_def asig_inputs_def) apply (rule trace_inclusion_for_simulations) -apply (simp (no_asm) add: Impl.sig_def Spec.sig_def Impl.ioa_def Spec.ioa_def +apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def externals_def asig_outputs_def asig_of_def asig_inputs_def) apply (rule issimulation) done diff -r a0189ff58b7c -r 24ec32bee347 src/HOLCF/IOA/Storage/Impl.thy --- a/src/HOLCF/IOA/Storage/Impl.thy Wed Jun 25 18:23:50 2008 +0200 +++ b/src/HOLCF/IOA/Storage/Impl.thy Wed Jun 25 21:25:51 2008 +0200 @@ -9,34 +9,32 @@ imports IOA Action begin -consts - -impl_sig :: "action signature" -impl_trans :: "(action, nat * bool)transition set" -impl_ioa :: "(action, nat * bool)ioa" - -defs - -sig_def: "impl_sig == (UN l.{Free l} Un {New}, - UN l.{Loc l}, - {})" +definition + impl_sig :: "action signature" where + "impl_sig = (UN l.{Free l} Un {New}, + UN l.{Loc l}, + {})" -trans_def: "impl_trans == - {tr. let s = fst(tr); k = fst s; b = snd s; - t = snd(snd(tr)); k' = fst t; b' = snd t - in - case fst(snd(tr)) - of - New => k' = k & b' | - Loc l => b & l= k & k'= (Suc k) & ~b' | - Free l => k'=k & b'=b}" +definition + impl_trans :: "(action, nat * bool)transition set" where + "impl_trans = + {tr. let s = fst(tr); k = fst s; b = snd s; + t = snd(snd(tr)); k' = fst t; b' = snd t + in + case fst(snd(tr)) + of + New => k' = k & b' | + Loc l => b & l= k & k'= (Suc k) & ~b' | + Free l => k'=k & b'=b}" -ioa_def: "impl_ioa == (impl_sig, {(0,False)}, impl_trans,{},{})" +definition + impl_ioa :: "(action, nat * bool)ioa" where + "impl_ioa = (impl_sig, {(0,False)}, impl_trans,{},{})" lemma in_impl_asig: "New : actions(impl_sig) & Loc l : actions(impl_sig) & Free l : actions(impl_sig) " - by (simp add: Impl.sig_def actions_def asig_projections) + by (simp add: impl_sig_def actions_def asig_projections) end diff -r a0189ff58b7c -r 24ec32bee347 src/HOLCF/IOA/Storage/Spec.thy --- a/src/HOLCF/IOA/Storage/Spec.thy Wed Jun 25 18:23:50 2008 +0200 +++ b/src/HOLCF/IOA/Storage/Spec.thy Wed Jun 25 21:25:51 2008 +0200 @@ -9,28 +9,26 @@ imports IOA Action begin -consts - -spec_sig :: "action signature" -spec_trans :: "(action, nat set * bool)transition set" -spec_ioa :: "(action, nat set * bool)ioa" - -defs - -sig_def: "spec_sig == (UN l.{Free l} Un {New}, - UN l.{Loc l}, - {})" +definition + spec_sig :: "action signature" where + "spec_sig = (UN l.{Free l} Un {New}, + UN l.{Loc l}, + {})" -trans_def: "spec_trans == - {tr. let s = fst(tr); used = fst s; c = snd s; - t = snd(snd(tr)); used' = fst t; c' = snd t - in - case fst(snd(tr)) - of - New => used' = used & c' | - Loc l => c & l~:used & used'= used Un {l} & ~c' | - Free l => used'=used - {l} & c'=c}" +definition + spec_trans :: "(action, nat set * bool)transition set" where + "spec_trans = + {tr. let s = fst(tr); used = fst s; c = snd s; + t = snd(snd(tr)); used' = fst t; c' = snd t + in + case fst(snd(tr)) + of + New => used' = used & c' | + Loc l => c & l~:used & used'= used Un {l} & ~c' | + Free l => used'=used - {l} & c'=c}" -ioa_def: "spec_ioa == (spec_sig, {({},False)}, spec_trans,{},{})" +definition + spec_ioa :: "(action, nat set * bool)ioa" where + "spec_ioa = (spec_sig, {({},False)}, spec_trans,{},{})" end diff -r a0189ff58b7c -r 24ec32bee347 src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Wed Jun 25 18:23:50 2008 +0200 +++ b/src/HOLCF/ex/Stream.thy Wed Jun 25 21:25:51 2008 +0200 @@ -41,11 +41,10 @@ Fin n \ (SOME s. (stream_take n$s=s1) & (i_rt n s = s2)) | \ \ s1)" -consts - constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" -primrec +primrec constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" +where constr_sconc'_0: "constr_sconc' 0 s1 s2 = s2" - constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 && +| constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 && constr_sconc' n (rt$s1) s2" definition