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