# HG changeset patch # User mueller # Date 912610539 -3600 # Node ID d0e9b161946894101e08b005b550be6ae2cff9be # Parent 91070f559b4d7a596cec0684fe0eb5df0096980b Memory storage case study from PhD p.240; diff -r 91070f559b4d -r d0e9b1619468 src/HOLCF/IOA/Storage/Action.ML --- /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()]; diff -r 91070f559b4d -r d0e9b1619468 src/HOLCF/IOA/Storage/Action.thy --- /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 diff -r 91070f559b4d -r d0e9b1619468 src/HOLCF/IOA/Storage/Correctness.ML --- /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"; + diff -r 91070f559b4d -r d0e9b1619468 src/HOLCF/IOA/Storage/Correctness.thy --- /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 diff -r 91070f559b4d -r d0e9b1619468 src/HOLCF/IOA/Storage/Impl.ML --- /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"; diff -r 91070f559b4d -r d0e9b1619468 src/HOLCF/IOA/Storage/Impl.thy --- /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 diff -r 91070f559b4d -r d0e9b1619468 src/HOLCF/IOA/Storage/Spec.thy --- /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