Memory storage case study from PhD p.240;
authormueller
Wed Dec 02 15:55:39 1998 +0100 (1998-12-02)
changeset 6008d0e9b1619468
parent 6007 91070f559b4d
child 6009 bfc06f358d70
Memory storage case study from PhD p.240;
src/HOLCF/IOA/Storage/Action.ML
src/HOLCF/IOA/Storage/Action.thy
src/HOLCF/IOA/Storage/Correctness.ML
src/HOLCF/IOA/Storage/Correctness.thy
src/HOLCF/IOA/Storage/Impl.ML
src/HOLCF/IOA/Storage/Impl.thy
src/HOLCF/IOA/Storage/Spec.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/Storage/Action.ML	Wed Dec 02 15:55:39 1998 +0100
     1.3 @@ -0,0 +1,13 @@
     1.4 +(*  Title:      HOLCF/IOA/ABP/Action.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Olaf Mueller
     1.7 +    Copyright   1997  TU Muenchen
     1.8 +
     1.9 +Derived rules for actions
    1.10 +*)
    1.11 +
    1.12 +Goal "!!x. x = y ==> action_case a b c x =     \
    1.13 +\                        action_case a b c y";
    1.14 +by (Asm_simp_tac 1);
    1.15 +
    1.16 +Addcongs [result()];
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOLCF/IOA/Storage/Action.thy	Wed Dec 02 15:55:39 1998 +0100
     2.3 @@ -0,0 +1,11 @@
     2.4 +(*  Title:      HOLCF/IOA/ABP/Action.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Olaf Mueller
     2.7 +    Copyright   1997  TU Muenchen
     2.8 +
     2.9 +The set of all actions of the system
    2.10 +*)
    2.11 +
    2.12 +Action =  Main +
    2.13 +datatype action = New  | Loc nat | Free nat        
    2.14 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOLCF/IOA/Storage/Correctness.ML	Wed Dec 02 15:55:39 1998 +0100
     3.3 @@ -0,0 +1,74 @@
     3.4 +(*  Title:      HOL/IOA/example/Correctness.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Olaf Mueller
     3.7 +    Copyright   1997  TU Muenchen
     3.8 +
     3.9 +Correctness Proof
    3.10 +*)
    3.11 +
    3.12 +
    3.13 +Addsimps [split_paired_All];
    3.14 +Delsimps [split_paired_Ex];
    3.15 +
    3.16 +
    3.17 +(* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive
    3.18 +         simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans 
    3.19 +   Idea: ?ex. move .. should be generally replaced by a step via a subst tac if desired,
    3.20 +         as this can be done globally *)
    3.21 +
    3.22 +Goal 
    3.23 +      "is_simulation sim_relation impl_ioa spec_ioa";
    3.24 +by (simp_tac (simpset() addsimps [is_simulation_def]) 1);
    3.25 +by (rtac conjI 1);
    3.26 +(* --------------  start states ----------------- *)
    3.27 +by (SELECT_GOAL (safe_tac set_cs) 1);
    3.28 +by (res_inst_tac [("x","({},False)")] exI 1);
    3.29 +by (asm_full_simp_tac (simpset() addsimps [sim_relation_def,starts_of_def,
    3.30 +        Spec.ioa_def,Impl.ioa_def]) 1);
    3.31 +(* ---------------- main-part ------------------- *)
    3.32 +
    3.33 +by (REPEAT (rtac allI 1));
    3.34 +br imp_conj_lemma 1;
    3.35 +ren "k b used c k' b' a" 1;
    3.36 +by (induct_tac "a" 1);
    3.37 +by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def,
    3.38 +      Impl.ioa_def,Impl.trans_def,trans_of_def])));
    3.39 +by (safe_tac set_cs);
    3.40 +(* NEW *)
    3.41 +by (res_inst_tac [("x","(used,True)")] exI 1);
    3.42 +by (Asm_full_simp_tac 1);
    3.43 +br transition_is_ex 1;
    3.44 +by (simp_tac (simpset() addsimps [
    3.45 +      Spec.ioa_def,Spec.trans_def,trans_of_def])1);
    3.46 +(* LOC *)
    3.47 +by (res_inst_tac [("x","(used Un {k},False)")] exI 1);
    3.48 +by (Asm_full_simp_tac 1);
    3.49 +br transition_is_ex 1;
    3.50 +by (simp_tac (simpset() addsimps [
    3.51 +      Spec.ioa_def,Spec.trans_def,trans_of_def])1);
    3.52 +by (Fast_tac 1);
    3.53 +(* FREE *)
    3.54 +by (res_inst_tac [("x","(used - {nat},c)")] exI 1);
    3.55 +by (Asm_full_simp_tac 1);
    3.56 +by (SELECT_GOAL (safe_tac set_cs) 1);
    3.57 +auto();
    3.58 +br transition_is_ex 1;
    3.59 +by (simp_tac (simpset() addsimps [
    3.60 +      Spec.ioa_def,Spec.trans_def,trans_of_def])1);
    3.61 +qed"issimulation";
    3.62 +
    3.63 +
    3.64 +
    3.65 +Goalw [ioa_implements_def] 
    3.66 +"impl_ioa =<| spec_ioa";
    3.67 +br conjI 1;
    3.68 +by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
    3.69 +    Impl.ioa_def,Spec.ioa_def, asig_outputs_def,asig_of_def,
    3.70 +    asig_inputs_def]) 1);
    3.71 +br trace_inclusion_for_simulations 1;
    3.72 +by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
    3.73 +    Impl.ioa_def,Spec.ioa_def, externals_def,asig_outputs_def,asig_of_def,
    3.74 +    asig_inputs_def]) 1);
    3.75 +br issimulation 1;
    3.76 +qed"implementation";
    3.77 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOLCF/IOA/Storage/Correctness.thy	Wed Dec 02 15:55:39 1998 +0100
     4.3 @@ -0,0 +1,26 @@
     4.4 +(*  Title:      HOL/IOA/example/Correctness.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Olaf Mueller
     4.7 +    Copyright   1997  TU Muenchen
     4.8 +
     4.9 +Correctness Proof
    4.10 +*)
    4.11 +
    4.12 +Correctness = SimCorrectness + Spec + Impl + 
    4.13 +
    4.14 +default term
    4.15 +
    4.16 +consts
    4.17 +
    4.18 +sim_relation   :: "((nat * bool) * (nat set * bool)) set"
    4.19 +
    4.20 +defs
    4.21 +  
    4.22 +sim_relation_def
    4.23 +  "sim_relation == {qua. let c = fst qua; a = snd qua ; 
    4.24 +                             k = fst c;   b = snd c;
    4.25 +                             used = fst a; c = snd a
    4.26 +                         in
    4.27 +                         (! l:used. l < k) & b=c }"
    4.28 +
    4.29 +end
    4.30 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOLCF/IOA/Storage/Impl.ML	Wed Dec 02 15:55:39 1998 +0100
     5.3 @@ -0,0 +1,16 @@
     5.4 +(*  Title:      HOL/IOA/example/Sender.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Olaf Mueller
     5.7 +    Copyright   1997  TU Muenchen
     5.8 +
     5.9 +Impl
    5.10 +*)
    5.11 + 
    5.12 +Goal 
    5.13 + "New : actions(impl_sig)       &   \
    5.14 +\ Loc l : actions(impl_sig)       &   \
    5.15 +\ Free l : actions(impl_sig) ";
    5.16 +by(simp_tac (simpset() addsimps 
    5.17 +             (Impl.sig_def :: actions_def :: 
    5.18 +              asig_projections)) 1);
    5.19 +qed "in_impl_asig";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOLCF/IOA/Storage/Impl.thy	Wed Dec 02 15:55:39 1998 +0100
     6.3 @@ -0,0 +1,36 @@
     6.4 +(*  Title:      HOL/IOA/example/Spec.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Olaf Mueller
     6.7 +    Copyright   1997  TU Muenchen
     6.8 +
     6.9 +The implementation of a memory
    6.10 +*)
    6.11 +
    6.12 +Impl = IOA + Action +
    6.13 +
    6.14 +
    6.15 +consts
    6.16 +
    6.17 +impl_sig   :: "action signature"
    6.18 +impl_trans :: "(action, nat  * bool)transition set"
    6.19 +impl_ioa   :: "(action, nat * bool)ioa"
    6.20 +
    6.21 +defs
    6.22 +
    6.23 +sig_def "impl_sig == (UN l.{Free l} Un {New}, 
    6.24 +                     UN l.{Loc l}, 
    6.25 +                     {})"
    6.26 +
    6.27 +trans_def "impl_trans ==                           
    6.28 + {tr. let s = fst(tr); k = fst s; b = snd s;                            
    6.29 +          t = snd(snd(tr)); k' = fst t; b' = snd t                      
    6.30 +      in                                          
    6.31 +      case fst(snd(tr))                           
    6.32 +      of   
    6.33 +      New       => k' = k & b'  |                    
    6.34 +      Loc l     => b & l= k & k'= (Suc k) & ~b' |                    
    6.35 +      Free l    => k'=k & b'=b}"
    6.36 +
    6.37 +ioa_def "impl_ioa == (impl_sig, {(0,False)}, impl_trans,{},{})"
    6.38 +
    6.39 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOLCF/IOA/Storage/Spec.thy	Wed Dec 02 15:55:39 1998 +0100
     7.3 @@ -0,0 +1,36 @@
     7.4 +(*  Title:      HOL/IOA/example/Spec.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Olaf Mueller
     7.7 +    Copyright   1997  TU Muenchen
     7.8 +
     7.9 +The specification of a memory
    7.10 +*)
    7.11 +
    7.12 +Spec = IOA + Action +
    7.13 +
    7.14 +
    7.15 +consts
    7.16 +
    7.17 +spec_sig   :: "action signature"
    7.18 +spec_trans :: "(action, nat set * bool)transition set"
    7.19 +spec_ioa   :: "(action, nat set * bool)ioa"
    7.20 +
    7.21 +defs
    7.22 +
    7.23 +sig_def "spec_sig == (UN l.{Free l} Un {New}, 
    7.24 +                     UN l.{Loc l}, 
    7.25 +                     {})"
    7.26 +
    7.27 +trans_def "spec_trans ==                           
    7.28 + {tr. let s = fst(tr); used = fst s; c = snd s;                            
    7.29 +          t = snd(snd(tr)); used' = fst t; c' = snd t                      
    7.30 +      in                                          
    7.31 +      case fst(snd(tr))                           
    7.32 +      of   
    7.33 +      New       => used' = used & c'  |                    
    7.34 +      Loc l     => c & l~:used  & used'= used Un {l} & ~c'   |                    
    7.35 +      Free l    => used'=used - {l} & c'=c}"
    7.36 +
    7.37 +ioa_def "spec_ioa == (spec_sig, {({},False)}, spec_trans,{},{})"
    7.38 +
    7.39 +end