# HG changeset patch # User mueller # Date 924771995 -7200 # Node ID f3015fd68d66fdbbad0844fad5b91784dc7e901b # Parent bafd705ee38ec5cd498d874f28d73020e8655e53 moved this trivial example to new ex dir; diff -r bafd705ee38e -r f3015fd68d66 src/HOLCF/IOA/ex/ROOT.ML --- /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"; diff -r bafd705ee38e -r f3015fd68d66 src/HOLCF/IOA/ex/TrivEx.ML --- /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"; + + diff -r bafd705ee38e -r f3015fd68d66 src/HOLCF/IOA/ex/TrivEx.thy --- /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 diff -r bafd705ee38e -r f3015fd68d66 src/HOLCF/IOA/ex/TrivEx2.ML --- /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))))"; + +*) + diff -r bafd705ee38e -r f3015fd68d66 src/HOLCF/IOA/ex/TrivEx2.thy --- /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