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