
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/AllocImpl.thy
--- a/src/HOL/UNITY/AllocImpl.thy	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/AllocImpl.thy	Fri Jul 21 18:01:36 2000 +0200
@@ -4,9 +4,6 @@
     Copyright   1998  University of Cambridge
 
 Implementation of a multiple-client allocator from a single-client allocator
-
-add_path "../Induct";
-with_path "../Induct" time_use_thy "AllocImpl";
 *)
 
 AllocImpl = AllocBase + Follows + PPROD + 
@@ -20,38 +17,38 @@
   Out  :: 'b list          (*merge's OUTPUT history: merged items*)
   iOut :: nat list         (*merge's OUTPUT history: origins of merged items*)
 
-record ('a,'b) merge_u =
+record ('a,'b) merge_d =
   'b merge +
-  extra :: 'a       (*dummy field for new variables*)
+  dummy :: 'a       (*dummy field for new variables*)
 
 constdefs
-  non_extra :: ('a,'b) merge_u => 'b merge
-    "non_extra s == (|In = In s, Out = Out s, iOut = iOut s|)"
+  non_dummy :: ('a,'b) merge_d => 'b merge
+    "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
 
 record 'b distr =
   In  :: 'b list          (*items to distribute*)
   iIn :: nat list         (*destinations of items to distribute*)
   Out :: nat => 'b list   (*distributed items*)
 
-record ('a,'b) distr_u =
+record ('a,'b) distr_d =
   'b distr +
-  extra :: 'a       (*dummy field for new variables*)
+  dummy :: 'a       (*dummy field for new variables*)
 
 record allocState =
   giv :: nat list   (*OUTPUT history: source of tokens*)
   ask :: nat list   (*INPUT: tokens requested from allocator*)
   rel :: nat list   (*INPUT: tokens released to allocator*)
 
-record 'a allocState_u =
+record 'a allocState_d =
   allocState +
-  extra    :: 'a                (*dummy field for new variables*)
+  dummy    :: 'a                (*dummy field for new variables*)
 
 record 'a systemState =
   allocState +
   mergeRel :: nat merge
   mergeAsk :: nat merge
   distr    :: nat distr
-  extra    :: 'a                  (*dummy field for new variables*)
+  dummy    :: 'a                  (*dummy field for new variables*)
 
 
 constdefs
@@ -59,25 +56,25 @@
 (** Merge specification (the number of inputs is Nclients) ***)
 
   (*spec (10)*)
-  merge_increasing :: ('a,'b) merge_u program set
+  merge_increasing :: ('a,'b) merge_d program set
     "merge_increasing ==
          UNIV guarantees[funPair merge.Out merge.iOut]
          (Increasing merge.Out) Int (Increasing merge.iOut)"
 
   (*spec (11)*)
-  merge_eqOut :: ('a,'b) merge_u program set
+  merge_eqOut :: ('a,'b) merge_d program set
     "merge_eqOut ==
          UNIV guarantees[funPair merge.Out merge.iOut]
          Always {s. length (merge.Out s) = length (merge.iOut s)}"
 
   (*spec (12)*)
-  merge_bounded :: ('a,'b) merge_u program set
+  merge_bounded :: ('a,'b) merge_d program set
     "merge_bounded ==
          UNIV guarantees[merge.iOut]
          Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
 
   (*spec (13)*)
-  merge_follows :: ('a,'b) merge_u program set
+  merge_follows :: ('a,'b) merge_d program set
     "merge_follows ==
 	 (INT i : lessThan Nclients. Increasing (sub i o merge.In))
 	 guarantees[funPair merge.Out merge.iOut]
@@ -87,17 +84,17 @@
 	  Fols (sub i o merge.In))"
 
   (*spec: preserves part*)
-    merge_preserves :: ('a,'b) merge_u program set
-    "merge_preserves == preserves (funPair merge.In merge_u.extra)"
+    merge_preserves :: ('a,'b) merge_d program set
+    "merge_preserves == preserves (funPair merge.In merge_d.dummy)"
 
-  merge_spec :: ('a,'b) merge_u program set
+  merge_spec :: ('a,'b) merge_d program set
     "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
                    merge_follows Int merge_preserves"
 
 (** Distributor specification (the number of outputs is Nclients) ***)
 
   (*spec (14)*)
-  distr_follows :: ('a,'b) distr_u program set
+  distr_follows :: ('a,'b) distr_d program set
     "distr_follows ==
 	 Increasing distr.In Int Increasing distr.iIn Int
 	 Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
@@ -111,17 +108,17 @@
 (** Single-client allocator specification (required) ***)
 
   (*spec (18)*)
-  alloc_increasing :: 'a allocState_u program set
+  alloc_increasing :: 'a allocState_d program set
     "alloc_increasing == UNIV guarantees[giv] Increasing giv"
 
   (*spec (19)*)
-  alloc_safety :: 'a allocState_u program set
+  alloc_safety :: 'a allocState_d program set
     "alloc_safety ==
 	 Increasing rel
          guarantees[giv] Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
 
   (*spec (20)*)
-  alloc_progress :: 'a allocState_u program set
+  alloc_progress :: 'a allocState_d program set
     "alloc_progress ==
 	 Increasing ask Int Increasing rel Int
          Always {s. ALL elt : set (ask s). elt <= NbT}
@@ -133,11 +130,11 @@
 	     (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
 
   (*spec: preserves part*)
-    alloc_preserves :: 'a allocState_u program set
+    alloc_preserves :: 'a allocState_d program set
     "alloc_preserves == preserves (funPair rel
-				   (funPair ask allocState_u.extra))"
+				   (funPair ask allocState_d.dummy))"
   
-  alloc_spec :: 'a allocState_u program set
+  alloc_spec :: 'a allocState_d program set
     "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
                    alloc_preserves"
 
@@ -177,26 +174,27 @@
 
 
     (** State mappings **)
-      sysOfAlloc :: "((nat => merge) * 'a) allocState_u => 'a systemState"
-	"sysOfAlloc == %s. let (cl,xtr) = allocState_u.extra s
+      sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
+	"sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
 			   in (| giv = giv s,
 				 ask = ask s,
 				 rel = rel s,
 				 client   = cl,
-				 extra    = xtr|)"
+				 dummy    = xtr|)"
 
 
-      sysOfClient :: "(nat => merge) * 'a allocState_u => 'a systemState"
+      sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
 	"sysOfClient == %(cl,al). (| giv = giv al,
 				     ask = ask al,
 				     rel = rel al,
 				     client   = cl,
-				     systemState.extra = allocState_u.extra al|)"
+				     systemState.dummy = allocState_d.dummy al|)"
 ****)
 
 consts 
-    Alloc  :: 'a allocState_u program
-    Merge  :: ('a,'b) merge_u program
+    Alloc  :: 'a allocState_d program
+    Merge  :: ('a,'b) merge_d program
+
 (*    
     Network :: 'a systemState program
     System  :: 'a systemState program
@@ -205,17 +203,9 @@
 rules
     Alloc   "Alloc   : alloc_spec"
     Merge  "Merge  : merge_spec"
+
 (**    Network "Network : network_spec"**)
 
 
 
-(**
-defs
-    System_def
-      "System == rename sysOfAlloc Alloc Join Network Join
-                 (rename sysOfMerge
-		  (plam x: lessThan Nclients. rename merge_map Merge))"
-**)
-
-
 end




