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