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