src/HOLCF/IOA/meta_theory/Traces.ML
changeset 5068 fb28eaa07e01
parent 4815 b8a32ef742d9
child 7229 6773ba0c36d5
equal deleted inserted replaced
5067:62b6288e6005 5068:fb28eaa07e01
    24 (* ---------------------------------------------------------------- *)
    24 (* ---------------------------------------------------------------- *)
    25 (*                               filter_act                         *)
    25 (*                               filter_act                         *)
    26 (* ---------------------------------------------------------------- *)
    26 (* ---------------------------------------------------------------- *)
    27 
    27 
    28 
    28 
    29 goal thy  "filter_act`UU = UU";
    29 Goal  "filter_act`UU = UU";
    30 by (simp_tac (simpset() addsimps [filter_act_def]) 1);
    30 by (simp_tac (simpset() addsimps [filter_act_def]) 1);
    31 qed"filter_act_UU";
    31 qed"filter_act_UU";
    32 
    32 
    33 goal thy  "filter_act`nil = nil";
    33 Goal  "filter_act`nil = nil";
    34 by (simp_tac (simpset() addsimps [filter_act_def]) 1);
    34 by (simp_tac (simpset() addsimps [filter_act_def]) 1);
    35 qed"filter_act_nil";
    35 qed"filter_act_nil";
    36 
    36 
    37 goal thy "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
    37 Goal "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
    38 by (simp_tac (simpset() addsimps [filter_act_def]) 1);
    38 by (simp_tac (simpset() addsimps [filter_act_def]) 1);
    39 qed"filter_act_cons";
    39 qed"filter_act_cons";
    40 
    40 
    41 Addsimps [filter_act_UU,filter_act_nil,filter_act_cons];
    41 Addsimps [filter_act_UU,filter_act_nil,filter_act_cons];
    42 
    42 
    43 
    43 
    44 (* ---------------------------------------------------------------- *)
    44 (* ---------------------------------------------------------------- *)
    45 (*                             mk_trace                             *)
    45 (*                             mk_trace                             *)
    46 (* ---------------------------------------------------------------- *)
    46 (* ---------------------------------------------------------------- *)
    47 
    47 
    48 goal thy "mk_trace A`UU=UU";
    48 Goal "mk_trace A`UU=UU";
    49 by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
    49 by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
    50 qed"mk_trace_UU";
    50 qed"mk_trace_UU";
    51 
    51 
    52 goal thy "mk_trace A`nil=nil";
    52 Goal "mk_trace A`nil=nil";
    53 by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
    53 by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
    54 qed"mk_trace_nil";
    54 qed"mk_trace_nil";
    55 
    55 
    56 goal thy "mk_trace A`(at >> xs) =    \
    56 Goal "mk_trace A`(at >> xs) =    \
    57 \            (if ((fst at):ext A)    \       
    57 \            (if ((fst at):ext A)    \       
    58 \                 then (fst at) >> (mk_trace A`xs) \   
    58 \                 then (fst at) >> (mk_trace A`xs) \   
    59 \                 else mk_trace A`xs)";
    59 \                 else mk_trace A`xs)";
    60 
    60 
    61 by (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1);
    61 by (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1);
    66 (* ---------------------------------------------------------------- *)
    66 (* ---------------------------------------------------------------- *)
    67 (*                             is_exec_fragC                             *)
    67 (*                             is_exec_fragC                             *)
    68 (* ---------------------------------------------------------------- *)
    68 (* ---------------------------------------------------------------- *)
    69 
    69 
    70 
    70 
    71 goal thy "is_exec_fragC A = (LAM ex. (%s. case ex of \
    71 Goal "is_exec_fragC A = (LAM ex. (%s. case ex of \
    72 \      nil => TT \
    72 \      nil => TT \
    73 \    | x##xs => (flift1 \ 
    73 \    | x##xs => (flift1 \ 
    74 \            (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
    74 \            (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
    75 \             `x) \
    75 \             `x) \
    76 \   ))";
    76 \   ))";
    79 by (rtac is_exec_fragC_def 1);
    79 by (rtac is_exec_fragC_def 1);
    80 by (rtac beta_cfun 1);
    80 by (rtac beta_cfun 1);
    81 by (simp_tac (simpset() addsimps [flift1_def]) 1);
    81 by (simp_tac (simpset() addsimps [flift1_def]) 1);
    82 qed"is_exec_fragC_unfold";
    82 qed"is_exec_fragC_unfold";
    83 
    83 
    84 goal thy "(is_exec_fragC A`UU) s=UU";
    84 Goal "(is_exec_fragC A`UU) s=UU";
    85 by (stac is_exec_fragC_unfold 1);
    85 by (stac is_exec_fragC_unfold 1);
    86 by (Simp_tac 1);
    86 by (Simp_tac 1);
    87 qed"is_exec_fragC_UU";
    87 qed"is_exec_fragC_UU";
    88 
    88 
    89 goal thy "(is_exec_fragC A`nil) s = TT";
    89 Goal "(is_exec_fragC A`nil) s = TT";
    90 by (stac is_exec_fragC_unfold 1);
    90 by (stac is_exec_fragC_unfold 1);
    91 by (Simp_tac 1);
    91 by (Simp_tac 1);
    92 qed"is_exec_fragC_nil";
    92 qed"is_exec_fragC_nil";
    93 
    93 
    94 goal thy "(is_exec_fragC A`(pr>>xs)) s = \
    94 Goal "(is_exec_fragC A`(pr>>xs)) s = \
    95 \                        (Def ((s,pr):trans_of A) \
    95 \                        (Def ((s,pr):trans_of A) \
    96 \                andalso (is_exec_fragC A`xs)(snd pr))";
    96 \                andalso (is_exec_fragC A`xs)(snd pr))";
    97 by (rtac trans 1);
    97 by (rtac trans 1);
    98 by (stac is_exec_fragC_unfold 1);
    98 by (stac is_exec_fragC_unfold 1);
    99 by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
    99 by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
   106 
   106 
   107 (* ---------------------------------------------------------------- *)
   107 (* ---------------------------------------------------------------- *)
   108 (*                        is_exec_frag                              *)
   108 (*                        is_exec_frag                              *)
   109 (* ---------------------------------------------------------------- *)
   109 (* ---------------------------------------------------------------- *)
   110 
   110 
   111 goal thy "is_exec_frag A (s, UU)";
   111 Goal "is_exec_frag A (s, UU)";
   112 by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
   112 by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
   113 qed"is_exec_frag_UU";
   113 qed"is_exec_frag_UU";
   114 
   114 
   115 goal thy "is_exec_frag A (s, nil)";
   115 Goal "is_exec_frag A (s, nil)";
   116 by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
   116 by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
   117 qed"is_exec_frag_nil";
   117 qed"is_exec_frag_nil";
   118 
   118 
   119 goal thy "is_exec_frag A (s, (a,t)>>ex) = \
   119 Goal "is_exec_frag A (s, (a,t)>>ex) = \
   120 \                               (((s,a,t):trans_of A) & \
   120 \                               (((s,a,t):trans_of A) & \
   121 \                               is_exec_frag A (t, ex))";
   121 \                               is_exec_frag A (t, ex))";
   122 by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
   122 by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
   123 qed"is_exec_frag_cons";
   123 qed"is_exec_frag_cons";
   124 
   124 
   128 
   128 
   129 (* ---------------------------------------------------------------------------- *)
   129 (* ---------------------------------------------------------------------------- *)
   130                            section "laststate";
   130                            section "laststate";
   131 (* ---------------------------------------------------------------------------- *)
   131 (* ---------------------------------------------------------------------------- *)
   132 
   132 
   133 goal thy "laststate (s,UU) = s";
   133 Goal "laststate (s,UU) = s";
   134 by (simp_tac (simpset() addsimps [laststate_def]) 1); 
   134 by (simp_tac (simpset() addsimps [laststate_def]) 1); 
   135 qed"laststate_UU";
   135 qed"laststate_UU";
   136 
   136 
   137 goal thy "laststate (s,nil) = s";
   137 Goal "laststate (s,nil) = s";
   138 by (simp_tac (simpset() addsimps [laststate_def]) 1);
   138 by (simp_tac (simpset() addsimps [laststate_def]) 1);
   139 qed"laststate_nil";
   139 qed"laststate_nil";
   140 
   140 
   141 goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
   141 Goal "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
   142 by (simp_tac (simpset() addsimps [laststate_def]) 1);
   142 by (simp_tac (simpset() addsimps [laststate_def]) 1);
   143 by (case_tac "ex=nil" 1);
   143 by (case_tac "ex=nil" 1);
   144 by (Asm_simp_tac 1);
   144 by (Asm_simp_tac 1);
   145 by (Asm_simp_tac 1);
   145 by (Asm_simp_tac 1);
   146 by (dtac (Finite_Last1 RS mp) 1);
   146 by (dtac (Finite_Last1 RS mp) 1);
   148 by (def_tac 1);
   148 by (def_tac 1);
   149 qed"laststate_cons";
   149 qed"laststate_cons";
   150 
   150 
   151 Addsimps [laststate_UU,laststate_nil,laststate_cons];
   151 Addsimps [laststate_UU,laststate_nil,laststate_cons];
   152 
   152 
   153 goal thy "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)";
   153 Goal "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)";
   154 by (Seq_Finite_induct_tac 1);
   154 by (Seq_Finite_induct_tac 1);
   155 qed"exists_laststate";
   155 qed"exists_laststate";
   156 
   156 
   157 
   157 
   158 (* -------------------------------------------------------------------------------- *)
   158 (* -------------------------------------------------------------------------------- *)
   160 section "has_trace, mk_trace";
   160 section "has_trace, mk_trace";
   161 
   161 
   162 (* alternative definition of has_trace tailored for the refinement proof, as it does not 
   162 (* alternative definition of has_trace tailored for the refinement proof, as it does not 
   163    take the detour of schedules *)
   163    take the detour of schedules *)
   164 
   164 
   165 goalw thy  [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def] 
   165 Goalw  [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def] 
   166 "has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))";
   166 "has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))";
   167 
   167 
   168 by (safe_tac set_cs);
   168 by (safe_tac set_cs);
   169 (* 1 *)
   169 (* 1 *)
   170 by (res_inst_tac[("x","ex")] bexI 1);
   170 by (res_inst_tac[("x","ex")] bexI 1);
   191 (* All executions of A have only actions of A. This is only true because of the 
   191 (* All executions of A have only actions of A. This is only true because of the 
   192    predicate state_trans (part of the predicate IOA): We have no dependent types.
   192    predicate state_trans (part of the predicate IOA): We have no dependent types.
   193    For executions of parallel automata this assumption is not needed, as in par_def
   193    For executions of parallel automata this assumption is not needed, as in par_def
   194    this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *)
   194    this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *)
   195 
   195 
   196 goal thy 
   196 Goal 
   197   "!! A. is_trans_of A ==> \
   197   "!! A. is_trans_of A ==> \
   198 \ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act`xs)";
   198 \ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act`xs)";
   199 
   199 
   200 by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
   200 by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
   201 (* main case *)
   201 (* main case *)
   202 ren "ss a t" 1;
   202 ren "ss a t" 1;
   203 by (safe_tac set_cs);
   203 by (safe_tac set_cs);
   204 by (REPEAT (asm_full_simp_tac (simpset() addsimps [is_trans_of_def]) 1));
   204 by (REPEAT (asm_full_simp_tac (simpset() addsimps [is_trans_of_def]) 1));
   205 qed"execfrag_in_sig";
   205 qed"execfrag_in_sig";
   206 
   206 
   207 goal thy 
   207 Goal 
   208   "!! A.[|  is_trans_of A; x:executions A |] ==> \
   208   "!! A.[|  is_trans_of A; x:executions A |] ==> \
   209 \ Forall (%a. a:act A) (filter_act`(snd x))";
   209 \ Forall (%a. a:act A) (filter_act`(snd x))";
   210 
   210 
   211 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   211 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   212 by (pair_tac "x" 1);
   212 by (pair_tac "x" 1);
   213 by (rtac (execfrag_in_sig RS spec RS mp) 1);
   213 by (rtac (execfrag_in_sig RS spec RS mp) 1);
   214 by Auto_tac;
   214 by Auto_tac;
   215 qed"exec_in_sig";
   215 qed"exec_in_sig";
   216 
   216 
   217 goalw thy [schedules_def,has_schedule_def]
   217 Goalw [schedules_def,has_schedule_def]
   218   "!! A.[|  is_trans_of A; x:schedules A |] ==> \
   218   "!! A.[|  is_trans_of A; x:schedules A |] ==> \
   219 \   Forall (%a. a:act A) x";
   219 \   Forall (%a. a:act A) x";
   220 
   220 
   221 by (fast_tac (claset() addSIs [exec_in_sig]) 1);
   221 by (fast_tac (claset() addSIs [exec_in_sig]) 1);
   222 qed"scheds_in_sig";
   222 qed"scheds_in_sig";
   223 
   223 
   224 (*
   224 (*
   225 
   225 
   226 is ok but needs ForallQFilterP which has to been proven first (is trivial also)
   226 is ok but needs ForallQFilterP which has to been proven first (is trivial also)
   227 
   227 
   228 goalw thy [traces_def,has_trace_def]
   228 Goalw [traces_def,has_trace_def]
   229   "!! A.[| x:traces A |] ==> \
   229   "!! A.[| x:traces A |] ==> \
   230 \   Forall (%a. a:act A) x";
   230 \   Forall (%a. a:act A) x";
   231  by (safe_tac set_cs );
   231  by (safe_tac set_cs );
   232 by (rtac ForallQFilterP 1);
   232 by (rtac ForallQFilterP 1);
   233 by (fast_tac (!claset addSIs [ext_is_act]) 1);
   233 by (fast_tac (!claset addSIs [ext_is_act]) 1);
   238 (* -------------------------------------------------------------------------------- *)
   238 (* -------------------------------------------------------------------------------- *)
   239 
   239 
   240 section "executions are prefix closed";
   240 section "executions are prefix closed";
   241 
   241 
   242 (* only admissible in y, not if done in x !! *)
   242 (* only admissible in y, not if done in x !! *)
   243 goal thy "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)";
   243 Goal "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)";
   244 by (pair_induct_tac "y" [is_exec_frag_def] 1);
   244 by (pair_induct_tac "y" [is_exec_frag_def] 1);
   245 by (strip_tac 1);
   245 by (strip_tac 1);
   246 by (Seq_case_simp_tac "xa" 1);
   246 by (Seq_case_simp_tac "xa" 1);
   247 by (pair_tac "a" 1);
   247 by (pair_tac "a" 1);
   248 by Auto_tac;
   248 by Auto_tac;
   251 bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
   251 bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
   252 
   252 
   253 
   253 
   254 (* second prefix notion for Finite x *)
   254 (* second prefix notion for Finite x *)
   255 
   255 
   256 goal thy "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
   256 Goal "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
   257 by (pair_induct_tac "x" [is_exec_frag_def] 1);
   257 by (pair_induct_tac "x" [is_exec_frag_def] 1);
   258 by (strip_tac 1);
   258 by (strip_tac 1);
   259 by (Seq_case_simp_tac "s" 1);
   259 by (Seq_case_simp_tac "s" 1);
   260 by (pair_tac "a" 1);
   260 by (pair_tac "a" 1);
   261 by Auto_tac;
   261 by Auto_tac;