# HG changeset patch
# User mueller
# Date 884623703 -3600
# Node ID 8e604d885b54683b86bac031ed4e51c8b42b17c4
# Parent  31becfd8d3299513e15a46a6f851629fbe25ca91
added files containing temproal logic and abstraction;

diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/Abstraction.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,498 @@
+(*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
+    ID:         $Id$
+    Author:     Olaf M"uller
+    Copyright   1997  TU Muenchen
+
+Abstraction Theory -- tailored for I/O automata
+*)   
+
+
+section "cex_abs";
+	
+
+(* ---------------------------------------------------------------- *)
+(*                             cex_abs                              *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "cex_abs f (s,UU) = (f s, UU)";
+by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
+qed"cex_abs_UU";
+
+goal thy "cex_abs f (s,nil) = (f s, nil)";
+by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
+qed"cex_abs_nil";
+
+goal thy "cex_abs f (s,(a,t)>>ex) = (f s, (a,f t) >> (snd (cex_abs f (t,ex))))";
+by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
+qed"cex_abs_cons";
+
+Addsimps [cex_abs_UU, cex_abs_nil, cex_abs_cons];
+
+ 
+
+section "lemmas";
+
+(* ---------------------------------------------------------------- *)
+(*                           Lemmas                                 *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))";
+by (simp_tac (simpset() addsimps [temp_weakening_def,temp_strengthening_def,
+     NOT_def,temp_sat_def,satisfies_def]) 1);
+auto();
+qed"temp_weakening_def2";
+
+goal thy "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))";
+by (simp_tac (simpset() addsimps [state_weakening_def,state_strengthening_def,
+     NOT_def]) 1);
+auto();
+qed"state_weakening_def2";
+
+
+section "Abstraction Rules for Properties";
+
+(* ---------------------------------------------------------------- *)
+(*                Abstraction Rules for Properties                  *)
+(* ---------------------------------------------------------------- *)
+
+
+goalw thy [cex_abs_def]
+ "!!h.[| is_abstraction h C A |] ==>\
+\ !s. reachable C s & is_exec_frag C (s,xs) \
+\ --> is_exec_frag A (cex_abs h (s,xs))"; 
+
+by (Asm_full_simp_tac 1);
+by (pair_induct_tac "xs" [is_exec_frag_def] 1);
+(* main case *)
+by (safe_tac set_cs);
+by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def])1);
+by (forward_tac [reachable.reachable_n] 1);
+by (assume_tac 1);
+by (Asm_full_simp_tac 1);
+qed"exec_frag_abstraction";
+
+
+goal thy "!!A. is_abstraction h C A ==> weakeningIOA A C h";
+by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1);
+auto();
+by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
+(* start state *) 
+by (rtac conjI 1);
+by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1);
+(* is-execution-fragment *)
+by (etac (exec_frag_abstraction RS spec RS mp) 1);
+by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
+qed"abs_is_weakening";
+
+
+goal thy "!!A. [|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
+\         ==> validIOA C P";
+bd abs_is_weakening 1;
+by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, 
+    validIOA_def, temp_strengthening_def])1);
+by (safe_tac set_cs);
+by (pair_tac "ex" 1);
+qed"AbsRuleT1";
+
+
+(* FIX: Nach TLS.ML *)
+
+goal thy "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))";
+by (simp_tac (simpset() addsimps [IMPLIES_def,temp_sat_def, satisfies_def])1);
+qed"IMPLIES_temp_sat";
+
+goal thy "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))";
+by (simp_tac (simpset() addsimps [AND_def,temp_sat_def, satisfies_def])1);
+qed"AND_temp_sat";
+
+goal thy "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))";
+by (simp_tac (simpset() addsimps [OR_def,temp_sat_def, satisfies_def])1);
+qed"OR_temp_sat";
+
+goal thy "(ex |== .~ P) = (~ (ex |== P))";
+by (simp_tac (simpset() addsimps [NOT_def,temp_sat_def, satisfies_def])1);
+qed"NOT_temp_sat";
+
+Addsimps [IMPLIES_temp_sat,AND_temp_sat,OR_temp_sat,NOT_temp_sat];
+
+
+goalw thy [is_live_abstraction_def]
+   "!!A. [|is_live_abstraction h (C,L) (A,M); \
+\         validLIOA (A,M) Q;  temp_strengthening Q P h |] \
+\         ==> validLIOA (C,L) P";
+auto();
+bd abs_is_weakening 1;
+by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
+    validLIOA_def, validIOA_def, temp_strengthening_def])1);
+by (safe_tac set_cs);
+by (pair_tac "ex" 1);
+qed"AbsRuleT2";
+
+
+goalw thy [is_live_abstraction_def]
+   "!!A. [|is_live_abstraction h (C,L) (A,M); \
+\         validLIOA (A,M) (H1 .--> Q);  temp_strengthening Q P h; \
+\         temp_weakening H1 H2 h; validLIOA (C,L) H2 |] \
+\         ==> validLIOA (C,L) P";
+auto();
+bd abs_is_weakening 1;
+by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
+    validLIOA_def, validIOA_def, temp_strengthening_def])1);
+by (safe_tac set_cs);
+by (pair_tac "ex" 1);
+qed"AbsRuleTImprove";
+
+
+section "Correctness of safe abstraction";
+
+(* ---------------------------------------------------------------- *)
+(*              Correctness of safe abstraction                     *)
+(* ---------------------------------------------------------------- *)
+
+
+goalw thy [is_abstraction_def,is_ref_map_def] 
+"!! h. is_abstraction h C A ==> is_ref_map h C A";
+by (safe_tac set_cs);
+by (res_inst_tac[("x","(a,h t)>>nil")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def])1);
+qed"abstraction_is_ref_map";
+
+
+goal thy "!! h. [| inp(C)=inp(A); out(C)=out(A); \
+\                  is_abstraction h C A |] \
+\               ==> C =<| A";
+by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1);
+br trace_inclusion 1;
+by (simp_tac (simpset() addsimps [externals_def])1);
+by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
+be abstraction_is_ref_map 1;
+qed"abs_safety";
+
+
+section "Correctness of life abstraction";
+
+(* ---------------------------------------------------------------- *)
+(*              Correctness of life abstraction                     *)
+(* ---------------------------------------------------------------- *)
+
+
+(* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x),
+   that is to special Map Lemma *)
+goalw thy [cex_abs_def,mk_trace_def,filter_act_def]
+  "!! f. ext C = ext A \
+\        ==> mk_trace C`xs = mk_trace A`(snd (cex_abs f (s,xs)))";
+by (Asm_full_simp_tac 1);
+by (pair_induct_tac "xs" [] 1);
+qed"traces_coincide_abs";
+
+
+goalw thy [cex_abs_def]
+ "!!f.[| is_abstraction h C A |] ==>\
+\ !s. reachable C s & is_exec_frag C (s,xs) \
+\ --> is_exec_frag A (cex_abs h (s,xs))"; 
+
+by (Asm_full_simp_tac 1);
+by (pair_induct_tac "xs" [is_exec_frag_def] 1);
+(* main case *)
+by (safe_tac set_cs);
+(* Stepd correspond to each other *)
+by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def])1);
+(* IH *)
+(* reachable_n looping, therefore apply it manually *)
+by (eres_inst_tac [("x","y")] allE 1);
+by (Asm_full_simp_tac 1);
+by (forward_tac [reachable.reachable_n] 1);
+by (assume_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp"correp_is_exec_abs";
+
+(* Does not work with abstraction_is_ref_map as proof of abs_safety, because
+   is_live_abstraction includes temp_strengthening which is necessarily based
+   on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific
+   way for cex_abs *)
+goal thy "!! h. [| inp(C)=inp(A); out(C)=out(A); \
+\                  is_live_abstraction h (C,M) (A,L) |] \
+\               ==> live_implements (C,M) (A,L)";
+
+by (asm_full_simp_tac (simpset() addsimps [is_live_abstraction_def, live_implements_def,
+livetraces_def,liveexecutions_def]) 1);
+by (safe_tac set_cs);
+by (res_inst_tac[("x","cex_abs h ex")] exI 1);
+by (safe_tac set_cs);
+  (* Traces coincide *)
+  by (pair_tac "ex" 1);
+  by (rtac traces_coincide_abs 1);
+  by (simp_tac (simpset() addsimps [externals_def])1);
+  by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
+ 
+  (* cex_abs is execution *)
+  by (pair_tac "ex" 1);
+  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
+  (* start state *) 
+  by (rtac conjI 1);
+  by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1);
+  (* is-execution-fragment *)
+  by (etac correp_is_exec_abs 1);
+  by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
+
+ (* Liveness *) 
+by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2]) 1);
+ by (pair_tac "ex" 1);
+qed"abs_liveness";
+
+(* FIX: NAch Traces.ML bringen *)
+
+goalw thy [ioa_implements_def] 
+"!! A. [| A =<| B; B =<| C|] ==> A =<| C"; 
+auto();
+qed"implements_trans";
+
+
+section "Abstraction Rules for Automata";
+
+(* ---------------------------------------------------------------- *)
+(*                Abstraction Rules for Automata                    *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "!! C. [| inp(C)=inp(A); out(C)=out(A); \
+\                  inp(Q)=inp(P); out(Q)=out(P); \
+\                  is_abstraction h1 C A; \
+\                  A =<| Q ; \
+\                  is_abstraction h2 Q P |] \
+\               ==> C =<| P";   
+bd abs_safety 1;
+by (REPEAT (atac 1));
+bd abs_safety 1;
+by (REPEAT (atac 1));
+be implements_trans 1;
+be implements_trans 1;
+ba 1;
+qed"AbsRuleA1";
+
+
+goal thy "!! C. [| inp(C)=inp(A); out(C)=out(A); \
+\                  inp(Q)=inp(P); out(Q)=out(P); \
+\                  is_live_abstraction h1 (C,LC) (A,LA); \
+\                  live_implements (A,LA) (Q,LQ) ; \
+\                  is_live_abstraction h2 (Q,LQ) (P,LP) |] \
+\               ==> live_implements (C,LC) (P,LP)";   
+bd abs_liveness 1;
+by (REPEAT (atac 1));
+bd abs_liveness 1;
+by (REPEAT (atac 1));
+be live_implements_trans 1;
+be live_implements_trans 1;
+ba 1;
+qed"AbsRuleA2";
+
+
+Delsimps [split_paired_All];
+
+
+section "Localizing Temporal Strengthenings and Weakenings";
+
+(* ---------------------------------------------------------------- *)
+(*                Localizing Temproal Strengthenings - 1               *)
+(* ---------------------------------------------------------------- *)
+
+goalw thy [temp_strengthening_def]
+"!! h. [| temp_strengthening P1 Q1 h; \
+\         temp_strengthening P2 Q2 h |] \
+\      ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h";
+auto();
+qed"strength_AND";
+
+goalw thy [temp_strengthening_def]
+"!! h. [| temp_strengthening P1 Q1 h; \
+\         temp_strengthening P2 Q2 h |] \
+\      ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h";
+auto();
+qed"strength_OR";
+
+goalw thy [temp_strengthening_def]
+"!! h. [| temp_weakening P Q h |] \
+\      ==> temp_strengthening (.~ P) (.~ Q) h";
+by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
+auto();
+qed"strength_NOT";
+
+goalw thy [temp_strengthening_def]
+"!! h. [| temp_weakening P1 Q1 h; \
+\         temp_strengthening P2 Q2 h |] \
+\      ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h";
+by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
+auto();
+qed"strength_IMPLIES";
+
+
+
+(* ---------------------------------------------------------------- *)
+(*                Localizing Temproal Weakenings - Part 1           *)
+(* ---------------------------------------------------------------- *)
+
+goal thy
+"!! h. [| temp_weakening P1 Q1 h; \
+\         temp_weakening P2 Q2 h |] \
+\      ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h";
+by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
+auto();
+qed"weak_AND";
+
+goal thy 
+"!! h. [| temp_weakening P1 Q1 h; \
+\         temp_weakening P2 Q2 h |] \
+\      ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h";
+by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
+auto();
+qed"weak_OR";
+
+goalw thy [temp_strengthening_def]
+"!! h. [| temp_strengthening P Q h |] \
+\      ==> temp_weakening (.~ P) (.~ Q) h";
+by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
+auto();
+qed"weak_NOT";
+
+goalw thy [temp_strengthening_def]
+"!! h. [| temp_strengthening P1 Q1 h; \
+\         temp_weakening P2 Q2 h |] \
+\      ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h";
+by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
+auto();
+qed"weak_IMPLIES";
+
+
+(* ---------------------------------------------------------------- *)
+(*             Localizing Temproal Strengthenings - 2               *)
+(* ---------------------------------------------------------------- *)
+(*
+goalw thy [temp_strengthening_def,state_strengthening_def,
+temp_sat_def,satisfies_def,Init_def]
+"!! h. [| state_strengthening P Q h |]\
+\      ==> temp_strengthening (Init P) (Init Q) h";
+by (safe_tac set_cs);
+by (pair_tac "ex" 1);
+by (Seq_case_simp_tac "y" 1);
+
+
+
+goalw thy [temp_strengthening_def,state_strengthening_def]
+"!! h. [| temp_strengthening P Q h |]\
+\      ==> temp_strengthening ([] P) ([] Q) h";
+
+goalw thy [temp_strengthening_def,state_strengthening_def]
+"!! h. [| temp_strengthening P Q h |]\
+\      ==> temp_strengthening (Next P) (Next Q) h";
+
+*)
+
+(* ---------------------------------------------------------------- *)
+(*             Localizing Temproal Weakenings     - 2               *)
+(* ---------------------------------------------------------------- *)
+
+(*
+goalw thy [temp_weakening_def,state_weakening_def,
+temp_sat_def,satisfies_def,Init_def]
+"!! h. [| state_weakening P Q h |]\
+\      ==> temp_weakening (Init P) (Init Q) h";
+by (safe_tac set_cs);
+by (pair_tac "ex" 1);
+by (Seq_case_simp_tac "y" 1);
+
+
+
+goalw thy [temp_weakening_def,state_weakening_def]
+"!! h. [| temp_weakening P Q h |]\
+\      ==> temp_weakening ([] P) ([] Q) h";
+
+goalw thy [temp_weakening_def,state_weakening_def]
+"!! h. [| temp_weakening P Q h |]\
+\      ==> temp_weakening (Next P) (Next Q) h";
+
+*)
+
+(* ---------------------------------------------------------------- *)
+(*             Localizing Temproal Strengthenings - 3               *)
+(* ---------------------------------------------------------------- *)
+
+
+goalw thy [Diamond_def]
+"!! h. [| temp_strengthening P Q h |]\
+\      ==> temp_strengthening (<> P) (<> Q) h";
+br strength_NOT 1;
+br weak_Box 1;
+be weak_NOT 1;
+qed"strength_Diamond";
+
+goalw thy [Leadsto_def]
+"!! h. [| temp_weakening P1 P2 h;\
+\         temp_strengthening Q1 Q2 h |]\
+\      ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h";
+br strength_Box 1;
+be strength_IMPLIES 1;
+be strength_Diamond 1;
+qed"strength_Leadsto";
+
+
+(* ---------------------------------------------------------------- *)
+(*             Localizing Temporal Weakenings - 3                   *)
+(* ---------------------------------------------------------------- *)
+
+
+goalw thy [Diamond_def]
+"!! h. [| temp_weakening P Q h |]\
+\      ==> temp_weakening (<> P) (<> Q) h";
+br weak_NOT 1;
+br strength_Box 1;
+be strength_NOT 1;
+qed"weak_Diamond";
+
+goalw thy [Leadsto_def]
+"!! h. [| temp_strengthening P1 P2 h;\
+\         temp_weakening Q1 Q2 h |]\
+\      ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h";
+br weak_Box 1;
+be weak_IMPLIES 1;
+be weak_Diamond 1;
+qed"weak_Leadsto";
+
+goalw thy [WF_def]
+  " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ 
+\   ==> temp_weakening (WF A acts) (WF C acts) h";
+br weak_IMPLIES 1;
+br strength_Diamond 1;
+br strength_Box 1;
+br strength_Init 1;
+br weak_Box 2;
+br weak_Diamond 2;
+br weak_Init 2;
+by (auto_tac (claset(),
+              simpset() addsimps [state_weakening_def,state_strengthening_def,
+                             xt2_def,plift_def,option_lift_def,NOT_def]));
+qed"weak_WF";
+
+goalw thy [SF_def]
+  " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ 
+\   ==> temp_weakening (SF A acts) (SF C acts) h";
+br weak_IMPLIES 1;
+br strength_Box 1;
+br strength_Diamond 1;
+br strength_Init 1;
+br weak_Box 2;
+br weak_Diamond 2;
+br weak_Init 2;
+by (auto_tac (claset(),
+              simpset() addsimps [state_weakening_def,state_strengthening_def,
+                             xt2_def,plift_def,option_lift_def,NOT_def]));
+qed"weak_SF";
+
+
+val weak_strength_lemmas = 
+    [weak_OR,weak_AND,weak_NOT,weak_IMPLIES,weak_Box,weak_Next,weak_Init,
+     weak_Diamond,weak_Leadsto,strength_OR,strength_AND,strength_NOT,
+     strength_IMPLIES,strength_Box,strength_Next,strength_Init,
+     strength_Diamond,strength_Leadsto,weak_WF,weak_SF];
+
+fun abstraction_tac i = 
+    SELECT_GOAL (auto_tac (claset() addSIs weak_strength_lemmas,
+                           simpset() addsimps [state_strengthening_def,state_weakening_def])) i;
\ No newline at end of file
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/Abstraction.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,88 @@
+(*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
+    ID:         $Id$
+    Author:     Olaf M"uller
+    Copyright   1997  TU Muenchen
+
+Abstraction Theory -- tailored for I/O automata
+*)   
+
+		       
+Abstraction = LiveIOA + TLS + 
+
+default term
+
+
+consts
+
+  cex_abs   ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution"
+
+  is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
+
+  weakeningIOA       :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" 
+  temp_weakening     :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" 
+  temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" 
+
+  state_weakening       :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool"
+  state_strengthening   :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool"
+
+  is_live_abstraction  :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
+
+
+defs
+
+is_abstraction_def
+  "is_abstraction f C A ==                          
+   (!s:starts_of(C). f(s):starts_of(A)) &        
+   (!s t a. reachable C s & s -a--C-> t     
+            --> (f s) -a--A-> (f t))"
+
+is_live_abstraction_def
+  "is_live_abstraction h CL AM == 
+      is_abstraction h (fst CL) (fst AM) &
+      temp_weakening (snd AM) (snd CL) h"
+
+cex_abs_def
+  "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))`(snd ex))"
+
+weakeningIOA_def
+   "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A"
+
+temp_weakening_def
+   "temp_weakening Q P h == temp_strengthening (.~ Q) (.~ P) h"
+
+temp_strengthening_def
+   "temp_strengthening Q P h == ! ex. (cex_abs h ex |== Q) --> (ex |== P)"
+
+state_weakening_def
+  "state_weakening Q P h == state_strengthening (.~Q) (.~P) h"
+
+state_strengthening_def
+  "state_strengthening Q P h == ! s t a.  Q (h(s),a,h(t)) --> P (s,a,t)"
+
+rules
+
+strength_Init
+ "state_strengthening P Q h 
+  ==> temp_strengthening (Init P) (Init Q) h"
+
+strength_Box
+"temp_strengthening P Q h 
+ ==> temp_strengthening ([] P) ([] Q) h"
+
+strength_Next
+"temp_strengthening P Q h 
+ ==> temp_strengthening (Next P) (Next Q) h"
+
+weak_Init
+ "state_weakening P Q h 
+  ==> temp_weakening (Init P) (Init Q) h"
+
+weak_Box
+"temp_weakening P Q h 
+ ==> temp_weakening ([] P) ([] Q) h"
+
+weak_Next
+"temp_weakening P Q h 
+ ==> temp_weakening (Next P) (Next Q) h"
+
+end
\ No newline at end of file
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Mon Jan 12 17:26:34 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -32,6 +32,25 @@
   input_enabled	 ::"('a,'s)ioa => bool"
   IOA	         ::"('a,'s)ioa => bool"
 
+  (* constraints for fair IOA *)
+
+  fairIOA        ::"('a,'s)ioa => bool"
+  input_resistant::"('a,'s)ioa => bool"
+
+  (* enabledness of actions and action sets *)
+
+  enabled        ::"('a,'s)ioa => 'a => 's => bool"
+  Enabled    ::"('a,'s)ioa => 'a set => 's => bool"
+
+  (* action set keeps enabled until probably disabled by itself *) 
+
+  en_persistent  :: "('a,'s)ioa => 'a set => bool"
+
+ (* post_conditions for actions and action sets *)
+
+  was_enabled        ::"('a,'s)ioa => 'a => 's => bool"
+  set_was_enabled    ::"('a,'s)ioa => 'a set => 's => bool"
+
   (* reachability and invariants *)
   reachable     :: "('a,'s)ioa => 's set"
   invariant     :: "[('a,'s)ioa, 's=>bool] => bool"
@@ -209,6 +228,35 @@
    {rename_set s ren | s. s: wfair_of ioa},
    {rename_set s ren | s. s: sfair_of ioa})"
 
