# Theory Union

Up to index of Isabelle/HOL/UNITY

theory Union
imports SubstAx FP
begin

    (*  Title:      HOL/UNITY/Union.thy
        ID:         $Id: Union.thy,v 1.27 2005/08/01 17:20:31 wenzelm Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge

    Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
    *)

    header{*Unions of Programs*}

    theory Union imports SubstAx FP begin

    constdefs

      (*FIXME: conjoin Init F ∩ Init G ≠ {} *)
      ok :: "['a program, 'a program] => bool"      (infixl "ok" 65)
        "F ok G == Acts F ⊆ AllowedActs G &
                   Acts G ⊆ AllowedActs F"

      (*FIXME: conjoin (\<Inter>i ∈ I. Init (F i)) ≠ {} *)
      OK  :: "['a set, 'a => 'b program] => bool"
        "OK I F == (∀i ∈ I. ∀j ∈ I-{i}. Acts (F i) ⊆ AllowedActs (F j))"

      JOIN  :: "['a set, 'a => 'b program] => 'b program"
        "JOIN I F == mk_program (\<Inter>i ∈ I. Init (F i), \<Union>i ∈ I. Acts (F i),
                                 \<Inter>i ∈ I. AllowedActs (F i))"

      Join :: "['a program, 'a program] => 'a program"      (infixl "Join" 65)
        "F Join G == mk_program (Init F ∩ Init G, Acts F ∪ Acts G,
                                 AllowedActs F ∩ AllowedActs G)"

      SKIP :: "'a program"
        "SKIP == mk_program (UNIV, {}, UNIV)"

      (*Characterizes safety properties.  Used with specifying Allowed*)
      safety_prop :: "'a program set => bool"
        "safety_prop X == SKIP: X & (∀G. Acts G ⊆ UNION X Acts --> G ∈ X)"

    syntax
      "@JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
      "@JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)

    translations
      "JN x : A. B"   == "JOIN A (%x. B)"
      "JN x y. B"   == "JN x. JN y. B"
      "JN x. B"     == "JOIN UNIV (%x. B)"

    syntax (xsymbols)
      SKIP     :: "'a program"                              ("⊥")
      Join     :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
      "@JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
      "@JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _∈_./ _)" 10)

    subsection{*SKIP*}

    lemma Init_SKIP [simp]: "Init SKIP = UNIV"
    by (simp add: SKIP_def)

    lemma Acts_SKIP [simp]: "Acts SKIP = {Id}"
    by (simp add: SKIP_def)

    lemma AllowedActs_SKIP [simp]: "AllowedActs SKIP = UNIV"
    by (auto simp add: SKIP_def)

    lemma reachable_SKIP [simp]: "reachable SKIP = UNIV"
    by (force elim: reachable.induct intro: reachable.intros)

    subsection{*SKIP and safety properties*}

    lemma SKIP_in_constrains_iff [iff]: "(SKIP ∈ A co B) = (A ⊆ B)"
    by (unfold constrains_def, auto)

    lemma SKIP_in_Constrains_iff [iff]: "(SKIP ∈ A Co B) = (A ⊆ B)"
    by (unfold Constrains_def, auto)

    lemma SKIP_in_stable [iff]: "SKIP ∈ stable A"
    by (unfold stable_def, auto)

    declare SKIP_in_stable [THEN stable_imp_Stable, iff]

    subsection{*Join*}

    lemma Init_Join [simp]: "Init (F\<squnion>G) = Init F ∩ Init G"
    by (simp add: Join_def)

    lemma Acts_Join [simp]: "Acts (F\<squnion>G) = Acts F ∪ Acts G"
    by (auto simp add: Join_def)

    lemma AllowedActs_Join [simp]:
         "AllowedActs (F\<squnion>G) = AllowedActs F ∩ AllowedActs G"
    by (auto simp add: Join_def)

    subsection{*JN*}

    lemma JN_empty [simp]: "(\<Squnion>i∈{}. F i) = SKIP"
    by (unfold JOIN_def SKIP_def, auto)

    lemma JN_insert [simp]: "(\<Squnion>i ∈ insert a I. F i) = (F a)\<squnion>(\<Squnion>i ∈ I. F i)"
    apply (rule program_equalityI)
    apply (auto simp add: JOIN_def Join_def)
    done

    lemma Init_JN [simp]: "Init (\<Squnion>i ∈ I. F i) = (\<Inter>i ∈ I. Init (F i))"
    by (simp add: JOIN_def)

    lemma Acts_JN [simp]: "Acts (\<Squnion>i ∈ I. F i) = insert Id (\<Union>i ∈ I. Acts (F i))"
    by (auto simp add: JOIN_def)

    lemma AllowedActs_JN [simp]:
         "AllowedActs (\<Squnion>i ∈ I. F i) = (\<Inter>i ∈ I. AllowedActs (F i))"
    by (auto simp add: JOIN_def)

    lemma JN_cong [cong]:
        "[| I=J;  !!i. i ∈ J ==> F i = G i |] ==> (\<Squnion>i ∈ I. F i) = (\<Squnion>i ∈ J. G i)"
    by (simp add: JOIN_def)

    subsection{*Algebraic laws*}

    lemma Join_commute: "F\<squnion>G = G\<squnion>F"
    by (simp add: Join_def Un_commute Int_commute)

    lemma Join_assoc: "(F\<squnion>G)\<squnion>H = F\<squnion>(G\<squnion>H)"
    by (simp add: Un_ac Join_def Int_assoc insert_absorb)

    lemma Join_left_commute: "A\<squnion>(B\<squnion>C) = B\<squnion>(A\<squnion>C)"
    by (simp add: Un_ac Int_ac Join_def insert_absorb)

    lemma Join_SKIP_left [simp]: "SKIP\<squnion>F = F"
    apply (unfold Join_def SKIP_def)
    apply (rule program_equalityI)
    apply (simp_all (no_asm) add: insert_absorb)
    done

    lemma Join_SKIP_right [simp]: "F\<squnion>SKIP = F"
    apply (unfold Join_def SKIP_def)
    apply (rule program_equalityI)
    apply (simp_all (no_asm) add: insert_absorb)
    done

    lemma Join_absorb [simp]: "F\<squnion>F = F"
    apply (unfold Join_def)
    apply (rule program_equalityI, auto)
    done

    lemma Join_left_absorb: "F\<squnion>(F\<squnion>G) = F\<squnion>G"
    apply (unfold Join_def)
    apply (rule program_equalityI, auto)
    done

    (*Join is an AC-operator*)
    lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute

    subsection{*Laws Governing @{text "\<Squnion>"}*}

    (*Also follows by JN_insert and insert_absorb, but the proof is longer*)
    lemma JN_absorb: "k ∈ I ==> F k\<squnion>(\<Squnion>i ∈ I. F i) = (\<Squnion>i ∈ I. F i)"
    by (auto intro!: program_equalityI)

    lemma JN_Un: "(\<Squnion>i ∈ I ∪ J. F i) = ((\<Squnion>i ∈ I. F i)\<squnion>(\<Squnion>i ∈ J. F i))"
    by (auto intro!: program_equalityI)

    lemma JN_constant: "(\<Squnion>i ∈ I. c) = (if I={} then SKIP else c)"
    by (rule program_equalityI, auto)

    lemma JN_Join_distrib:
         "(\<Squnion>i ∈ I. F i\<squnion>G i) = (\<Squnion>i ∈ I. F i) \<squnion> (\<Squnion>i ∈ I. G i)"
    by (auto intro!: program_equalityI)

    lemma JN_Join_miniscope:
         "i ∈ I ==> (\<Squnion>i ∈ I. F i\<squnion>G) = ((\<Squnion>i ∈ I. F i)\<squnion>G)"
    by (auto simp add: JN_Join_distrib JN_constant)

    (*Used to prove guarantees_JN_I*)
    lemma JN_Join_diff: "i ∈ I ==> F i\<squnion>JOIN (I - {i}) F = JOIN I F"
    apply (unfold JOIN_def Join_def)
    apply (rule program_equalityI, auto)
    done

    subsection{*Safety: co, stable, FP*}

    (*Fails if I={} because it collapses to SKIP ∈ A co B, i.e. to A ⊆ B.  So an
      alternative precondition is A ⊆ B, but most proofs using this rule require
      I to be nonempty for other reasons anyway.*)
    lemma JN_constrains:
        "i ∈ I ==> (\<Squnion>i ∈ I. F i) ∈ A co B = (∀i ∈ I. F i ∈ A co B)"
    by (simp add: constrains_def JOIN_def, blast)

    lemma Join_constrains [simp]:
         "(F\<squnion>G ∈ A co B) = (F ∈ A co B & G ∈ A co B)"
    by (auto simp add: constrains_def Join_def)

    lemma Join_unless [simp]:
         "(F\<squnion>G ∈ A unless B) = (F ∈ A unless B & G ∈ A unless B)"
    by (simp add: Join_constrains unless_def)

    (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
      reachable (F\<squnion>G) could be much bigger than reachable F, reachable G
    *)

    lemma Join_constrains_weaken:
         "[| F ∈ A co A';  G ∈ B co B' |]
          ==> F\<squnion>G ∈ (A ∩ B) co (A' ∪ B')"
    by (simp, blast intro: constrains_weaken)

    (*If I={}, it degenerates to SKIP ∈ UNIV co {}, which is false.*)
    lemma JN_constrains_weaken:
         "[| ∀i ∈ I. F i ∈ A i co A' i;  i ∈ I |]
          ==> (\<Squnion>i ∈ I. F i) ∈ (\<Inter>i ∈ I. A i) co (\<Union>i ∈ I. A' i)"
    apply (simp (no_asm_simp) add: JN_constrains)
    apply (blast intro: constrains_weaken)
    done

    lemma JN_stable: "(\<Squnion>i ∈ I. F i) ∈ stable A = (∀i ∈ I. F i ∈ stable A)"
    by (simp add: stable_def constrains_def JOIN_def)

    lemma invariant_JN_I:
         "[| !!i. i ∈ I ==> F i ∈ invariant A;  i ∈ I |]
           ==> (\<Squnion>i ∈ I. F i) ∈ invariant A"
    by (simp add: invariant_def JN_stable, blast)

    lemma Join_stable [simp]:
         "(F\<squnion>G ∈ stable A) =
          (F ∈ stable A & G ∈ stable A)"
    by (simp add: stable_def)

    lemma Join_increasing [simp]:
         "(F\<squnion>G ∈ increasing f) =
          (F ∈ increasing f & G ∈ increasing f)"
    by (simp add: increasing_def Join_stable, blast)

    lemma invariant_JoinI:
         "[| F ∈ invariant A; G ∈ invariant A |]
          ==> F\<squnion>G ∈ invariant A"
    by (simp add: invariant_def, blast)

    lemma FP_JN: "FP (\<Squnion>i ∈ I. F i) = (\<Inter>i ∈ I. FP (F i))"
    by (simp add: FP_def JN_stable INTER_def)

    subsection{*Progress: transient, ensures*}

    lemma JN_transient:
         "i ∈ I ==>
        (\<Squnion>i ∈ I. F i) ∈ transient A = (∃i ∈ I. F i ∈ transient A)"
    by (auto simp add: transient_def JOIN_def)

    lemma Join_transient [simp]:
         "F\<squnion>G ∈ transient A =
          (F ∈ transient A | G ∈ transient A)"
    by (auto simp add: bex_Un transient_def Join_def)

    lemma Join_transient_I1: "F ∈ transient A ==> F\<squnion>G ∈ transient A"
    by (simp add: Join_transient)

    lemma Join_transient_I2: "G ∈ transient A ==> F\<squnion>G ∈ transient A"
    by (simp add: Join_transient)

    (*If I={} it degenerates to (SKIP ∈ A ensures B) = False, i.e. to ~(A ⊆ B) *)
    lemma JN_ensures:
         "i ∈ I ==>
          (\<Squnion>i ∈ I. F i) ∈ A ensures B =
          ((∀i ∈ I. F i ∈ (A-B) co (A ∪ B)) & (∃i ∈ I. F i ∈ A ensures B))"
    by (auto simp add: ensures_def JN_constrains JN_transient)

    lemma Join_ensures:
         "F\<squnion>G ∈ A ensures B =
          (F ∈ (A-B) co (A ∪ B) & G ∈ (A-B) co (A ∪ B) &
           (F ∈ transient (A-B) | G ∈ transient (A-B)))"
    by (auto simp add: ensures_def Join_transient)

    lemma stable_Join_constrains:
        "[| F ∈ stable A;  G ∈ A co A' |]
         ==> F\<squnion>G ∈ A co A'"
    apply (unfold stable_def constrains_def Join_def)
    apply (simp add: ball_Un, blast)
    done

    (*Premise for G cannot use Always because  F ∈ Stable A  is weaker than
      G ∈ stable A *)
    lemma stable_Join_Always1:
         "[| F ∈ stable A;  G ∈ invariant A |] ==> F\<squnion>G ∈ Always A"
    apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable)
    apply (force intro: stable_Int)
    done

    (*As above, but exchanging the roles of F and G*)
    lemma stable_Join_Always2:
         "[| F ∈ invariant A;  G ∈ stable A |] ==> F\<squnion>G ∈ Always A"
    apply (subst Join_commute)
    apply (blast intro: stable_Join_Always1)
    done

    lemma stable_Join_ensures1:
         "[| F ∈ stable A;  G ∈ A ensures B |] ==> F\<squnion>G ∈ A ensures B"
    apply (simp (no_asm_simp) add: Join_ensures)
    apply (simp add: stable_def ensures_def)
    apply (erule constrains_weaken, auto)
    done

    (*As above, but exchanging the roles of F and G*)
    lemma stable_Join_ensures2:
         "[| F ∈ A ensures B;  G ∈ stable A |] ==> F\<squnion>G ∈ A ensures B"
    apply (subst Join_commute)
    apply (blast intro: stable_Join_ensures1)
    done

    subsection{*the ok and OK relations*}

    lemma ok_SKIP1 [iff]: "SKIP ok F"
    by (simp add: ok_def)

    lemma ok_SKIP2 [iff]: "F ok SKIP"
    by (simp add: ok_def)

    lemma ok_Join_commute:
         "(F ok G & (F\<squnion>G) ok H) = (G ok H & F ok (G\<squnion>H))"
    by (auto simp add: ok_def)

    lemma ok_commute: "(F ok G) = (G ok F)"
    by (auto simp add: ok_def)

    lemmas ok_sym = ok_commute [THEN iffD1, standard]

    lemma ok_iff_OK:
         "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)"
    apply (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb
                  all_conj_distrib)
    apply blast
    done

    lemma ok_Join_iff1 [iff]: "F ok (G\<squnion>H) = (F ok G & F ok H)"
    by (auto simp add: ok_def)

    lemma ok_Join_iff2 [iff]: "(G\<squnion>H) ok F = (G ok F & H ok F)"
    by (auto simp add: ok_def)

    (*useful?  Not with the previous two around*)
    lemma ok_Join_commute_I: "[| F ok G; (F\<squnion>G) ok H |] ==> F ok (G\<squnion>H)"
    by (auto simp add: ok_def)

    lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (∀i ∈ I. F ok G i)"
    by (auto simp add: ok_def)

    lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F =  (∀i ∈ I. G i ok F)"
    by (auto simp add: ok_def)

    lemma OK_iff_ok: "OK I F = (∀i ∈ I. ∀j ∈ I-{i}. (F i) ok (F j))"
    by (auto simp add: ok_def OK_def)

    lemma OK_imp_ok: "[| OK I F; i ∈ I; j ∈ I; i ≠ j|] ==> (F i) ok (F j)"
    by (auto simp add: OK_iff_ok)

    subsection{*Allowed*}

    lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
    by (auto simp add: Allowed_def)

    lemma Allowed_Join [simp]: "Allowed (F\<squnion>G) = Allowed F ∩ Allowed G"
    by (auto simp add: Allowed_def)

    lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\<Inter>i ∈ I. Allowed (F i))"
    by (auto simp add: Allowed_def)

    lemma ok_iff_Allowed: "F ok G = (F ∈ Allowed G & G ∈ Allowed F)"
    by (simp add: ok_def Allowed_def)

    lemma OK_iff_Allowed: "OK I F = (∀i ∈ I. ∀j ∈ I-{i}. F i ∈ Allowed(F j))"
    by (auto simp add: OK_iff_ok ok_iff_Allowed)

    subsection{*@{term safety_prop}, for reasoning about
     given instances of "ok"*}

    lemma safety_prop_Acts_iff:
         "safety_prop X ==> (Acts G ⊆ insert Id (UNION X Acts)) = (G ∈ X)"
    by (auto simp add: safety_prop_def)

    lemma safety_prop_AllowedActs_iff_Allowed:
         "safety_prop X ==> (UNION X Acts ⊆ AllowedActs F) = (X ⊆ Allowed F)"
    by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric])

    lemma Allowed_eq:
         "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X"
    by (simp add: Allowed_def safety_prop_Acts_iff)

    (*For safety_prop to hold, the property must be satisfiable!*)
    lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A ⊆ B)"
    by (simp add: safety_prop_def constrains_def, blast)

    lemma safety_prop_stable [iff]: "safety_prop (stable A)"
    by (simp add: stable_def)

    lemma safety_prop_Int [simp]:
         "[| safety_prop X; safety_prop Y |] ==> safety_prop (X ∩ Y)"
    by (simp add: safety_prop_def, blast)

    lemma safety_prop_INTER1 [simp]:
         "(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)"
    by (auto simp add: safety_prop_def, blast)

    lemma safety_prop_INTER [simp]:
         "(!!i. i ∈ I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i ∈ I. X i)"
    by (auto simp add: safety_prop_def, blast)

    lemma def_prg_Allowed:
         "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]
          ==> Allowed F = X"
    by (simp add: Allowed_eq)

    lemma Allowed_totalize [simp]: "Allowed (totalize F) = Allowed F"
    by (simp add: Allowed_def)

    lemma def_total_prg_Allowed:
         "[| F == mk_total_program (init, acts, UNION X Acts) ; safety_prop X |]
          ==> Allowed F = X"
    by (simp add: mk_total_program_def def_prg_Allowed)

    lemma def_UNION_ok_iff:
         "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]
          ==> F ok G = (G ∈ X & acts ⊆ AllowedActs G)"
    by (auto simp add: ok_def safety_prop_Acts_iff)

    text{*The union of two total programs is total.*}
    lemma totalize_Join: "totalize F\<squnion>totalize G = totalize (F\<squnion>G)"
    by (simp add: program_equalityI totalize_def Join_def image_Un)

    lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F\<squnion>G)"
    by (simp add: all_total_def, blast)

    lemma totalize_JN: "(\<Squnion>i ∈ I. totalize (F i)) = totalize(\<Squnion>i ∈ I. F i)"
    by (simp add: program_equalityI totalize_def JOIN_def image_UN)

    lemma all_total_JN: "(!!i. i∈I ==> all_total (F i)) ==> all_total(\<Squnion>i∈I. F i)"
    by (simp add: all_total_iff_totalize totalize_JN [symmetric])

    end

