src/HOL/HOLCF/IOA/meta_theory/Automata.thy
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58880 0baae4311a9f
child 59807 22bc39064290
permissions -rw-r--r--
proper context for match_tac etc.;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/IOA/meta_theory/Automata.thy
wenzelm@40945
     2
    Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
wenzelm@17233
     3
*)
mueller@3071
     4
wenzelm@58880
     5
section {* The I/O automata of Lynch and Tuttle in HOLCF *}
mueller@3071
     6
wenzelm@17233
     7
theory Automata
wenzelm@17233
     8
imports Asig
wenzelm@17233
     9
begin
wenzelm@17233
    10
wenzelm@36452
    11
default_sort type
wenzelm@17233
    12
huffman@41476
    13
type_synonym
wenzelm@17233
    14
  ('a, 's) transition = "'s * 'a * 's"
huffman@41476
    15
huffman@41476
    16
type_synonym
wenzelm@17233
    17
  ('a, 's) ioa = "'a signature * 's set * ('a,'s)transition set * ('a set set) * ('a set set)"
mueller@3071
    18
mueller@3071
    19
consts
wenzelm@17233
    20
mueller@3071
    21
  (* IO automata *)
mueller@3521
    22
mueller@3521
    23
  asig_of        ::"('a,'s)ioa => 'a signature"
mueller@3521
    24
  starts_of      ::"('a,'s)ioa => 's set"
mueller@3521
    25
  trans_of       ::"('a,'s)ioa => ('a,'s)transition set"
mueller@3521
    26
  wfair_of       ::"('a,'s)ioa => ('a set) set"
mueller@3521
    27
  sfair_of       ::"('a,'s)ioa => ('a set) set"
mueller@3521
    28
mueller@3521
    29
  is_asig_of     ::"('a,'s)ioa => bool"
wenzelm@17233
    30
  is_starts_of   ::"('a,'s)ioa => bool"
wenzelm@17233
    31
  is_trans_of    ::"('a,'s)ioa => bool"
wenzelm@17233
    32
  input_enabled  ::"('a,'s)ioa => bool"
wenzelm@17233
    33
  IOA            ::"('a,'s)ioa => bool"
mueller@3071
    34
mueller@4559
    35
  (* constraints for fair IOA *)
mueller@4559
    36
mueller@4559
    37
  fairIOA        ::"('a,'s)ioa => bool"
mueller@4559
    38
  input_resistant::"('a,'s)ioa => bool"
mueller@4559
    39
mueller@4559
    40
  (* enabledness of actions and action sets *)
mueller@4559
    41
mueller@4559
    42
  enabled        ::"('a,'s)ioa => 'a => 's => bool"
mueller@4559
    43
  Enabled    ::"('a,'s)ioa => 'a set => 's => bool"
mueller@4559
    44
wenzelm@17233
    45
  (* action set keeps enabled until probably disabled by itself *)
mueller@4559
    46
mueller@4559
    47
  en_persistent  :: "('a,'s)ioa => 'a set => bool"
mueller@4559
    48
mueller@4559
    49
 (* post_conditions for actions and action sets *)
mueller@4559
    50
mueller@4559
    51
  was_enabled        ::"('a,'s)ioa => 'a => 's => bool"
mueller@4559
    52
  set_was_enabled    ::"('a,'s)ioa => 'a set => 's => bool"
mueller@4559
    53
berghofe@23778
    54
  (* invariants *)
mueller@3071
    55
  invariant     :: "[('a,'s)ioa, 's=>bool] => bool"
mueller@3071
    56
mueller@3071
    57
  (* binary composition of action signatures and automata *)
mueller@3071
    58
  asig_comp    ::"['a signature, 'a signature] => 'a signature"
mueller@3521
    59
  compatible   ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
wenzelm@22808
    60
  par          ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
mueller@3071
    61
mueller@3521
    62
  (* hiding and restricting *)
mueller@3521
    63
  hide_asig     :: "['a signature, 'a set] => 'a signature"
wenzelm@36176
    64
  hide          :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
mueller@3071
    65
  restrict_asig :: "['a signature, 'a set] => 'a signature"
mueller@3071
    66
  restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
mueller@3071
    67
mueller@3071
    68
  (* renaming *)
mueller@3521
    69
  rename_set    :: "'a set => ('c => 'a option) => 'c set"
mueller@3521
    70
  rename        :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
mueller@3071
    71
wenzelm@22808
    72
notation (xsymbols)
wenzelm@22808
    73
  par  (infixr "\<parallel>" 10)
mueller@3071
    74
mueller@3071
    75
berghofe@23778
    76
inductive
berghofe@23778
    77
  reachable :: "('a, 's) ioa => 's => bool"
berghofe@23778
    78
  for C :: "('a, 's) ioa"
berghofe@23778
    79
  where
berghofe@23778
    80
    reachable_0:  "s : starts_of C ==> reachable C s"
berghofe@23778
    81
  | reachable_n:  "[| reachable C s; (s, a, t) : trans_of C |] ==> reachable C t"
mueller@3071
    82
wenzelm@25131
    83
abbreviation
wenzelm@25131
    84
  trans_of_syn  ("_ -_--_-> _" [81,81,81,81] 100) where
wenzelm@25131
    85
  "s -a--A-> t == (s,a,t):trans_of A"
