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