### SKIP

lemma Init_SKIP:

      Init SKIP = UNIV

lemma Acts_SKIP:

      Acts SKIP = {Id}

lemma AllowedActs_SKIP:

      AllowedActs SKIP = UNIV

lemma reachable_SKIP:

      reachable SKIP = UNIV

### SKIP and safety properties

lemma SKIP_in_constrains_iff:

      (SKIP ∈ A co B) = (A ⊆ B)

lemma SKIP_in_Constrains_iff:

      (SKIP ∈ A Co B) = (A ⊆ B)

lemma SKIP_in_stable:

      SKIP ∈ stable A

### Join

lemma Init_Join:

      Init (F Join G) = Init F ∩ Init G

lemma Acts_Join:

      Acts (F Join G) = Acts F ∪ Acts G

lemma AllowedActs_Join:

      AllowedActs (F Join G) = AllowedActs F ∩ AllowedActs G

### JN

lemma JN_empty:

      JOIN {} F = SKIP

lemma JN_insert:

      JOIN (insert a I) F = F a Join JOIN I F

lemma Init_JN:

      Init (JOIN I F) = (INT i:I. Init (F i))

lemma Acts_JN:

      Acts (JOIN I F) = insert Id (UN i:I. Acts (F i))

lemma AllowedActs_JN:

      AllowedActs (JOIN I F) = (INT i:I. AllowedActs (F i))

