# Theory PPROD

theory PPROD
imports Lift_prog
```(*  Title:      HOL/UNITY/PPROD.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Abstraction over replicated components (PLam)
General products of programs (Pi operation)

*)

theory PPROD imports Lift_prog begin

definition PLam :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
=> ((nat=>'b) * 'c) program" where
"PLam I F == ⨆i ∈ I. lift i (F i)"

syntax
"_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"  ("(3plam _:_./ _)" 10)
translations
"plam x : A. B" == "CONST PLam A (%x. B)"

(*** Basic properties ***)

lemma Init_PLam [simp]: "Init (PLam I F) = (⋂i ∈ I. lift_set i (Init (F i)))"
by (simp add: PLam_def lift_def lift_set_def)

lemma PLam_empty [simp]: "PLam {} F = SKIP"

lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"

lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) ⊔ (PLam I F)"
by (unfold PLam_def, auto)

lemma PLam_component_iff: "((PLam I F) ≤ H) = (∀i ∈ I. lift i (F i) ≤ H)"

lemma component_PLam: "i ∈ I ==> lift i (F i) ≤ (PLam I F)"
apply (unfold PLam_def)
(*blast_tac doesn't use HO unification*)
apply (fast intro: component_JN)
done

(** Safety & Progress: but are they used anywhere? **)

lemma PLam_constrains:
"[| i ∈ I;  ∀j. F j ∈ preserves snd |]
==> (PLam I F ∈ (lift_set i (A × UNIV)) co
(lift_set i (B × UNIV)))  =
(F i ∈ (A × UNIV) co (B × UNIV))"
apply (subst insert_Diff [symmetric], assumption)
apply (blast intro: constrains_imp_lift_constrains)
done

lemma PLam_stable:
"[| i ∈ I;  ∀j. F j ∈ preserves snd |]
==> (PLam I F ∈ stable (lift_set i (A × UNIV))) =
(F i ∈ stable (A × UNIV))"

lemma PLam_transient:
"i ∈ I ==>
PLam I F ∈ transient A = (∃i ∈ I. lift i (F i) ∈ transient A)"

text‹This holds because the @{term "F j"} cannot change @{term "lift_set i"}›
lemma PLam_ensures:
"[| i ∈ I;  F i ∈ (A × UNIV) ensures (B × UNIV);
∀j. F j ∈ preserves snd |]
==> PLam I F ∈ lift_set i (A × UNIV) ensures lift_set i (B × UNIV)"
apply (simp add: ensures_def PLam_constrains PLam_transient
lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric]
Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
apply (rule rev_bexI, assumption)
done

"[| i ∈ I;
F i ∈ ((A × UNIV) - (B × UNIV)) co
((A × UNIV) ∪ (B × UNIV));
F i ∈ transient ((A × UNIV) - (B × UNIV));
∀j. F j ∈ preserves snd |]
==> PLam I F ∈ lift_set i (A × UNIV) leadsTo lift_set i (B × UNIV)"
by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)

(** invariant **)

lemma invariant_imp_PLam_invariant:
"[| F i ∈ invariant (A × UNIV);  i ∈ I;
∀j. F j ∈ preserves snd |]
==> PLam I F ∈ invariant (lift_set i (A × UNIV))"
by (auto simp add: PLam_stable invariant_def)

lemma PLam_preserves_fst [simp]:
"∀j. F j ∈ preserves snd
==> (PLam I F ∈ preserves (v o sub j o fst)) =
(if j ∈ I then F j ∈ preserves (v o fst) else True)"

lemma PLam_preserves_snd [simp,intro]:
"∀j. F j ∈ preserves snd ==> PLam I F ∈ preserves snd"

(*** guarantees properties ***)

text‹This rule looks unsatisfactory because it refers to @{term lift}.
One must use
‹lift_guarantees_eq_lift_inv› to rewrite the first subgoal and
something like ‹lift_preserves_sub› to rewrite the third.  However
there's no obvious alternative for the third premise.›
lemma guarantees_PLam_I:
"[| lift i (F i) ∈ X guarantees Y;  i ∈ I;
OK I (λi. lift i (F i)) |]
==> (PLam I F) ∈ X guarantees Y"
apply (unfold PLam_def)
done

lemma Allowed_PLam [simp]:
"Allowed (PLam I F) = (⋂i ∈ I. lift i ` Allowed(F i))"

lemma PLam_preserves [simp]:
"(PLam I F) ∈ preserves v = (∀i ∈ I. F i ∈ preserves (v o lift_map i))"
by (simp add: PLam_def lift_def rename_preserves)