+(* ------------------------- fairness ----------------------------- *)
+
+fairIOA_def
+  "fairIOA A == (! S : wfair_of A. S<= local A) & 
+                (! S : sfair_of A. S<= local A)"
+
+input_resistant_def
+  "input_resistant A == ! W : sfair_of A. ! s a t. 
+                        reachable A s & reachable A t & a:inp A &
+                        Enabled A W s & s -a--A-> t
+                        --> Enabled A W t"
+
+enabled_def
+  "enabled A a s == ? t. s-a--A-> t"
+
+Enabled_def
+  "Enabled A W s == ? w:W. enabled A w s"
+
+en_persistent_def
+  "en_persistent A W == ! s a t. Enabled A W s & 
+                                 a ~:W & 
+                                 s -a--A-> t 
+                                 --> Enabled A W t"
+was_enabled_def
+  "was_enabled A a t == ? s. s-a--A-> t"
+
+set_was_enabled_def
+  "set_was_enabled A W t == ? w:W. was_enabled A w t"
+
 
 end
 
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/LiveIOA.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,73 @@
+(*  Title:      HOLCF/IOA/meta_theory/LiveIOA.ML
+    ID:         $Id$
+    Author:     Olaf M"uller
+    Copyright   1997  TU Muenchen
+
+Live I/O Automata
+
+*)   
+
+Delsimps [split_paired_Ex];
+
+goalw thy [live_implements_def] 
+"!! A. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
+\     ==> live_implements (A,LA) (C,LC)"; 
+auto();
+qed"live_implements_trans";
+
+
+section "Correctness of live refmap";
+	
+
+(* ---------------------------------------------------------------- *)
+(*                Correctness of live refmap                        *)
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "!! f. [| inp(C)=inp(A); out(C)=out(A); \
+\                  is_live_ref_map f (C,M) (A,L) |] \
+\               ==> live_implements (C,M) (A,L)";
+
+by (asm_full_simp_tac (simpset() addsimps [is_live_ref_map_def, live_implements_def,
+livetraces_def,liveexecutions_def]) 1);
+by (safe_tac set_cs);
+by (res_inst_tac[("x","corresp_ex A f ex")] exI 1);
+by (safe_tac set_cs);
+  (* Traces coincide, Lemma 1 *)
+  by (pair_tac "ex" 1);
+  by (etac (lemma_1 RS spec RS mp) 1);
+  by (simp_tac (simpset() addsimps [externals_def])1);
+  by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
+  by (asm_full_simp_tac (simpset() addsimps [executions_def,reachable.reachable_0]) 1);
+ 
+  (* corresp_ex is execution, Lemma 2 *)
+  by (pair_tac "ex" 1);
+  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
+  (* start state *) 
+  by (rtac conjI 1);
+  by (asm_full_simp_tac (simpset() addsimps [is_ref_map_def,corresp_ex_def]) 1);
+  (* is-execution-fragment *)
+  by (etac (lemma_2 RS spec RS mp) 1);
+  by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
+
+ (* Liveness *)
+auto();
+qed"live_implements";
+
+
+(*
+
+(* Classical Fairness and Fairness by Temporal Formula coincide *)
+ 
+goal thy "!! ex. Finite (snd ex) ==> \
+\          (ex |== WF A acts) = (~ Enabled A acts (laststate ex))";
+
+In 3 steps:
+
+1) []<>P and <>[]P mean both P (Last`s)
+2) Transform this to executions and laststate
+3) plift is used to show that plift (laststate ex) : acts == False. 
+
+
+
+*)
\ No newline at end of file
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/LiveIOA.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,62 @@
+(*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
+    ID:         $Id$
+    Author:     Olaf M"uller
+    Copyright   1997  TU Muenchen
+
+Live I/O automata -- specified by temproal formulas
+
+*) 
+  
+LiveIOA = IOA + TLS + 
+
+default term
+
+types
+
+ ('a,'s)live_ioa       = "('a,'s)ioa * ('a,'s)ioa_temp"
+ 
+consts
+
+validLIOA   :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool"
+
+WF         :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
+SF         :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
+
+liveexecutions    :: "('a,'s)live_ioa => ('a,'s)execution set"
+livetraces        :: "('a,'s)live_ioa => 'a trace set"
+live_implements   :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
+is_live_ref_map   :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
+
+ 
+defs
+
+validLIOA_def
+  "validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)"
+
+
+WF_def
+  "WF A acts ==  <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
+
+SF_def
+  "SF A acts ==  [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
+
+
+liveexecutions_def
+   "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
+
+livetraces_def
+  "livetraces AP == {mk_trace (fst AP)`(snd ex) | ex. ex:liveexecutions AP}"
+
+live_implements_def
+  "live_implements CL AM == (inp (fst CL) = inp (fst AM)) & 
+                            (out (fst CL) = out (fst AM)) &
+                            livetraces CL <= livetraces AM"
+
+is_live_ref_map_def
+   "is_live_ref_map f CL AM ==  
+            is_ref_map f (fst CL ) (fst AM) & 
+            (! exec : executions (fst CL). (exec |== (snd CL)) --> 
+                                           ((corresp_ex (fst AM) f exec) |== (snd AM)))"
+
+
+end
\ No newline at end of file
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/Pred.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,72 @@
+(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
+    ID:         $Id$
+    Author:     Olaf M"uller
+    Copyright   1997  TU Muenchen
+
+Logical Connectives lifted to predicates.
+
+ToDo:
+
+<--> einfuehren.
+
+*)   
+	       
+Pred = Arith +  
+
+default term
+
+types
+
+'a predicate      = "'a => bool"
+
+consts
+
+satisfies    ::"'a  => 'a predicate => bool"    ("_ |= _" [100,9] 8)
+valid        ::"'a predicate => bool"           (*  ("|-") *)         
+
+NOT          ::"'a predicate => 'a predicate"  (".~ _" [40] 40)
+AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".&" 35)
+OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".|" 30)
+IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)
+
+
+syntax ("" output)
+  "NOT"     ::"'a predicate => 'a predicate" ("~ _" [40] 40)
+  "AND"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "&" 35)
+  "OR"      ::"'a predicate => 'a predicate => 'a predicate"    (infixr "|" 30)
+  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "-->" 25)
+
+syntax (symbols output)
+  "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
+  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)
+  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)
+  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<midarrow>\\<rightarrow>" 25)
+
+syntax (symbols)
+  "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)
+
+
+defs
+
+satisfies_def
+   "s |= P  == P s" 
+
+(* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)
+valid_def
+   "valid P == (! s. (s |= P))"
+
+
+NOT_def
+  "NOT P s ==  ~ (P s)"
+
+AND_def
+  "(P .& Q) s == (P s) & (Q s)"
+
+
+OR_def
+  "(P .| Q) s ==  (P s) | (Q s)"
+
+IMPLIES_def
+  "(P .--> Q) s == (P s) --> (Q s)"
+
+end
\ No newline at end of file
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Jan 12 17:26:34 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Jan 12 17:48:23 1998 +0100
@@ -248,6 +248,97 @@
 qed"trace_inclusion"; 
 
 
