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