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