mueller@3071
    86
wenzelm@25131
    87
notation (xsymbols)
wenzelm@25131
    88
  trans_of_syn  ("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100)
wenzelm@25131
    89
wenzelm@25131
    90
abbreviation "act A == actions (asig_of A)"
wenzelm@25131
    91
abbreviation "ext A == externals (asig_of A)"
wenzelm@25131
    92
abbreviation int where "int A == internals (asig_of A)"
wenzelm@25131
    93
abbreviation "inp A == inputs (asig_of A)"
wenzelm@25131
    94
abbreviation "out A == outputs (asig_of A)"
wenzelm@25131
    95
abbreviation "local A == locals (asig_of A)"
mueller@3433
    96
mueller@3071
    97
defs
mueller@3071
    98
mueller@3071
    99
(* --------------------------------- IOA ---------------------------------*)
mueller@3071
   100
wenzelm@17233
   101
asig_of_def:   "asig_of == fst"
wenzelm@17233
   102
starts_of_def: "starts_of == (fst o snd)"
wenzelm@17233
   103
trans_of_def:  "trans_of == (fst o snd o snd)"
wenzelm@17233
   104
wfair_of_def:  "wfair_of == (fst o snd o snd o snd)"
wenzelm@17233
   105
sfair_of_def:  "sfair_of == (snd o snd o snd o snd)"
wenzelm@17233
   106
wenzelm@17233
   107
is_asig_of_def:
wenzelm@17233
   108
  "is_asig_of A == is_asig (asig_of A)"
wenzelm@17233
   109
wenzelm@17233
   110
is_starts_of_def:
wenzelm@17233
   111
  "is_starts_of A ==  (~ starts_of A = {})"
wenzelm@17233
   112
wenzelm@17233
   113
is_trans_of_def:
wenzelm@17233
   114
  "is_trans_of A ==
wenzelm@17233
   115
    (!triple. triple:(trans_of A) --> fst(snd(triple)):actions(asig_of A))"
wenzelm@17233
   116
wenzelm@17233
   117
input_enabled_def:
wenzelm@17233
   118
  "input_enabled A ==
wenzelm@17233
   119
    (!a. (a:inputs(asig_of A)) --> (!s1. ? s2. (s1,a,s2):(trans_of A)))"
mueller@3071
   120
mueller@3071
   121
wenzelm@17233
   122
ioa_def:
wenzelm@17233
   123
  "IOA A == (is_asig_of A    &
wenzelm@17233
   124
             is_starts_of A  &
mueller@3521
   125
             is_trans_of A   &
mueller@3521
   126
             input_enabled A)"
mueller@3071
   127
mueller@3071
   128
wenzelm@17233
   129
invariant_def: "invariant A P == (!s. reachable A s --> P(s))"
mueller@3071
   130
mueller@3071
   131
mueller@3071
   132
(* ------------------------- parallel composition --------------------------*)
mueller@3071
   133
mueller@3071
   134
wenzelm@17233
   135
compatible_def:
wenzelm@17233
   136
  "compatible A B ==
wenzelm@17233
   137
  (((out A Int out B) = {}) &
wenzelm@17233
   138
   ((int A Int act B) = {}) &
mueller@3433
   139
   ((int B Int act A) = {}))"
mueller@3071
   140
wenzelm@17233
   141
asig_comp_def:
wenzelm@17233
   142
  "asig_comp a1 a2 ==
wenzelm@17233
   143
     (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
wenzelm@17233
   144
       (outputs(a1) Un outputs(a2)),
mueller@3071
   145
       (internals(a1) Un internals(a2))))"
mueller@3071
   146
wenzelm@17233
   147
par_def:
wenzelm@17233
   148
  "(A || B) ==
wenzelm@17233
   149
      (asig_comp (asig_of A) (asig_of B),
wenzelm@17233
   150
       {pr. fst(pr):starts_of(A) & snd(pr):starts_of(B)},
wenzelm@17233
   151
       {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
wenzelm@17233
   152
            in (a:act A | a:act B) &
wenzelm@17233
   153
               (if a:act A then
wenzelm@17233
   154
                  (fst(s),a,fst(t)):trans_of(A)
wenzelm@17233
   155
                else fst(t) = fst(s))
wenzelm@17233
   156
               &
wenzelm@17233
   157
               (if a:act B then
wenzelm@17233
   158
                  (snd(s),a,snd(t)):trans_of(B)
mueller@3521
   159
                else snd(t) = snd(s))},
mueller@3521
   160
        wfair_of A Un wfair_of B,
mueller@3521
   161
        sfair_of A Un sfair_of B)"
mueller@3521
   162
mueller@3071
   163
mueller@3071
   164
(* ------------------------ hiding -------------------------------------------- *)
mueller@3071
   165
wenzelm@17233
   166
restrict_asig_def:
wenzelm@17233
   167
  "restrict_asig asig actns ==
wenzelm@17233
   168
    (inputs(asig) Int actns,
wenzelm@17233
   169
     outputs(asig) Int actns,
mueller@3071
   170
     internals(asig) Un (externals(asig) - actns))"
mueller@3071
   171
wenzelm@17233
   172
(* Notice that for wfair_of and sfair_of nothing has to be changed, as
wenzelm@17233
   173
   changes from the outputs to the internals does not touch the locals as
mueller@3521
   174
   a whole, which is of importance for fairness only *)
