src/HOL/UNITY/PPROD.thy
author paulson
Tue Feb 04 18:12:40 2003 +0100 (2003-02-04)
changeset 13805 3786b2fd6808
parent 13798 4c1a53627500
child 13812 91713a1915ee
permissions -rw-r--r--
some x-symbols
     1 (*  Title:      HOL/UNITY/PPROD.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Abstraction over replicated components (PLam)
     7 General products of programs (Pi operation)
     8 
     9 Some dead wood here!
    10 *)
    11 
    12 theory PPROD = Lift_prog:
    13 
    14 constdefs
    15 
    16   PLam  :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
    17             => ((nat=>'b) * 'c) program"
    18     "PLam I F == \<Squnion>i \<in> I. lift i (F i)"
    19 
    20 syntax
    21   "@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"
    22               ("(3plam _:_./ _)" 10)
    23 
    24 translations
    25   "plam x : A. B"   == "PLam A (%x. B)"
    26 
    27 
    28 (*** Basic properties ***)
    29 
    30 lemma Init_PLam: "Init (PLam I F) = (\<Inter>i \<in> I. lift_set i (Init (F i)))"
    31 apply (simp (no_asm) add: PLam_def lift_def lift_set_def)
    32 done
    33 
    34 declare Init_PLam [simp]
    35 
    36 lemma PLam_empty: "PLam {} F = SKIP"
    37 apply (simp (no_asm) add: PLam_def)
    38 done
    39 
    40 lemma PLam_SKIP: "(plam i : I. SKIP) = SKIP"
    41 apply (simp (no_asm) add: PLam_def lift_SKIP JN_constant)
    42 done
    43 
    44 declare PLam_SKIP [simp] PLam_empty [simp]
    45 
    46 lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
    47 by (unfold PLam_def, auto)
    48 
    49 lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
    50 apply (simp (no_asm) add: PLam_def JN_component_iff)
    51 done
    52 
    53 lemma component_PLam: "i \<in> I ==> lift i (F i) \<le> (PLam I F)"
    54 apply (unfold PLam_def)
    55 (*blast_tac doesn't use HO unification*)
    56 apply (fast intro: component_JN)
    57 done
    58 
    59 
    60 (** Safety & Progress: but are they used anywhere? **)
    61 
    62 lemma PLam_constrains: 
    63      "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |] ==>   
    64       (PLam I F \<in> (lift_set i (A <*> UNIV)) co  
    65                   (lift_set i (B <*> UNIV)))  =   
    66       (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
    67 apply (simp (no_asm_simp) add: PLam_def JN_constrains)
    68 apply (subst insert_Diff [symmetric], assumption)
    69 apply (simp (no_asm_simp) add: lift_constrains)
    70 apply (blast intro: constrains_imp_lift_constrains)
    71 done
    72 
    73 lemma PLam_stable: 
    74      "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]   
    75       ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =  
    76           (F i \<in> stable (A <*> UNIV))"
    77 apply (simp (no_asm_simp) add: stable_def PLam_constrains)
    78 done
    79 
    80 lemma PLam_transient: 
    81      "i \<in> I ==>  
    82     PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
    83 apply (simp (no_asm_simp) add: JN_transient PLam_def)
    84 done
    85 
    86 (*This holds because the F j cannot change (lift_set i)*)
    87 lemma PLam_ensures: 
    88      "[| i \<in> I;  F i \<in> (A <*> UNIV) ensures (B <*> UNIV);   
    89          \<forall>j. F j \<in> preserves snd |] ==>   
    90       PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
    91 apply (auto simp add: ensures_def PLam_constrains PLam_transient lift_transient_eq_disj lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
    92 done
    93 
    94 lemma PLam_leadsTo_Basis: 
    95      "[| i \<in> I;   
    96          F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co  
    97                ((A <*> UNIV) \<union> (B <*> UNIV));   
    98          F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));   
    99          \<forall>j. F j \<in> preserves snd |] ==>   
   100       PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
   101 by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
   102 
   103 
   104 
   105 (** invariant **)
   106 
   107 lemma invariant_imp_PLam_invariant: 
   108      "[| F i \<in> invariant (A <*> UNIV);  i \<in> I;   
   109          \<forall>j. F j \<in> preserves snd |]  
   110       ==> PLam I F \<in> invariant (lift_set i (A <*> UNIV))"
   111 by (auto simp add: PLam_stable invariant_def)
   112 
   113 
   114 lemma PLam_preserves_fst [simp]:
   115      "\<forall>j. F j \<in> preserves snd  
   116       ==> (PLam I F \<in> preserves (v o sub j o fst)) =  
   117           (if j \<in> I then F j \<in> preserves (v o fst) else True)"
   118 by (simp (no_asm_simp) add: PLam_def lift_preserves_sub)
   119 
   120 lemma PLam_preserves_snd [simp,intro]:
   121      "\<forall>j. F j \<in> preserves snd ==> PLam I F \<in> preserves snd"
   122 by (simp (no_asm_simp) add: PLam_def lift_preserves_snd_I)
   123 
   124 
   125 
   126 (*** guarantees properties ***)
   127 
   128 (*This rule looks unsatisfactory because it refers to "lift".  One must use
   129   lift_guarantees_eq_lift_inv to rewrite the first subgoal and
   130   something like lift_preserves_sub to rewrite the third.  However there's
   131   no obvious way to alternative for the third premise.*)
   132 lemma guarantees_PLam_I: 
   133     "[| lift i (F i): X guarantees Y;  i \<in> I;   
   134         OK I (%i. lift i (F i)) |]   
   135      ==> (PLam I F) \<in> X guarantees Y"
   136 apply (unfold PLam_def)
   137 apply (simp (no_asm_simp) add: guarantees_JN_I)
   138 done
   139 
   140 lemma Allowed_PLam [simp]:
   141      "Allowed (PLam I F) = (\<Inter>i \<in> I. lift i ` Allowed(F i))"
   142 by (simp (no_asm) add: PLam_def)
   143 
   144 
   145 lemma PLam_preserves [simp]:
   146      "(PLam I F) \<in> preserves v = (\<forall>i \<in> I. F i \<in> preserves (v o lift_map i))"
   147 by (simp add: PLam_def lift_def rename_preserves)
   148 
   149 
   150 (**UNUSED
   151     (*The f0 premise ensures that the product is well-defined.*)
   152     lemma PLam_invariant_imp_invariant: 
   153      "[| PLam I F \<in> invariant (lift_set i A);  i \<in> I;   
   154              f0: Init (PLam I F) |] ==> F i \<in> invariant A"
   155     apply (auto simp add: invariant_def)
   156     apply (drule_tac c = "f0 (i:=x) " in subsetD)
   157     apply auto
   158     done
   159 
   160     lemma PLam_invariant: 
   161      "[| i \<in> I;  f0: Init (PLam I F) |]  
   162           ==> (PLam I F \<in> invariant (lift_set i A)) = (F i \<in> invariant A)"
   163     apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
   164     done
   165 
   166     (*The f0 premise isn't needed if F is a constant program because then
   167       we get an initial state by replicating that of F*)
   168     lemma reachable_PLam: 
   169      "i \<in> I  
   170           ==> ((plam x \<in> I. F) \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
   171     apply (auto simp add: invariant_def)
   172     done
   173 **)
   174 
   175 
   176 (**UNUSED
   177     (** Reachability **)
   178 
   179     Goal "[| f \<in> reachable (PLam I F);  i \<in> I |] ==> f i \<in> reachable (F i)"
   180     apply (erule reachable.induct)
   181     apply (auto intro: reachable.intrs)
   182     done
   183 
   184     (*Result to justify a re-organization of this file*)
   185     lemma "{f. \<forall>i \<in> I. f i \<in> R i} = (\<Inter>i \<in> I. lift_set i (R i))"
   186     by auto
   187 
   188     lemma reachable_PLam_subset1: 
   189      "reachable (PLam I F) \<subseteq> (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
   190     apply (force dest!: reachable_PLam)
   191     done
   192 
   193     (*simplify using reachable_lift??*)
   194     lemma reachable_lift_Join_PLam [rule_format]:
   195       "[| i \<notin> I;  A \<in> reachable (F i) |]      
   196        ==> \<forall>f. f \<in> reachable (PLam I F)       
   197                   --> f(i:=A) \<in> reachable (lift i (F i) Join PLam I F)"
   198     apply (erule reachable.induct)
   199     apply (ALLGOALS Clarify_tac)
   200     apply (erule reachable.induct)
   201     (*Init, Init case*)
   202     apply (force intro: reachable.intrs)
   203     (*Init of F, action of PLam F case*)
   204     apply (rule_tac act = act in reachable.Acts)
   205     apply force
   206     apply assumption
   207     apply (force intro: ext)
   208     (*induction over the 2nd "reachable" assumption*)
   209     apply (erule_tac xa = f in reachable.induct)
   210     (*Init of PLam F, action of F case*)
   211     apply (rule_tac act = "lift_act i act" in reachable.Acts)
   212     apply force
   213     apply (force intro: reachable.Init)
   214     apply (force intro: ext simp add: lift_act_def)
   215     (*last case: an action of PLam I F*)
   216     apply (rule_tac act = acta in reachable.Acts)
   217     apply force
   218     apply assumption
   219     apply (force intro: ext)
   220     done
   221 
   222 
   223     (*The index set must be finite: otherwise infinitely many copies of F can
   224       perform actions, and PLam can never catch up in finite time.*)
   225     lemma reachable_PLam_subset2: 
   226      "finite I  
   227           ==> (\<Inter>i \<in> I. lift_set i (reachable (F i))) \<subseteq> reachable (PLam I F)"
   228     apply (erule finite_induct)
   229     apply (simp (no_asm))
   230     apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
   231     done
   232 
   233     lemma reachable_PLam_eq: 
   234      "finite I ==>  
   235           reachable (PLam I F) = (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
   236     apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
   237     done
   238 
   239 
   240     (** Co **)
   241 
   242     lemma Constrains_imp_PLam_Constrains: 
   243      "[| F i \<in> A Co B;  i \<in> I;  finite I |]   
   244           ==> PLam I F \<in> (lift_set i A) Co (lift_set i B)"
   245     apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
   246     apply (auto simp add: constrains_def PLam_def)
   247     apply (REPEAT (blast intro: reachable.intrs))
   248     done
   249 
   250 
   251 
   252     lemma PLam_Constrains: 
   253      "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]   
   254           ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) =   
   255               (F i \<in> A Co B)"
   256     apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
   257     done
   258 
   259     lemma PLam_Stable: 
   260      "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]   
   261           ==> (PLam I F \<in> Stable (lift_set i A)) = (F i \<in> Stable A)"
   262     apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains)
   263     done
   264 
   265 
   266     (** const_PLam (no dependence on i) doesn't require the f0 premise **)
   267 
   268     lemma const_PLam_Constrains: 
   269      "[| i \<in> I;  finite I |]   
   270           ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) =   
   271               (F \<in> A Co B)"
   272     apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
   273     done
   274 
   275     lemma const_PLam_Stable: 
   276      "[| i \<in> I;  finite I |]   
   277           ==> ((plam x \<in> I. F) \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
   278     apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains)
   279     done
   280 
   281     lemma const_PLam_Increasing: 
   282 	 "[| i \<in> I;  finite I |]   
   283           ==> ((plam x \<in> I. F) \<in> Increasing (f o sub i)) = (F \<in> Increasing f)"
   284     apply (unfold Increasing_def)
   285     apply (subgoal_tac "\<forall>z. {s. z \<subseteq> (f o sub i) s} = lift_set i {s. z \<subseteq> f s}")
   286     apply (asm_simp_tac (simpset () add: lift_set_sub) 2)
   287     apply (simp add: finite_lessThan const_PLam_Stable)
   288     done
   289 **)
   290 
   291 
   292 end