# HG changeset patch
# User paulson
# Date 935572164 -7200
# Node ID ad0ce67e4eb6231a4cd16cf2924709423cbdd6af
# Parent  dace49c16aca9fc33a0d4f3ac0add864339339f2
another snapshot

diff -r dace49c16aca -r ad0ce67e4eb6 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Wed Aug 25 11:04:28 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Wed Aug 25 11:09:24 1999 +0200
@@ -6,6 +6,20 @@
 Specification of Chandy and Charpentier's Allocator
 *)
 
+		Goal "(%(x,y). f(x,y)) = f";
+		by (rtac ext 1);
+		by (pair_tac "x" 1);
+		by (Simp_tac 1);
+		qed "split_Pair_apply";
+
+		Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
+		by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
+		qed "split_paired_Eps";
+
+		Goal "[| inj(f);  f x = y |] ==> inv f y = x";
+		by (etac subst 1);
+		by (etac inv_f_f 1);
+		qed "inv_f_eq";
 
 (*Generalized version allowing different clients*)
 Goal "[| Alloc : alloc_spec;  \
@@ -18,11 +32,9 @@
 Goal "System : system_spec";
 
 
-
-
 Goalw [sysOfAlloc_def] "inj sysOfAlloc";
 by (rtac injI 1);
-by Auto_tac;
+by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
 qed "inj_sysOfAlloc";
 
 Goalw [sysOfAlloc_def] "surj sysOfAlloc";
@@ -30,11 +42,28 @@
 \                                allocAsk = allocAsk s,    \
 \                                allocRel = allocRel s |), \
 \                             client s)")] surjI 1);
-by Auto_tac;
+by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
 qed "surj_sysOfAlloc";
 
 AddIffs [inj_sysOfAlloc, surj_sysOfAlloc];
 
+(**THESE SHOULD NOT BE NECESSARY...THE VARIOUS INJECTIONS INTO THE SYSTEM
+   STATE NEED TO BE TREATED SYMMETRICALLY OR DONE AUTOMATICALLY*)
+Goalw [sysOfClient_def] "inj sysOfClient";
+by (rtac injI 1);
+by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD]
+		       addSWrapper record_split_wrapper, simpset()));
+qed "inj_sysOfClient";
+
+Goalw [sysOfClient_def] "surj sysOfClient";
+by (cut_facts_tac [surj_sysOfAlloc] 1);
+by (rewtac surj_def);
+by Auto_tac;
+by (Blast_tac 1);
+qed "surj_sysOfClient";
+
+AddIffs [inj_sysOfClient, surj_sysOfClient];
+
 
 Open_locale "System";
 
@@ -46,51 +75,100 @@
 AddIffs [finite_lessThan];
 
 
+Goal "Client : UNIV guar Increasing ask";
+by (cut_facts_tac [Client] 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [client_spec_def, client_increasing_def,
+			 guarantees_Int_right]) 1);
+qed "Client_Increasing_ask";
 