mueller@3071
   175
wenzelm@17233
   176
restrict_def:
wenzelm@17233
   177
  "restrict A actns ==
wenzelm@17233
   178
    (restrict_asig (asig_of A) actns,
wenzelm@17233
   179
     starts_of A,
mueller@3521
   180
     trans_of A,
mueller@3521
   181
     wfair_of A,
mueller@3521
   182
     sfair_of A)"
mueller@3521
   183
wenzelm@17233
   184
hide_asig_def:
wenzelm@17233
   185
  "hide_asig asig actns ==
wenzelm@17233
   186
    (inputs(asig) - actns,
wenzelm@17233
   187
     outputs(asig) - actns,
mueller@3521
   188
     internals(asig) Un actns)"
mueller@3521
   189
wenzelm@17233
   190
hide_def:
wenzelm@17233
   191
  "hide A actns ==
wenzelm@17233
   192
    (hide_asig (asig_of A) actns,
wenzelm@17233
   193
     starts_of A,
mueller@3521
   194
     trans_of A,
mueller@3521
   195
     wfair_of A,
mueller@3521
   196
     sfair_of A)"
mueller@3071
   197
mueller@3071
   198
(* ------------------------- renaming ------------------------------------------- *)
wenzelm@17233
   199
wenzelm@17233
   200
rename_set_def:
wenzelm@17233
   201
  "rename_set A ren == {b. ? x. Some x = ren b & x : A}"
mueller@3521
   202
wenzelm@17233
   203
rename_def:
wenzelm@17233
   204
"rename ioa ren ==
wenzelm@17233
   205
  ((rename_set (inp ioa) ren,
wenzelm@17233
   206
    rename_set (out ioa) ren,
wenzelm@17233
   207
    rename_set (int ioa) ren),
wenzelm@17233
   208
   starts_of ioa,
wenzelm@17233
   209
   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
wenzelm@17233
   210
        in
mueller@3521
   211
        ? x. Some(x) = ren(a) & (s,x,t):trans_of ioa},
mueller@3521
   212
   {rename_set s ren | s. s: wfair_of ioa},
mueller@3521
   213
   {rename_set s ren | s. s: sfair_of ioa})"
mueller@3071
   214
mueller@4559
   215
(* ------------------------- fairness ----------------------------- *)
mueller@4559
   216
wenzelm@17233
   217
fairIOA_def:
wenzelm@17233
   218
  "fairIOA A == (! S : wfair_of A. S<= local A) &
mueller@4559
   219
                (! S : sfair_of A. S<= local A)"
mueller@4559
   220
wenzelm@17233
   221
input_resistant_def:
wenzelm@17233
   222
  "input_resistant A == ! W : sfair_of A. ! s a t.
mueller@4559
   223
                        reachable A s & reachable A t & a:inp A &
mueller@4559
   224
                        Enabled A W s & s -a--A-> t
mueller@4559
   225
                        --> Enabled A W t"
mueller@4559
   226
wenzelm@17233
   227
enabled_def:
mueller@4559
   228
  "enabled A a s == ? t. s-a--A-> t"
mueller@4559
   229
wenzelm@17233
   230
Enabled_def:
mueller@4559
   231
  "Enabled A W s == ? w:W. enabled A w s"
mueller@4559
   232
wenzelm@17233
   233
en_persistent_def:
wenzelm@17233
   234
  "en_persistent A W == ! s a t. Enabled A W s &
wenzelm@17233
   235
                                 a ~:W &
wenzelm@17233
   236
                                 s -a--A-> t
mueller@4559
   237
                                 --> Enabled A W t"
wenzelm@17233
   238
was_enabled_def:
mueller@4559
   239
  "was_enabled A a t == ? s. s-a--A-> t"
mueller@4559
   240
wenzelm@17233
   241
set_was_enabled_def:
mueller@4559
   242
  "set_was_enabled A W t == ? w:W. was_enabled A w t"
mueller@4559
   243
wenzelm@19741
   244
wenzelm@19741
   245
declare split_paired_Ex [simp del]
wenzelm@19741
   246
wenzelm@19741
   247
lemmas ioa_projections = asig_of_def starts_of_def trans_of_def wfair_of_def sfair_of_def
wenzelm@19741
   248
wenzelm@19741
   249
wenzelm@19741
   250
subsection "asig_of, starts_of, trans_of"
wenzelm@19741
   251
wenzelm@19741
   252
lemma ioa_triple_proj: 
wenzelm@19741
   253
 "((asig_of (x,y,z,w,s)) = x)   &  
wenzelm@19741
   254
  ((starts_of (x,y,z,w,s)) = y) &  
wenzelm@19741
   255
  ((trans_of (x,y,z,w,s)) = z)  &  
wenzelm@19741
   256
  ((wfair_of (x,y,z,w,s)) = w) &  
wenzelm@19741
   257
  ((sfair_of (x,y,z,w,s)) = s)"
wenzelm@19741
   258
  apply (simp add: ioa_projections)
wenzelm@19741
   259
  done
wenzelm@19741
   260
wenzelm@19741
   261
lemma trans_in_actions: 
wenzelm@19741
   262
  "[| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A"
wenzelm@19741
   263
