src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
changeset 40774 0437dbc127b3
parent 37785 173667d73115
child 40945 b8703f63bfb2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,615 @@
     1.4 +(*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
     1.5 +    Author:     Olaf Müller
     1.6 +*)
     1.7 +
     1.8 +header {* Abstraction Theory -- tailored for I/O automata *}
     1.9 +
    1.10 +theory Abstraction
    1.11 +imports LiveIOA
    1.12 +begin
    1.13 +
    1.14 +default_sort type
    1.15 +
    1.16 +definition
    1.17 +  cex_abs :: "('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" where
    1.18 +  "cex_abs f ex = (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))"
    1.19 +definition
    1.20 +  -- {* equals cex_abs on Sequences -- after ex2seq application *}
    1.21 +  cex_absSeq :: "('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq" where
    1.22 +  "cex_absSeq f = (%s. Map (%(s,a,t). (f s,a,f t))$s)"
    1.23 +
    1.24 +definition
    1.25 +  is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
    1.26 +  "is_abstraction f C A =
    1.27 +   ((!s:starts_of(C). f(s):starts_of(A)) &
    1.28 +   (!s t a. reachable C s & s -a--C-> t
    1.29 +            --> (f s) -a--A-> (f t)))"
    1.30 +
    1.31 +definition
    1.32 +  weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" where
    1.33 +  "weakeningIOA A C h = (!ex. ex : executions C --> cex_abs h ex : executions A)"
    1.34 +definition
    1.35 +  temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where
    1.36 +  "temp_strengthening Q P h = (!ex. (cex_abs h ex |== Q) --> (ex |== P))"
    1.37 +definition
    1.38 +  temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where
    1.39 +  "temp_weakening Q P h = temp_strengthening (.~ Q) (.~ P) h"
    1.40 +
    1.41 +definition
    1.42 +  state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where
    1.43 +  "state_strengthening Q P h = (!s t a.  Q (h(s),a,h(t)) --> P (s,a,t))"
    1.44 +definition
    1.45 +  state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where
    1.46 +  "state_weakening Q P h = state_strengthening (.~Q) (.~P) h"
    1.47 +
    1.48 +definition
    1.49 +  is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
    1.50 +  "is_live_abstraction h CL AM =
    1.51 +     (is_abstraction h (fst CL) (fst AM) &
    1.52 +      temp_weakening (snd AM) (snd CL) h)"
    1.53 +
    1.54 +
    1.55 +axiomatization where
    1.56 +(* thm about ex2seq which is not provable by induction as ex2seq is not continous *)
    1.57 +ex2seq_abs_cex:
    1.58 +  "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)"
    1.59 +
    1.60 +axiomatization where
    1.61 +(* analog to the proved thm strength_Box - proof skipped as trivial *)
    1.62 +weak_Box:
    1.63 +"temp_weakening P Q h
    1.64 + ==> temp_weakening ([] P) ([] Q) h"
    1.65 +
    1.66 +axiomatization where
    1.67 +(* analog to the proved thm strength_Next - proof skipped as trivial *)
    1.68 +weak_Next:
    1.69 +"temp_weakening P Q h
    1.70 + ==> temp_weakening (Next P) (Next Q) h"
    1.71 +
    1.72 +
    1.73 +subsection "cex_abs"
    1.74 +
    1.75 +lemma cex_abs_UU: "cex_abs f (s,UU) = (f s, UU)"
    1.76 +  by (simp add: cex_abs_def)
    1.77 +
    1.78 +lemma cex_abs_nil: "cex_abs f (s,nil) = (f s, nil)"
    1.79 +  by (simp add: cex_abs_def)
    1.80 +
    1.81 +lemma cex_abs_cons: "cex_abs f (s,(a,t)>>ex) = (f s, (a,f t) >> (snd (cex_abs f (t,ex))))"
    1.82 +  by (simp add: cex_abs_def)
    1.83 +
    1.84 +declare cex_abs_UU [simp] cex_abs_nil [simp] cex_abs_cons [simp]
    1.85 +
    1.86 +
    1.87 +subsection "lemmas"
    1.88 +
    1.89 +lemma temp_weakening_def2: "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))"
    1.90 +  apply (simp add: temp_weakening_def temp_strengthening_def NOT_def temp_sat_def satisfies_def)
    1.91 +  apply auto
    1.92 +  done
    1.93 +
    1.94 +lemma state_weakening_def2: "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))"
    1.95 +  apply (simp add: state_weakening_def state_strengthening_def NOT_def)
    1.96 +  apply auto
    1.97 +  done
    1.98 +
    1.99 +
   1.100 +subsection "Abstraction Rules for Properties"
   1.101 +
   1.102 +lemma exec_frag_abstraction [rule_format]:
   1.103 + "[| is_abstraction h C A |] ==>
   1.104 +  !s. reachable C s & is_exec_frag C (s,xs)
   1.105 +  --> is_exec_frag A (cex_abs h (s,xs))"
   1.106 +apply (unfold cex_abs_def)
   1.107 +apply simp
   1.108 +apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
   1.109 +txt {* main case *}
   1.110 +apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
   1.111 +done
   1.112 +
   1.113 +
   1.114 +lemma abs_is_weakening: "is_abstraction h C A ==> weakeningIOA A C h"
   1.115 +apply (simp add: weakeningIOA_def)
   1.116 +apply auto
   1.117 +apply (simp add: executions_def)
   1.118 +txt {* start state *}
   1.119 +apply (rule conjI)
   1.120 +apply (simp add: is_abstraction_def cex_abs_def)
   1.121 +txt {* is-execution-fragment *}
   1.122 +apply (erule exec_frag_abstraction)
   1.123 +apply (simp add: reachable.reachable_0)
   1.124 +done
   1.125 +
   1.126 +
   1.127 +lemma AbsRuleT1: "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |]
   1.128 +          ==> validIOA C P"
   1.129 +apply (drule abs_is_weakening)
   1.130 +apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def)
   1.131 +apply (auto simp add: split_paired_all)
   1.132 +done
   1.133 +
   1.134 +
   1.135 +(* FIX: Nach TLS.ML *)
   1.136 +
   1.137 +lemma IMPLIES_temp_sat: "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))"
   1.138 +  by (simp add: IMPLIES_def temp_sat_def satisfies_def)
   1.139 +
   1.140 +lemma AND_temp_sat: "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))"
   1.141 +  by (simp add: AND_def temp_sat_def satisfies_def)
   1.142 +
   1.143 +lemma OR_temp_sat: "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))"
   1.144 +  by (simp add: OR_def temp_sat_def satisfies_def)
   1.145 +
   1.146 +lemma NOT_temp_sat: "(ex |== .~ P) = (~ (ex |== P))"
   1.147 +  by (simp add: NOT_def temp_sat_def satisfies_def)
   1.148 +
   1.149 +declare IMPLIES_temp_sat [simp] AND_temp_sat [simp] OR_temp_sat [simp] NOT_temp_sat [simp]
   1.150 +
   1.151 +
   1.152 +lemma AbsRuleT2:
   1.153 +   "[|is_live_abstraction h (C,L) (A,M);
   1.154 +          validLIOA (A,M) Q;  temp_strengthening Q P h |]
   1.155 +          ==> validLIOA (C,L) P"
   1.156 +apply (unfold is_live_abstraction_def)
   1.157 +apply auto
   1.158 +apply (drule abs_is_weakening)
   1.159 +apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
   1.160 +apply (auto simp add: split_paired_all)
   1.161 +done
   1.162 +
   1.163 +
   1.164 +lemma AbsRuleTImprove:
   1.165 +   "[|is_live_abstraction h (C,L) (A,M);
   1.166 +          validLIOA (A,M) (H1 .--> Q);  temp_strengthening Q P h;
   1.167 +          temp_weakening H1 H2 h; validLIOA (C,L) H2 |]
   1.168 +          ==> validLIOA (C,L) P"
   1.169 +apply (unfold is_live_abstraction_def)
   1.170 +apply auto
   1.171 +apply (drule abs_is_weakening)
   1.172 +apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
   1.173 +apply (auto simp add: split_paired_all)
   1.174 +done
   1.175 +
   1.176 +
   1.177 +subsection "Correctness of safe abstraction"
   1.178 +
   1.179 +lemma abstraction_is_ref_map:
   1.180 +"is_abstraction h C A ==> is_ref_map h C A"
   1.181 +apply (unfold is_abstraction_def is_ref_map_def)
   1.182 +apply auto
   1.183 +apply (rule_tac x = "(a,h t) >>nil" in exI)
   1.184 +apply (simp add: move_def)
   1.185 +done
   1.186 +
   1.187 +
   1.188 +lemma abs_safety: "[| inp(C)=inp(A); out(C)=out(A);
   1.189 +                   is_abstraction h C A |]
   1.190 +                ==> C =<| A"
   1.191 +apply (simp add: ioa_implements_def)
   1.192 +apply (rule trace_inclusion)
   1.193 +apply (simp (no_asm) add: externals_def)
   1.194 +apply (auto)[1]
   1.195 +apply (erule abstraction_is_ref_map)
   1.196 +done
   1.197 +
   1.198 +
   1.199 +subsection "Correctness of life abstraction"
   1.200 +
   1.201 +(* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x),
   1.202 +   that is to special Map Lemma *)
   1.203 +lemma traces_coincide_abs:
   1.204 +  "ext C = ext A
   1.205 +         ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))"
   1.206 +apply (unfold cex_abs_def mk_trace_def filter_act_def)
   1.207 +apply simp
   1.208 +apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
   1.209 +done
   1.210 +
   1.211 +
   1.212 +(* Does not work with abstraction_is_ref_map as proof of abs_safety, because
   1.213 +   is_live_abstraction includes temp_strengthening which is necessarily based
   1.214 +   on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific
   1.215 +   way for cex_abs *)
   1.216 +lemma abs_liveness: "[| inp(C)=inp(A); out(C)=out(A);
   1.217 +                   is_live_abstraction h (C,M) (A,L) |]
   1.218 +                ==> live_implements (C,M) (A,L)"
   1.219 +apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def)
   1.220 +apply auto
   1.221 +apply (rule_tac x = "cex_abs h ex" in exI)
   1.222 +apply auto
   1.223 +  (* Traces coincide *)
   1.224 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.225 +  apply (rule traces_coincide_abs)
   1.226 +  apply (simp (no_asm) add: externals_def)
   1.227 +  apply (auto)[1]
   1.228 +
   1.229 +  (* cex_abs is execution *)
   1.230 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.231 +  apply (simp add: executions_def)
   1.232 +  (* start state *)
   1.233 +  apply (rule conjI)
   1.234 +  apply (simp add: is_abstraction_def cex_abs_def)
   1.235 +  (* is-execution-fragment *)
   1.236 +  apply (erule exec_frag_abstraction)
   1.237 +  apply (simp add: reachable.reachable_0)
   1.238 +
   1.239 + (* Liveness *)
   1.240 +apply (simp add: temp_weakening_def2)
   1.241 + apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.242 +done
   1.243 +
   1.244 +(* FIX: NAch Traces.ML bringen *)
   1.245 +
   1.246 +lemma implements_trans:
   1.247 +"[| A =<| B; B =<| C|] ==> A =<| C"
   1.248 +by (auto simp add: ioa_implements_def)
   1.249 +
   1.250 +
   1.251 +subsection "Abstraction Rules for Automata"
   1.252 +
   1.253 +lemma AbsRuleA1: "[| inp(C)=inp(A); out(C)=out(A);
   1.254 +                   inp(Q)=inp(P); out(Q)=out(P);
   1.255 +                   is_abstraction h1 C A;
   1.256 +                   A =<| Q ;
   1.257 +                   is_abstraction h2 Q P |]
   1.258 +                ==> C =<| P"
   1.259 +apply (drule abs_safety)
   1.260 +apply assumption+
   1.261 +apply (drule abs_safety)
   1.262 +apply assumption+
   1.263 +apply (erule implements_trans)
   1.264 +apply (erule implements_trans)
   1.265 +apply assumption
   1.266 +done
   1.267 +
   1.268 +
   1.269 +lemma AbsRuleA2: "!!LC. [| inp(C)=inp(A); out(C)=out(A);
   1.270 +                   inp(Q)=inp(P); out(Q)=out(P);
   1.271 +                   is_live_abstraction h1 (C,LC) (A,LA);
   1.272 +                   live_implements (A,LA) (Q,LQ) ;
   1.273 +                   is_live_abstraction h2 (Q,LQ) (P,LP) |]
   1.274 +                ==> live_implements (C,LC) (P,LP)"
   1.275 +apply (drule abs_liveness)
   1.276 +apply assumption+
   1.277 +apply (drule abs_liveness)
   1.278 +apply assumption+
   1.279 +apply (erule live_implements_trans)
   1.280 +apply (erule live_implements_trans)
   1.281 +apply assumption
   1.282 +done
   1.283 +
   1.284 +
   1.285 +declare split_paired_All [simp del]
   1.286 +
   1.287 +
   1.288 +subsection "Localizing Temporal Strengthenings and Weakenings"
   1.289 +
   1.290 +lemma strength_AND:
   1.291 +"[| temp_strengthening P1 Q1 h;
   1.292 +          temp_strengthening P2 Q2 h |]
   1.293 +       ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h"
   1.294 +apply (unfold temp_strengthening_def)
   1.295 +apply auto
   1.296 +done
   1.297 +
   1.298 +lemma strength_OR:
   1.299 +"[| temp_strengthening P1 Q1 h;
   1.300 +          temp_strengthening P2 Q2 h |]
   1.301 +       ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h"
   1.302 +apply (unfold temp_strengthening_def)
   1.303 +apply auto
   1.304 +done
   1.305 +
   1.306 +lemma strength_NOT:
   1.307 +"[| temp_weakening P Q h |]
   1.308 +       ==> temp_strengthening (.~ P) (.~ Q) h"
   1.309 +apply (unfold temp_strengthening_def)
   1.310 +apply (simp add: temp_weakening_def2)
   1.311 +apply auto
   1.312 +done
   1.313 +
   1.314 +lemma strength_IMPLIES:
   1.315 +"[| temp_weakening P1 Q1 h;
   1.316 +          temp_strengthening P2 Q2 h |]
   1.317 +       ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h"
   1.318 +apply (unfold temp_strengthening_def)
   1.319 +apply (simp add: temp_weakening_def2)
   1.320 +done
   1.321 +
   1.322 +
   1.323 +lemma weak_AND:
   1.324 +"[| temp_weakening P1 Q1 h;
   1.325 +          temp_weakening P2 Q2 h |]
   1.326 +       ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h"
   1.327 +apply (simp add: temp_weakening_def2)
   1.328 +done
   1.329 +
   1.330 +lemma weak_OR:
   1.331 +"[| temp_weakening P1 Q1 h;
   1.332 +          temp_weakening P2 Q2 h |]
   1.333 +       ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h"
   1.334 +apply (simp add: temp_weakening_def2)
   1.335 +done
   1.336 +
   1.337 +lemma weak_NOT:
   1.338 +"[| temp_strengthening P Q h |]
   1.339 +       ==> temp_weakening (.~ P) (.~ Q) h"
   1.340 +apply (unfold temp_strengthening_def)
   1.341 +apply (simp add: temp_weakening_def2)
   1.342 +apply auto
   1.343 +done
   1.344 +
   1.345 +lemma weak_IMPLIES:
   1.346 +"[| temp_strengthening P1 Q1 h;
   1.347 +          temp_weakening P2 Q2 h |]
   1.348 +       ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h"
   1.349 +apply (unfold temp_strengthening_def)
   1.350 +apply (simp add: temp_weakening_def2)
   1.351 +done
   1.352 +
   1.353 +
   1.354 +subsubsection {* Box *}
   1.355 +
   1.356 +(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
   1.357 +lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))"
   1.358 +apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *})
   1.359 +done
   1.360 +
   1.361 +lemma ex2seqConc [rule_format]:
   1.362 +"Finite s1 -->
   1.363 +  (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))"
   1.364 +apply (rule impI)
   1.365 +apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
   1.366 +apply blast
   1.367 +(* main case *)
   1.368 +apply clarify
   1.369 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.370 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   1.371 +(* UU case *)
   1.372 +apply (simp add: nil_is_Conc)
   1.373 +(* nil case *)
   1.374 +apply (simp add: nil_is_Conc)
   1.375 +(* cons case *)
   1.376 +apply (tactic {* pair_tac @{context} "aa" 1 *})
   1.377 +apply auto
   1.378 +done
   1.379 +
   1.380 +(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
   1.381 +
   1.382 +lemma ex2seq_tsuffix:
   1.383 +"tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')"
   1.384 +apply (unfold tsuffix_def suffix_def)
   1.385 +apply auto
   1.386 +apply (drule ex2seqConc)
   1.387 +apply auto
   1.388 +done
   1.389 +
   1.390 +
   1.391 +(* FIX: NAch Sequence.ML bringen *)
   1.392 +
   1.393 +lemma Mapnil: "(Map f$s = nil) = (s=nil)"
   1.394 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   1.395 +done
   1.396 +
   1.397 +lemma MapUU: "(Map f$s = UU) = (s=UU)"
   1.398 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   1.399 +done
   1.400 +
   1.401 +
   1.402 +(* important property of cex_absSeq: As it is a 1to1 correspondence,
   1.403 +  properties carry over *)
   1.404 +
   1.405 +lemma cex_absSeq_tsuffix:
   1.406 +"tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)"
   1.407 +apply (unfold tsuffix_def suffix_def cex_absSeq_def)
   1.408 +apply auto
   1.409 +apply (simp add: Mapnil)
   1.410 +apply (simp add: MapUU)
   1.411 +apply (rule_tac x = "Map (% (s,a,t) . (h s,a, h t))$s1" in exI)
   1.412 +apply (simp add: Map2Finite MapConc)
   1.413 +done
   1.414 +
   1.415 +
   1.416 +lemma strength_Box:
   1.417 +"[| temp_strengthening P Q h |]
   1.418 +       ==> temp_strengthening ([] P) ([] Q) h"
   1.419 +apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def)
   1.420 +apply clarify
   1.421 +apply (frule ex2seq_tsuffix)
   1.422 +apply clarify
   1.423 +apply (drule_tac h = "h" in cex_absSeq_tsuffix)
   1.424 +apply (simp add: ex2seq_abs_cex)
   1.425 +done
   1.426 +
   1.427 +
   1.428 +subsubsection {* Init *}
   1.429 +
   1.430 +lemma strength_Init:
   1.431 +"[| state_strengthening P Q h |]
   1.432 +       ==> temp_strengthening (Init P) (Init Q) h"
   1.433 +apply (unfold temp_strengthening_def state_strengthening_def
   1.434 +  temp_sat_def satisfies_def Init_def unlift_def)
   1.435 +apply auto
   1.436 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.437 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   1.438 +apply (tactic {* pair_tac @{context} "a" 1 *})
   1.439 +done
   1.440 +
   1.441 +
   1.442 +subsubsection {* Next *}
   1.443 +
   1.444 +lemma TL_ex2seq_UU:
   1.445 +"(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"
   1.446 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.447 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   1.448 +apply (tactic {* pair_tac @{context} "a" 1 *})
   1.449 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   1.450 +apply (tactic {* pair_tac @{context} "a" 1 *})
   1.451 +done
   1.452 +
   1.453 +lemma TL_ex2seq_nil:
   1.454 +"(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"
   1.455 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.456 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   1.457 +apply (tactic {* pair_tac @{context} "a" 1 *})
   1.458 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   1.459 +apply (tactic {* pair_tac @{context} "a" 1 *})
   1.460 +done
   1.461 +
   1.462 +(* FIX: put to Sequence Lemmas *)
   1.463 +lemma MapTL: "Map f$(TL$s) = TL$(Map f$s)"
   1.464 +apply (tactic {* Seq_induct_tac @{context} "s" [] 1 *})
   1.465 +done
   1.466 +
   1.467 +(* important property of cex_absSeq: As it is a 1to1 correspondence,
   1.468 +  properties carry over *)
   1.469 +
   1.470 +lemma cex_absSeq_TL:
   1.471 +"cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))"
   1.472 +apply (unfold cex_absSeq_def)
   1.473 +apply (simp add: MapTL)
   1.474 +done
   1.475 +
   1.476 +(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
   1.477 +
   1.478 +lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')"
   1.479 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.480 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   1.481 +apply (tactic {* pair_tac @{context} "a" 1 *})
   1.482 +apply auto
   1.483 +done
   1.484 +
   1.485 +
   1.486 +lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"
   1.487 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.488 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   1.489 +apply (tactic {* pair_tac @{context} "a" 1 *})
   1.490 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   1.491 +apply (tactic {* pair_tac @{context} "a" 1 *})
   1.492 +done
   1.493 +
   1.494 +
   1.495 +lemma strength_Next:
   1.496 +"[| temp_strengthening P Q h |]
   1.497 +       ==> temp_strengthening (Next P) (Next Q) h"
   1.498 +apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def)
   1.499 +apply simp
   1.500 +apply auto
   1.501 +apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
   1.502 +apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
   1.503 +apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
   1.504 +apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
   1.505 +(* cons case *)
   1.506 +apply (simp add: TL_ex2seq_nil TL_ex2seq_UU ex2seq_abs_cex cex_absSeq_TL [symmetric] ex2seqnilTL)
   1.507 +apply (erule conjE)
   1.508 +apply (drule TLex2seq)
   1.509 +apply assumption
   1.510 +apply auto
   1.511 +done
   1.512 +
   1.513 +
   1.514 +text {* Localizing Temporal Weakenings     - 2 *}
   1.515 +
   1.516 +lemma weak_Init:
   1.517 +"[| state_weakening P Q h |]
   1.518 +       ==> temp_weakening (Init P) (Init Q) h"
   1.519 +apply (simp add: temp_weakening_def2 state_weakening_def2
   1.520 +  temp_sat_def satisfies_def Init_def unlift_def)
   1.521 +apply auto
   1.522 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.523 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   1.524 +apply (tactic {* pair_tac @{context} "a" 1 *})
   1.525 +done
   1.526 +
   1.527 +
   1.528 +text {* Localizing Temproal Strengthenings - 3 *}
   1.529 +
   1.530 +lemma strength_Diamond:
   1.531 +"[| temp_strengthening P Q h |]
   1.532 +       ==> temp_strengthening (<> P) (<> Q) h"
   1.533 +apply (unfold Diamond_def)
   1.534 +apply (rule strength_NOT)
   1.535 +apply (rule weak_Box)
   1.536 +apply (erule weak_NOT)
   1.537 +done
   1.538 +
   1.539 +lemma strength_Leadsto:
   1.540 +"[| temp_weakening P1 P2 h;
   1.541 +          temp_strengthening Q1 Q2 h |]
   1.542 +       ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h"
   1.543 +apply (unfold Leadsto_def)
   1.544 +apply (rule strength_Box)
   1.545 +apply (erule strength_IMPLIES)
   1.546 +apply (erule strength_Diamond)
   1.547 +done
   1.548 +
   1.549 +
   1.550 +text {* Localizing Temporal Weakenings - 3 *}
   1.551 +
   1.552 +lemma weak_Diamond:
   1.553 +"[| temp_weakening P Q h |]
   1.554 +       ==> temp_weakening (<> P) (<> Q) h"
   1.555 +apply (unfold Diamond_def)
   1.556 +apply (rule weak_NOT)
   1.557 +apply (rule strength_Box)
   1.558 +apply (erule strength_NOT)
   1.559 +done
   1.560 +
   1.561 +lemma weak_Leadsto:
   1.562 +"[| temp_strengthening P1 P2 h;
   1.563 +          temp_weakening Q1 Q2 h |]
   1.564 +       ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h"
   1.565 +apply (unfold Leadsto_def)
   1.566 +apply (rule weak_Box)
   1.567 +apply (erule weak_IMPLIES)
   1.568 +apply (erule weak_Diamond)
   1.569 +done
   1.570 +
   1.571 +lemma weak_WF:
   1.572 +  " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|]
   1.573 +    ==> temp_weakening (WF A acts) (WF C acts) h"
   1.574 +apply (unfold WF_def)
   1.575 +apply (rule weak_IMPLIES)
   1.576 +apply (rule strength_Diamond)
   1.577 +apply (rule strength_Box)
   1.578 +apply (rule strength_Init)
   1.579 +apply (rule_tac [2] weak_Box)
   1.580 +apply (rule_tac [2] weak_Diamond)
   1.581 +apply (rule_tac [2] weak_Init)
   1.582 +apply (auto simp add: state_weakening_def state_strengthening_def
   1.583 +  xt2_def plift_def option_lift_def NOT_def)
   1.584 +done
   1.585 +
   1.586 +lemma weak_SF:
   1.587 +  " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|]
   1.588 +    ==> temp_weakening (SF A acts) (SF C acts) h"
   1.589 +apply (unfold SF_def)
   1.590 +apply (rule weak_IMPLIES)
   1.591 +apply (rule strength_Box)
   1.592 +apply (rule strength_Diamond)
   1.593 +apply (rule strength_Init)
   1.594 +apply (rule_tac [2] weak_Box)
   1.595 +apply (rule_tac [2] weak_Diamond)
   1.596 +apply (rule_tac [2] weak_Init)
   1.597 +apply (auto simp add: state_weakening_def state_strengthening_def
   1.598 +  xt2_def plift_def option_lift_def NOT_def)
   1.599 +done
   1.600 +
   1.601 +
   1.602 +lemmas weak_strength_lemmas =
   1.603 +  weak_OR weak_AND weak_NOT weak_IMPLIES weak_Box weak_Next weak_Init
   1.604 +  weak_Diamond weak_Leadsto strength_OR strength_AND strength_NOT
   1.605 +  strength_IMPLIES strength_Box strength_Next strength_Init
   1.606 +  strength_Diamond strength_Leadsto weak_WF weak_SF
   1.607 +
   1.608 +ML {*
   1.609 +fun abstraction_tac ctxt =
   1.610 +  let val (cs, ss) = clasimpset_of ctxt in
   1.611 +    SELECT_GOAL (auto_tac (cs addSIs @{thms weak_strength_lemmas},
   1.612 +        ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
   1.613 +  end
   1.614 +*}
   1.615 +
   1.616 +method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
   1.617 +
   1.618 +end