--- a/src/HOL/IOA/Asig.ML Tue Sep 06 18:49:25 2005 +0200
+++ b/src/HOL/IOA/Asig.ML Tue Sep 06 19:03:39 2005 +0200
@@ -2,13 +2,9 @@
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
-
-Action signatures
*)
-open Asig;
-
-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 "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
--- a/src/HOL/IOA/Asig.thy Tue Sep 06 18:49:25 2005 +0200
+++ b/src/HOL/IOA/Asig.thy Tue Sep 06 19:03:39 2005 +0200
@@ -2,44 +2,50 @@
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
-
-Action signatures
*)
-Asig = Main +
+header {* Action signatures *}
-types
+theory Asig
+imports Main
+begin
-'a signature = "('a set * 'a set * 'a set)"
+types
+ 'a signature = "('a set * 'a set * 'a set)"
consts
- actions,inputs,outputs,internals,externals
- ::"'action signature => 'action set"
+ "actions" :: "'action signature => 'action set"
+ "inputs" :: "'action signature => 'action set"
+ "outputs" :: "'action signature => 'action set"
+ "internals" :: "'action signature => 'action set"
+ externals :: "'action signature => 'action set"
+
is_asig ::"'action signature => bool"
mk_ext_asig ::"'action signature => 'action signature"
defs
-asig_inputs_def "inputs == fst"
-asig_outputs_def "outputs == (fst o snd)"
-asig_internals_def "internals == (snd o snd)"
+asig_inputs_def: "inputs == fst"
+asig_outputs_def: "outputs == (fst o snd)"
+asig_internals_def: "internals == (snd o snd)"
-actions_def
+actions_def:
"actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
-externals_def
+externals_def:
"externals(asig) == (inputs(asig) Un outputs(asig))"
-is_asig_def
- "is_asig(triple) ==
- ((inputs(triple) Int outputs(triple) = {}) &
- (outputs(triple) Int internals(triple) = {}) &
+is_asig_def:
+ "is_asig(triple) ==
+ ((inputs(triple) Int outputs(triple) = {}) &
+ (outputs(triple) Int internals(triple) = {}) &
(inputs(triple) Int internals(triple) = {}))"
-mk_ext_asig_def
+mk_ext_asig_def:
"mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
+ML {* use_legacy_bindings (the_context ()) *}
-end
+end
--- a/src/HOL/IOA/IOA.ML Tue Sep 06 18:49:25 2005 +0200
+++ b/src/HOL/IOA/IOA.ML Tue Sep 06 19:03:39 2005 +0200
@@ -2,15 +2,13 @@
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
-
-The I/O automata of Lynch and Tuttle.
*)
Addsimps [Let_def];
-val ioa_projections = [asig_of_def, starts_of_def, trans_of_def];
+bind_thms ("ioa_projections", [asig_of_def, starts_of_def, trans_of_def]);
-val exec_rws = [executions_def,is_execution_fragment_def];
+bind_thms ("exec_rws", [executions_def,is_execution_fragment_def]);
Goal
"asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z";
@@ -67,7 +65,7 @@
by Auto_tac;
qed "reachable_n";
-val [p1,p2] = goalw IOA.thy [invariant_def]
+val [p1,p2] = goalw (the_context ()) [invariant_def]
"[| !!s. s:starts_of(A) ==> P(s); \
\ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
\ ==> invariant A P";
@@ -85,19 +83,19 @@
by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
qed "invariantI";
-val [p1,p2] = goal IOA.thy
+val [p1,p2] = goal (the_context ())
"[| !!s. s : starts_of(A) ==> P(s); \
\ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
\ |] ==> invariant A P";
by (fast_tac (claset() addSIs [invariantI] addSDs [p1,p2]) 1);
qed "invariantI1";
-val [p1,p2] = goalw IOA.thy [invariant_def]
+val [p1,p2] = goalw (the_context ()) [invariant_def]
"[| invariant A P; reachable A s |] ==> P(s)";
by (rtac (p2 RS (p1 RS spec RS mp)) 1);
qed "invariantE";
-Goal
+Goal
"actions(asig_comp a b) = actions(a) Un actions(b)";
by (simp_tac (simpset() addsimps
([actions_def,asig_comp_def]@asig_projections)) 1);
@@ -110,13 +108,13 @@
qed "starts_of_par";
(* Every state in an execution is reachable *)
-Goalw [reachable_def]
+Goalw [reachable_def]
"ex:executions(A) ==> !n. reachable A (snd ex n)";
by (Fast_tac 1);
qed "states_of_exec_reachable";
-Goal
+Goal
"(s,a,t) : trans_of(A || B || C || D) = \
\ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) | \
\ a:actions(asig_of(D))) & \
@@ -150,9 +148,9 @@
Goal "externals(asig_of(A1||A2)) = \
\ (externals(asig_of(A1)) Un externals(asig_of(A2)))";
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
-by (rtac set_ext 1);
+by (rtac set_ext 1);
by (Fast_tac 1);
-qed"externals_of_par";
+qed"externals_of_par";
Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
"[| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
@@ -168,4 +166,3 @@
val ext1_ext2_is_not_act2 = ext1_is_not_int2 RS int_and_ext_is_act;
val ext1_ext2_is_not_act1 = ext2_is_not_int1 RS int_and_ext_is_act;
-
--- a/src/HOL/IOA/IOA.thy Tue Sep 06 18:49:25 2005 +0200
+++ b/src/HOL/IOA/IOA.thy Tue Sep 06 19:03:39 2005 +0200
@@ -2,11 +2,13 @@
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
-
-The I/O automata of Lynch and Tuttle.
*)
-IOA = Asig +
+header {* The I/O automata of Lynch and Tuttle *}
+
+theory IOA
+imports Asig
+begin
types
'a seq = "nat => 'a"
@@ -26,7 +28,7 @@
(* Executions, schedules, and traces *)
- is_execution_fragment,
+ is_execution_fragment ::"[('action,'state)ioa, ('action,'state)execution] => bool"
has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool"
executions :: "('action,'state)ioa => ('action,'state)execution set"
mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
@@ -46,7 +48,7 @@
compat_asigs ::"['action signature, 'action signature] => bool"
asig_comp ::"['action signature, 'action signature] => 'action signature"
compat_ioas ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
- "||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr 10)
+ par ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "||" 10)
(* Filtering and hiding *)
filter_oseq :: "('a => bool) => 'a oseq => 'a oseq"
@@ -62,19 +64,19 @@
defs
-state_trans_def
- "state_trans asig R ==
- (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
+state_trans_def:
+ "state_trans asig R ==
+ (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
(!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)"
+asig_of_def: "asig_of == fst"
+starts_of_def: "starts_of == (fst o snd)"
+trans_of_def: "trans_of == (snd o snd)"
-ioa_def
- "IOA(ioa) == (is_asig(asig_of(ioa)) &
- (~ starts_of(ioa) = {}) &
+ioa_def:
+ "IOA(ioa) == (is_asig(asig_of(ioa)) &
+ (~ starts_of(ioa) = {}) &
state_trans (asig_of ioa) (trans_of ioa))"
@@ -82,115 +84,117 @@
* the first is the action options, the second the state sequence.
* Finite executions have None actions from some point on.
*******)
-is_execution_fragment_def
- "is_execution_fragment A ex ==
- let act = fst(ex); state = snd(ex)
- in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
+is_execution_fragment_def:
+ "is_execution_fragment A ex ==
+ let act = fst(ex); state = snd(ex)
+ in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
(act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
-executions_def
- "executions(ioa) == {e. snd e 0:starts_of(ioa) &
+executions_def:
+ "executions(ioa) == {e. snd e 0:starts_of(ioa) &
is_execution_fragment ioa e}"
-
-reachable_def
+
+reachable_def:
"reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
-invariant_def "invariant A P == (!s. reachable A s --> P(s))"
+invariant_def: "invariant A P == (!s. reachable A s --> P(s))"
(* Restrict the trace to those members of the set s *)
-filter_oseq_def
- "filter_oseq p s ==
- (%i. case s(i)
- of None => None
+filter_oseq_def:
+ "filter_oseq p s ==
+ (%i. case s(i)
+ of None => None
| Some(x) => if p x then Some x else None)"
-mk_trace_def
+mk_trace_def:
"mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
(* Does an ioa have an execution with the given trace *)
-has_trace_def
- "has_trace ioa b ==
+has_trace_def:
+ "has_trace ioa b ==
(? ex:executions(ioa). b = mk_trace ioa (fst ex))"
-normal_form_def
- "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
- (!j. j ~: range(f) --> nf(j)= None) &
+normal_form_def:
+ "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
+ (!j. j ~: range(f) --> nf(j)= None) &
(!i. nf(i)=None --> (nf (Suc i)) = None) "
-
+
(* All the traces of an ioa *)
- traces_def
+ traces_def:
"traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
(*
- traces_def
+ traces_def:
"traces(ioa) == {tr. has_trace ioa tr}"
*)
-
-compat_asigs_def
- "compat_asigs a1 a2 ==
- (((outputs(a1) Int outputs(a2)) = {}) &
- ((internals(a1) Int actions(a2)) = {}) &
+
+compat_asigs_def:
+ "compat_asigs a1 a2 ==
+ (((outputs(a1) Int outputs(a2)) = {}) &
+ ((internals(a1) Int actions(a2)) = {}) &
((internals(a2) Int actions(a1)) = {}))"
-compat_ioas_def
+compat_ioas_def:
"compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
-asig_comp_def
- "asig_comp a1 a2 ==
- (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
- (outputs(a1) Un outputs(a2)),
+asig_comp_def:
+ "asig_comp a1 a2 ==
+ (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
+ (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)},
- {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
- in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
- (if a:actions(asig_of(ioa1)) then
- (fst(s),a,fst(t)):trans_of(ioa1)
- else fst(t) = fst(s))
- &
- (if a:actions(asig_of(ioa2)) then
- (snd(s),a,snd(t)):trans_of(ioa2)
+par_def:
+ "(ioa1 || ioa2) ==
+ (asig_comp (asig_of ioa1) (asig_of ioa2),
+ {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
+ {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
+ in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
+ (if a:actions(asig_of(ioa1)) then
+ (fst(s),a,fst(t)):trans_of(ioa1)
+ else fst(t) = fst(s))
+ &
+ (if a:actions(asig_of(ioa2)) then
+ (snd(s),a,snd(t)):trans_of(ioa2)
else snd(t) = snd(s))})"
-restrict_asig_def
- "restrict_asig asig actns ==
- (inputs(asig) Int actns, outputs(asig) Int actns,
+restrict_asig_def:
+ "restrict_asig asig actns ==
+ (inputs(asig) Int actns, outputs(asig) Int actns,
internals(asig) Un (externals(asig) - actns))"
-restrict_def
- "restrict ioa actns ==
+restrict_def:
+ "restrict ioa actns ==
(restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
-ioa_implements_def
- "ioa_implements ioa1 ioa2 ==
- ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
- (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &
+ioa_implements_def:
+ "ioa_implements ioa1 ioa2 ==
+ ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
+ (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &
traces(ioa1) <= traces(ioa2))"
-
-rename_def
-"rename ioa ren ==
- (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
- {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
- {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
- starts_of(ioa) ,
- {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
- in
+
+rename_def:
+"rename ioa ren ==
+ (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
+ {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
+ {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
+ 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)})"
-end
+ML {* use_legacy_bindings (the_context ()) *}
+
+end
--- a/src/HOL/IOA/Solve.ML Tue Sep 06 18:49:25 2005 +0200
+++ b/src/HOL/IOA/Solve.ML Tue Sep 06 19:03:39 2005 +0200
@@ -2,12 +2,8 @@
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
-
-Weak possibilities mapping (abstraction)
*)
-open Solve;
-
Addsimps [mk_trace_thm,trans_in_actions];
Goalw [is_weak_pmap_def,traces_def]
@@ -57,16 +53,16 @@
(* fist_order_tautology of externals_of_par *)
-goal IOA.thy "a:externals(asig_of(A1||A2)) = \
+goal (theory "IOA") "a:externals(asig_of(A1||A2)) = \
\ (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) | \
\ a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) | \
\ a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))";
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1);
by (Fast_tac 1);
-val externals_of_par_extra = result();
+val externals_of_par_extra = result();
Goal "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
-by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
by (etac bexE 1);
by (res_inst_tac [("x",
"(filter_oseq (%a. a:actions(asig_of(C1))) \
@@ -77,16 +73,16 @@
(* projected execution is indeed an execution *)
by (asm_full_simp_tac
(simpset() delcongs [if_weak_cong]
- addsimps [executions_def,is_execution_fragment_def,
- par_def,starts_of_def,trans_of_def,filter_oseq_def]
+ addsimps [executions_def,is_execution_fragment_def,
+ par_def,starts_of_def,trans_of_def,filter_oseq_def]
addsplits [option.split]) 1);
qed"comp1_reachable";
-(* Exact copy of proof of comp1_reachable for the second
+(* Exact copy of proof of comp1_reachable for the second
component of a parallel composition. *)
Goal "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
-by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
by (etac bexE 1);
by (res_inst_tac [("x",
"(filter_oseq (%a. a:actions(asig_of(C2)))\
@@ -97,8 +93,8 @@
(* projected execution is indeed an execution *)
by (asm_full_simp_tac
(simpset() delcongs [if_weak_cong]
- addsimps [executions_def,is_execution_fragment_def,
- par_def,starts_of_def,trans_of_def,filter_oseq_def]
+ addsimps [executions_def,is_execution_fragment_def,
+ par_def,starts_of_def,trans_of_def,filter_oseq_def]
addsplits [option.split]) 1);
qed"comp2_reachable";
@@ -124,7 +120,7 @@
by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
by (stac split_if 1);
by (rtac conjI 1);
-by (rtac impI 1);
+by (rtac impI 1);
by (etac disjE 1);
(* case 1 a:e(A1) | a:e(A2) *)
by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
@@ -145,13 +141,13 @@
by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
addsplits [split_if]) 1);
by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
- asm_full_simp_tac(simpset() addsimps[comp1_reachable,
- comp2_reachable])1));
+ asm_full_simp_tac(simpset() addsimps[comp1_reachable,
+ comp2_reachable])1));
qed"fxg_is_weak_pmap_of_product_IOA";
Goal "[| reachable (rename C g) s |] ==> reachable C s";
-by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
by (etac bexE 1);
by (res_inst_tac [("x",
"((%i. case (fst ex i) \
@@ -202,8 +198,8 @@
by (assume_tac 1);
by (Asm_full_simp_tac 1);
(* x is internal *)
-by (simp_tac (simpset() addsimps [de_Morgan_disj, de_Morgan_conj, not_ex]
- addcongs [conj_cong]) 1);
+by (simp_tac (simpset() addsimps [de_Morgan_disj, de_Morgan_conj, not_ex]
+ addcongs [conj_cong]) 1);
by (rtac impI 1);
by (etac conjE 1);
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
--- a/src/HOL/IOA/Solve.thy Tue Sep 06 18:49:25 2005 +0200
+++ b/src/HOL/IOA/Solve.thy Tue Sep 06 19:03:39 2005 +0200
@@ -2,21 +2,25 @@
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
-
-Weak possibilities mapping (abstraction)
*)
-Solve = IOA +
+header {* Weak possibilities mapping (abstraction) *}
+
+theory Solve
+imports IOA
+begin
constdefs
is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
- "is_weak_pmap f C A ==
- (!s:starts_of(C). f(s):starts_of(A)) &
- (!s t a. reachable C s &
- (s,a,t):trans_of(C)
- --> (if a:externals(asig_of(C)) then
- (f(s),a,f(t)):trans_of(A)
+ "is_weak_pmap f C A ==
+ (!s:starts_of(C). f(s):starts_of(A)) &
+ (!s t a. reachable C s &
+ (s,a,t):trans_of(C)
+ --> (if a:externals(asig_of(C)) then
+ (f(s),a,f(t)):trans_of(A)
else f(s)=f(t)))"
+ML {* use_legacy_bindings (the_context ()) *}
+
end