# HG changeset patch
# User wenzelm
# Date 1126119630 -7200
# Node ID 1322ed8e0ee4d79c45fb0d399fc5cc6d92e358f8
# Parent  c43ed29bd197aad1ade8446caa6a8f8bd3040620
converted to Isar theory format;

diff -r c43ed29bd197 -r 1322ed8e0ee4 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Wed Sep 07 20:22:39 2005 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Wed Sep 07 21:00:30 2005 +0200
@@ -6,14 +6,16 @@
 Specification of Chandy and Charpentier's Allocator
 *)
 
-Alloc = AllocBase + PPROD +
+theory Alloc
+imports AllocBase PPROD
+begin
 
 (** State definitions.  OUTPUT variables are locals **)
 
 record clientState =
-  giv :: nat list   (*client's INPUT history:  tokens GRANTED*)
-  ask :: nat list   (*client's OUTPUT history: tokens REQUESTED*)
-  rel :: nat list   (*client's OUTPUT history: tokens RELEASED*)
+  giv :: "nat list"   (*client's INPUT history:  tokens GRANTED*)
+  ask :: "nat list"   (*client's OUTPUT history: tokens REQUESTED*)
+  rel :: "nat list"   (*client's OUTPUT history: tokens RELEASED*)
 
 record 'a clientState_d =
   clientState +
@@ -22,7 +24,7 @@
 constdefs
   (*DUPLICATED FROM Client.thy, but with "tok" removed*)
   (*Maybe want a special theory section to declare such maps*)
-  non_dummy :: 'a clientState_d => clientState
+  non_dummy :: "'a clientState_d => clientState"
     "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)"
 
   (*Renaming map to put a Client into the standard form*)
@@ -31,9 +33,9 @@
 
   
 record allocState =
-  allocGiv :: nat => nat list   (*OUTPUT history: source of "giv" for i*)
-  allocAsk :: nat => nat list   (*INPUT: allocator's copy of "ask" for i*)
-  allocRel :: nat => nat list   (*INPUT: allocator's copy of "rel" for i*)
+  allocGiv :: "nat => nat list"   (*OUTPUT history: source of "giv" for i*)
+  allocAsk :: "nat => nat list"   (*INPUT: allocator's copy of "ask" for i*)
+  allocRel :: "nat => nat list"   (*INPUT: allocator's copy of "rel" for i*)
 
 record 'a allocState_d =
   allocState +
@@ -41,8 +43,8 @@
 
 record 'a systemState =
   allocState +
-  client :: nat => clientState  (*states of all clients*)
-  dummy  :: 'a                  (*dummy field for new variables*)
+  client :: "nat => clientState"  (*states of all clients*)
+  dummy  :: 'a                    (*dummy field for new variables*)
 
 
 constdefs
@@ -50,64 +52,64 @@
 (** Resource allocation system specification **)
 
   (*spec (1)*)
-  system_safety :: 'a systemState program set
+  system_safety :: "'a systemState program set"
     "system_safety ==
      Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s)
      <= NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
 
   (*spec (2)*)
-  system_progress :: 'a systemState program set
+  system_progress :: "'a systemState program set"
     "system_progress == INT i : lessThan Nclients.
 			INT h. 
 			  {s. h <= (ask o sub i o client)s} LeadsTo
 			  {s. h pfixLe (giv o sub i o client) s}"
 
-  system_spec :: 'a systemState program set
+  system_spec :: "'a systemState program set"
     "system_spec == system_safety Int system_progress"
 
 (** Client specification (required) ***)
 
   (*spec (3)*)
-  client_increasing :: 'a clientState_d program set
+  client_increasing :: "'a clientState_d program set"
     "client_increasing ==
          UNIV guarantees  Increasing ask Int Increasing rel"
 
   (*spec (4)*)
-  client_bounded :: 'a clientState_d program set
+  client_bounded :: "'a clientState_d program set"
     "client_bounded ==
          UNIV guarantees  Always {s. ALL elt : set (ask s). elt <= NbT}"
 
   (*spec (5)*)
-  client_progress :: 'a clientState_d program set
+  client_progress :: "'a clientState_d program set"
     "client_progress ==
 	 Increasing giv  guarantees
 	 (INT h. {s. h <= giv s & h pfixGe ask s}
 		 LeadsTo {s. tokens h <= (tokens o rel) s})"
 
   (*spec: preserves part*)
-  client_preserves :: 'a clientState_d program set
+  client_preserves :: "'a clientState_d program set"
     "client_preserves == preserves giv Int preserves clientState_d.dummy"
 
   (*environmental constraints*)
-  client_allowed_acts :: 'a clientState_d program set
+  client_allowed_acts :: "'a clientState_d program set"
     "client_allowed_acts ==
        {F. AllowedActs F =
 	    insert Id (UNION (preserves (funPair rel ask)) Acts)}"
 
-  client_spec :: 'a clientState_d program set
+  client_spec :: "'a clientState_d program set"
     "client_spec == client_increasing Int client_bounded Int client_progress
                     Int client_allowed_acts Int client_preserves"
 
 (** Allocator specification (required) ***)
 
   (*spec (6)*)
-  alloc_increasing :: 'a allocState_d program set
+  alloc_increasing :: "'a allocState_d program set"
     "alloc_increasing ==
 	 UNIV  guarantees
 	 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
 
   (*spec (7)*)
-  alloc_safety :: 'a allocState_d program set
+  alloc_safety :: "'a allocState_d program set"
     "alloc_safety ==
 	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
          guarantees
@@ -115,7 +117,7 @@
          <= NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
 
   (*spec (8)*)
-  alloc_progress :: 'a allocState_d program set
+  alloc_progress :: "'a allocState_d program set"
     "alloc_progress ==
 	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
 	                             Increasing (sub i o allocRel))
@@ -141,51 +143,51 @@
     looked at.*)
 
   (*spec: preserves part*)
-  alloc_preserves :: 'a allocState_d program set
+  alloc_preserves :: "'a allocState_d program set"
     "alloc_preserves == preserves allocRel Int preserves allocAsk Int
                         preserves allocState_d.dummy"
   
   (*environmental constraints*)
-  alloc_allowed_acts :: 'a allocState_d program set
+  alloc_allowed_acts :: "'a allocState_d program set"
     "alloc_allowed_acts ==
        {F. AllowedActs F =
 	    insert Id (UNION (preserves allocGiv) Acts)}"
 
-  alloc_spec :: 'a allocState_d program set
+  alloc_spec :: "'a allocState_d program set"
     "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
                    alloc_allowed_acts Int alloc_preserves"
 
 (** Network specification ***)
 
   (*spec (9.1)*)
-  network_ask :: 'a systemState program set
+  network_ask :: "'a systemState program set"
     "network_ask == INT i : lessThan Nclients.
 			Increasing (ask o sub i o client)  guarantees
 			((sub i o allocAsk) Fols (ask o sub i o client))"
 
   (*spec (9.2)*)
-  network_giv :: 'a systemState program set
+  network_giv :: "'a systemState program set"
     "network_giv == INT i : lessThan Nclients.
 			Increasing (sub i o allocGiv)
 			guarantees
 			((giv o sub i o client) Fols (sub i o allocGiv))"
 
   (*spec (9.3)*)
-  network_rel :: 'a systemState program set
+  network_rel :: "'a systemState program set"
     "network_rel == INT i : lessThan Nclients.
 			Increasing (rel o sub i o client)
 			guarantees
 			((sub i o allocRel) Fols (rel o sub i o client))"
 
   (*spec: preserves part*)
-  network_preserves :: 'a systemState program set
+  network_preserves :: "'a systemState program set"
     "network_preserves ==
        preserves allocGiv  Int
        (INT i : lessThan Nclients. preserves (rel o sub i o client)  Int
                                    preserves (ask o sub i o client))"
   
   (*environmental constraints*)
-  network_allowed_acts :: 'a systemState program set
+  network_allowed_acts :: "'a systemState program set"
     "network_allowed_acts ==
        {F. AllowedActs F =
            insert Id
@@ -193,7 +195,7 @@
 		    (INT i: lessThan Nclients. preserves(giv o sub i o client)))
 		  Acts)}"
 
-  network_spec :: 'a systemState program set
+  network_spec :: "'a systemState program set"
     "network_spec == network_ask Int network_giv Int
                      network_rel Int network_allowed_acts Int
                      network_preserves"
@@ -217,18 +219,18 @@
 			         systemState.dummy = allocState_d.dummy al|)"
 
 consts 
-    Alloc   :: 'a allocState_d program
-    Client  :: 'a clientState_d program
-    Network :: 'a systemState program
-    System  :: 'a systemState program
+    Alloc   :: "'a allocState_d program"
+    Client  :: "'a clientState_d program"
+    Network :: "'a systemState program"
+    System  :: "'a systemState program"
   
-rules
-    Alloc   "Alloc   : alloc_spec"
-    Client  "Client  : client_spec"
-    Network "Network : network_spec"
+axioms
+    Alloc:   "Alloc   : alloc_spec"
+    Client:  "Client  : client_spec"
+    Network: "Network : network_spec"
 
 defs
-    System_def
+    System_def:
       "System == rename sysOfAlloc Alloc Join Network Join
                  (rename sysOfClient
 		  (plam x: lessThan Nclients. rename client_map Client))"
@@ -257,5 +259,6 @@
 		  (plam x: lessThan Nclients. rename client_map Client))"
 **)
 
+ML {* use_legacy_bindings (the_context ()) *}
 
 end