src/HOLCF/IOA/meta_theory/Traces.thy
author wenzelm
Fri Mar 20 15:24:18 2009 +0100 (2009-03-20)
changeset 30607 c3d1590debd8
parent 27208 5fe899199f85
child 36452 d37c6eed8117
permissions -rw-r--r--
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/Traces.thy
wenzelm@12218
     2
    Author:     Olaf Müller
wenzelm@17233
     3
*)
mueller@3071
     4
wenzelm@17233
     5
header {* Executions and Traces of I/O automata in HOLCF *}
mueller@3071
     6
wenzelm@17233
     7
theory Traces
wenzelm@17233
     8
imports Sequence Automata
wenzelm@17233
     9
begin
mueller@3071
    10
wenzelm@17233
    11
defaultsort type
wenzelm@17233
    12
wenzelm@17233
    13
types
mueller@3071
    14
   ('a,'s)pairs            =    "('a * 's) Seq"
mueller@3071
    15
   ('a,'s)execution        =    "'s * ('a,'s)pairs"
mueller@3071
    16
   'a trace                =    "'a Seq"
mueller@3521
    17
mueller@3521
    18
   ('a,'s)execution_module = "('a,'s)execution set * 'a signature"
mueller@3521
    19
   'a schedule_module      = "'a trace set * 'a signature"
mueller@3521
    20
   'a trace_module         = "'a trace set * 'a signature"
wenzelm@17233
    21
mueller@3071
    22
consts
mueller@3071
    23
mueller@3071
    24
   (* Executions *)
mueller@3433
    25
wenzelm@17233
    26
  is_exec_fragC ::"('a,'s)ioa => ('a,'s)pairs -> 's => tr"
wenzelm@17233
    27
  is_exec_frag  ::"[('a,'s)ioa, ('a,'s)execution] => bool"
mueller@3071
    28
  has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool"
mueller@3071
    29
  executions    :: "('a,'s)ioa => ('a,'s)execution set"
mueller@3071
    30
mueller@3071
    31
  (* Schedules and traces *)
mueller@3071
    32
  filter_act    ::"('a,'s)pairs -> 'a trace"
wenzelm@17233
    33
  has_schedule  :: "[('a,'s)ioa, 'a trace] => bool"
mueller@3071
    34
  has_trace     :: "[('a,'s)ioa, 'a trace] => bool"
wenzelm@17233
    35
  schedules     :: "('a,'s)ioa => 'a trace set"
mueller@3071
    36
  traces        :: "('a,'s)ioa => 'a trace set"
mueller@3071
    37
  mk_trace      :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace"
mueller@3071
    38
mueller@4559
    39
  laststate    ::"('a,'s)execution => 's"
mueller@4559
    40
mueller@4559
    41
  (* A predicate holds infinitely (finitely) often in a sequence *)
mueller@4559
    42
mueller@4559
    43
  inf_often      ::"('a => bool) => 'a Seq => bool"
mueller@4559
    44
  fin_often      ::"('a => bool) => 'a Seq => bool"
mueller@4559
    45
mueller@4559
    46
  (* fairness of executions *)
mueller@4559
    47
mueller@4559
    48
  wfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
mueller@4559
    49
  sfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
mueller@4559
    50
  is_wfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
mueller@4559
    51
  is_sfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
mueller@4559
    52
  fair_ex        ::"('a,'s)ioa => ('a,'s)execution => bool"
mueller@4559
    53
mueller@4559
    54
  (* fair behavior sets *)
wenzelm@17233
    55
mueller@4559
    56
  fairexecutions ::"('a,'s)ioa => ('a,'s)execution set"
mueller@4559
    57
  fairtraces     ::"('a,'s)ioa => 'a trace set"
mueller@4559
    58
mueller@4559
    59
  (* Notions of implementation *)
wenzelm@22808
    60
  ioa_implements :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool"   (infixr "=<|" 12)
mueller@4559
    61
  fair_implements  :: "('a,'s1)ioa => ('a,'s2)ioa => bool"