+(* -------------------------------------------------------------------------------- *)
+
+section "Corollary:  F A I R  T R A C E - I N C L U S I O N";
+
+(* -------------------------------------------------------------------------------- *)
+
+
+goalw thy [fin_often_def] "(~inf_often P s) = fin_often P s";
+auto();
+qed"fininf";
+
+
+goal thy 
+"is_wfair A W (s,ex) = \
+\ (fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)";
+by (asm_full_simp_tac (simpset() addsimps [is_wfair_def,fin_often_def])1);
+auto();
+qed"WF_alt";
+
+goal thy  
+"!! ex. [|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; \
+\         en_persistent A W|] \
+\   ==> inf_often (%x. fst x :W) ex";
+bd persistent 1;
+ba 1;
+by (asm_full_simp_tac (simpset() addsimps [WF_alt])1);
+auto();
+qed"WF_persistent";
+
+
+goal thy "!! C A. \
+\         [| is_ref_map f C A; ext C = ext A; \
+\         !! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |] \
+\         ==> fairtraces C <= fairtraces A";
+by (simp_tac (simpset() addsimps [fairtraces_def,
+   fairexecutions_def]) 1);
+by (safe_tac set_cs);
+by (res_inst_tac[("x","corresp_ex A f ex")] exI 1);
+by (safe_tac set_cs);
+
+  (* Traces coincide, Lemma 1 *)
+  by (pair_tac "ex" 1);
+  by (etac (lemma_1 RS spec RS mp) 1);
+  by (REPEAT (atac 1));
+  by (asm_full_simp_tac (simpset() addsimps [executions_def,reachable.reachable_0]) 1);
+ 
+  (* corresp_ex is execution, Lemma 2 *)
+  by (pair_tac "ex" 1);
+  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
+  (* start state *) 
+  by (rtac conjI 1);
+  by (asm_full_simp_tac (simpset() addsimps [is_ref_map_def,corresp_ex_def]) 1);
+  (* is-execution-fragment *)
+  by (etac (lemma_2 RS spec RS mp) 1);
+  by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
+
+ (* Fairness *)
+auto();
+qed"fair_trace_inclusion";
+
+goal thy "!! C A. \
+\         [| inp(C) = inp(A); out(C)=out(A); \
+\            is_fair_ref_map f C A |] \
+\         ==> fair_implements C A";
+by (asm_full_simp_tac (simpset() addsimps [is_fair_ref_map_def, fair_implements_def,
+    fairtraces_def, fairexecutions_def]) 1);
+by (safe_tac set_cs);
+by (res_inst_tac[("x","corresp_ex A f ex")] exI 1);
+by (safe_tac set_cs);
+  (* Traces coincide, Lemma 1 *)
+  by (pair_tac "ex" 1);
+  by (etac (lemma_1 RS spec RS mp) 1);
+  by (simp_tac (simpset() addsimps [externals_def])1);
+  by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
+  by (asm_full_simp_tac (simpset() addsimps [executions_def,reachable.reachable_0]) 1);
+ 
+  (* corresp_ex is execution, Lemma 2 *)
+  by (pair_tac "ex" 1);
+  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
+  (* start state *) 
+  by (rtac conjI 1);
+  by (asm_full_simp_tac (simpset() addsimps [is_ref_map_def,corresp_ex_def]) 1);
+  (* is-execution-fragment *)
+  by (etac (lemma_2 RS spec RS mp) 1);
+  by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
+
+ (* Fairness *)
+auto();
+qed"fair_trace_inclusion2";
 
 
 
