src/HOL/UNITY/Alloc.ML
changeset 7826 c6a8b73b6c2a
parent 7689 affe0c2fdfbf
child 7841 65d91d13fc13
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Mon Oct 11 10:52:51 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Mon Oct 11 10:53:39 1999 +0200
     1.3 @@ -71,6 +71,16 @@
     1.4  qed "inv_sysOfAlloc_eq";
     1.5  Addsimps [inv_sysOfAlloc_eq];
     1.6  
     1.7 +
     1.8 +(*SHOULD NOT BE NECESSARY????????????????
     1.9 +Goal "!!z. (| allocGiv = allocGiv z, allocAsk = allocAsk z, \
    1.10 +\             allocRel = allocRel z |) = z";
    1.11 +by (auto_tac (claset() addSWrapper record_split_wrapper, 
    1.12 +	      simpset()));
    1.13 +qed "allocState_eq";
    1.14 +Addsimps [allocState_eq];
    1.15 +????*)
    1.16 +
    1.17  (**SHOULD NOT BE NECESSARY: The various injections into the system
    1.18     state need to be treated symmetrically or done automatically*)
    1.19  Goalw [sysOfClient_def] "inj sysOfClient";
    1.20 @@ -183,15 +193,14 @@
    1.21  AddIffs [Network_component_System, Alloc_component_System];
    1.22  
    1.23  
    1.24 -fun alloc_export th = good_map_sysOfAlloc RS export th;
    1.25 +fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset());
    1.26  
    1.27 -fun client_export th = good_map_sysOfClient RS export th;
    1.28 +fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset());
    1.29  
    1.30  (* F : UNIV guarantees Increasing func
    1.31     ==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
    1.32  val extend_Client_guar_Increasing =
    1.33 -  client_export extend_guar_Increasing
    1.34 -  |> simplify (simpset() addsimps [inv_sysOfClient_eq]);
    1.35 +  client_export extend_guar_Increasing;
    1.36  
    1.37  (*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
    1.38  Goal "i < Nclients \
    1.39 @@ -221,6 +230,8 @@
    1.40  			       System_Increasing_rel]) 1);
    1.41  qed "System_Increasing_allocRel";
    1.42  
    1.43 +
    1.44 +
    1.45  (*safety (1), step 3*)
    1.46  Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
    1.47  \                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
    1.48 @@ -230,14 +241,14 @@
    1.49  by (rtac Alloc_component_System 3);
    1.50  by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
    1.51  by (rtac (Alloc_Safety RS project_guarantees) 1);
    1.52 +(*1: Increasing precondition*)
    1.53 +br (ballI RS projecting_INT) 1;
    1.54 +by (rtac (alloc_export projecting_Increasing RS projecting_weaken) 1);
    1.55  by Auto_tac;
    1.56 -(*1: Increasing precondition*)
    1.57 -by (stac (alloc_export project_Increasing) 1);
    1.58 -by (force_tac
    1.59 -    (claset(),
    1.60 -     simpset() addsimps [o_def, alloc_export project_Increasing]) 1);
    1.61 +by (asm_full_simp_tac (simpset() addsimps [o_def]) 1);
    1.62  (*2: Always postcondition*)
    1.63 -by (dtac (subset_refl RS alloc_export project_Always_D) 1);
    1.64 +by (rtac ((alloc_export extending_Always RS extending_weaken)) 1);
    1.65 +by Auto_tac;
    1.66  by (asm_full_simp_tac
    1.67       (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
    1.68  qed "System_sum_bounded";