# HG changeset patch # User mueller # Date 862394177 -7200 # Node ID 984866a8f905797dd57e922e19b4f3d5590d1013 # Parent 750b766645b8ede5864be6c16d3f4682cc340532 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); diff -r 750b766645b8 -r 984866a8f905 src/HOL/IOA/Asig.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/Asig.ML Wed Apr 30 11:56:17 1997 +0200 @@ -0,0 +1,19 @@ +(* Title: HOL/IOA/meta_theory/Asig.ML + 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]; + +goal Asig.thy "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"; +by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1); +qed"int_and_ext_is_act"; + +goal Asig.thy "!!a.[|a:externals(S)|] ==> a:actions(S)"; +by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1); +qed"ext_is_act"; diff -r 750b766645b8 -r 984866a8f905 src/HOL/IOA/Asig.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/Asig.thy Wed Apr 30 11:56:17 1997 +0200 @@ -0,0 +1,45 @@ +(* Title: HOL/IOA/meta_theory/Asig.thy + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +Action signatures +*) + +Asig = Prod + + +types + +'a signature = "('a set * 'a set * 'a set)" + +consts + actions,inputs,outputs,internals,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)" + +actions_def + "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" + +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) = {}) & + (inputs(triple) Int internals(triple) = {}))" + + +mk_ext_asig_def + "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})" + + +end diff -r 750b766645b8 -r 984866a8f905 src/HOL/IOA/IOA.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/IOA.ML Wed Apr 30 11:56:17 1997 +0200 @@ -0,0 +1,176 @@ +(* Title: HOL/IOA/meta_theory/IOA.ML + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +The I/O automata of Lynch and Tuttle. +*) + +Addsimps [Let_def]; + +open IOA Asig; + +val ioa_projections = [asig_of_def, starts_of_def, trans_of_def]; + +val exec_rws = [executions_def,is_execution_fragment_def]; + +goal IOA.thy +"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z"; + by (simp_tac (!simpset addsimps ioa_projections) 1); + qed "ioa_triple_proj"; + +goalw IOA.thy [ioa_def,state_trans_def,actions_def, is_asig_def] + "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))"; + by (REPEAT(etac conjE 1)); + by (EVERY1[etac allE, etac impE, atac]); + by (Asm_full_simp_tac 1); +qed "trans_in_actions"; + + +goal IOA.thy "filter_oseq p (filter_oseq p s) = filter_oseq p s"; + by (simp_tac (!simpset addsimps [filter_oseq_def]) 1); + by (rtac ext 1); + by (Option.option.induct_tac "s(i)" 1); + by (Simp_tac 1); + by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); +qed "filter_oseq_idemp"; + +goalw IOA.thy [mk_trace_def,filter_oseq_def] +"(mk_trace A s n = None) = \ +\ (s(n)=None | (? a. s(n)=Some(a) & a ~: externals(asig_of(A)))) \ +\ & \ +\ (mk_trace A s n = Some(a)) = \ +\ (s(n)=Some(a) & a : externals(asig_of(A)))"; + by (Option.option.induct_tac "s(n)" 1); + by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if])))); + by (Fast_tac 1); +qed "mk_trace_thm"; + +goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable A s"; + by (res_inst_tac [("x","(%i.None,%i.s)")] bexI 1); + by (Simp_tac 1); + by (asm_simp_tac (!simpset addsimps exec_rws) 1); +qed "reachable_0"; + +goalw IOA.thy (reachable_def::exec_rws) +"!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"; + by (asm_full_simp_tac (!simpset delsimps bex_simps) 1); + by (safe_tac (!claset)); + by (res_inst_tac [("x","(%i.if i P(s); \ +\ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \ +\ ==> invariant A P"; + by (rewrite_goals_tac(reachable_def::Let_def::exec_rws)); + by (safe_tac (!claset)); + by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1); + by (nat_ind_tac "n" 1); + by (fast_tac (!claset addIs [p1,reachable_0]) 1); + by (eres_inst_tac[("x","n")]allE 1); + by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n")] optionE 1); + by (Asm_simp_tac 1); + by (safe_tac (!claset)); + by (etac (p2 RS mp) 1); + by (ALLGOALS(fast_tac(!claset addDs [hd Option.option.inject RS iffD1, + reachable_n]))); +qed "invariantI"; + +val [p1,p2] = goal IOA.thy + "[| !!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] +"[| invariant A P; reachable A s |] ==> P(s)"; + by (rtac (p2 RS (p1 RS spec RS mp)) 1); +qed "invariantE"; + +goal IOA.thy +"actions(asig_comp a b) = actions(a) Un actions(b)"; + by (simp_tac (!simpset addsimps + ([actions_def,asig_comp_def]@asig_projections)) 1); + by (Fast_tac 1); +qed "actions_asig_comp"; + +goal IOA.thy +"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"; + by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1); +qed "starts_of_par"; + +(* Every state in an execution is reachable *) +goalw IOA.thy [reachable_def] +"!!A. ex:executions(A) ==> !n. reachable A (snd ex n)"; + by (Fast_tac 1); +qed "states_of_exec_reachable"; + + +goal IOA.thy +"(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))) & \ +\ (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A) \ +\ else fst t=fst s) & \ +\ (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B) \ +\ else fst(snd(t))=fst(snd(s))) & \ +\ (if a:actions(asig_of(C)) then \ +\ (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) \ +\ else fst(snd(snd(t)))=fst(snd(snd(s)))) & \ +\ (if a:actions(asig_of(D)) then \ +\ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \ +\ else snd(snd(snd(t)))=snd(snd(snd(s)))))"; + by (simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@ + ioa_projections) + setloop (split_tac [expand_if])) 1); +qed "trans_of_par4"; + +goal IOA.thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ +\ trans_of(restrict ioa acts) = trans_of(ioa) & \ +\ reachable (restrict ioa acts) s = reachable ioa s"; +by (simp_tac (!simpset addsimps ([is_execution_fragment_def,executions_def, + reachable_def,restrict_def]@ioa_projections)) 1); +qed "cancel_restrict"; + +goal IOA.thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"; + by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1); +qed "asig_of_par"; + + +goal IOA.thy "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 (Fast_tac 1); +qed"externals_of_par"; + +goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] + "!! a. [| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"; +by (Asm_full_simp_tac 1); +by (best_tac (!claset addEs [equalityCE]) 1); +qed"ext1_is_not_int2"; + +goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] + "!! a. [| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"; +by (Asm_full_simp_tac 1); +by (best_tac (!claset addEs [equalityCE]) 1); +qed"ext2_is_not_int1"; + +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 750b766645b8 -r 984866a8f905 src/HOL/IOA/IOA.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/IOA.thy Wed Apr 30 11:56:17 1997 +0200 @@ -0,0 +1,196 @@ +(* Title: HOL/IOA/meta_theory/IOA.thy + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +The I/O automata of Lynch and Tuttle. +*) + +IOA = Asig + Option + + +types + 'a seq = "nat => 'a" + 'a oseq = "nat => 'a option" + ('a,'b)execution = "'a oseq * 'b seq" + ('a,'s)transition = "('s * 'a * 's)" + ('a,'s)ioa = "'a signature * 's set * ('a,'s)transition set" + +consts + + (* IO automata *) + state_trans::"['action signature, ('action,'state)transition set] => bool" + asig_of ::"('action,'state)ioa => 'action signature" + starts_of ::"('action,'state)ioa => 'state set" + trans_of ::"('action,'state)ioa => ('action,'state)transition set" + IOA ::"('action,'state)ioa => bool" + + (* Executions, schedules, and traces *) + + is_execution_fragment, + 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" + reachable :: "[('action,'state)ioa, 'state] => bool" + invariant :: "[('action,'state)ioa, 'state=>bool] => bool" + has_trace :: "[('action,'state)ioa, 'action oseq] => bool" + traces :: "('action,'state)ioa => 'action oseq set" + NF :: "'a oseq => 'a oseq" + + (* Composition of action signatures and automata *) + compatible_asigs ::"('a => 'action signature) => bool" + asig_composition ::"('a => 'action signature) => 'action signature" + compatible_ioas ::"('a => ('action,'state)ioa) => bool" + ioa_composition ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa" + + (* binary composition of action signatures and automata *) + 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) + + (* Filtering and hiding *) + filter_oseq :: "('a => bool) => 'a oseq => 'a oseq" + + restrict_asig :: "['a signature, 'a set] => 'a signature" + restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" + + (* Notions of correctness *) + ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool" + + (* Instantiation of abstract IOA by concrete actions *) + rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" + +defs + +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)" + +ioa_def + "IOA(ioa) == (is_asig(asig_of(ioa)) & + (~ starts_of(ioa) = {}) & + state_trans (asig_of ioa) (trans_of ioa))" + + +(* An execution fragment is modelled with a pair of sequences: + * 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)) & + (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))" + + +executions_def + "executions(ioa) == {e. snd e 0:starts_of(ioa) & + is_execution_fragment ioa e}" + + +reachable_def + "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = 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 + | Some(x) => if p x then Some x else None)" + + +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 == + (? 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) & + (!i. nf(i)=None --> (nf (Suc i)) = None) " + +(* All the traces of an ioa *) + + traces_def + "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}" + +(* + 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)) = {}) & + ((internals(a2) Int actions(a1)) = {}))" + + +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)), + (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) + else snd(t) = snd(s))})" + + +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_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))) & + 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 + ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})" + +end diff -r 750b766645b8 -r 984866a8f905 src/HOL/IOA/README.html diff -r 750b766645b8 -r 984866a8f905 src/HOL/IOA/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ROOT.ML Wed Apr 30 11:56:17 1997 +0200 @@ -0,0 +1,31 @@ +(* Title: HOL/IOA/ROOT.ML + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +This is the ROOT file for the meta theory of I/O-Automata. + + +@inproceedings{Nipkow-Slind-IOA, +author={Tobias Nipkow and Konrad Slind}, +title={{I/O} Automata in {Isabelle/HOL}}, +booktitle={Proc.\ TYPES Workshop 1994}, +publisher=Springer, +series=LNCS, +note={To appear}} +ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz + +and + +@inproceedings{Mueller-Nipkow, +author={Olaf M\"uller and Tobias Nipkow}, +title={Combining Model Checking and Deduction for {I/O}-Automata}, +booktitle={Proc.\ TACAS Workshop}, +organization={Aarhus University, BRICS report}, +year=1995} +ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz + +Should be executed in the subdirectory HOL/IOA/NTP. +*) + +use_thy "Solve"; diff -r 750b766645b8 -r 984866a8f905 src/HOL/IOA/Solve.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/Solve.ML Wed Apr 30 11:56:17 1997 +0200 @@ -0,0 +1,209 @@ +(* Title: HOL/IOA/meta_theory/Solve.ML + 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 Solve.thy [is_weak_pmap_def,traces_def] + "!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \ +\ is_weak_pmap f C A |] ==> traces(C) <= traces(A)"; + + by (simp_tac(!simpset addsimps [has_trace_def])1); + by (safe_tac (!claset)); + + (* choose same trace, therefore same NF *) + by (res_inst_tac[("x","mk_trace C (fst ex)")] exI 1); + by (Asm_full_simp_tac 1); + + (* give execution of abstract automata *) + by (res_inst_tac[("x","(mk_trace A (fst ex),%i.f(snd ex i))")] bexI 1); + + (* Traces coincide *) + by (asm_simp_tac (!simpset addsimps [mk_trace_def,filter_oseq_idemp])1); + + (* Use lemma *) + by (forward_tac [states_of_exec_reachable] 1); + + (* Now show that it's an execution *) + by (asm_full_simp_tac(!simpset addsimps [executions_def]) 1); + by (safe_tac (!claset)); + + (* Start states map to start states *) + by (dtac bspec 1); + by (atac 1); + + (* Show that it's an execution fragment *) + by (asm_full_simp_tac (!simpset addsimps [is_execution_fragment_def])1); + by (safe_tac (!claset)); + + by (eres_inst_tac [("x","snd ex n")] allE 1); + by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1); + by (eres_inst_tac [("x","a")] allE 1); + by (Asm_full_simp_tac 1); +qed "trace_inclusion"; + +(* Lemmata *) + +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; + by(fast_tac (!claset addDs prems) 1); +val imp_conj_lemma = result(); + + +(* fist_order_tautology of externals_of_par *) +goal IOA.thy "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(); + +goal Solve.thy "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)"; +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))) \ +\ (fst ex), \ +\ %i.fst (snd ex i))")] bexI 1); +(* fst(s) is in projected execution *) + by (Simp_tac 1); + by (Fast_tac 1); +(* projected execution is indeed an execution *) +by (asm_full_simp_tac + (!simpset addsimps [executions_def,is_execution_fragment_def, + par_def,starts_of_def,trans_of_def,filter_oseq_def] + setloop (split_tac[expand_if,expand_option_case])) 1); +qed"comp1_reachable"; + + +(* Exact copy of proof of comp1_reachable for the second + component of a parallel composition. *) +goal Solve.thy "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)"; +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)))\ +\ (fst ex), \ +\ %i.snd (snd ex i))")] bexI 1); +(* fst(s) is in projected execution *) + by (Simp_tac 1); + by (Fast_tac 1); +(* projected execution is indeed an execution *) +by (asm_full_simp_tac + (!simpset addsimps [executions_def,is_execution_fragment_def, + par_def,starts_of_def,trans_of_def,filter_oseq_def] + setloop (split_tac[expand_if,expand_option_case])) 1); +qed"comp2_reachable"; + + +(* Composition of possibility-mappings *) + +goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \ +\ externals(asig_of(A1))=externals(asig_of(C1)) &\ +\ is_weak_pmap g C2 A2 & \ +\ externals(asig_of(A2))=externals(asig_of(C2)) & \ +\ compat_ioas C1 C2 & compat_ioas A1 A2 |] \ +\ ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)"; + by (rtac conjI 1); +(* start_states *) + by (asm_full_simp_tac (!simpset addsimps [par_def, starts_of_def]) 1); +(* transitions *) +by (REPEAT (rtac allI 1)); +by (rtac imp_conj_lemma 1); +by (REPEAT(etac conjE 1)); +by (simp_tac (!simpset addsimps [externals_of_par_extra]) 1); +by (simp_tac (!simpset addsimps [par_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [trans_of_def]) 1); +by (rtac (expand_if RS ssubst) 1); +by (rtac conjI 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, + ext_is_act]) 1); +by (etac disjE 1); +(* case 2 a:e(A1) | a~:e(A2) *) +by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable, + ext_is_act,ext1_ext2_is_not_act2]) 1); +(* case 3 a:~e(A1) | a:e(A2) *) +by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable, + ext_is_act,ext1_ext2_is_not_act1]) 1); +(* case 4 a:~e(A1) | a~:e(A2) *) +by (rtac impI 1); +by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1); +(* delete auxiliary subgoal *) +by (Asm_full_simp_tac 2); +by (Fast_tac 2); +by (simp_tac (!simpset addsimps [conj_disj_distribR] addcongs [conj_cong] + setloop (split_tac [expand_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)); +qed"fxg_is_weak_pmap_of_product_IOA"; + + +goal Solve.thy "!!s.[| reachable (rename C g) s |] ==> reachable C s"; +by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); +by (etac bexE 1); +by (res_inst_tac [("x", + "((%i. case (fst ex i) \ +\ of None => None\ +\ | Some(x) => g x) ,snd ex)")] bexI 1); +by (Simp_tac 1); +(* execution is indeed an execution of C *) +by (asm_full_simp_tac + (!simpset addsimps [executions_def,is_execution_fragment_def, + par_def,starts_of_def,trans_of_def,rename_def] + setloop (split_tac[expand_option_case])) 1); +by (best_tac (!claset addSDs [spec] addDs [sym] addss (!simpset)) 1); +qed"reachable_rename_ioa"; + + +goal Solve.thy "!!f.[| is_weak_pmap f C A |]\ +\ ==> (is_weak_pmap f (rename C g) (rename A g))"; +by (asm_full_simp_tac (!simpset addsimps [is_weak_pmap_def]) 1); +by (rtac conjI 1); +by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1); +by (REPEAT (rtac allI 1)); +by (rtac imp_conj_lemma 1); +by (simp_tac (!simpset addsimps [rename_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)); +by (rtac (expand_if RS ssubst) 1); + by (rtac conjI 1); + by (rtac impI 1); + by (etac disjE 1); + by (etac exE 1); +by (etac conjE 1); +(* x is input *) + by (dtac sym 1); + by (dtac sym 1); +by (Asm_full_simp_tac 1); +by (REPEAT (hyp_subst_tac 1)); +by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); +by (assume_tac 1); +by (Asm_full_simp_tac 1); +(* x is output *) + by (etac exE 1); +by (etac conjE 1); + by (dtac sym 1); + by (dtac sym 1); +by (Asm_full_simp_tac 1); +by (REPEAT (hyp_subst_tac 1)); +by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); +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 (rtac impI 1); +by (etac conjE 1); +by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); +by (Auto_tac()); +qed"rename_through_pmap"; diff -r 750b766645b8 -r 984866a8f905 src/HOL/IOA/Solve.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/Solve.thy Wed Apr 30 11:56:17 1997 +0200 @@ -0,0 +1,22 @@ +(* Title: HOL/IOA/meta_theory/Solve.thy + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +Weak possibilities mapping (abstraction) +*) + +Solve = IOA + + +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) + else f(s)=f(t)))" + +end