mueller@3071
    62
mueller@3521
    63
  (* Execution, schedule and trace modules *)
mueller@3521
    64
  Execs         ::  "('a,'s)ioa => ('a,'s)execution_module"
mueller@3521
    65
  Scheds        ::  "('a,'s)ioa => 'a schedule_module"
mueller@3521
    66
  Traces        ::  "('a,'s)ioa => 'a trace_module"
mueller@3521
    67
mueller@3071
    68
mueller@3071
    69
defs
mueller@3071
    70
mueller@3071
    71
mueller@3071
    72
(*  ------------------- Executions ------------------------------ *)
mueller@3071
    73
mueller@3071
    74
wenzelm@17233
    75
is_exec_frag_def:
nipkow@10835
    76
  "is_exec_frag A ex ==  ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)"
mueller@3071
    77
mueller@3433
    78
wenzelm@17233
    79
is_exec_fragC_def:
wenzelm@17233
    80
  "is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of
mueller@3071
    81
      nil => TT
wenzelm@17233
    82
    | x##xs => (flift1
wenzelm@17233
    83
            (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p))
nipkow@10835
    84
             $x)
wenzelm@17233
    85
   )))"
mueller@3433
    86
mueller@3433
    87
mueller@3433
    88
wenzelm@17233
    89
executions_def:
wenzelm@17233
    90
  "executions ioa == {e. ((fst e) : starts_of(ioa)) &
mueller@3433
    91
                         is_exec_frag ioa e}"
mueller@3071
    92
mueller@3071
    93
mueller@3071
    94
(*  ------------------- Schedules ------------------------------ *)
mueller@3071
    95
mueller@3071
    96
wenzelm@17233
    97
filter_act_def:
mueller@3071
    98
  "filter_act == Map fst"
mueller@3071
    99
wenzelm@17233
   100
has_schedule_def:
wenzelm@17233
   101
  "has_schedule ioa sch ==
nipkow@10835
   102
     (? ex:executions ioa. sch = filter_act$(snd ex))"
mueller@3071
   103
wenzelm@17233
   104
schedules_def:
mueller@3071
   105
  "schedules ioa == {sch. has_schedule ioa sch}"
mueller@3071
   106
mueller@3071
   107
mueller@3071
   108
(*  ------------------- Traces ------------------------------ *)
mueller@3071
   109
wenzelm@17233
   110
has_trace_def:
wenzelm@17233
   111
  "has_trace ioa tr ==
nipkow@10835
   112
     (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)"
wenzelm@17233
   113
wenzelm@17233
   114
traces_def:
mueller@3071
   115
  "traces ioa == {tr. has_trace ioa tr}"
mueller@3071
   116
mueller@3071
   117
wenzelm@17233
   118
mk_trace_def:
wenzelm@17233
   119
  "mk_trace ioa == LAM tr.
nipkow@10835
   120
     Filter (%a. a:ext(ioa))$(filter_act$tr)"
mueller@3071
   121
mueller@3071
   122
mueller@4559
   123
(*  ------------------- Fair Traces ------------------------------ *)
mueller@4559
   124
wenzelm@17233
   125
laststate_def:
nipkow@10835
   126
  "laststate ex == case Last$(snd ex) of
wenzelm@12028
   127
                      UU  => fst ex
mueller@4559
   128
                    | Def at => snd at"
mueller@4559
   129
wenzelm@17233
   130
inf_often_def:
nipkow@10835
   131
  "inf_often P s == Infinite (Filter P$s)"
mueller@4559
   132
mueller@4559
   133
(*  filtering P yields a finite or partial sequence *)
wenzelm@17233
   134
fin_often_def:
mueller@4559
   135
  "fin_often P s == ~inf_often P s"
mueller@4559
   136
wenzelm@17233
   137
(* Note that partial execs cannot be wfair as the inf_often predicate in the
wenzelm@17233
   138
   else branch prohibits it. However they can be sfair in the case when all W
wenzelm@17233
   139
   are only finitely often enabled: Is this the right model?
mueller@5976
   140
   See LiveIOA for solution conforming with the literature and superseding this one *)
