--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Storage/Action.ML Wed Dec 02 15:55:39 1998 +0100
@@ -0,0 +1,13 @@
+(* Title: HOLCF/IOA/ABP/Action.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1997 TU Muenchen
+
+Derived rules for actions
+*)
+
+Goal "!!x. x = y ==> action_case a b c x = \
+\ action_case a b c y";
+by (Asm_simp_tac 1);
+
+Addcongs [result()];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Storage/Action.thy Wed Dec 02 15:55:39 1998 +0100
@@ -0,0 +1,11 @@
+(* Title: HOLCF/IOA/ABP/Action.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1997 TU Muenchen
+
+The set of all actions of the system
+*)
+
+Action = Main +
+datatype action = New | Loc nat | Free nat
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Storage/Correctness.ML Wed Dec 02 15:55:39 1998 +0100
@@ -0,0 +1,74 @@
+(* Title: HOL/IOA/example/Correctness.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1997 TU Muenchen
+
+Correctness Proof
+*)
+
+
+Addsimps [split_paired_All];
+Delsimps [split_paired_Ex];
+
+
+(* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive
+ simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans
+ Idea: ?ex. move .. should be generally replaced by a step via a subst tac if desired,
+ as this can be done globally *)
+
+Goal
+ "is_simulation sim_relation impl_ioa spec_ioa";
+by (simp_tac (simpset() addsimps [is_simulation_def]) 1);
+by (rtac conjI 1);
+(* -------------- start states ----------------- *)
+by (SELECT_GOAL (safe_tac set_cs) 1);
+by (res_inst_tac [("x","({},False)")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps [sim_relation_def,starts_of_def,
+ Spec.ioa_def,Impl.ioa_def]) 1);
+(* ---------------- main-part ------------------- *)
+
+by (REPEAT (rtac allI 1));
+br imp_conj_lemma 1;
+ren "k b used c k' b' a" 1;
+by (induct_tac "a" 1);
+by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def,
+ Impl.ioa_def,Impl.trans_def,trans_of_def])));
+by (safe_tac set_cs);
+(* NEW *)
+by (res_inst_tac [("x","(used,True)")] exI 1);
+by (Asm_full_simp_tac 1);
+br transition_is_ex 1;
+by (simp_tac (simpset() addsimps [
+ Spec.ioa_def,Spec.trans_def,trans_of_def])1);
+(* LOC *)
+by (res_inst_tac [("x","(used Un {k},False)")] exI 1);
+by (Asm_full_simp_tac 1);
+br transition_is_ex 1;
+by (simp_tac (simpset() addsimps [
+ Spec.ioa_def,Spec.trans_def,trans_of_def])1);
+by (Fast_tac 1);
+(* FREE *)
+by (res_inst_tac [("x","(used - {nat},c)")] exI 1);
+by (Asm_full_simp_tac 1);
+by (SELECT_GOAL (safe_tac set_cs) 1);
+auto();
+br transition_is_ex 1;
+by (simp_tac (simpset() addsimps [
+ Spec.ioa_def,Spec.trans_def,trans_of_def])1);
+qed"issimulation";
+
+
+
+Goalw [ioa_implements_def]
+"impl_ioa =<| spec_ioa";
+br conjI 1;
+by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
+ Impl.ioa_def,Spec.ioa_def, asig_outputs_def,asig_of_def,
+ asig_inputs_def]) 1);
+br trace_inclusion_for_simulations 1;
+by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
+ Impl.ioa_def,Spec.ioa_def, externals_def,asig_outputs_def,asig_of_def,
+ asig_inputs_def]) 1);
+br issimulation 1;
+qed"implementation";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Storage/Correctness.thy Wed Dec 02 15:55:39 1998 +0100
@@ -0,0 +1,26 @@
+(* Title: HOL/IOA/example/Correctness.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1997 TU Muenchen
+
+Correctness Proof
+*)
+
+Correctness = SimCorrectness + Spec + Impl +
+
+default term
+
+consts
+
+sim_relation :: "((nat * bool) * (nat set * bool)) set"
+
+defs
+
+sim_relation_def
+ "sim_relation == {qua. let c = fst qua; a = snd qua ;
+ k = fst c; b = snd c;
+ used = fst a; c = snd a
+ in
+ (! l:used. l < k) & b=c }"
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Storage/Impl.ML Wed Dec 02 15:55:39 1998 +0100
@@ -0,0 +1,16 @@
+(* Title: HOL/IOA/example/Sender.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1997 TU Muenchen
+
+Impl
+*)
+
+Goal
+ "New : actions(impl_sig) & \
+\ Loc l : actions(impl_sig) & \
+\ Free l : actions(impl_sig) ";
+by(simp_tac (simpset() addsimps
+ (Impl.sig_def :: actions_def ::
+ asig_projections)) 1);
+qed "in_impl_asig";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Storage/Impl.thy Wed Dec 02 15:55:39 1998 +0100
@@ -0,0 +1,36 @@
+(* Title: HOL/IOA/example/Spec.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1997 TU Muenchen
+
+The implementation of a memory
+*)
+
+Impl = IOA + Action +
+
+
+consts
+
+impl_sig :: "action signature"
+impl_trans :: "(action, nat * bool)transition set"
+impl_ioa :: "(action, nat * bool)ioa"
+
+defs
+
+sig_def "impl_sig == (UN l.{Free l} Un {New},
+ UN l.{Loc l},
+ {})"
+
+trans_def "impl_trans ==
+ {tr. let s = fst(tr); k = fst s; b = snd s;
+ t = snd(snd(tr)); k' = fst t; b' = snd t
+ in
+ case fst(snd(tr))
+ of
+ New => k' = k & b' |
+ Loc l => b & l= k & k'= (Suc k) & ~b' |
+ Free l => k'=k & b'=b}"
+
+ioa_def "impl_ioa == (impl_sig, {(0,False)}, impl_trans,{},{})"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Storage/Spec.thy Wed Dec 02 15:55:39 1998 +0100
@@ -0,0 +1,36 @@
+(* Title: HOL/IOA/example/Spec.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1997 TU Muenchen
+
+The specification of a memory
+*)
+
+Spec = IOA + Action +
+
+
+consts
+
+spec_sig :: "action signature"
+spec_trans :: "(action, nat set * bool)transition set"
+spec_ioa :: "(action, nat set * bool)ioa"
+
+defs
+
+sig_def "spec_sig == (UN l.{Free l} Un {New},
+ UN l.{Loc l},
+ {})"
+
+trans_def "spec_trans ==
+ {tr. let s = fst(tr); used = fst s; c = snd s;
+ t = snd(snd(tr)); used' = fst t; c' = snd t
+ in
+ case fst(snd(tr))
+ of
+ New => used' = used & c' |
+ Loc l => c & l~:used & used'= used Un {l} & ~c' |
+ Free l => used'=used - {l} & c'=c}"
+
+ioa_def "spec_ioa == (spec_sig, {({},False)}, spec_trans,{},{})"
+
+end