# Theory PPROD

Up to index of Isabelle/HOL/UNITY

theory PPROD
imports Lift_prog
begin

    (*  Title:      HOL/UNITY/PPROD.thy
        ID:         $Id: PPROD.thy,v 1.15 2005/06/17 14:13:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge

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

    Some dead wood here!
    *)

    theory PPROD imports Lift_prog begin

    constdefs

      PLam  :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
                => ((nat=>'b) * 'c) program"
        "PLam I F == \<Squnion>i ∈ I. lift i (F i)"

    syntax
      "@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"
                  ("(3plam _:_./ _)" 10)

    translations
      "plam x : A. B"   == "PLam A (%x. B)"

    (*** Basic properties ***)

    lemma Init_PLam [simp]: "Init (PLam I F) = (\<Inter>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"
    by (simp add: PLam_def)

    lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
    by (simp add: PLam_def lift_SKIP JN_constant)

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

    lemma PLam_component_iff: "((PLam I F) ≤ H) = (∀i ∈ I. lift i (F i) ≤ H)"
    by (simp add: PLam_def JN_component_iff)

    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 (simp add: PLam_def JN_constrains)
    apply (subst insert_Diff [symmetric], assumption)
    apply (simp add: lift_constrains)
    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))"
    by (simp add: stable_def PLam_constrains)

    lemma PLam_transient:
         "i ∈ I ==>
        PLam I F ∈ transient A = (∃i ∈ I. lift i (F i) ∈ transient A)"
    by (simp add: JN_transient PLam_def)

    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)
    apply (simp add: lift_transient)
    done

    lemma PLam_leadsTo_Basis:
         "[| 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)"
    by (simp add: PLam_def lift_preserves_sub)

    lemma PLam_preserves_snd [simp,intro]:
         "∀j. F j ∈ preserves snd ==> PLam I F ∈ preserves snd"
    by (simp add: PLam_def lift_preserves_snd_I)

    (*** guarantees properties ***)

    text{*This rule looks unsatisfactory because it refers to @{term lift}.
      One must use
      @{text lift_guarantees_eq_lift_inv} to rewrite the first subgoal and
      something like @{text 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)
    apply (simp add: guarantees_JN_I)
    done

    lemma Allowed_PLam [simp]:
         "Allowed (PLam I F) = (\<Inter>i ∈ I. lift i ` Allowed(F i))"
    by (simp add: PLam_def)

    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 (auto simp add: invariant_def)
        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)"
        apply (auto simp add: invariant_def)
        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} = (\<Inter>i ∈ I. lift_set i (R i))"
        by auto

        lemma reachable_PLam_subset1:
         "reachable (PLam I F) ⊆ (\<Inter>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) Join 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
              ==> (\<Inter>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) = (\<Inter>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)"
        apply (simp add: Stable_def const_PLam_Constrains)
        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)
        apply (simp add: finite_lessThan const_PLam_Stable)
        done
    **)

    end

lemma Init_PLam:

      Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))

lemma PLam_empty:

      PLam {} F = SKIP

lemma PLam_SKIP:

      (plam i:I. SKIP) = SKIP

lemma PLam_insert:

      PLam (insert i I) F = lift i (F i) Join PLam I F

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

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)

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)

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)

lemma PLam_leadsTo_Basis:

      [| 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)

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))

lemma PLam_preserves_fst:

      ∀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:

      ∀j. F j ∈ preserves snd ==> PLam I F ∈ preserves snd

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

lemma Allowed_PLam:

      Allowed (PLam I F) = (INT i:I. lift i ` Allowed (F i))

lemma PLam_preserves:

      (PLam I F ∈ preserves v) = (∀i∈I. F i ∈ preserves (v o lift_map i))