--- a/src/HOLCF/IOA/meta_theory/Automata.ML Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Thu Jul 17 12:43:32 1997 +0200
@@ -11,7 +11,7 @@
open reachable;
-val ioa_projections = [asig_of_def, starts_of_def, trans_of_def];
+val ioa_projections = [asig_of_def, starts_of_def, trans_of_def,wfair_of_def,sfair_of_def];
(* ----------------------------------------------------------------------------------- *)
@@ -19,12 +19,16 @@
goal thy
-"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z";
+ "((asig_of (x,y,z,w,s)) = x) & \
+\ ((starts_of (x,y,z,w,s)) = y) & \
+\ ((trans_of (x,y,z,w,s)) = z) & \
+\ ((wfair_of (x,y,z,w,s)) = w) & \
+\ ((sfair_of (x,y,z,w,s)) = s)";
by (simp_tac (!simpset addsimps ioa_projections) 1);
qed "ioa_triple_proj";
-goalw thy [ioa_def,state_trans_def,actions_def, is_asig_def]
- "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:act A";
+goalw thy [is_trans_of_def,actions_def, is_asig_def]
+ "!!A. [| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A";
by (REPEAT(etac conjE 1));
by (EVERY1[etac allE, etac impE, atac]);
by (Asm_full_simp_tac 1);
@@ -35,6 +39,20 @@
by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
qed "starts_of_par";
+goal thy
+"trans_of(A || B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \
+\ in (a:act A | a:act B) & \
+\ (if a:act A then \
+\ (fst(s),a,fst(t)):trans_of(A) \
+\ else fst(t) = fst(s)) \
+\ & \
+\ (if a:act B then \
+\ (snd(s),a,snd(t)):trans_of(B) \
+\ else snd(t) = snd(s))}";
+
+by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+qed "trans_of_par";
+
(* ----------------------------------------------------------------------------------- *)
@@ -70,7 +88,6 @@
by (fast_tac set_cs 1);
qed"actions_of_par";
-
goal thy "inp (A1||A2) =\
\ ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))";
by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
@@ -121,6 +138,7 @@
by (best_tac (set_cs addEs [equalityCE]) 1);
qed"intA_is_not_actB";
+(* the only one that needs disjointness of outputs and of internals and _all_ acts *)
goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
compatible_def,is_asig_def,asig_of_def]
"!! a. [| compatible A B; a:out A ;a:act B|] ==> a : inp B";
@@ -128,7 +146,85 @@
by (best_tac (set_cs addEs [equalityCE]) 1);
qed"outAactB_is_inpB";
+(* needed for propagation of input_enabledness from A,B to A||B *)
+goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
+ compatible_def,is_asig_def,asig_of_def]
+"!! a. [| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B";
+by (Asm_full_simp_tac 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"inpAAactB_is_inpBoroutB";
+(* ---------------------------------------------------------------------------------- *)
+
+section "input_enabledness and par";
+
+
+(* ugly case distinctions. Heart of proof:
+ 1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
+ 2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
+goalw thy [input_enabled_def]
+"!!A. [| compatible A B; input_enabled A; input_enabled B|] \
+\ ==> input_enabled (A||B)";
+by (asm_full_simp_tac (!simpset addsimps [inputs_of_par,trans_of_par]) 1);
+by (safe_tac set_cs);
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 2);
+(* a: inp A *)
+by (case_tac "a:act B" 1);
+(* a:act B *)
+by (eres_inst_tac [("x","a")] allE 1);
+by (Asm_full_simp_tac 1);
+bd inpAAactB_is_inpBoroutB 1;
+ba 1;
+ba 1;
+by (eres_inst_tac [("x","a")] allE 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","aa")] allE 1);
+by (eres_inst_tac [("x","b")] allE 1);
+be exE 1;
+be exE 1;
+by (res_inst_tac [("x","(s2,s2a)")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+(* a~: act B*)
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","aa")] allE 1);
+be exE 1;
+by (res_inst_tac [("x","(s2,b)")] exI 1);
+by (Asm_full_simp_tac 1);
+
+(* a:inp B *)
+by (case_tac "a:act A" 1);
+(* a:act A *)
+by (eres_inst_tac [("x","a")] allE 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
+bd inpAAactB_is_inpBoroutB 1;
+back();
+ba 1;
+ba 1;
+by (Asm_full_simp_tac 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","aa")] allE 1);
+by (eres_inst_tac [("x","b")] allE 1);
+be exE 1;
+be exE 1;
+by (res_inst_tac [("x","(s2,s2a)")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+(* a~: act B*)
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","b")] allE 1);
+be exE 1;
+by (res_inst_tac [("x","(aa,s2)")] exI 1);
+by (Asm_full_simp_tac 1);
+qed"input_enabled_par";
(* ---------------------------------------------------------------------------------- *)
@@ -288,4 +384,55 @@
qed "trans_of_par4";
+(* ---------------------------------------------------------------------------------- *)
+section "proof obligation generator for IOA requirements";
+
+(* without assumptions on A and B because is_trans_of is also incorporated in ||def *)
+goalw thy [is_trans_of_def]
+"is_trans_of (A||B)";
+by (simp_tac (!simpset addsimps [actions_of_par,trans_of_par]) 1);
+qed"is_trans_of_par";
+
+
+(*
+
+goalw thy [is_trans_of_def,restrict_def,restrict_asig_def]
+"!!A. is_trans_of A ==> is_trans_of (restrict A acts)";
+by (asm_full_simp_tac (!simpset addsimps [actions_def,trans_of_def,
+ asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,asig_of_def]) 1);
+
+qed"";
+
+
+goalw thy [is_trans_of_def,restrict_def,restrict_asig_def]
+"!!A. is_trans_of A ==> is_trans_of (rename A f)";
+by (asm_full_simp_tac (!simpset addsimps [actions_def,trans_of_def,
+ asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,asig_of_def]) 1);
+
+qed"";
+
+goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)";
+
+
+goalw thy [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def,
+ asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def]
+"!! A. is_asig_of A ==> is_asig_of (restrict A f)";
+by (Asm_full_simp_tac 1);
+
+
+
+
+goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|] \
+\ ==> is_asig_of (A||B)";
+
+
+
+
+
+*)
+
+
+
+
+
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Thu Jul 17 12:43:32 1997 +0200
@@ -13,17 +13,24 @@
types
('a,'s)transition = "'s * 'a * 's"
- ('a,'s)ioa = "'a signature * 's set * ('a,'s)transition set"
+ ('a,'s)ioa = "'a signature * 's set * ('a,'s)transition set *
+ (('a set) set) * (('a set) set)"
consts
(* IO automata *)
- state_trans ::"['a signature, ('a,'s)transition set] => bool"
- input_enabled::"['a signature, ('a,'s)transition set] => bool"
- asig_of ::"('a,'s)ioa => 'a signature"
- starts_of ::"('a,'s)ioa => 's set"
- trans_of ::"('a,'s)ioa => ('a,'s)transition set"
- IOA ::"('a,'s)ioa => bool"
+
+ asig_of ::"('a,'s)ioa => 'a signature"
+ starts_of ::"('a,'s)ioa => 's set"
+ trans_of ::"('a,'s)ioa => ('a,'s)transition set"
+ wfair_of ::"('a,'s)ioa => ('a set) set"
+ sfair_of ::"('a,'s)ioa => ('a set) set"
+
+ is_asig_of ::"('a,'s)ioa => bool"
+ is_starts_of ::"('a,'s)ioa => bool"
+ is_trans_of ::"('a,'s)ioa => bool"
+ input_enabled ::"('a,'s)ioa => bool"
+ IOA ::"('a,'s)ioa => bool"
(* reachability and invariants *)
reachable :: "('a,'s)ioa => 's set"
@@ -31,15 +38,18 @@
(* binary composition of action signatures and automata *)
asig_comp ::"['a signature, 'a signature] => 'a signature"
- compatible ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
+ compatible ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
"||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr 10)
- (* hiding *)
+ (* hiding and restricting *)
+ hide_asig :: "['a signature, 'a set] => 'a signature"
+ hide :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
restrict_asig :: "['a signature, 'a set] => 'a signature"
restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
(* renaming *)
- rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
+ rename_set :: "'a set => ('c => 'a option) => 'c set"
+ rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
syntax
@@ -83,24 +93,34 @@
(* --------------------------------- IOA ---------------------------------*)
-state_trans_def
- "state_trans asig R ==
- (!triple. triple:R --> fst(snd(triple)):actions(asig))"
-
-input_enabled_def
- "input_enabled asig R ==
- (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
asig_of_def "asig_of == fst"
starts_of_def "starts_of == (fst o snd)"
-trans_of_def "trans_of == (snd o snd)"
+trans_of_def "trans_of == (fst o snd o snd)"
+wfair_of_def "wfair_of == (fst o snd o snd o snd)"
+sfair_of_def "sfair_of == (snd o snd o snd o snd)"
+
+is_asig_of_def
+ "is_asig_of A == is_asig (asig_of A)"
+
+is_starts_of_def
+ "is_starts_of A == (~ starts_of A = {})"
+
+is_trans_of_def
+ "is_trans_of A ==
+ (!triple. triple:(trans_of A) --> fst(snd(triple)):actions(asig_of A))"
+
+input_enabled_def
+ "input_enabled A ==
+ (!a. (a:inputs(asig_of A)) --> (!s1. ? s2. (s1,a,s2):(trans_of A)))"
+
ioa_def
- "IOA(ioa) == (is_asig(asig_of(ioa)) &
- (~ starts_of(ioa) = {}) &
- state_trans (asig_of ioa) (trans_of ioa) &
- input_enabled (asig_of ioa) (trans_of ioa))"
+ "IOA A == (is_asig_of A &
+ is_starts_of A &
+ is_trans_of A &
+ input_enabled A)"
invariant_def "invariant A P == (!s. reachable A s --> P(s))"
@@ -121,44 +141,73 @@
(outputs(a1) Un outputs(a2)),
(internals(a1) Un internals(a2))))"
-
par_def
- "(ioa1 || ioa2) ==
- (asig_comp (asig_of ioa1) (asig_of ioa2),
- {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
+ "(A || B) ==
+ (asig_comp (asig_of A) (asig_of B),
+ {pr. fst(pr):starts_of(A) & snd(pr):starts_of(B)},
{tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
- in (a:act ioa1 | a:act ioa2) &
- (if a:act ioa1 then
- (fst(s),a,fst(t)):trans_of(ioa1)
+ in (a:act A | a:act B) &
+ (if a:act A then
+ (fst(s),a,fst(t)):trans_of(A)
else fst(t) = fst(s))
&
- (if a:act ioa2 then
- (snd(s),a,snd(t)):trans_of(ioa2)
- else snd(t) = snd(s))})"
+ (if a:act B then
+ (snd(s),a,snd(t)):trans_of(B)
+ else snd(t) = snd(s))},
+ wfair_of A Un wfair_of B,
+ sfair_of A Un sfair_of B)"
+
(* ------------------------ hiding -------------------------------------------- *)
restrict_asig_def
"restrict_asig asig actns ==
- (inputs(asig) Int actns, outputs(asig) Int actns,
+ (inputs(asig) Int actns,
+ outputs(asig) Int actns,
internals(asig) Un (externals(asig) - actns))"
+(* Notice that for wfair_of and sfair_of nothing has to be changed, as
+ changes from the outputs to the internals does not touch the locals as
+ a whole, which is of importance for fairness only *)
restrict_def
- "restrict ioa actns ==
- (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
+ "restrict A actns ==
+ (restrict_asig (asig_of A) actns,
+ starts_of A,
+ trans_of A,
+ wfair_of A,
+ sfair_of A)"
+
+hide_asig_def
+ "hide_asig asig actns ==
+ (inputs(asig) - actns,
+ outputs(asig) - actns,
+ internals(asig) Un actns)"
+
+hide_def
+ "hide A actns ==
+ (hide_asig (asig_of A) actns,
+ starts_of A,
+ trans_of A,
+ wfair_of A,
+ sfair_of A)"
(* ------------------------- renaming ------------------------------------------- *)
+rename_set_def
+ "rename_set set ren == {b. ? x. Some x = ren b & x : set}"
+
rename_def
"rename ioa ren ==
- (({b. ? x. Some(x)= ren(b) & x : inp ioa},
- {b. ? x. Some(x)= ren(b) & x : out ioa},
- {b. ? x. Some(x)= ren(b) & x : int ioa}),
- starts_of(ioa) ,
+ ((rename_set (inp ioa) ren,
+ rename_set (out ioa) ren,
+ rename_set (int ioa) ren),
+ starts_of ioa,
{tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
in
- ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
+ ? x. Some(x) = ren(a) & (s,x,t):trans_of ioa},
+ {rename_set s ren | s. s: wfair_of ioa},
+ {rename_set s ren | s. s: sfair_of ioa})"
end
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Thu Jul 17 12:43:32 1997 +0200
@@ -57,18 +57,18 @@
(* ---------------------------------------------------------------- *)
-goal thy "Filter_ex2 A`UU=UU";
+goal thy "Filter_ex2 sig`UU=UU";
by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
qed"Filter_ex2_UU";
-goal thy "Filter_ex2 A`nil=nil";
+goal thy "Filter_ex2 sig`nil=nil";
by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
qed"Filter_ex2_nil";
-goal thy "Filter_ex2 A`(at >> xs) = \
-\ (if (fst at:act A) \
-\ then at >> (Filter_ex2 A`xs) \
-\ else Filter_ex2 A`xs)";
+goal thy "Filter_ex2 sig`(at >> xs) = \
+\ (if (fst at:actions sig) \
+\ then at >> (Filter_ex2 sig`xs) \
+\ else Filter_ex2 sig`xs)";
by (asm_full_simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
qed"Filter_ex2_cons";
@@ -79,13 +79,13 @@
(* ---------------------------------------------------------------- *)
-goal thy "stutter2 A = (LAM ex. (%s. case ex of \
+goal thy "stutter2 sig = (LAM ex. (%s. case ex of \
\ nil => TT \
\ | x##xs => (flift1 \
-\ (%p.(If Def ((fst p)~:act A) \
+\ (%p.(If Def ((fst p)~:actions sig) \
\ then Def (s=(snd p)) \
\ else TT fi) \
-\ andalso (stutter2 A`xs) (snd p)) \
+\ andalso (stutter2 sig`xs) (snd p)) \
\ `x) \
\ ))";
by (rtac trans 1);
@@ -95,20 +95,20 @@
by (simp_tac (!simpset addsimps [flift1_def]) 1);
qed"stutter2_unfold";
-goal thy "(stutter2 A`UU) s=UU";
+goal thy "(stutter2 sig`UU) s=UU";
by (stac stutter2_unfold 1);
by (Simp_tac 1);
qed"stutter2_UU";
-goal thy "(stutter2 A`nil) s = TT";
+goal thy "(stutter2 sig`nil) s = TT";
by (stac stutter2_unfold 1);
by (Simp_tac 1);
qed"stutter2_nil";
-goal thy "(stutter2 A`(at>>xs)) s = \
-\ ((if (fst at)~:act A then Def (s=snd at) else TT) \
-\ andalso (stutter2 A`xs) (snd at))";
-by (rtac trans 1);
+goal thy "(stutter2 sig`(at>>xs)) s = \
+\ ((if (fst at)~:actions sig then Def (s=snd at) else TT) \
+\ andalso (stutter2 sig`xs) (snd at))";
+br trans 1;
by (stac stutter2_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1);
by (Simp_tac 1);
@@ -122,16 +122,16 @@
(* stutter *)
(* ---------------------------------------------------------------- *)
-goal thy "stutter A (s, UU)";
+goal thy "stutter sig (s, UU)";
by (simp_tac (!simpset addsimps [stutter_def]) 1);
qed"stutter_UU";
-goal thy "stutter A (s, nil)";
+goal thy "stutter sig (s, nil)";
by (simp_tac (!simpset addsimps [stutter_def]) 1);
qed"stutter_nil";
-goal thy "stutter A (s, (a,t)>>ex) = \
-\ ((a~:act A --> (s=t)) & stutter A (t,ex))";
+goal thy "stutter sig (s, (a,t)>>ex) = \
+\ ((a~:actions sig --> (s=t)) & stutter sig (t,ex))";
by (simp_tac (!simpset addsimps [stutter_def]
setloop (split_tac [expand_if]) ) 1);
qed"stutter_cons";
@@ -160,8 +160,8 @@
(* --------------------------------------------------------------------- *)
goal thy "!s. is_exec_frag (A||B) (s,xs) \
-\ --> is_exec_frag A (fst s, Filter_ex2 A`(ProjA2`xs)) &\
-\ is_exec_frag B (snd s, Filter_ex2 B`(ProjB2`xs))";
+\ --> is_exec_frag A (fst s, Filter_ex2 (asig_of A)`(ProjA2`xs)) &\
+\ is_exec_frag B (snd s, Filter_ex2 (asig_of B)`(ProjB2`xs))";
by (pair_induct_tac "xs" [is_exec_frag_def] 1);
(* main case *)
@@ -177,8 +177,8 @@
(* --------------------------------------------------------------------- *)
goal thy "!s. is_exec_frag (A||B) (s,xs) \
-\ --> stutter A (fst s,ProjA2`xs) &\
-\ stutter B (snd s,ProjB2`xs)";
+\ --> stutter (asig_of A) (fst s,ProjA2`xs) &\
+\ stutter (asig_of B) (snd s,ProjB2`xs)";
by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
(* main case *)
@@ -208,10 +208,10 @@
(* ----------------------------------------------------------------------- *)
goal thy
-"!s. is_exec_frag A (fst s,Filter_ex2 A`(ProjA2`xs)) &\
-\ is_exec_frag B (snd s,Filter_ex2 B`(ProjB2`xs)) &\
-\ stutter A (fst s,(ProjA2`xs)) & \
-\ stutter B (snd s,(ProjB2`xs)) & \
+"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)`(ProjA2`xs)) &\
+\ is_exec_frag B (snd s,Filter_ex2 (asig_of B)`(ProjB2`xs)) &\
+\ stutter (asig_of A) (fst s,(ProjA2`xs)) & \
+\ stutter (asig_of B) (snd s,(ProjB2`xs)) & \
\ Forall (%x.fst x:act (A||B)) xs \
\ --> is_exec_frag (A||B) (s,xs)";
@@ -239,9 +239,9 @@
goal thy
"ex:executions(A||B) =\
-\(Filter_ex A (ProjA ex) : executions A &\
-\ Filter_ex B (ProjB ex) : executions B &\
-\ stutter A (ProjA ex) & stutter B (ProjB ex) &\
+\(Filter_ex (asig_of A) (ProjA ex) : executions A &\
+\ Filter_ex (asig_of B) (ProjB ex) : executions B &\
+\ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\
\ Forall (%x.fst x:act (A||B)) (snd ex))";
by (simp_tac (!simpset addsimps [executions_def,ProjB_def,
@@ -258,5 +258,23 @@
qed"compositionality_ex";
+(* ------------------------------------------------------------------ *)
+(* COMPOSITIONALITY on EXECUTION Level *)
+(* For Modules *)
+(* ------------------------------------------------------------------ *)
+
+goalw thy [Execs_def,par_execs_def]
+
+"Execs (A||B) = par_execs (Execs A) (Execs B)";
+
+by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
+br set_ext 1;
+by (asm_full_simp_tac (!simpset addsimps [compositionality_ex,actions_of_par]) 1);
+qed"compositionality_ex_modules";
+
+
+
+
+
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Thu Jul 17 12:43:32 1997 +0200
@@ -15,10 +15,12 @@
ProjA2 ::"('a,'s * 't)pairs -> ('a,'s)pairs"
ProjB ::"('a,'s * 't)execution => ('a,'t)execution"
ProjB2 ::"('a,'s * 't)pairs -> ('a,'t)pairs"
- Filter_ex ::"('a,'s)ioa => ('a,'s)execution => ('a,'s)execution"
- Filter_ex2 ::"('a,'s)ioa => ('a,'s)pairs -> ('a,'s)pairs"
- stutter ::"('a,'s)ioa => ('a,'s)execution => bool"
- stutter2 ::"('a,'s)ioa => ('a,'s)pairs -> ('s => tr)"
+ Filter_ex ::"'a signature => ('a,'s)execution => ('a,'s)execution"
+ Filter_ex2 ::"'a signature => ('a,'s)pairs -> ('a,'s)pairs"
+ stutter ::"'a signature => ('a,'s)execution => bool"
+ stutter2 ::"'a signature => ('a,'s)pairs -> ('s => tr)"
+
+ par_execs ::"[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module"
defs
@@ -39,27 +41,36 @@
Filter_ex_def
- "Filter_ex A ex == (fst ex,Filter_ex2 A`(snd ex))"
+ "Filter_ex sig ex == (fst ex,Filter_ex2 sig`(snd ex))"
Filter_ex2_def
- "Filter_ex2 A == Filter (%x.fst x:act A)"
+ "Filter_ex2 sig == Filter (%x.fst x:actions sig)"
stutter_def
- "stutter A ex == ((stutter2 A`(snd ex)) (fst ex) ~= FF)"
+ "stutter sig ex == ((stutter2 sig`(snd ex)) (fst ex) ~= FF)"
stutter2_def
- "stutter2 A ==(fix`(LAM h ex. (%s. case ex of
+ "stutter2 sig ==(fix`(LAM h ex. (%s. case ex of
nil => TT
| x##xs => (flift1
- (%p.(If Def ((fst p)~:act A)
+ (%p.(If Def ((fst p)~:actions sig)
then Def (s=(snd p))
else TT fi)
andalso (h`xs) (snd p))
`x)
)))"
-
-
+par_execs_def
+ "par_execs ExecsA ExecsB ==
+ let exA = fst ExecsA; sigA = snd ExecsA;
+ exB = fst ExecsB; sigB = snd ExecsB
+ in
+ ( {ex. Filter_ex sigA (ProjA ex) : exA}
+ Int {ex. Filter_ex sigB (ProjB ex) : exB}
+ Int {ex. stutter sigA (ProjA ex)}
+ Int {ex. stutter sigB (ProjB ex)}
+ Int {ex. Forall (%x.fst x:(actions sigA Un actions sigB)) (snd ex)},
+ asig_comp sigA sigB)"
end
\ No newline at end of file
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Thu Jul 17 12:43:32 1997 +0200
@@ -159,7 +159,7 @@
(* --------------------------------------------------------------------- *)
goalw thy [filter_act_def,Filter_ex2_def]
- "filter_act`(Filter_ex2 A`xs)=\
+ "filter_act`(Filter_ex2 (asig_of A)`xs)=\
\ Filter (%a.a:act A)`(filter_act`xs)";
by (simp_tac (!simpset addsimps [MapFilter,o_def]) 1);
@@ -273,7 +273,7 @@
\ Forall (%x.x:act (A||B)) sch & \
\ Filter (%a.a:act A)`sch << filter_act`exA &\
\ Filter (%a.a:act B)`sch << filter_act`exB \
-\ --> stutter A (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
+\ --> stutter (asig_of A) (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
by (mkex_induct_tac "sch" "exA" "exB");
@@ -284,7 +284,7 @@
\ Forall (%x.x:act (A||B)) sch ; \
\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
-\ ==> stutter A (ProjA (mkex A B sch exA exB))";
+\ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))";
by (cut_facts_tac [stutterA_mkex] 1);
by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjA_def,mkex_def]) 1);
@@ -304,7 +304,7 @@
\ Forall (%x.x:act (A||B)) sch & \
\ Filter (%a.a:act A)`sch << filter_act`exA &\
\ Filter (%a.a:act B)`sch << filter_act`exB \
-\ --> stutter B (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
+\ --> stutter (asig_of B) (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
by (mkex_induct_tac "sch" "exA" "exB");
@@ -315,7 +315,7 @@
\ Forall (%x.x:act (A||B)) sch ; \
\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
-\ ==> stutter B (ProjB (mkex A B sch exA exB))";
+\ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))";
by (cut_facts_tac [stutterB_mkex] 1);
by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjB_def,mkex_def]) 1);
@@ -337,7 +337,7 @@
\ Forall (%x.x:act (A||B)) sch & \
\ Filter (%a.a:act A)`sch << filter_act`exA &\
\ Filter (%a.a:act B)`sch << filter_act`exB \
-\ --> Filter_ex2 A`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) = \
+\ --> Filter_ex2 (asig_of A)`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) = \
\ Zip`(Filter (%a.a:act A)`sch)`(Map snd`exA)";
by (mkex_induct_tac "sch" "exA" "exB");
@@ -376,7 +376,7 @@
\ [| Forall (%a.a:act (A||B)) sch ; \
\ Filter (%a.a:act A)`sch = filter_act`(snd exA) ;\
\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
-\ ==> Filter_ex A (ProjA (mkex A B sch exA exB)) = exA";
+\ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA";
by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
by (pair_tac "exA" 1);
by (pair_tac "exB" 1);
@@ -401,7 +401,7 @@
\ Forall (%x.x:act (A||B)) sch & \
\ Filter (%a.a:act A)`sch << filter_act`exA &\
\ Filter (%a.a:act B)`sch << filter_act`exB \
-\ --> Filter_ex2 B`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) = \
+\ --> Filter_ex2 (asig_of B)`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) = \
\ Zip`(Filter (%a.a:act B)`sch)`(Map snd`exB)";
(* notice necessary change of arguments exA and exB *)
@@ -420,7 +420,7 @@
\ [| Forall (%a.a:act (A||B)) sch ; \
\ Filter (%a.a:act A)`sch = filter_act`(snd exA) ;\
\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
-\ ==> Filter_ex B (ProjB (mkex A B sch exA exB)) = exB";
+\ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB";
by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
by (pair_tac "exA" 1);
by (pair_tac "exB" 1);
@@ -463,11 +463,11 @@
by (simp_tac (!simpset addsimps [schedules_def, has_schedule_def]) 1);
by (safe_tac set_cs);
(* ==> *)
-by (res_inst_tac [("x","Filter_ex A (ProjA ex)")] bexI 1);
+by (res_inst_tac [("x","Filter_ex (asig_of A) (ProjA ex)")] bexI 1);
by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
by (simp_tac (!simpset addsimps [Filter_ex_def,ProjA_def,
lemma_2_1a,lemma_2_1b]) 1);
-by (res_inst_tac [("x","Filter_ex B (ProjB ex)")] bexI 1);
+by (res_inst_tac [("x","Filter_ex (asig_of B) (ProjB ex)")] bexI 1);
by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
by (simp_tac (!simpset addsimps [Filter_ex_def,ProjB_def,
lemma_2_1a,lemma_2_1b]) 1);
@@ -498,6 +498,20 @@
qed"compositionality_sch";
+(* ------------------------------------------------------------------ *)
+(* COMPOSITIONALITY on SCHEDULE Level *)
+(* For Modules *)
+(* ------------------------------------------------------------------ *)
+
+goalw thy [Scheds_def,par_scheds_def]
+
+"Scheds (A||B) = par_scheds (Scheds A) (Scheds B)";
+
+by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
+br set_ext 1;
+by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,actions_of_par]) 1);
+qed"compositionality_sch_modules";
+
Delsimps compoex_simps;
Delsimps composch_simps;
\ No newline at end of file
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Jul 17 12:43:32 1997 +0200
@@ -17,6 +17,8 @@
mkex2 ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq ->
('a,'s)pairs -> ('a,'t)pairs ->
('s => 't => ('a,'s*'t)pairs)"
+ par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module"
+
defs
@@ -60,4 +62,14 @@
)
))))"
-end
\ No newline at end of file
+par_scheds_def
+ "par_scheds SchedsA SchedsB ==
+ let schA = fst SchedsA; sigA = snd SchedsA;
+ schB = fst SchedsB; sigB = snd SchedsB
+ in
+ ( {sch. Filter (%a.a:actions sigA)`sch : schA}
+ Int {sch. Filter (%a.a:actions sigB)`sch : schB}
+ Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
+ asig_comp sigA sigB)"
+
+end
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Thu Jul 17 12:43:32 1997 +0200
@@ -1170,7 +1170,7 @@
(* ------------------------------------------------------------------ *)
goal thy
-"!! A B. [| IOA A; IOA B; compatible A B; compatible B A; \
+"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
\ is_asig(asig_of A); is_asig(asig_of B)|] \
\ ==> tr: traces(A||B) = \
\ (Filter (%a.a:act A)`tr : traces A &\
@@ -1227,9 +1227,25 @@
+(* ------------------------------------------------------------------ *)
+(* COMPOSITIONALITY on TRACE Level *)
+(* For Modules *)
+(* ------------------------------------------------------------------ *)
+
+goalw thy [Traces_def,par_traces_def]
+
+"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
+\ is_asig(asig_of A); is_asig(asig_of B)|] \
+\==> Traces (A||B) = par_traces (Traces A) (Traces B)";
+
+by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
+br set_ext 1;
+by (asm_full_simp_tac (!simpset addsimps [compositionality_tr,externals_of_par]) 1);
+qed"compositionality_tr_modules";
+
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Jul 17 12:43:32 1997 +0200
@@ -11,8 +11,8 @@
consts
- mksch ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq"
-
+ mksch ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq"
+ par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"
defs
@@ -51,6 +51,16 @@
)))"
+par_traces_def
+ "par_traces TracesA TracesB ==
+ let trA = fst TracesA; sigA = snd TracesA;
+ trB = fst TracesB; sigB = snd TracesB
+ in
+ ( {tr. Filter (%a.a:actions sigA)`tr : trA}
+ Int {tr. Filter (%a.a:actions sigB)`tr : trB}
+ Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
+ asig_comp sigA sigB)"
+
rules
@@ -60,5 +70,3 @@
end
-
-
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Thu Jul 17 12:43:32 1997 +0200
@@ -17,6 +17,7 @@
"!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
\ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
by (rtac ForallPFilterQR 1);
+(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q`tr = Filter R`tr *)
by (assume_tac 2);
by (rtac compatibility_consequence3 1);
by (REPEAT (asm_full_simp_tac (!simpset
@@ -49,14 +50,15 @@
goal thy "!! A1 A2 B1 B2. \
-\ [| IOA A1; IOA A2; IOA B1; IOA B2;\
-\ is_asig (asig_of A1); is_asig (asig_of A2); \
-\ is_asig (asig_of B1); is_asig (asig_of B2); \
+\ [| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2;\
+\ is_asig_of A1; is_asig_of A2; \
+\ is_asig_of B1; is_asig_of B2; \
\ compatible A1 B1; compatible A2 B2; \
\ A1 =<| A2; \
\ B1 =<| B2 |] \
\ ==> (A1 || B1) =<| (A2 || B2)";
+by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def]) 1);
by (forw_inst_tac [("A2","A1")] (compat_commute RS iffD1) 1);
by (forw_inst_tac [("A2","A2")] (compat_commute RS iffD1) 1);
by (asm_full_simp_tac (!simpset addsimps [ioa_implements_def,
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Thu Jul 17 12:43:32 1997 +0200
@@ -10,7 +10,7 @@
input actions may always be added to a schedule
**********************************************************************************)
-goal thy "!! sch. [| Filter (%x.x:act A)`sch : schedules A; a:inp A; IOA A; Finite sch|] \
+goal thy "!! sch. [| Filter (%x.x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
\ ==> Filter (%x.x:act A)`sch @@ a>>nil : schedules A";
by (asm_full_simp_tac (!simpset addsimps [schedules_def,has_schedule_def]) 1);
by (safe_tac set_cs);
@@ -29,7 +29,7 @@
by (etac allE 1);
by (etac exE 1);
(* using input-enabledness *)
-by (asm_full_simp_tac (!simpset addsimps [ioa_def,input_enabled_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps [input_enabled_def]) 1);
by (REPEAT (etac conjE 1));
by (eres_inst_tac [("x","a")] allE 1);
by (Asm_full_simp_tac 1);
@@ -46,13 +46,13 @@
(********************************************************************************
Deadlock freedom: component B cannot block an out or int action
- of component A in every schedule
+ of component A in every schedule.
Needs compositionality on schedule level, input-enabledness, compatibility
and distributivity of is_exec_frag over @@
**********************************************************************************)
goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
-\ Filter (%x.x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; IOA B |] \
+\ Filter (%x.x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
\ ==> (sch @@ a>>nil) : schedules (A||B)";
by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,locals_def]) 1);
--- a/src/HOLCF/IOA/meta_theory/Deadlock.thy Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy Thu Jul 17 12:43:32 1997 +0200
@@ -6,4 +6,4 @@
Deadlock freedom of I/O Automata
*)
-Deadlock = RefCorrectness + CompoScheds
\ No newline at end of file
+Deadlock = RefCorrectness + CompoScheds
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Thu Jul 17 12:43:32 1997 +0200
@@ -92,19 +92,20 @@
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by (fast_tac (!claset addDs prems) 1);
-qed "imp_conj_lemma";
+ by(fast_tac (!claset addDs prems) 1);
+val lemma = result();
+
goal thy "!!f.[| is_weak_ref_map f C A |]\
\ ==> (is_weak_ref_map f (rename C g) (rename A g))";
by (asm_full_simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
by (rtac conjI 1);
(* 1: start states *)
-by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps [rename_def,rename_set_def,starts_of_def]) 1);
(* 2: reachable transitions *)
by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
-by (simp_tac (!simpset addsimps [rename_def]) 1);
+by (rtac lemma 1);
+by (simp_tac (!simpset addsimps [rename_def,rename_set_def]) 1);
by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,
asig_outputs_def,asig_of_def,trans_of_def]) 1);
by (safe_tac (!claset));
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Jul 17 12:43:32 1997 +0200
@@ -1034,6 +1034,35 @@
(*
+local
+
+fun qnt_tac i (tac, var) = tac THEN res_inst_tac [("x", var)] spec i;
+
+fun add_frees tsig =
+ let
+ fun add (Free (x, T), vars) =
+ if Type.of_sort tsig (T, HOLogic.termS) then x ins vars
+ else vars
+ | add (Abs (_, _, t), vars) = add (t, vars)
+ | add (t $ u, vars) = add (t, add (u, vars))
+ | add (_, vars) = vars;
+ in add end;
+
+
+in
+
+(*Generalizes over all free variables, with the named var outermost.*)
+fun all_frees_tac x i thm =
+ let
+ val tsig = #tsig (Sign.rep_sg (#sign (rep_thm thm)));
+ val frees = add_frees tsig (nth_elem (i - 1, prems_of thm), [x]);
+ val frees' = sort (op >) (frees \ x) @ [x];
+ in
+ foldl (qnt_tac i) (all_tac, frees') thm
+ end;
+
+end;
+
goal thy
"!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Thu Jul 17 12:43:32 1997 +0200
@@ -162,18 +162,18 @@
this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *)
goal thy
- "!! A. IOA A ==> \
+ "!! A. is_trans_of A ==> \
\ ! s. is_exec_frag A (s,xs) --> Forall (%a.a:act A) (filter_act`xs)";
by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
(* main case *)
ren "ss a t" 1;
by (safe_tac set_cs);
-by (REPEAT (asm_full_simp_tac (!simpset addsimps [ioa_def,state_trans_def]) 1));
+by (REPEAT (asm_full_simp_tac (!simpset addsimps [is_trans_of_def]) 1));
qed"execfrag_in_sig";
goal thy
- "!! A.[| IOA A; x:executions A |] ==> \
+ "!! A.[| is_trans_of A; x:executions A |] ==> \
\ Forall (%a.a:act A) (filter_act`(snd x))";
by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
@@ -183,7 +183,7 @@
qed"exec_in_sig";
goalw thy [schedules_def,has_schedule_def]
- "!! A.[| IOA A; x:schedules A |] ==> \
+ "!! A.[| is_trans_of A; x:schedules A |] ==> \
\ Forall (%a.a:act A) x";
by (fast_tac (!claset addSIs [exec_in_sig]) 1);
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Thu Jul 17 12:43:32 1997 +0200
@@ -15,6 +15,10 @@
('a,'s)pairs = "('a * 's) Seq"
('a,'s)execution = "'s * ('a,'s)pairs"
'a trace = "'a Seq"
+
+ ('a,'s)execution_module = "('a,'s)execution set * 'a signature"
+ 'a schedule_module = "'a trace set * 'a signature"
+ 'a trace_module = "'a trace set * 'a signature"
consts
@@ -31,12 +35,16 @@
has_trace :: "[('a,'s)ioa, 'a trace] => bool"
schedules,
traces :: "('a,'s)ioa => 'a trace set"
-
mk_trace :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace"
(* Notion of implementation *)
"=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr 12)
+ (* Execution, schedule and trace modules *)
+ Execs :: "('a,'s)ioa => ('a,'s)execution_module"
+ Scheds :: "('a,'s)ioa => 'a schedule_module"
+ Traces :: "('a,'s)ioa => 'a trace_module"
+
(*
(* FIX: introduce good symbol *)
syntax (symbols)
@@ -107,5 +115,16 @@
(outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) &
traces(ioa1) <= traces(ioa2))"
+(* ------------------- Modules ------------------------------ *)
+
+Execs_def
+ "Execs A == (executions A, asig_of A)"
+
+Scheds_def
+ "Scheds A == (schedules A, asig_of A)"
+
+Traces_def
+ "Traces A == (traces A,asig_of A)"
+
end
\ No newline at end of file