wenzelm@17233
   141
wfair_ex_def:
wenzelm@17233
   142
  "wfair_ex A ex == ! W : wfair_of A.
wenzelm@17233
   143
                      if   Finite (snd ex)
mueller@4559
   144
                      then ~Enabled A W (laststate ex)
mueller@4559
   145
                      else is_wfair A W ex"
mueller@4559
   146
wenzelm@17233
   147
is_wfair_def:
mueller@4559
   148
  "is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex)
mueller@4559
   149
                     | inf_often (%x.~Enabled A W (snd x)) (snd ex))"
mueller@4559
   150
wenzelm@17233
   151
sfair_ex_def:
mueller@4559
   152
  "sfair_ex A ex == ! W : sfair_of A.
wenzelm@17233
   153
                      if   Finite (snd ex)
mueller@4559
   154
                      then ~Enabled A W (laststate ex)
mueller@4559
   155
                      else is_sfair A W ex"
mueller@4559
   156
wenzelm@17233
   157
is_sfair_def:
mueller@4559
   158
  "is_sfair A W ex ==  (inf_often (%x. fst x:W) (snd ex)
mueller@4559
   159
                      | fin_often (%x. Enabled A W (snd x)) (snd ex))"
mueller@4559
   160
wenzelm@17233
   161
fair_ex_def:
mueller@4559
   162
  "fair_ex A ex == wfair_ex A ex & sfair_ex A ex"
mueller@4559
   163
wenzelm@17233
   164
fairexecutions_def:
mueller@4559
   165
  "fairexecutions A == {ex. ex:executions A & fair_ex A ex}"
mueller@4559
   166
wenzelm@17233
   167
fairtraces_def:
nipkow@10835
   168
  "fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}"
mueller@4559
   169
mueller@4559
   170
mueller@3071
   171
(*  ------------------- Implementation ------------------------------ *)
mueller@3071
   172
wenzelm@17233
   173
ioa_implements_def:
wenzelm@17233
   174
  "ioa1 =<| ioa2 ==
wenzelm@17233
   175
    (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
mueller@3071
   176
     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) &
mueller@3071
   177
      traces(ioa1) <= traces(ioa2))"
mueller@3071
   178
wenzelm@17233
   179
fair_implements_def:
mueller@4559
   180
  "fair_implements C A == inp(C) = inp(A) &  out(C)=out(A) &
mueller@4559
   181
                          fairtraces(C) <= fairtraces(A)"
mueller@4559
   182
mueller@3521
   183
(*  ------------------- Modules ------------------------------ *)
mueller@3521
   184
wenzelm@17233
   185
Execs_def:
mueller@3521
   186
  "Execs A  == (executions A, asig_of A)"
mueller@3521
   187
wenzelm@17233
   188
Scheds_def:
mueller@3521
   189
  "Scheds A == (schedules A, asig_of A)"
mueller@3521
   190
wenzelm@17233
   191
Traces_def:
mueller@3521
   192
  "Traces A == (traces A,asig_of A)"
mueller@3521
   193
wenzelm@19741
   194
wenzelm@19741
   195
lemmas [simp del] = ex_simps all_simps split_paired_Ex
wenzelm@19741
   196
declare Let_def [simp]
wenzelm@26339
   197
declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
wenzelm@19741
   198
wenzelm@19741
   199
lemmas exec_rws = executions_def is_exec_frag_def
wenzelm@19741
   200
wenzelm@19741
   201
wenzelm@19741
   202
wenzelm@19741
   203
subsection "recursive equations of operators"
wenzelm@19741
   204
wenzelm@19741
   205
(* ---------------------------------------------------------------- *)
wenzelm@19741
   206
(*                               filter_act                         *)
wenzelm@19741
   207
(* ---------------------------------------------------------------- *)
wenzelm@19741
   208
wenzelm@19741
   209
wenzelm@19741
   210
