src/HOLCF/IOA/meta_theory/Abstraction.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 7499 23e090051cb8
child 12218 6597093b77e7
permissions -rw-r--r--
` -> $
     1 (*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
     2     ID:         $Id$
     3     Author:     Olaf M"uller
     4     Copyright   1997  TU Muenchen
     5 
     6 Abstraction Theory -- tailored for I/O automata
     7 *)   
     8 
     9 
    10 
    11 section "cex_abs";
    12 	
    13 
    14 (* ---------------------------------------------------------------- *)
    15 (*                             cex_abs                              *)
    16 (* ---------------------------------------------------------------- *)
    17 
    18 Goal "cex_abs f (s,UU) = (f s, UU)";
    19 by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
    20 qed"cex_abs_UU";
    21 
    22 Goal "cex_abs f (s,nil) = (f s, nil)";
    23 by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
    24 qed"cex_abs_nil";
    25 
    26 Goal "cex_abs f (s,(a,t)>>ex) = (f s, (a,f t) >> (snd (cex_abs f (t,ex))))";
    27 by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
    28 qed"cex_abs_cons";
    29 
    30 Addsimps [cex_abs_UU, cex_abs_nil, cex_abs_cons];
    31 
    32  
    33 
    34 section "lemmas";
    35 
    36 (* ---------------------------------------------------------------- *)
    37 (*                           Lemmas                                 *)
    38 (* ---------------------------------------------------------------- *)
    39 
    40 Goal "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))";
    41 by (simp_tac (simpset() addsimps [temp_weakening_def,temp_strengthening_def,
    42      NOT_def,temp_sat_def,satisfies_def]) 1);
    43 by Auto_tac;
    44 qed"temp_weakening_def2";
    45 
    46 Goal "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))";
    47 by (simp_tac (simpset() addsimps [state_weakening_def,state_strengthening_def,
    48      NOT_def]) 1);
    49 by Auto_tac;
    50 qed"state_weakening_def2";
    51 
    52 
    53 section "Abstraction Rules for Properties";
    54 
    55 (* ---------------------------------------------------------------- *)
    56 (*                Abstraction Rules for Properties                  *)
    57 (* ---------------------------------------------------------------- *)
    58 
    59 
    60 Goalw [cex_abs_def]
    61  "[| is_abstraction h C A |] ==>\
    62 \ !s. reachable C s & is_exec_frag C (s,xs) \
    63 \ --> is_exec_frag A (cex_abs h (s,xs))"; 
    64 
    65 by (Asm_full_simp_tac 1);
    66 by (pair_induct_tac "xs" [is_exec_frag_def] 1);
    67 (* main case *)
    68 by (safe_tac set_cs);
    69 by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def])1);
    70 by (forward_tac [reachable.reachable_n] 1);
    71 by (assume_tac 1);
    72 by (Asm_full_simp_tac 1);
    73 qed_spec_mp"exec_frag_abstraction";
    74 
    75 
    76 Goal "is_abstraction h C A ==> weakeningIOA A C h";
    77 by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1);
    78 by Auto_tac;
    79 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
    80 (* start state *) 
    81 by (rtac conjI 1);
    82 by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1);
    83 (* is-execution-fragment *)
    84 by (etac exec_frag_abstraction 1);
    85 by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
    86 qed"abs_is_weakening";
    87 
    88 
    89 Goal "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
    90 \         ==> validIOA C P";
    91 by (dtac abs_is_weakening 1);
    92 by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, 
    93     validIOA_def, temp_strengthening_def])1);
    94 by (safe_tac set_cs);
    95 by (pair_tac "ex" 1);
    96 qed"AbsRuleT1";
    97 
    98 
    99 (* FIX: Nach TLS.ML *)
   100 
   101 Goal "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))";
   102 by (simp_tac (simpset() addsimps [IMPLIES_def,temp_sat_def, satisfies_def])1);
   103 qed"IMPLIES_temp_sat";
   104 
   105 Goal "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))";
   106 by (simp_tac (simpset() addsimps [AND_def,temp_sat_def, satisfies_def])1);
   107 qed"AND_temp_sat";
   108 
   109 Goal "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))";
   110 by (simp_tac (simpset() addsimps [OR_def,temp_sat_def, satisfies_def])1);
   111 qed"OR_temp_sat";
   112 
   113 Goal "(ex |== .~ P) = (~ (ex |== P))";
   114 by (simp_tac (simpset() addsimps [NOT_def,temp_sat_def, satisfies_def])1);
   115 qed"NOT_temp_sat";
   116 
   117 Addsimps [IMPLIES_temp_sat,AND_temp_sat,OR_temp_sat,NOT_temp_sat];
   118 
   119 
   120 Goalw [is_live_abstraction_def]
   121    "[|is_live_abstraction h (C,L) (A,M); \
   122 \         validLIOA (A,M) Q;  temp_strengthening Q P h |] \
   123 \         ==> validLIOA (C,L) P";
   124 by Auto_tac;
   125 by (dtac abs_is_weakening 1);
   126 by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
   127     validLIOA_def, validIOA_def, temp_strengthening_def])1);
   128 by (safe_tac set_cs);
   129 by (pair_tac "ex" 1);
   130 qed"AbsRuleT2";
   131 
   132 
   133 Goalw [is_live_abstraction_def]
   134    "[|is_live_abstraction h (C,L) (A,M); \
   135 \         validLIOA (A,M) (H1 .--> Q);  temp_strengthening Q P h; \
   136 \         temp_weakening H1 H2 h; validLIOA (C,L) H2 |] \
   137 \         ==> validLIOA (C,L) P";
   138 by Auto_tac;
   139 by (dtac abs_is_weakening 1);
   140 by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
   141     validLIOA_def, validIOA_def, temp_strengthening_def])1);
   142 by (safe_tac set_cs);
   143 by (pair_tac "ex" 1);
   144 qed"AbsRuleTImprove";
   145 
   146 
   147 section "Correctness of safe abstraction";
   148 
   149 (* ---------------------------------------------------------------- *)
   150 (*              Correctness of safe abstraction                     *)
   151 (* ---------------------------------------------------------------- *)
   152 
   153 
   154 Goalw [is_abstraction_def,is_ref_map_def] 
   155 "is_abstraction h C A ==> is_ref_map h C A";
   156 by (safe_tac set_cs);
   157 by (res_inst_tac[("x","(a,h t)>>nil")] exI 1);
   158 by (asm_full_simp_tac (simpset() addsimps [move_def])1);
   159 qed"abstraction_is_ref_map";
   160 
   161 
   162 Goal "[| inp(C)=inp(A); out(C)=out(A); \
   163 \                  is_abstraction h C A |] \
   164 \               ==> C =<| A";
   165 by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1);
   166 by (rtac trace_inclusion 1);
   167 by (simp_tac (simpset() addsimps [externals_def])1);
   168 by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
   169 by (etac abstraction_is_ref_map 1);
   170 qed"abs_safety";
   171 
   172 
   173 section "Correctness of life abstraction";
   174 
   175 (* ---------------------------------------------------------------- *)
   176 (*              Correctness of life abstraction                     *)
   177 (* ---------------------------------------------------------------- *)
   178 
   179 
   180 (* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x),
   181    that is to special Map Lemma *)
   182 Goalw [cex_abs_def,mk_trace_def,filter_act_def]
   183   "ext C = ext A \
   184 \        ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))";
   185 by (Asm_full_simp_tac 1);
   186 by (pair_induct_tac "xs" [] 1);
   187 qed"traces_coincide_abs";
   188 
   189 
   190 (* Does not work with abstraction_is_ref_map as proof of abs_safety, because
   191    is_live_abstraction includes temp_strengthening which is necessarily based
   192    on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific
   193    way for cex_abs *)
   194 Goal "[| inp(C)=inp(A); out(C)=out(A); \
   195 \                  is_live_abstraction h (C,M) (A,L) |] \
   196 \               ==> live_implements (C,M) (A,L)";
   197 
   198 by (asm_full_simp_tac (simpset() addsimps [is_live_abstraction_def, live_implements_def,
   199 livetraces_def,liveexecutions_def]) 1);
   200 by (safe_tac set_cs);
   201 by (res_inst_tac[("x","cex_abs h ex")] exI 1);
   202 by (safe_tac set_cs);
   203   (* Traces coincide *)
   204   by (pair_tac "ex" 1);
   205   by (rtac traces_coincide_abs 1);
   206   by (simp_tac (simpset() addsimps [externals_def])1);
   207   by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
   208  
   209   (* cex_abs is execution *)
   210   by (pair_tac "ex" 1);
   211   by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   212   (* start state *) 
   213   by (rtac conjI 1);
   214   by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1);
   215   (* is-execution-fragment *)
   216   by (etac exec_frag_abstraction 1);
   217   by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
   218 
   219  (* Liveness *) 
   220 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2]) 1);
   221  by (pair_tac "ex" 1);
   222 qed"abs_liveness";
   223 
   224 (* FIX: NAch Traces.ML bringen *)
   225 
   226 Goalw [ioa_implements_def] 
   227 "[| A =<| B; B =<| C|] ==> A =<| C"; 
   228 by Auto_tac;
   229 qed"implements_trans";
   230 
   231 
   232 section "Abstraction Rules for Automata";
   233 
   234 (* ---------------------------------------------------------------- *)
   235 (*                Abstraction Rules for Automata                    *)
   236 (* ---------------------------------------------------------------- *)
   237 
   238 Goal "[| inp(C)=inp(A); out(C)=out(A); \
   239 \                  inp(Q)=inp(P); out(Q)=out(P); \
   240 \                  is_abstraction h1 C A; \
   241 \                  A =<| Q ; \
   242 \                  is_abstraction h2 Q P |] \
   243 \               ==> C =<| P";   
   244 by (dtac abs_safety 1);
   245 by (REPEAT (atac 1));
   246 by (dtac abs_safety 1);
   247 by (REPEAT (atac 1));
   248 by (etac implements_trans 1);
   249 by (etac implements_trans 1);
   250 by (assume_tac 1);
   251 qed"AbsRuleA1";
   252 
   253 
   254 Goal "[| inp(C)=inp(A); out(C)=out(A); \
   255 \                  inp(Q)=inp(P); out(Q)=out(P); \
   256 \                  is_live_abstraction h1 (C,LC) (A,LA); \
   257 \                  live_implements (A,LA) (Q,LQ) ; \
   258 \                  is_live_abstraction h2 (Q,LQ) (P,LP) |] \
   259 \               ==> live_implements (C,LC) (P,LP)";   
   260 by (dtac abs_liveness 1);
   261 by (REPEAT (atac 1));
   262 by (dtac abs_liveness 1);
   263 by (REPEAT (atac 1));
   264 by (etac live_implements_trans 1);
   265 by (etac live_implements_trans 1);
   266 by (assume_tac 1);
   267 qed"AbsRuleA2";
   268 
   269 
   270 Delsimps [split_paired_All];
   271 
   272 
   273 section "Localizing Temporal Strengthenings and Weakenings";
   274 
   275 (* ---------------------------------------------------------------- *)
   276 (*                Localizing Temproal Strengthenings - 1               *)
   277 (* ---------------------------------------------------------------- *)
   278 
   279 Goalw [temp_strengthening_def]
   280 "[| temp_strengthening P1 Q1 h; \
   281 \         temp_strengthening P2 Q2 h |] \
   282 \      ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h";
   283 by Auto_tac;
   284 qed"strength_AND";
   285 
   286 Goalw [temp_strengthening_def]
   287 "[| temp_strengthening P1 Q1 h; \
   288 \         temp_strengthening P2 Q2 h |] \
   289 \      ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h";
   290 by Auto_tac;
   291 qed"strength_OR";
   292 
   293 Goalw [temp_strengthening_def]
   294 "[| temp_weakening P Q h |] \
   295 \      ==> temp_strengthening (.~ P) (.~ Q) h";
   296 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   297 by Auto_tac;
   298 qed"strength_NOT";
   299 
   300 Goalw [temp_strengthening_def]
   301 "[| temp_weakening P1 Q1 h; \
   302 \         temp_strengthening P2 Q2 h |] \
   303 \      ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h";
   304 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   305 qed"strength_IMPLIES";
   306 
   307 
   308 
   309 (* ---------------------------------------------------------------- *)
   310 (*                Localizing Temproal Weakenings - Part 1           *)
   311 (* ---------------------------------------------------------------- *)
   312 
   313 Goal
   314 "[| temp_weakening P1 Q1 h; \
   315 \         temp_weakening P2 Q2 h |] \
   316 \      ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h";
   317 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   318 qed"weak_AND";
   319 
   320 Goal 
   321 "[| temp_weakening P1 Q1 h; \
   322 \         temp_weakening P2 Q2 h |] \
   323 \      ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h";
   324 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   325 qed"weak_OR";
   326 
   327 Goalw [temp_strengthening_def]
   328 "[| temp_strengthening P Q h |] \
   329 \      ==> temp_weakening (.~ P) (.~ Q) h";
   330 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   331 by Auto_tac;
   332 qed"weak_NOT";
   333 
   334 Goalw [temp_strengthening_def]
   335 "[| temp_strengthening P1 Q1 h; \
   336 \         temp_weakening P2 Q2 h |] \
   337 \      ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h";
   338 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   339 qed"weak_IMPLIES";
   340 
   341 
   342 (* ---------------------------------------------------------------- *)
   343 (*             Localizing Temproal Strengthenings - 2               *)
   344 (* ---------------------------------------------------------------- *)
   345 
   346 
   347 (* ------------------ Box ----------------------------*)
   348 
   349 (* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
   350 Goal "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))";
   351 by (Seq_case_simp_tac "x" 1);
   352 by Auto_tac;
   353 qed"UU_is_Conc";
   354 
   355 Goal 
   356 "Finite s1 --> \
   357 \ (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))";
   358 by (rtac impI 1);
   359 by (Seq_Finite_induct_tac 1);
   360 by (Blast_tac 1);
   361 (* main case *)
   362 by (clarify_tac set_cs 1);
   363 by (pair_tac "ex" 1);
   364 by (Seq_case_simp_tac "y" 1);
   365 (* UU case *)
   366 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1);
   367 (* nil case *)
   368 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1);
   369 (* cons case *)
   370 by (pair_tac "aa" 1);
   371 by Auto_tac;
   372 qed_spec_mp"ex2seqConc";
   373 
   374 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
   375 
   376 Goalw [tsuffix_def,suffix_def]
   377 "tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
   378 by Auto_tac;
   379 by (dtac ex2seqConc 1);
   380 by Auto_tac;
   381 qed"ex2seq_tsuffix";
   382 
   383 
   384 (* FIX: NAch Sequence.ML bringen *)
   385 
   386 Goal "(Map f$s = nil) = (s=nil)";
   387 by (Seq_case_simp_tac "s" 1);
   388 qed"Mapnil";
   389 
   390 Goal "(Map f$s = UU) = (s=UU)";
   391 by (Seq_case_simp_tac "s" 1);
   392 qed"MapUU";
   393 
   394 
   395 (* important property of cex_absSeq: As it is a 1to1 correspondence, 
   396   properties carry over *)
   397 
   398 Goalw [tsuffix_def,suffix_def,cex_absSeq_def]
   399 "tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
   400 by Auto_tac;
   401 by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
   402 by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
   403 by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))$s1")] exI 1);
   404 by (asm_full_simp_tac (simpset() addsimps [Map2Finite,MapConc])1);
   405 qed"cex_absSeq_tsuffix";
   406 
   407 
   408 Goalw [temp_strengthening_def,state_strengthening_def, temp_sat_def,
   409 satisfies_def,Box_def]
   410 "[| temp_strengthening P Q h |]\
   411 \      ==> temp_strengthening ([] P) ([] Q) h";
   412 by (clarify_tac set_cs 1);
   413 by (ftac ex2seq_tsuffix 1);
   414 by (clarify_tac set_cs 1);
   415 by (dres_inst_tac [("h","h")] cex_absSeq_tsuffix 1);
   416 by (asm_full_simp_tac (simpset() addsimps [ex2seq_abs_cex])1);
   417 qed"strength_Box";
   418 
   419 
   420 (* ------------------ Init ----------------------------*)
   421 
   422 Goalw [temp_strengthening_def,state_strengthening_def,
   423 temp_sat_def,satisfies_def,Init_def,unlift_def]
   424 "[| state_strengthening P Q h |]\
   425 \      ==> temp_strengthening (Init P) (Init Q) h";
   426 by (safe_tac set_cs);
   427 by (pair_tac "ex" 1);
   428 by (Seq_case_simp_tac "y" 1);
   429 by (pair_tac "a" 1);
   430 qed"strength_Init";
   431 
   432 
   433 (* ------------------ Next ----------------------------*)
   434 
   435 Goal 
   436 "(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)";
   437 by (pair_tac "ex" 1);
   438 by (Seq_case_simp_tac "y" 1);
   439 by (pair_tac "a" 1);
   440 by (Seq_case_simp_tac "s" 1);
   441 by (pair_tac "a" 1);
   442 qed"TL_ex2seq_UU";
   443 
   444 Goal 
   445 "(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)";
   446 by (pair_tac "ex" 1);
   447 by (Seq_case_simp_tac "y" 1);
   448 by (pair_tac "a" 1);
   449 by (Seq_case_simp_tac "s" 1);
   450 by (pair_tac "a" 1);
   451 qed"TL_ex2seq_nil";
   452 
   453 (* FIX: put to Sequence Lemmas *)
   454 Goal "Map f$(TL$s) = TL$(Map f$s)";
   455 by (Seq_induct_tac "s" [] 1);
   456 qed"MapTL";
   457 
   458 (* important property of cex_absSeq: As it is a 1to1 correspondence, 
   459   properties carry over *)
   460 
   461 Goalw [cex_absSeq_def]
   462 "cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))";
   463 by (simp_tac (simpset() addsimps [MapTL]) 1);
   464 qed"cex_absSeq_TL";
   465 
   466 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
   467 
   468 Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')";
   469 by (pair_tac "ex" 1);
   470 by (Seq_case_simp_tac "y" 1);
   471 by (pair_tac "a" 1);
   472 by Auto_tac;
   473 qed"TLex2seq";
   474 
   475  
   476 Goal "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)";
   477 by (pair_tac "ex" 1);
   478 by (Seq_case_simp_tac "y" 1);
   479 by (pair_tac "a" 1);
   480 by (Seq_case_simp_tac "s" 1);
   481 by (pair_tac "a" 1);
   482 qed"ex2seqnilTL";
   483 
   484 
   485 Goalw [temp_strengthening_def,state_strengthening_def,
   486 temp_sat_def, satisfies_def,Next_def]
   487 "[| temp_strengthening P Q h |]\
   488 \      ==> temp_strengthening (Next P) (Next Q) h";
   489 by (Asm_full_simp_tac 1);
   490 by (safe_tac set_cs);
   491 by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
   492 by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
   493 by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
   494 by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
   495 (* cons case *)
   496 by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
   497         ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqnilTL])1);
   498 by (etac conjE 1);
   499 by (dtac TLex2seq 1);
   500 by (assume_tac 1);
   501 by Auto_tac;
   502 qed"strength_Next";
   503 
   504 
   505 
   506 (* ---------------------------------------------------------------- *)
   507 (*             Localizing Temporal Weakenings     - 2               *)
   508 (* ---------------------------------------------------------------- *)
   509 
   510 
   511 Goal 
   512 "[| state_weakening P Q h |]\
   513 \      ==> temp_weakening (Init P) (Init Q) h";
   514 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
   515       state_weakening_def2, temp_sat_def,satisfies_def,Init_def,unlift_def])1);
   516 by (safe_tac set_cs);
   517 by (pair_tac "ex" 1);
   518 by (Seq_case_simp_tac "y" 1);
   519 by (pair_tac "a" 1);
   520 qed"weak_Init";
   521 
   522 
   523 (* ---------------------------------------------------------------- *)
   524 (*             Localizing Temproal Strengthenings - 3               *)
   525 (* ---------------------------------------------------------------- *)
   526 
   527 
   528 Goalw [Diamond_def]
   529 "[| temp_strengthening P Q h |]\
   530 \      ==> temp_strengthening (<> P) (<> Q) h";
   531 by (rtac strength_NOT 1);
   532 by (rtac weak_Box 1);
   533 by (etac weak_NOT 1);
   534 qed"strength_Diamond";
   535 
   536 Goalw [Leadsto_def]
   537 "[| temp_weakening P1 P2 h;\
   538 \         temp_strengthening Q1 Q2 h |]\
   539 \      ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h";
   540 by (rtac strength_Box 1);
   541 by (etac strength_IMPLIES 1);
   542 by (etac strength_Diamond 1);
   543 qed"strength_Leadsto";
   544 
   545 
   546 (* ---------------------------------------------------------------- *)
   547 (*             Localizing Temporal Weakenings - 3                   *)
   548 (* ---------------------------------------------------------------- *)
   549 
   550 
   551 Goalw [Diamond_def]
   552 "[| temp_weakening P Q h |]\
   553 \      ==> temp_weakening (<> P) (<> Q) h";
   554 by (rtac weak_NOT 1);
   555 by (rtac strength_Box 1);
   556 by (etac strength_NOT 1);
   557 qed"weak_Diamond";
   558 
   559 Goalw [Leadsto_def]
   560 "[| temp_strengthening P1 P2 h;\
   561 \         temp_weakening Q1 Q2 h |]\
   562 \      ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h";
   563 by (rtac weak_Box 1);
   564 by (etac weak_IMPLIES 1);
   565 by (etac weak_Diamond 1);
   566 qed"weak_Leadsto";
   567 
   568 Goalw [WF_def]
   569   " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ 
   570 \   ==> temp_weakening (WF A acts) (WF C acts) h";
   571 by (rtac weak_IMPLIES 1);
   572 by (rtac strength_Diamond 1);
   573 by (rtac strength_Box 1);
   574 by (rtac strength_Init 1);
   575 by (rtac weak_Box 2);
   576 by (rtac weak_Diamond 2);
   577 by (rtac weak_Init 2);
   578 by (auto_tac (claset(),
   579               simpset() addsimps [state_weakening_def,state_strengthening_def,
   580                              xt2_def,plift_def,option_lift_def,NOT_def]));
   581 qed"weak_WF";
   582 
   583 Goalw [SF_def]
   584   " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ 
   585 \   ==> temp_weakening (SF A acts) (SF C acts) h";
   586 by (rtac weak_IMPLIES 1);
   587 by (rtac strength_Box 1);
   588 by (rtac strength_Diamond 1);
   589 by (rtac strength_Init 1);
   590 by (rtac weak_Box 2);
   591 by (rtac weak_Diamond 2);
   592 by (rtac weak_Init 2);
   593 by (auto_tac (claset(),
   594               simpset() addsimps [state_weakening_def,state_strengthening_def,
   595                              xt2_def,plift_def,option_lift_def,NOT_def]));
   596 qed"weak_SF";
   597 
   598 
   599 val weak_strength_lemmas = 
   600     [weak_OR,weak_AND,weak_NOT,weak_IMPLIES,weak_Box,weak_Next,weak_Init,
   601      weak_Diamond,weak_Leadsto,strength_OR,strength_AND,strength_NOT,
   602      strength_IMPLIES,strength_Box,strength_Next,strength_Init,
   603      strength_Diamond,strength_Leadsto,weak_WF,weak_SF];
   604 
   605 fun abstraction_tac i = 
   606     SELECT_GOAL (auto_tac (claset() addSIs weak_strength_lemmas,
   607                            simpset() addsimps [state_strengthening_def,state_weakening_def])) i;