src/HOLCF/IOA/meta_theory/Traces.ML
changeset 4559 8e604d885b54
parent 4536 74f7c556fd90
child 4815 b8a32ef742d9
equal deleted inserted replaced
4558:31becfd8d329 4559:8e604d885b54
   121 
   121 
   122 
   122 
   123 (* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *)
   123 (* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *)
   124 Addsimps [is_exec_frag_UU,is_exec_frag_nil, is_exec_frag_cons];  
   124 Addsimps [is_exec_frag_UU,is_exec_frag_nil, is_exec_frag_cons];  
   125 
   125 
       
   126 (* ---------------------------------------------------------------------------- *)
       
   127                            section "laststate";
       
   128 (* ---------------------------------------------------------------------------- *)
       
   129 
       
   130 goal thy "laststate (s,UU) = s";
       
   131 by (simp_tac (simpset() addsimps [laststate_def]) 1); 
       
   132 qed"laststate_UU";
       
   133 
       
   134 goal thy "laststate (s,nil) = s";
       
   135 by (simp_tac (simpset() addsimps [laststate_def]) 1);
       
   136 qed"laststate_nil";
       
   137 
       
   138 goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
       
   139 by (simp_tac (simpset() addsimps [laststate_def]) 1);
       
   140 by (case_tac "ex=nil" 1);
       
   141 by (Asm_simp_tac 1);
       
   142 by (Asm_simp_tac 1);
       
   143 by (dtac (Finite_Last1 RS mp) 1);
       
   144 by (assume_tac 1);
       
   145 by (def_tac 1);
       
   146 qed"laststate_cons";
       
   147 
       
   148 Addsimps [laststate_UU,laststate_nil,laststate_cons];
       
   149 
       
   150 goal thy "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)";
       
   151 by (Seq_Finite_induct_tac 1);
       
   152 qed"exists_laststate";
       
   153 
   126 
   154 
   127 (* -------------------------------------------------------------------------------- *)
   155 (* -------------------------------------------------------------------------------- *)
   128 
   156 
   129 section "has_trace, mk_trace";
   157 section "has_trace, mk_trace";
   130 
   158