--- 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 @@
-
-
-
-
-
--- 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
--- 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
--- 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,
--- 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
-
-
--- 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
-
--- 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
--- 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
-
--- 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 =
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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";
-
--- 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
--- 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
--- 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);
--- 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
--- 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);
--- 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
--- 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
+
--- 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";
--- 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
--- 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];
--- 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
--- 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];
--- 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
--- 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];
--- 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
--- 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
--- 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
--- 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";
-
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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) & \