src/HOL/UNITY/Alloc.ML
changeset 7538 357873391561
parent 7537 875754b599df
child 7540 8af61a565a4a
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Fri Sep 10 18:40:06 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Fri Sep 17 10:31:38 1999 +0200
     1.3 @@ -17,6 +17,14 @@
     1.4  
     1.5  
     1.6  
     1.7 +Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
     1.8 +by (induct_tac "n" 1);
     1.9 +by Auto_tac;
    1.10 +by (dres_inst_tac [("x","n")] bspec 1);
    1.11 +by Auto_tac;
    1.12 +by (arith_tac 1);
    1.13 +qed_spec_mp "sum_mono";
    1.14 +
    1.15  
    1.16  (*Generalized version allowing different clients*)
    1.17  Goal "[| Alloc : alloc_spec;  \
    1.18 @@ -59,6 +67,7 @@
    1.19  	      simpset() addsimps [sysOfAlloc_def]));
    1.20  qed "inv_sysOfAlloc_eq";
    1.21  
    1.22 +Addsimps [inv_sysOfAlloc_eq];
    1.23  
    1.24  (**SHOULD NOT BE NECESSARY: The various injections into the system
    1.25     state need to be treated symmetrically or done automatically*)
    1.26 @@ -202,15 +211,13 @@
    1.27  qed "System_Increasing_allocRel";
    1.28  
    1.29  
    1.30 -(*NEED TO PROVE something like this (maybe without premise)*)
    1.31 -Goal "i < Nclients ==> System : (sub i o allocRel) localTo Network";
    1.32 -
    1.33  fun alloc_export th = good_map_sysOfAlloc RS export th;
    1.34  
    1.35  val extend_Alloc_guar_Increasing =
    1.36    alloc_export extend_guar_Increasing
    1.37 -  |> simplify (simpset() addsimps [inv_sysOfAlloc_eq]);
    1.38 +  |> simplify (simpset());
    1.39  
    1.40 +(*step 2*)
    1.41  Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
    1.42  \                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
    1.43  by (res_inst_tac 
    1.44 @@ -218,72 +225,30 @@
    1.45      component_guaranteesD 1);
    1.46  by (rtac Alloc_component_System 3);
    1.47  by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
    1.48 -by (rtac project_guarantees 1);
    1.49 -by (rtac Alloc_Safety 1);
    1.50 +by (rtac (Alloc_Safety RS project_guarantees) 1);
    1.51  by Auto_tac;
    1.52 -by (rtac project_Increasing_I 1);
    1.53 +(*1: Increasing precondition*)
    1.54 +by (stac (alloc_export project_Increasing) 1);
    1.55 +by (force_tac
    1.56 +    (claset(),
    1.57 +     simpset() addsimps [o_def, alloc_export project_Increasing]) 1);
    1.58 +(*2: Always postcondition*)
    1.59 +by (dtac (subset_refl RS alloc_export project_Always_D) 1);
    1.60 +by (asm_full_simp_tac
    1.61 +     (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
    1.62 +qed "System_sum_bounded";
    1.63  
    1.64 -by (dtac (alloc_export (project_extend_Join RSN (2, subst_elem RS project_Always_D))) 2 
    1.65 -     THEN
    1.66 -     full_simp_tac
    1.67 -     (simpset() addsimps [inv_sysOfAlloc_eq,
    1.68 -			  alloc_export Collect_eq_extend_set RS sym]) 2);
    1.69 +(*step 3*)
    1.70 +Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients \
    1.71 +\                  <= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}";
    1.72 +by (rtac (System_sum_bounded RS Always_weaken) 1);
    1.73 +by Auto_tac;
    1.74 +br order_trans 1;
    1.75 +br sum_mono 1;
    1.76 +bd order_trans 2;
    1.77 +br add_le_mono 2;
    1.78 +br order_refl 2;
    1.79 +br sum_mono 2;
    1.80 +ba 3;
    1.81  by Auto_tac;
    1.82  
    1.83 -by (dtac bspec 1);
    1.84 -by (Blast_tac 1);
    1.85 -
    1.86 -
    1.87 -xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
    1.88 -FIRST STEP WAS
    1.89 -by (res_inst_tac 
    1.90 -    [("X", "(INT i : lessThan Nclients. (sub i o allocRel) localTo Network \
    1.91 -\                                       Int Increasing (sub i o allocRel))")] 
    1.92 -    component_guaranteesD 1);
    1.93 -
    1.94 -
    1.95 -       [| i < Nclients;
    1.96 -          extend sysOfAlloc Alloc Join G
    1.97 -          : (sub i o allocRel) localTo Network &
    1.98 -          extend sysOfAlloc Alloc Join G : Increasing (sub i o allocRel) |]
    1.99 -       ==> Alloc Join project sysOfAlloc G : Increasing (sub i o allocRel)
   1.100 -
   1.101 -
   1.102 -       [| i < Nclients;
   1.103 -          H : (sub i o allocRel) localTo Network &
   1.104 -          H : Increasing (sub i o allocRel) |]
   1.105 -       ==> project sysOfAlloc H : Increasing (sub i o allocRel)
   1.106 -
   1.107 -Open_locale"Extend";
   1.108 -
   1.109 -Goal "(H : (func o f) localTo G) ==> (project h H : func localTo (project h G))";
   1.110 -by (asm_full_simp_tac 
   1.111 -    (simpset() addsimps [localTo_def, 
   1.112 -			 project_extend_Join RS sym,
   1.113 -			 Diff_project_stable,
   1.114 -			 Collect_eq_extend_set RS sym]) 1);
   1.115 -by Auto_tac;
   1.116 -by (rtac Diff_project_stable 1);
   1.117 -PROBABLY FALSE;
   1.118 -
   1.119 -by (Clarify_tac 1);
   1.120 -by (dres_inst_tac [("x","z")] spec 1);
   1.121 -
   1.122 -by (rtac (alloc_export project_Always_D) 2);
   1.123 -
   1.124 -by (rtac (alloc_export extend_Always RS iffD2) 2);
   1.125 -
   1.126 -xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
   1.127 -
   1.128 -by (rtac guaranteesI 1);
   1.129 -
   1.130 -by (res_inst_tac 
   1.131 -    [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] 
   1.132 -    component_guaranteesD 1);;
   1.133 -
   1.134 -
   1.135 -by (rtac (Alloc_Safety RS component_guaranteesD) 1);
   1.136 -
   1.137 -
   1.138 -by (rtac (alloc_export guarantees_imp_extend_guarantees RS guarantees_weaken) 1);
   1.139 -by (rtac Alloc_Safety 1);