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