--- /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
--- /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
--- 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
--- /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
--- /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
--- /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
--- 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";
+
+
--- 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
--- 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";
(* ---------------------------------------------------------------------------- *)
--- 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
--- 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 ("[(_)?]")
--- /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();
+
+
--- /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
--- /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);
+
+
+
+
--- /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
+
--- 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";
+
(* -------------------------------------------------------------------------------- *)
--- 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
--- /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";
+
+
--- /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
--- /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";
+
+
--- /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