lemma filter_act_UU: "filter_act$UU = UU"
wenzelm@19741
   211
apply (simp add: filter_act_def)
wenzelm@19741
   212
done
wenzelm@19741
   213
wenzelm@19741
   214
lemma filter_act_nil: "filter_act$nil = nil"
wenzelm@19741
   215
apply (simp add: filter_act_def)
wenzelm@19741
   216
done
wenzelm@19741
   217
wenzelm@19741
   218
lemma filter_act_cons: "filter_act$(x>>xs) = (fst x) >> filter_act$xs"
wenzelm@19741
   219
apply (simp add: filter_act_def)
wenzelm@19741
   220
done
wenzelm@19741
   221
wenzelm@19741
   222
declare filter_act_UU [simp] filter_act_nil [simp] filter_act_cons [simp]
wenzelm@19741
   223
wenzelm@19741
   224
wenzelm@19741
   225
(* ---------------------------------------------------------------- *)
wenzelm@19741
   226
(*                             mk_trace                             *)
wenzelm@19741
   227
(* ---------------------------------------------------------------- *)
wenzelm@19741
   228
wenzelm@19741
   229
lemma mk_trace_UU: "mk_trace A$UU=UU"
wenzelm@19741
   230
apply (simp add: mk_trace_def)
wenzelm@19741
   231
done
wenzelm@19741
   232
wenzelm@19741
   233
lemma mk_trace_nil: "mk_trace A$nil=nil"
wenzelm@19741
   234
apply (simp add: mk_trace_def)
wenzelm@19741
   235
done
wenzelm@19741
   236
wenzelm@19741
   237
lemma mk_trace_cons: "mk_trace A$(at >> xs) =     
wenzelm@19741
   238
             (if ((fst at):ext A)            
wenzelm@19741
   239
                  then (fst at) >> (mk_trace A$xs)     
wenzelm@19741
   240
                  else mk_trace A$xs)"
wenzelm@19741
   241
wenzelm@19741
   242
apply (simp add: mk_trace_def)
wenzelm@19741
   243
done
wenzelm@19741
   244
wenzelm@19741
   245
declare mk_trace_UU [simp] mk_trace_nil [simp] mk_trace_cons [simp]
wenzelm@19741
   246
wenzelm@19741
   247
(* ---------------------------------------------------------------- *)
wenzelm@19741
   248
(*                             is_exec_fragC                             *)
wenzelm@19741
   249
(* ---------------------------------------------------------------- *)
wenzelm@19741
   250
wenzelm@19741
   251
wenzelm@19741
   252
lemma is_exec_fragC_unfold: "is_exec_fragC A = (LAM ex. (%s. case ex of  
wenzelm@19741
   253
       nil => TT  
wenzelm@19741
   254
     | x##xs => (flift1   
wenzelm@19741
   255
             (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p))  
wenzelm@19741
   256
              $x)  
wenzelm@19741
   257
    ))"
wenzelm@19741
   258
apply (rule trans)
wenzelm@19741
   259
apply (rule fix_eq2)
wenzelm@19741
   260
apply (rule is_exec_fragC_def)
wenzelm@19741
   261
apply (rule beta_cfun)
wenzelm@19741
   262
apply (simp add: flift1_def)
wenzelm@19741
   263
done
wenzelm@19741
   264
wenzelm@19741
   265
lemma is_exec_fragC_UU: "(is_exec_fragC A$UU) s=UU"
wenzelm@19741
   266
apply (subst is_exec_fragC_unfold)
wenzelm@19741
   267
apply simp
wenzelm@19741
   268
done
wenzelm@19741
   269
wenzelm@19741
   270
lemma is_exec_fragC_nil: "(is_exec_fragC A$nil) s = TT"
wenzelm@19741
   271
apply (subst is_exec_fragC_unfold)
wenzelm@19741
   272
apply simp
wenzelm@19741
   273
done
wenzelm@19741
   274
wenzelm@19741
   275
