1.1 --- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy Wed Jun 25 18:23:50 2008 +0200
1.2 +++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy Wed Jun 25 21:25:51 2008 +0200
1.3 @@ -9,10 +9,10 @@
1.4 imports Abschannel IOA Action Lemmas
1.5 begin
1.6
1.7 -consts reverse :: "'a list => 'a list"
1.8 -primrec
1.9 +primrec reverse :: "'a list => 'a list"
1.10 +where
1.11 reverse_Nil: "reverse([]) = []"
1.12 - reverse_Cons: "reverse(x#xs) = reverse(xs)@[x]"
1.13 +| reverse_Cons: "reverse(x#xs) = reverse(xs)@[x]"
1.14
1.15 definition
1.16 ch_fin_asig :: "'a abs_action signature" where
2.1 --- a/src/HOLCF/IOA/ABP/Correctness.thy Wed Jun 25 18:23:50 2008 +0200
2.2 +++ b/src/HOLCF/IOA/ABP/Correctness.thy Wed Jun 25 21:25:51 2008 +0200
2.3 @@ -9,11 +9,10 @@
2.4 imports IOA Env Impl Impl_finite
2.5 begin
2.6
2.7 -consts
2.8 - reduce :: "'a list => 'a list"
2.9 -primrec
2.10 +primrec reduce :: "'a list => 'a list"
2.11 +where
2.12 reduce_Nil: "reduce [] = []"
2.13 - reduce_Cons: "reduce(x#xs) =
2.14 +| reduce_Cons: "reduce(x#xs) =
2.15 (case xs of
2.16 [] => [x]
2.17 | y#ys => (if (x=y)
3.1 --- a/src/HOLCF/IOA/NTP/Abschannel.thy Wed Jun 25 18:23:50 2008 +0200
3.2 +++ b/src/HOLCF/IOA/NTP/Abschannel.thy Wed Jun 25 21:25:51 2008 +0200
3.3 @@ -11,65 +11,28 @@
3.4
3.5 datatype 'a abs_action = S 'a | R 'a
3.6
3.7 -consts
3.8 +definition
3.9 + ch_asig :: "'a abs_action signature" where
3.10 + "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})"
3.11
3.12 -ch_asig :: "'a abs_action signature"
3.13 +definition
3.14 + ch_trans :: "('a abs_action, 'a multiset)transition set" where
3.15 + "ch_trans =
3.16 + {tr. let s = fst(tr);
3.17 + t = snd(snd(tr))
3.18 + in
3.19 + case fst(snd(tr))
3.20 + of S(b) => t = addm s b |
3.21 + R(b) => count s b ~= 0 & t = delm s b}"
3.22
3.23 -ch_trans :: "('a abs_action, 'a multiset)transition set"
3.24 +definition
3.25 + ch_ioa :: "('a abs_action, 'a multiset)ioa" where
3.26 + "ch_ioa = (ch_asig, {{|}}, ch_trans,{},{})"
3.27
3.28 -ch_ioa :: "('a abs_action, 'a multiset)ioa"
3.29 -
3.30 -rsch_actions :: "'m action => bool abs_action option"
3.31 -srch_actions :: "'m action =>(bool * 'm) abs_action option"
3.32 -
3.33 -srch_asig :: "'m action signature"
3.34 -rsch_asig :: "'m action signature"
3.35 -
3.36 -srch_wfair :: "('m action)set set"
3.37 -srch_sfair :: "('m action)set set"
3.38 -rsch_sfair :: "('m action)set set"
3.39 -rsch_wfair :: "('m action)set set"
3.40 -
3.41 -srch_trans :: "('m action, 'm packet multiset)transition set"
3.42 -rsch_trans :: "('m action, bool multiset)transition set"
3.43 -
3.44 -srch_ioa :: "('m action, 'm packet multiset)ioa"
3.45 -rsch_ioa :: "('m action, bool multiset)ioa"
3.46 -
3.47 -
3.48 -defs
3.49 -
3.50 -srch_asig_def: "srch_asig == asig_of(srch_ioa)"
3.51 -rsch_asig_def: "rsch_asig == asig_of(rsch_ioa)"
3.52 -
3.53 -srch_trans_def: "srch_trans == trans_of(srch_ioa)"
3.54 -rsch_trans_def: "rsch_trans == trans_of(rsch_ioa)"
3.55 -
3.56 -srch_wfair_def: "srch_wfair == wfair_of(srch_ioa)"
3.57 -rsch_wfair_def: "rsch_wfair == wfair_of(rsch_ioa)"
3.58 -
3.59 -srch_sfair_def: "srch_sfair == sfair_of(srch_ioa)"
3.60 -rsch_sfair_def: "rsch_sfair == sfair_of(rsch_ioa)"
3.61 -
3.62 -srch_ioa_def: "srch_ioa == rename ch_ioa srch_actions"
3.63 -rsch_ioa_def: "rsch_ioa == rename ch_ioa rsch_actions"
3.64 -
3.65 -
3.66 -ch_asig_def: "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
3.67 -
3.68 -ch_trans_def: "ch_trans ==
3.69 - {tr. let s = fst(tr);
3.70 - t = snd(snd(tr))
3.71 - in
3.72 - case fst(snd(tr))
3.73 - of S(b) => t = addm s b |
3.74 - R(b) => count s b ~= 0 & t = delm s b}"
3.75 -
3.76 -ch_ioa_def: "ch_ioa == (ch_asig, {{|}}, ch_trans,{},{})"
3.77 -
3.78 -
3.79 -rsch_actions_def: "rsch_actions (akt) ==
3.80 - case akt of
3.81 +definition
3.82 + rsch_actions :: "'m action => bool abs_action option" where
3.83 + "rsch_actions (akt) =
3.84 + (case akt of
3.85 S_msg(m) => None |
3.86 R_msg(m) => None |
3.87 S_pkt(packet) => None |
3.88 @@ -79,10 +42,12 @@
3.89 C_m_s => None |
3.90 C_m_r => None |
3.91 C_r_s => None |
3.92 - C_r_r(m) => None"
3.93 + C_r_r(m) => None)"
3.94
3.95 -srch_actions_def: "srch_actions (akt) ==
3.96 - case akt of
3.97 +definition
3.98 + srch_actions :: "'m action =>(bool * 'm) abs_action option" where
3.99 + "srch_actions (akt) =
3.100 + (case akt of
3.101 S_msg(m) => None |
3.102 R_msg(m) => None |
3.103 S_pkt(p) => Some(S(p)) |
3.104 @@ -92,7 +57,44 @@
3.105 C_m_s => None |
3.106 C_m_r => None |
3.107 C_r_s => None |
3.108 - C_r_r(m) => None"
3.109 + C_r_r(m) => None)"
3.110 +
3.111 +definition
3.112 + srch_ioa :: "('m action, 'm packet multiset)ioa" where
3.113 + "srch_ioa = rename ch_ioa srch_actions"
3.114 +
3.115 +definition
3.116 + rsch_ioa :: "('m action, bool multiset)ioa" where
3.117 + "rsch_ioa = rename ch_ioa rsch_actions"
3.118 +
3.119 +definition
3.120 + srch_asig :: "'m action signature" where
3.121 + "srch_asig = asig_of(srch_ioa)"
3.122 +
3.123 +definition
3.124 + rsch_asig :: "'m action signature" where
3.125 + "rsch_asig = asig_of(rsch_ioa)"
3.126 +
3.127 +definition
3.128 + srch_wfair :: "('m action)set set" where
3.129 + "srch_wfair = wfair_of(srch_ioa)"
3.130 +definition
3.131 + srch_sfair :: "('m action)set set" where
3.132 + "srch_sfair = sfair_of(srch_ioa)"
3.133 +definition
3.134 + rsch_sfair :: "('m action)set set" where
3.135 + "rsch_sfair = sfair_of(rsch_ioa)"
3.136 +definition
3.137 + rsch_wfair :: "('m action)set set" where
3.138 + "rsch_wfair = wfair_of(rsch_ioa)"
3.139 +
3.140 +definition
3.141 + srch_trans :: "('m action, 'm packet multiset)transition set" where
3.142 + "srch_trans = trans_of(srch_ioa)"
3.143 +definition
3.144 + rsch_trans :: "('m action, bool multiset)transition set" where
3.145 + "rsch_trans = trans_of(rsch_ioa)"
3.146 +
3.147
3.148 lemmas unfold_renaming =
3.149 srch_asig_def rsch_asig_def rsch_ioa_def srch_ioa_def ch_ioa_def
3.150 @@ -110,7 +112,6 @@
3.151 C_m_s ~: actions(srch_asig) &
3.152 C_m_r ~: actions(srch_asig) &
3.153 C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)"
3.154 -
3.155 by (simp add: unfold_renaming)
3.156
3.157 lemma in_rsch_asig:
4.1 --- a/src/HOLCF/IOA/NTP/Impl.thy Wed Jun 25 18:23:50 2008 +0200
4.2 +++ b/src/HOLCF/IOA/NTP/Impl.thy Wed Jun 25 21:25:51 2008 +0200
4.3 @@ -14,39 +14,29 @@
4.4 (* sender_state * receiver_state * srch_state * rsch_state *)
4.5
4.6
4.7 -consts
4.8 - impl_ioa :: "('m action, 'm impl_state)ioa"
4.9 - sen :: "'m impl_state => 'm sender_state"
4.10 - rec :: "'m impl_state => 'm receiver_state"
4.11 - srch :: "'m impl_state => 'm packet multiset"
4.12 - rsch :: "'m impl_state => bool multiset"
4.13 - inv1 :: "'m impl_state => bool"
4.14 - inv2 :: "'m impl_state => bool"
4.15 - inv3 :: "'m impl_state => bool"
4.16 - inv4 :: "'m impl_state => bool"
4.17 - hdr_sum :: "'m packet multiset => bool => nat"
4.18 +definition
4.19 + impl_ioa :: "('m action, 'm impl_state)ioa" where
4.20 + impl_def: "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
4.21
4.22 -defs
4.23 - impl_def:
4.24 - "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
4.25 +definition sen :: "'m impl_state => 'm sender_state" where "sen = fst"
4.26 +definition rec :: "'m impl_state => 'm receiver_state" where "rec = fst o snd"
4.27 +definition srch :: "'m impl_state => 'm packet multiset" where "srch = fst o snd o snd"
4.28 +definition rsch :: "'m impl_state => bool multiset" where "rsch = snd o snd o snd"
4.29
4.30 - sen_def: "sen == fst"
4.31 - rec_def: "rec == fst o snd"
4.32 - srch_def: "srch == fst o snd o snd"
4.33 - rsch_def: "rsch == snd o snd o snd"
4.34 -
4.35 -hdr_sum_def:
4.36 - "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)"
4.37 +definition
4.38 + hdr_sum :: "'m packet multiset => bool => nat" where
4.39 + "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)"
4.40
4.41 (* Lemma 5.1 *)
4.42 -inv1_def:
4.43 +definition
4.44 "inv1(s) ==
4.45 (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b)
4.46 & (!b. count (ssent(sen s)) b
4.47 = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
4.48
4.49 (* Lemma 5.2 *)
4.50 - inv2_def: "inv2(s) ==
4.51 +definition
4.52 + "inv2(s) ==
4.53 (rbit(rec(s)) = sbit(sen(s)) &
4.54 ssending(sen(s)) &
4.55 count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &
4.56 @@ -58,7 +48,8 @@
4.57 count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
4.58
4.59 (* Lemma 5.3 *)
4.60 - inv3_def: "inv3(s) ==
4.61 +definition
4.62 + "inv3(s) ==
4.63 rbit(rec(s)) = sbit(sen(s))
4.64 --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))
4.65 --> count (rrcvd(rec s)) (sbit(sen(s)),m)
4.66 @@ -66,7 +57,7 @@
4.67 <= count (rsent(rec s)) (~sbit(sen s)))"
4.68
4.69 (* Lemma 5.4 *)
4.70 - inv4_def: "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
4.71 +definition "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
4.72
4.73
4.74 subsection {* Invariants *}
4.75 @@ -229,7 +220,8 @@
4.76 (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
4.77
4.78 apply (tactic "tac2 1")
4.79 - apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
4.80 + apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}]
4.81 + (@{thm Impl.hdr_sum_def})] *})
4.82 apply arith
4.83
4.84 txt {* 2 *}
5.1 --- a/src/HOLCF/IOA/NTP/Receiver.thy Wed Jun 25 18:23:50 2008 +0200
5.2 +++ b/src/HOLCF/IOA/NTP/Receiver.thy Wed Jun 25 21:25:51 2008 +0200
5.3 @@ -15,31 +15,22 @@
5.4 = "'m list * bool multiset * 'm packet multiset * bool * bool"
5.5 (* messages #replies #received header mode *)
5.6
5.7 -consts
5.8 +definition rq :: "'m receiver_state => 'm list" where "rq == fst"
5.9 +definition rsent :: "'m receiver_state => bool multiset" where "rsent == fst o snd"
5.10 +definition rrcvd :: "'m receiver_state => 'm packet multiset" where "rrcvd == fst o snd o snd"
5.11 +definition rbit :: "'m receiver_state => bool" where "rbit == fst o snd o snd o snd"
5.12 +definition rsending :: "'m receiver_state => bool" where "rsending == snd o snd o snd o snd"
5.13
5.14 - receiver_asig :: "'m action signature"
5.15 - receiver_trans:: "('m action, 'm receiver_state)transition set"
5.16 - receiver_ioa :: "('m action, 'm receiver_state)ioa"
5.17 - rq :: "'m receiver_state => 'm list"
5.18 - rsent :: "'m receiver_state => bool multiset"
5.19 - rrcvd :: "'m receiver_state => 'm packet multiset"
5.20 - rbit :: "'m receiver_state => bool"
5.21 - rsending :: "'m receiver_state => bool"
5.22 +definition
5.23 + receiver_asig :: "'m action signature" where
5.24 + "receiver_asig =
5.25 + (UN pkt. {R_pkt(pkt)},
5.26 + (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
5.27 + insert C_m_r (UN m. {C_r_r(m)}))"
5.28
5.29 -defs
5.30 -
5.31 -rq_def: "rq == fst"
5.32 -rsent_def: "rsent == fst o snd"
5.33 -rrcvd_def: "rrcvd == fst o snd o snd"
5.34 -rbit_def: "rbit == fst o snd o snd o snd"
5.35 -rsending_def: "rsending == snd o snd o snd o snd"
5.36 -
5.37 -receiver_asig_def: "receiver_asig ==
5.38 - (UN pkt. {R_pkt(pkt)},
5.39 - (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
5.40 - insert C_m_r (UN m. {C_r_r(m)}))"
5.41 -
5.42 -receiver_trans_def: "receiver_trans ==
5.43 +definition
5.44 + receiver_trans:: "('m action, 'm receiver_state)transition set" where
5.45 +"receiver_trans =
5.46 {tr. let s = fst(tr);
5.47 t = snd(snd(tr))
5.48 in
5.49 @@ -83,9 +74,10 @@
5.50 ~rsending(s) &
5.51 rsending(t)}"
5.52
5.53 -
5.54 -receiver_ioa_def: "receiver_ioa ==
5.55 - (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})"
5.56 +definition
5.57 + receiver_ioa :: "('m action, 'm receiver_state)ioa" where
5.58 + "receiver_ioa =
5.59 + (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})"
5.60
5.61 lemma in_receiver_asig:
5.62 "S_msg(m) ~: actions(receiver_asig)"
6.1 --- a/src/HOLCF/IOA/NTP/Sender.thy Wed Jun 25 18:23:50 2008 +0200
6.2 +++ b/src/HOLCF/IOA/NTP/Sender.thy Wed Jun 25 21:25:51 2008 +0200
6.3 @@ -13,31 +13,21 @@
6.4 'm sender_state = "'m list * bool multiset * bool multiset * bool * bool"
6.5 (* messages #sent #received header mode *)
6.6
6.7 -consts
6.8 +definition sq :: "'m sender_state => 'm list" where "sq = fst"
6.9 +definition ssent :: "'m sender_state => bool multiset" where "ssent = fst o snd"
6.10 +definition srcvd :: "'m sender_state => bool multiset" where "srcvd = fst o snd o snd"
6.11 +definition sbit :: "'m sender_state => bool" where "sbit = fst o snd o snd o snd"
6.12 +definition ssending :: "'m sender_state => bool" where "ssending = snd o snd o snd o snd"
6.13
6.14 -sender_asig :: "'m action signature"
6.15 -sender_trans :: "('m action, 'm sender_state)transition set"
6.16 -sender_ioa :: "('m action, 'm sender_state)ioa"
6.17 -sq :: "'m sender_state => 'm list"
6.18 -ssent :: "'m sender_state => bool multiset"
6.19 -srcvd :: "'m sender_state => bool multiset"
6.20 -sbit :: "'m sender_state => bool"
6.21 -ssending :: "'m sender_state => bool"
6.22 +definition
6.23 + sender_asig :: "'m action signature" where
6.24 + "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
6.25 + UN pkt. {S_pkt(pkt)},
6.26 + {C_m_s,C_r_s})"
6.27
6.28 -defs
6.29 -
6.30 -sq_def: "sq == fst"
6.31 -ssent_def: "ssent == fst o snd"
6.32 -srcvd_def: "srcvd == fst o snd o snd"
6.33 -sbit_def: "sbit == fst o snd o snd o snd"
6.34 -ssending_def: "ssending == snd o snd o snd o snd"
6.35 -
6.36 -sender_asig_def:
6.37 - "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
6.38 - UN pkt. {S_pkt(pkt)},
6.39 - {C_m_s,C_r_s})"
6.40 -
6.41 -sender_trans_def: "sender_trans ==
6.42 +definition
6.43 + sender_trans :: "('m action, 'm sender_state)transition set" where
6.44 + "sender_trans =
6.45 {tr. let s = fst(tr);
6.46 t = snd(snd(tr))
6.47 in case fst(snd(tr))
6.48 @@ -80,8 +70,10 @@
6.49 ssending(t) |
6.50 C_r_r(m) => False}"
6.51
6.52 -sender_ioa_def: "sender_ioa ==
6.53 - (sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})"
6.54 +definition
6.55 + sender_ioa :: "('m action, 'm sender_state)ioa" where
6.56 + "sender_ioa =
6.57 + (sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})"
6.58
6.59 lemma in_sender_asig:
6.60 "S_msg(m) : actions(sender_asig)"
7.1 --- a/src/HOLCF/IOA/NTP/Spec.thy Wed Jun 25 18:23:50 2008 +0200
7.2 +++ b/src/HOLCF/IOA/NTP/Spec.thy Wed Jun 25 21:25:51 2008 +0200
7.3 @@ -9,35 +9,33 @@
7.4 imports IOA Action
7.5 begin
7.6
7.7 -consts
7.8 +definition
7.9 + spec_sig :: "'m action signature" where
7.10 + sig_def: "spec_sig = (UN m.{S_msg(m)},
7.11 + UN m.{R_msg(m)},
7.12 + {})"
7.13
7.14 -spec_sig :: "'m action signature"
7.15 -spec_trans :: "('m action, 'm list)transition set"
7.16 -spec_ioa :: "('m action, 'm list)ioa"
7.17 +definition
7.18 + spec_trans :: "('m action, 'm list)transition set" where
7.19 + trans_def: "spec_trans =
7.20 + {tr. let s = fst(tr);
7.21 + t = snd(snd(tr))
7.22 + in
7.23 + case fst(snd(tr))
7.24 + of
7.25 + S_msg(m) => t = s@[m] |
7.26 + R_msg(m) => s = (m#t) |
7.27 + S_pkt(pkt) => False |
7.28 + R_pkt(pkt) => False |
7.29 + S_ack(b) => False |
7.30 + R_ack(b) => False |
7.31 + C_m_s => False |
7.32 + C_m_r => False |
7.33 + C_r_s => False |
7.34 + C_r_r(m) => False}"
7.35
7.36 -defs
7.37 -
7.38 -sig_def: "spec_sig == (UN m.{S_msg(m)},
7.39 - UN m.{R_msg(m)},
7.40 - {})"
7.41 -
7.42 -trans_def: "spec_trans ==
7.43 - {tr. let s = fst(tr);
7.44 - t = snd(snd(tr))
7.45 - in
7.46 - case fst(snd(tr))
7.47 - of
7.48 - S_msg(m) => t = s@[m] |
7.49 - R_msg(m) => s = (m#t) |
7.50 - S_pkt(pkt) => False |
7.51 - R_pkt(pkt) => False |
7.52 - S_ack(b) => False |
7.53 - R_ack(b) => False |
7.54 - C_m_s => False |
7.55 - C_m_r => False |
7.56 - C_r_s => False |
7.57 - C_r_r(m) => False}"
7.58 -
7.59 -ioa_def: "spec_ioa == (spec_sig, {[]}, spec_trans,{},{})"
7.60 +definition
7.61 + spec_ioa :: "('m action, 'm list)ioa" where
7.62 + ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans,{},{})"
7.63
7.64 end
8.1 --- a/src/HOLCF/IOA/Storage/Correctness.thy Wed Jun 25 18:23:50 2008 +0200
8.2 +++ b/src/HOLCF/IOA/Storage/Correctness.thy Wed Jun 25 21:25:51 2008 +0200
8.3 @@ -35,30 +35,30 @@
8.4 txt {* start states *}
8.5 apply (auto)[1]
8.6 apply (rule_tac x = " ({},False) " in exI)
8.7 -apply (simp add: sim_relation_def starts_of_def Spec.ioa_def Impl.ioa_def)
8.8 +apply (simp add: sim_relation_def starts_of_def spec_ioa_def impl_ioa_def)
8.9 txt {* main-part *}
8.10 apply (rule allI)+
8.11 apply (rule imp_conj_lemma)
8.12 apply (rename_tac k b used c k' b' a)
8.13 apply (induct_tac "a")
8.14 -apply (simp_all (no_asm) add: sim_relation_def Impl.ioa_def Impl.trans_def trans_of_def)
8.15 +apply (simp_all (no_asm) add: sim_relation_def impl_ioa_def impl_trans_def trans_of_def)
8.16 apply auto
8.17 txt {* NEW *}
8.18 apply (rule_tac x = "(used,True)" in exI)
8.19 apply simp
8.20 apply (rule transition_is_ex)
8.21 -apply (simp (no_asm) add: Spec.ioa_def Spec.trans_def trans_of_def)
8.22 +apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
8.23 txt {* LOC *}
8.24 apply (rule_tac x = " (used Un {k},False) " in exI)
8.25 apply (simp add: less_SucI)
8.26 apply (rule transition_is_ex)
8.27 -apply (simp (no_asm) add: Spec.ioa_def Spec.trans_def trans_of_def)
8.28 +apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
8.29 apply fast
8.30 txt {* FREE *}
8.31 apply (rule_tac x = " (used - {nat},c) " in exI)
8.32 apply simp
8.33 apply (rule transition_is_ex)
8.34 -apply (simp (no_asm) add: Spec.ioa_def Spec.trans_def trans_of_def)
8.35 +apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
8.36 done
8.37
8.38
8.39 @@ -66,10 +66,10 @@
8.40 "impl_ioa =<| spec_ioa"
8.41 apply (unfold ioa_implements_def)
8.42 apply (rule conjI)
8.43 -apply (simp (no_asm) add: Impl.sig_def Spec.sig_def Impl.ioa_def Spec.ioa_def
8.44 +apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def
8.45 asig_outputs_def asig_of_def asig_inputs_def)
8.46 apply (rule trace_inclusion_for_simulations)
8.47 -apply (simp (no_asm) add: Impl.sig_def Spec.sig_def Impl.ioa_def Spec.ioa_def
8.48 +apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def
8.49 externals_def asig_outputs_def asig_of_def asig_inputs_def)
8.50 apply (rule issimulation)
8.51 done
9.1 --- a/src/HOLCF/IOA/Storage/Impl.thy Wed Jun 25 18:23:50 2008 +0200
9.2 +++ b/src/HOLCF/IOA/Storage/Impl.thy Wed Jun 25 21:25:51 2008 +0200
9.3 @@ -9,34 +9,32 @@
9.4 imports IOA Action
9.5 begin
9.6
9.7 -consts
9.8 +definition
9.9 + impl_sig :: "action signature" where
9.10 + "impl_sig = (UN l.{Free l} Un {New},
9.11 + UN l.{Loc l},
9.12 + {})"
9.13
9.14 -impl_sig :: "action signature"
9.15 -impl_trans :: "(action, nat * bool)transition set"
9.16 -impl_ioa :: "(action, nat * bool)ioa"
9.17 +definition
9.18 + impl_trans :: "(action, nat * bool)transition set" where
9.19 + "impl_trans =
9.20 + {tr. let s = fst(tr); k = fst s; b = snd s;
9.21 + t = snd(snd(tr)); k' = fst t; b' = snd t
9.22 + in
9.23 + case fst(snd(tr))
9.24 + of
9.25 + New => k' = k & b' |
9.26 + Loc l => b & l= k & k'= (Suc k) & ~b' |
9.27 + Free l => k'=k & b'=b}"
9.28
9.29 -defs
9.30 -
9.31 -sig_def: "impl_sig == (UN l.{Free l} Un {New},
9.32 - UN l.{Loc l},
9.33 - {})"
9.34 -
9.35 -trans_def: "impl_trans ==
9.36 - {tr. let s = fst(tr); k = fst s; b = snd s;
9.37 - t = snd(snd(tr)); k' = fst t; b' = snd t
9.38 - in
9.39 - case fst(snd(tr))
9.40 - of
9.41 - New => k' = k & b' |
9.42 - Loc l => b & l= k & k'= (Suc k) & ~b' |
9.43 - Free l => k'=k & b'=b}"
9.44 -
9.45 -ioa_def: "impl_ioa == (impl_sig, {(0,False)}, impl_trans,{},{})"
9.46 +definition
9.47 + impl_ioa :: "(action, nat * bool)ioa" where
9.48 + "impl_ioa = (impl_sig, {(0,False)}, impl_trans,{},{})"
9.49
9.50 lemma in_impl_asig:
9.51 "New : actions(impl_sig) &
9.52 Loc l : actions(impl_sig) &
9.53 Free l : actions(impl_sig) "
9.54 - by (simp add: Impl.sig_def actions_def asig_projections)
9.55 + by (simp add: impl_sig_def actions_def asig_projections)
9.56
9.57 end
10.1 --- a/src/HOLCF/IOA/Storage/Spec.thy Wed Jun 25 18:23:50 2008 +0200
10.2 +++ b/src/HOLCF/IOA/Storage/Spec.thy Wed Jun 25 21:25:51 2008 +0200
10.3 @@ -9,28 +9,26 @@
10.4 imports IOA Action
10.5 begin
10.6
10.7 -consts
10.8 +definition
10.9 + spec_sig :: "action signature" where
10.10 + "spec_sig = (UN l.{Free l} Un {New},
10.11 + UN l.{Loc l},
10.12 + {})"
10.13
10.14 -spec_sig :: "action signature"
10.15 -spec_trans :: "(action, nat set * bool)transition set"
10.16 -spec_ioa :: "(action, nat set * bool)ioa"
10.17 +definition
10.18 + spec_trans :: "(action, nat set * bool)transition set" where
10.19 + "spec_trans =
10.20 + {tr. let s = fst(tr); used = fst s; c = snd s;
10.21 + t = snd(snd(tr)); used' = fst t; c' = snd t
10.22 + in
10.23 + case fst(snd(tr))
10.24 + of
10.25 + New => used' = used & c' |
10.26 + Loc l => c & l~:used & used'= used Un {l} & ~c' |
10.27 + Free l => used'=used - {l} & c'=c}"
10.28
10.29 -defs
10.30 -
10.31 -sig_def: "spec_sig == (UN l.{Free l} Un {New},
10.32 - UN l.{Loc l},
10.33 - {})"
10.34 -
10.35 -trans_def: "spec_trans ==
10.36 - {tr. let s = fst(tr); used = fst s; c = snd s;
10.37 - t = snd(snd(tr)); used' = fst t; c' = snd t
10.38 - in
10.39 - case fst(snd(tr))
10.40 - of
10.41 - New => used' = used & c' |
10.42 - Loc l => c & l~:used & used'= used Un {l} & ~c' |
10.43 - Free l => used'=used - {l} & c'=c}"
10.44 -
10.45 -ioa_def: "spec_ioa == (spec_sig, {({},False)}, spec_trans,{},{})"
10.46 +definition
10.47 + spec_ioa :: "(action, nat set * bool)ioa" where
10.48 + "spec_ioa = (spec_sig, {({},False)}, spec_trans,{},{})"
10.49
10.50 end
11.1 --- a/src/HOLCF/ex/Stream.thy Wed Jun 25 18:23:50 2008 +0200
11.2 +++ b/src/HOLCF/ex/Stream.thy Wed Jun 25 21:25:51 2008 +0200
11.3 @@ -41,11 +41,10 @@
11.4 Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
11.5 | \<infinity> \<Rightarrow> s1)"
11.6
11.7 -consts
11.8 - constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream"
11.9 -primrec
11.10 +primrec constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream"
11.11 +where
11.12 constr_sconc'_0: "constr_sconc' 0 s1 s2 = s2"
11.13 - constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 &&
11.14 +| constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 &&
11.15 constr_sconc' n (rt$s1) s2"
11.16
11.17 definition