--- 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
--- 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)
--- 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:
--- 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 *}
--- 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)"
--- 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)"
--- 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
--- 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
--- 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
--- 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
--- 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 \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
| \<infinity> \<Rightarrow> 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