(**UNUSED
(*The f0 premise ensures that the product is well-defined.*)
lemma PLam_invariant_imp_invariant:
"[| PLam I F ∈ invariant (lift_set i A);  i ∈ I;
f0: Init (PLam I F) |] ==> F i ∈ invariant A"
apply (drule_tac c = "f0 (i:=x) " in subsetD)
apply auto
done

lemma PLam_invariant:
"[| i ∈ I;  f0: Init (PLam I F) |]
==> (PLam I F ∈ invariant (lift_set i A)) = (F i ∈ invariant A)"
apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
done

(*The f0 premise isn't needed if F is a constant program because then
we get an initial state by replicating that of F*)
lemma reachable_PLam:
"i ∈ I
==> ((plam x ∈ I. F) ∈ invariant (lift_set i A)) = (F ∈ invariant A)"
done
**)

(**UNUSED
(** Reachability **)

Goal "[| f ∈ reachable (PLam I F);  i ∈ I |] ==> f i ∈ reachable (F i)"
apply (erule reachable.induct)
apply (auto intro: reachable.intrs)
done

(*Result to justify a re-organization of this file*)
lemma "{f. ∀i ∈ I. f i ∈ R i} = (⋂i ∈ I. lift_set i (R i))"
by auto

lemma reachable_PLam_subset1:
"reachable (PLam I F) ⊆ (⋂i ∈ I. lift_set i (reachable (F i)))"
apply (force dest!: reachable_PLam)
done

(*simplify using reachable_lift??*)
lemma reachable_lift_Join_PLam [rule_format]:
"[| i ∉ I;  A ∈ reachable (F i) |]
==> ∀f. f ∈ reachable (PLam I F)
--> f(i:=A) ∈ reachable (lift i (F i) ⊔ PLam I F)"
apply (erule reachable.induct)
apply (ALLGOALS Clarify_tac)
apply (erule reachable.induct)
(*Init, Init case*)
apply (force intro: reachable.intrs)
(*Init of F, action of PLam F case*)
apply (rule_tac act = act in reachable.Acts)
apply force
apply assumption
apply (force intro: ext)
(*induction over the 2nd "reachable" assumption*)
apply (erule_tac xa = f in reachable.induct)
(*Init of PLam F, action of F case*)
apply (rule_tac act = "lift_act i act" in reachable.Acts)
apply force
apply (force intro: reachable.Init)
apply (force intro: ext simp add: lift_act_def)
(*last case: an action of PLam I F*)
apply (rule_tac act = acta in reachable.Acts)
apply force
apply assumption
apply (force intro: ext)
done

(*The index set must be finite: otherwise infinitely many copies of F can
perform actions, and PLam can never catch up in finite time.*)
lemma reachable_PLam_subset2:
"finite I
==> (⋂i ∈ I. lift_set i (reachable (F i))) ⊆ reachable (PLam I F)"
apply (erule finite_induct)
apply (simp (no_asm))
apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
done

lemma reachable_PLam_eq:
"finite I ==>
reachable (PLam I F) = (⋂i ∈ I. lift_set i (reachable (F i)))"
apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
done

(** Co **)

lemma Constrains_imp_PLam_Constrains:
"[| F i ∈ A Co B;  i ∈ I;  finite I |]
==> PLam I F ∈ (lift_set i A) Co (lift_set i B)"
apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
apply (auto simp add: constrains_def PLam_def)
apply (REPEAT (blast intro: reachable.intrs))
done

lemma PLam_Constrains:
"[| i ∈ I;  finite I;  f0: Init (PLam I F) |]
==> (PLam I F ∈ (lift_set i A) Co (lift_set i B)) =
(F i ∈ A Co B)"
apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
done

lemma PLam_Stable:
"[| i ∈ I;  finite I;  f0: Init (PLam I F) |]
==> (PLam I F ∈ Stable (lift_set i A)) = (F i ∈ Stable A)"
apply (simp del: Init_PLam add: Stable_def PLam_Constrains)
done

(** const_PLam (no dependence on i) doesn't require the f0 premise **)

lemma const_PLam_Constrains:
"[| i ∈ I;  finite I |]
==> ((plam x ∈ I. F) ∈ (lift_set i A) Co (lift_set i B)) =
(F ∈ A Co B)"
apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
done

lemma const_PLam_Stable:
"[| i ∈ I;  finite I |]
==> ((plam x ∈ I. F) ∈ Stable (lift_set i A)) = (F ∈ Stable A)"
done

lemma const_PLam_Increasing:
"[| i ∈ I;  finite I |]
==> ((plam x ∈ I. F) ∈ Increasing (f o sub i)) = (F ∈ Increasing f)"
apply (unfold Increasing_def)
apply (subgoal_tac "∀z. {s. z ⊆ (f o sub i) s} = lift_set i {s. z ⊆ f s}")
apply (asm_simp_tac (simpset () add: lift_set_sub) 2)