src/HOLCF/IOA/meta_theory/Traces.ML
author oheimb
Thu, 08 Jan 1998 18:09:47 +0100
changeset 4536 74f7c556fd90
parent 4477 b3e5857d8d99
child 4559 8e604d885b54
permissions -rw-r--r--
added split_paired_Ex to the implicit simpset
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);
4536
74f7c556fd90 added split_paired_Ex to the implicit simpset
oheimb
parents: 4477
diff changeset
    10
Delsimps [split_paired_Ex];
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    11
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    12
val exec_rws = [executions_def,is_exec_frag_def];
3071
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
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    18
section "recursive equations of operators";
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
(* ---------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    22
(*                               filter_act                         *)
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
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    26
goal thy  "filter_act`UU = UU";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    27
by (simp_tac (simpset() addsimps [filter_act_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    28
qed"filter_act_UU";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    29
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    30
goal thy  "filter_act`nil = nil";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    31
by (simp_tac (simpset() addsimps [filter_act_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    32
qed"filter_act_nil";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    33
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    34
goal thy "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    35
by (simp_tac (simpset() addsimps [filter_act_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    36
qed"filter_act_cons";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    37
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    38
Addsimps [filter_act_UU,filter_act_nil,filter_act_cons];
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
(* ---------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    42
(*                             mk_trace                             *)
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
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    45
goal thy "mk_trace A`UU=UU";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    46
by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    47
qed"mk_trace_UU";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    48
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    49
goal thy "mk_trace A`nil=nil";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    50
by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    51
qed"mk_trace_nil";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    52
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    53
goal thy "mk_trace A`(at >> xs) =    \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    54
\            (if ((fst at):ext A)    \       
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    55
\                 then (fst at) >> (mk_trace A`xs) \   
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    56
\                 else mk_trace A`xs)";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    57
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    58
by (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    59
qed"mk_trace_cons";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    60
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    61
Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons];
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    62
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    63
(* ---------------------------------------------------------------- *)
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    64
(*                             is_exec_fragC                             *)
3071
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
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    67
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    68
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
    69
\      nil => TT \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    70
\    | x##xs => (flift1 \ 
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3521
diff changeset
    71
\            (%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
    72
\             `x) \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    73
\   ))";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    74
by (rtac trans 1);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
    75
by (rtac fix_eq2 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
    76
by (rtac is_exec_fragC_def 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
    77
by (rtac beta_cfun 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    78
by (simp_tac (simpset() addsimps [flift1_def]) 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    79
qed"is_exec_fragC_unfold";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    80
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    81
goal thy "(is_exec_fragC A`UU) s=UU";
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    82
by (stac is_exec_fragC_unfold 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    83
by (Simp_tac 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    84
qed"is_exec_fragC_UU";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    85
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    86
goal thy "(is_exec_fragC A`nil) s = TT";
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    87
by (stac is_exec_fragC_unfold 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    88
by (Simp_tac 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    89
qed"is_exec_fragC_nil";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    90
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    91
goal thy "(is_exec_fragC A`(pr>>xs)) s = \
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    92
\                        (Def ((s,pr):trans_of A) \
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    93
\                andalso (is_exec_fragC A`xs)(snd pr))";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
    94
by (rtac trans 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    95
by (stac is_exec_fragC_unfold 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    96
by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    97
by (Simp_tac 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
    98
qed"is_exec_fragC_cons";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    99
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   100
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   101
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
   102
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   103
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   104
(* ---------------------------------------------------------------- *)
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   105
(*                        is_exec_frag                              *)
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   106
(* ---------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   107
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   108
goal thy "is_exec_frag A (s, UU)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   109
by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   110
qed"is_exec_frag_UU";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   111
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   112
goal thy "is_exec_frag A (s, nil)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   113
by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   114
qed"is_exec_frag_nil";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   115
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   116
goal thy "is_exec_frag A (s, (a,t)>>ex) = \
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   117
\                               (((s,a,t):trans_of A) & \
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   118
\                               is_exec_frag A (t, ex))";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   119
by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   120
qed"is_exec_frag_cons";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   121
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   122
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   123
(* 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
   124
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
   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
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   129
section "has_trace, mk_trace";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   130
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   131
(* 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
   132
   take the detour of schedules *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   133
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   134
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
   135
"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
   136
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   137
by (safe_tac set_cs);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   138
(* 1 *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   139
by (res_inst_tac[("x","ex")] bexI 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   140
by (stac beta_cfun 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   141
by (cont_tacR 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   142
by (Simp_tac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   143
by (Asm_simp_tac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   144
(* 2 *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   145
by (res_inst_tac[("x","filter_act`(snd ex)")] bexI 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   146
by (stac beta_cfun 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   147
by (cont_tacR 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   148
by (Simp_tac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   149
by (safe_tac set_cs);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   150
by (res_inst_tac[("x","ex")] bexI 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   151
by (REPEAT (Asm_simp_tac 1));
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   152
qed"has_trace_def2";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   153
3275
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
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   157
section "signatures and executions, schedules";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   158
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   159
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   160
(* 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
   161
   predicate state_trans (part of the predicate IOA): We have no dependent types.
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   162
   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
   163
   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
   164
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   165
goal thy 
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   166
  "!! A. is_trans_of A ==> \
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3521
diff changeset
   167
\ ! 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
   168
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   169
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
   170
(* main case *)
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   171
ren "ss a t" 1;
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   172
by (safe_tac set_cs);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   173
by (REPEAT (asm_full_simp_tac (simpset() addsimps [is_trans_of_def]) 1));
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   174
qed"execfrag_in_sig";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   175
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   176
goal thy 
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   177
  "!! A.[|  is_trans_of A; x:executions A |] ==> \
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3521
diff changeset
   178
\ Forall (%a. a:act A) (filter_act`(snd x))";
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   179
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   180
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   181
by (pair_tac "x" 1);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   182
by (rtac (execfrag_in_sig RS spec RS mp) 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4423
diff changeset
   183
by Auto_tac;
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   184
qed"exec_in_sig";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   185
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   186
goalw thy [schedules_def,has_schedule_def]
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   187
  "!! A.[|  is_trans_of A; x:schedules A |] ==> \
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3521
diff changeset
   188
\   Forall (%a. a:act A) x";
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   189
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   190
by (fast_tac (claset() addSIs [exec_in_sig]) 1);
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   191
qed"scheds_in_sig";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   192
4283
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   193
(*
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   194
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   195
is ok but needs ForallQFilterP which has to been proven first (is trivial also)
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   196
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   197
goalw thy [traces_def,has_trace_def]
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   198
  "!! A.[| x:traces A |] ==> \
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   199
\   Forall (%a. a:act A) x";
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   200
 by (safe_tac set_cs );
4423
a129b817b58a expandshort;
wenzelm
parents: 4283
diff changeset
   201
by (rtac ForallQFilterP 1);
4283
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   202
by (fast_tac (!claset addSIs [ext_is_act]) 1);
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   203
qed"traces_in_sig";
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   204
*)
92707e24b62b managed merge details;
mueller
parents: 4098
diff changeset
   205
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   206
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   207
(* -------------------------------------------------------------------------------- *)
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   208
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   209
section "executions are prefix closed";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   210
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   211
(* only admissible in y, not if done in x !! *)
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   212
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
   213
by (pair_induct_tac "y" [is_exec_frag_def] 1);
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   214
by (strip_tac 1);
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   215
by (Seq_case_simp_tac "xa" 1);
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   216
by (pair_tac "a" 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4423
diff changeset
   217
by Auto_tac;
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   218
qed"execfrag_prefixclosed";
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   219
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
   220
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
   221
3361
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   222
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   223
(* second prefix notion for Finite x *)
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   224
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3521
diff changeset
   225
goal thy "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3361
diff changeset
   226
by (pair_induct_tac "x" [is_exec_frag_def] 1);
3361
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   227
by (strip_tac 1);
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   228
by (Seq_case_simp_tac "s" 1);
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   229
by (pair_tac "a" 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4423
diff changeset
   230
by Auto_tac;
3361
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   231
qed_spec_mp"exec_prefix2closed";
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
   232