1.1 --- a/src/HOLCF/IOA/meta_theory/IOA.thy Tue Jan 13 10:40:38 1998 +0100
1.2 +++ b/src/HOLCF/IOA/meta_theory/IOA.thy Tue Jan 13 14:26:21 1998 +0100
1.3 @@ -8,6 +8,6 @@
1.4
1.5
1.6
1.7 -IOA = RefCorrectness + Compositionality + Deadlock
1.8 +IOA = SimCorrectness + RefCorrectness + Compositionality + Deadlock
1.9
1.10
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Tue Jan 13 14:26:21 1998 +0100
2.3 @@ -0,0 +1,297 @@
2.4 +(* Title: HOLCF/IOA/meta_theory/SimCorrectness.ML
2.5 + ID: $Id$
2.6 + Author: Olaf Mueller
2.7 + Copyright 1996 TU Muenchen
2.8 +
2.9 +Correctness of Simulations in HOLCF/IOA
2.10 +*)
2.11 +
2.12 +
2.13 +
2.14 +(* -------------------------------------------------------------------------------- *)
2.15 +
2.16 +section "corresp_ex_sim";
2.17 +
2.18 +
2.19 +(* ---------------------------------------------------------------- *)
2.20 +(* corresp_ex_simC *)
2.21 +(* ---------------------------------------------------------------- *)
2.22 +
2.23 +
2.24 +goal thy "corresp_ex_simC A R = (LAM ex. (%s. case ex of \
2.25 +\ nil => nil \
2.26 +\ | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr); \
2.27 +\ T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \
2.28 +\ in \
2.29 +\ (@cex. move A cex s a T') \
2.30 +\ @@ ((corresp_ex_simC A R `xs) T')) \
2.31 +\ `x) ))";
2.32 +by (rtac trans 1);
2.33 +br fix_eq2 1;
2.34 +br corresp_ex_simC_def 1;
2.35 +br beta_cfun 1;
2.36 +by (simp_tac (simpset() addsimps [flift1_def]) 1);
2.37 +qed"corresp_ex_simC_unfold";
2.38 +
2.39 +goal thy "(corresp_ex_simC A R`UU) s=UU";
2.40 +by (stac corresp_ex_simC_unfold 1);
2.41 +by (Simp_tac 1);
2.42 +qed"corresp_ex_simC_UU";
2.43 +
2.44 +goal thy "(corresp_ex_simC A R`nil) s = nil";
2.45 +by (stac corresp_ex_simC_unfold 1);
2.46 +by (Simp_tac 1);
2.47 +qed"corresp_ex_simC_nil";
2.48 +
2.49 +goal thy "(corresp_ex_simC A R`((a,t)>>xs)) s = \
2.50 +\ (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \
2.51 +\ in \
2.52 +\ (@cex. move A cex s a T') \
2.53 +\ @@ ((corresp_ex_simC A R`xs) T'))";
2.54 +br trans 1;
2.55 +by (stac corresp_ex_simC_unfold 1);
2.56 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
2.57 +by (Simp_tac 1);
2.58 +qed"corresp_ex_simC_cons";
2.59 +
2.60 +
2.61 +Addsimps [corresp_ex_simC_UU,corresp_ex_simC_nil,corresp_ex_simC_cons];
2.62 +
2.63 +
2.64 +
2.65 +(* ------------------------------------------------------------------ *)
2.66 +(* The following lemmata describe the definition *)
2.67 +(* of move in more detail *)
2.68 +(* ------------------------------------------------------------------ *)
2.69 +
2.70 +section"properties of move";
2.71 +
2.72 +Delsimps [Let_def];
2.73 +
2.74 +goalw thy [is_simulation_def]
2.75 + "!!f. [|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>\
2.76 +\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
2.77 +\ (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'";
2.78 +
2.79 +(* Does not perform conditional rewriting on assumptions automatically as
2.80 + usual. Instantiate all variables per hand. Ask Tobias?? *)
2.81 +by (subgoal_tac "? t' ex. (t,t'):R & move A ex s' a t'" 1);
2.82 +by (Asm_full_simp_tac 2);
2.83 +by (etac conjE 2);
2.84 +by (eres_inst_tac [("x","s")] allE 2);
2.85 +by (eres_inst_tac [("x","s'")] allE 2);
2.86 +by (eres_inst_tac [("x","t")] allE 2);
2.87 +by (eres_inst_tac [("x","a")] allE 2);
2.88 +by (Asm_full_simp_tac 2);
2.89 +(* Go on as usual *)
2.90 +be exE 1;
2.91 +by (dres_inst_tac [("x","t'"),
2.92 + ("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] selectI 1);
2.93 +be exE 1;
2.94 +be conjE 1;
2.95 +by (asm_full_simp_tac (simpset() addsimps [Let_def]) 1);
2.96 +by (res_inst_tac [("x","ex")] selectI 1);
2.97 +be conjE 1;
2.98 +ba 1;
2.99 +qed"move_is_move_sim";
2.100 +
2.101 +
2.102 +Addsimps [Let_def];
2.103 +
2.104 +goal thy
2.105 + "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
2.106 +\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
2.107 +\ is_exec_frag A (s',@x. move A x s' a T')";
2.108 +by (cut_inst_tac [] move_is_move_sim 1);
2.109 +by (REPEAT (assume_tac 1));
2.110 +by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
2.111 +qed"move_subprop1_sim";
2.112 +
2.113 +goal thy
2.114 + "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
2.115 +\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
2.116 +\ Finite (@x. move A x s' a T')";
2.117 +by (cut_inst_tac [] move_is_move_sim 1);
2.118 +by (REPEAT (assume_tac 1));
2.119 +by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
2.120 +qed"move_subprop2_sim";
2.121 +
2.122 +goal thy
2.123 + "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
2.124 +\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
2.125 +\ laststate (s',@x. move A x s' a T') = T'";
2.126 +by (cut_inst_tac [] move_is_move_sim 1);
2.127 +by (REPEAT (assume_tac 1));
2.128 +by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
2.129 +qed"move_subprop3_sim";
2.130 +
2.131 +goal thy
2.132 + "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
2.133 +\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
2.134 +\ mk_trace A`((@x. move A x s' a T')) = \
2.135 +\ (if a:ext A then a>>nil else nil)";
2.136 +by (cut_inst_tac [] move_is_move_sim 1);
2.137 +by (REPEAT (assume_tac 1));
2.138 +by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
2.139 +qed"move_subprop4_sim";
2.140 +
2.141 +goal thy
2.142 + "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
2.143 +\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
2.144 +\ (t,T'):R";
2.145 +by (cut_inst_tac [] move_is_move_sim 1);
2.146 +by (REPEAT (assume_tac 1));
2.147 +by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
2.148 +qed"move_subprop5_sim";
2.149 +
2.150 +(* ------------------------------------------------------------------ *)
2.151 +(* The following lemmata contribute to *)
2.152 +(* TRACE INCLUSION Part 1: Traces coincide *)
2.153 +(* ------------------------------------------------------------------ *)
2.154 +
2.155 +section "Lemmata for <==";
2.156 +
2.157 +
2.158 +(* ------------------------------------------------------
2.159 + Lemma 1 :Traces coincide
2.160 + ------------------------------------------------------- *)
2.161 +
2.162 +goal thy
2.163 + "!!f.[|is_simulation R C A; ext C = ext A|] ==> \
2.164 +\ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
2.165 +\ mk_trace C`ex = mk_trace A`((corresp_ex_simC A R`ex) s')";
2.166 +
2.167 +by (pair_induct_tac "ex" [is_exec_frag_def] 1);
2.168 +(* cons case *)
2.169 +by (safe_tac set_cs);
2.170 +ren "ex a t s s'" 1;
2.171 +by (asm_full_simp_tac (simpset() addsimps [mk_traceConc]) 1);
2.172 +by (forward_tac [reachable.reachable_n] 1);
2.173 +ba 1;
2.174 +by (eres_inst_tac [("x","t")] allE 1);
2.175 +by (eres_inst_tac [("x",
2.176 + "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")]
2.177 + allE 1);
2.178 +by (Asm_full_simp_tac 1);
2.179 +by (asm_full_simp_tac (simpset() addsimps
2.180 + [rewrite_rule [Let_def] move_subprop5_sim,
2.181 + rewrite_rule [Let_def] move_subprop4_sim]
2.182 + setloop split_tac [expand_if] ) 1);
2.183 +qed_spec_mp"traces_coincide_sim";
2.184 +
2.185 +
2.186 +(* ----------------------------------------------------------- *)
2.187 +(* Lemma 2 : corresp_ex_sim is execution *)
2.188 +(* ----------------------------------------------------------- *)
2.189 +
2.190 +
2.191 +goal thy
2.192 + "!!f.[| is_simulation R C A |] ==>\
2.193 +\ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R \
2.194 +\ --> is_exec_frag A (s',(corresp_ex_simC A R`ex) s')";
2.195 +
2.196 +by (Asm_full_simp_tac 1);
2.197 +by (pair_induct_tac "ex" [is_exec_frag_def] 1);
2.198 +(* main case *)
2.199 +by (safe_tac set_cs);
2.200 +ren "ex a t s s'" 1;
2.201 +by (res_inst_tac [("t",
2.202 + "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")]
2.203 + lemma_2_1 1);
2.204 +
2.205 +(* Finite *)
2.206 +be (rewrite_rule [Let_def] move_subprop2_sim) 1;
2.207 +by (REPEAT (atac 1));
2.208 +by (rtac conjI 1);
2.209 +
2.210 +(* is_exec_frag *)
2.211 +be (rewrite_rule [Let_def] move_subprop1_sim) 1;
2.212 +by (REPEAT (atac 1));
2.213 +by (rtac conjI 1);
2.214 +
2.215 +(* Induction hypothesis *)
2.216 +(* reachable_n looping, therefore apply it manually *)
2.217 +by (eres_inst_tac [("x","t")] allE 1);
2.218 +by (eres_inst_tac [("x",
2.219 + "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")]
2.220 + allE 1);
2.221 +by (Asm_full_simp_tac 1);
2.222 +by (forward_tac [reachable.reachable_n] 1);
2.223 +ba 1;
2.224 +by (asm_full_simp_tac (simpset() addsimps
2.225 + [rewrite_rule [Let_def] move_subprop5_sim]) 1);
2.226 +(* laststate *)
2.227 +be ((rewrite_rule [Let_def] move_subprop3_sim) RS sym) 1;
2.228 +by (REPEAT (atac 1));
2.229 +qed_spec_mp"correspsim_is_execution";
2.230 +
2.231 +
2.232 +(* -------------------------------------------------------------------------------- *)
2.233 +
2.234 +section "Main Theorem: T R A C E - I N C L U S I O N";
2.235 +
2.236 +(* -------------------------------------------------------------------------------- *)
2.237 +
2.238 + (* generate condition (s,S'):R & S':starts_of A, the first being intereting
2.239 + for the induction cases concerning the two lemmas correpsim_is_execution and
2.240 + traces_coincide_sim, the second for the start state case.
2.241 + S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C *)
2.242 +
2.243 +goal thy
2.244 +"!!C. [| is_simulation R C A; s:starts_of C |] \
2.245 +\ ==> let S' = @s'. (s,s'):R & s':starts_of A in \
2.246 +\ (s,S'):R & S':starts_of A";
2.247 + by (asm_full_simp_tac (simpset() addsimps [is_simulation_def,
2.248 + corresp_ex_sim_def, Int_non_empty,Image_def]) 1);
2.249 + by (REPEAT (etac conjE 1));
2.250 + be ballE 1;
2.251 + by (Blast_tac 2);
2.252 + be exE 1;
2.253 + br selectI2 1;
2.254 + ba 1;
2.255 + by (Blast_tac 1);
2.256 +qed"simulation_starts";
2.257 +
2.258 +bind_thm("sim_starts1",(rewrite_rule [Let_def] simulation_starts) RS conjunct1);
2.259 +bind_thm("sim_starts2",(rewrite_rule [Let_def] simulation_starts) RS conjunct2);
2.260 +
2.261 +
2.262 +goalw thy [traces_def]
2.263 + "!!f. [| ext C = ext A; is_simulation R C A |] \
2.264 +\ ==> traces C <= traces A";
2.265 +
2.266 + by (simp_tac(simpset() addsimps [has_trace_def2])1);
2.267 + by (safe_tac set_cs);
2.268 +
2.269 + (* give execution of abstract automata *)
2.270 + by (res_inst_tac[("x","corresp_ex_sim A R ex")] bexI 1);
2.271 +
2.272 + (* Traces coincide, Lemma 1 *)
2.273 + by (pair_tac "ex" 1);
2.274 + ren "s ex" 1;
2.275 + by (simp_tac (simpset() addsimps [corresp_ex_sim_def]) 1);
2.276 + by (res_inst_tac [("s","s")] traces_coincide_sim 1);
2.277 + by (REPEAT (atac 1));
2.278 + by (asm_full_simp_tac (simpset() addsimps [executions_def,
2.279 + reachable.reachable_0,sim_starts1]) 1);
2.280 +
2.281 + (* corresp_ex_sim is execution, Lemma 2 *)
2.282 + by (pair_tac "ex" 1);
2.283 + by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
2.284 + ren "s ex" 1;
2.285 +
2.286 + (* start state *)
2.287 + by (rtac conjI 1);
2.288 + by (asm_full_simp_tac (simpset() addsimps [sim_starts2,
2.289 + corresp_ex_sim_def]) 1);
2.290 +
2.291 + (* is-execution-fragment *)
2.292 + by (asm_full_simp_tac (simpset() addsimps [corresp_ex_sim_def]) 1);
2.293 + by (res_inst_tac [("s","s")] correspsim_is_execution 1);
2.294 + ba 1;
2.295 + by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0,sim_starts1]) 1);
2.296 +qed"trace_inclusion_for_simulations";
2.297 +
2.298 +
2.299 +
2.300 +
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Tue Jan 13 14:26:21 1998 +0100
3.3 @@ -0,0 +1,39 @@
3.4 +(* Title: HOLCF/IOA/meta_theory/SimCorrectness.thy
3.5 + ID: $Id$
3.6 + Author: Olaf Mueller
3.7 + Copyright 1997 TU Muenchen
3.8 +
3.9 +Correctness of Simulations in HOLCF/IOA
3.10 +*)
3.11 +
3.12 +
3.13 +SimCorrectness = Simulations +
3.14 +
3.15 +consts
3.16 +
3.17 + corresp_ex_sim ::"('a,'s2)ioa => (('s1 *'s2)set) =>
3.18 + ('a,'s1)execution => ('a,'s2)execution"
3.19 + (* Note: s2 instead of s1 in last argument type !! *)
3.20 + corresp_ex_simC ::"('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs
3.21 + -> ('s2 => ('a,'s2)pairs)"
3.22 +
3.23 +
3.24 +defs
3.25 +
3.26 +corresp_ex_sim_def
3.27 + "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A)
3.28 + in
3.29 + (S',(corresp_ex_simC A R`(snd ex)) S')"
3.30 +
3.31 +
3.32 +corresp_ex_simC_def
3.33 + "corresp_ex_simC A R == (fix`(LAM h ex. (%s. case ex of
3.34 + nil => nil
3.35 + | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
3.36 + T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
3.37 + in
3.38 + (@cex. move A cex s a T')
3.39 + @@ ((h`xs) T'))
3.40 + `x) )))"
3.41 +
3.42 +end
3.43 \ No newline at end of file
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOLCF/IOA/meta_theory/Simulations.ML Tue Jan 13 14:26:21 1998 +0100
4.3 @@ -0,0 +1,39 @@
4.4 +(* Title: HOLCF/IOA/meta_theory/Simulations.ML
4.5 + ID: $Id$
4.6 + Author: Olaf Mueller
4.7 + Copyright 1997 TU Muenchen
4.8 +
4.9 +Simulations in HOLCF/IOA
4.10 +*)
4.11 +
4.12 +
4.13 +
4.14 +goal thy "(A~={}) = (? x. x:A)";
4.15 +by (safe_tac set_cs);
4.16 +auto();
4.17 +qed"set_non_empty";
4.18 +
4.19 +goal thy "(A Int B ~= {}) = (? x. x: A & x:B)";
4.20 +by (simp_tac (simpset() addsimps [set_non_empty]) 1);
4.21 +qed"Int_non_empty";
4.22 +
4.23 +
4.24 +goalw thy [Image_def]
4.25 +"(R^^{x} Int S ~= {}) = (? y. (x,y):R & y:S)";
4.26 +by (simp_tac (simpset() addsimps [Int_non_empty]) 1);
4.27 +qed"Sim_start_convert";
4.28 +
4.29 +Addsimps [Sim_start_convert];
4.30 +
4.31 +
4.32 +goalw thy [is_ref_map_def,is_simulation_def]
4.33 +"!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A";
4.34 +(* start states *)
4.35 +by (Asm_full_simp_tac 1);
4.36 +(* main case *)
4.37 +by (Blast_tac 1);
4.38 +qed"ref_map_is_simulation";
4.39 +
4.40 +
4.41 +
4.42 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOLCF/IOA/meta_theory/Simulations.thy Tue Jan 13 14:26:21 1998 +0100
5.3 @@ -0,0 +1,64 @@
5.4 +(* Title: HOLCF/IOA/meta_theory/Simulations.thy
5.5 + ID: $Id$
5.6 + Author: Olaf Mueller
5.7 + Copyright 1997 TU Muenchen
5.8 +
5.9 +Simulations in HOLCF/IOA
5.10 +*)
5.11 +
5.12 +Simulations = RefCorrectness +
5.13 +
5.14 +default term
5.15 +
5.16 +consts
5.17 +
5.18 + is_simulation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
5.19 + is_backward_simulation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
5.20 + is_forw_back_simulation ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
5.21 + is_back_forw_simulation ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
5.22 + is_history_relation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
5.23 + is_prophecy_relation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
5.24 +
5.25 +defs
5.26 +
5.27 +is_simulation_def
5.28 + "is_simulation R C A ==
5.29 + (!s:starts_of C. R^^{s} Int starts_of A ~= {}) &
5.30 + (!s s' t a. reachable C s &
5.31 + s -a--C-> t &
5.32 + (s,s') : R
5.33 + --> (? t' ex. (t,t'):R & move A ex s' a t'))"
5.34 +
5.35 +is_backward_simulation_def
5.36 + "is_backward_simulation R C A ==
5.37 + (!s:starts_of C. R^^{s} <= starts_of A) &
5.38 + (!s t t' a. reachable C s &
5.39 + s -a--C-> t &
5.40 + (t,t') : R
5.41 + --> (? ex s'. (s,s'):R & move A ex s' a t'))"
5.42 +
5.43 +is_forw_back_simulation_def
5.44 + "is_forw_back_simulation R C A ==
5.45 + (!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &
5.46 + (!s S' t a. reachable C s &
5.47 + s -a--C-> t &
5.48 + (s,S') : R
5.49 + --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t')))"
5.50 +
5.51 +is_back_forw_simulation_def
5.52 + "is_back_forw_simulation R C A ==
5.53 + (!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &
5.54 + (!s t T' a. reachable C s &
5.55 + s -a--C-> t &
5.56 + (t,T') : R
5.57 + --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t')))"
5.58 +
5.59 +is_history_relation_def
5.60 + "is_history_relation R C A == is_simulation R C A &
5.61 + is_ref_map (%x.(@y. (x,y):(R^-1))) A C"
5.62 +
5.63 +is_prophecy_relation_def
5.64 + "is_prophecy_relation R C A == is_backward_simulation R C A &
5.65 + is_ref_map (%x.(@y. (x,y):(R^-1))) A C"
5.66 +
5.67 +end
6.1 --- a/src/HOLCF/IOA/meta_theory/TrivEx2.ML Tue Jan 13 10:40:38 1998 +0100
6.2 +++ b/src/HOLCF/IOA/meta_theory/TrivEx2.ML Tue Jan 13 14:26:21 1998 +0100
6.3 @@ -64,3 +64,9 @@
6.4 qed"TrivEx2_abstraction";
6.5
6.6
6.7 +(*
6.8 +goal thy "validIOA aut_ioa (Box (Init (%(s,a,t). a= Some(Alarm(APonR))))
6.9 +IMPLIES (Next (Init (%(s,a,t). info_comp(s) = APonR))))";
6.10 +
6.11 +*)
6.12 +