another little bug ;-) and minor changes in TLS.*;
authormueller
Mon Oct 19 16:13:13 1998 +0200 (1998-10-19)
changeset 56774feffde494cf
parent 5676 96b048840bb3
child 5678 e68c518b9140
another little bug ;-) and minor changes in TLS.*;
src/HOLCF/IOA/meta_theory/Abstraction.ML
src/HOLCF/IOA/meta_theory/TLS.ML
src/HOLCF/IOA/meta_theory/TLS.thy
     1.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Oct 19 15:49:55 1998 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Oct 19 16:13:13 1998 +0200
     1.3 @@ -492,15 +492,8 @@
     1.4  by Auto_tac;
     1.5  qed"TLex2seq";
     1.6  
     1.7 -Goal "(TL`(ex2seq ex)~=UU) = ((snd ex)~=UU)";
     1.8 -by (pair_tac "ex" 1);
     1.9 -by (Seq_case_simp_tac "y" 1);
    1.10 -by (pair_tac "a" 1);
    1.11 -by (Seq_case_simp_tac "s" 1);
    1.12 -by (pair_tac "a" 1);
    1.13 -qed"ex2seqUUTL";
    1.14   
    1.15 -Goal "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil)";
    1.16 +Goal "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)";
    1.17  by (pair_tac "ex" 1);
    1.18  by (Seq_case_simp_tac "y" 1);
    1.19  by (pair_tac "a" 1);
    1.20 @@ -521,7 +514,8 @@
    1.21  by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
    1.22  (* cons case *)
    1.23  by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
    1.24 -        ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqUUTL,ex2seqnilTL])1);
    1.25 +        ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqnilTL])1);
    1.26 +be conjE 1;
    1.27  by (dtac TLex2seq 1);
    1.28  by (assume_tac 1);
    1.29  by Auto_tac;
     2.1 --- a/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Oct 19 15:49:55 1998 +0200
     2.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Oct 19 16:13:13 1998 +0200
     2.3 @@ -51,7 +51,10 @@
     2.4  Addsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons];
     2.5  
     2.6  
     2.7 -Goal "ex2seq (s, UU) = UU";
     2.8 +
     2.9 +Addsimps [mkfin_UU,mkfin_nil,mkfin_cons];
    2.10 +
    2.11 +Goal "ex2seq (s, UU) = (s,None,s)>>nil";
    2.12  by (simp_tac (simpset() addsimps [ex2seq_def]) 1);
    2.13  qed"ex2seq_UU";
    2.14  
    2.15 @@ -64,12 +67,16 @@
    2.16  qed"ex2seq_cons";
    2.17  
    2.18  Delsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons]; 
    2.19 -Addsimps [ex2seq_UUAlt,ex2seq_nil, ex2seq_cons];  
    2.20 +Addsimps [ex2seq_UU,ex2seq_nil, ex2seq_cons];  
    2.21 +
    2.22  
    2.23  
    2.24  
    2.25 -(* FIX: Not true for UU, as ex2seq is defined continously !!!!! *)
    2.26  Goal "ex2seq exec ~= UU & ex2seq exec ~= nil";
    2.27 +by (pair_tac "exec" 1);
    2.28 +by (Seq_case_simp_tac "y" 1);
    2.29 +by (pair_tac "a" 1);
    2.30 +qed"ex2seq_nUUnnil";
    2.31  
    2.32  
    2.33  Goal "ex |== [] P .--> P";
    2.34 @@ -79,15 +86,45 @@
    2.35  (*           Interface TL -- TLS                               *)
    2.36  (* ---------------------------------------------------------- *)
    2.37  
    2.38 +
    2.39 +(* uses the fact that in executions states overlap, which is lost in 
    2.40 +   after the translation via ex2seq !! *)
    2.41 +
    2.42  Goalw [Init_def,Next_def,temp_sat_def,satisfies_def,IMPLIES_def,AND_def]
    2.43 - "!! s. (P s) & s-a--A-> t --> (Q t) \
    2.44 + "!! A. [| ! s a t. (P s) & s-a--A-> t --> (Q t) |]\
    2.45  \  ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) \
    2.46  \             .--> (Next (Init (%(s,a,t).Q s))))";
    2.47  
    2.48 -by (Asm_full_simp_tac 1);
    2.49 +by (clarify_tac set_cs 1);
    2.50 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
    2.51 +(* TL = UU *)
    2.52 +br conjI 1;
    2.53 +by (pair_tac "ex" 1);
    2.54 +by (Seq_case_simp_tac "y" 1);
    2.55 +by (pair_tac "a" 1);
    2.56 +by (Seq_case_simp_tac "s" 1);
    2.57 +by (pair_tac "a" 1);
    2.58 +(* TL = nil *)
    2.59 +br conjI 1;
    2.60  by (pair_tac "ex" 1);
    2.61  by (Seq_case_simp_tac "y" 1);
    2.62 -
    2.63 +by (asm_full_simp_tac (simpset() addsimps [unlift_def])1);
    2.64 +by (Fast_tac 1);
    2.65 +by (asm_full_simp_tac (simpset() addsimps [unlift_def])1);
    2.66 +by (Fast_tac 1);
    2.67 +by (asm_full_simp_tac (simpset() addsimps [unlift_def])1);
    2.68 +by (pair_tac "a" 1);
    2.69 +by (Seq_case_simp_tac "s" 1);
    2.70 +by (pair_tac "a" 1);
    2.71 +(* TL =cons *)
    2.72 +by (asm_full_simp_tac (simpset() addsimps [unlift_def])1);
    2.73  
    2.74 -
    2.75 -
    2.76 +by (pair_tac "ex" 1);
    2.77 +by (Seq_case_simp_tac "y" 1);
    2.78 +by (pair_tac "a" 1);
    2.79 +by (Seq_case_simp_tac "s" 1);
    2.80 + by (Fast_tac 1);
    2.81 + by (Fast_tac 1);
    2.82 +by (pair_tac "a" 1);
    2.83 + by (Fast_tac 1);
    2.84 +qed"TL_TLS";
     3.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Mon Oct 19 15:49:55 1998 +0200
     3.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Mon Oct 19 16:13:13 1998 +0200
     3.3 @@ -30,6 +30,7 @@
     3.4  validTE    :: "('a,'s)ioa_temp => bool"
     3.5  validIOA   :: "('a,'s)ioa => ('a,'s)ioa_temp => bool"
     3.6  
     3.7 +mkfin      :: "'a Seq => 'a Seq"
     3.8  
     3.9  ex2seq     :: "('a,'s)execution => ('a option,'s)transition Seq"
    3.10  ex2seqC    :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" 
    3.11 @@ -37,6 +38,10 @@
    3.12  
    3.13  defs
    3.14  
    3.15 +mkfin_def
    3.16 +  "mkfin s == if Partial s then @t. Finite t & s = t @@ UU
    3.17 +                           else s"
    3.18 +
    3.19  (* should be in Option as option_lift1, and option_map should be renamed to 
    3.20     option_lift2 *)
    3.21  option_lift_def
    3.22 @@ -56,10 +61,8 @@
    3.23  xt2_def
    3.24    "xt2 P tr == P (fst (snd tr))"
    3.25  
    3.26 -
    3.27 -(* FIX: Clarify type and Herkunft of a !! *)
    3.28  ex2seq_def
    3.29 -  "ex2seq ex == ((ex2seqC `(snd ex)) (fst ex))"
    3.30 +  "ex2seq ex == ((ex2seqC `(mkfin (snd ex))) (fst ex))"
    3.31  
    3.32  ex2seqC_def
    3.33    "ex2seqC == (fix`(LAM h ex. (%s. case ex of 
    3.34 @@ -77,8 +80,15 @@
    3.35  
    3.36  rules
    3.37  
    3.38 -ex2seq_UUAlt
    3.39 -  "ex2seq (s,UU) = (s,None,s)>>UU"
    3.40 +mkfin_UU
    3.41 +  "mkfin UU = nil"
    3.42 +
    3.43 +mkfin_nil
    3.44 +  "mkfin nil =nil"
    3.45 +
    3.46 +mkfin_cons
    3.47 +  "(mkfin (a>>s)) = (a>>(mkfin s))"
    3.48 +
    3.49  
    3.50  
    3.51  end