--- a/src/HOLCF/IOA/meta_theory/Traces.ML Mon Jan 12 17:26:34 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Mon Jan 12 17:48:23 1998 +0100
@@ -123,6 +123,34 @@
(* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *)
Addsimps [is_exec_frag_UU,is_exec_frag_nil, is_exec_frag_cons];
+(* ---------------------------------------------------------------------------- *)
+ section "laststate";
+(* ---------------------------------------------------------------------------- *)
+
+goal thy "laststate (s,UU) = s";
+by (simp_tac (simpset() addsimps [laststate_def]) 1);
+qed"laststate_UU";
+
+goal thy "laststate (s,nil) = s";
+by (simp_tac (simpset() addsimps [laststate_def]) 1);
+qed"laststate_nil";
+
+goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
+by (simp_tac (simpset() addsimps [laststate_def]) 1);
+by (case_tac "ex=nil" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (dtac (Finite_Last1 RS mp) 1);
+by (assume_tac 1);
+by (def_tac 1);
+qed"laststate_cons";
+
+Addsimps [laststate_UU,laststate_nil,laststate_cons];
+
+goal thy "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)";
+by (Seq_Finite_induct_tac 1);
+qed"exists_laststate";
+
(* -------------------------------------------------------------------------------- *)