another little bug ;-) and minor changes in TLS.*;

--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Oct 19 15:49:55 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Oct 19 16:13:13 1998 +0200
@@ -492,15 +492,8 @@
 by Auto_tac;
 qed"TLex2seq";
 
-Goal "(TL`(ex2seq ex)~=UU) = ((snd ex)~=UU)";
-by (pair_tac "ex" 1);
-by (Seq_case_simp_tac "y" 1);
-by (pair_tac "a" 1);
-by (Seq_case_simp_tac "s" 1);
-by (pair_tac "a" 1);
-qed"ex2seqUUTL";
  
-Goal "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil)";
+Goal "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)";
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
 by (pair_tac "a" 1);
@@ -521,7 +514,8 @@
 by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
 (* cons case *)
 by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
-        ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqUUTL,ex2seqnilTL])1);
+        ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqnilTL])1);
+be conjE 1;
 by (dtac TLex2seq 1);
 by (assume_tac 1);
 by Auto_tac;

--- a/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Oct 19 15:49:55 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Oct 19 16:13:13 1998 +0200
@@ -51,7 +51,10 @@
 Addsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons];
 
 
-Goal "ex2seq (s, UU) = UU";
+
+Addsimps [mkfin_UU,mkfin_nil,mkfin_cons];
+
+Goal "ex2seq (s, UU) = (s,None,s)>>nil";
 by (simp_tac (simpset() addsimps [ex2seq_def]) 1);
 qed"ex2seq_UU";
 
@@ -64,12 +67,16 @@
 qed"ex2seq_cons";
 
 Delsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons]; 
-Addsimps [ex2seq_UUAlt,ex2seq_nil, ex2seq_cons];  
+Addsimps [ex2seq_UU,ex2seq_nil, ex2seq_cons];  
+
 
 
 
-(* FIX: Not true for UU, as ex2seq is defined continously !!!!! *)
 Goal "ex2seq exec ~= UU & ex2seq exec ~= nil";
+by (pair_tac "exec" 1);
+by (Seq_case_simp_tac "y" 1);
+by (pair_tac "a" 1);
+qed"ex2seq_nUUnnil";
 
 
 Goal "ex |== [] P .--> P";
@@ -79,15 +86,45 @@
 (*           Interface TL -- TLS                               *)
 (* ---------------------------------------------------------- *)
 
+
+(* uses the fact that in executions states overlap, which is lost in 
+   after the translation via ex2seq !! *)
+
 Goalw [Init_def,Next_def,temp_sat_def,satisfies_def,IMPLIES_def,AND_def]
- "!! s. (P s) & s-a--A-> t --> (Q t) \
+ "!! A. [| ! s a t. (P s) & s-a--A-> t --> (Q t) |]\
 \  ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) \
 \             .--> (Next (Init (%(s,a,t).Q s))))";
 
-by (Asm_full_simp_tac 1);
+by (clarify_tac set_cs 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+(* TL = UU *)
+br conjI 1;
+by (pair_tac "ex" 1);
+by (Seq_case_simp_tac "y" 1);
+by (pair_tac "a" 1);
+by (Seq_case_simp_tac "s" 1);
+by (pair_tac "a" 1);
+(* TL = nil *)
+br conjI 1;
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
-
+by (asm_full_simp_tac (simpset() addsimps [unlift_def])1);
+by (Fast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [unlift_def])1);
+by (Fast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [unlift_def])1);
+by (pair_tac "a" 1);
+by (Seq_case_simp_tac "s" 1);
+by (pair_tac "a" 1);
+(* TL =cons *)
+by (asm_full_simp_tac (simpset() addsimps [unlift_def])1);
 
-
-
+by (pair_tac "ex" 1);
+by (Seq_case_simp_tac "y" 1);
+by (pair_tac "a" 1);
+by (Seq_case_simp_tac "s" 1);
+ by (Fast_tac 1);
+ by (Fast_tac 1);
+by (pair_tac "a" 1);
+ by (Fast_tac 1);
+qed"TL_TLS";

--- a/src/HOLCF/IOA/meta_theory/TLS.thy	Mon Oct 19 15:49:55 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Mon Oct 19 16:13:13 1998 +0200
@@ -30,6 +30,7 @@
 validTE    :: "('a,'s)ioa_temp => bool"
 validIOA   :: "('a,'s)ioa => ('a,'s)ioa_temp => bool"
 
+mkfin      :: "'a Seq => 'a Seq"
 
 ex2seq     :: "('a,'s)execution => ('a option,'s)transition Seq"
 ex2seqC    :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" 
@@ -37,6 +38,10 @@
 
 defs
 
+mkfin_def
+  "mkfin s == if Partial s then @t. Finite t & s = t @@ UU
+                           else s"
+
 (* should be in Option as option_lift1, and option_map should be renamed to 
    option_lift2 *)
 option_lift_def
@@ -56,10 +61,8 @@
 xt2_def
   "xt2 P tr == P (fst (snd tr))"
 
-
-(* FIX: Clarify type and Herkunft of a !! *)
 ex2seq_def
-  "ex2seq ex == ((ex2seqC `(snd ex)) (fst ex))"
+  "ex2seq ex == ((ex2seqC `(mkfin (snd ex))) (fst ex))"
 
 ex2seqC_def
   "ex2seqC == (fix`(LAM h ex. (%s. case ex of 
@@ -77,8 +80,15 @@
 
 rules
 
-ex2seq_UUAlt
-  "ex2seq (s,UU) = (s,None,s)>>UU"
+mkfin_UU
+  "mkfin UU = nil"
+
+mkfin_nil
+  "mkfin nil =nil"
+
+mkfin_cons
+  "(mkfin (a>>s)) = (a>>(mkfin s))"
+
 
 
 end