# 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