+
+
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/RefCorrectness.thy
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Mon Jan 12 17:26:34 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -15,7 +15,7 @@
                   ('a,'s1)execution => ('a,'s2)execution"
   corresp_exC  ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
                    -> ('s1 => ('a,'s2)pairs)"
-
+  is_fair_ref_map  :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool"
 
 defs
 
@@ -30,6 +30,40 @@
                               @@ ((h`xs) (snd pr)))
                         `x) )))"
  
+is_fair_ref_map_def
+  "is_fair_ref_map f C A == 
+       is_ref_map f C A &
+       (! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex))"
+
 
 
+rules
+(* Axioms for fair trace inclusion proof support, not for the correctness proof
+   of refeinment mappings ! *)
+
+corresp_laststate
+  "Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))"
+
+corresp_Finite
+  "Finite (snd (corresp_ex A f (s,ex))) = Finite ex"
+
+FromAtoC
+  "fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex"
+
+FromCtoA
+  "inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))"
+
+
+(* Proof by case on inf W in ex: If so, ok. If not, only fin W in ex, ie there is
+   an index i from which on no W in ex. But W inf enabled, ie at least once after i
+   W is enabled. As W does not occur after i and W is enabling_persistent, W keeps
+   enabled until infinity, ie. indefinitely *)
+persistent
+  "[|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W|]
+   ==> inf_often (%x. fst x :W) ex | fin_often (%x. ~Enabled A W (snd x)) ex"
+
+infpostcond
+  "[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|]
+    ==> inf_often (% x. set_was_enabled A W (snd x)) ex"
+
 end