lemma is_exec_fragC_cons: "(is_exec_fragC A$(pr>>xs)) s =  
wenzelm@19741
   276
                         (Def ((s,pr):trans_of A)  
wenzelm@19741
   277
                 andalso (is_exec_fragC A$xs)(snd pr))"
wenzelm@19741
   278
apply (rule trans)
wenzelm@19741
   279
apply (subst is_exec_fragC_unfold)
wenzelm@19741
   280
apply (simp add: Consq_def flift1_def)
wenzelm@19741
   281
apply simp
wenzelm@19741
   282
done
wenzelm@19741
   283
wenzelm@19741
   284
wenzelm@19741
   285
declare is_exec_fragC_UU [simp] is_exec_fragC_nil [simp] is_exec_fragC_cons [simp]
wenzelm@19741
   286
wenzelm@19741
   287
wenzelm@19741
   288
(* ---------------------------------------------------------------- *)
wenzelm@19741
   289
(*                        is_exec_frag                              *)
wenzelm@19741
   290
(* ---------------------------------------------------------------- *)
wenzelm@19741
   291
wenzelm@19741
   292
lemma is_exec_frag_UU: "is_exec_frag A (s, UU)"
wenzelm@19741
   293
apply (simp add: is_exec_frag_def)
wenzelm@19741
   294
done
wenzelm@19741
   295
wenzelm@19741
   296
lemma is_exec_frag_nil: "is_exec_frag A (s, nil)"
wenzelm@19741
   297
apply (simp add: is_exec_frag_def)
wenzelm@19741
   298
done
wenzelm@19741
   299
wenzelm@19741
   300
lemma is_exec_frag_cons: "is_exec_frag A (s, (a,t)>>ex) =  
wenzelm@19741
   301
                                (((s,a,t):trans_of A) &  
wenzelm@19741
   302
                                is_exec_frag A (t, ex))"
wenzelm@19741
   303
apply (simp add: is_exec_frag_def)
wenzelm@19741
   304
done
wenzelm@19741
   305
wenzelm@19741
   306
wenzelm@19741
   307
(* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *)
wenzelm@19741
   308
declare is_exec_frag_UU [simp] is_exec_frag_nil [simp] is_exec_frag_cons [simp]
wenzelm@19741
   309
wenzelm@19741
   310
(* ---------------------------------------------------------------------------- *)
wenzelm@19741
   311
                           section "laststate"
wenzelm@19741
   312
(* ---------------------------------------------------------------------------- *)
wenzelm@19741
   313
wenzelm@19741
   314
lemma laststate_UU: "laststate (s,UU) = s"
wenzelm@19741
   315
apply (simp add: laststate_def)
wenzelm@19741
   316
done
wenzelm@19741
   317
wenzelm@19741
   318
lemma laststate_nil: "laststate (s,nil) = s"
wenzelm@19741
   319
apply (simp add: laststate_def)
wenzelm@19741
   320
done
wenzelm@19741
   321
wenzelm@19741
   322
lemma laststate_cons: "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)"
wenzelm@19741
   323
apply (simp (no_asm) add: laststate_def)
wenzelm@19741
   324
apply (case_tac "ex=nil")
wenzelm@19741
   325
apply (simp (no_asm_simp))
wenzelm@19741
   326
apply (simp (no_asm_simp))
wenzelm@19741
   327
apply (drule Finite_Last1 [THEN mp])
wenzelm@19741
   328
apply assumption
wenzelm@30607
   329
apply defined
wenzelm@19741
   330
done
wenzelm@19741
   331
wenzelm@19741
   332
declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp]
wenzelm@19741
   333
wenzelm@19741
   334
lemma exists_laststate: "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)"
wenzelm@27208
   335
apply (tactic "Seq_Finite_induct_tac @{context} 1")
wenzelm@19741
   336
done
wenzelm@19741
   337
wenzelm@19741
   338
wenzelm@19741
   339
subsection "has_trace, mk_trace"
wenzelm@19741
   340
wenzelm@19741
   341
