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