-Goal "i < Nclients ==> \
-\     lift_prog i Client : UNIV guar Increasing (rel o sub i)";
+Goal "Client : UNIV guar Increasing rel";
+by (cut_facts_tac [Client] 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [client_spec_def, client_increasing_def,
+			 guarantees_Int_right]) 1);
+qed "Client_Increasing_rel";
+
+AddIffs [Client_Increasing_ask, Client_Increasing_rel];
+
+Goal "Client : UNIV guar Always {s. ALL elt : set (ask s). elt <= NbT}";
+by (cut_facts_tac [Client] 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [client_spec_def, client_bounded_def]) 1);
+qed "Client_Bounded";
+
+(*Client_Progress we omit for now, since it's cumbersome to state*)
 
 
 
+Goal "lift_prog i Client : UNIV guar Increasing (rel o sub i)";
+by (rtac (Client_Increasing_rel RS lift_prog_guar_Increasing) 1);
+qed "lift_prog_Client_Increasing_rel";
 
 
 
+(*Comp.ML??????????*)
+
+
+
+val project_guarantees' =
+  [inj_sysOfClient, surj_sysOfClient] MRS export project_guarantees;
+
+val extend_guar_Increasing' =
+  [inj_sysOfClient, surj_sysOfClient] MRS export extend_guar_Increasing;
+
+
+(*MUST BE AUTOMATED: even the statement of such results*)
+Goal "!!s. inv sysOfClient s = \
+\            (client s, \
+\             (| allocGiv = allocGiv s, \
+\                allocAsk = allocAsk s, \
+\                allocRel = allocRel s|) )";
+by (rtac (inj_sysOfClient RS inv_f_eq) 1);
+by (rewrite_goals_tac [sysOfAlloc_def, sysOfClient_def]);
+by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
+qed "inv_sysOfClient";
+
+
 
 
-by (stac Acts_eq 1);
-
-fr conjI;
-by (Clarify_tac 1);
-by (stac Init_eq 1);
-
-
-{GX. EX G:X. lift_prog i G component GX}
-{GY. EX G:Y. lift_prog i G component GY}
-
-
-
-uuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuu;
-
-
+val prems =
+Goalw [PLam_def]
+     "[| !!i. i:I ==> F i : X i guar Y i;  \
+\        !!i H. [| i:I; H : XX i |] ==> drop_prog i H : X i;  \
+\        !!i G. [| i:I; F i Join drop_prog i G : Y i |] \
+\               ==> lift_prog i (F i) Join G : YY i |] \
+\        ==> (PLam I F) : (INTER I XX) guar (INTER I YY)";
+by (rtac (drop_prog_guarantees RS guarantees_JN_INT) 1);
+by (REPEAT (ares_tac prems 1));
+qed "drop_prog_guarantees_PLam";
 
 
-Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
-by (cut_facts_tac [Client] 1);
-by (full_simp_tac
-    (simpset() addsimps [System_def,
-			 client_spec_def, client_increasing_def,
-			 guarantees_Int_right]) 1);
+(*for proof of property (1) *)
+Goal "i < Nclients ==> System : Increasing (rel o sub i o client)";
+by (full_simp_tac (simpset() addsimps [System_def]) 1);
+by (rtac ([asm_rl, UNIV_I] MRS guaranteesD) 1);
+by (rtac (disjI2 RS guarantees_Join_I) 1);
+by (rtac project_guarantees' 1);
+by (rtac subset_refl 2);
+by (Clarify_tac 2);
+by (rtac ([extend_guar_Increasing',subset_refl] MRS 
+    guarantees_weaken RS guaranteesD) 2);
+by (rtac UNIV_I 4);
+by (force_tac (claset(),
+	       simpset() addsimps [inv_sysOfClient]) 3);
+by (asm_simp_tac (simpset() addsimps [guarantees_PLam_I, 
+		      Client_Increasing_rel RS lift_prog_guar_Increasing]) 2);
+
+by (rtac (Client_Increasing_rel RS drop_prog_guarantees_PLam RS guarantees_weaken) 1);
+by (force_tac (claset() addIs [lift_prog_Join_Stable],
+	       simpset() addsimps [Increasing_def]) 2);
 by Auto_tac;
-by (dtac lift_prog_guarantees 1);
-by (dtac (UNIV_I RSN (2, guaranteesD)) 1);
-back();
-by (dtac (lessThan_iff RS iffD2 RS const_PLam_Increasing RS iffD2) 1);
-by Auto_tac;
+qed "System_Increasing_rel";
 
 
-by (full_simp_tac (simpset() addsimps [read_instantiate [("f1","rel"),("I1","lessThan Nclients")] (const_PLam_Increasing RS sym)]) 1);
+yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy;
 
-yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy;
 
 
 (*partial system...*)
@@ -121,7 +199,7 @@
 by (full_simp_tac
     (simpset() addsimps [network_spec_def, network_rel_def]) 1);
 
-by (subgoal_tac "" 1);
+
 by (full_simp_tac
     (simpset() addsimps [alloc_spec_def, alloc_safety_def]) 1);
 by Auto_tac;
diff -r dace49c16aca -r ad0ce67e4eb6 src/HOL/UNITY/Alloc.thy
--- a/src/HOL/UNITY/Alloc.thy	Wed Aug 25 11:04:28 1999 +0200
+++ b/src/HOL/UNITY/Alloc.thy	Wed Aug 25 11:09:24 1999 +0200
@@ -64,7 +64,7 @@
 
 (** Client specification (required) ***)
 
-  (*spec (3)*)
+  (*spec (3) PROBABLY REQUIRES A LOCALTO PRECONDITION*)
   client_increasing :: clientState program set
     "client_increasing ==
          UNIV guar Increasing ask Int Increasing rel"
@@ -88,7 +88,7 @@
 
 (** Allocator specification (required) ***)
 
-  (*spec (6)*)
+  (*spec (6)  PROBABLY REQUIRES A LOCALTO PRECONDITION*)
   alloc_increasing :: allocState program set
     "alloc_increasing ==
 	 UNIV