apply (unfold is_trans_of_def actions_def is_asig_def)
wenzelm@19741
   264
  apply (erule allE, erule impE, assumption)
wenzelm@19741
   265
  apply simp
wenzelm@19741
   266
done
wenzelm@19741
   267
wenzelm@19741
   268
lemma starts_of_par: 
wenzelm@19741
   269
"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"
wenzelm@19741
   270
  apply (simp add: par_def ioa_projections)
wenzelm@19741
   271
done
wenzelm@19741
   272
wenzelm@19741
   273
lemma trans_of_par: 
wenzelm@19741
   274
"trans_of(A || B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))  
wenzelm@19741
   275
             in (a:act A | a:act B) &  
wenzelm@19741
   276
                (if a:act A then        
wenzelm@19741
   277
                   (fst(s),a,fst(t)):trans_of(A)  
wenzelm@19741
   278
                 else fst(t) = fst(s))             
wenzelm@19741
   279
                &                                   
wenzelm@19741
   280
                (if a:act B then                     
wenzelm@19741
   281
                   (snd(s),a,snd(t)):trans_of(B)      
wenzelm@19741
   282
                 else snd(t) = snd(s))}"
wenzelm@19741
   283
wenzelm@19741
   284
apply (simp add: par_def ioa_projections)
wenzelm@19741
   285
done
wenzelm@19741
   286
wenzelm@19741
   287
wenzelm@19741
   288
subsection "actions and par"
wenzelm@19741
   289
wenzelm@19741
   290
lemma actions_asig_comp: 
wenzelm@19741
   291
  "actions(asig_comp a b) = actions(a) Un actions(b)"
wenzelm@19741
   292
  apply (simp (no_asm) add: actions_def asig_comp_def asig_projections)
wenzelm@19741
   293
  apply blast
wenzelm@19741
   294
  done
wenzelm@19741
   295
wenzelm@19741
   296
lemma asig_of_par: "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"
wenzelm@19741
   297
  apply (simp add: par_def ioa_projections)
wenzelm@19741
   298
  done
wenzelm@19741
   299
wenzelm@19741
   300
wenzelm@19741
   301
lemma externals_of_par: "ext (A1||A2) =     
wenzelm@19741
   302
   (ext A1) Un (ext A2)"
wenzelm@19741
   303
apply (simp add: externals_def asig_of_par asig_comp_def
berghofe@26806
   304
  asig_inputs_def asig_outputs_def Un_def set_diff_eq)
wenzelm@19741
   305
apply blast
wenzelm@19741
   306
done
wenzelm@19741
   307
wenzelm@19741
   308
lemma actions_of_par: "act (A1||A2) =     
wenzelm@19741
   309
   (act A1) Un (act A2)"
wenzelm@19741
   310
apply (simp add: actions_def asig_of_par asig_comp_def
berghofe@26806
   311
  asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
wenzelm@19741
   312
apply blast
wenzelm@19741
   313
done
wenzelm@19741
   314
wenzelm@19741
   315
lemma inputs_of_par: "inp (A1||A2) = 
wenzelm@19741
   316
          ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"
wenzelm@19741
   317
apply (simp add: actions_def asig_of_par asig_comp_def
berghofe@26806
   318
  asig_inputs_def asig_outputs_def Un_def set_diff_eq)
wenzelm@19741
   319
done
wenzelm@19741
   320
wenzelm@19741
   321
lemma outputs_of_par: "out (A1||A2) = 
wenzelm@19741
   322
          (out A1) Un (out A2)"
wenzelm@19741
   323
apply (simp add: actions_def asig_of_par asig_comp_def
berghofe@26806
   324
  asig_outputs_def Un_def set_diff_eq)
wenzelm@19741
   325
done
wenzelm@19741
   326
wenzelm@19741
   327
lemma internals_of_par: "int (A1||A2) = 
wenzelm@19741
   328
          (int A1) Un (int A2)"
wenzelm@19741
   329
apply (simp add: actions_def asig_of_par asig_comp_def
berghofe@26806
   330
  asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
wenzelm@19741
   331
done
wenzelm@19741
   332
wenzelm@19741
   333
wenzelm@19741
   334
subsection "actions and compatibility"
wenzelm@19741
   335
wenzelm@19741
   336
lemma compat_commute: "compatible A B = compatible B A"
wenzelm@19741
   337
apply (simp add: compatible_def Int_commute)
wenzelm@19741
   338
apply auto
wenzelm@19741
   339
done
wenzelm@19741
   340
wenzelm@19741
   341
lemma ext1_is_not_int2: 
wenzelm@19741
   342
 "[| compatible A1 A2; a:ext A1|] ==> a~:int A2"
wenzelm@19741
   343
apply (unfold externals_def actions_def compatible_def)
wenzelm@19741
   344
apply simp
wenzelm@19741
   345
apply blast
wenzelm@19741
   346
done
wenzelm@19741
   347
wenzelm@19741
   348
(* just commuting the previous one: better commute compatible *)
wenzelm@19741
   349
lemma ext2_is_not_int1: 
wenzelm@19741
   350
 "[| compatible A2 A1 ; a:ext A1|] ==> a~:int A2"
wenzelm@19741
   351
apply (unfold externals_def actions_def compatible_def)
wenzelm@19741
   352
apply simp
wenzelm@19741
   353
apply blast
wenzelm@19741
   354
done
wenzelm@19741
   355
wenzelm@45606
   356
lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act]
wenzelm@45606
   357
lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act]
wenzelm@19741
   358
