# HG changeset patch # User mueller # Date 862394122 -7200 # Node ID 750b766645b8ede5864be6c16d3f4682cc340532 # Parent 3e8d80cdd3e7da60dafdffb3658f80e6708d19f0 moved to .. (see also new version in HOLCF/IOA/meta_theory); diff -r 3e8d80cdd3e7 -r 750b766645b8 src/HOL/IOA/meta_theory/Asig.ML --- a/src/HOL/IOA/meta_theory/Asig.ML Wed Apr 30 11:53:30 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -(* 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 3e8d80cdd3e7 -r 750b766645b8 src/HOL/IOA/meta_theory/Asig.thy --- a/src/HOL/IOA/meta_theory/Asig.thy Wed Apr 30 11:53:30 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,45 +0,0 @@ -(* 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 3e8d80cdd3e7 -r 750b766645b8 src/HOL/IOA/meta_theory/IOA.ML --- a/src/HOL/IOA/meta_theory/IOA.ML Wed Apr 30 11:53:30 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,176 +0,0 @@ -(* 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 3e8d80cdd3e7 -r 750b766645b8 src/HOL/IOA/meta_theory/IOA.thy --- a/src/HOL/IOA/meta_theory/IOA.thy Wed Apr 30 11:53:30 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,196 +0,0 @@ -(* 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 3e8d80cdd3e7 -r 750b766645b8 src/HOL/IOA/meta_theory/Solve.ML --- a/src/HOL/IOA/meta_theory/Solve.ML Wed Apr 30 11:53:30 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,209 +0,0 @@ -(* 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 3e8d80cdd3e7 -r 750b766645b8 src/HOL/IOA/meta_theory/Solve.thy --- a/src/HOL/IOA/meta_theory/Solve.thy Wed Apr 30 11:53:30 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -(* 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