# HG changeset patch # User clasohm # Date 795710223 -3600 # Node ID 3fd66f245ad754b79fddf59a25a85d9190e37d3c # Parent 24eef3860714dd91e3e969fe2d2dbb64bc171e8f converted IOA with curried function application diff -r 24eef3860714 -r 3fd66f245ad7 src/HOL/IOA/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ROOT.ML Mon Mar 20 15:37:03 1995 +0100 @@ -0,0 +1,22 @@ +(* Title: HOL/IOA/ROOT.ML + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +This is the ROOT file for the theory of I/O-Automata. +The formalization is by a semantic model of I/O-Automata. +For details see + +@unpublished{Nipkow-Slind-IOA, +author={Tobias Nipkow and Konrad Slind}, +title={{I/O} Automata in {Isabelle/HOL}}, +year=1994, +note={Submitted for publication}} +ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz + +Should be executed in the subdirectory HOL. +*) +goals_limit := 1; + +loadpath := "IOA/meta_theory" :: "IOA/example" :: !loadpath; +use_thy "Correctness" handle _ => exit 1; diff -r 24eef3860714 -r 3fd66f245ad7 src/HOL/IOA/meta_theory/Asig.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/meta_theory/Asig.ML Mon Mar 20 15:37:03 1995 +0100 @@ -0,0 +1,11 @@ +(* 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]; diff -r 24eef3860714 -r 3fd66f245ad7 src/HOL/IOA/meta_theory/Asig.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/meta_theory/Asig.thy Mon Mar 20 15:37:03 1995 +0100 @@ -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 = Option + + +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) == " + + +end diff -r 24eef3860714 -r 3fd66f245ad7 src/HOL/IOA/meta_theory/IOA.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/meta_theory/IOA.ML Mon Mar 20 15:37:03 1995 +0100 @@ -0,0 +1,151 @@ +(* 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. +*) + +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 & starts_of() = y & trans_of() = z"; + by (simp_tac (SS addsimps ioa_projections) 1); + qed "ioa_triple_proj"; + +goalw IOA.thy [ioa_def,state_trans_def,actions_def, is_asig_def] + "!!A. [| IOA(A); :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 SS 1); +qed "trans_in_actions"; + + +goal IOA.thy "filter_oseq p (filter_oseq p s) = filter_oseq p s"; + by (simp_tac (SS addsimps [filter_oseq_def]) 1); + by (rtac ext 1); + by (Option.option.induct_tac "s(i)" 1); + by (simp_tac SS 1); + by (simp_tac (SS setloop (split_tac [expand_if])) 1); +qed "filter_oseq_idemp"; + +goalw IOA.thy [mk_behaviour_def,filter_oseq_def] +"(mk_behaviour A s n = None) = \ +\ (s(n)=None | (? a. s(n)=Some(a) & a ~: externals(asig_of(A)))) \ +\ & \ +\ (mk_behaviour 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 (SS setloop (split_tac [expand_if])))); + by (fast_tac HOL_cs 1); +qed "mk_behaviour_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 SS 1); + by (asm_simp_tac (SS addsimps exec_rws) 1); +qed "reachable_0"; + +goalw IOA.thy (reachable_def::exec_rws) +"!!A. [| reachable A s; : trans_of(A) |] ==> reachable A t"; + by(asm_full_simp_tac SS 1); + by(safe_tac set_cs); + by(res_inst_tac [("x","<%i.if i")] bexI 1); + by(res_inst_tac [("x","Suc(n)")] exI 1); + by(simp_tac SS 1); + by(asm_simp_tac (SS delsimps [less_Suc_eq]) 1); + by(REPEAT(rtac allI 1)); + by(res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1); + be disjE 1; + by(asm_simp_tac SS 1); + be disjE 1; + by(asm_simp_tac SS 1); + by(fast_tac HOL_cs 1); + by(forward_tac [less_not_sym] 1); + by(asm_simp_tac (SS addsimps [less_not_refl2]) 1); +qed "reachable_n"; + +val [p1,p2] = goalw IOA.thy [invariant_def] + "[| !!s. s:starts_of(A) ==> P(s); \ +\ !!s t a. [|reachable A s; P(s)|] ==> : trans_of(A) --> P(t) |] \ +\ ==> invariant A P"; + by (rewrite_goals_tac(reachable_def::Let_def::exec_rws)); + by (safe_tac set_cs); + by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1); + by (nat_ind_tac "n" 1); + by (fast_tac (set_cs addIs [p1,reachable_0]) 1); + by (eres_inst_tac[("x","n1")]allE 1); + by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optE 1); + by (asm_simp_tac HOL_ss 1); + by (safe_tac HOL_cs); + by (etac (p2 RS mp) 1); + by (ALLGOALS(fast_tac(set_cs 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) --> :trans_of(A) --> P(t) \ +\ |] ==> invariant A P"; + by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1); +qed "invariantI1"; + +val [p1,p2] = goalw IOA.thy [invariant_def] +"[| invariant A P; reachable A s |] ==> P(s)"; + br(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 (prod_ss addsimps + ([actions_def,asig_comp_def]@asig_projections)) 1); + by(fast_tac eq_cs 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 (SS 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 set_cs 1); +qed "states_of_exec_reachable"; + + +goal IOA.thy +" : 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 :trans_of(A) \ +\ else fst t=fst s) & \ +\ (if a:actions(asig_of(B)) then :trans_of(B) \ +\ else fst(snd(t))=fst(snd(s))) & \ +\ (if a:actions(asig_of(C)) then \ +\ :trans_of(C) \ +\ else fst(snd(snd(t)))=fst(snd(snd(s)))) & \ +\ (if a:actions(asig_of(D)) then \ +\ :trans_of(D) \ +\ else snd(snd(snd(t)))=snd(snd(snd(s)))))"; + by(simp_tac (SS 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 (SS 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 (SS addsimps (par_def::ioa_projections)) 1); +qed "asig_of_par"; diff -r 24eef3860714 -r 3fd66f245ad7 src/HOL/IOA/meta_theory/IOA.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/meta_theory/IOA.thy Mon Mar 20 15:37:03 1995 +0100 @@ -0,0 +1,186 @@ +(* 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 + + +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 behaviours *) + + is_execution_fragment, + has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool" + executions :: "('action,'state)ioa => ('action,'state)execution set" + mk_behaviour :: "[('action,'state)ioa, 'action oseq] => 'action oseq" + reachable :: "[('action,'state)ioa, 'state] => bool" + invariant :: "[('action,'state)ioa, 'state=>bool] => bool" + has_behaviour :: "[('action,'state)ioa, 'action oseq] => bool" + behaviours :: "('action,'state)ioa => 'action oseq set" + + (* 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,'state)ioa, ('action,'state)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" + + +defs + +state_trans_def + "state_trans asig R == \ + \ (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \ + \ (!a. (a:inputs(asig)) --> (!s1. ? 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) --> :trans_of(A))" + + +executions_def + "executions(ioa) == {e. snd e 0:starts_of(ioa) & \ +\ is_execution_fragment ioa e}" + + +(* Is a state reachable. Using an inductive definition, this could be defined + * by the following 2 rules + * + * x:starts_of(ioa) + * ---------------- + * reachable(ioa,x) + * + * reachable(ioa,s) & ? :trans_of(ioa) + * ------------------------------------------- + * reachable(ioa,s') + * + * A direkt definition follows. + *******************************) +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_behaviour_def + "mk_behaviour(ioa) == filter_oseq(%a.a:externals(asig_of(ioa)))" + + +(* Does an ioa have an execution with the given behaviour *) +has_behaviour_def + "has_behaviour ioa b == \ +\ (? ex:executions(ioa). b = mk_behaviour ioa (fst ex))" + + +(* All the behaviours of an ioa *) +behaviours_def + "behaviours(ioa) == {b. has_behaviour ioa b}" + + +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) == \ + \ :trans_of(ioa1) \ + \ else fst(t) = fst(s)) \ + \ & \ + \ (if a:actions(asig_of(ioa2)) then \ + \ :trans_of(ioa2) \ + \ else snd(t) = snd(s))}>" + + +restrict_asig_def + "restrict_asig asig actns == \ +\ " + + +restrict_def + "restrict ioa actns == \ +\ " + + +ioa_implements_def + "ioa_implements ioa1 ioa2 == \ +\ (externals(asig_of(ioa1)) = externals(asig_of(ioa2)) & \ +\ behaviours(ioa1) <= behaviours(ioa2))" + +end diff -r 24eef3860714 -r 3fd66f245ad7 src/HOL/IOA/meta_theory/Option.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/meta_theory/Option.ML Mon Mar 20 15:37:03 1995 +0100 @@ -0,0 +1,16 @@ +(* Title: Option.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Derived rules +*) + +val option_rws = Let_def :: Option.option.simps; +val SS = arith_ss addsimps option_rws; + +val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))"; + br (prem RS rev_mp) 1; + by (Option.option.induct_tac "opt" 1); + by (ALLGOALS(fast_tac HOL_cs)); +val optE = store_thm("optE", standard(result() RS disjE)); diff -r 24eef3860714 -r 3fd66f245ad7 src/HOL/IOA/meta_theory/Option.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/meta_theory/Option.thy Mon Mar 20 15:37:03 1995 +0100 @@ -0,0 +1,11 @@ +(* Title: Option.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Datatype 'a option +*) + +Option = Arith + +datatype 'a option = None | Some('a) +end diff -r 24eef3860714 -r 3fd66f245ad7 src/HOL/IOA/meta_theory/Solve.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/meta_theory/Solve.ML Mon Mar 20 15:37:03 1995 +0100 @@ -0,0 +1,45 @@ +(* Title: HOL/IOA/meta_theory/Solve.ML + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +Weak possibilities mapping (abstraction) +*) + +open Solve; + +val SS = SS addsimps [mk_behaviour_thm,trans_in_actions]; + +goalw Solve.thy [is_weak_pmap_def,behaviours_def] + "!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \ +\ is_weak_pmap f C A |] ==> behaviours(C) <= behaviours(A)"; + + by (simp_tac(SS addsimps [has_behaviour_def])1); + by (safe_tac set_cs); + + (* give execution of abstract automata *) + by (res_inst_tac[("x","")] bexI 1); + + (* Behaviours coincide *) + by (asm_simp_tac (SS addsimps [mk_behaviour_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(SS addsimps [executions_def]) 1); + by (safe_tac set_cs); + + (* 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 (SS addsimps [is_execution_fragment_def])1); + by (safe_tac HOL_cs); + + 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 SS 1); +qed "trace_inclusion"; diff -r 24eef3860714 -r 3fd66f245ad7 src/HOL/IOA/meta_theory/Solve.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/meta_theory/Solve.thy Mon Mar 20 15:37:03 1995 +0100 @@ -0,0 +1,26 @@ +(* Title: HOL/IOA/meta_theory/Solve.thy + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +Weak possibilities mapping (abstraction) +*) + +Solve = IOA + + +consts + + is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool" + +defs + +is_weak_pmap_def + "is_weak_pmap f C A == \ +\ (!s:starts_of(C). f(s):starts_of(A)) & \ +\ (!s t a. reachable C s & \ +\ :trans_of(C) \ +\ --> (if a:externals(asig_of(C)) then \ +\ :trans_of(A) \ +\ else f(s)=f(t)))" + +end