wenzelm@19741
   359
lemma intA_is_not_extB: 
wenzelm@19741
   360
 "[| compatible A B; x:int A |] ==> x~:ext B"
wenzelm@19741
   361
apply (unfold externals_def actions_def compatible_def)
wenzelm@19741
   362
apply simp
wenzelm@19741
   363
apply blast
wenzelm@19741
   364
done
wenzelm@19741
   365
wenzelm@19741
   366
lemma intA_is_not_actB: 
wenzelm@19741
   367
"[| compatible A B; a:int A |] ==> a ~: act B"
wenzelm@19741
   368
apply (unfold externals_def actions_def compatible_def is_asig_def asig_of_def)
wenzelm@19741
   369
apply simp
wenzelm@19741
   370
apply blast
wenzelm@19741
   371
done
wenzelm@19741
   372
wenzelm@19741
   373
(* the only one that needs disjointness of outputs and of internals and _all_ acts *)
wenzelm@19741
   374
lemma outAactB_is_inpB: 
wenzelm@19741
   375
"[| compatible A B; a:out A ;a:act B|] ==> a : inp B"
wenzelm@19741
   376
apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def 
wenzelm@19741
   377
    compatible_def is_asig_def asig_of_def)
wenzelm@19741
   378
apply simp
wenzelm@19741
   379
apply blast
wenzelm@19741
   380
done
wenzelm@19741
   381
wenzelm@19741
   382
(* needed for propagation of input_enabledness from A,B to A||B *)
wenzelm@19741
   383
lemma inpAAactB_is_inpBoroutB: 
wenzelm@19741
   384
"[| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B"
wenzelm@19741
   385
apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def 
wenzelm@19741
   386
    compatible_def is_asig_def asig_of_def)
wenzelm@19741
   387
apply simp
wenzelm@19741
   388
apply blast
wenzelm@19741
   389
done
wenzelm@19741
   390
wenzelm@19741
   391
wenzelm@19741
   392
subsection "input_enabledness and par"
wenzelm@19741
   393
wenzelm@19741
   394
(* ugly case distinctions. Heart of proof:
wenzelm@19741
   395
     1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
wenzelm@19741
   396
     2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
wenzelm@19741
   397
lemma input_enabled_par: 
wenzelm@19741
   398
"[| compatible A B; input_enabled A; input_enabled B|]  
wenzelm@19741
   399
      ==> input_enabled (A||B)"
wenzelm@19741
   400
apply (unfold input_enabled_def)
wenzelm@19741
   401
apply (simp add: Let_def inputs_of_par trans_of_par)
wenzelm@58957
   402
apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})")
wenzelm@19741
   403
apply (simp add: inp_is_act)
wenzelm@19741
   404
prefer 2
wenzelm@19741
   405
apply (simp add: inp_is_act)
wenzelm@19741
   406
(* a: inp A *)
wenzelm@19741
   407
apply (case_tac "a:act B")
wenzelm@19741
   408
(* a:act B *)
wenzelm@19741
   409
apply (erule_tac x = "a" in allE)
wenzelm@19741
   410
apply simp
wenzelm@19741
   411
apply (drule inpAAactB_is_inpBoroutB)
wenzelm@19741
   412
apply assumption
wenzelm@19741
   413
apply assumption
wenzelm@19741
   414
apply (erule_tac x = "a" in allE)
wenzelm@19741
   415
apply simp
wenzelm@19741
   416
apply (erule_tac x = "aa" in allE)
wenzelm@19741
   417
apply (erule_tac x = "b" in allE)
wenzelm@19741
   418
apply (erule exE)
wenzelm@19741
   419
apply (erule exE)
wenzelm@19741
   420
apply (rule_tac x = " (s2,s2a) " in exI)
wenzelm@19741
   421
apply (simp add: inp_is_act)
wenzelm@19741
   422
(* a~: act B*)
wenzelm@19741
   423
apply (simp add: inp_is_act)
wenzelm@19741
   424
apply (erule_tac x = "a" in allE)
wenzelm@19741
   425
apply simp
wenzelm@19741
   426
apply (erule_tac x = "aa" in allE)
wenzelm@19741
   427
apply (erule exE)
wenzelm@19741
   428
apply (rule_tac x = " (s2,b) " in exI)
wenzelm@19741
   429
apply simp
wenzelm@19741
   430
wenzelm@19741
   431
(* a:inp B *)
wenzelm@19741
   432
apply (case_tac "a:act A")
wenzelm@19741
   433
(* a:act A *)
wenzelm@19741
   434
apply (erule_tac x = "a" in allE)
wenzelm@19741
   435
apply (erule_tac x = "a" in allE)
wenzelm@19741
   436
apply (simp add: inp_is_act)
wenzelm@19741
   437
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
wenzelm@19741
   438
apply (drule inpAAactB_is_inpBoroutB)
wenzelm@19741
   439
back
wenzelm@19741
   440
apply assumption
wenzelm@19741
   441
apply assumption
wenzelm@19741
   442
apply simp
wenzelm@19741
   443
apply (erule_tac x = "aa" in allE)
wenzelm@19741
   444
apply (erule_tac x = "b" in allE)
wenzelm@19741
   445
