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