src/ZF/UNITY/ClientImpl.thy

--- a/src/ZF/UNITY/ClientImpl.thy	Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy	Wed Jun 25 13:17:26 2003 +0200
@@ -8,6 +8,22 @@
 
 
 theory ClientImpl = AllocBase + Guar:
+
+(*????MOVE UP*)
+method_setup constrains = {*
+    Method.ctxt_args (fn ctxt =>
+        Method.METHOD (fn facts =>
+            gen_constrains_tac (Classical.get_local_claset ctxt,
+                               Simplifier.get_local_simpset ctxt) 1)) *}
+    "for proving safety properties"
+
+(*For using "disjunction" (union over an index set) to eliminate a variable.
+  ????move way up*)
+lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
+      ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
+by blast
+
+
 consts
   ask :: i (* input history:  tokens requested *)
   giv :: i (* output history: tokens granted *)
@@ -66,20 +82,6 @@
 declare type_assumes [simp] default_val_assumes [simp]
 (* This part should be automated *)
 
-(*????MOVE UP*)
-method_setup constrains = {*
-    Method.ctxt_args (fn ctxt =>
-        Method.METHOD (fn facts =>
-            gen_constrains_tac (Classical.get_local_claset ctxt,
-                               Simplifier.get_local_simpset ctxt) 1)) *}
-    "for proving safety properties"
-
-(*For using "disjunction" (union over an index set) to eliminate a variable.
-  ????move way up*)
-lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
-      ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
-by blast
-
 lemma ask_value_type [simp,TC]: "s \<in> state ==> s`ask \<in> list(nat)"
 apply (unfold state_def)
 apply (drule_tac a = ask in apply_type, auto)
@@ -164,7 +166,7 @@
 
 lemma ask_Bounded_lemma: 
 "[| client_prog ok G; G \<in> program |] 
-      ==> client_prog Join G \<in>    
+      ==> client_prog \<squnion> G \<in>    
               Always({s \<in> state. s`tok \<le> NbT}  Int   
                       {s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})"
 apply (rotate_tac -1)
@@ -194,15 +196,15 @@
 by (constrains, auto)
 
 lemma client_prog_Join_Stable_rel_le_giv: 
-"[| client_prog Join G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
-    ==> client_prog Join G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
+"[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
+    ==> client_prog \<squnion> G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
 apply (rule client_prog_stable_rel_le_giv [THEN Increasing_preserves_Stable])
 apply (auto simp add: lift_def)
 done
 
 lemma client_prog_Join_Always_rel_le_giv:
-     "[| client_prog Join G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
-    ==> client_prog Join G  \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
+     "[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
+    ==> client_prog \<squnion> G  \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
 by (force intro!: AlwaysI client_prog_Join_Stable_rel_le_giv)
 
 lemma def_act_eq:
@@ -243,8 +245,8 @@
 done
 
 lemma induct_lemma: 
-"[| client_prog Join G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
-  ==> client_prog Join G \<in>  
+"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
+  ==> client_prog \<squnion> G \<in>  
   {s \<in> state. s`rel = k & <k,h> \<in> strict_prefix(nat)  
    & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
         LeadsTo {s \<in> state. <k, s`rel> \<in> strict_prefix(nat)  
@@ -272,8 +274,8 @@
 done
 
 lemma rel_progress_lemma: 
-"[| client_prog Join G  \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
-  ==> client_prog Join G  \<in>  
+"[| client_prog \<squnion> G  \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
+  ==> client_prog \<squnion> G  \<in>  
      {s \<in> state. <s`rel, h> \<in> strict_prefix(nat)  
            & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
                       LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
@@ -301,11 +303,12 @@
 done
 
 lemma progress_lemma: 
-"[| client_prog Join G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] 
- ==> client_prog Join G  \<in>  
-      {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
-      LeadsTo  {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
-apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI], assumption)
+"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] 
+ ==> client_prog \<squnion> G
+       \<in> {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
+         LeadsTo  {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
+apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI], 
+       assumption)
 apply (force simp add: client_prog_ok_iff)
 apply (rule LeadsTo_weaken_L) 
 apply (rule LeadsTo_Un [OF rel_progress_lemma 
@@ -331,4 +334,4 @@
                       cons_Int_distrib safety_prop_Acts_iff)
 done
 
-end
\ No newline at end of file
+end