apply (erule exE)
wenzelm@19741
   446
apply (erule exE)
wenzelm@19741
   447
apply (rule_tac x = " (s2,s2a) " in exI)
wenzelm@19741
   448
apply (simp add: inp_is_act)
wenzelm@19741
   449
(* a~: act B*)
wenzelm@19741
   450
apply (simp add: inp_is_act)
wenzelm@19741
   451
apply (erule_tac x = "a" in allE)
wenzelm@19741
   452
apply (erule_tac x = "a" in allE)
wenzelm@19741
   453
apply simp
wenzelm@19741
   454
apply (erule_tac x = "b" in allE)
wenzelm@19741
   455
apply (erule exE)
wenzelm@19741
   456
apply (rule_tac x = " (aa,s2) " in exI)
wenzelm@19741
   457
apply simp
wenzelm@19741
   458
done
wenzelm@19741
   459
wenzelm@19741
   460
wenzelm@19741
   461
subsection "invariants"
wenzelm@19741
   462
wenzelm@19741
   463
lemma invariantI:
wenzelm@19741
   464
  "[| !!s. s:starts_of(A) ==> P(s);      
wenzelm@19741
   465
      !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |]  
wenzelm@19741
   466
   ==> invariant A P"
wenzelm@19741
   467
apply (unfold invariant_def)
wenzelm@19741
   468
apply (rule allI)
wenzelm@19741
   469
apply (rule impI)
berghofe@23778
   470
apply (rule_tac x = "s" in reachable.induct)
wenzelm@19741
   471
apply assumption
wenzelm@19741
   472
apply blast
wenzelm@19741
   473
apply blast
wenzelm@19741
   474
done
wenzelm@19741
   475
wenzelm@19741
   476
lemma invariantI1:
wenzelm@19741
   477
 "[| !!s. s : starts_of(A) ==> P(s);  
wenzelm@19741
   478
     !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t)  
wenzelm@19741
   479
  |] ==> invariant A P"
wenzelm@19741
   480
  apply (blast intro: invariantI)
wenzelm@19741
   481
  done
wenzelm@19741
   482
wenzelm@19741
   483
lemma invariantE: "[| invariant A P; reachable A s |] ==> P(s)"
wenzelm@19741
   484
  apply (unfold invariant_def)
wenzelm@19741
   485
  apply blast
wenzelm@19741
   486
  done
wenzelm@19741
   487
wenzelm@19741
   488
wenzelm@19741
   489
subsection "restrict"
wenzelm@19741
   490
wenzelm@19741
   491
wenzelm@19741
   492
lemmas reachable_0 = reachable.reachable_0
wenzelm@19741
   493
  and reachable_n = reachable.reachable_n
wenzelm@19741
   494
wenzelm@19741
   495
lemma cancel_restrict_a: "starts_of(restrict ioa acts) = starts_of(ioa) &      
wenzelm@19741
   496
          trans_of(restrict ioa acts) = trans_of(ioa)"
wenzelm@19741
   497
apply (simp add: restrict_def ioa_projections)
wenzelm@19741
   498
done
wenzelm@19741
   499
wenzelm@19741
   500
lemma cancel_restrict_b: "reachable (restrict ioa acts) s = reachable ioa s"
wenzelm@19741
   501
apply (rule iffI)
wenzelm@19741
   502
apply (erule reachable.induct)
wenzelm@19741
   503
apply (simp add: cancel_restrict_a reachable_0)
wenzelm@19741
   504
apply (erule reachable_n)
wenzelm@19741
   505
apply (simp add: cancel_restrict_a)
wenzelm@19741
   506
(* <--  *)
wenzelm@19741
   507
apply (erule reachable.induct)
wenzelm@19741
   508
apply (rule reachable_0)
wenzelm@19741
   509
apply (simp add: cancel_restrict_a)
wenzelm@19741
   510
apply (erule reachable_n)
wenzelm@19741
   511
apply (simp add: cancel_restrict_a)
wenzelm@19741
   512
done
wenzelm@19741
   513
wenzelm@19741
   514
lemma acts_restrict: "act (restrict A acts) = act A"
wenzelm@19741
   515
apply (simp (no_asm) add: actions_def asig_internals_def
wenzelm@19741
   516
  asig_outputs_def asig_inputs_def externals_def asig_of_def restrict_def restrict_asig_def)
wenzelm@19741
   517
apply auto
wenzelm@19741
   518
done
wenzelm@19741
   519
wenzelm@19741
   520
lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) &      
wenzelm@19741
   521
          trans_of(restrict ioa acts) = trans_of(ioa) &  
wenzelm@19741
   522
          reachable (restrict ioa acts) s = reachable ioa s &  
wenzelm@19741
   523
          act (restrict A acts) = act A"
wenzelm@19741
   524
  apply (simp (no_asm) add: cancel_restrict_a cancel_restrict_b acts_restrict)
wenzelm@19741
   525
  done
wenzelm@19741
   526
wenzelm@19741
   527
wenzelm@19741
   528
subsection "rename"
wenzelm@19741
   529
wenzelm@19741
   530
lemma trans_rename: "s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)"
wenzelm@19741
   531
apply (simp add: Let_def rename_def trans_of_def)
wenzelm@19741
   532
done
wenzelm@19741
   533
