# HG changeset patch # User wenzelm # Date 1125759022 -7200 # Node ID 0b2ff9541727b10c5a121e8a9a5db18653f3c028 # Parent c4ff384ee28f61d93caf458429887a670197fef4 converted to Isar theory format; diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Abschannel.thy --- a/src/HOLCF/IOA/ABP/Abschannel.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Abschannel.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,91 +1,93 @@ (* Title: HOLCF/IOA/ABP/Abschannel.thy ID: $Id$ Author: Olaf Müller - -The transmission channel. *) -Abschannel = IOA + Action + Lemmas + List + +header {* The transmission channel *} +theory Abschannel +imports IOA Action Lemmas +begin -datatype ('a)abs_action = S('a) | R('a) +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 +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 +rsch_actions :: "'m action => bool abs_action option" srch_actions :: "'m action =>(bool * 'm) abs_action option" -srch_asig, +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 +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_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_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" +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)}, {})" + +ch_asig_def: "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) & +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))) }" - -ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans,{},{})" + +ch_ioa_def: "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 + 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 - Next => None | - S_msg(m) => None | - R_msg(m) => None | - S_pkt(packet) => None | - R_pkt(packet) => None | - S_ack(b) => Some(S(b)) | + +rsch_actions_def: "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))" -srch_actions_def "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 | +srch_actions_def: "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" +ML {* use_legacy_bindings (the_context ()) *} -end +end @@ -99,8 +101,3 @@ - - - - - diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Abschannel_finite.thy --- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,78 +1,64 @@ (* Title: HOLCF/IOA/ABP/Abschannels.thy ID: $Id$ Author: Olaf Müller - -The transmission channel -- finite version. *) -Abschannel_finite = Abschannel+ IOA + Action + Lemmas + List + - +header {* The transmission channel -- finite version *} + +theory Abschannel_finite +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_trans :: "('a abs_action, 'a list)transition set" -ch_fin_ioa :: ('a abs_action, 'a list)ioa +ch_fin_ioa :: "('a abs_action, 'a list)ioa" -srch_fin_asig, +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_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 +srch_fin_ioa :: "('m action, 'm packet list)ioa" +rsch_fin_ioa :: "('m action, bool list)ioa" -reverse :: 'a list => 'a list +reverse :: "'a list => 'a list" primrec - reverse_Nil "reverse([]) = []" - reverse_Cons "reverse(x#xs) = reverse(xs)@[x]" + 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)" +srch_fin_asig_def: "srch_fin_asig == asig_of(srch_fin_ioa)" +rsch_fin_asig_def: "rsch_fin_asig == asig_of(rsch_fin_ioa)" -srch_fin_trans_def "srch_fin_trans == trans_of(srch_fin_ioa)" -rsch_fin_trans_def "rsch_fin_trans == trans_of(rsch_fin_ioa)" +srch_fin_trans_def: "srch_fin_trans == trans_of(srch_fin_ioa)" +rsch_fin_trans_def: "rsch_fin_trans == trans_of(rsch_fin_ioa)" -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" +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" -ch_fin_asig_def "ch_fin_asig == ch_asig" - -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))) }" - -ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans,{},{})" - -end +ch_fin_asig_def: "ch_fin_asig == ch_asig" - - - - - - - - +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))) }" - - - +ch_fin_ioa_def: "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans,{},{})" - +ML {* use_legacy_bindings (the_context ()) *} - - +end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Action.thy --- a/src/HOLCF/IOA/ABP/Action.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Action.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,12 +1,19 @@ (* Title: HOLCF/IOA/ABP/Action.thy ID: $Id$ Author: Olaf Müller - -The set of all actions of the system. *) -Action = Packet + Datatype + -datatype 'm action = Next | S_msg ('m) | R_msg ('m) - | S_pkt ('m packet) | R_pkt ('m packet) - | S_ack (bool) | R_ack (bool) +header {* The set of all actions of the system *} + +theory Action +imports Packet +begin + +datatype 'm action = + Next | S_msg 'm | R_msg 'm + | S_pkt "'m packet" | R_pkt "'m packet" + | S_ack bool | R_ack bool + +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Correctness.ML --- a/src/HOLCF/IOA/ABP/Correctness.ML Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Correctness.ML Sat Sep 03 16:50:22 2005 +0200 @@ -4,10 +4,6 @@ *) -goal Abschannel.thy "(? x. x=P & Q(x)) = Q(P)"; -by (Fast_tac 1); -qed"exis_elim"; - Delsimps [split_paired_All,Collect_empty_eq]; Addsimps ([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, @@ -20,13 +16,13 @@ ch_fin_ioa_def,ch_fin_trans_def,ch_fin_asig_def]; Addsimps abschannel_fin; -val impl_ioas = [Sender.sender_ioa_def,Receiver.receiver_ioa_def]; -val impl_trans = [Sender.sender_trans_def,Receiver.receiver_trans_def]; -val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def]; +val impl_ioas = [sender_ioa_def,receiver_ioa_def]; +val impl_trans = [sender_trans_def,receiver_trans_def]; +val impl_asigs = [sender_asig_def,receiver_asig_def]; Addcongs [let_weak_cong]; Addsimps [Let_def, ioa_triple_proj, starts_of_par]; -val env_ioas = [Env.env_ioa_def,Env.env_asig_def,Env.env_trans_def]; +val env_ioas = [env_ioa_def,env_asig_def,env_trans_def]; val hom_ioas = env_ioas @ impl_ioas @ impl_trans @ impl_asigs @ asig_projections @ set_lemmas; Addsimps hom_ioas; @@ -58,11 +54,11 @@ Goal "l~=[] ==> hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))"; by (Simp_tac 1); by (auto_tac (claset(), HOL_ss addsplits [thm"list.split"] - addsimps [reverse_Cons,hd_append, - rev_red_not_nil])); + addsimps (reverse.simps @ [hd_append, + rev_red_not_nil]))); qed"last_ind_on_first"; -val impl_ss = simpset() delsimps [reduce_Cons]; +val impl_ss = simpset() delsimps [reduce.reduce_Cons]; (* Main Lemma 1 for S_pkt in showing that reduce is refinement *) Goal @@ -75,7 +71,7 @@ by (induct_tac "l" 1); by (Simp_tac 1); by (case_tac "list=[]" 1); - by (asm_full_simp_tac (simpset() addsimps [reverse_Nil,reverse_Cons]) 1); + by (asm_full_simp_tac (simpset() addsimps reverse.simps) 1); by (rtac impI 1); by (Simp_tac 1); by (cut_inst_tac [("l","list")] cons_not_nil 1); @@ -204,8 +200,8 @@ simpset() delsimps ([trans_of_def, srch_asig_def,rsch_asig_def, asig_of_def, actions_def, srch_trans_def, rsch_trans_def, srch_ioa_def, srch_fin_ioa_def, rsch_fin_ioa_def, - rsch_ioa_def, Sender.sender_trans_def, - Receiver.receiver_trans_def] @ set_lemmas); + rsch_ioa_def, sender_trans_def, + receiver_trans_def] @ set_lemmas); Goal "compatible receiver_ioa (srch_ioa || rsch_ioa)"; by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def, diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Correctness.thy --- a/src/HOLCF/IOA/ABP/Correctness.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Correctness.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,47 +1,49 @@ (* Title: HOLCF/IOA/ABP/Correctness.thy ID: $Id$ Author: Olaf Müller - -The main correctness proof: System_fin implements System. *) -Correctness = IOA + Env + Impl + Impl_finite + +header {* The main correctness proof: System_fin implements System *} + +theory Correctness +imports IOA Env Impl Impl_finite +begin consts -reduce :: 'a list => 'a list +reduce :: "'a list => 'a list" abs :: 'c system_ioa :: "('m action, bool * 'm impl_state)ioa" system_fin_ioa :: "('m action, bool * 'm impl_state)ioa" - + primrec - reduce_Nil "reduce [] = []" - reduce_Cons "reduce(x#xs) = - (case xs of - [] => [x] - | y#ys => (if (x=y) - then reduce xs + reduce_Nil: "reduce [] = []" + reduce_Cons: "reduce(x#xs) = + (case xs of + [] => [x] + | y#ys => (if (x=y) + then reduce xs else (x#(reduce xs))))" - + defs - -system_def + +system_def: "system_ioa == (env_ioa || impl_ioa)" -system_fin_def +system_fin_def: "system_fin_ioa == (env_ioa || impl_fin_ioa)" - -abs_def "abs == - (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), + +abs_def: "abs == + (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))" -rules +axioms - sys_IOA "IOA system_ioa" - sys_fin_IOA "IOA system_fin_ioa" - + sys_IOA: "IOA system_ioa" + sys_fin_IOA: "IOA system_fin_ioa" + +ML {* use_legacy_bindings (the_context ()) *} + end - - diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Env.thy --- a/src/HOLCF/IOA/ABP/Env.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Env.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,46 +1,43 @@ (* Title: HOLCF/IOA/ABP/Impl.thy ID: $Id$ Author: Olaf Müller - -The environment. *) -Env = IOA + Action + +header {* The environment *} + +theory Env +imports IOA Action +begin types + 'm env_state = bool -- {* give next bit to system *} -'m env_state = "bool" -(* give next bit to system *) +constdefs +env_asig :: "'m action signature" +"env_asig == ({Next}, + UN m. {S_msg(m)}, + {})" + +env_trans :: "('m action, 'm env_state)transition set" +"env_trans == + {tr. let s = fst(tr); + t = snd(snd(tr)) + in case fst(snd(tr)) + of + Next => t=True | + S_msg(m) => s=True & t=False | + R_msg(m) => False | + S_pkt(pkt) => False | + R_pkt(pkt) => False | + S_ack(b) => False | + R_ack(b) => False}" + +env_ioa :: "('m action, 'm env_state)ioa" +"env_ioa == (env_asig, {True}, env_trans,{},{})" consts - -env_asig :: "'m action signature" -env_trans :: ('m action, 'm env_state)transition set -env_ioa :: ('m action, 'm env_state)ioa -next :: 'm env_state => bool - -defs - -env_asig_def - "env_asig == ({Next}, - UN m. {S_msg(m)}, - {})" + "next" :: "'m env_state => bool" -env_trans_def "env_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - Next => t=True | - S_msg(m) => s=True & t=False | - R_msg(m) => False | - S_pkt(pkt) => False | - R_pkt(pkt) => False | - S_ack(b) => False | - R_ack(b) => False}" - -env_ioa_def "env_ioa == - (env_asig, {True}, env_trans,{},{})" +ML {* use_legacy_bindings (the_context ()) *} end - diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Impl.thy --- a/src/HOLCF/IOA/ABP/Impl.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Impl.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,34 +1,35 @@ (* Title: HOLCF/IOA/ABP/Impl.thy ID: $Id$ Author: Olaf Müller - -The implementation. *) -Impl = Sender + Receiver + Abschannel + - -types +header {* The implementation *} -'m impl_state -= "'m sender_state * 'm receiver_state * 'm packet list * bool list" -(* sender_state * receiver_state * srch_state * rsch_state *) +theory Impl +imports Sender Receiver Abschannel +begin +types + 'm impl_state = "'m sender_state * 'm receiver_state * 'm packet list * bool list" + (* sender_state * receiver_state * srch_state * rsch_state *) constdefs - impl_ioa :: ('m action, 'm impl_state)ioa + impl_ioa :: "('m action, 'm impl_state)ioa" "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" - sen :: 'm impl_state => 'm sender_state + sen :: "'m impl_state => 'm sender_state" "sen == fst" - rec :: 'm impl_state => 'm receiver_state + rec :: "'m impl_state => 'm receiver_state" "rec == fst o snd" - srch :: 'm impl_state => 'm packet list + srch :: "'m impl_state => 'm packet list" "srch == fst o snd o snd" - rsch :: 'm impl_state => bool list + rsch :: "'m impl_state => bool list" "rsch == snd o snd o snd" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Impl_finite.thy --- a/src/HOLCF/IOA/ABP/Impl_finite.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Impl_finite.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,35 +1,37 @@ (* Title: HOLCF/IOA/ABP/Impl.thy ID: $Id$ Author: Olaf Müller - -The implementation. *) -Impl_finite = Sender + Receiver + Abschannel_finite + - -types +header {* The implementation *} -'m impl_fin_state -= "'m sender_state * 'm receiver_state * 'm packet list * bool list" +theory Impl_finite +imports Sender Receiver Abschannel_finite +begin + +types + 'm impl_fin_state + = "'m sender_state * 'm receiver_state * 'm packet list * bool list" (* sender_state * receiver_state * srch_state * rsch_state *) constdefs - impl_fin_ioa :: ('m action, 'm impl_fin_state)ioa + impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)" - sen_fin :: 'm impl_fin_state => 'm sender_state + sen_fin :: "'m impl_fin_state => 'm sender_state" "sen_fin == fst" - rec_fin :: 'm impl_fin_state => 'm receiver_state + rec_fin :: "'m impl_fin_state => 'm receiver_state" "rec_fin == fst o snd" - srch_fin :: 'm impl_fin_state => 'm packet list + srch_fin :: "'m impl_fin_state => 'm packet list" "srch_fin == fst o snd o snd" - rsch_fin :: 'm impl_fin_state => bool list + rsch_fin :: "'m impl_fin_state => bool list" "rsch_fin == snd o snd o snd" +ML {* use_legacy_bindings (the_context ()) *} + end - diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Lemmas.ML --- a/src/HOLCF/IOA/ABP/Lemmas.ML Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML Sat Sep 03 16:50:22 2005 +0200 @@ -14,6 +14,11 @@ by (Fast_tac 1); qed "bool_if_impl_or"; +Goal "(? x. x=P & Q(x)) = Q(P)"; +by (Fast_tac 1); +qed"exis_elim"; + + (* Sets *) val set_lemmas = diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Lemmas.thy --- a/src/HOLCF/IOA/ABP/Lemmas.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Lemmas.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,8 +1,10 @@ (* Title: HOLCF/IOA/ABP/Lemmas.thy ID: $Id$ Author: Olaf Müller - -Arithmetic lemmas. *) -Lemmas = Main +theory Lemmas +imports Main +begin + +end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Packet.thy --- a/src/HOLCF/IOA/ABP/Packet.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Packet.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,22 +1,24 @@ (* Title: HOLCF/IOA/ABP/Packet.thy ID: $Id$ Author: Olaf Müller - -Packets. *) -Packet = NatArith + +header {* Packets *} + +theory Packet +imports Main +begin types - - 'msg packet = "bool * 'msg" + 'msg packet = "bool * 'msg" constdefs - - hdr :: 'msg packet => bool + hdr :: "'msg packet => bool" "hdr == fst" - msg :: 'msg packet => 'msg + msg :: "'msg packet => 'msg" "msg == snd" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Receiver.thy --- a/src/HOLCF/IOA/ABP/Receiver.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Receiver.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,58 +1,56 @@ (* Title: HOLCF/IOA/ABP/Receiver.thy ID: $Id$ Author: Olaf Müller - -The implementation: receiver. *) -Receiver = List + IOA + Action + Lemmas + - -types +header {* The implementation: receiver *} -'m receiver_state -= "'m list * bool" -(* messages mode *) +theory Receiver +imports IOA Action Lemmas +begin -consts +types + 'm receiver_state = "'m list * bool" -- {* messages, mode *} - 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 - rbit :: 'm receiver_state => bool +constdefs + rq :: "'m receiver_state => 'm list" + "rq == fst" -defs + rbit :: "'m receiver_state => bool" + "rbit == snd" -rq_def "rq == fst" -rbit_def "rbit == snd" - -receiver_asig_def "receiver_asig == - (UN pkt. {R_pkt(pkt)}, - (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), +receiver_asig :: "'m action signature" +"receiver_asig == + (UN pkt. {R_pkt(pkt)}, + (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), {})" -receiver_trans_def "receiver_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in - case fst(snd(tr)) - of - Next => False | - S_msg(m) => False | - R_msg(m) => (rq(s) ~= []) & - m = hd(rq(s)) & - rq(t) = tl(rq(s)) & - rbit(t)=rbit(s) | - S_pkt(pkt) => False | - R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then - rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else - rq(t) =rq(s) & rbit(t)=rbit(s) | - S_ack(b) => b = rbit(s) & - rq(t) = rq(s) & - rbit(t)=rbit(s) | +receiver_trans :: "('m action, 'm receiver_state)transition set" +"receiver_trans == + {tr. let s = fst(tr); + t = snd(snd(tr)) + in + case fst(snd(tr)) + of + Next => False | + S_msg(m) => False | + R_msg(m) => (rq(s) ~= []) & + m = hd(rq(s)) & + rq(t) = tl(rq(s)) & + rbit(t)=rbit(s) | + S_pkt(pkt) => False | + R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then + rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else + rq(t) =rq(s) & rbit(t)=rbit(s) | + S_ack(b) => b = rbit(s) & + rq(t) = rq(s) & + rbit(t)=rbit(s) | R_ack(b) => False}" -receiver_ioa_def "receiver_ioa == +receiver_ioa :: "('m action, 'm receiver_state)ioa" +"receiver_ioa == (receiver_asig, {([],False)}, receiver_trans,{},{})" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Sender.thy --- a/src/HOLCF/IOA/ABP/Sender.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Sender.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,56 +1,54 @@ (* Title: HOLCF/IOA/ABP/Sender.thy ID: $Id$ Author: Olaf Müller - -The implementation: sender. *) -Sender = IOA + Action + List + Lemmas + +header {* The implementation: sender *} + +theory Sender +imports IOA Action Lemmas +begin types + 'm sender_state = "'m list * bool" -- {* messages, Alternating Bit *} -'m sender_state = "'m list * bool" -(* messages Alternating Bit *) +constdefs +sq :: "'m sender_state => 'm list" +"sq == fst" -consts +sbit :: "'m sender_state => bool" +"sbit == snd" 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 -sbit :: 'm sender_state => bool - -defs - -sq_def "sq == fst" -sbit_def "sbit == snd" - -sender_asig_def - "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), - UN pkt. {S_pkt(pkt)}, +"sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), + UN pkt. {S_pkt(pkt)}, {})" -sender_trans_def "sender_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - Next => if sq(s)=[] then t=s else False | - S_msg(m) => sq(t)=sq(s)@[m] & - sbit(t)=sbit(s) | - R_msg(m) => False | - S_pkt(pkt) => sq(s) ~= [] & - hdr(pkt) = sbit(s) & - msg(pkt) = hd(sq(s)) & - sq(t) = sq(s) & - sbit(t) = sbit(s) | - R_pkt(pkt) => False | - S_ack(b) => False | - R_ack(b) => if b = sbit(s) then - sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else +sender_trans :: "('m action, 'm sender_state)transition set" +"sender_trans == + {tr. let s = fst(tr); + t = snd(snd(tr)) + in case fst(snd(tr)) + of + Next => if sq(s)=[] then t=s else False | + S_msg(m) => sq(t)=sq(s)@[m] & + sbit(t)=sbit(s) | + R_msg(m) => False | + S_pkt(pkt) => sq(s) ~= [] & + hdr(pkt) = sbit(s) & + msg(pkt) = hd(sq(s)) & + sq(t) = sq(s) & + sbit(t) = sbit(s) | + R_pkt(pkt) => False | + S_ack(b) => False | + R_ack(b) => if b = sbit(s) then + sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else sq(t)=sq(s) & sbit(t)=sbit(s)}" -sender_ioa_def "sender_ioa == +sender_ioa :: "('m action, 'm sender_state)ioa" +"sender_ioa == (sender_asig, {([],True)}, sender_trans,{},{})" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ABP/Spec.thy --- a/src/HOLCF/IOA/ABP/Spec.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ABP/Spec.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,31 +1,33 @@ (* Title: HOLCF/IOA/ABP/Spec.thy ID: $Id$ Author: Olaf Müller - -The specification of reliable transmission. *) -Spec = List + IOA + Action + +header {* The specification of reliable transmission *} + +theory Spec +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 +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)}, +sig_def: "spec_sig == (UN m.{S_msg(m)}, UN m.{R_msg(m)} Un {Next}, {})" -trans_def "spec_trans == +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 *) + 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 | @@ -33,6 +35,6 @@ S_ack(b) => False | R_ack(b) => False}" -ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)" +ioa_def: "spec_ioa == (spec_sig, {[]}, spec_trans)" end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/Modelcheck/Cockpit.thy --- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,43 +1,49 @@ -Cockpit = MuIOAOracle + +(* $Id$ *) + +theory Cockpit +imports MuIOAOracle +begin datatype 'a action = Alarm 'a | Info 'a | Ack 'a datatype event = NONE | PonR | Eng | Fue -(*This cockpit automaton is a deeply simplified version of the +text {* + This cockpit automaton is a deeply simplified version of the control component of a helicopter alarm system considered in a study of ESG. Some properties will be proved by using model checker - mucke.*) + mucke. *} automaton cockpit = signature - actions event action + actions "event action" inputs "Alarm a" - outputs "Ack a","Info a" + outputs "Ack a", "Info a" states APonR_incl :: bool info :: event - initially "info=NONE & ~APonR_incl" + initially "info = NONE & ~APonR_incl" transitions "Alarm a" - post info:="if (a=NONE) then info else a", - APonR_incl:="if (a=PonR) then True else APonR_incl" + post info := "if (a=NONE) then info else a", + APonR_incl := "if (a=PonR) then True else APonR_incl" "Info a" pre "(a=info)" "Ack a" pre "(a=PonR --> APonR_incl) & (a=NONE --> ~APonR_incl)" - post info:="NONE",APonR_incl:="if (a=PonR) then False else APonR_incl" + post info := "NONE", + APonR_incl := "if (a=PonR) then False else APonR_incl" automaton cockpit_hide = hide_action "Info a" in cockpit - -(*Subsequent automata express the properties to be proved, see also - Cockpit.ML*) +text {* + Subsequent automata express the properties to be proved, see also + Cockpit.ML *} automaton Al_before_Ack = signature - actions event action + actions "event action" inputs "Alarm a" outputs "Ack a" states @@ -52,7 +58,7 @@ automaton Info_while_Al = signature - actions event action + actions "event action" inputs "Alarm a" outputs "Ack a", "Info i" states @@ -69,7 +75,7 @@ automaton Info_before_Al = signature - actions event action + actions "event action" inputs "Alarm a" outputs "Ack a", "Info i" states @@ -83,4 +89,6 @@ "Ack a" post info_at_NONE:="True" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/Modelcheck/MuIOA.thy --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,16 +1,20 @@ -MuIOA = IOA + MuckeSyn + +(* $Id$ *) + +theory MuIOA +imports IOA MuckeSyn +begin consts - Internal_of_A :: 'a => bool - Internal_of_C :: 'a => bool - Start_of_A :: 'a => bool - Start_of_C :: 'a => bool - Trans_of_A :: 'a => 'b => bool - Trans_of_C :: 'a => 'b => bool - IntStep_of_A :: 'a => bool - IntStepStar_of_A :: 'a => bool - Move_of_A :: 'a => 'b => bool - isSimCA :: 'a => bool + Internal_of_A :: "'a => bool" + Internal_of_C :: "'a => bool" + Start_of_A :: "'a => bool" + Start_of_C :: "'a => bool" + Trans_of_A :: "'a => 'b => bool" + Trans_of_C :: "'a => 'b => bool" + IntStep_of_A :: "'a => bool" + IntStepStar_of_A :: "'a => bool" + Move_of_A :: "'a => 'b => bool" + isSimCA :: "'a => bool" end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy --- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,7 +1,11 @@ -MuIOAOracle = MuIOA + +(* $Id$ *) -oracle - Sim = mk_sim_oracle +theory MuIOAOracle +imports MuIOA +begin + +oracle sim_oracle ("term * thm list") = + mk_sim_oracle end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/Modelcheck/Ring3.thy --- a/src/HOLCF/IOA/Modelcheck/Ring3.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,5 +1,9 @@ -Ring3 = MuIOAOracle + +(* $Id$ *) + +theory Ring3 +imports MuIOAOracle +begin datatype token = Leader | id0 | id1 | id2 | id3 | id4 @@ -8,7 +12,7 @@ Leader_Zero | Leader_One | Leader_Two constdefs - Greater :: [token, token] => bool + Greater :: "[token, token] => bool" "Greater x y == (x~=Leader & x~=id0 & y=id0) | (x=id4 & y~=id4 & y~=Leader) | (x=id2 & y=id1) | (x=id3 & y=id1) | (x=id3 & y=id2)" @@ -79,7 +83,7 @@ automaton one_leader = signature actions Comm - outputs "Zero_One t","One_Two t","Two_Zero t","Leader_Zero","Leader_One","Leader_Two" + outputs "Zero_One t","One_Two t","Two_Zero t","Leader_Zero","Leader_One","Leader_Two" states leader :: token initially "leader=Leader" @@ -89,16 +93,17 @@ "One_Two t" pre "True" "Two_Zero t" - pre "True" + pre "True" "Leader_Zero" pre "leader=id0 | leader=Leader" post leader:="id0" "Leader_One" pre "leader=id1 | leader=Leader" - post leader:="id1" + post leader:="id1" "Leader_Two" pre "leader=id2 | leader=Leader" post leader:="id2" +ML {* use_legacy_bindings (the_context ()) *} end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Abschannel.ML --- a/src/HOLCF/IOA/NTP/Abschannel.ML Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Abschannel.ML Sat Sep 03 16:50:22 2005 +0200 @@ -5,12 +5,10 @@ Derived rules. *) -open Abschannel; - -val unfold_renaming = - [srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, - ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, - actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, +val unfold_renaming = + [srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, + ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, + actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, trans_of_def] @ asig_projections; Goal @@ -55,4 +53,3 @@ wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1); by (simp_tac (simpset() addsimps unfold_renaming) 1); qed"rsch_ioa_thm"; - diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Abschannel.thy --- a/src/HOLCF/IOA/NTP/Abschannel.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Abschannel.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,111 +1,99 @@ (* Title: HOL/IOA/NTP/Abschannel.thy ID: $Id$ Author: Olaf Müller - -The (faulty) transmission channel (both directions). *) -Abschannel = IOA + Action + - -datatype ('a)abs_action = S('a) | R('a) +header {* The (faulty) transmission channel (both directions) *} + +theory Abschannel +imports IOA Action +begin + +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_trans :: "('a abs_action, 'a multiset)transition set" -ch_ioa :: ('a abs_action, 'a multiset)ioa +ch_ioa :: "('a abs_action, 'a multiset)ioa" -rsch_actions :: 'm action => bool abs_action option +rsch_actions :: "'m action => bool abs_action option" srch_actions :: "'m action =>(bool * 'm) abs_action option" -srch_asig, +srch_asig :: "'m action signature" rsch_asig :: "'m action signature" -srch_wfair, srch_sfair, rsch_sfair, -rsch_wfair ::('m action)set set +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_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 +srch_ioa :: "('m action, 'm packet multiset)ioa" +rsch_ioa :: "('m action, bool multiset)ioa" defs -srch_asig_def "srch_asig == asig_of(srch_ioa)" -rsch_asig_def "rsch_asig == asig_of(rsch_ioa)" +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_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_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_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" +srch_ioa_def: "srch_ioa == rename ch_ioa srch_actions" +rsch_ioa_def: "rsch_ioa == rename ch_ioa rsch_actions" -ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})" +ch_asig_def: "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 = addm s b | +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,{},{})" +ch_ioa_def: "ch_ioa == (ch_asig, {{|}}, ch_trans,{},{})" -rsch_actions_def "rsch_actions (akt) == - case akt of - 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)) | - C_m_s => None | - C_m_r => None | - C_r_s => None | +rsch_actions_def: "rsch_actions (akt) == + case akt of + 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)) | + C_m_s => None | + C_m_r => None | + C_r_s => None | C_r_r(m) => None" -srch_actions_def "srch_actions (akt) == - case akt of - 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 | - C_m_s => None | - C_m_r => None | - C_r_s => None | +srch_actions_def: "srch_actions (akt) == + case akt of + 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 | + C_m_s => None | + C_m_r => None | + C_r_s => None | C_r_r(m) => None" -end - - - - - - - - +ML {* use_legacy_bindings (the_context ()) *} - - - - - - - - - +end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Action.thy --- a/src/HOLCF/IOA/NTP/Action.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Action.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,13 +1,19 @@ (* Title: HOL/IOA/NTP/Action.thy ID: $Id$ Author: Tobias Nipkow & Konrad Slind - -The set of all actions of the system. *) -Action = Packet + Datatype + -datatype 'm action = S_msg ('m) | R_msg ('m) - | S_pkt ('m packet) | R_pkt ('m packet) - | S_ack (bool) | R_ack (bool) - | C_m_s | C_m_r | C_r_s | C_r_r ('m) +header {* The set of all actions of the system *} + +theory Action +imports Packet +begin + +datatype 'm action = S_msg 'm | R_msg 'm + | S_pkt "'m packet" | R_pkt "'m packet" + | S_ack bool | R_ack bool + | C_m_s | C_m_r | C_r_s | C_r_r 'm + +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Correctness.ML --- a/src/HOLCF/IOA/NTP/Correctness.ML Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Correctness.ML Sat Sep 03 16:50:22 2005 +0200 @@ -1,20 +1,18 @@ (* Title: HOL/IOA/NTP/Correctness.ML ID: $Id$ Author: Tobias Nipkow & Konrad Slind - -The main correctness proof: Impl implements Spec. *) (* repeated from Traces.ML *) claset_ref() := claset() delSWrapper "split_all_tac"; -val hom_ioas = [Spec.ioa_def, Spec.trans_def, - Sender.sender_trans_def,Receiver.receiver_trans_def] +val hom_ioas = [thm "Spec.ioa_def", thm "Spec.trans_def", + sender_trans_def,receiver_trans_def] @ impl_ioas; -val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def, - Abschannel.srch_asig_def,Abschannel.rsch_asig_def]; +val impl_asigs = [sender_asig_def,receiver_asig_def, + srch_asig_def,rsch_asig_def]; (* Two simpsets: - simpset() is basic, ss' unfolds hom_ioas *) @@ -40,7 +38,7 @@ \ | C_r_s => False \ \ | C_r_r(m) => False)"; by (simp_tac (simpset() addsimps ([externals_def, restrict_def, - restrict_asig_def, Spec.sig_def] + restrict_asig_def, thm "Spec.sig_def"] @asig_projections)) 1); by (induct_tac "a" 1); @@ -59,16 +57,16 @@ qed "externals_lemma"; -val sels = [Sender.sbit_def, Sender.sq_def, Sender.ssending_def, - Receiver.rbit_def, Receiver.rq_def, Receiver.rsending_def]; +val sels = [sbit_def, sq_def, ssending_def, + rbit_def, rq_def, rsending_def]; (* Proof of correctness *) -Goalw [Spec.ioa_def, is_weak_ref_map_def] +Goalw [thm "Spec.ioa_def", is_weak_ref_map_def] "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) \ \ spec_ioa"; by (simp_tac (simpset() delcongs [if_weak_cong] delsplits [split_if] - addsimps [Correctness.hom_def, cancel_restrict, + addsimps [thm "Correctness.hom_def", cancel_restrict, externals_lemma]) 1); by (rtac conjI 1); by (simp_tac ss' 1); diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Correctness.thy --- a/src/HOLCF/IOA/NTP/Correctness.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Correctness.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,16 +1,19 @@ (* Title: HOL/IOA/NTP/Correctness.thy ID: $Id$ Author: Tobias Nipkow & Konrad Slind - -The main correctness proof: Impl implements Spec. *) -Correctness = Impl + Spec + +header {* The main correctness proof: Impl implements Spec *} + +theory Correctness +imports Impl Spec +begin constdefs - - hom :: 'm impl_state => 'm list - "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) + hom :: "'m impl_state => 'm list" + "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) else tl(sq(sen s)))" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Impl.ML --- a/src/HOLCF/IOA/NTP/Impl.ML Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Impl.ML Sat Sep 03 16:50:22 2005 +0200 @@ -9,18 +9,16 @@ Addsimps [Let_def, le_SucI]; -open Abschannel Impl; - val impl_ioas = - [Impl.impl_def, - Sender.sender_ioa_def, - Receiver.receiver_ioa_def, + [impl_def, + sender_ioa_def, + receiver_ioa_def, srch_ioa_thm RS eq_reflection, rsch_ioa_thm RS eq_reflection]; -val transitions = [Sender.sender_trans_def, Receiver.receiver_trans_def, +val transitions = [sender_trans_def, receiver_trans_def, srch_trans_def, rsch_trans_def]; - + Addsimps [ioa_triple_proj, starts_of_par, trans_of_par4, in_sender_asig, in_receiver_asig, in_srch_asig, @@ -47,15 +45,15 @@ Delsimps [split_paired_All]; -(* Three Simp_sets in different sizes +(* Three Simp_sets in different sizes ---------------------------------------------- -1) simpset() does not unfold the transition relations -2) ss unfolds transition relations +1) simpset() does not unfold the transition relations +2) ss unfolds transition relations 3) renname_ss unfolds transitions and the abstract channel *) -val ss = (simpset() addsimps transitions); +val ss = (simpset() addsimps transitions); val rename_ss = (ss addsimps unfold_renaming); val tac = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]); @@ -68,19 +66,19 @@ Goalw impl_ioas "invariant impl_ioa inv1"; by (rtac invariantI 1); by (asm_full_simp_tac (simpset() - addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def, - Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1); + addsimps [inv1_def, hdr_sum_def, srcvd_def, + ssent_def, rsent_def,rrcvd_def]) 1); by (simp_tac (simpset() delsimps [trans_of_par4] addsimps [imp_conjR,inv1_def]) 1); (* Split proof in two *) -by (rtac conjI 1); +by (rtac conjI 1); (* First half *) -by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def] +by (asm_full_simp_tac (simpset() addsimps [thm "Impl.inv1_def"] delsplits [split_if]) 1); -by (rtac Action.action.induct 1); +by (rtac action.induct 1); by (EVERY1[tac, tac, tac, tac]); by (tac 1); @@ -96,9 +94,9 @@ (* Now the other half *) -by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def] +by (asm_full_simp_tac (simpset() addsimps [thm "Impl.inv1_def"] delsplits [split_if]) 1); -by (rtac Action.action.induct 1); +by (rtac action.induct 1); by (EVERY1[tac, tac]); (* detour 1 *) @@ -114,7 +112,7 @@ by (tac_ren 1); by (rtac impI 1); by (REPEAT (etac conjE 1)); -by (asm_full_simp_tac (simpset() addsimps [Impl.hdr_sum_def, +by (asm_full_simp_tac (simpset() addsimps [thm "Impl.hdr_sum_def", Multiset.count_def, Multiset.countm_nonempty_def, Multiset.delm_nonempty_def] @@ -125,7 +123,7 @@ by (hyp_subst_tac 1); by (rtac (pred_suc RS iffD1) 1); by (dtac less_le_trans 1); -by (cut_facts_tac [rewrite_rule[Packet.hdr_def] +by (cut_facts_tac [rewrite_rule[thm "Packet.hdr_def"] eq_packet_imp_eq_hdr RS countm_props] 1);; by (assume_tac 1); by (assume_tac 1); @@ -150,10 +148,10 @@ Goal "invariant impl_ioa inv2"; - by (rtac invariantI1 1); + by (rtac invariantI1 1); (* Base case *) by (asm_full_simp_tac (simpset() addsimps (inv2_def :: - (receiver_projections + (receiver_projections @ sender_projections @ impl_ioas))) 1); @@ -167,26 +165,26 @@ (* 10 - 7 *) by (EVERY1[tac2,tac2,tac2,tac2]); (* 6 *) - by (forward_tac [rewrite_rule [Impl.inv1_def] + by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] (inv1 RS invariantE) RS conjunct1] 1); (* 6 - 5 *) by (EVERY1[tac2,tac2]); (* 4 *) - by (forward_tac [rewrite_rule [Impl.inv1_def] + by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] (inv1 RS invariantE) RS conjunct1] 1); by (tac2 1); (* 3 *) - by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1); + by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] (inv1 RS invariantE)] 1); by (tac2 1); - by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]); + by (fold_tac [rewrite_rule [thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")]); by (arith_tac 1); (* 2 *) by (tac2 1); - by (forward_tac [rewrite_rule [Impl.inv1_def] + by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] (inv1 RS invariantE) RS conjunct1] 1); by (strip_tac 1); by (REPEAT (etac conjE 1)); @@ -194,11 +192,11 @@ (* 1 *) by (tac2 1); - by (forward_tac [rewrite_rule [Impl.inv1_def] + by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] (inv1 RS invariantE) RS conjunct2] 1); by (strip_tac 1); by (REPEAT (etac conjE 1)); - by (fold_tac [rewrite_rule[Packet.hdr_def]Impl.hdr_sum_def]); + by (fold_tac [rewrite_rule[thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")]); by (Asm_full_simp_tac 1); qed "inv2"; @@ -207,10 +205,10 @@ Goal "invariant impl_ioa inv3"; - by (rtac invariantI 1); + by (rtac invariantI 1); (* Base case *) - by (asm_full_simp_tac (simpset() addsimps - (Impl.inv3_def :: (receiver_projections + by (asm_full_simp_tac (simpset() addsimps + (thm "Impl.inv3_def" :: (receiver_projections @ sender_projections @ impl_ioas))) 1); by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1); @@ -221,7 +219,7 @@ (* 10 - 8 *) by (EVERY1[tac3,tac3,tac3]); - + by (tac_ren 1); by (strip_tac 1 THEN REPEAT (etac conjE 1)); by (hyp_subst_tac 1); @@ -231,7 +229,7 @@ (* 7 *) by (tac3 1); by (tac_ren 1); - by (Force_tac 1); + by (Force_tac 1); (* 6 - 3 *) @@ -243,7 +241,7 @@ by (strip_tac 1 THEN REPEAT (etac conjE 1)); by (rtac (imp_disjL RS iffD1) 1); by (rtac impI 1); - by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1); + by (forward_tac [rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE)] 1); by (Asm_full_simp_tac 1); by (REPEAT (etac conjE 1)); by (res_inst_tac [("j","count (ssent(sen s)) (~sbit(sen s))"), @@ -264,7 +262,7 @@ by (strip_tac 1 THEN REPEAT (etac conjE 1)); by (rtac (imp_disjL RS iffD1) 1); by (rtac impI 1); - by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1); + by (forward_tac [rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE)] 1); by (Asm_full_simp_tac 1); qed "inv3"; @@ -273,10 +271,10 @@ Goal "invariant impl_ioa inv4"; - by (rtac invariantI 1); + by (rtac invariantI 1); (* Base case *) - by (asm_full_simp_tac (simpset() addsimps - (Impl.inv4_def :: (receiver_projections + by (asm_full_simp_tac (simpset() addsimps + (thm "Impl.inv4_def" :: (receiver_projections @ sender_projections @ impl_ioas))) 1); by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1); @@ -291,7 +289,7 @@ (* 2 b *) by (strip_tac 1 THEN REPEAT (etac conjE 1)); - by (forward_tac [rewrite_rule [Impl.inv2_def] + by (forward_tac [rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE)] 1); by (Asm_full_simp_tac 1); @@ -299,9 +297,9 @@ by (tac4 1); by (strip_tac 1 THEN REPEAT (etac conjE 1)); by (rtac ccontr 1); - by (forward_tac [rewrite_rule [Impl.inv2_def] + by (forward_tac [rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE)] 1); - by (forward_tac [rewrite_rule [Impl.inv3_def] + by (forward_tac [rewrite_rule [thm "Impl.inv3_def"] (inv3 RS invariantE)] 1); by (Asm_full_simp_tac 1); by (eres_inst_tac [("x","m")] allE 1); @@ -311,7 +309,7 @@ (* rebind them *) -val inv1 = rewrite_rule [Impl.inv1_def] (inv1 RS invariantE); -val inv2 = rewrite_rule [Impl.inv2_def] (inv2 RS invariantE); -val inv3 = rewrite_rule [Impl.inv3_def] (inv3 RS invariantE); -val inv4 = rewrite_rule [Impl.inv4_def] (inv4 RS invariantE); +val inv1 = rewrite_rule [thm "Impl.inv1_def"] (inv1 RS invariantE); +val inv2 = rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE); +val inv3 = rewrite_rule [thm "Impl.inv3_def"] (inv3 RS invariantE); +val inv4 = rewrite_rule [thm "Impl.inv4_def"] (inv4 RS invariantE); diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Impl.thy --- a/src/HOLCF/IOA/NTP/Impl.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Impl.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,70 +1,76 @@ (* Title: HOL/IOA/NTP/Impl.thy ID: $Id$ Author: Tobias Nipkow & Konrad Slind - -The implementation. *) -Impl = Sender + Receiver + Abschannel + +header {* The implementation *} -types +theory Impl +imports Sender Receiver Abschannel +begin -'m impl_state +types + +'m impl_state = "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset" (* 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, inv2, - inv3, inv4 :: 'm impl_state => bool - hdr_sum :: 'm packet multiset => bool => nat + 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" defs - impl_def + impl_def: "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" - 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" + 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_def: "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)" (* Lemma 5.1 *) -inv1_def - "inv1(s) == - (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) - & (!b. count (ssent(sen s)) b +inv1_def: + "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) == - (rbit(rec(s)) = sbit(sen(s)) & - ssending(sen(s)) & + inv2_def: "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)) & - count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s))) - | - (rbit(rec(s)) = (~sbit(sen(s))) & - rsending(rec(s)) & + count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s))) + | + (rbit(rec(s)) = (~sbit(sen(s))) & + rsending(rec(s)) & count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) & count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))" (* Lemma 5.3 *) - inv3_def "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) - + count (srch s) (sbit(sen(s)),m) + inv3_def: "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) + + count (srch s) (sbit(sen(s)),m) <= count (rsent(rec s)) (~sbit(sen s)))" (* Lemma 5.4 *) - inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []" + inv4_def: "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []" + +ML {* use_legacy_bindings (the_context ()) *} end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Lemmas.thy --- a/src/HOLCF/IOA/NTP/Lemmas.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Lemmas.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,8 +1,11 @@ (* Title: HOL/IOA/NTP/Lemmas.thy ID: $Id$ Author: Tobias Nipkow & Konrad Slind - -Arithmetic lemmas. *) -Lemmas = NatArith +theory Lemmas +imports Main +begin + +end + diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Multiset.ML --- a/src/HOLCF/IOA/NTP/Multiset.ML Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Multiset.ML Sat Sep 03 16:50:22 2005 +0200 @@ -66,8 +66,9 @@ [Multiset.delm_empty_def, Multiset.countm_empty_def]) 1); by (asm_simp_tac (simpset() addsimps - [eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def, + [count_addm_simp,Multiset.delm_nonempty_def, Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1); + by (asm_simp_tac (simpset() addsimps [eq_sym_conv]) 1); qed "countm_done_delm"; diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Multiset.thy --- a/src/HOLCF/IOA/NTP/Multiset.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Multiset.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,47 +1,47 @@ (* Title: HOL/IOA/NTP/Multiset.thy ID: $Id$ Author: Tobias Nipkow & Konrad Slind - -Axiomatic multisets. -Should be done as a subtype and moved to a global place. *) -Multiset = Lemmas + +header {* Axiomatic multisets *} -types +theory Multiset +imports Lemmas +begin +typedecl 'a multiset -arities - - multiset :: (type) type - consts - "{|}" :: 'a multiset ("{|}") - addm :: ['a multiset, 'a] => 'a multiset - delm :: ['a multiset, 'a] => 'a multiset - countm :: ['a multiset, 'a => bool] => nat - count :: ['a multiset, 'a] => nat + "{|}" :: "'a multiset" ("{|}") + addm :: "['a multiset, 'a] => 'a multiset" + delm :: "['a multiset, 'a] => 'a multiset" + countm :: "['a multiset, 'a => bool] => nat" + count :: "['a multiset, 'a] => nat" -rules +axioms -delm_empty_def - "delm {|} x = {|}" +delm_empty_def: + "delm {|} x = {|}" -delm_nonempty_def +delm_nonempty_def: "delm (addm M x) y == (if x=y then M else addm (delm M y) x)" -countm_empty_def +countm_empty_def: "countm {|} P == 0" -countm_nonempty_def +countm_nonempty_def: "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)" -count_def +count_def: "count M x == countm M (%y. y = x)" -induction +"induction": "[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)" +ML {* use_text Context.ml_output true + ("structure Multiset = struct " ^ legacy_bindings (the_context ()) ^ " end") *} +ML {* open Multiset *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Packet.ML --- a/src/HOLCF/IOA/NTP/Packet.ML Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Packet.ML Sat Sep 03 16:50:22 2005 +0200 @@ -7,7 +7,7 @@ (* Instantiation of a tautology? *) Goal "!x. x = packet --> hdr(x) = hdr(packet)"; - by (simp_tac (simpset() addsimps [Packet.hdr_def]) 1); + by (simp_tac (simpset() addsimps [hdr_def]) 1); qed "eq_packet_imp_eq_hdr"; -Addsimps [Packet.hdr_def,Packet.msg_def]; +Addsimps [hdr_def,msg_def]; diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Packet.thy --- a/src/HOLCF/IOA/NTP/Packet.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Packet.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,22 +1,23 @@ (* Title: HOL/IOA/NTP/Packet.thy ID: $Id$ Author: Tobias Nipkow & Konrad Slind - -Packets. *) -Packet = Multiset + +theory Packet +imports Multiset +begin types - - 'msg packet = "bool * 'msg" + 'msg packet = "bool * 'msg" constdefs - hdr :: 'msg packet => bool + hdr :: "'msg packet => bool" "hdr == fst" - msg :: 'msg packet => 'msg + msg :: "'msg packet => 'msg" "msg == snd" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Receiver.ML --- a/src/HOLCF/IOA/NTP/Receiver.ML Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Receiver.ML Sat Sep 03 16:50:22 2005 +0200 @@ -14,15 +14,13 @@ \ C_m_r : actions(receiver_asig) & \ \ C_r_s ~: actions(receiver_asig) & \ \ C_r_r(m) : actions(receiver_asig)"; - by (simp_tac (simpset() addsimps (Receiver.receiver_asig_def :: actions_def :: + by (simp_tac (simpset() addsimps (receiver_asig_def :: actions_def :: asig_projections)) 1); qed "in_receiver_asig"; -val receiver_projections = - [Receiver.rq_def, - Receiver.rsent_def, - Receiver.rrcvd_def, - Receiver.rbit_def, - Receiver.rsending_def]; - - +val receiver_projections = + [rq_def, + rsent_def, + rrcvd_def, + rbit_def, + rsending_def]; diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Receiver.thy --- a/src/HOLCF/IOA/NTP/Receiver.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Receiver.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,13 +1,15 @@ (* Title: HOL/IOA/NTP/Receiver.thy ID: $Id$ Author: Tobias Nipkow & Konrad Slind - -The implementation: receiver. *) -Receiver = List + IOA + Action + +header {* The implementation: receiver *} -types +theory Receiver +imports IOA Action +begin + +types 'm receiver_state = "'m list * bool multiset * 'm packet multiset * bool * bool" @@ -16,73 +18,75 @@ 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 + 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 -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" +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" -receiver_asig_def "receiver_asig == - (UN pkt. {R_pkt(pkt)}, - (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), +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 == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in - case fst(snd(tr)) - of - S_msg(m) => False | - R_msg(m) => rq(s) = (m # rq(t)) & - rsent(t)=rsent(s) & - rrcvd(t)=rrcvd(s) & - rbit(t)=rbit(s) & - rsending(t)=rsending(s) | - S_pkt(pkt) => False | - R_pkt(pkt) => rq(t) = rq(s) & - rsent(t) = rsent(s) & - rrcvd(t) = addm (rrcvd s) pkt & - rbit(t) = rbit(s) & - rsending(t) = rsending(s) | - S_ack(b) => b = rbit(s) & - rq(t) = rq(s) & - rsent(t) = addm (rsent s) (rbit s) & - rrcvd(t) = rrcvd(s) & - rbit(t)=rbit(s) & - rsending(s) & - rsending(t) | - R_ack(b) => False | - C_m_s => False | - C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y. hdr(y)=rbit(s)) & - rq(t) = rq(s) & - rsent(t)=rsent(s) & - rrcvd(t)=rrcvd(s) & - rbit(t)=rbit(s) & - rsending(s) & - ~rsending(t) | - C_r_s => False | - C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y. hdr(y)=rbit(s)) & - count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) & - rq(t) = rq(s)@[m] & - rsent(t)=rsent(s) & - rrcvd(t)=rrcvd(s) & - rbit(t) = (~rbit(s)) & - ~rsending(s) & +receiver_trans_def: "receiver_trans == + {tr. let s = fst(tr); + t = snd(snd(tr)) + in + case fst(snd(tr)) + of + S_msg(m) => False | + R_msg(m) => rq(s) = (m # rq(t)) & + rsent(t)=rsent(s) & + rrcvd(t)=rrcvd(s) & + rbit(t)=rbit(s) & + rsending(t)=rsending(s) | + S_pkt(pkt) => False | + R_pkt(pkt) => rq(t) = rq(s) & + rsent(t) = rsent(s) & + rrcvd(t) = addm (rrcvd s) pkt & + rbit(t) = rbit(s) & + rsending(t) = rsending(s) | + S_ack(b) => b = rbit(s) & + rq(t) = rq(s) & + rsent(t) = addm (rsent s) (rbit s) & + rrcvd(t) = rrcvd(s) & + rbit(t)=rbit(s) & + rsending(s) & + rsending(t) | + R_ack(b) => False | + C_m_s => False | + C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y. hdr(y)=rbit(s)) & + rq(t) = rq(s) & + rsent(t)=rsent(s) & + rrcvd(t)=rrcvd(s) & + rbit(t)=rbit(s) & + rsending(s) & + ~rsending(t) | + C_r_s => False | + C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y. hdr(y)=rbit(s)) & + count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) & + rq(t) = rq(s)@[m] & + rsent(t)=rsent(s) & + rrcvd(t)=rrcvd(s) & + rbit(t) = (~rbit(s)) & + ~rsending(s) & rsending(t)}" -receiver_ioa_def "receiver_ioa == +receiver_ioa_def: "receiver_ioa == (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Sender.ML --- a/src/HOLCF/IOA/NTP/Sender.ML Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Sender.ML Sat Sep 03 16:50:22 2005 +0200 @@ -15,10 +15,10 @@ \ C_r_s : actions(sender_asig) & \ \ C_r_r(m) ~: actions(sender_asig)"; by (simp_tac (simpset() addsimps - (Sender.sender_asig_def :: actions_def :: + (sender_asig_def :: actions_def :: asig_projections)) 1); qed "in_sender_asig"; val sender_projections = - [Sender.sq_def,Sender.ssent_def,Sender.srcvd_def, - Sender.sbit_def,Sender.ssending_def]; + [sq_def,ssent_def,srcvd_def, + sbit_def,ssending_def]; diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Sender.thy --- a/src/HOLCF/IOA/NTP/Sender.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Sender.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,84 +1,88 @@ (* Title: HOL/IOA/NTP/Sender.thy ID: $Id$ Author: Tobias Nipkow & Konrad Slind - -The implementation: sender. *) -Sender = IOA + Action + List + +header {* The implementation: sender *} + +theory Sender +imports IOA Action +begin types - '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,srcvd :: 'm sender_state => bool multiset -sbit :: 'm sender_state => bool -ssending :: 'm sender_state => bool +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 -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" +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" -sender_asig_def - "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), - UN pkt. {S_pkt(pkt)}, +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 == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - S_msg(m) => sq(t)=sq(s)@[m] & - ssent(t)=ssent(s) & - srcvd(t)=srcvd(s) & - sbit(t)=sbit(s) & - ssending(t)=ssending(s) | - R_msg(m) => False | - S_pkt(pkt) => hdr(pkt) = sbit(s) & - (? Q. sq(s) = (msg(pkt)#Q)) & - sq(t) = sq(s) & - ssent(t) = addm (ssent s) (sbit s) & - srcvd(t) = srcvd(s) & - sbit(t) = sbit(s) & - ssending(s) & - ssending(t) | - R_pkt(pkt) => False | - S_ack(b) => False | - R_ack(b) => sq(t)=sq(s) & - ssent(t)=ssent(s) & - srcvd(t) = addm (srcvd s) b & - sbit(t)=sbit(s) & - ssending(t)=ssending(s) | - C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) & - sq(t)=sq(s) & - ssent(t)=ssent(s) & - srcvd(t)=srcvd(s) & - sbit(t)=sbit(s) & - ssending(s) & - ~ssending(t) | - C_m_r => False | - C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) & - sq(t)=tl(sq(s)) & - ssent(t)=ssent(s) & - srcvd(t)=srcvd(s) & - sbit(t) = (~sbit(s)) & - ~ssending(s) & - ssending(t) | +sender_trans_def: "sender_trans == + {tr. let s = fst(tr); + t = snd(snd(tr)) + in case fst(snd(tr)) + of + S_msg(m) => sq(t)=sq(s)@[m] & + ssent(t)=ssent(s) & + srcvd(t)=srcvd(s) & + sbit(t)=sbit(s) & + ssending(t)=ssending(s) | + R_msg(m) => False | + S_pkt(pkt) => hdr(pkt) = sbit(s) & + (? Q. sq(s) = (msg(pkt)#Q)) & + sq(t) = sq(s) & + ssent(t) = addm (ssent s) (sbit s) & + srcvd(t) = srcvd(s) & + sbit(t) = sbit(s) & + ssending(s) & + ssending(t) | + R_pkt(pkt) => False | + S_ack(b) => False | + R_ack(b) => sq(t)=sq(s) & + ssent(t)=ssent(s) & + srcvd(t) = addm (srcvd s) b & + sbit(t)=sbit(s) & + ssending(t)=ssending(s) | + C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) & + sq(t)=sq(s) & + ssent(t)=ssent(s) & + srcvd(t)=srcvd(s) & + sbit(t)=sbit(s) & + ssending(s) & + ~ssending(t) | + C_m_r => False | + C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) & + sq(t)=tl(sq(s)) & + ssent(t)=ssent(s) & + srcvd(t)=srcvd(s) & + sbit(t) = (~sbit(s)) & + ~ssending(s) & + ssending(t) | C_r_r(m) => False}" -sender_ioa_def "sender_ioa == +sender_ioa_def: "sender_ioa == (sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Spec.thy --- a/src/HOLCF/IOA/NTP/Spec.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Spec.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,25 +1,27 @@ (* Title: HOL/IOA/NTP/Spec.thy ID: $Id$ Author: Tobias Nipkow & Konrad Slind - -The specification of reliable transmission. *) -Spec = List + IOA + Action + +header {* The specification of reliable transmission *} + +theory Spec +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 +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)}, +sig_def: "spec_sig == (UN m.{S_msg(m)}, UN m.{R_msg(m)}, {})" -trans_def "spec_trans == +trans_def: "spec_trans == {tr. let s = fst(tr); t = snd(snd(tr)) in @@ -36,6 +38,8 @@ C_r_s => False | C_r_r(m) => False}" -ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans,{},{})" +ioa_def: "spec_ioa == (spec_sig, {[]}, spec_trans,{},{})" + +ML {* use_legacy_bindings (the_context ()) *} end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/Storage/Action.thy --- a/src/HOLCF/IOA/Storage/Action.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/Storage/Action.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,10 +1,19 @@ (* Title: HOLCF/IOA/ABP/Action.thy ID: $Id$ Author: Olaf Müller - -The set of all actions of the system. *) -Action = Main + -datatype action = New | Loc nat | Free nat +header {* The set of all actions of the system *} + +theory Action +imports Main +begin + +datatype action = New | Loc nat | Free nat + +lemma [cong]: "!!x. x = y ==> action_case a b c x = action_case a b c y" + by simp + +ML {* use_legacy_bindings (the_context ()) *} + end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/Storage/Correctness.ML --- a/src/HOLCF/IOA/Storage/Correctness.ML Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/Storage/Correctness.ML Sat Sep 03 16:50:22 2005 +0200 @@ -1,8 +1,6 @@ (* Title: HOL/IOA/example/Correctness.ML ID: $Id$ Author: Olaf Müller - -Correctness Proof. *) @@ -11,11 +9,11 @@ (* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive - simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans + simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans Idea: ?ex. move .. should be generally replaced by a step via a subst tac if desired, as this can be done globally *) -Goal +Goal "is_simulation sim_relation impl_ioa spec_ioa"; by (simp_tac (simpset() addsimps [is_simulation_def]) 1); by (rtac conjI 1); @@ -23,7 +21,7 @@ by (SELECT_GOAL (safe_tac set_cs) 1); by (res_inst_tac [("x","({},False)")] exI 1); by (asm_full_simp_tac (simpset() addsimps [sim_relation_def,starts_of_def, - Spec.ioa_def,Impl.ioa_def]) 1); + thm "Spec.ioa_def", thm "Impl.ioa_def"]) 1); (* ---------------- main-part ------------------- *) by (REPEAT (rtac allI 1)); @@ -31,41 +29,40 @@ ren "k b used c k' b' a" 1; by (induct_tac "a" 1); by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def, - Impl.ioa_def,Impl.trans_def,trans_of_def]))); + thm"Impl.ioa_def",thm "Impl.trans_def",trans_of_def]))); by (safe_tac set_cs); (* NEW *) by (res_inst_tac [("x","(used,True)")] exI 1); by (Asm_full_simp_tac 1); by (rtac transition_is_ex 1); by (simp_tac (simpset() addsimps [ - Spec.ioa_def,Spec.trans_def,trans_of_def])1); + thm "Spec.ioa_def", thm "Spec.trans_def",trans_of_def])1); (* LOC *) by (res_inst_tac [("x","(used Un {k},False)")] exI 1); by (asm_full_simp_tac (simpset() addsimps [less_SucI]) 1); by (rtac transition_is_ex 1); by (simp_tac (simpset() addsimps [ - Spec.ioa_def,Spec.trans_def,trans_of_def])1); + thm "Spec.ioa_def", thm "Spec.trans_def",trans_of_def])1); by (Fast_tac 1); (* FREE *) by (res_inst_tac [("x","(used - {nat},c)")] exI 1); by (Asm_full_simp_tac 1); by (rtac transition_is_ex 1); by (simp_tac (simpset() addsimps [ - Spec.ioa_def,Spec.trans_def,trans_of_def])1); + thm "Spec.ioa_def",thm "Spec.trans_def",trans_of_def])1); qed"issimulation"; -Goalw [ioa_implements_def] +Goalw [ioa_implements_def] "impl_ioa =<| spec_ioa"; by (rtac conjI 1); -by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def, - Impl.ioa_def,Spec.ioa_def, asig_outputs_def,asig_of_def, +by (simp_tac (simpset() addsimps [thm "Impl.sig_def",thm "Spec.sig_def", + thm "Impl.ioa_def",thm "Spec.ioa_def", asig_outputs_def,asig_of_def, asig_inputs_def]) 1); by (rtac trace_inclusion_for_simulations 1); -by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def, - Impl.ioa_def,Spec.ioa_def, externals_def,asig_outputs_def,asig_of_def, +by (simp_tac (simpset() addsimps [thm "Impl.sig_def",thm "Spec.sig_def", + thm "Impl.ioa_def",thm "Spec.ioa_def", externals_def,asig_outputs_def,asig_of_def, asig_inputs_def]) 1); by (rtac issimulation 1); qed"implementation"; - diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/Storage/Correctness.thy --- a/src/HOLCF/IOA/Storage/Correctness.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/Storage/Correctness.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,25 +1,24 @@ (* Title: HOL/IOA/example/Correctness.thy ID: $Id$ Author: Olaf Müller - -Correctness Proof. *) -Correctness = SimCorrectness + Spec + Impl + +header {* Correctness Proof *} -default type - -consts +theory Correctness +imports SimCorrectness Spec Impl +begin -sim_relation :: "((nat * bool) * (nat set * bool)) set" +defaultsort type -defs - -sim_relation_def - "sim_relation == {qua. let c = fst qua; a = snd qua ; +constdefs + sim_relation :: "((nat * bool) * (nat set * bool)) set" + "sim_relation == {qua. let c = fst qua; a = snd qua ; k = fst c; b = snd c; used = fst a; c = snd a in (! l:used. l < k) & b=c }" -end \ No newline at end of file +ML {* use_legacy_bindings (the_context ()) *} + +end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/Storage/Impl.thy --- a/src/HOLCF/IOA/Storage/Impl.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/Storage/Impl.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,12 +1,13 @@ (* Title: HOL/IOA/example/Spec.thy ID: $Id$ Author: Olaf Müller - -The implementation of a memory. *) -Impl = IOA + Action + +header {* The implementation of a memory *} +theory Impl +imports IOA Action +begin consts @@ -16,20 +17,28 @@ defs -sig_def "impl_sig == (UN l.{Free l} Un {New}, - UN l.{Loc l}, +sig_def: "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' | +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}" -ioa_def "impl_ioa == (impl_sig, {(0,False)}, impl_trans,{},{})" +ioa_def: "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) + +ML {* use_legacy_bindings (the_context ()) *} end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/Storage/Spec.thy --- a/src/HOLCF/IOA/Storage/Spec.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/Storage/Spec.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,12 +1,13 @@ (* Title: HOL/IOA/example/Spec.thy ID: $Id$ Author: Olaf Müller - -The specification of a memory. *) -Spec = IOA + Action + +header {* The specification of a memory *} +theory Spec +imports IOA Action +begin consts @@ -16,20 +17,22 @@ defs -sig_def "spec_sig == (UN l.{Free l} Un {New}, - UN l.{Loc l}, +sig_def: "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' | +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}" -ioa_def "spec_ioa == (spec_sig, {({},False)}, spec_trans,{},{})" +ioa_def: "spec_ioa == (spec_sig, {({},False)}, spec_trans,{},{})" + +ML {* use_legacy_bindings (the_context ()) *} end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ex/TrivEx.thy --- a/src/HOLCF/IOA/ex/TrivEx.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ex/TrivEx.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,60 +1,64 @@ (* Title: HOLCF/IOA/TrivEx.thy ID: $Id$ Author: Olaf Müller - -Trivial Abstraction Example. *) -TrivEx = Abstraction + +header {* Trivial Abstraction Example *} + +theory TrivEx +imports Abstraction +begin datatype action = INC consts C_asig :: "action signature" -C_trans :: (action, nat)transition set -C_ioa :: (action, nat)ioa +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 +A_trans :: "(action, bool)transition set" +A_ioa :: "(action, bool)ioa" h_abs :: "nat => bool" defs -C_asig_def +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 +C_trans_def: "C_trans == + {tr. let s = fst(tr); + t = snd(snd(tr)) + in case fst(snd(tr)) + of INC => t = Suc(s)}" -C_ioa_def "C_ioa == +C_ioa_def: "C_ioa == (C_asig, {0}, C_trans,{},{})" -A_asig_def +A_asig_def: "A_asig == ({},{INC},{})" -A_trans_def "A_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of +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_ioa_def: "A_ioa == (A_asig, {False}, A_trans,{},{})" -h_abs_def +h_abs_def: "h_abs n == n~=0" -rules +axioms -MC_result +MC_result: "validIOA A_ioa (<>[] <%(b,a,c). b>)" -end \ No newline at end of file +ML {* use_legacy_bindings (the_context ()) *} + +end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/ex/TrivEx2.thy --- a/src/HOLCF/IOA/ex/TrivEx2.thy Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/ex/TrivEx2.thy Sat Sep 03 16:50:22 2005 +0200 @@ -1,70 +1,73 @@ (* Title: HOLCF/IOA/TrivEx.thy ID: $Id$ Author: Olaf Müller - -Trivial Abstraction Example with fairness. *) -TrivEx2 = Abstraction + IOA + +header {* Trivial Abstraction Example with fairness *} + +theory TrivEx2 +imports IOA Abstraction +begin 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 +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 +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_def: "C_asig == ({},{INC},{})" -C_trans_def "C_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of +C_trans_def: "C_trans == + {tr. let s = fst(tr); + t = snd(snd(tr)) + in case fst(snd(tr)) + of INC => t = Suc(s)}" -C_ioa_def "C_ioa == +C_ioa_def: "C_ioa == (C_asig, {0}, C_trans,{},{})" -C_live_ioa_def +C_live_ioa_def: "C_live_ioa == (C_ioa, WF C_ioa {INC})" -A_asig_def +A_asig_def: "A_asig == ({},{INC},{})" -A_trans_def "A_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of +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_ioa_def: "A_ioa == (A_asig, {False}, A_trans,{},{})" -A_live_ioa_def +A_live_ioa_def: "A_live_ioa == (A_ioa, WF A_ioa {INC})" - -h_abs_def +h_abs_def: "h_abs n == n~=0" -rules +axioms -MC_result +MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)" -end \ No newline at end of file +ML {* use_legacy_bindings (the_context ()) *} + +end diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/meta_theory/Asig.ML --- a/src/HOLCF/IOA/meta_theory/Asig.ML Sat Sep 03 16:49:48 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Asig.ML Sat Sep 03 16:50:22 2005 +0200 @@ -3,7 +3,7 @@ Author: Olaf Müller, Tobias Nipkow & Konrad Slind *) -val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def]; +bind_thms ("asig_projections", [asig_inputs_def, asig_outputs_def, asig_internals_def]); Goal "(outputs (a,b,c) = b) & \