src/HOLCF/IOA/meta_theory/Traces.ML
author paulson
Mon, 23 Jun 1997 10:42:03 +0200
changeset 3457 a8ab7c64817c
parent 3433 2de17c994071
child 3521 bdc51b4c6050
permissions -rw-r--r--
Ran expandshort
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     1
(*  Title:      HOLCF/IOA/meta_theory/Traces.ML
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
     2
    ID:         $Id$
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     3
    Author:     Olaf M"uller
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     4
    Copyright   1996  TU Muenchen
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     5
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     6
Theorems about Executions and Traces of I/O automata in HOLCF.
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     7
*)   
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     8
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
     9
Delsimps (ex_simps @ all_simps);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    10
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    11
val exec_rws = [executions_def,is_exec_frag_def];
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    12
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    13
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    14
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    15
(* ----------------------------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    16
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    17
section "recursive equations of operators";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    18
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    19
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    20
(* ---------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    21
(*                               filter_act                         *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    22
(* ---------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    23
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    24
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    25
goal thy  "filter_act`UU = UU";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    26
by (simp_tac (!simpset addsimps [filter_act_def]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    27
qed"filter_act_UU";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    28
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    29
goal thy  "filter_act`nil = nil";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    30
by (simp_tac (!simpset addsimps [filter_act_def]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    31
qed"filter_act_nil";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    32
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    33
goal thy "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    34
by (simp_tac (!simpset addsimps [filter_act_def]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    35
qed"filter_act_cons";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    36
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    37
Addsimps [filter_act_UU,filter_act_nil,filter_act_cons];
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    38
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    39
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    40
(* ---------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    41
(*                             mk_trace                             *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    42
(* ---------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    43
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    44
goal thy "mk_trace A`UU=UU";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    45
by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    46
qed"mk_trace_UU";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    47
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    48
goal thy "mk_trace A`nil=nil";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    49
by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    50
qed"mk_trace_nil";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    51
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    52
goal thy "mk_trace A`(at >> xs) =    \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    53
\            (if ((fst at):ext A)    \       
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    54
\                 then (fst at) >> (mk_trace A`xs) \   
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    55
\                 else mk_trace A`xs)";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    56
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    57
by (asm_full_simp_tac (!simpset addsimps [mk_trace_def]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    58
qed"mk_trace_cons";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    59
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    60
Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons];
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    61
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    62
(* ---------------------------------------------------------------- *)
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    63
(*                             is_exec_fragC                             *)
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    64
(* ---------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    65
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    66
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    67
goal thy "is_exec_fragC A = (LAM ex. (%s. case ex of \
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    68
\      nil => TT \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    69
\    | x##xs => (flift1 \ 
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    70
\            (%p.Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    71
\             `x) \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    72
\   ))";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    73
by (rtac trans 1);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
    74
by (rtac fix_eq2 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
    75
by (rtac is_exec_fragC_def 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
    76
by (rtac beta_cfun 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    77
by (simp_tac (!simpset addsimps [flift1_def]) 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    78
qed"is_exec_fragC_unfold";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    79
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    80
goal thy "(is_exec_fragC A`UU) s=UU";
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    81
by (stac is_exec_fragC_unfold 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    82
by (Simp_tac 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    83
qed"is_exec_fragC_UU";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    84
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    85
goal thy "(is_exec_fragC A`nil) s = TT";
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    86
by (stac is_exec_fragC_unfold 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    87
by (Simp_tac 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    88
qed"is_exec_fragC_nil";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    89
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    90
goal thy "(is_exec_fragC A`(pr>>xs)) s = \
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    91
\                        (Def ((s,pr):trans_of A) \
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    92
\                andalso (is_exec_fragC A`xs)(snd pr))";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
    93
by (rtac trans 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    94
by (stac is_exec_fragC_unfold 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    95
by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    96
by (Simp_tac 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    97
qed"is_exec_fragC_cons";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    98
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    99
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   100
Addsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons];
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   101
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   102
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   103
(* ---------------------------------------------------------------- *)
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   104
(*                        is_exec_frag                              *)
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   105
(* ---------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   106
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   107
goal thy "is_exec_frag A (s, UU)";
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   108
by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   109
qed"is_exec_frag_UU";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   110
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   111
goal thy "is_exec_frag A (s, nil)";
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   112
by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   113
qed"is_exec_frag_nil";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   114
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   115
goal thy "is_exec_frag A (s, (a,t)>>ex) = \
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   116
\                               (((s,a,t):trans_of A) & \
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   117
\                               is_exec_frag A (t, ex))";
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   118
by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   119
qed"is_exec_frag_cons";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   120
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   121
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   122
(* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *)
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   123
Addsimps [is_exec_frag_UU,is_exec_frag_nil, is_exec_frag_cons];  
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   124
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   125
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   126
(* -------------------------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   127
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   128
section "has_trace, mk_trace";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   129
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   130
(* alternative definition of has_trace tailored for the refinement proof, as it does not 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   131
   take the detour of schedules *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   132
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   133
goalw thy  [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def] 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   134
"has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   135
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   136
by (safe_tac set_cs);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   137
(* 1 *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   138
by (res_inst_tac[("x","ex")] bexI 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   139
by (stac beta_cfun 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   140
by (cont_tacR 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   141
by (Simp_tac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   142
by (Asm_simp_tac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   143
(* 2 *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   144
by (res_inst_tac[("x","filter_act`(snd ex)")] bexI 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   145
by (stac beta_cfun 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   146
by (cont_tacR 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   147
by (Simp_tac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   148
by (safe_tac set_cs);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   149
by (res_inst_tac[("x","ex")] bexI 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   150
by (REPEAT (Asm_simp_tac 1));
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   151
qed"has_trace_def2";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   152
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   153
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   154
(* -------------------------------------------------------------------------------- *)
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   155
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   156
section "signatures and executions, schedules";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   157
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   158
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   159
(* All executions of A have only actions of A. This is only true because of the 
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   160
   predicate state_trans (part of the predicate IOA): We have no dependent types.
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   161
   For executions of parallel automata this assumption is not needed, as in par_def
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   162
   this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *)
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   163
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   164
goal thy 
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   165
  "!! A. IOA A ==> \
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   166
\ ! s. is_exec_frag A (s,xs) --> Forall (%a.a:act A) (filter_act`xs)";
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   167
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   168
by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   169
(* main case *)
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   170
ren "ss a t" 1;
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   171
by (safe_tac set_cs);
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   172
by (REPEAT (asm_full_simp_tac (!simpset addsimps [ioa_def,state_trans_def]) 1));
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   173
qed"execfrag_in_sig";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   174
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   175
goal thy 
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   176
  "!! A.[|  IOA A; x:executions A |] ==> \
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   177
\ Forall (%a.a:act A) (filter_act`(snd x))";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   178
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   179
by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   180
by (pair_tac "x" 1);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   181
by (rtac (execfrag_in_sig RS spec RS mp) 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   182
by (Auto_tac());
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   183
qed"exec_in_sig";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   184
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   185
goalw thy [schedules_def,has_schedule_def]
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   186
  "!! A.[|  IOA A; x:schedules A |] ==> \
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   187
\   Forall (%a.a:act A) x";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   188
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   189
by (fast_tac (!claset addSIs [exec_in_sig]) 1);
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   190
qed"scheds_in_sig";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   191
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   192
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   193
(* -------------------------------------------------------------------------------- *)
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   194
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   195
section "executions are prefix closed";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   196
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   197
(* only admissible in y, not if done in x !! *)
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   198
goal thy "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)";
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   199
by (pair_induct_tac "y" [is_exec_frag_def] 1);
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   200
by (strip_tac 1);
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   201
by (Seq_case_simp_tac "xa" 1);
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   202
by (pair_tac "a" 1);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   203
by (Auto_tac());
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   204
qed"execfrag_prefixclosed";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   205
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   206
bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   207
3361
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   208
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   209
(* second prefix notion for Finite x *)
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   210
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   211
goal thy "! y s.is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   212
by (pair_induct_tac "x" [is_exec_frag_def] 1);
3361
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   213
by (strip_tac 1);
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   214
by (Seq_case_simp_tac "s" 1);
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   215
by (pair_tac "a" 1);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   216
by (Auto_tac());
3361
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   217
qed_spec_mp"exec_prefix2closed";
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   218