tuning to assimiliate it with PhD;
authormueller
Thu Nov 26 16:37:56 1998 +0100 (1998-11-26)
changeset 597644290b71a85f
parent 5975 cd19eaa90f45
child 5977 9f0c8869cf71
tuning to assimiliate it with PhD;
src/HOLCF/IOA/meta_theory/Abstraction.ML
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/CompoScheds.ML
src/HOLCF/IOA/meta_theory/Compositionality.ML
src/HOLCF/IOA/meta_theory/LiveIOA.ML
src/HOLCF/IOA/meta_theory/Pred.thy
src/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOLCF/IOA/meta_theory/Seq.ML
src/HOLCF/IOA/meta_theory/Seq.thy
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/IOA/meta_theory/ShortExecutions.ML
src/HOLCF/IOA/meta_theory/TL.ML
src/HOLCF/IOA/meta_theory/TL.thy
src/HOLCF/IOA/meta_theory/TLS.ML
src/HOLCF/IOA/meta_theory/TLS.thy
src/HOLCF/IOA/meta_theory/Traces.thy
     1.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Thu Nov 26 12:18:51 1998 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Thu Nov 26 16:37:56 1998 +0100
     1.3 @@ -185,29 +185,6 @@
     1.4  by (pair_induct_tac "xs" [] 1);
     1.5  qed"traces_coincide_abs";
     1.6  
     1.7 -(* 
     1.8 -FIX: Is this needed anywhere? 
     1.9 -
    1.10 -Goalw [cex_abs_def]
    1.11 - "!!f.[| is_abstraction h C A |] ==>\
    1.12 -\ !s. reachable C s & is_exec_frag C (s,xs) \
    1.13 -\ --> is_exec_frag A (cex_abs h (s,xs))"; 
    1.14 -
    1.15 -by (Asm_full_simp_tac 1);
    1.16 -by (pair_induct_tac "xs" [is_exec_frag_def] 1);
    1.17 -(* main case *)
    1.18 -by (safe_tac set_cs);
    1.19 -(* Stepd correspond to each other *)
    1.20 -by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def])1);
    1.21 -(* IH *)
    1.22 -(* reachable_n looping, therefore apply it manually *)
    1.23 -by (eres_inst_tac [("x","y")] allE 1);
    1.24 -by (Asm_full_simp_tac 1);
    1.25 -by (forward_tac [reachable.reachable_n] 1);
    1.26 -by (assume_tac 1);
    1.27 -by (Asm_full_simp_tac 1);
    1.28 -qed_spec_mp"correp_is_exec_abs";
    1.29 -*) 
    1.30  
    1.31  (* Does not work with abstraction_is_ref_map as proof of abs_safety, because
    1.32     is_live_abstraction includes temp_strengthening which is necessarily based
    1.33 @@ -403,6 +380,8 @@
    1.34  qed"ex2seq_tsuffix";
    1.35  
    1.36  
    1.37 +(* FIX: NAch Sequence.ML bringen *)
    1.38 +
    1.39  Goal "(Map f`s = nil) = (s=nil)";
    1.40  by (Seq_case_simp_tac "s" 1);
    1.41  qed"Mapnil";
    1.42 @@ -540,26 +519,6 @@
    1.43  qed"weak_Init";
    1.44  
    1.45  
    1.46 -(*
    1.47 -
    1.48 -(* analog to strengthening thm above, with analog lemmas used  *)
    1.49 -
    1.50 -Goalw [state_weakening_def]
    1.51 -"!! h. [| temp_weakening P Q h |]\
    1.52 -\      ==> temp_weakening ([] P) ([] Q) h";
    1.53 -by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
    1.54 -         temp_sat_def,satisfies_def,Box_def])1);
    1.55 -
    1.56 -(* analog to strengthening thm above, with analog lemmas used  *)
    1.57 -
    1.58 -Goalw [state_weakening_def]
    1.59 -"!! h. [| temp_weakening P Q h |]\
    1.60 -\      ==> temp_weakening (Next P) (Next Q) h";
    1.61 -by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
    1.62 -         temp_sat_def,satisfies_def,Next_def])1);
    1.63 -
    1.64 -*)
    1.65 -
    1.66  (* ---------------------------------------------------------------- *)
    1.67  (*             Localizing Temproal Strengthenings - 3               *)
    1.68  (* ---------------------------------------------------------------- *)
     2.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Nov 26 12:18:51 1998 +0100
     2.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Nov 26 16:37:56 1998 +0100
     2.3 @@ -70,12 +70,12 @@
     2.4  ex2seq_abs_cex
     2.5    "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" 
     2.6  
     2.7 -(* analog to the proved thm strength_Box  *)
     2.8 +(* analog to the proved thm strength_Box - proof skipped as trivial *)
     2.9  weak_Box
    2.10  "temp_weakening P Q h 
    2.11   ==> temp_weakening ([] P) ([] Q) h"
    2.12  
    2.13 -(* analog to the proved thm strength_Next  *)
    2.14 +(* analog to the proved thm strength_Next - proof skipped as trivial *)
    2.15  weak_Next
    2.16  "temp_weakening P Q h 
    2.17   ==> temp_weakening (Next P) (Next Q) h"
     3.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Thu Nov 26 12:18:51 1998 +0100
     3.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Thu Nov 26 16:37:56 1998 +0100
     3.3 @@ -460,7 +460,7 @@
     3.4  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
     3.5  qed"compatible_par";
     3.6  
     3.7 -(* FIX: better derive by previous one and compat_commute *)
     3.8 +(*  better derive by previous one and compat_commute *)
     3.9  Goalw [compatible_def]
    3.10  "!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
    3.11  by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
     4.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Thu Nov 26 12:18:51 1998 +0100
     4.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Thu Nov 26 16:37:56 1998 +0100
     4.3 @@ -179,7 +179,7 @@
     4.4  (*             Schedules of A||B have only  A- or B-actions              *)
     4.5  (* --------------------------------------------------------------------- *)
     4.6  
     4.7 -(* FIX: very similar to lemma_1_1c, but it is not checking if every action element of 
     4.8 +(* very similar to lemma_1_1c, but it is not checking if every action element of 
     4.9     an ex is in A or B, but after projecting it onto the action schedule. Of course, this
    4.10     is the same proposition, but we cannot change this one, when then rather lemma_1_1c  *)
    4.11  
     5.1 --- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Thu Nov 26 12:18:51 1998 +0100
     5.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Thu Nov 26 16:37:56 1998 +0100
     5.3 @@ -25,8 +25,7 @@
     5.4  qed"Filter_actAisFilter_extA";
     5.5  
     5.6  
     5.7 -(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A)
     5.8 -    or even better A||B= B||A, FIX *)
     5.9 +(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *)
    5.10  
    5.11  Goal "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
    5.12  by Auto_tac;
     6.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Thu Nov 26 12:18:51 1998 +0100
     6.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Thu Nov 26 16:37:56 1998 +0100
     6.3 @@ -56,18 +56,3 @@
     6.4  
     6.5  
     6.6  (*
     6.7 -
     6.8 -(* Classical Fairness and Fairness by Temporal Formula coincide *)
     6.9 - 
    6.10 -Goal "!! ex. Finite (snd ex) ==> \
    6.11 -\          (ex |== WF A acts) = (~ Enabled A acts (laststate ex))";
    6.12 -
    6.13 -In 3 steps:
    6.14 -
    6.15 -1) []<>P and <>[]P mean both P (Last`s)
    6.16 -2) Transform this to executions and laststate
    6.17 -3) plift is used to show that plift (laststate ex) : acts == False. 
    6.18 -
    6.19 -
    6.20 -
    6.21 -*)
    6.22 \ No newline at end of file
     7.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy	Thu Nov 26 12:18:51 1998 +0100
     7.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Thu Nov 26 16:37:56 1998 +0100
     7.3 @@ -1,14 +1,10 @@
     7.4 -(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
     7.5 +(*  Title:      HOLCF/IOA/meta_theory/Pred.thy
     7.6      ID:         $Id$
     7.7      Author:     Olaf M"uller
     7.8      Copyright   1997  TU Muenchen
     7.9  
    7.10  Logical Connectives lifted to predicates.
    7.11  
    7.12 -ToDo:
    7.13 -
    7.14 -<--> einfuehren.
    7.15 -
    7.16  *)   
    7.17  	       
    7.18  Pred = Arith +  
     8.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Nov 26 12:18:51 1998 +0100
     8.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Nov 26 16:37:56 1998 +0100
     8.3 @@ -39,7 +39,8 @@
     8.4  
     8.5  rules
     8.6  (* Axioms for fair trace inclusion proof support, not for the correctness proof
     8.7 -   of refeinment mappings ! *)
     8.8 +   of refinement mappings ! 
     8.9 +   Note: Everything is superseded by LiveIOA.thy! *)
    8.10  
    8.11  corresp_laststate
    8.12    "Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))"
     9.1 --- a/src/HOLCF/IOA/meta_theory/Seq.ML	Thu Nov 26 12:18:51 1998 +0100
     9.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Thu Nov 26 16:37:56 1998 +0100
     9.3 @@ -376,7 +376,6 @@
     9.4  by (simp_tac (simpset() addsimps [sforall_def]) 1);
     9.5  by (res_inst_tac[("x","x")] seq.ind 1);
     9.6  (* adm *)
     9.7 -(* FIX should be refined in _one_ tactic *)
     9.8  by (simp_tac (simpset() addsimps [adm_trick_1]) 1);
     9.9  (* base cases *)
    9.10  by (Simp_tac 1);
    9.11 @@ -460,63 +459,3 @@
    9.12  qed"seq_finite_ind";
    9.13  
    9.14  
    9.15 -
    9.16 -
    9.17 -(*
    9.18 -(* -----------------------------------------------------------------
    9.19 -   Fr"uhere Herleitung des endlichen Induktionsprinzips 
    9.20 -   aus dem seq_finite Induktionsprinzip.
    9.21 -   Problem bei admissibility von Finite-->seq_finite!
    9.22 -   Deshalb Finite jetzt induktiv und nicht mehr rekursiv definiert! 
    9.23 -   ------------------------------------------------------------------ *)
    9.24 -
    9.25 -Goal "seq_finite nil";
    9.26 -by (simp_tac (simpset() addsimps [seq.sfinite_def]) 1);
    9.27 -by (res_inst_tac [("x","Suc 0")] exI 1);
    9.28 -by (simp_tac (simpset() addsimps seq.rews) 1);
    9.29 -qed"seq_finite_nil";
    9.30 -
    9.31 -Goal "seq_finite UU";
    9.32 -by (simp_tac (simpset() addsimps [seq.sfinite_def]) 1);
    9.33 -qed"seq_finite_UU";
    9.34 -
    9.35 -Addsimps[seq_finite_nil,seq_finite_UU];
    9.36 -
    9.37 -goal HOL.thy "(B-->A) --> (A--> (B-->C))--> (B--> C)";
    9.38 -by (fast_tac HOL_cs 1);
    9.39 -qed"logic_lemma";
    9.40 -
    9.41 -
    9.42 -Goal "!!P.[| P nil; \
    9.43 -\                !!a t. [|a~=UU;Finite t; P t|] ==> P (a##t)|]\
    9.44 -\            ==> Finite x --> P x";
    9.45 -
    9.46 -by (rtac (logic_lemma RS mp RS mp) 1);
    9.47 -by (rtac trf_impl_tf 1);
    9.48 -by (rtac seq_finite_ind 1);
    9.49 -by (simp_tac (simpset() addsimps [Finite_def]) 1);
    9.50 -by (simp_tac (simpset() addsimps [Finite_def]) 1);
    9.51 -by (asm_full_simp_tac (simpset() addsimps [Finite_def]) 1);
    9.52 -qed"Finite_ind";
    9.53 -
    9.54 -
    9.55 -Goal "Finite tr --> seq_finite tr";
    9.56 -by (rtac seq.ind 1);
    9.57 -(* adm *)
    9.58 -(* hier grosses Problem !!!!!!!!!!!!!!! *)
    9.59 -
    9.60 -by (simp_tac (simpset() addsimps [Finite_def]) 2);
    9.61 -by (simp_tac (simpset() addsimps [Finite_def]) 2);
    9.62 -
    9.63 -(* main case *)
    9.64 -by (asm_full_simp_tac (simpset() addsimps [Finite_def,seq.sfinite_def]) 2);
    9.65 -by (rtac impI 2);
    9.66 -by (rotate_tac 2 2);
    9.67 -by (Asm_full_simp_tac 2);
    9.68 -by (etac exE 2);
    9.69 -by (res_inst_tac [("x","Suc n")] exI 2);
    9.70 -by (asm_full_simp_tac (simpset() addsimps seq.rews) 2);
    9.71 -qed"tf_is_trf";
    9.72 -
    9.73 -*)
    9.74 -
    10.1 --- a/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Nov 26 12:18:51 1998 +0100
    10.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Nov 26 16:37:56 1998 +0100
    10.3 @@ -104,16 +104,6 @@
    10.4               | x##xs => (case t2 of 
    10.5                            nil => UU 
    10.6                          | y##ys => <x,y>##(h`xs`ys))))"
    10.7 - 
    10.8 -(*
    10.9 -nproj_def 
   10.10 - "nproj == (%n tr.HD`(iterate n TL tr))"   
   10.11 -
   10.12 -
   10.13 -sproj_def 
   10.14 - "sproj == (%n tr.iterate n TL tr)"   
   10.15 -*)
   10.16 -
   10.17  
   10.18  Partial_def
   10.19    "Partial x  == (seq_finite x) & ~(Finite x)"
    11.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Nov 26 12:18:51 1998 +0100
    11.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Nov 26 16:37:56 1998 +0100
    11.3 @@ -188,8 +188,6 @@
    11.4  by (rtac trans 1);
    11.5  by (stac Zip_unfold 1);
    11.6  by (Simp_tac 1);
    11.7 -(* FIX: Why Simp_tac 2 times. Does continuity in simpflication make job sometimes not 
    11.8 -  completely ready ? *)
    11.9  by (simp_tac (simpset() addsimps [Cons_def]) 1);
   11.10  qed"Zip_cons";
   11.11  
   11.12 @@ -214,25 +212,6 @@
   11.13            Zip_UU1,Zip_UU2,Zip_nil,Zip_cons_nil,Zip_cons];
   11.14  
   11.15  
   11.16 -(*
   11.17 -
   11.18 -Can Filter with HOL predicate directly be defined as fixpoint ?
   11.19 -
   11.20 -Goal "Filter2 P = (LAM tr. case tr of  \
   11.21 - \         nil   => nil \
   11.22 - \       | x##xs => (case x of Undef => UU | Def y => \
   11.23 -\                   (if P y then y>>(Filter2 P`xs) else Filter2 P`xs)))";
   11.24 -by (rtac trans 1);
   11.25 -by (rtac fix_eq2 1);
   11.26 -by (rtac Filter2_def 1);
   11.27 -by (rtac beta_cfun 1);
   11.28 -by (Simp_tac 1);
   11.29 -
   11.30 -is also possible, if then else has to be proven continuous and it would be nice if a case for 
   11.31 -Seq would be available.
   11.32 -
   11.33 -*)
   11.34 -
   11.35  
   11.36  (* ------------------------------------------------------------------------------------- *)
   11.37  
   11.38 @@ -524,7 +503,7 @@
   11.39  
   11.40  Addsimps [nilConc];
   11.41  
   11.42 -(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
   11.43 +(* should be same as nil_is_Conc2 when all nils are turned to right side !! *)
   11.44  Goal "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
   11.45  by (Seq_case_simp_tac "x" 1);
   11.46  by Auto_tac;
   11.47 @@ -1155,7 +1134,7 @@
   11.48  by (res_inst_tac [("A1","%x. True") 
   11.49                   ,("Q1","%x.~(P x & Q x)"),("x1","s")]
   11.50                   (take_lemma_induct RS mp) 1);
   11.51 -(* FIX: better support for A = %x. True *)
   11.52 +(* better support for A = %x. True *)
   11.53  by (Fast_tac 3);
   11.54  by (asm_full_simp_tac (simpset() addsimps [Filter_lemma1]) 1);
   11.55  by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3]) 1);
    12.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Thu Nov 26 12:18:51 1998 +0100
    12.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Thu Nov 26 16:37:56 1998 +0100
    12.3 @@ -179,36 +179,6 @@
    12.4  
    12.5  
    12.6  
    12.7 -(*
    12.8 -
    12.9 -Goal "Finite s --> (? y. s = Cut P s @@ y)";
   12.10 -by (strip_tac 1);
   12.11 -by (rtac exI 1);
   12.12 -by (resolve_tac seq.take_lemmas 1);
   12.13 -by (rtac mp 1);
   12.14 -by (assume_tac 2);
   12.15 -by (thin_tac' 1 1);
   12.16 -by (res_inst_tac [("x","s")] spec 1);
   12.17 -by (rtac less_induct 1);
   12.18 -by (strip_tac 1);
   12.19 -ren "na n s" 1;
   12.20 -by (case_tac "Forall (%x. ~ P x) s" 1);
   12.21 -by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
   12.22 -by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1);
   12.23 -(* main case *)
   12.24 -by (dtac divide_Seq3 1);
   12.25 -by (REPEAT (etac exE 1));
   12.26 -by (REPEAT (etac conjE 1));
   12.27 -by (hyp_subst_tac 1);
   12.28 -by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,Conc_assoc]) 1);
   12.29 -by (rtac take_reduction 1);
   12.30 -
   12.31 -qed_spec_mp"Cut_prefixcl_Finite";
   12.32 -
   12.33 -*)
   12.34 -
   12.35 -
   12.36 -
   12.37  Goal "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)";
   12.38  by (case_tac "Finite ex" 1);
   12.39  by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1);
    13.1 --- a/src/HOLCF/IOA/meta_theory/TL.ML	Thu Nov 26 12:18:51 1998 +0100
    13.2 +++ b/src/HOLCF/IOA/meta_theory/TL.ML	Thu Nov 26 16:37:56 1998 +0100
    13.3 @@ -11,7 +11,7 @@
    13.4  by (rtac ext 1);
    13.5  by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
    13.6  by Auto_tac;
    13.7 -qed"simple_try";
    13.8 +qed"simple";
    13.9  
   13.10  Goal "nil |= [] P";
   13.11  by (asm_full_simp_tac (simpset() addsimps [satisfies_def,
   13.12 @@ -73,27 +73,6 @@
   13.13  qed"normalT";
   13.14  
   13.15  
   13.16 -(*
   13.17 -Goal "s |= <> F .& <> G .--> (<> (F .& <> G) .| <> (G .& <> F))";
   13.18 -by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,AND_def,OR_def,Diamond_def2])1);
   13.19 -by (rtac impI 1);
   13.20 -by (etac conjE 1);
   13.21 -by (etac exE 1);
   13.22 -by (etac exE 1);
   13.23 -
   13.24 -
   13.25 -by (rtac disjI1 1);
   13.26 -
   13.27 -Goal "!!s. [| tsuffix s1 s ; tsuffix s2 s|] ==> tsuffix s2 s1 | tsuffix s1 s2";
   13.28 -by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
   13.29 -by (REPEAT (etac conjE 1));
   13.30 -by (REPEAT (etac exE 1));
   13.31 -by (REPEAT (etac conjE 1));
   13.32 -by (hyp_subst_tac 1);
   13.33 -
   13.34 -*)
   13.35 -
   13.36 -
   13.37  section "TLA Rules by Lamport";
   13.38  
   13.39  (* ---------------------------------------------------------------- *)
   13.40 @@ -113,8 +92,6 @@
   13.41  by (etac STL1b 1);
   13.42  qed"STL1";
   13.43  
   13.44 -
   13.45 -
   13.46  (* Note that unlift and HD is not at all used !!! *)
   13.47  Goal "!! P. valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
   13.48  by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
   13.49 @@ -175,7 +152,6 @@
   13.50  by (Asm_full_simp_tac 1);
   13.51  by Auto_tac;
   13.52  
   13.53 -
   13.54  by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
   13.55  by Auto_tac;
   13.56  
    14.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Thu Nov 26 12:18:51 1998 +0100
    14.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Thu Nov 26 16:37:56 1998 +0100
    14.3 @@ -5,8 +5,6 @@
    14.4  
    14.5  A General Temporal Logic
    14.6  
    14.7 -Version 2: Interface directly after Sequeces, i.e. predicates and predicate transformers are in HOL
    14.8 -
    14.9  *)   
   14.10  
   14.11  
    15.1 --- a/src/HOLCF/IOA/meta_theory/TLS.ML	Thu Nov 26 12:18:51 1998 +0100
    15.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Thu Nov 26 16:37:56 1998 +0100
    15.3 @@ -4,7 +4,7 @@
    15.4      Copyright   1997  TU Muenchen
    15.5  
    15.6  Temporal Logic of Steps -- tailored for I/O automata
    15.7 -*)   
    15.8 +*)    
    15.9  
   15.10  (* global changes to simpset() and claset(), repeated from Traces.ML *)
   15.11  Delsimps (ex_simps @ all_simps);
   15.12 @@ -70,8 +70,6 @@
   15.13  Addsimps [ex2seq_UU,ex2seq_nil, ex2seq_cons];  
   15.14  
   15.15  
   15.16 -
   15.17 -
   15.18  Goal "ex2seq exec ~= UU & ex2seq exec ~= nil";
   15.19  by (pair_tac "exec" 1);
   15.20  by (Seq_case_simp_tac "y" 1);
   15.21 @@ -79,9 +77,6 @@
   15.22  qed"ex2seq_nUUnnil";
   15.23  
   15.24  
   15.25 -Goal "ex |== [] P .--> P";
   15.26 -
   15.27 -
   15.28  (* ----------------------------------------------------------- *)
   15.29  (*           Interface TL -- TLS                               *)
   15.30  (* ---------------------------------------------------------- *)
    16.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Nov 26 12:18:51 1998 +0100
    16.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Nov 26 16:37:56 1998 +0100
    16.3 @@ -42,8 +42,6 @@
    16.4    "mkfin s == if Partial s then @t. Finite t & s = t @@ UU
    16.5                             else s"
    16.6  
    16.7 -(* should be in Option as option_lift1, and option_map should be renamed to 
    16.8 -   option_lift2 *)
    16.9  option_lift_def
   16.10    "option_lift f s y == case y of None => s | Some x => (f x)"
   16.11  
   16.12 @@ -78,6 +76,8 @@
   16.13  validIOA_def
   16.14    "validIOA A P == ! ex : executions A . (ex |== P)"
   16.15  
   16.16 +
   16.17 +
   16.18  rules
   16.19  
   16.20  mkfin_UU
    17.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Thu Nov 26 12:18:51 1998 +0100
    17.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Thu Nov 26 16:37:56 1998 +0100
    17.3 @@ -66,13 +66,6 @@
    17.4    Scheds        ::  "('a,'s)ioa => 'a schedule_module"
    17.5    Traces        ::  "('a,'s)ioa => 'a trace_module"
    17.6  
    17.7 -(*
    17.8 -(* FIX: introduce good symbol *)
    17.9 -syntax (symbols)
   17.10 -
   17.11 -  "op <<|"       ::"[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "\\<parallel>" 10)
   17.12 -*)
   17.13 -
   17.14  
   17.15  defs
   17.16  
   17.17 @@ -144,7 +137,8 @@
   17.18  
   17.19  (* Note that partial execs cannot be wfair as the inf_often predicate in the 
   17.20     else branch prohibits it. However they can be sfair in the case when all W 
   17.21 -   are only finitely often enabled: FIX Is this the right model? *)
   17.22 +   are only finitely often enabled: Is this the right model?  
   17.23 +   See LiveIOA for solution conforming with the literature and superseding this one *)
   17.24  wfair_ex_def
   17.25    "wfair_ex A ex == ! W : wfair_of A.  
   17.26                        if   Finite (snd ex)