\ No newline at end of file
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/RefMappings.ML
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Jan 12 17:26:34 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Jan 12 17:48:23 1998 +0100
@@ -8,33 +8,6 @@
 
 
 
-(* ---------------------------------------------------------------------------- *)
-                           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";
 
 
 (* ---------------------------------------------------------------------------- *)
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/RefMappings.thy
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Mon Jan 12 17:26:34 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -11,17 +11,14 @@
 default term
 
 consts
-  laststate    ::"('a,'s)execution => 's"
+
   move         ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool"
   is_ref_map   ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
   is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
  
+
 defs
 
-laststate_def
-  "laststate ex == case Last`(snd ex) of
-                      Undef  => fst ex
-                    | Def at => snd at"
 
 move_def
   "move ioa ex s a t ==    
@@ -45,4 +42,5 @@
                  then (f s) -a--A-> (f t)
                  else (f s)=(f t)))" 
 
+
 end
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Jan 12 17:26:34 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -29,7 +29,7 @@
 
 syntax
 
- "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_>>_)"  [66,65] 65)
+ "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_/>>_)"  [66,65] 65)
  (* list Enumeration *)
   "_totlist"      :: args => 'a Seq                          ("[(_)!]")
   "_partlist"     :: args => 'a Seq                          ("[(_)?]")
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/TL.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/TL.ML	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,179 @@
+(*  Title:      HOLCF/IOA/meta_theory/TL.ML
+    ID:         $Id$
+    Author:     Olaf M"uller
+    Copyright   1997  TU Muenchen
+
+Temporal Logic 
+*)   
+
+
+goal thy "[] <> (.~ P) = (.~ <> [] P)";
+br ext 1;
+by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
+auto();
+qed"simple_try";
+
+goal thy "nil |= [] P";
+by (asm_full_simp_tac (simpset() addsimps [satisfies_def,
+     Box_def,tsuffix_def,suffix_def,nil_is_Conc])1);
+qed"Boxnil";
+
+goal thy "~(nil |= <> P)";
+by (simp_tac (simpset() addsimps [Diamond_def,satisfies_def,NOT_def])1);
+by (cut_inst_tac [] Boxnil 1);
+by (asm_full_simp_tac (simpset() addsimps [satisfies_def])1);
+qed"Diamondnil";
+
+goal thy "(<> F) s = (? s2. tsuffix s2 s & F s2)";
+by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
+qed"Diamond_def2";
+
+
+
+section "TLA Axiomatization by Merz";
+
+(* ---------------------------------------------------------------- *)
+(*                 TLA Axiomatization by Merz                       *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "suffix s s";
+by (simp_tac (simpset() addsimps [suffix_def])1);
+by (res_inst_tac [("x","nil")] exI 1);
+auto();
+qed"suffix_refl";
+
+goal thy "s~=UU & s~=nil --> (s |= [] F .--> F)";
+by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def])1);
+by (REPEAT (rtac impI 1));
+by (eres_inst_tac [("x","s")] allE 1);
+by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
+qed"reflT";
+
+
+goal thy "!!x. [| suffix y x ; suffix z y |]  ==> suffix z x";
+by (asm_full_simp_tac (simpset() addsimps [suffix_def])1);
+auto();
+by (res_inst_tac [("x","s1 @@ s1a")] exI 1);
+auto();
+by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
+qed"suffix_trans";
+
+goal thy "s |= [] F .--> [] [] F";
+by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def,tsuffix_def])1);
+auto();
+bd suffix_trans 1;
+ba 1;
+by (eres_inst_tac [("x","s2a")] allE 1);
+auto();
+qed"transT";
+
+
+goal thy "s |= [] (F .--> G) .--> [] F .--> [] G";
+by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def])1);
+qed"normalT";
+
+
+(*
+goal thy "s |= <> F .& <> G .--> (<> (F .& <> G) .| <> (G .& <> F))";
+by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,AND_def,OR_def,Diamond_def2])1);
+br impI 1;
+be conjE 1;
+be exE 1;
+be exE 1;
+
+
+br disjI1 1;
+
+goal thy "!!s. [| tsuffix s1 s ; tsuffix s2 s|] ==> tsuffix s2 s1 | tsuffix s1 s2";
+by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
+by (REPEAT (etac conjE 1));
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+by (hyp_subst_tac 1);
+
+*)
+
+
+section "TLA Rules by Lamport";
+
+(* ---------------------------------------------------------------- *)
+(*                      TLA Rules by Lamport                        *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "!! P. validT P ==> validT ([] P)";
+by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Box_def,tsuffix_def])1);
+qed"STL1a";
+
+goal thy "!! P. valid P ==> validT (Init P)";
+by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,Init_def])1);
+qed"STL1b";
+
+goal thy "!! P. valid P ==> validT ([] (Init P))";
+br STL1a 1;
+be STL1b 1;
+qed"STL1";
+
+(* Note that unlift and HD is not at all used !!! *)
+goal thy "!! P. valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
+by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
+qed"STL4";
+
+
+section "LTL Axioms by Manna/Pnueli";
+
+(* ---------------------------------------------------------------- *)
+(*                LTL Axioms by Manna/Pnueli                        *)
+(* ---------------------------------------------------------------- *)
+
+
+goalw thy [tsuffix_def,suffix_def]
+"s~=UU & s~=nil --> tsuffix s2 (TL`s) --> tsuffix s2 s";
+auto();
+by (Seq_case_simp_tac "s" 1);
+by (res_inst_tac [("x","a>>s1")] exI 1);
+auto();
+qed_spec_mp"tsuffix_TL";
+
+val tsuffix_TL2 = conjI RS tsuffix_TL;
+
+
+goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] 
+   "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
+auto();
+(* []F .--> F *)
+by (eres_inst_tac [("x","s")] allE 1);
+by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
+(* []F .--> Next [] F *)
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+auto();
+bd tsuffix_TL2 1;
+by (REPEAT (atac 1));
+auto();
+qed"LTL1";
+
+
+goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
+    "s |= .~ (Next F) .--> (Next (.~ F))";
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+qed"LTL2a";
+
+goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
+    "s |= (Next (.~ F)) .--> (.~ (Next F))";
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+qed"LTL2b";
+
+goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
+"ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)";
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+qed"LTL3";
+
+goalw thy [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] 
+ "s |= [] (F .--> Next F) .--> F .--> []F";
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+auto();
+
+
+by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
+auto();
+
+
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/TL.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/TL.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,81 @@
+(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
+    ID:         $Id$
+    Author:     Olaf M"uller
+    Copyright   1997  TU Muenchen
+
+A General Temporal Logic
+
+Version 2: Interface directly after Sequeces, i.e. predicates and predicate transformers are in HOL
+
+*)   
+
+
+		       
+TL = Pred + Sequence +  
+
+default term
+
+types
+
+'a temporal      = 'a Seq predicate
+
+ 
+consts
+
+
+suffix     :: "'a Seq => 'a Seq => bool"
+tsuffix    :: "'a Seq => 'a Seq => bool"
+
+validT     :: "'a Seq predicate => bool"
+
+unlift     ::  "'a lift => 'a"
+
+Init         ::"'a predicate => 'a temporal"          ("<_>" [0] 1000)
+
+Box          ::"'a temporal => 'a temporal"   ("[] (_)" [80] 80)
+Diamond      ::"'a temporal => 'a temporal"   ("<> (_)" [80] 80)
+Next         ::"'a temporal => 'a temporal"   
+Leadsto      ::"'a temporal => 'a temporal => 'a temporal"  (infixr "~>" 22)
+
+syntax (symbols)
+   "Box"        ::"'a temporal => 'a temporal"   ("\\<box> (_)" [80] 80)
+   "Diamond"    ::"'a temporal => 'a temporal"   ("\\<diamond> (_)" [80] 80)
+   "Leadsto"    ::"'a temporal => 'a temporal => 'a temporal"  (infixr "\\<leadsto>" 22)
+ 
+defs
+
+
+unlift_def
+  "unlift x == (case x of 
+                 Undef   => arbitrary
+               | Def y   => y)"
+
+(* this means that for nil and UU the effect is unpredictable *)
+Init_def
+  "Init P s ==  (P (unlift (HD`s)))" 
+
+
+(* FIX: Introduce nice symbol infix suntax *)
+suffix_def
+  "suffix s2 s == ? s1. (Finite s1  & s = s1 @@ s2)" 
+
+(* FIX: Introduce nice symbol infix suntax *)
+tsuffix_def
+  "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"
+
+Box_def
+  "([] P) s == ! s2. tsuffix s2 s --> P s2"
+
+Next_def
+  "(Next P) s == if TL`s=UU then (P s) else P (TL`s)"
+
+Diamond_def
+  "<> P == .~ ([] (.~ P))"
+
+Leadsto_def
+   "P ~> Q == ([] (P .--> (<> Q)))"  
+
+validT_def
+  "validT P == ! s. s~=UU & s~=nil --> (s |= P)"
+
+end
\ No newline at end of file
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/TLS.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,87 @@
+(*  Title:      HOLCF/IOA/meta_theory/TLS.ML
+    ID:         $Id$
+    Author:     Olaf M"uller
+    Copyright   1997  TU Muenchen
+
+Temporal Logic of Steps -- tailored for I/O automata
+*)   
+
+
+(* ---------------------------------------------------------------- *)
+(*                                 ex2seqC                          *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "ex2seqC  = (LAM ex. (%s. case ex of \
+\      nil =>  (s,None,s)>>nil   \
+\    | x##xs => (flift1 (%pr. \
+\                (s,Some (fst pr), snd pr)>> (ex2seqC`xs) (snd pr))  \
+\                `x)  \
+\      ))";
+by (rtac trans 1);
+by (rtac fix_eq2 1);
+by (rtac ex2seqC_def 1);
+by (rtac beta_cfun 1);
+by (simp_tac (simpset() addsimps [flift1_def]) 1);
+qed"ex2seqC_unfold";
+
+goal thy "(ex2seqC `UU) s=UU";
+by (stac ex2seqC_unfold 1);
+by (Simp_tac 1);
+qed"ex2seqC_UU";
+
+goal thy "(ex2seqC `nil) s = (s,None,s)>>nil";
+by (stac ex2seqC_unfold 1);
+by (Simp_tac 1);
+qed"ex2seqC_nil";
+
+goal thy "(ex2seqC `((a,t)>>xs)) s = \
+\          (s,Some a,t)>> ((ex2seqC`xs) t)";
+by (rtac trans 1);
+by (stac ex2seqC_unfold 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
+qed"ex2seqC_cons";
+
+Addsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons];
+
+
+goal thy "ex2seq (s, UU) = UU";
+by (simp_tac (simpset() addsimps [ex2seq_def]) 1);
+qed"ex2seq_UU";
+
+goal thy "ex2seq (s, nil) = (s,None,s)>>nil";
+by (simp_tac (simpset() addsimps [ex2seq_def]) 1);
+qed"ex2seq_nil";
+
+goal thy "ex2seq (s, (a,t)>>ex) = (s,Some a,t) >> ex2seq (t, ex)";
+by (simp_tac (simpset() addsimps [ex2seq_def]) 1);
+qed"ex2seq_cons";
+
+Delsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons]; 
+Addsimps [ex2seq_UU,ex2seq_nil, ex2seq_cons];  
+
+
+
+(* FIX: Not true for UU, as ex2seq is defined continously !!!!! *)
+goal thy "ex2seq exec ~= UU & ex2seq exec ~= nil";
+
+
+goal thy "ex |== [] P .--> P";
+
+
+(* ----------------------------------------------------------- *)
+(*           Interface TL -- TLS                               *)
+(* ---------------------------------------------------------- *)
+
+goalw thy [Init_def,Next_def,temp_sat_def,satisfies_def,IMPLIES_def,AND_def]
+ "!! s. (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 (simpset() setloop split_tac [expand_if]) 1);
+by (pair_tac "ex" 1);
+by (Seq_case_simp_tac "y" 1);
+
+
+
+
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/TLS.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,80 @@
+(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
+    ID:         $Id$
+    Author:     Olaf M"uller
+    Copyright   1997  TU Muenchen
+
+Temporal Logic of Steps -- tailored for I/O automata
+*)   
+
+		       
+TLS = IOA + TL + 
+
+default term
+
+types
+
+ ('a,'s)ioa_temp       = "('a option,'s)transition temporal" 
+ ('a,'s)step_pred      = "('a option,'s)transition predicate"
+  's state_pred        = "'s predicate"
+ 
+consts
+
+
+option_lift :: "('a => 'b) => 'b => ('a option => 'b)"
+plift       :: "('a => bool) => ('a option => bool)"
+ 
+temp_sat   :: "('a,'s)execution => ('a,'s)ioa_temp => bool"    (infixr "|==" 22)
+xt1        :: "'s predicate => ('a,'s)step_pred"
+xt2        :: "'a option predicate => ('a,'s)step_pred"
+
+validTE    :: "('a,'s)ioa_temp => bool"
+validIOA   :: "('a,'s)ioa => ('a,'s)ioa_temp => bool"
+
+
+ex2seq     :: "('a,'s)execution => ('a option,'s)transition Seq"
+ex2seqC    :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" 
+
+
+defs
+
+(* should be in Option as option_lift1, and option_map should be renamed to 
+   option_lift2 *)
+option_lift_def
+  "option_lift f s y == case y of None => s | Some x => (f x)"
+
+(* plift is used to determine that None action is always false in 
+   transition predicates *)
+plift_def
+  "plift P == option_lift P False"
+
+temp_sat_def
+  "ex |== P == ((ex2seq ex) |= P)"
+
+xt1_def
+  "xt1 P tr == P (fst tr)"
+
+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))"
+
+ex2seqC_def
+  "ex2seqC == (fix`(LAM h ex. (%s. case ex of 
+      nil =>  (s,None,s)>>nil
+    | x##xs => (flift1 (%pr.
+                (s,Some (fst pr), snd pr)>> (h`xs) (snd pr)) 
+                `x)
+      )))"
+
+validTE_def
+  "validTE P == ! ex. (ex |== P)"
+
+validIOA_def
+  "validIOA A P == ! ex : executions A . (ex |== P)"
+
+
+end
+
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/Traces.ML
--- 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";
+
 
 (* -------------------------------------------------------------------------------- *)
 
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Mon Jan 12 17:26:34 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -37,8 +37,29 @@
   traces        :: "('a,'s)ioa => 'a trace set"
   mk_trace      :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace"
 