lemma JN_cong:

      [| I = J; !!i. i ∈ J ==> F i = G i |] ==> JOIN I F = JOIN J G

### Algebraic laws

lemma Join_commute:

      F Join G = G Join F

lemma Join_assoc:

      F Join G Join H = F Join (G Join H)

lemma Join_left_commute:

      A Join (B Join C) = B Join (A Join C)

lemma Join_SKIP_left:

      SKIP Join F = F

lemma Join_SKIP_right:

      F Join SKIP = F

lemma Join_absorb:

      F Join F = F

lemma Join_left_absorb:

      F Join (F Join G) = F Join G

lemmas Join_ac:

      F Join G Join H = F Join (G Join H)

      F Join (F Join G) = F Join G

      F Join G = G Join F

      A Join (B Join C) = B Join (A Join C)

lemmas Join_ac:

      F Join G Join H = F Join (G Join H)

      F Join (F Join G) = F Join G

      F Join G = G Join F

      A Join (B Join C) = B Join (A Join C)

### Laws Governing @{text "\<Squnion>"}

lemma JN_absorb:

      k ∈ I ==> F k Join JOIN I F = JOIN I F

lemma JN_Un:

      JOIN (I ∪ J) F = JOIN I F Join JOIN J F

lemma JN_constant:

      (JN i:I. c) = (if I = {} then SKIP else c)