(* alternative definition of has_trace tailored for the refinement proof, as it does not 
wenzelm@19741
   342
   take the detour of schedules *)
wenzelm@19741
   343
wenzelm@19741
   344
lemma has_trace_def2: 
wenzelm@19741
   345
"has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))"
wenzelm@19741
   346
apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def)
haftmann@26359
   347
apply auto
wenzelm@19741
   348
done
wenzelm@19741
   349
wenzelm@19741
   350
wenzelm@19741
   351
subsection "signatures and executions, schedules"
wenzelm@19741
   352
wenzelm@19741
   353
(* All executions of A have only actions of A. This is only true because of the 
wenzelm@19741
   354
   predicate state_trans (part of the predicate IOA): We have no dependent types.
wenzelm@19741
   355
   For executions of parallel automata this assumption is not needed, as in par_def
wenzelm@19741
   356
   this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *)
wenzelm@19741
   357
wenzelm@19741
   358
lemma execfrag_in_sig: 
wenzelm@19741
   359
  "!! A. is_trans_of A ==>  
wenzelm@19741
   360
  ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)"
wenzelm@27208
   361
apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
wenzelm@27208
   362
  @{thm Forall_def}, @{thm sforall_def}] 1 *})
wenzelm@19741
   363
(* main case *)
haftmann@26359
   364
apply (auto simp add: is_trans_of_def)
wenzelm@19741
   365
done
wenzelm@19741
   366
wenzelm@19741
   367
lemma exec_in_sig: 
wenzelm@19741
   368
  "!! A.[|  is_trans_of A; x:executions A |] ==>  
wenzelm@19741
   369
  Forall (%a. a:act A) (filter_act$(snd x))"
wenzelm@19741
   370
apply (simp add: executions_def)
wenzelm@27208
   371
apply (tactic {* pair_tac @{context} "x" 1 *})
wenzelm@19741
   372
apply (rule execfrag_in_sig [THEN spec, THEN mp])
wenzelm@19741
   373
apply auto
wenzelm@19741
   374
done
wenzelm@19741
   375
wenzelm@19741
   376
lemma scheds_in_sig: 
wenzelm@19741
   377
  "!! A.[|  is_trans_of A; x:schedules A |] ==>  
wenzelm@19741
   378
    Forall (%a. a:act A) x"
wenzelm@19741
   379
apply (unfold schedules_def has_schedule_def)
wenzelm@19741
   380
apply (fast intro!: exec_in_sig)
wenzelm@19741
   381
done
wenzelm@19741
   382
wenzelm@19741
   383
wenzelm@19741
   384
subsection "executions are prefix closed"
wenzelm@19741
   385
wenzelm@19741
   386
(* only admissible in y, not if done in x !! *)
wenzelm@19741
   387
lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)"
wenzelm@27208
   388
apply (tactic {* pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1 *})
wenzelm@19741
   389
apply (intro strip)
wenzelm@27208
   390
apply (tactic {* Seq_case_simp_tac @{context} "xa" 1 *})
wenzelm@27208
   391
apply (tactic {* pair_tac @{context} "a" 1 *})
wenzelm@19741
   392
apply auto
wenzelm@19741
   393
done
wenzelm@19741
   394
wenzelm@19741
   395
lemmas exec_prefixclosed =
wenzelm@19741
   396
  conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp], standard]
wenzelm@19741
   397
wenzelm@19741
   398
wenzelm@19741
   399
(* second prefix notion for Finite x *)
wenzelm@19741
   400
wenzelm@19741
   401
lemma exec_prefix2closed [rule_format]:
wenzelm@19741
   402
  "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)"
wenzelm@27208
   403
apply (tactic {* pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1 *})
wenzelm@19741
   404
apply (intro strip)
wenzelm@27208
   405
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
wenzelm@27208
   406
apply (tactic {* pair_tac @{context} "a" 1 *})
wenzelm@19741
   407
apply auto
wenzelm@19741
   408
done
wenzelm@19741
   409
wenzelm@17233
   410
end