-  (* Notion of implementation *)
+  laststate    ::"('a,'s)execution => 's"
+
+  (* A predicate holds infinitely (finitely) often in a sequence *)
+
+  inf_often      ::"('a => bool) => 'a Seq => bool"
+  fin_often      ::"('a => bool) => 'a Seq => bool"
+
+  (* fairness of executions *)
+
+  wfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
+  sfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
+  is_wfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
+  is_sfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
+  fair_ex        ::"('a,'s)ioa => ('a,'s)execution => bool"
+
+  (* fair behavior sets *)
+ 
+  fairexecutions ::"('a,'s)ioa => ('a,'s)execution set"
+  fairtraces     ::"('a,'s)ioa => 'a trace set"
+
+  (* Notions of implementation *)
   "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool"   (infixr 12) 
+  fair_implements  :: "('a,'s1)ioa => ('a,'s2)ioa => bool"
 
   (* Execution, schedule and trace modules *)
   Execs         ::  "('a,'s)ioa => ('a,'s)execution_module"
@@ -97,7 +118,7 @@
 has_trace_def
   "has_trace ioa tr ==                                               
      (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))`sch)"
-
+ 
 traces_def
   "traces ioa == {tr. has_trace ioa tr}"
 
@@ -107,6 +128,53 @@
      Filter (%a. a:ext(ioa))`(filter_act`tr)"
 
 
+(*  ------------------- Fair Traces ------------------------------ *)
+
+laststate_def
+  "laststate ex == case Last`(snd ex) of
+                      Undef  => fst ex
+                    | Def at => snd at"
+
+inf_often_def
+  "inf_often P s == Infinite (Filter P`s)"
+
+(*  filtering P yields a finite or partial sequence *)
+fin_often_def
+  "fin_often P s == ~inf_often P s"
+
+(* Note that partial execs cannot be wfair as the inf_often predicate in the 
+   else branch prohibits it. However they can be sfair in the case when all W 
+   are only finitely often enabled: FIX Is this the right model? *)
+wfair_ex_def
+  "wfair_ex A ex == ! W : wfair_of A.  
+                      if   Finite (snd ex) 
+                      then ~Enabled A W (laststate ex)
+                      else is_wfair A W ex"
+
+is_wfair_def
+  "is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex)
+                     | inf_often (%x.~Enabled A W (snd x)) (snd ex))"
+
+sfair_ex_def
+  "sfair_ex A ex == ! W : sfair_of A.
+                      if   Finite (snd ex) 
+                      then ~Enabled A W (laststate ex)
+                      else is_sfair A W ex"
+
+is_sfair_def
+  "is_sfair A W ex ==  (inf_often (%x. fst x:W) (snd ex)
+                      | fin_often (%x. Enabled A W (snd x)) (snd ex))"
+
+fair_ex_def
+  "fair_ex A ex == wfair_ex A ex & sfair_ex A ex"
+
+fairexecutions_def
+  "fairexecutions A == {ex. ex:executions A & fair_ex A ex}"
+
+fairtraces_def
+  "fairtraces A == {mk_trace A`(snd ex) | ex. ex:fairexecutions A}"
+
+
 (*  ------------------- Implementation ------------------------------ *)
 
 ioa_implements_def
