# HG changeset patch # User wenzelm # Date 1126026219 -7200 # Node ID aa3833fb7bee457c4d5bd083eb9762ebb2dbb84f # Parent bd49e10bbd24d8389082bbfb7724ca87db0e8938 converted to Isar theory format; diff -r bd49e10bbd24 -r aa3833fb7bee src/HOL/IOA/Asig.ML --- 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); diff -r bd49e10bbd24 -r aa3833fb7bee src/HOL/IOA/Asig.thy --- 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 diff -r bd49e10bbd24 -r aa3833fb7bee src/HOL/IOA/IOA.ML --- 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; - diff -r bd49e10bbd24 -r aa3833fb7bee src/HOL/IOA/IOA.thy --- 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 diff -r bd49e10bbd24 -r aa3833fb7bee src/HOL/IOA/Solve.ML --- 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); diff -r bd49e10bbd24 -r aa3833fb7bee src/HOL/IOA/Solve.thy --- 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