wenzelm@19741
   534
wenzelm@19741
   535
lemma reachable_rename: "[| reachable (rename C g) s |] ==> reachable C s"
wenzelm@19741
   536
apply (erule reachable.induct)
wenzelm@19741
   537
apply (rule reachable_0)
wenzelm@19741
   538
apply (simp add: rename_def ioa_projections)
wenzelm@19741
   539
apply (drule trans_rename)
wenzelm@19741
   540
apply (erule exE)
wenzelm@19741
   541
apply (erule conjE)
wenzelm@19741
   542
apply (erule reachable_n)
wenzelm@19741
   543
apply assumption
wenzelm@19741
   544
done
wenzelm@19741
   545
wenzelm@19741
   546
wenzelm@19741
   547
subsection "trans_of(A||B)"
wenzelm@19741
   548
wenzelm@19741
   549
wenzelm@19741
   550
lemma trans_A_proj: "[|(s,a,t):trans_of (A||B); a:act A|]  
wenzelm@19741
   551
              ==> (fst s,a,fst t):trans_of A"
wenzelm@19741
   552
apply (simp add: Let_def par_def trans_of_def)
wenzelm@19741
   553
done
wenzelm@19741
   554
wenzelm@19741
   555
lemma trans_B_proj: "[|(s,a,t):trans_of (A||B); a:act B|]  
wenzelm@19741
   556
              ==> (snd s,a,snd t):trans_of B"
wenzelm@19741
   557
apply (simp add: Let_def par_def trans_of_def)
wenzelm@19741
   558
done
wenzelm@19741
   559
wenzelm@19741
   560
lemma trans_A_proj2: "[|(s,a,t):trans_of (A||B); a~:act A|] 
wenzelm@19741
   561
              ==> fst s = fst t"
wenzelm@19741
   562
apply (simp add: Let_def par_def trans_of_def)
wenzelm@19741
   563
done
wenzelm@19741
   564
wenzelm@19741
   565
lemma trans_B_proj2: "[|(s,a,t):trans_of (A||B); a~:act B|] 
wenzelm@19741
   566
              ==> snd s = snd t"
wenzelm@19741
   567
apply (simp add: Let_def par_def trans_of_def)
wenzelm@19741
   568
done
wenzelm@19741
   569
wenzelm@19741
   570
lemma trans_AB_proj: "(s,a,t):trans_of (A||B)  
wenzelm@19741
   571
               ==> a :act A | a :act B"
wenzelm@19741
   572
apply (simp add: Let_def par_def trans_of_def)
wenzelm@19741
   573
done
wenzelm@19741
   574
wenzelm@19741
   575
lemma trans_AB: "[|a:act A;a:act B; 
wenzelm@19741
   576
       (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|] 
wenzelm@19741
   577
   ==> (s,a,t):trans_of (A||B)"
wenzelm@19741
   578
apply (simp add: Let_def par_def trans_of_def)
wenzelm@19741
   579
done
wenzelm@19741
   580
wenzelm@19741
   581
lemma trans_A_notB: "[|a:act A;a~:act B; 
wenzelm@19741
   582
       (fst s,a,fst t):trans_of A;snd s=snd t|] 
wenzelm@19741
   583
   ==> (s,a,t):trans_of (A||B)"
wenzelm@19741
   584
apply (simp add: Let_def par_def trans_of_def)
wenzelm@19741
   585
done
wenzelm@19741
   586
wenzelm@19741
   587
lemma trans_notA_B: "[|a~:act A;a:act B; 
wenzelm@19741
   588
       (snd s,a,snd t):trans_of B;fst s=fst t|] 
wenzelm@19741
   589
   ==> (s,a,t):trans_of (A||B)"
wenzelm@19741
   590
apply (simp add: Let_def par_def trans_of_def)
wenzelm@19741
   591
done
wenzelm@19741
   592
wenzelm@19741
   593
lemmas trans_of_defs1 = trans_AB trans_A_notB trans_notA_B
wenzelm@19741
   594
  and trans_of_defs2 = trans_A_proj trans_B_proj trans_A_proj2 trans_B_proj2 trans_AB_proj
wenzelm@19741
   595
wenzelm@19741
   596
wenzelm@19741
   597
lemma trans_of_par4: 
wenzelm@19741
   598
"((s,a,t) : trans_of(A || B || C || D)) =                                     
wenzelm@19741
   599
  ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |   
wenzelm@19741
   600
    a:actions(asig_of(D))) &                                                  
wenzelm@19741
   601
   (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)               
wenzelm@19741
   602
    else fst t=fst s) &                                                       
wenzelm@19741
   603
   (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B)     
wenzelm@19741
   604
    else fst(snd(t))=fst(snd(s))) &                                           
wenzelm@19741
   605
   (if a:actions(asig_of(C)) then                                             
wenzelm@19741
   606
      (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)                       
wenzelm@19741
   607
    else fst(snd(snd(t)))=fst(snd(snd(s)))) &                                 
wenzelm@19741
   608
   (if a:actions(asig_of(D)) then                                             
wenzelm@19741
   609
      (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                       
wenzelm@19741
   610
    else snd(snd(snd(t)))=snd(snd(snd(s)))))"
huffman@44066
   611
  apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections)
wenzelm@19741
   612
  done
wenzelm@19741
   613
