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