lemma JN_Join_distrib:

      (JN i:I. F i Join G i) = JOIN I F Join JOIN I G

lemma JN_Join_miniscope:

      i ∈ I ==> (JN i:I. F i Join G) = JOIN I F Join G

lemma JN_Join_diff:

      i ∈ I ==> F i Join JOIN (I - {i}) F = JOIN I F

### Safety: co, stable, FP

lemma JN_constrains:

      i ∈ I ==> (JOIN I F ∈ A co B) = (∀i∈I. F i ∈ A co B)

lemma Join_constrains:

      (F Join G ∈ A co B) = (F ∈ A co B ∧ G ∈ A co B)

lemma Join_unless:

      (F Join G ∈ A unless B) = (F ∈ A unless B ∧ G ∈ A unless B)

lemma Join_constrains_weaken:

      [| F ∈ A co A'; G ∈ B co B' |] ==> F Join G ∈ A ∩ B co A' ∪ B'

lemma JN_constrains_weaken:

      [| ∀i∈I. F i ∈ A i co A' i; i ∈ I |]
      ==> JOIN I F ∈ (INT i:I. A i) co (UN i:I. A' i)

lemma JN_stable:

      (JOIN I F ∈ stable A) = (∀i∈I. F i ∈ stable A)

lemma invariant_JN_I:

      [| !!i. i ∈ I ==> F i ∈ invariant A; i ∈ I |] ==> JOIN I F ∈ invariant A

lemma Join_stable:

      (F Join G ∈ stable A) = (F ∈ stable A ∧ G ∈ stable A)

lemma Join_increasing:

      (F Join G ∈ increasing f) = (F ∈ increasing f ∧ G ∈ increasing f)

lemma invariant_JoinI:

      [| F ∈ invariant A; G ∈ invariant A |] ==> F Join G ∈ invariant A

lemma FP_JN:

      FP (JOIN I F) = (INT i:I. FP (F i))

### Progress: transient, ensures

lemma JN_transient:

      i ∈ I ==> (JOIN I F ∈ transient A) = (∃i∈I. F i ∈ transient A)

lemma Join_transient:

      (F Join G ∈ transient A) = (F ∈ transient A ∨ G ∈ transient A)

lemma Join_transient_I1:

      F ∈ transient A ==> F Join G ∈ transient A

lemma Join_transient_I2:

      G ∈ transient A ==> F Join G ∈ transient A

lemma JN_ensures:

      i ∈ I
      ==> (JOIN I F ∈ A ensures B) =
          ((∀i∈I. F i ∈ A - B co A ∪ B) ∧ (∃i∈I. F i ∈ A ensures B))

lemma Join_ensures:

      (F Join G ∈ A ensures B) =
      (F ∈ A - B co A ∪ B ∧
       G ∈ A - B co A ∪ B ∧ (F ∈ transient (A - B) ∨ G ∈ transient (A - B)))

lemma stable_Join_constrains:

      [| F ∈ stable A; G ∈ A co A' |] ==> F Join G ∈ A co A'

lemma stable_Join_Always1:

      [| F ∈ stable A; G ∈ invariant A |] ==> F Join G ∈ Always A

lemma stable_Join_Always2:

      [| F ∈ invariant A; G ∈ stable A |] ==> F Join G ∈ Always A

lemma stable_Join_ensures1:

      [| F ∈ stable A; G ∈ A ensures B |] ==> F Join G ∈ A ensures B

lemma stable_Join_ensures2:

      [| F ∈ A ensures B; G ∈ stable A |] ==> F Join G ∈ A ensures B

### the ok and OK relations

lemma ok_SKIP1:

      SKIP ok F

lemma ok_SKIP2:

      F ok SKIP

lemma ok_Join_commute:

      (F ok G ∧ F Join G ok H) = (G ok H ∧ F ok (G Join H))

lemma ok_commute:

      F ok G = G ok F

lemmas ok_sym:

      F ok G ==> G ok F

lemmas ok_sym:

      F ok G ==> G ok F

lemma ok_iff_OK:

      OK {(0, F), (1, G), (2, H)} snd = (F ok G ∧ F Join G ok H)

lemma ok_Join_iff1:

      F ok (G Join H) = (F ok G ∧ F ok H)

lemma ok_Join_iff2:

      G Join H ok F = (G ok F ∧ H ok F)

lemma ok_Join_commute_I:

      [| F ok G; F Join G ok H |] ==> F ok (G Join H)

lemma ok_JN_iff1:

      F ok JOIN I G = (∀i∈I. F ok G i)

lemma ok_JN_iff2:

      JOIN I G ok F = (∀i∈I. G i ok F)

lemma OK_iff_ok:

      OK I F = (∀i∈I. ∀j∈I - {i}. F i ok F j)

lemma OK_imp_ok:

      [| OK I F; i ∈ I; j ∈ I; i ≠ j |] ==> F i ok F j

### Allowed

lemma Allowed_SKIP:

      Allowed SKIP = UNIV

lemma Allowed_Join:

      Allowed (F Join G) = Allowed F ∩ Allowed G

lemma Allowed_JN:

      Allowed (JOIN I F) = (INT i:I. Allowed (F i))

lemma ok_iff_Allowed:

      F ok G = (F ∈ Allowed G ∧ G ∈ Allowed F)

lemma OK_iff_Allowed:

      OK I F = (∀i∈I. ∀j∈I - {i}. F i ∈ Allowed (F j))

### @{term safety_prop}, for reasoning about given instances of "ok"

lemma safety_prop_Acts_iff:

      safety_prop X ==> (Acts G ⊆ insert Id (UNION X Acts)) = (G ∈ X)

lemma safety_prop_AllowedActs_iff_Allowed:

      safety_prop X ==> (UNION X Acts ⊆ AllowedActs F) = (X ⊆ Allowed F)

lemma Allowed_eq:

      safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X

lemma safety_prop_constrains:

      safety_prop (A co B) = (A ⊆ B)

lemma safety_prop_stable:

      safety_prop (stable A)

lemma safety_prop_Int:

      [| safety_prop X; safety_prop Y |] ==> safety_prop (X ∩ Y)

lemma safety_prop_INTER1:

      (!!i. safety_prop (X i)) ==> safety_prop (INT i. X i)

lemma safety_prop_INTER:

      (!!i. i ∈ I ==> safety_prop (X i)) ==> safety_prop (INT i:I. X i)

lemma def_prg_Allowed:

      [| F == mk_program (init, acts, UNION X Acts); safety_prop X |]
      ==> Allowed F = X

lemma Allowed_totalize:

      Allowed (totalize F) = Allowed F

lemma def_total_prg_Allowed:

      [| F == mk_total_program (init, acts, UNION X Acts); safety_prop X |]
      ==> Allowed F = X

lemma def_UNION_ok_iff:

      [| F == mk_program (init, acts, UNION X Acts); safety_prop X |]
      ==> F ok G = (G ∈ X ∧ acts ⊆ AllowedActs G)

lemma totalize_Join:

      totalize F Join totalize G = totalize (F Join G)

lemma all_total_Join:

      [| all_total F; all_total G |] ==> all_total (F Join G)

lemma totalize_JN:

      (JN i:I. totalize (F i)) = totalize (JOIN I F)

lemma all_total_JN:

      (!!i. i ∈ I ==> all_total (F i)) ==> all_total (JOIN I F)