--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ex/ROOT.ML Thu Apr 22 11:06:35 1999 +0200
@@ -0,0 +1,14 @@
+(* Title: HOL/IOA/ex/ROOT.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1997 TU Muenchen
+
+This is the ROOT file for the formalization of a semantic model of
+I/O-Automata. See the README.html file for details.
+*)
+
+goals_limit := 1;
+
+
+use_thy "TrivEx";
+use_thy "TrivEx2";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ex/TrivEx.ML Thu Apr 22 11:06:35 1999 +0200
@@ -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 [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 (induct_tac "a" 1);
+by Auto_tac;
+qed"h_abs_is_abstraction";
+
+
+Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
+by (rtac AbsRuleT1 1);
+by (rtac h_abs_is_abstraction 1);
+by (rtac 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/ex/TrivEx.thy Thu Apr 22 11:06:35 1999 +0200
@@ -0,0 +1,61 @@
+(* Title: HOLCF/IOA/TrivEx.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 TU Muenchen
+
+Trivial Abstraction Example
+*)
+
+TrivEx = Abstraction +
+
+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/ex/TrivEx2.ML Thu Apr 22 11:06:35 1999 +0200
@@ -0,0 +1,72 @@
+(* 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 [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 (induct_tac "a" 1);
+by Auto_tac;
+qed"h_abs_is_abstraction";
+
+
+(*
+Goalw [xt2_def,plift,option_lift]
+ "(xt2 (plift afun)) (s,a,t) = (afun a)";
+(* !!!!!!!!!!!!! Occurs check !!!! *)
+by (induct_tac "a" 1);
+
+*)
+
+Goalw [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";
+by Auto_tac;
+qed"Enabled_implication";
+
+
+Goalw [is_live_abstraction_def]
+"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})";
+by Auto_tac;
+(* is_abstraction *)
+by (rtac h_abs_is_abstraction 1);
+(* temp_weakening *)
+by (abstraction_tac 1);
+by (etac Enabled_implication 1);
+qed"h_abs_is_liveabstraction";
+
+
+Goalw [C_live_ioa_def]
+"validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";
+by (rtac AbsRuleT2 1);
+by (rtac h_abs_is_liveabstraction 1);
+by (rtac MC_result 1);
+by (abstraction_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
+qed"TrivEx2_abstraction";
+
+
+(*
+Goal "validIOA aut_ioa (Box (Init (%(s,a,t). a= Some(Alarm(APonR))))
+IMPLIES (Next (Init (%(s,a,t). info_comp(s) = APonR))))";
+
+*)
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ex/TrivEx2.thy Thu Apr 22 11:06:35 1999 +0200
@@ -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 + 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