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