added files containing temproal logic and abstraction;
authormueller
Mon Jan 12 17:48:23 1998 +0100 (1998-01-12)
changeset 45598e604d885b54
parent 4558 31becfd8d329
child 4560 83e1eec9cfeb
added files containing temproal logic and abstraction;
src/HOLCF/IOA/meta_theory/Abstraction.ML
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/LiveIOA.ML
src/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOLCF/IOA/meta_theory/Pred.thy
src/HOLCF/IOA/meta_theory/RefCorrectness.ML
src/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOLCF/IOA/meta_theory/RefMappings.ML
src/HOLCF/IOA/meta_theory/RefMappings.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/IOA/meta_theory/TL.ML
src/HOLCF/IOA/meta_theory/TL.thy
src/HOLCF/IOA/meta_theory/TLS.ML
src/HOLCF/IOA/meta_theory/TLS.thy
src/HOLCF/IOA/meta_theory/Traces.ML
src/HOLCF/IOA/meta_theory/Traces.thy
src/HOLCF/IOA/meta_theory/TrivEx.ML
src/HOLCF/IOA/meta_theory/TrivEx.thy
src/HOLCF/IOA/meta_theory/TrivEx2.ML
src/HOLCF/IOA/meta_theory/TrivEx2.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Jan 12 17:48:23 1998 +0100
     1.3 @@ -0,0 +1,498 @@
     1.4 +(*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Olaf M"uller
     1.7 +    Copyright   1997  TU Muenchen
     1.8 +
     1.9 +Abstraction Theory -- tailored for I/O automata
    1.10 +*)   
    1.11 +
    1.12 +
    1.13 +section "cex_abs";
    1.14 +	
    1.15 +
    1.16 +(* ---------------------------------------------------------------- *)
    1.17 +(*                             cex_abs                              *)
    1.18 +(* ---------------------------------------------------------------- *)
    1.19 +
    1.20 +goal thy "cex_abs f (s,UU) = (f s, UU)";
    1.21 +by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
    1.22 +qed"cex_abs_UU";
    1.23 +
    1.24 +goal thy "cex_abs f (s,nil) = (f s, nil)";
    1.25 +by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
    1.26 +qed"cex_abs_nil";
    1.27 +
    1.28 +goal thy "cex_abs f (s,(a,t)>>ex) = (f s, (a,f t) >> (snd (cex_abs f (t,ex))))";
    1.29 +by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
    1.30 +qed"cex_abs_cons";
    1.31 +
    1.32 +Addsimps [cex_abs_UU, cex_abs_nil, cex_abs_cons];
    1.33 +
    1.34 + 
    1.35 +
    1.36 +section "lemmas";
    1.37 +
    1.38 +(* ---------------------------------------------------------------- *)
    1.39 +(*                           Lemmas                                 *)
    1.40 +(* ---------------------------------------------------------------- *)
    1.41 +
    1.42 +goal thy "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))";
    1.43 +by (simp_tac (simpset() addsimps [temp_weakening_def,temp_strengthening_def,
    1.44 +     NOT_def,temp_sat_def,satisfies_def]) 1);
    1.45 +auto();
    1.46 +qed"temp_weakening_def2";
    1.47 +
    1.48 +goal thy "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))";
    1.49 +by (simp_tac (simpset() addsimps [state_weakening_def,state_strengthening_def,
    1.50 +     NOT_def]) 1);
    1.51 +auto();
    1.52 +qed"state_weakening_def2";
    1.53 +
    1.54 +
    1.55 +section "Abstraction Rules for Properties";
    1.56 +
    1.57 +(* ---------------------------------------------------------------- *)
    1.58 +(*                Abstraction Rules for Properties                  *)
    1.59 +(* ---------------------------------------------------------------- *)
    1.60 +
    1.61 +
    1.62 +goalw thy [cex_abs_def]
    1.63 + "!!h.[| is_abstraction h C A |] ==>\
    1.64 +\ !s. reachable C s & is_exec_frag C (s,xs) \
    1.65 +\ --> is_exec_frag A (cex_abs h (s,xs))"; 
    1.66 +
    1.67 +by (Asm_full_simp_tac 1);
    1.68 +by (pair_induct_tac "xs" [is_exec_frag_def] 1);
    1.69 +(* main case *)
    1.70 +by (safe_tac set_cs);
    1.71 +by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def])1);
    1.72 +by (forward_tac [reachable.reachable_n] 1);
    1.73 +by (assume_tac 1);
    1.74 +by (Asm_full_simp_tac 1);
    1.75 +qed"exec_frag_abstraction";
    1.76 +
    1.77 +
    1.78 +goal thy "!!A. is_abstraction h C A ==> weakeningIOA A C h";
    1.79 +by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1);
    1.80 +auto();
    1.81 +by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
    1.82 +(* start state *) 
    1.83 +by (rtac conjI 1);
    1.84 +by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1);
    1.85 +(* is-execution-fragment *)
    1.86 +by (etac (exec_frag_abstraction RS spec RS mp) 1);
    1.87 +by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
    1.88 +qed"abs_is_weakening";
    1.89 +
    1.90 +
    1.91 +goal thy "!!A. [|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
    1.92 +\         ==> validIOA C P";
    1.93 +bd abs_is_weakening 1;
    1.94 +by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, 
    1.95 +    validIOA_def, temp_strengthening_def])1);
    1.96 +by (safe_tac set_cs);
    1.97 +by (pair_tac "ex" 1);
    1.98 +qed"AbsRuleT1";
    1.99 +
   1.100 +
   1.101 +(* FIX: Nach TLS.ML *)
   1.102 +
   1.103 +goal thy "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))";
   1.104 +by (simp_tac (simpset() addsimps [IMPLIES_def,temp_sat_def, satisfies_def])1);
   1.105 +qed"IMPLIES_temp_sat";
   1.106 +
   1.107 +goal thy "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))";
   1.108 +by (simp_tac (simpset() addsimps [AND_def,temp_sat_def, satisfies_def])1);
   1.109 +qed"AND_temp_sat";
   1.110 +
   1.111 +goal thy "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))";
   1.112 +by (simp_tac (simpset() addsimps [OR_def,temp_sat_def, satisfies_def])1);
   1.113 +qed"OR_temp_sat";
   1.114 +
   1.115 +goal thy "(ex |== .~ P) = (~ (ex |== P))";
   1.116 +by (simp_tac (simpset() addsimps [NOT_def,temp_sat_def, satisfies_def])1);
   1.117 +qed"NOT_temp_sat";
   1.118 +
   1.119 +Addsimps [IMPLIES_temp_sat,AND_temp_sat,OR_temp_sat,NOT_temp_sat];
   1.120 +
   1.121 +
   1.122 +goalw thy [is_live_abstraction_def]
   1.123 +   "!!A. [|is_live_abstraction h (C,L) (A,M); \
   1.124 +\         validLIOA (A,M) Q;  temp_strengthening Q P h |] \
   1.125 +\         ==> validLIOA (C,L) P";
   1.126 +auto();
   1.127 +bd abs_is_weakening 1;
   1.128 +by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
   1.129 +    validLIOA_def, validIOA_def, temp_strengthening_def])1);
   1.130 +by (safe_tac set_cs);
   1.131 +by (pair_tac "ex" 1);
   1.132 +qed"AbsRuleT2";
   1.133 +
   1.134 +
   1.135 +goalw thy [is_live_abstraction_def]
   1.136 +   "!!A. [|is_live_abstraction h (C,L) (A,M); \
   1.137 +\         validLIOA (A,M) (H1 .--> Q);  temp_strengthening Q P h; \
   1.138 +\         temp_weakening H1 H2 h; validLIOA (C,L) H2 |] \
   1.139 +\         ==> validLIOA (C,L) P";
   1.140 +auto();
   1.141 +bd abs_is_weakening 1;
   1.142 +by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
   1.143 +    validLIOA_def, validIOA_def, temp_strengthening_def])1);
   1.144 +by (safe_tac set_cs);
   1.145 +by (pair_tac "ex" 1);
   1.146 +qed"AbsRuleTImprove";
   1.147 +
   1.148 +
   1.149 +section "Correctness of safe abstraction";
   1.150 +
   1.151 +(* ---------------------------------------------------------------- *)
   1.152 +(*              Correctness of safe abstraction                     *)
   1.153 +(* ---------------------------------------------------------------- *)
   1.154 +
   1.155 +
   1.156 +goalw thy [is_abstraction_def,is_ref_map_def] 
   1.157 +"!! h. is_abstraction h C A ==> is_ref_map h C A";
   1.158 +by (safe_tac set_cs);
   1.159 +by (res_inst_tac[("x","(a,h t)>>nil")] exI 1);
   1.160 +by (asm_full_simp_tac (simpset() addsimps [move_def])1);
   1.161 +qed"abstraction_is_ref_map";
   1.162 +
   1.163 +
   1.164 +goal thy "!! h. [| inp(C)=inp(A); out(C)=out(A); \
   1.165 +\                  is_abstraction h C A |] \
   1.166 +\               ==> C =<| A";
   1.167 +by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1);
   1.168 +br trace_inclusion 1;
   1.169 +by (simp_tac (simpset() addsimps [externals_def])1);
   1.170 +by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
   1.171 +be abstraction_is_ref_map 1;
   1.172 +qed"abs_safety";
   1.173 +
   1.174 +
   1.175 +section "Correctness of life abstraction";
   1.176 +
   1.177 +(* ---------------------------------------------------------------- *)
   1.178 +(*              Correctness of life abstraction                     *)
   1.179 +(* ---------------------------------------------------------------- *)
   1.180 +
   1.181 +
   1.182 +(* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x),
   1.183 +   that is to special Map Lemma *)
   1.184 +goalw thy [cex_abs_def,mk_trace_def,filter_act_def]
   1.185 +  "!! f. ext C = ext A \
   1.186 +\        ==> mk_trace C`xs = mk_trace A`(snd (cex_abs f (s,xs)))";
   1.187 +by (Asm_full_simp_tac 1);
   1.188 +by (pair_induct_tac "xs" [] 1);
   1.189 +qed"traces_coincide_abs";
   1.190 +
   1.191 +
   1.192 +goalw thy [cex_abs_def]
   1.193 + "!!f.[| is_abstraction h C A |] ==>\
   1.194 +\ !s. reachable C s & is_exec_frag C (s,xs) \
   1.195 +\ --> is_exec_frag A (cex_abs h (s,xs))"; 
   1.196 +
   1.197 +by (Asm_full_simp_tac 1);
   1.198 +by (pair_induct_tac "xs" [is_exec_frag_def] 1);
   1.199 +(* main case *)
   1.200 +by (safe_tac set_cs);
   1.201 +(* Stepd correspond to each other *)
   1.202 +by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def])1);
   1.203 +(* IH *)
   1.204 +(* reachable_n looping, therefore apply it manually *)
   1.205 +by (eres_inst_tac [("x","y")] allE 1);
   1.206 +by (Asm_full_simp_tac 1);
   1.207 +by (forward_tac [reachable.reachable_n] 1);
   1.208 +by (assume_tac 1);
   1.209 +by (Asm_full_simp_tac 1);
   1.210 +qed_spec_mp"correp_is_exec_abs";
   1.211 +
   1.212 +(* Does not work with abstraction_is_ref_map as proof of abs_safety, because
   1.213 +   is_live_abstraction includes temp_strengthening which is necessarily based
   1.214 +   on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific
   1.215 +   way for cex_abs *)
   1.216 +goal thy "!! h. [| inp(C)=inp(A); out(C)=out(A); \
   1.217 +\                  is_live_abstraction h (C,M) (A,L) |] \
   1.218 +\               ==> live_implements (C,M) (A,L)";
   1.219 +
   1.220 +by (asm_full_simp_tac (simpset() addsimps [is_live_abstraction_def, live_implements_def,
   1.221 +livetraces_def,liveexecutions_def]) 1);
   1.222 +by (safe_tac set_cs);
   1.223 +by (res_inst_tac[("x","cex_abs h ex")] exI 1);
   1.224 +by (safe_tac set_cs);
   1.225 +  (* Traces coincide *)
   1.226 +  by (pair_tac "ex" 1);
   1.227 +  by (rtac traces_coincide_abs 1);
   1.228 +  by (simp_tac (simpset() addsimps [externals_def])1);
   1.229 +  by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
   1.230 + 
   1.231 +  (* cex_abs is execution *)
   1.232 +  by (pair_tac "ex" 1);
   1.233 +  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   1.234 +  (* start state *) 
   1.235 +  by (rtac conjI 1);
   1.236 +  by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1);
   1.237 +  (* is-execution-fragment *)
   1.238 +  by (etac correp_is_exec_abs 1);
   1.239 +  by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
   1.240 +
   1.241 + (* Liveness *) 
   1.242 +by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2]) 1);
   1.243 + by (pair_tac "ex" 1);
   1.244 +qed"abs_liveness";
   1.245 +
   1.246 +(* FIX: NAch Traces.ML bringen *)
   1.247 +
   1.248 +goalw thy [ioa_implements_def] 
   1.249 +"!! A. [| A =<| B; B =<| C|] ==> A =<| C"; 
   1.250 +auto();
   1.251 +qed"implements_trans";
   1.252 +
   1.253 +
   1.254 +section "Abstraction Rules for Automata";
   1.255 +
   1.256 +(* ---------------------------------------------------------------- *)
   1.257 +(*                Abstraction Rules for Automata                    *)
   1.258 +(* ---------------------------------------------------------------- *)
   1.259 +
   1.260 +goal thy "!! C. [| inp(C)=inp(A); out(C)=out(A); \
   1.261 +\                  inp(Q)=inp(P); out(Q)=out(P); \
   1.262 +\                  is_abstraction h1 C A; \
   1.263 +\                  A =<| Q ; \
   1.264 +\                  is_abstraction h2 Q P |] \
   1.265 +\               ==> C =<| P";   
   1.266 +bd abs_safety 1;
   1.267 +by (REPEAT (atac 1));
   1.268 +bd abs_safety 1;
   1.269 +by (REPEAT (atac 1));
   1.270 +be implements_trans 1;
   1.271 +be implements_trans 1;
   1.272 +ba 1;
   1.273 +qed"AbsRuleA1";
   1.274 +
   1.275 +
   1.276 +goal thy "!! C. [| inp(C)=inp(A); out(C)=out(A); \
   1.277 +\                  inp(Q)=inp(P); out(Q)=out(P); \
   1.278 +\                  is_live_abstraction h1 (C,LC) (A,LA); \
   1.279 +\                  live_implements (A,LA) (Q,LQ) ; \
   1.280 +\                  is_live_abstraction h2 (Q,LQ) (P,LP) |] \
   1.281 +\               ==> live_implements (C,LC) (P,LP)";   
   1.282 +bd abs_liveness 1;
   1.283 +by (REPEAT (atac 1));
   1.284 +bd abs_liveness 1;
   1.285 +by (REPEAT (atac 1));
   1.286 +be live_implements_trans 1;
   1.287 +be live_implements_trans 1;
   1.288 +ba 1;
   1.289 +qed"AbsRuleA2";
   1.290 +
   1.291 +
   1.292 +Delsimps [split_paired_All];
   1.293 +
   1.294 +
   1.295 +section "Localizing Temporal Strengthenings and Weakenings";
   1.296 +
   1.297 +(* ---------------------------------------------------------------- *)
   1.298 +(*                Localizing Temproal Strengthenings - 1               *)
   1.299 +(* ---------------------------------------------------------------- *)
   1.300 +
   1.301 +goalw thy [temp_strengthening_def]
   1.302 +"!! h. [| temp_strengthening P1 Q1 h; \
   1.303 +\         temp_strengthening P2 Q2 h |] \
   1.304 +\      ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h";
   1.305 +auto();
   1.306 +qed"strength_AND";
   1.307 +
   1.308 +goalw thy [temp_strengthening_def]
   1.309 +"!! h. [| temp_strengthening P1 Q1 h; \
   1.310 +\         temp_strengthening P2 Q2 h |] \
   1.311 +\      ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h";
   1.312 +auto();
   1.313 +qed"strength_OR";
   1.314 +
   1.315 +goalw thy [temp_strengthening_def]
   1.316 +"!! h. [| temp_weakening P Q h |] \
   1.317 +\      ==> temp_strengthening (.~ P) (.~ Q) h";
   1.318 +by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   1.319 +auto();
   1.320 +qed"strength_NOT";
   1.321 +
   1.322 +goalw thy [temp_strengthening_def]
   1.323 +"!! h. [| temp_weakening P1 Q1 h; \
   1.324 +\         temp_strengthening P2 Q2 h |] \
   1.325 +\      ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h";
   1.326 +by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   1.327 +auto();
   1.328 +qed"strength_IMPLIES";
   1.329 +
   1.330 +
   1.331 +
   1.332 +(* ---------------------------------------------------------------- *)
   1.333 +(*                Localizing Temproal Weakenings - Part 1           *)
   1.334 +(* ---------------------------------------------------------------- *)
   1.335 +
   1.336 +goal thy
   1.337 +"!! h. [| temp_weakening P1 Q1 h; \
   1.338 +\         temp_weakening P2 Q2 h |] \
   1.339 +\      ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h";
   1.340 +by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   1.341 +auto();
   1.342 +qed"weak_AND";
   1.343 +
   1.344 +goal thy 
   1.345 +"!! h. [| temp_weakening P1 Q1 h; \
   1.346 +\         temp_weakening P2 Q2 h |] \
   1.347 +\      ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h";
   1.348 +by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   1.349 +auto();
   1.350 +qed"weak_OR";
   1.351 +
   1.352 +goalw thy [temp_strengthening_def]
   1.353 +"!! h. [| temp_strengthening P Q h |] \
   1.354 +\      ==> temp_weakening (.~ P) (.~ Q) h";
   1.355 +by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   1.356 +auto();
   1.357 +qed"weak_NOT";
   1.358 +
   1.359 +goalw thy [temp_strengthening_def]
   1.360 +"!! h. [| temp_strengthening P1 Q1 h; \
   1.361 +\         temp_weakening P2 Q2 h |] \
   1.362 +\      ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h";
   1.363 +by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   1.364 +auto();
   1.365 +qed"weak_IMPLIES";
   1.366 +
   1.367 +
   1.368 +(* ---------------------------------------------------------------- *)
   1.369 +(*             Localizing Temproal Strengthenings - 2               *)
   1.370 +(* ---------------------------------------------------------------- *)
   1.371 +(*
   1.372 +goalw thy [temp_strengthening_def,state_strengthening_def,
   1.373 +temp_sat_def,satisfies_def,Init_def]
   1.374 +"!! h. [| state_strengthening P Q h |]\
   1.375 +\      ==> temp_strengthening (Init P) (Init Q) h";
   1.376 +by (safe_tac set_cs);
   1.377 +by (pair_tac "ex" 1);
   1.378 +by (Seq_case_simp_tac "y" 1);
   1.379 +
   1.380 +
   1.381 +
   1.382 +goalw thy [temp_strengthening_def,state_strengthening_def]
   1.383 +"!! h. [| temp_strengthening P Q h |]\
   1.384 +\      ==> temp_strengthening ([] P) ([] Q) h";
   1.385 +
   1.386 +goalw thy [temp_strengthening_def,state_strengthening_def]
   1.387 +"!! h. [| temp_strengthening P Q h |]\
   1.388 +\      ==> temp_strengthening (Next P) (Next Q) h";
   1.389 +
   1.390 +*)
   1.391 +
   1.392 +(* ---------------------------------------------------------------- *)
   1.393 +(*             Localizing Temproal Weakenings     - 2               *)
   1.394 +(* ---------------------------------------------------------------- *)
   1.395 +
   1.396 +(*
   1.397 +goalw thy [temp_weakening_def,state_weakening_def,
   1.398 +temp_sat_def,satisfies_def,Init_def]
   1.399 +"!! h. [| state_weakening P Q h |]\
   1.400 +\      ==> temp_weakening (Init P) (Init Q) h";
   1.401 +by (safe_tac set_cs);
   1.402 +by (pair_tac "ex" 1);
   1.403 +by (Seq_case_simp_tac "y" 1);
   1.404 +
   1.405 +
   1.406 +
   1.407 +goalw thy [temp_weakening_def,state_weakening_def]
   1.408 +"!! h. [| temp_weakening P Q h |]\
   1.409 +\      ==> temp_weakening ([] P) ([] Q) h";
   1.410 +
   1.411 +goalw thy [temp_weakening_def,state_weakening_def]
   1.412 +"!! h. [| temp_weakening P Q h |]\
   1.413 +\      ==> temp_weakening (Next P) (Next Q) h";
   1.414 +
   1.415 +*)
   1.416 +
   1.417 +(* ---------------------------------------------------------------- *)
   1.418 +(*             Localizing Temproal Strengthenings - 3               *)
   1.419 +(* ---------------------------------------------------------------- *)
   1.420 +
   1.421 +
   1.422 +goalw thy [Diamond_def]
   1.423 +"!! h. [| temp_strengthening P Q h |]\
   1.424 +\      ==> temp_strengthening (<> P) (<> Q) h";
   1.425 +br strength_NOT 1;
   1.426 +br weak_Box 1;
   1.427 +be weak_NOT 1;
   1.428 +qed"strength_Diamond";
   1.429 +
   1.430 +goalw thy [Leadsto_def]
   1.431 +"!! h. [| temp_weakening P1 P2 h;\
   1.432 +\         temp_strengthening Q1 Q2 h |]\
   1.433 +\      ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h";
   1.434 +br strength_Box 1;
   1.435 +be strength_IMPLIES 1;
   1.436 +be strength_Diamond 1;
   1.437 +qed"strength_Leadsto";
   1.438 +
   1.439 +
   1.440 +(* ---------------------------------------------------------------- *)
   1.441 +(*             Localizing Temporal Weakenings - 3                   *)
   1.442 +(* ---------------------------------------------------------------- *)
   1.443 +
   1.444 +
   1.445 +goalw thy [Diamond_def]
   1.446 +"!! h. [| temp_weakening P Q h |]\
   1.447 +\      ==> temp_weakening (<> P) (<> Q) h";
   1.448 +br weak_NOT 1;
   1.449 +br strength_Box 1;
   1.450 +be strength_NOT 1;
   1.451 +qed"weak_Diamond";
   1.452 +
   1.453 +goalw thy [Leadsto_def]
   1.454 +"!! h. [| temp_strengthening P1 P2 h;\
   1.455 +\         temp_weakening Q1 Q2 h |]\
   1.456 +\      ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h";
   1.457 +br weak_Box 1;
   1.458 +be weak_IMPLIES 1;
   1.459 +be weak_Diamond 1;
   1.460 +qed"weak_Leadsto";
   1.461 +
   1.462 +goalw thy [WF_def]
   1.463 +  " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ 
   1.464 +\   ==> temp_weakening (WF A acts) (WF C acts) h";
   1.465 +br weak_IMPLIES 1;
   1.466 +br strength_Diamond 1;
   1.467 +br strength_Box 1;
   1.468 +br strength_Init 1;
   1.469 +br weak_Box 2;
   1.470 +br weak_Diamond 2;
   1.471 +br weak_Init 2;
   1.472 +by (auto_tac (claset(),
   1.473 +              simpset() addsimps [state_weakening_def,state_strengthening_def,
   1.474 +                             xt2_def,plift_def,option_lift_def,NOT_def]));
   1.475 +qed"weak_WF";
   1.476 +
   1.477 +goalw thy [SF_def]
   1.478 +  " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ 
   1.479 +\   ==> temp_weakening (SF A acts) (SF C acts) h";
   1.480 +br weak_IMPLIES 1;
   1.481 +br strength_Box 1;
   1.482 +br strength_Diamond 1;
   1.483 +br strength_Init 1;
   1.484 +br weak_Box 2;
   1.485 +br weak_Diamond 2;
   1.486 +br weak_Init 2;
   1.487 +by (auto_tac (claset(),
   1.488 +              simpset() addsimps [state_weakening_def,state_strengthening_def,
   1.489 +                             xt2_def,plift_def,option_lift_def,NOT_def]));
   1.490 +qed"weak_SF";
   1.491 +
   1.492 +
   1.493 +val weak_strength_lemmas = 
   1.494 +    [weak_OR,weak_AND,weak_NOT,weak_IMPLIES,weak_Box,weak_Next,weak_Init,
   1.495 +     weak_Diamond,weak_Leadsto,strength_OR,strength_AND,strength_NOT,
   1.496 +     strength_IMPLIES,strength_Box,strength_Next,strength_Init,
   1.497 +     strength_Diamond,strength_Leadsto,weak_WF,weak_SF];
   1.498 +
   1.499 +fun abstraction_tac i = 
   1.500 +    SELECT_GOAL (auto_tac (claset() addSIs weak_strength_lemmas,
   1.501 +                           simpset() addsimps [state_strengthening_def,state_weakening_def])) i;
   1.502 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Mon Jan 12 17:48:23 1998 +0100
     2.3 @@ -0,0 +1,88 @@
     2.4 +(*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Olaf M"uller
     2.7 +    Copyright   1997  TU Muenchen
     2.8 +
     2.9 +Abstraction Theory -- tailored for I/O automata
    2.10 +*)   
    2.11 +
    2.12 +		       
    2.13 +Abstraction = LiveIOA + TLS + 
    2.14 +
    2.15 +default term
    2.16 +
    2.17 +
    2.18 +consts
    2.19 +
    2.20 +  cex_abs   ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution"
    2.21 +
    2.22 +  is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
    2.23 +
    2.24 +  weakeningIOA       :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" 
    2.25 +  temp_weakening     :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" 
    2.26 +  temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" 
    2.27 +
    2.28 +  state_weakening       :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool"
    2.29 +  state_strengthening   :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool"
    2.30 +
    2.31 +  is_live_abstraction  :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
    2.32 +
    2.33 +
    2.34 +defs
    2.35 +
    2.36 +is_abstraction_def
    2.37 +  "is_abstraction f C A ==                          
    2.38 +   (!s:starts_of(C). f(s):starts_of(A)) &        
    2.39 +   (!s t a. reachable C s & s -a--C-> t     
    2.40 +            --> (f s) -a--A-> (f t))"
    2.41 +
    2.42 +is_live_abstraction_def
    2.43 +  "is_live_abstraction h CL AM == 
    2.44 +      is_abstraction h (fst CL) (fst AM) &
    2.45 +      temp_weakening (snd AM) (snd CL) h"
    2.46 +
    2.47 +cex_abs_def
    2.48 +  "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))`(snd ex))"
    2.49 +
    2.50 +weakeningIOA_def
    2.51 +   "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A"
    2.52 +
    2.53 +temp_weakening_def
    2.54 +   "temp_weakening Q P h == temp_strengthening (.~ Q) (.~ P) h"
    2.55 +
    2.56 +temp_strengthening_def
    2.57 +   "temp_strengthening Q P h == ! ex. (cex_abs h ex |== Q) --> (ex |== P)"
    2.58 +
    2.59 +state_weakening_def
    2.60 +  "state_weakening Q P h == state_strengthening (.~Q) (.~P) h"
    2.61 +
    2.62 +state_strengthening_def
    2.63 +  "state_strengthening Q P h == ! s t a.  Q (h(s),a,h(t)) --> P (s,a,t)"
    2.64 +
    2.65 +rules
    2.66 +
    2.67 +strength_Init
    2.68 + "state_strengthening P Q h 
    2.69 +  ==> temp_strengthening (Init P) (Init Q) h"
    2.70 +
    2.71 +strength_Box
    2.72 +"temp_strengthening P Q h 
    2.73 + ==> temp_strengthening ([] P) ([] Q) h"
    2.74 +
    2.75 +strength_Next
    2.76 +"temp_strengthening P Q h 
    2.77 + ==> temp_strengthening (Next P) (Next Q) h"
    2.78 +
    2.79 +weak_Init
    2.80 + "state_weakening P Q h 
    2.81 +  ==> temp_weakening (Init P) (Init Q) h"
    2.82 +
    2.83 +weak_Box
    2.84 +"temp_weakening P Q h 
    2.85 + ==> temp_weakening ([] P) ([] Q) h"
    2.86 +
    2.87 +weak_Next
    2.88 +"temp_weakening P Q h 
    2.89 + ==> temp_weakening (Next P) (Next Q) h"
    2.90 +
    2.91 +end
    2.92 \ No newline at end of file
     3.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Mon Jan 12 17:26:34 1998 +0100
     3.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Mon Jan 12 17:48:23 1998 +0100
     3.3 @@ -32,6 +32,25 @@
     3.4    input_enabled	 ::"('a,'s)ioa => bool"
     3.5    IOA	         ::"('a,'s)ioa => bool"
     3.6  
     3.7 +  (* constraints for fair IOA *)
     3.8 +
     3.9 +  fairIOA        ::"('a,'s)ioa => bool"
    3.10 +  input_resistant::"('a,'s)ioa => bool"
    3.11 +
    3.12 +  (* enabledness of actions and action sets *)
    3.13 +
    3.14 +  enabled        ::"('a,'s)ioa => 'a => 's => bool"
    3.15 +  Enabled    ::"('a,'s)ioa => 'a set => 's => bool"
    3.16 +
    3.17 +  (* action set keeps enabled until probably disabled by itself *) 
    3.18 +
    3.19 +  en_persistent  :: "('a,'s)ioa => 'a set => bool"
    3.20 +
    3.21 + (* post_conditions for actions and action sets *)
    3.22 +
    3.23 +  was_enabled        ::"('a,'s)ioa => 'a => 's => bool"
    3.24 +  set_was_enabled    ::"('a,'s)ioa => 'a set => 's => bool"
    3.25 +
    3.26    (* reachability and invariants *)
    3.27    reachable     :: "('a,'s)ioa => 's set"
    3.28    invariant     :: "[('a,'s)ioa, 's=>bool] => bool"
    3.29 @@ -209,6 +228,35 @@
    3.30     {rename_set s ren | s. s: wfair_of ioa},
    3.31     {rename_set s ren | s. s: sfair_of ioa})"
    3.32  
    3.33 +(* ------------------------- fairness ----------------------------- *)
    3.34 +
    3.35 +fairIOA_def
    3.36 +  "fairIOA A == (! S : wfair_of A. S<= local A) & 
    3.37 +                (! S : sfair_of A. S<= local A)"
    3.38 +
    3.39 +input_resistant_def
    3.40 +  "input_resistant A == ! W : sfair_of A. ! s a t. 
    3.41 +                        reachable A s & reachable A t & a:inp A &
    3.42 +                        Enabled A W s & s -a--A-> t
    3.43 +                        --> Enabled A W t"
    3.44 +
    3.45 +enabled_def
    3.46 +  "enabled A a s == ? t. s-a--A-> t"
    3.47 +
    3.48 +Enabled_def
    3.49 +  "Enabled A W s == ? w:W. enabled A w s"
    3.50 +
    3.51 +en_persistent_def
    3.52 +  "en_persistent A W == ! s a t. Enabled A W s & 
    3.53 +                                 a ~:W & 
    3.54 +                                 s -a--A-> t 
    3.55 +                                 --> Enabled A W t"
    3.56 +was_enabled_def
    3.57 +  "was_enabled A a t == ? s. s-a--A-> t"
    3.58 +
    3.59 +set_was_enabled_def
    3.60 +  "set_was_enabled A W t == ? w:W. was_enabled A w t"
    3.61 +
    3.62  
    3.63  end
    3.64  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Mon Jan 12 17:48:23 1998 +0100
     4.3 @@ -0,0 +1,73 @@
     4.4 +(*  Title:      HOLCF/IOA/meta_theory/LiveIOA.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Olaf M"uller
     4.7 +    Copyright   1997  TU Muenchen
     4.8 +
     4.9 +Live I/O Automata
    4.10 +
    4.11 +*)   
    4.12 +
    4.13 +Delsimps [split_paired_Ex];
    4.14 +
    4.15 +goalw thy [live_implements_def] 
    4.16 +"!! A. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
    4.17 +\     ==> live_implements (A,LA) (C,LC)"; 
    4.18 +auto();
    4.19 +qed"live_implements_trans";
    4.20 +
    4.21 +
    4.22 +section "Correctness of live refmap";
    4.23 +	
    4.24 +
    4.25 +(* ---------------------------------------------------------------- *)
    4.26 +(*                Correctness of live refmap                        *)
    4.27 +(* ---------------------------------------------------------------- *)
    4.28 +
    4.29 +
    4.30 +goal thy "!! f. [| inp(C)=inp(A); out(C)=out(A); \
    4.31 +\                  is_live_ref_map f (C,M) (A,L) |] \
    4.32 +\               ==> live_implements (C,M) (A,L)";
    4.33 +
    4.34 +by (asm_full_simp_tac (simpset() addsimps [is_live_ref_map_def, live_implements_def,
    4.35 +livetraces_def,liveexecutions_def]) 1);
    4.36 +by (safe_tac set_cs);
    4.37 +by (res_inst_tac[("x","corresp_ex A f ex")] exI 1);
    4.38 +by (safe_tac set_cs);
    4.39 +  (* Traces coincide, Lemma 1 *)
    4.40 +  by (pair_tac "ex" 1);
    4.41 +  by (etac (lemma_1 RS spec RS mp) 1);
    4.42 +  by (simp_tac (simpset() addsimps [externals_def])1);
    4.43 +  by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
    4.44 +  by (asm_full_simp_tac (simpset() addsimps [executions_def,reachable.reachable_0]) 1);
    4.45 + 
    4.46 +  (* corresp_ex is execution, Lemma 2 *)
    4.47 +  by (pair_tac "ex" 1);
    4.48 +  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
    4.49 +  (* start state *) 
    4.50 +  by (rtac conjI 1);
    4.51 +  by (asm_full_simp_tac (simpset() addsimps [is_ref_map_def,corresp_ex_def]) 1);
    4.52 +  (* is-execution-fragment *)
    4.53 +  by (etac (lemma_2 RS spec RS mp) 1);
    4.54 +  by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
    4.55 +
    4.56 + (* Liveness *)
    4.57 +auto();
    4.58 +qed"live_implements";
    4.59 +
    4.60 +
    4.61 +(*
    4.62 +
    4.63 +(* Classical Fairness and Fairness by Temporal Formula coincide *)
    4.64 + 
    4.65 +goal thy "!! ex. Finite (snd ex) ==> \
    4.66 +\          (ex |== WF A acts) = (~ Enabled A acts (laststate ex))";
    4.67 +
    4.68 +In 3 steps:
    4.69 +
    4.70 +1) []<>P and <>[]P mean both P (Last`s)
    4.71 +2) Transform this to executions and laststate
    4.72 +3) plift is used to show that plift (laststate ex) : acts == False. 
    4.73 +
    4.74 +
    4.75 +
    4.76 +*)
    4.77 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Mon Jan 12 17:48:23 1998 +0100
     5.3 @@ -0,0 +1,62 @@
     5.4 +(*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Olaf M"uller
     5.7 +    Copyright   1997  TU Muenchen
     5.8 +
     5.9 +Live I/O automata -- specified by temproal formulas
    5.10 +
    5.11 +*) 
    5.12 +  
    5.13 +LiveIOA = IOA + TLS + 
    5.14 +
    5.15 +default term
    5.16 +
    5.17 +types
    5.18 +
    5.19 + ('a,'s)live_ioa       = "('a,'s)ioa * ('a,'s)ioa_temp"
    5.20 + 
    5.21 +consts
    5.22 +
    5.23 +validLIOA   :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool"
    5.24 +
    5.25 +WF         :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
    5.26 +SF         :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
    5.27 +
    5.28 +liveexecutions    :: "('a,'s)live_ioa => ('a,'s)execution set"
    5.29 +livetraces        :: "('a,'s)live_ioa => 'a trace set"
    5.30 +live_implements   :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
    5.31 +is_live_ref_map   :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
    5.32 +
    5.33 + 
    5.34 +defs
    5.35 +
    5.36 +validLIOA_def
    5.37 +  "validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)"
    5.38 +
    5.39 +
    5.40 +WF_def
    5.41 +  "WF A acts ==  <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
    5.42 +
    5.43 +SF_def
    5.44 +  "SF A acts ==  [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
    5.45 +
    5.46 +
    5.47 +liveexecutions_def
    5.48 +   "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
    5.49 +
    5.50 +livetraces_def
    5.51 +  "livetraces AP == {mk_trace (fst AP)`(snd ex) | ex. ex:liveexecutions AP}"
    5.52 +
    5.53 +live_implements_def
    5.54 +  "live_implements CL AM == (inp (fst CL) = inp (fst AM)) & 
    5.55 +                            (out (fst CL) = out (fst AM)) &
    5.56 +                            livetraces CL <= livetraces AM"
    5.57 +
    5.58 +is_live_ref_map_def
    5.59 +   "is_live_ref_map f CL AM ==  
    5.60 +            is_ref_map f (fst CL ) (fst AM) & 
    5.61 +            (! exec : executions (fst CL). (exec |== (snd CL)) --> 
    5.62 +                                           ((corresp_ex (fst AM) f exec) |== (snd AM)))"
    5.63 +
    5.64 +
    5.65 +end
    5.66 \ No newline at end of file
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Mon Jan 12 17:48:23 1998 +0100
     6.3 @@ -0,0 +1,72 @@
     6.4 +(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Olaf M"uller
     6.7 +    Copyright   1997  TU Muenchen
     6.8 +
     6.9 +Logical Connectives lifted to predicates.
    6.10 +
    6.11 +ToDo:
    6.12 +
    6.13 +<--> einfuehren.
    6.14 +
    6.15 +*)   
    6.16 +	       
    6.17 +Pred = Arith +  
    6.18 +
    6.19 +default term
    6.20 +
    6.21 +types
    6.22 +
    6.23 +'a predicate      = "'a => bool"
    6.24 +
    6.25 +consts
    6.26 +
    6.27 +satisfies    ::"'a  => 'a predicate => bool"    ("_ |= _" [100,9] 8)
    6.28 +valid        ::"'a predicate => bool"           (*  ("|-") *)         
    6.29 +
    6.30 +NOT          ::"'a predicate => 'a predicate"  (".~ _" [40] 40)
    6.31 +AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".&" 35)
    6.32 +OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".|" 30)
    6.33 +IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)
    6.34 +
    6.35 +
    6.36 +syntax ("" output)
    6.37 +  "NOT"     ::"'a predicate => 'a predicate" ("~ _" [40] 40)
    6.38 +  "AND"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "&" 35)
    6.39 +  "OR"      ::"'a predicate => 'a predicate => 'a predicate"    (infixr "|" 30)
    6.40 +  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "-->" 25)
    6.41 +
    6.42 +syntax (symbols output)
    6.43 +  "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
    6.44 +  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)
    6.45 +  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)
    6.46 +  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<midarrow>\\<rightarrow>" 25)
    6.47 +
    6.48 +syntax (symbols)
    6.49 +  "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)
    6.50 +
    6.51 +
    6.52 +defs
    6.53 +
    6.54 +satisfies_def
    6.55 +   "s |= P  == P s" 
    6.56 +
    6.57 +(* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)
    6.58 +valid_def
    6.59 +   "valid P == (! s. (s |= P))"
    6.60 +
    6.61 +
    6.62 +NOT_def
    6.63 +  "NOT P s ==  ~ (P s)"
    6.64 +
    6.65 +AND_def
    6.66 +  "(P .& Q) s == (P s) & (Q s)"
    6.67 +
    6.68 +
    6.69 +OR_def
    6.70 +  "(P .| Q) s ==  (P s) | (Q s)"
    6.71 +
    6.72 +IMPLIES_def
    6.73 +  "(P .--> Q) s == (P s) --> (Q s)"
    6.74 +
    6.75 +end
    6.76 \ No newline at end of file
     7.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Jan 12 17:26:34 1998 +0100
     7.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Jan 12 17:48:23 1998 +0100
     7.3 @@ -248,6 +248,97 @@
     7.4  qed"trace_inclusion"; 
     7.5  
     7.6  
     7.7 +(* -------------------------------------------------------------------------------- *)
     7.8 +
     7.9 +section "Corollary:  F A I R  T R A C E - I N C L U S I O N";
    7.10 +
    7.11 +(* -------------------------------------------------------------------------------- *)
    7.12 +
    7.13 +
    7.14 +goalw thy [fin_often_def] "(~inf_often P s) = fin_often P s";
    7.15 +auto();
    7.16 +qed"fininf";
    7.17 +
    7.18 +
    7.19 +goal thy 
    7.20 +"is_wfair A W (s,ex) = \
    7.21 +\ (fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)";
    7.22 +by (asm_full_simp_tac (simpset() addsimps [is_wfair_def,fin_often_def])1);
    7.23 +auto();
    7.24 +qed"WF_alt";
    7.25 +
    7.26 +goal thy  
    7.27 +"!! ex. [|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; \
    7.28 +\         en_persistent A W|] \
    7.29 +\   ==> inf_often (%x. fst x :W) ex";
    7.30 +bd persistent 1;
    7.31 +ba 1;
    7.32 +by (asm_full_simp_tac (simpset() addsimps [WF_alt])1);
    7.33 +auto();
    7.34 +qed"WF_persistent";
    7.35 +
    7.36 +
    7.37 +goal thy "!! C A. \
    7.38 +\         [| is_ref_map f C A; ext C = ext A; \
    7.39 +\         !! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |] \
    7.40 +\         ==> fairtraces C <= fairtraces A";
    7.41 +by (simp_tac (simpset() addsimps [fairtraces_def,
    7.42 +   fairexecutions_def]) 1);
    7.43 +by (safe_tac set_cs);
    7.44 +by (res_inst_tac[("x","corresp_ex A f ex")] exI 1);
    7.45 +by (safe_tac set_cs);
    7.46 +
    7.47 +  (* Traces coincide, Lemma 1 *)
    7.48 +  by (pair_tac "ex" 1);
    7.49 +  by (etac (lemma_1 RS spec RS mp) 1);
    7.50 +  by (REPEAT (atac 1));
    7.51 +  by (asm_full_simp_tac (simpset() addsimps [executions_def,reachable.reachable_0]) 1);
    7.52 + 
    7.53 +  (* corresp_ex is execution, Lemma 2 *)
    7.54 +  by (pair_tac "ex" 1);
    7.55 +  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
    7.56 +  (* start state *) 
    7.57 +  by (rtac conjI 1);
    7.58 +  by (asm_full_simp_tac (simpset() addsimps [is_ref_map_def,corresp_ex_def]) 1);
    7.59 +  (* is-execution-fragment *)
    7.60 +  by (etac (lemma_2 RS spec RS mp) 1);
    7.61 +  by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
    7.62 +
    7.63 + (* Fairness *)
    7.64 +auto();
    7.65 +qed"fair_trace_inclusion";
    7.66 +
    7.67 +goal thy "!! C A. \
    7.68 +\         [| inp(C) = inp(A); out(C)=out(A); \
    7.69 +\            is_fair_ref_map f C A |] \
    7.70 +\         ==> fair_implements C A";
    7.71 +by (asm_full_simp_tac (simpset() addsimps [is_fair_ref_map_def, fair_implements_def,
    7.72 +    fairtraces_def, fairexecutions_def]) 1);
    7.73 +by (safe_tac set_cs);
    7.74 +by (res_inst_tac[("x","corresp_ex A f ex")] exI 1);
    7.75 +by (safe_tac set_cs);
    7.76 +  (* Traces coincide, Lemma 1 *)
    7.77 +  by (pair_tac "ex" 1);
    7.78 +  by (etac (lemma_1 RS spec RS mp) 1);
    7.79 +  by (simp_tac (simpset() addsimps [externals_def])1);
    7.80 +  by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
    7.81 +  by (asm_full_simp_tac (simpset() addsimps [executions_def,reachable.reachable_0]) 1);
    7.82 + 
    7.83 +  (* corresp_ex is execution, Lemma 2 *)
    7.84 +  by (pair_tac "ex" 1);
    7.85 +  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
    7.86 +  (* start state *) 
    7.87 +  by (rtac conjI 1);
    7.88 +  by (asm_full_simp_tac (simpset() addsimps [is_ref_map_def,corresp_ex_def]) 1);
    7.89 +  (* is-execution-fragment *)
    7.90 +  by (etac (lemma_2 RS spec RS mp) 1);
    7.91 +  by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
    7.92 +
    7.93 + (* Fairness *)
    7.94 +auto();
    7.95 +qed"fair_trace_inclusion2";
    7.96  
    7.97  
    7.98  
    7.99 +
   7.100 +
     8.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Mon Jan 12 17:26:34 1998 +0100
     8.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Mon Jan 12 17:48:23 1998 +0100
     8.3 @@ -15,7 +15,7 @@
     8.4                    ('a,'s1)execution => ('a,'s2)execution"
     8.5    corresp_exC  ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
     8.6                     -> ('s1 => ('a,'s2)pairs)"
     8.7 -
     8.8 +  is_fair_ref_map  :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool"
     8.9  
    8.10  defs
    8.11  
    8.12 @@ -30,6 +30,40 @@
    8.13                                @@ ((h`xs) (snd pr)))
    8.14                          `x) )))"
    8.15   
    8.16 +is_fair_ref_map_def
    8.17 +  "is_fair_ref_map f C A == 
    8.18 +       is_ref_map f C A &
    8.19 +       (! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex))"
    8.20 +
    8.21  
    8.22  
    8.23 +rules
    8.24 +(* Axioms for fair trace inclusion proof support, not for the correctness proof
    8.25 +   of refeinment mappings ! *)
    8.26 +
    8.27 +corresp_laststate
    8.28 +  "Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))"
    8.29 +
    8.30 +corresp_Finite
    8.31 +  "Finite (snd (corresp_ex A f (s,ex))) = Finite ex"
    8.32 +
    8.33 +FromAtoC
    8.34 +  "fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex"
    8.35 +
    8.36 +FromCtoA
    8.37 +  "inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))"
    8.38 +
    8.39 +
    8.40 +(* Proof by case on inf W in ex: If so, ok. If not, only fin W in ex, ie there is
    8.41 +   an index i from which on no W in ex. But W inf enabled, ie at least once after i
    8.42 +   W is enabled. As W does not occur after i and W is enabling_persistent, W keeps
    8.43 +   enabled until infinity, ie. indefinitely *)
    8.44 +persistent
    8.45 +  "[|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W|]
    8.46 +   ==> inf_often (%x. fst x :W) ex | fin_often (%x. ~Enabled A W (snd x)) ex"
    8.47 +
    8.48 +infpostcond
    8.49 +  "[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|]
    8.50 +    ==> inf_often (% x. set_was_enabled A W (snd x)) ex"
    8.51 +
    8.52  end
    8.53 \ No newline at end of file
     9.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Jan 12 17:26:34 1998 +0100
     9.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Jan 12 17:48:23 1998 +0100
     9.3 @@ -8,33 +8,6 @@
     9.4  
     9.5  
     9.6  
     9.7 -(* ---------------------------------------------------------------------------- *)
     9.8 -                           section "laststate";
     9.9 -(* ---------------------------------------------------------------------------- *)
    9.10 -
    9.11 -goal thy "laststate (s,UU) = s";
    9.12 -by (simp_tac (simpset() addsimps [laststate_def]) 1); 
    9.13 -qed"laststate_UU";
    9.14 -
    9.15 -goal thy "laststate (s,nil) = s";
    9.16 -by (simp_tac (simpset() addsimps [laststate_def]) 1);
    9.17 -qed"laststate_nil";
    9.18 -
    9.19 -goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
    9.20 -by (simp_tac (simpset() addsimps [laststate_def]) 1);
    9.21 -by (case_tac "ex=nil" 1);
    9.22 -by (Asm_simp_tac 1);
    9.23 -by (Asm_simp_tac 1);
    9.24 -by (dtac (Finite_Last1 RS mp) 1);
    9.25 -by (assume_tac 1);
    9.26 -by (def_tac 1);
    9.27 -qed"laststate_cons";
    9.28 -
    9.29 -Addsimps [laststate_UU,laststate_nil,laststate_cons];
    9.30 -
    9.31 -goal thy "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)";
    9.32 -by (Seq_Finite_induct_tac 1);
    9.33 -qed"exists_laststate";
    9.34  
    9.35  
    9.36  (* ---------------------------------------------------------------------------- *)
    10.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Mon Jan 12 17:26:34 1998 +0100
    10.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Mon Jan 12 17:48:23 1998 +0100
    10.3 @@ -11,17 +11,14 @@
    10.4  default term
    10.5  
    10.6  consts
    10.7 -  laststate    ::"('a,'s)execution => 's"
    10.8 +
    10.9    move         ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool"
   10.10    is_ref_map   ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
   10.11    is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
   10.12   
   10.13 +
   10.14  defs
   10.15  
   10.16 -laststate_def
   10.17 -  "laststate ex == case Last`(snd ex) of
   10.18 -                      Undef  => fst ex
   10.19 -                    | Def at => snd at"
   10.20  
   10.21  move_def
   10.22    "move ioa ex s a t ==    
   10.23 @@ -45,4 +42,5 @@
   10.24                   then (f s) -a--A-> (f t)
   10.25                   else (f s)=(f t)))" 
   10.26  
   10.27 +
   10.28  end
    11.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Jan 12 17:26:34 1998 +0100
    11.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Jan 12 17:48:23 1998 +0100
    11.3 @@ -29,7 +29,7 @@
    11.4  
    11.5  syntax
    11.6  
    11.7 - "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_>>_)"  [66,65] 65)
    11.8 + "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_/>>_)"  [66,65] 65)
    11.9   (* list Enumeration *)
   11.10    "_totlist"      :: args => 'a Seq                          ("[(_)!]")
   11.11    "_partlist"     :: args => 'a Seq                          ("[(_)?]")
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOLCF/IOA/meta_theory/TL.ML	Mon Jan 12 17:48:23 1998 +0100
    12.3 @@ -0,0 +1,179 @@
    12.4 +(*  Title:      HOLCF/IOA/meta_theory/TL.ML
    12.5 +    ID:         $Id$
    12.6 +    Author:     Olaf M"uller
    12.7 +    Copyright   1997  TU Muenchen
    12.8 +
    12.9 +Temporal Logic 
   12.10 +*)   
   12.11 +
   12.12 +
   12.13 +goal thy "[] <> (.~ P) = (.~ <> [] P)";
   12.14 +br ext 1;
   12.15 +by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
   12.16 +auto();
   12.17 +qed"simple_try";
   12.18 +
   12.19 +goal thy "nil |= [] P";
   12.20 +by (asm_full_simp_tac (simpset() addsimps [satisfies_def,
   12.21 +     Box_def,tsuffix_def,suffix_def,nil_is_Conc])1);
   12.22 +qed"Boxnil";
   12.23 +
   12.24 +goal thy "~(nil |= <> P)";
   12.25 +by (simp_tac (simpset() addsimps [Diamond_def,satisfies_def,NOT_def])1);
   12.26 +by (cut_inst_tac [] Boxnil 1);
   12.27 +by (asm_full_simp_tac (simpset() addsimps [satisfies_def])1);
   12.28 +qed"Diamondnil";
   12.29 +
   12.30 +goal thy "(<> F) s = (? s2. tsuffix s2 s & F s2)";
   12.31 +by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
   12.32 +qed"Diamond_def2";
   12.33 +
   12.34 +
   12.35 +
   12.36 +section "TLA Axiomatization by Merz";
   12.37 +
   12.38 +(* ---------------------------------------------------------------- *)
   12.39 +(*                 TLA Axiomatization by Merz                       *)
   12.40 +(* ---------------------------------------------------------------- *)
   12.41 +
   12.42 +goal thy "suffix s s";
   12.43 +by (simp_tac (simpset() addsimps [suffix_def])1);
   12.44 +by (res_inst_tac [("x","nil")] exI 1);
   12.45 +auto();
   12.46 +qed"suffix_refl";
   12.47 +
   12.48 +goal thy "s~=UU & s~=nil --> (s |= [] F .--> F)";
   12.49 +by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def])1);
   12.50 +by (REPEAT (rtac impI 1));
   12.51 +by (eres_inst_tac [("x","s")] allE 1);
   12.52 +by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
   12.53 +qed"reflT";
   12.54 +
   12.55 +
   12.56 +goal thy "!!x. [| suffix y x ; suffix z y |]  ==> suffix z x";
   12.57 +by (asm_full_simp_tac (simpset() addsimps [suffix_def])1);
   12.58 +auto();
   12.59 +by (res_inst_tac [("x","s1 @@ s1a")] exI 1);
   12.60 +auto();
   12.61 +by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
   12.62 +qed"suffix_trans";
   12.63 +
   12.64 +goal thy "s |= [] F .--> [] [] F";
   12.65 +by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def,tsuffix_def])1);
   12.66 +auto();
   12.67 +bd suffix_trans 1;
   12.68 +ba 1;
   12.69 +by (eres_inst_tac [("x","s2a")] allE 1);
   12.70 +auto();
   12.71 +qed"transT";
   12.72 +
   12.73 +
   12.74 +goal thy "s |= [] (F .--> G) .--> [] F .--> [] G";
   12.75 +by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def])1);
   12.76 +qed"normalT";
   12.77 +
   12.78 +
   12.79 +(*
   12.80 +goal thy "s |= <> F .& <> G .--> (<> (F .& <> G) .| <> (G .& <> F))";
   12.81 +by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,AND_def,OR_def,Diamond_def2])1);
   12.82 +br impI 1;
   12.83 +be conjE 1;
   12.84 +be exE 1;
   12.85 +be exE 1;
   12.86 +
   12.87 +
   12.88 +br disjI1 1;
   12.89 +
   12.90 +goal thy "!!s. [| tsuffix s1 s ; tsuffix s2 s|] ==> tsuffix s2 s1 | tsuffix s1 s2";
   12.91 +by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
   12.92 +by (REPEAT (etac conjE 1));
   12.93 +by (REPEAT (etac exE 1));
   12.94 +by (REPEAT (etac conjE 1));
   12.95 +by (hyp_subst_tac 1);
   12.96 +
   12.97 +*)
   12.98 +
   12.99 +
  12.100 +section "TLA Rules by Lamport";
  12.101 +
  12.102 +(* ---------------------------------------------------------------- *)
  12.103 +(*                      TLA Rules by Lamport                        *)
  12.104 +(* ---------------------------------------------------------------- *)
  12.105 +
  12.106 +goal thy "!! P. validT P ==> validT ([] P)";
  12.107 +by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Box_def,tsuffix_def])1);
  12.108 +qed"STL1a";
  12.109 +
  12.110 +goal thy "!! P. valid P ==> validT (Init P)";
  12.111 +by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,Init_def])1);
  12.112 +qed"STL1b";
  12.113 +
  12.114 +goal thy "!! P. valid P ==> validT ([] (Init P))";
  12.115 +br STL1a 1;
  12.116 +be STL1b 1;
  12.117 +qed"STL1";
  12.118 +
  12.119 +(* Note that unlift and HD is not at all used !!! *)
  12.120 +goal thy "!! P. valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
  12.121 +by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
  12.122 +qed"STL4";
  12.123 +
  12.124 +
  12.125 +section "LTL Axioms by Manna/Pnueli";
  12.126 +
  12.127 +(* ---------------------------------------------------------------- *)
  12.128 +(*                LTL Axioms by Manna/Pnueli                        *)
  12.129 +(* ---------------------------------------------------------------- *)
  12.130 +
  12.131 +
  12.132 +goalw thy [tsuffix_def,suffix_def]
  12.133 +"s~=UU & s~=nil --> tsuffix s2 (TL`s) --> tsuffix s2 s";
  12.134 +auto();
  12.135 +by (Seq_case_simp_tac "s" 1);
  12.136 +by (res_inst_tac [("x","a>>s1")] exI 1);
  12.137 +auto();
  12.138 +qed_spec_mp"tsuffix_TL";
  12.139 +
  12.140 +val tsuffix_TL2 = conjI RS tsuffix_TL;
  12.141 +
  12.142 +
  12.143 +goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] 
  12.144 +   "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
  12.145 +auto();
  12.146 +(* []F .--> F *)
  12.147 +by (eres_inst_tac [("x","s")] allE 1);
  12.148 +by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
  12.149 +(* []F .--> Next [] F *)
  12.150 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
  12.151 +auto();
  12.152 +bd tsuffix_TL2 1;
  12.153 +by (REPEAT (atac 1));
  12.154 +auto();
  12.155 +qed"LTL1";
  12.156 +
  12.157 +
  12.158 +goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
  12.159 +    "s |= .~ (Next F) .--> (Next (.~ F))";
  12.160 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
  12.161 +qed"LTL2a";
  12.162 +
  12.163 +goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
  12.164 +    "s |= (Next (.~ F)) .--> (.~ (Next F))";
  12.165 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
  12.166 +qed"LTL2b";
  12.167 +
  12.168 +goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
  12.169 +"ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)";
  12.170 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
  12.171 +qed"LTL3";
  12.172 +
  12.173 +goalw thy [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] 
  12.174 + "s |= [] (F .--> Next F) .--> F .--> []F";
  12.175 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
  12.176 +auto();
  12.177 +
  12.178 +
  12.179 +by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
  12.180 +auto();
  12.181 +
  12.182 +
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Mon Jan 12 17:48:23 1998 +0100
    13.3 @@ -0,0 +1,81 @@
    13.4 +(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
    13.5 +    ID:         $Id$
    13.6 +    Author:     Olaf M"uller
    13.7 +    Copyright   1997  TU Muenchen
    13.8 +
    13.9 +A General Temporal Logic
   13.10 +
   13.11 +Version 2: Interface directly after Sequeces, i.e. predicates and predicate transformers are in HOL
   13.12 +
   13.13 +*)   
   13.14 +
   13.15 +
   13.16 +		       
   13.17 +TL = Pred + Sequence +  
   13.18 +
   13.19 +default term
   13.20 +
   13.21 +types
   13.22 +
   13.23 +'a temporal      = 'a Seq predicate
   13.24 +
   13.25 + 
   13.26 +consts
   13.27 +
   13.28 +
   13.29 +suffix     :: "'a Seq => 'a Seq => bool"
   13.30 +tsuffix    :: "'a Seq => 'a Seq => bool"
   13.31 +
   13.32 +validT     :: "'a Seq predicate => bool"
   13.33 +
   13.34 +unlift     ::  "'a lift => 'a"
   13.35 +
   13.36 +Init         ::"'a predicate => 'a temporal"          ("<_>" [0] 1000)
   13.37 +
   13.38 +Box          ::"'a temporal => 'a temporal"   ("[] (_)" [80] 80)
   13.39 +Diamond      ::"'a temporal => 'a temporal"   ("<> (_)" [80] 80)
   13.40 +Next         ::"'a temporal => 'a temporal"   
   13.41 +Leadsto      ::"'a temporal => 'a temporal => 'a temporal"  (infixr "~>" 22)
   13.42 +
   13.43 +syntax (symbols)
   13.44 +   "Box"        ::"'a temporal => 'a temporal"   ("\\<box> (_)" [80] 80)
   13.45 +   "Diamond"    ::"'a temporal => 'a temporal"   ("\\<diamond> (_)" [80] 80)
   13.46 +   "Leadsto"    ::"'a temporal => 'a temporal => 'a temporal"  (infixr "\\<leadsto>" 22)
   13.47 + 
   13.48 +defs
   13.49 +
   13.50 +
   13.51 +unlift_def
   13.52 +  "unlift x == (case x of 
   13.53 +                 Undef   => arbitrary
   13.54 +               | Def y   => y)"
   13.55 +
   13.56 +(* this means that for nil and UU the effect is unpredictable *)
   13.57 +Init_def
   13.58 +  "Init P s ==  (P (unlift (HD`s)))" 
   13.59 +
   13.60 +
   13.61 +(* FIX: Introduce nice symbol infix suntax *)
   13.62 +suffix_def
   13.63 +  "suffix s2 s == ? s1. (Finite s1  & s = s1 @@ s2)" 
   13.64 +
   13.65 +(* FIX: Introduce nice symbol infix suntax *)
   13.66 +tsuffix_def
   13.67 +  "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"
   13.68 +
   13.69 +Box_def
   13.70 +  "([] P) s == ! s2. tsuffix s2 s --> P s2"
   13.71 +
   13.72 +Next_def
   13.73 +  "(Next P) s == if TL`s=UU then (P s) else P (TL`s)"
   13.74 +
   13.75 +Diamond_def
   13.76 +  "<> P == .~ ([] (.~ P))"
   13.77 +
   13.78 +Leadsto_def
   13.79 +   "P ~> Q == ([] (P .--> (<> Q)))"  
   13.80 +
   13.81 +validT_def
   13.82 +  "validT P == ! s. s~=UU & s~=nil --> (s |= P)"
   13.83 +
   13.84 +end
   13.85 \ No newline at end of file
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Jan 12 17:48:23 1998 +0100
    14.3 @@ -0,0 +1,87 @@
    14.4 +(*  Title:      HOLCF/IOA/meta_theory/TLS.ML
    14.5 +    ID:         $Id$
    14.6 +    Author:     Olaf M"uller
    14.7 +    Copyright   1997  TU Muenchen
    14.8 +
    14.9 +Temporal Logic of Steps -- tailored for I/O automata
   14.10 +*)   
   14.11 +
   14.12 +
   14.13 +(* ---------------------------------------------------------------- *)
   14.14 +(*                                 ex2seqC                          *)
   14.15 +(* ---------------------------------------------------------------- *)
   14.16 +
   14.17 +goal thy "ex2seqC  = (LAM ex. (%s. case ex of \
   14.18 +\      nil =>  (s,None,s)>>nil   \
   14.19 +\    | x##xs => (flift1 (%pr. \
   14.20 +\                (s,Some (fst pr), snd pr)>> (ex2seqC`xs) (snd pr))  \
   14.21 +\                `x)  \
   14.22 +\      ))";
   14.23 +by (rtac trans 1);
   14.24 +by (rtac fix_eq2 1);
   14.25 +by (rtac ex2seqC_def 1);
   14.26 +by (rtac beta_cfun 1);
   14.27 +by (simp_tac (simpset() addsimps [flift1_def]) 1);
   14.28 +qed"ex2seqC_unfold";
   14.29 +
   14.30 +goal thy "(ex2seqC `UU) s=UU";
   14.31 +by (stac ex2seqC_unfold 1);
   14.32 +by (Simp_tac 1);
   14.33 +qed"ex2seqC_UU";
   14.34 +
   14.35 +goal thy "(ex2seqC `nil) s = (s,None,s)>>nil";
   14.36 +by (stac ex2seqC_unfold 1);
   14.37 +by (Simp_tac 1);
   14.38 +qed"ex2seqC_nil";
   14.39 +
   14.40 +goal thy "(ex2seqC `((a,t)>>xs)) s = \
   14.41 +\          (s,Some a,t)>> ((ex2seqC`xs) t)";
   14.42 +by (rtac trans 1);
   14.43 +by (stac ex2seqC_unfold 1);
   14.44 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
   14.45 +by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
   14.46 +qed"ex2seqC_cons";
   14.47 +
   14.48 +Addsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons];
   14.49 +
   14.50 +
   14.51 +goal thy "ex2seq (s, UU) = UU";
   14.52 +by (simp_tac (simpset() addsimps [ex2seq_def]) 1);
   14.53 +qed"ex2seq_UU";
   14.54 +
   14.55 +goal thy "ex2seq (s, nil) = (s,None,s)>>nil";
   14.56 +by (simp_tac (simpset() addsimps [ex2seq_def]) 1);
   14.57 +qed"ex2seq_nil";
   14.58 +
   14.59 +goal thy "ex2seq (s, (a,t)>>ex) = (s,Some a,t) >> ex2seq (t, ex)";
   14.60 +by (simp_tac (simpset() addsimps [ex2seq_def]) 1);
   14.61 +qed"ex2seq_cons";
   14.62 +
   14.63 +Delsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons]; 
   14.64 +Addsimps [ex2seq_UU,ex2seq_nil, ex2seq_cons];  
   14.65 +
   14.66 +
   14.67 +
   14.68 +(* FIX: Not true for UU, as ex2seq is defined continously !!!!! *)
   14.69 +goal thy "ex2seq exec ~= UU & ex2seq exec ~= nil";
   14.70 +
   14.71 +
   14.72 +goal thy "ex |== [] P .--> P";
   14.73 +
   14.74 +
   14.75 +(* ----------------------------------------------------------- *)
   14.76 +(*           Interface TL -- TLS                               *)
   14.77 +(* ---------------------------------------------------------- *)
   14.78 +
   14.79 +goalw thy [Init_def,Next_def,temp_sat_def,satisfies_def,IMPLIES_def,AND_def]
   14.80 + "!! s. (P s) & s-a--A-> t --> (Q t) \
   14.81 +\  ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) \
   14.82 +\             .--> (Next (Init (%(s,a,t).Q s))))";
   14.83 +
   14.84 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   14.85 +by (pair_tac "ex" 1);
   14.86 +by (Seq_case_simp_tac "y" 1);
   14.87 +
   14.88 +
   14.89 +
   14.90 +
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Mon Jan 12 17:48:23 1998 +0100
    15.3 @@ -0,0 +1,80 @@
    15.4 +(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
    15.5 +    ID:         $Id$
    15.6 +    Author:     Olaf M"uller
    15.7 +    Copyright   1997  TU Muenchen
    15.8 +
    15.9 +Temporal Logic of Steps -- tailored for I/O automata
   15.10 +*)   
   15.11 +
   15.12 +		       
   15.13 +TLS = IOA + TL + 
   15.14 +
   15.15 +default term
   15.16 +
   15.17 +types
   15.18 +
   15.19 + ('a,'s)ioa_temp       = "('a option,'s)transition temporal" 
   15.20 + ('a,'s)step_pred      = "('a option,'s)transition predicate"
   15.21 +  's state_pred        = "'s predicate"
   15.22 + 
   15.23 +consts
   15.24 +
   15.25 +
   15.26 +option_lift :: "('a => 'b) => 'b => ('a option => 'b)"
   15.27 +plift       :: "('a => bool) => ('a option => bool)"
   15.28 + 
   15.29 +temp_sat   :: "('a,'s)execution => ('a,'s)ioa_temp => bool"    (infixr "|==" 22)
   15.30 +xt1        :: "'s predicate => ('a,'s)step_pred"
   15.31 +xt2        :: "'a option predicate => ('a,'s)step_pred"
   15.32 +
   15.33 +validTE    :: "('a,'s)ioa_temp => bool"
   15.34 +validIOA   :: "('a,'s)ioa => ('a,'s)ioa_temp => bool"
   15.35 +
   15.36 +
   15.37 +ex2seq     :: "('a,'s)execution => ('a option,'s)transition Seq"
   15.38 +ex2seqC    :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" 
   15.39 +
   15.40 +
   15.41 +defs
   15.42 +
   15.43 +(* should be in Option as option_lift1, and option_map should be renamed to 
   15.44 +   option_lift2 *)
   15.45 +option_lift_def
   15.46 +  "option_lift f s y == case y of None => s | Some x => (f x)"
   15.47 +
   15.48 +(* plift is used to determine that None action is always false in 
   15.49 +   transition predicates *)
   15.50 +plift_def
   15.51 +  "plift P == option_lift P False"
   15.52 +
   15.53 +temp_sat_def
   15.54 +  "ex |== P == ((ex2seq ex) |= P)"
   15.55 +
   15.56 +xt1_def
   15.57 +  "xt1 P tr == P (fst tr)"
   15.58 +
   15.59 +xt2_def
   15.60 +  "xt2 P tr == P (fst (snd tr))"
   15.61 +
   15.62 +
   15.63 +(* FIX: Clarify type and Herkunft of a !! *)
   15.64 +ex2seq_def
   15.65 +  "ex2seq ex == ((ex2seqC `(snd ex)) (fst ex))"
   15.66 +
   15.67 +ex2seqC_def
   15.68 +  "ex2seqC == (fix`(LAM h ex. (%s. case ex of 
   15.69 +      nil =>  (s,None,s)>>nil
   15.70 +    | x##xs => (flift1 (%pr.
   15.71 +                (s,Some (fst pr), snd pr)>> (h`xs) (snd pr)) 
   15.72 +                `x)
   15.73 +      )))"
   15.74 +
   15.75 +validTE_def
   15.76 +  "validTE P == ! ex. (ex |== P)"
   15.77 +
   15.78 +validIOA_def
   15.79 +  "validIOA A P == ! ex : executions A . (ex |== P)"
   15.80 +
   15.81 +
   15.82 +end
   15.83 +
    16.1 --- a/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Jan 12 17:26:34 1998 +0100
    16.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Jan 12 17:48:23 1998 +0100
    16.3 @@ -123,6 +123,34 @@
    16.4  (* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *)
    16.5  Addsimps [is_exec_frag_UU,is_exec_frag_nil, is_exec_frag_cons];  
    16.6  
    16.7 +(* ---------------------------------------------------------------------------- *)
    16.8 +                           section "laststate";
    16.9 +(* ---------------------------------------------------------------------------- *)
   16.10 +
   16.11 +goal thy "laststate (s,UU) = s";
   16.12 +by (simp_tac (simpset() addsimps [laststate_def]) 1); 
   16.13 +qed"laststate_UU";
   16.14 +
   16.15 +goal thy "laststate (s,nil) = s";
   16.16 +by (simp_tac (simpset() addsimps [laststate_def]) 1);
   16.17 +qed"laststate_nil";
   16.18 +
   16.19 +goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
   16.20 +by (simp_tac (simpset() addsimps [laststate_def]) 1);
   16.21 +by (case_tac "ex=nil" 1);
   16.22 +by (Asm_simp_tac 1);
   16.23 +by (Asm_simp_tac 1);
   16.24 +by (dtac (Finite_Last1 RS mp) 1);
   16.25 +by (assume_tac 1);
   16.26 +by (def_tac 1);
   16.27 +qed"laststate_cons";
   16.28 +
   16.29 +Addsimps [laststate_UU,laststate_nil,laststate_cons];
   16.30 +
   16.31 +goal thy "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)";
   16.32 +by (Seq_Finite_induct_tac 1);
   16.33 +qed"exists_laststate";
   16.34 +
   16.35  
   16.36  (* -------------------------------------------------------------------------------- *)
   16.37  
    17.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Mon Jan 12 17:26:34 1998 +0100
    17.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Mon Jan 12 17:48:23 1998 +0100
    17.3 @@ -37,8 +37,29 @@
    17.4    traces        :: "('a,'s)ioa => 'a trace set"
    17.5    mk_trace      :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace"
    17.6  
    17.7 -  (* Notion of implementation *)
    17.8 +  laststate    ::"('a,'s)execution => 's"
    17.9 +
   17.10 +  (* A predicate holds infinitely (finitely) often in a sequence *)
   17.11 +
   17.12 +  inf_often      ::"('a => bool) => 'a Seq => bool"
   17.13 +  fin_often      ::"('a => bool) => 'a Seq => bool"
   17.14 +
   17.15 +  (* fairness of executions *)
   17.16 +
   17.17 +  wfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
   17.18 +  sfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
   17.19 +  is_wfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
   17.20 +  is_sfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
   17.21 +  fair_ex        ::"('a,'s)ioa => ('a,'s)execution => bool"
   17.22 +
   17.23 +  (* fair behavior sets *)
   17.24 + 
   17.25 +  fairexecutions ::"('a,'s)ioa => ('a,'s)execution set"
   17.26 +  fairtraces     ::"('a,'s)ioa => 'a trace set"
   17.27 +
   17.28 +  (* Notions of implementation *)
   17.29    "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool"   (infixr 12) 
   17.30 +  fair_implements  :: "('a,'s1)ioa => ('a,'s2)ioa => bool"
   17.31  
   17.32    (* Execution, schedule and trace modules *)
   17.33    Execs         ::  "('a,'s)ioa => ('a,'s)execution_module"
   17.34 @@ -97,7 +118,7 @@
   17.35  has_trace_def
   17.36    "has_trace ioa tr ==                                               
   17.37       (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))`sch)"
   17.38 -
   17.39 + 
   17.40  traces_def
   17.41    "traces ioa == {tr. has_trace ioa tr}"
   17.42  
   17.43 @@ -107,6 +128,53 @@
   17.44       Filter (%a. a:ext(ioa))`(filter_act`tr)"
   17.45  
   17.46  
   17.47 +(*  ------------------- Fair Traces ------------------------------ *)
   17.48 +
   17.49 +laststate_def
   17.50 +  "laststate ex == case Last`(snd ex) of
   17.51 +                      Undef  => fst ex
   17.52 +                    | Def at => snd at"
   17.53 +
   17.54 +inf_often_def
   17.55 +  "inf_often P s == Infinite (Filter P`s)"
   17.56 +
   17.57 +(*  filtering P yields a finite or partial sequence *)
   17.58 +fin_often_def
   17.59 +  "fin_often P s == ~inf_often P s"
   17.60 +
   17.61 +(* Note that partial execs cannot be wfair as the inf_often predicate in the 
   17.62 +   else branch prohibits it. However they can be sfair in the case when all W 
   17.63 +   are only finitely often enabled: FIX Is this the right model? *)
   17.64 +wfair_ex_def
   17.65 +  "wfair_ex A ex == ! W : wfair_of A.  
   17.66 +                      if   Finite (snd ex) 
   17.67 +                      then ~Enabled A W (laststate ex)
   17.68 +                      else is_wfair A W ex"
   17.69 +
   17.70 +is_wfair_def
   17.71 +  "is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex)
   17.72 +                     | inf_often (%x.~Enabled A W (snd x)) (snd ex))"
   17.73 +
   17.74 +sfair_ex_def
   17.75 +  "sfair_ex A ex == ! W : sfair_of A.
   17.76 +                      if   Finite (snd ex) 
   17.77 +                      then ~Enabled A W (laststate ex)
   17.78 +                      else is_sfair A W ex"
   17.79 +
   17.80 +is_sfair_def
   17.81 +  "is_sfair A W ex ==  (inf_often (%x. fst x:W) (snd ex)
   17.82 +                      | fin_often (%x. Enabled A W (snd x)) (snd ex))"
   17.83 +
   17.84 +fair_ex_def
   17.85 +  "fair_ex A ex == wfair_ex A ex & sfair_ex A ex"
   17.86 +
   17.87 +fairexecutions_def
   17.88 +  "fairexecutions A == {ex. ex:executions A & fair_ex A ex}"
   17.89 +
   17.90 +fairtraces_def
   17.91 +  "fairtraces A == {mk_trace A`(snd ex) | ex. ex:fairexecutions A}"
   17.92 +
   17.93 +
   17.94  (*  ------------------- Implementation ------------------------------ *)
   17.95  
   17.96  ioa_implements_def
   17.97 @@ -115,6 +183,10 @@
   17.98       (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) &
   17.99        traces(ioa1) <= traces(ioa2))"
  17.100  
  17.101 +fair_implements_def
  17.102 +  "fair_implements C A == inp(C) = inp(A) &  out(C)=out(A) &
  17.103 +                          fairtraces(C) <= fairtraces(A)"
  17.104 +
  17.105  (*  ------------------- Modules ------------------------------ *)
  17.106  
  17.107  Execs_def
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOLCF/IOA/meta_theory/TrivEx.ML	Mon Jan 12 17:48:23 1998 +0100
    18.3 @@ -0,0 +1,39 @@
    18.4 +(*  Title:      HOLCF/IOA/TrivEx.thy
    18.5 +    ID:         $Id$
    18.6 +    Author:     Olaf Mueller
    18.7 +    Copyright   1995  TU Muenchen
    18.8 +
    18.9 +Trivial Abstraction Example
   18.10 +*)
   18.11 +
   18.12 +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
   18.13 +  by(fast_tac (claset() addDs prems) 1);
   18.14 +qed "imp_conj_lemma";
   18.15 +
   18.16 +
   18.17 +goalw  thy [is_abstraction_def] 
   18.18 +"is_abstraction h_abs C_ioa A_ioa";
   18.19 +by (rtac conjI 1);
   18.20 +(* ------------- start states ------------ *)
   18.21 +by (simp_tac (simpset() addsimps 
   18.22 +    [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
   18.23 +(* -------------- step case ---------------- *)
   18.24 +by (REPEAT (rtac allI 1));
   18.25 +by (rtac imp_conj_lemma 1);
   18.26 +by (simp_tac (simpset() addsimps [trans_of_def,
   18.27 +        C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
   18.28 +by (simp_tac (simpset() addsimps [h_abs_def]) 1);
   18.29 +by (action.induct_tac "a" 1);
   18.30 +auto();
   18.31 +qed"h_abs_is_abstraction";
   18.32 +
   18.33 +
   18.34 +goal thy "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
   18.35 +br AbsRuleT1 1;
   18.36 +br h_abs_is_abstraction 1;
   18.37 +br MC_result 1;
   18.38 +by (abstraction_tac 1);
   18.39 +by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
   18.40 +qed"TrivEx_abstraction";
   18.41 +
   18.42 +
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOLCF/IOA/meta_theory/TrivEx.thy	Mon Jan 12 17:48:23 1998 +0100
    19.3 @@ -0,0 +1,61 @@
    19.4 +(*  Title:      HOLCF/IOA/TrivEx.thy
    19.5 +    ID:         $Id$
    19.6 +    Author:     Olaf Mueller
    19.7 +    Copyright   1995  TU Muenchen
    19.8 +
    19.9 +Trivial Abstraction Example
   19.10 +*)
   19.11 +
   19.12 +TrivEx = Abstraction + TLS + IOA +
   19.13 +
   19.14 +datatype action = INC
   19.15 +
   19.16 +consts
   19.17 +
   19.18 +C_asig   ::  action signature
   19.19 +C_trans  :: (action, nat)transition set
   19.20 +C_ioa    :: (action, nat)ioa
   19.21 +
   19.22 +A_asig   :: action signature
   19.23 +A_trans  :: (action, bool)transition set
   19.24 +A_ioa    :: (action, bool)ioa
   19.25 +
   19.26 +h_abs    :: "nat => bool"
   19.27 +
   19.28 +defs
   19.29 +
   19.30 +C_asig_def
   19.31 +  "C_asig == ({},{INC},{})"
   19.32 +
   19.33 +C_trans_def "C_trans ==                                           
   19.34 + {tr. let s = fst(tr);                                               
   19.35 +          t = snd(snd(tr))                                           
   19.36 +      in case fst(snd(tr))                                           
   19.37 +      of                                                             
   19.38 +      INC       => t = Suc(s)}"
   19.39 +
   19.40 +C_ioa_def "C_ioa == 
   19.41 + (C_asig, {0}, C_trans,{},{})"
   19.42 +
   19.43 +A_asig_def
   19.44 +  "A_asig == ({},{INC},{})"
   19.45 +
   19.46 +A_trans_def "A_trans ==                                           
   19.47 + {tr. let s = fst(tr);                                               
   19.48 +          t = snd(snd(tr))                                           
   19.49 +      in case fst(snd(tr))                                           
   19.50 +      of                                                             
   19.51 +      INC       => t = True}"
   19.52 +
   19.53 +A_ioa_def "A_ioa == 
   19.54 + (A_asig, {False}, A_trans,{},{})"
   19.55 +
   19.56 +h_abs_def
   19.57 +  "h_abs n == n~=0"
   19.58 +
   19.59 +rules
   19.60 +
   19.61 +MC_result
   19.62 +  "validIOA A_ioa (<>[] <%(b,a,c). b>)"
   19.63 +
   19.64 +end
   19.65 \ No newline at end of file
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Mon Jan 12 17:48:23 1998 +0100
    20.3 @@ -0,0 +1,66 @@
    20.4 +(*  Title:      HOLCF/IOA/TrivEx.thy
    20.5 +    ID:         $Id$
    20.6 +    Author:     Olaf Mueller
    20.7 +    Copyright   1995  TU Muenchen
    20.8 +
    20.9 +Trivial Abstraction Example
   20.10 +*)
   20.11 +
   20.12 +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
   20.13 +  by(fast_tac (claset() addDs prems) 1);
   20.14 +qed "imp_conj_lemma";
   20.15 +
   20.16 +
   20.17 +goalw  thy [is_abstraction_def] 
   20.18 +"is_abstraction h_abs C_ioa A_ioa";
   20.19 +by (rtac conjI 1);
   20.20 +(* ------------- start states ------------ *)
   20.21 +by (simp_tac (simpset() addsimps 
   20.22 +    [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
   20.23 +(* -------------- step case ---------------- *)
   20.24 +by (REPEAT (rtac allI 1));
   20.25 +by (rtac imp_conj_lemma 1);
   20.26 +by (simp_tac (simpset() addsimps [trans_of_def,
   20.27 +        C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
   20.28 +by (simp_tac (simpset() addsimps [h_abs_def]) 1);
   20.29 +by (action.induct_tac "a" 1);
   20.30 +auto();
   20.31 +qed"h_abs_is_abstraction";
   20.32 +
   20.33 +
   20.34 +(*
   20.35 +goalw thy [xt2_def,plift,option_lift]
   20.36 +  "(xt2 (plift afun)) (s,a,t) = (afun a)";
   20.37 +(* !!!!!!!!!!!!! Occurs check !!!! *)
   20.38 +by (option.induct_tac "a" 1);
   20.39 +
   20.40 +*)
   20.41 +
   20.42 +goalw thy [Enabled_def, enabled_def, h_abs_def,A_ioa_def,C_ioa_def,A_trans_def,
   20.43 +           C_trans_def,trans_of_def] 
   20.44 +"!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s";
   20.45 +auto();
   20.46 +qed"Enabled_implication";
   20.47 +
   20.48 +
   20.49 +goalw thy [is_live_abstraction_def]
   20.50 +"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})";
   20.51 +auto();
   20.52 +(* is_abstraction *)
   20.53 +br h_abs_is_abstraction 1;
   20.54 +(* temp_weakening *)
   20.55 +by (abstraction_tac 1);
   20.56 +be Enabled_implication 1;
   20.57 +qed"h_abs_is_liveabstraction";
   20.58 +
   20.59 +
   20.60 +goalw thy [C_live_ioa_def]
   20.61 +"validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";
   20.62 +br AbsRuleT2 1;
   20.63 +br h_abs_is_liveabstraction 1;
   20.64 +br MC_result 1;
   20.65 +by (abstraction_tac 1);
   20.66 +by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
   20.67 +qed"TrivEx2_abstraction";
   20.68 +
   20.69 +
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/HOLCF/IOA/meta_theory/TrivEx2.thy	Mon Jan 12 17:48:23 1998 +0100
    21.3 @@ -0,0 +1,71 @@
    21.4 +(*  Title:      HOLCF/IOA/TrivEx.thy
    21.5 +    ID:         $Id$
    21.6 +    Author:     Olaf Mueller
    21.7 +    Copyright   1995  TU Muenchen
    21.8 +
    21.9 +Trivial Abstraction Example with fairness
   21.10 +*)
   21.11 +
   21.12 +TrivEx2 = Abstraction + TLS + IOA +
   21.13 +
   21.14 +datatype action = INC
   21.15 +
   21.16 +consts
   21.17 +
   21.18 +C_asig   ::  action signature
   21.19 +C_trans  :: (action, nat)transition set
   21.20 +C_ioa    :: (action, nat)ioa
   21.21 +C_live_ioa :: (action, nat)live_ioa
   21.22 +
   21.23 +A_asig   :: action signature
   21.24 +A_trans  :: (action, bool)transition set
   21.25 +A_ioa    :: (action, bool)ioa
   21.26 +A_live_ioa :: (action, bool)live_ioa
   21.27 +
   21.28 +h_abs    :: "nat => bool"
   21.29 +
   21.30 +defs
   21.31 +
   21.32 +C_asig_def
   21.33 +  "C_asig == ({},{INC},{})"
   21.34 +
   21.35 +C_trans_def "C_trans ==                                           
   21.36 + {tr. let s = fst(tr);                                               
   21.37 +          t = snd(snd(tr))                                           
   21.38 +      in case fst(snd(tr))                                           
   21.39 +      of                                                             
   21.40 +      INC       => t = Suc(s)}"
   21.41 +
   21.42 +C_ioa_def "C_ioa == 
   21.43 + (C_asig, {0}, C_trans,{},{})"
   21.44 +
   21.45 +C_live_ioa_def 
   21.46 +  "C_live_ioa == (C_ioa, WF C_ioa {INC})"
   21.47 +
   21.48 +A_asig_def
   21.49 +  "A_asig == ({},{INC},{})"
   21.50 +
   21.51 +A_trans_def "A_trans ==                                           
   21.52 + {tr. let s = fst(tr);                                               
   21.53 +          t = snd(snd(tr))                                           
   21.54 +      in case fst(snd(tr))                                           
   21.55 +      of                                                             
   21.56 +      INC       => t = True}"
   21.57 +
   21.58 +A_ioa_def "A_ioa == 
   21.59 + (A_asig, {False}, A_trans,{},{})"
   21.60 +
   21.61 +A_live_ioa_def 
   21.62 +  "A_live_ioa == (A_ioa, WF A_ioa {INC})"
   21.63 +
   21.64 +
   21.65 +
   21.66 +h_abs_def
   21.67 +  "h_abs n == n~=0"
   21.68 +
   21.69 +rules
   21.70 +
   21.71 +MC_result
   21.72 +  "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
   21.73 +
   21.74 +end
   21.75 \ No newline at end of file