@@ -115,6 +183,10 @@
      (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) &
       traces(ioa1) <= traces(ioa2))"
 
+fair_implements_def
+  "fair_implements C A == inp(C) = inp(A) &  out(C)=out(A) &
+                          fairtraces(C) <= fairtraces(A)"
+
 (*  ------------------- Modules ------------------------------ *)
 
 Execs_def
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/TrivEx.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/TrivEx.ML	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,39 @@
+(*  Title:      HOLCF/IOA/TrivEx.thy
+    ID:         $Id$
+    Author:     Olaf Mueller
+    Copyright   1995  TU Muenchen
+
+Trivial Abstraction Example
+*)
+
+val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
+  by(fast_tac (claset() addDs prems) 1);
+qed "imp_conj_lemma";
+
+
+goalw  thy [is_abstraction_def] 
+"is_abstraction h_abs C_ioa A_ioa";
+by (rtac conjI 1);
+(* ------------- start states ------------ *)
+by (simp_tac (simpset() addsimps 
+    [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
+(* -------------- step case ---------------- *)
+by (REPEAT (rtac allI 1));
+by (rtac imp_conj_lemma 1);
+by (simp_tac (simpset() addsimps [trans_of_def,
+        C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
+by (simp_tac (simpset() addsimps [h_abs_def]) 1);
+by (action.induct_tac "a" 1);
+auto();
+qed"h_abs_is_abstraction";
+
+
+goal thy "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
+br AbsRuleT1 1;
+br h_abs_is_abstraction 1;
+br MC_result 1;
+by (abstraction_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
+qed"TrivEx_abstraction";
+
+
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/TrivEx.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/TrivEx.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,61 @@
+(*  Title:      HOLCF/IOA/TrivEx.thy
+    ID:         $Id$
+    Author:     Olaf Mueller
+    Copyright   1995  TU Muenchen
+
+Trivial Abstraction Example
+*)
+
+TrivEx = Abstraction + TLS + IOA +
+
+datatype action = INC
+
+consts
+
+C_asig   ::  action signature
+C_trans  :: (action, nat)transition set
+C_ioa    :: (action, nat)ioa
+
+A_asig   :: action signature
+A_trans  :: (action, bool)transition set
+A_ioa    :: (action, bool)ioa
+
+h_abs    :: "nat => bool"
+
+defs
+
+C_asig_def
+  "C_asig == ({},{INC},{})"
+
+C_trans_def "C_trans ==                                           
+ {tr. let s = fst(tr);                                               
+          t = snd(snd(tr))                                           
+      in case fst(snd(tr))                                           
+      of                                                             
+      INC       => t = Suc(s)}"
+
+C_ioa_def "C_ioa == 
+ (C_asig, {0}, C_trans,{},{})"
+
+A_asig_def
+  "A_asig == ({},{INC},{})"
+
+A_trans_def "A_trans ==                                           
+ {tr. let s = fst(tr);                                               
+          t = snd(snd(tr))                                           
+      in case fst(snd(tr))                                           
+      of                                                             
+      INC       => t = True}"
+
+A_ioa_def "A_ioa == 
+ (A_asig, {False}, A_trans,{},{})"
+
+h_abs_def
+  "h_abs n == n~=0"
+
+rules
+
+MC_result
+  "validIOA A_ioa (<>[] <%(b,a,c). b>)"
+
+end
\ No newline at end of file
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/TrivEx2.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,66 @@
+(*  Title:      HOLCF/IOA/TrivEx.thy
+    ID:         $Id$
+    Author:     Olaf Mueller
+    Copyright   1995  TU Muenchen
+
+Trivial Abstraction Example
+*)
+
+val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
+  by(fast_tac (claset() addDs prems) 1);
+qed "imp_conj_lemma";
+
+
+goalw  thy [is_abstraction_def] 
+"is_abstraction h_abs C_ioa A_ioa";
+by (rtac conjI 1);
+(* ------------- start states ------------ *)
+by (simp_tac (simpset() addsimps 
+    [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
+(* -------------- step case ---------------- *)
+by (REPEAT (rtac allI 1));
+by (rtac imp_conj_lemma 1);
+by (simp_tac (simpset() addsimps [trans_of_def,
+        C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
+by (simp_tac (simpset() addsimps [h_abs_def]) 1);
+by (action.induct_tac "a" 1);
+auto();
+qed"h_abs_is_abstraction";
+
+
+(*
+goalw thy [xt2_def,plift,option_lift]
+  "(xt2 (plift afun)) (s,a,t) = (afun a)";
+(* !!!!!!!!!!!!! Occurs check !!!! *)
+by (option.induct_tac "a" 1);
+
+*)
+
+goalw thy [Enabled_def, enabled_def, h_abs_def,A_ioa_def,C_ioa_def,A_trans_def,
+           C_trans_def,trans_of_def] 
+"!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s";
+auto();
+qed"Enabled_implication";
+
+
+goalw thy [is_live_abstraction_def]
+"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})";
+auto();
+(* is_abstraction *)
+br h_abs_is_abstraction 1;
+(* temp_weakening *)
+by (abstraction_tac 1);
+be Enabled_implication 1;
+qed"h_abs_is_liveabstraction";
+
+
+goalw thy [C_live_ioa_def]
+"validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";
+br AbsRuleT2 1;
+br h_abs_is_liveabstraction 1;
+br MC_result 1;
+by (abstraction_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
+qed"TrivEx2_abstraction";
+
+
diff -r 31becfd8d329 -r 8e604d885b54 src/HOLCF/IOA/meta_theory/TrivEx2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/TrivEx2.thy	Mon Jan 12 17:48:23 1998 +0100
@@ -0,0 +1,71 @@
+(*  Title:      HOLCF/IOA/TrivEx.thy
+    ID:         $Id$
+    Author:     Olaf Mueller
+    Copyright   1995  TU Muenchen
+
+Trivial Abstraction Example with fairness
+*)
+
+TrivEx2 = Abstraction + TLS + IOA +
+
+datatype action = INC
+
+consts
+
+C_asig   ::  action signature
+C_trans  :: (action, nat)transition set
+C_ioa    :: (action, nat)ioa
+C_live_ioa :: (action, nat)live_ioa
+
+A_asig   :: action signature
+A_trans  :: (action, bool)transition set
+A_ioa    :: (action, bool)ioa
+A_live_ioa :: (action, bool)live_ioa
+
+h_abs    :: "nat => bool"
+
+defs
+
+C_asig_def
+  "C_asig == ({},{INC},{})"
+
+C_trans_def "C_trans ==                                           
+ {tr. let s = fst(tr);                                               
+          t = snd(snd(tr))                                           
+      in case fst(snd(tr))                                           
+      of                                                             
+      INC       => t = Suc(s)}"
+
+C_ioa_def "C_ioa == 
+ (C_asig, {0}, C_trans,{},{})"
+
+C_live_ioa_def 
+  "C_live_ioa == (C_ioa, WF C_ioa {INC})"
+
+A_asig_def
+  "A_asig == ({},{INC},{})"
+
+A_trans_def "A_trans ==                                           
+ {tr. let s = fst(tr);                                               
+          t = snd(snd(tr))                                           
+      in case fst(snd(tr))                                           
+      of                                                             
+      INC       => t = True}"
+
+A_ioa_def "A_ioa == 
+ (A_asig, {False}, A_trans,{},{})"
+
+A_live_ioa_def 
+  "A_live_ioa == (A_ioa, WF A_ioa {INC})"
+
+
+
+h_abs_def
+  "h_abs n == n~=0"
+
+rules
+
+MC_result
+  "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
+
+end
\ No newline at end of file