paulson@5899: (*  Title:      HOL/UNITY/PPROD.thy
paulson@5899:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5899:     Copyright   1998  University of Cambridge
paulson@5899: 
paulson@7188: Abstraction over replicated components (PLam)
paulson@7188: General products of programs (Pi operation)
paulson@13786: 
paulson@13786: Some dead wood here!
paulson@5899: *)
paulson@5899: 
haftmann@16417: theory PPROD imports Lift_prog begin
paulson@5899: 
haftmann@35416: definition PLam :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
haftmann@35416:             => ((nat=>'b) * 'c) program" where
paulson@13805:     "PLam I F == \<Squnion>i \<in> I. lift i (F i)"
paulson@5899: 
paulson@5899: syntax
wenzelm@35054:   "_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"  ("(3plam _:_./ _)" 10)
paulson@5899: translations
wenzelm@35054:   "plam x : A. B" == "CONST PLam A (%x. B)"
paulson@5899: 
paulson@13786: 
paulson@13786: (*** Basic properties ***)
paulson@13786: 
paulson@13812: lemma Init_PLam [simp]: "Init (PLam I F) = (\<Inter>i \<in> I. lift_set i (Init (F i)))"
paulson@13812: by (simp add: PLam_def lift_def lift_set_def)
paulson@13786: 
paulson@13812: lemma PLam_empty [simp]: "PLam {} F = SKIP"
paulson@13812: by (simp add: PLam_def)
paulson@13786: 
paulson@13812: lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
wenzelm@46577: by (simp add: PLam_def JN_constant)
paulson@13786: 
wenzelm@60773: lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) \<squnion> (PLam I F)"
paulson@13786: by (unfold PLam_def, auto)
paulson@13786: 
paulson@13805: lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
paulson@13812: by (simp add: PLam_def JN_component_iff)
paulson@13786: 
paulson@13805: lemma component_PLam: "i \<in> I ==> lift i (F i) \<le> (PLam I F)"
paulson@13786: apply (unfold PLam_def)
paulson@13786: (*blast_tac doesn't use HO unification*)
paulson@13786: apply (fast intro: component_JN)
paulson@13786: done
paulson@13786: 
paulson@13786: 
paulson@13786: (** Safety & Progress: but are they used anywhere? **)
paulson@13786: 
paulson@13812: lemma PLam_constrains:
paulson@13812:      "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
wenzelm@61943:       ==> (PLam I F \<in> (lift_set i (A \<times> UNIV)) co
wenzelm@61943:                       (lift_set i (B \<times> UNIV)))  =
wenzelm@61943:           (F i \<in> (A \<times> UNIV) co (B \<times> UNIV))"
paulson@13812: apply (simp add: PLam_def JN_constrains)
paulson@13786: apply (subst insert_Diff [symmetric], assumption)
paulson@13812: apply (simp add: lift_constrains)
paulson@13786: apply (blast intro: constrains_imp_lift_constrains)
paulson@13786: done
paulson@13786: 
paulson@13812: lemma PLam_stable:
paulson@13812:      "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
wenzelm@61943:       ==> (PLam I F \<in> stable (lift_set i (A \<times> UNIV))) =
wenzelm@61943:           (F i \<in> stable (A \<times> UNIV))"
paulson@13812: by (simp add: stable_def PLam_constrains)
paulson@13812: 
paulson@13812: lemma PLam_transient:
paulson@13812:      "i \<in> I ==>
paulson@13812:     PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
paulson@13812: by (simp add: JN_transient PLam_def)
paulson@13786: 
paulson@13812: text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*}
paulson@13812: lemma PLam_ensures:
wenzelm@61943:      "[| i \<in> I;  F i \<in> (A \<times> UNIV) ensures (B \<times> UNIV);
paulson@13812:          \<forall>j. F j \<in> preserves snd |]
wenzelm@61943:       ==> PLam I F \<in> lift_set i (A \<times> UNIV) ensures lift_set i (B \<times> UNIV)"
paulson@13812: apply (simp add: ensures_def PLam_constrains PLam_transient
paulson@13812:               lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric]
paulson@13812:               Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
paulson@13812: apply (rule rev_bexI, assumption)
paulson@13812: apply (simp add: lift_transient)
paulson@13786: done
paulson@13786: 
paulson@13812: lemma PLam_leadsTo_Basis:
paulson@13812:      "[| i \<in> I;
wenzelm@61943:          F i \<in> ((A \<times> UNIV) - (B \<times> UNIV)) co
wenzelm@61943:                ((A \<times> UNIV) \<union> (B \<times> UNIV));
wenzelm@61943:          F i \<in> transient ((A \<times> UNIV) - (B \<times> UNIV));
paulson@13812:          \<forall>j. F j \<in> preserves snd |]
wenzelm@61943:       ==> PLam I F \<in> lift_set i (A \<times> UNIV) leadsTo lift_set i (B \<times> UNIV)"
paulson@13786: by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
paulson@13786: 
paulson@13786: 
paulson@13786: 
paulson@13786: (** invariant **)
paulson@13786: 
paulson@13812: lemma invariant_imp_PLam_invariant:
wenzelm@61943:      "[| F i \<in> invariant (A \<times> UNIV);  i \<in> I;
paulson@13812:          \<forall>j. F j \<in> preserves snd |]
wenzelm@61943:       ==> PLam I F \<in> invariant (lift_set i (A \<times> UNIV))"
paulson@13786: by (auto simp add: PLam_stable invariant_def)
paulson@13786: 
paulson@13786: 
paulson@13786: lemma PLam_preserves_fst [simp]:
paulson@13812:      "\<forall>j. F j \<in> preserves snd
paulson@13812:       ==> (PLam I F \<in> preserves (v o sub j o fst)) =
paulson@13805:           (if j \<in> I then F j \<in> preserves (v o fst) else True)"
paulson@13812: by (simp add: PLam_def lift_preserves_sub)
paulson@13786: 
paulson@13786: lemma PLam_preserves_snd [simp,intro]:
paulson@13805:      "\<forall>j. F j \<in> preserves snd ==> PLam I F \<in> preserves snd"
paulson@13812: by (simp add: PLam_def lift_preserves_snd_I)
paulson@13786: 
paulson@13786: 
paulson@13786: 
paulson@13786: (*** guarantees properties ***)
paulson@13786: 
paulson@14150: text{*This rule looks unsatisfactory because it refers to @{term lift}. 
paulson@14150:   One must use
paulson@14150:   @{text lift_guarantees_eq_lift_inv} to rewrite the first subgoal and
paulson@14150:   something like @{text lift_preserves_sub} to rewrite the third.  However
paulson@14150:   there's no obvious alternative for the third premise.*}
paulson@13812: lemma guarantees_PLam_I:
paulson@13812:     "[| lift i (F i): X guarantees Y;  i \<in> I;
paulson@13812:         OK I (%i. lift i (F i)) |]
paulson@13805:      ==> (PLam I F) \<in> X guarantees Y"
paulson@13786: apply (unfold PLam_def)
paulson@13812: apply (simp add: guarantees_JN_I)
paulson@13786: done
paulson@13786: 
paulson@13786: lemma Allowed_PLam [simp]:
paulson@13805:      "Allowed (PLam I F) = (\<Inter>i \<in> I. lift i ` Allowed(F i))"
paulson@13812: by (simp add: PLam_def)
paulson@13786: 
paulson@13786: 
paulson@13786: lemma PLam_preserves [simp]:
paulson@13805:      "(PLam I F) \<in> preserves v = (\<forall>i \<in> I. F i \<in> preserves (v o lift_map i))"
paulson@13805: by (simp add: PLam_def lift_def rename_preserves)
paulson@13786: 
paulson@13786: 
paulson@13786: (**UNUSED
paulson@13786:     (*The f0 premise ensures that the product is well-defined.*)
paulson@13812:     lemma PLam_invariant_imp_invariant:
paulson@13812:      "[| PLam I F \<in> invariant (lift_set i A);  i \<in> I;
paulson@13805:              f0: Init (PLam I F) |] ==> F i \<in> invariant A"
paulson@13786:     apply (auto simp add: invariant_def)
paulson@13786:     apply (drule_tac c = "f0 (i:=x) " in subsetD)
paulson@13786:     apply auto
paulson@13786:     done
paulson@13786: 
paulson@13812:     lemma PLam_invariant:
paulson@13812:      "[| i \<in> I;  f0: Init (PLam I F) |]
paulson@13805:           ==> (PLam I F \<in> invariant (lift_set i A)) = (F i \<in> invariant A)"
paulson@13786:     apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
paulson@13786:     done
paulson@13786: 
paulson@13786:     (*The f0 premise isn't needed if F is a constant program because then
paulson@13786:       we get an initial state by replicating that of F*)
paulson@13812:     lemma reachable_PLam:
paulson@13812:      "i \<in> I
paulson@13805:           ==> ((plam x \<in> I. F) \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
paulson@13786:     apply (auto simp add: invariant_def)
paulson@13786:     done
paulson@13786: **)
paulson@13786: 
paulson@13786: 
paulson@13786: (**UNUSED
paulson@13786:     (** Reachability **)
paulson@13786: 
paulson@13805:     Goal "[| f \<in> reachable (PLam I F);  i \<in> I |] ==> f i \<in> reachable (F i)"
paulson@13786:     apply (erule reachable.induct)
paulson@13786:     apply (auto intro: reachable.intrs)
paulson@13786:     done
paulson@13786: 
paulson@13786:     (*Result to justify a re-organization of this file*)
paulson@13805:     lemma "{f. \<forall>i \<in> I. f i \<in> R i} = (\<Inter>i \<in> I. lift_set i (R i))"
paulson@13798:     by auto
paulson@13786: 
paulson@13812:     lemma reachable_PLam_subset1:
paulson@13805:      "reachable (PLam I F) \<subseteq> (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
paulson@13786:     apply (force dest!: reachable_PLam)
paulson@13786:     done
paulson@13786: 
paulson@13786:     (*simplify using reachable_lift??*)
paulson@13798:     lemma reachable_lift_Join_PLam [rule_format]:
paulson@13812:       "[| i \<notin> I;  A \<in> reachable (F i) |]
paulson@13812:        ==> \<forall>f. f \<in> reachable (PLam I F)
wenzelm@60773:                   --> f(i:=A) \<in> reachable (lift i (F i) \<squnion> PLam I F)"
paulson@13786:     apply (erule reachable.induct)
paulson@13786:     apply (ALLGOALS Clarify_tac)
paulson@13786:     apply (erule reachable.induct)
paulson@13786:     (*Init, Init case*)
paulson@13786:     apply (force intro: reachable.intrs)
paulson@13786:     (*Init of F, action of PLam F case*)
paulson@13786:     apply (rule_tac act = act in reachable.Acts)
paulson@13786:     apply force
paulson@13786:     apply assumption
paulson@13786:     apply (force intro: ext)
paulson@13786:     (*induction over the 2nd "reachable" assumption*)
paulson@13786:     apply (erule_tac xa = f in reachable.induct)
paulson@13786:     (*Init of PLam F, action of F case*)
paulson@13786:     apply (rule_tac act = "lift_act i act" in reachable.Acts)
paulson@13786:     apply force
paulson@13786:     apply (force intro: reachable.Init)
paulson@13786:     apply (force intro: ext simp add: lift_act_def)
paulson@13786:     (*last case: an action of PLam I F*)
paulson@13786:     apply (rule_tac act = acta in reachable.Acts)
paulson@13786:     apply force
paulson@13786:     apply assumption
paulson@13786:     apply (force intro: ext)
paulson@13786:     done
paulson@13786: 
paulson@13786: 
paulson@13786:     (*The index set must be finite: otherwise infinitely many copies of F can
paulson@13786:       perform actions, and PLam can never catch up in finite time.*)
paulson@13812:     lemma reachable_PLam_subset2:
paulson@13812:      "finite I
paulson@13805:           ==> (\<Inter>i \<in> I. lift_set i (reachable (F i))) \<subseteq> reachable (PLam I F)"
paulson@13786:     apply (erule finite_induct)
paulson@13786:     apply (simp (no_asm))
paulson@13786:     apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
paulson@13786:     done
paulson@13786: 
paulson@13812:     lemma reachable_PLam_eq:
paulson@13812:      "finite I ==>
paulson@13805:           reachable (PLam I F) = (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
paulson@13786:     apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
paulson@13786:     done
paulson@13786: 
paulson@13786: 
paulson@13786:     (** Co **)
paulson@13786: 
paulson@13812:     lemma Constrains_imp_PLam_Constrains:
paulson@13812:      "[| F i \<in> A Co B;  i \<in> I;  finite I |]
paulson@13805:           ==> PLam I F \<in> (lift_set i A) Co (lift_set i B)"
paulson@13786:     apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
paulson@13786:     apply (auto simp add: constrains_def PLam_def)
paulson@13786:     apply (REPEAT (blast intro: reachable.intrs))
paulson@13786:     done
paulson@13786: 
paulson@13786: 
paulson@13786: 
paulson@13812:     lemma PLam_Constrains:
paulson@13812:      "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]
paulson@13812:           ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) =
paulson@13805:               (F i \<in> A Co B)"
paulson@13786:     apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
paulson@13786:     done
paulson@13786: 
paulson@13812:     lemma PLam_Stable:
paulson@13812:      "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]
paulson@13805:           ==> (PLam I F \<in> Stable (lift_set i A)) = (F i \<in> Stable A)"
paulson@13812:     apply (simp del: Init_PLam add: Stable_def PLam_Constrains)
paulson@13786:     done
paulson@13786: 
paulson@13786: 
paulson@13786:     (** const_PLam (no dependence on i) doesn't require the f0 premise **)
paulson@13786: 
paulson@13812:     lemma const_PLam_Constrains:
paulson@13812:      "[| i \<in> I;  finite I |]
paulson@13812:           ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) =
paulson@13805:               (F \<in> A Co B)"
paulson@13786:     apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
paulson@13786:     done
paulson@13786: 
paulson@13812:     lemma const_PLam_Stable:
paulson@13812:      "[| i \<in> I;  finite I |]
paulson@13805:           ==> ((plam x \<in> I. F) \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
paulson@13812:     apply (simp add: Stable_def const_PLam_Constrains)
paulson@13786:     done
paulson@13786: 
paulson@13812:     lemma const_PLam_Increasing:
wenzelm@32960:          "[| i \<in> I;  finite I |]
paulson@13805:           ==> ((plam x \<in> I. F) \<in> Increasing (f o sub i)) = (F \<in> Increasing f)"
paulson@13786:     apply (unfold Increasing_def)
paulson@13805:     apply (subgoal_tac "\<forall>z. {s. z \<subseteq> (f o sub i) s} = lift_set i {s. z \<subseteq> f s}")
paulson@13786:     apply (asm_simp_tac (simpset () add: lift_set_sub) 2)
paulson@13786:     apply (simp add: finite_lessThan const_PLam_Stable)
paulson@13786:     done
paulson@13786: **)
paulson@13786: 
paulson@13786: 
paulson@5899: end