wenzelm@19741
   614
wenzelm@19741
   615
subsection "proof obligation generator for IOA requirements"
wenzelm@19741
   616
wenzelm@19741
   617
(* without assumptions on A and B because is_trans_of is also incorporated in ||def *)
wenzelm@19741
   618
lemma is_trans_of_par: "is_trans_of (A||B)"
wenzelm@19741
   619
apply (unfold is_trans_of_def)
wenzelm@19741
   620
apply (simp add: Let_def actions_of_par trans_of_par)
wenzelm@19741
   621
done
wenzelm@19741
   622
wenzelm@19741
   623
lemma is_trans_of_restrict: 
wenzelm@19741
   624
"is_trans_of A ==> is_trans_of (restrict A acts)"
wenzelm@19741
   625
apply (unfold is_trans_of_def)
wenzelm@19741
   626
apply (simp add: cancel_restrict acts_restrict)
wenzelm@19741
   627
done
wenzelm@19741
   628
wenzelm@19741
   629
lemma is_trans_of_rename: 
wenzelm@19741
   630
"is_trans_of A ==> is_trans_of (rename A f)"
wenzelm@19741
   631
apply (unfold is_trans_of_def restrict_def restrict_asig_def)
wenzelm@19741
   632
apply (simp add: Let_def actions_def trans_of_def asig_internals_def
wenzelm@19741
   633
  asig_outputs_def asig_inputs_def externals_def asig_of_def rename_def rename_set_def)
wenzelm@19741
   634
apply blast
wenzelm@19741
   635
done
wenzelm@19741
   636
wenzelm@19741
   637
lemma is_asig_of_par: "[| is_asig_of A; is_asig_of B; compatible A B|]   
wenzelm@19741
   638
          ==> is_asig_of (A||B)"
wenzelm@19741
   639
apply (simp add: is_asig_of_def asig_of_par asig_comp_def compatible_def
wenzelm@19741
   640
  asig_internals_def asig_outputs_def asig_inputs_def actions_def is_asig_def)
wenzelm@19741
   641
apply (simp add: asig_of_def)
wenzelm@19741
   642
apply auto
wenzelm@19741
   643
done
wenzelm@19741
   644
wenzelm@19741
   645
lemma is_asig_of_restrict: 
wenzelm@19741
   646
"is_asig_of A ==> is_asig_of (restrict A f)"
wenzelm@19741
   647
apply (unfold is_asig_of_def is_asig_def asig_of_def restrict_def restrict_asig_def 
wenzelm@19741
   648
           asig_internals_def asig_outputs_def asig_inputs_def externals_def o_def)
wenzelm@19741
   649
apply simp
wenzelm@19741
   650
apply auto
wenzelm@19741
   651
done
wenzelm@19741
   652
wenzelm@19741
   653
lemma is_asig_of_rename: "is_asig_of A ==> is_asig_of (rename A f)"
wenzelm@19741
   654
apply (simp add: is_asig_of_def rename_def rename_set_def asig_internals_def
wenzelm@19741
   655
  asig_outputs_def asig_inputs_def actions_def is_asig_def asig_of_def)
wenzelm@19741
   656
apply auto
wenzelm@19741
   657
apply (drule_tac [!] s = "Some ?x" in sym)
wenzelm@19741
   658
apply auto
wenzelm@19741
   659
done
wenzelm@19741
   660
wenzelm@19741
   661
lemmas [simp] = is_asig_of_par is_asig_of_restrict
wenzelm@19741
   662
  is_asig_of_rename is_trans_of_par is_trans_of_restrict is_trans_of_rename
wenzelm@19741
   663
wenzelm@19741
   664
wenzelm@19741
   665
lemma compatible_par: 
wenzelm@19741
   666
"[|compatible A B; compatible A C |]==> compatible A (B||C)"
wenzelm@19741
   667
apply (unfold compatible_def)
wenzelm@19741
   668
apply (simp add: internals_of_par outputs_of_par actions_of_par)
wenzelm@19741
   669
apply auto
wenzelm@19741
   670
done
wenzelm@19741
   671
wenzelm@19741
   672
(*  better derive by previous one and compat_commute *)
wenzelm@19741
   673
lemma compatible_par2: 
wenzelm@19741
   674
"[|compatible A C; compatible B C |]==> compatible (A||B) C"
wenzelm@19741
   675
apply (unfold compatible_def)
wenzelm@19741
   676
apply (simp add: internals_of_par outputs_of_par actions_of_par)
wenzelm@19741
   677
apply auto
wenzelm@19741
   678
done
wenzelm@19741
   679
wenzelm@19741
   680
lemma compatible_restrict: 
wenzelm@19741
   681
"[| compatible A B; (ext B - S) Int ext A = {}|]  
wenzelm@19741
   682
      ==> compatible A (restrict B S)"
wenzelm@19741
   683
apply (unfold compatible_def)
wenzelm@19741
   684
apply (simp add: ioa_triple_proj asig_triple_proj externals_def
wenzelm@19741
   685
  restrict_def restrict_asig_def actions_def)
wenzelm@19741
   686
apply auto
wenzelm@19741
   687
done
wenzelm@19741
   688
wenzelm@19741
   689
wenzelm@19741
   690
declare split_paired_Ex [simp]
mueller@3071
   691
mueller@3071
   692
end