Theory Union

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

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

section‹Unions of Programs›

theory Union imports SubstAx FP begin

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

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

definition
JOIN  :: "['a set, 'a => 'b program] => 'b program"
where "JOIN I F = mk_program (⋂i ∈ I. Init (F i), ⋃i ∈ I. Acts (F i),
⋂i ∈ I. AllowedActs (F i))"

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

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

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

syntax
"_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3⨆_./ _)" 10)
"_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3⨆_∈_./ _)" 10)
translations
"⨆x ∈ A. B" == "CONST JOIN A (λx. B)"
"⨆x y. B" == "⨆x. ⨆y. B"
"⨆x. B" == "CONST JOIN (CONST UNIV) (λx. B)"

subsection‹SKIP›

lemma Init_SKIP [simp]: "Init SKIP = UNIV"

lemma Acts_SKIP [simp]: "Acts SKIP = {Id}"

lemma AllowedActs_SKIP [simp]: "AllowedActs SKIP = UNIV"

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⊔G) = Init F ∩ Init G"

lemma Acts_Join [simp]: "Acts (F⊔G) = Acts F ∪ Acts G"

lemma AllowedActs_Join [simp]:
"AllowedActs (F⊔G) = AllowedActs F ∩ AllowedActs G"

subsection‹JN›

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

lemma JN_insert [simp]: "(⨆i ∈ insert a I. F i) = (F a)⊔(⨆i ∈ I. F i)"
apply (rule program_equalityI)
apply (auto simp add: JOIN_def Join_def)
done

lemma Init_JN [simp]: "Init (⨆i ∈ I. F i) = (⋂i ∈ I. Init (F i))"

lemma Acts_JN [simp]: "Acts (⨆i ∈ I. F i) = insert Id (⋃i ∈ I. Acts (F i))"

lemma AllowedActs_JN [simp]:
"AllowedActs (⨆i ∈ I. F i) = (⋂i ∈ I. AllowedActs (F i))"

lemma JN_cong [cong]:
"[| I=J;  !!i. i ∈ J ==> F i = G i |] ==> (⨆i ∈ I. F i) = (⨆i ∈ J. G i)"

subsection‹Algebraic laws›

lemma Join_commute: "F⊔G = G⊔F"
by (simp add: Join_def Un_commute Int_commute)

lemma Join_assoc: "(F⊔G)⊔H = F⊔(G⊔H)"
by (simp add: Un_ac Join_def Int_assoc insert_absorb)

lemma Join_left_commute: "A⊔(B⊔C) = B⊔(A⊔C)"
by (simp add: Un_ac Int_ac Join_def insert_absorb)

lemma Join_SKIP_left [simp]: "SKIP⊔F = F"
apply (unfold Join_def SKIP_def)
apply (rule program_equalityI)
done

lemma Join_SKIP_right [simp]: "F⊔SKIP = F"
apply (unfold Join_def SKIP_def)
apply (rule program_equalityI)
done

lemma Join_absorb [simp]: "F⊔F = F"
apply (unfold Join_def)
apply (rule program_equalityI, auto)
done

lemma Join_left_absorb: "F⊔(F⊔G) = F⊔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 ‹⨆››

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

lemma JN_Un: "(⨆i ∈ I ∪ J. F i) = ((⨆i ∈ I. F i)⊔(⨆i ∈ J. F i))"
by (auto intro!: program_equalityI)

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

lemma JN_Join_distrib:
"(⨆i ∈ I. F i⊔G i) = (⨆i ∈ I. F i) ⊔ (⨆i ∈ I. G i)"
by (auto intro!: program_equalityI)

lemma JN_Join_miniscope:
"i ∈ I ==> (⨆i ∈ I. F i⊔G) = ((⨆i ∈ I. F i)⊔G)"
by (auto simp add: JN_Join_distrib JN_constant)

(*Used to prove guarantees_JN_I*)
lemma JN_Join_diff: "i ∈ I ==> F i⊔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 ==> (⨆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⊔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⊔G ∈ A unless B) = (F ∈ A unless B & G ∈ A unless B)"

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

lemma Join_constrains_weaken:
"[| F ∈ A co A';  G ∈ B co B' |]
==> F⊔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 |]
==> (⨆i ∈ I. F i) ∈ (⋂i ∈ I. A i) co (⋃i ∈ I. A' i)"
apply (blast intro: constrains_weaken)
done

lemma JN_stable: "(⨆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 |]
==> (⨆i ∈ I. F i) ∈ invariant A"
by (simp add: invariant_def JN_stable, blast)

lemma Join_stable [simp]:
"(F⊔G ∈ stable A) =
(F ∈ stable A & G ∈ stable A)"

lemma Join_increasing [simp]:
"(F⊔G ∈ increasing f) =
(F ∈ increasing f & G ∈ increasing f)"

lemma invariant_JoinI:
"[| F ∈ invariant A; G ∈ invariant A |]
==> F⊔G ∈ invariant A"

lemma FP_JN: "FP (⨆i ∈ I. F i) = (⋂i ∈ I. FP (F i))"
by (simp add: FP_def JN_stable INTER_eq)

subsection‹Progress: transient, ensures›

lemma JN_transient:
"i ∈ I ==>
(⨆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⊔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⊔G ∈ transient A"
by simp

lemma Join_transient_I2: "G ∈ transient A ==> F⊔G ∈ transient A"
by simp

(*If I={} it degenerates to (SKIP ∈ A ensures B) = False, i.e. to ~(A ⊆ B) *)
lemma JN_ensures:
"i ∈ I ==>
(⨆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⊔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⊔G ∈ A co A'"
apply (unfold stable_def constrains_def Join_def)
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⊔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⊔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⊔G ∈ A ensures B"
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⊔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"

lemma ok_SKIP2 [iff]: "F ok SKIP"

lemma ok_Join_commute:
"(F ok G & (F⊔G) ok H) = (G ok H & F ok (G⊔H))"

lemma ok_commute: "(F ok G) = (G ok F)"

lemmas ok_sym = ok_commute [THEN iffD1]

lemma ok_iff_OK:
"OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F⊔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⊔H) = (F ok G & F ok H)"

lemma ok_Join_iff2 [iff]: "(G⊔H) ok F = (G ok F & H ok F)"

(*useful?  Not with the previous two around*)
lemma ok_Join_commute_I: "[| F ok G; (F⊔G) ok H |] ==> F ok (G⊔H)"

lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (∀i ∈ I. F ok G i)"

lemma ok_JN_iff2 [iff]: "(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))"
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)"

subsection‹Allowed›

lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"

lemma Allowed_Join [simp]: "Allowed (F⊔G) = Allowed F ∩ Allowed G"

lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (⋂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))"
by (auto simp add: OK_iff_ok ok_iff_Allowed)

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

(*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)"

lemma safety_prop_Int [simp]:
"safety_prop X ⟹ safety_prop Y ⟹ safety_prop (X ∩ Y)"
fix G
assume "∀G. Acts G ⊆ (⋃x∈X. Acts x) ⟶ G ∈ X"
then have X: "Acts G ⊆ (⋃x∈X. Acts x) ⟹ G ∈ X" by blast
assume "∀G. Acts G ⊆ (⋃x∈Y. Acts x) ⟶ G ∈ Y"
then have Y: "Acts G ⊆ (⋃x∈Y. Acts x) ⟹ G ∈ Y" by blast
assume Acts: "Acts G ⊆ (⋃x∈X ∩ Y. Acts x)"
with X and Y show "G ∈ X ∧ G ∈ Y" by auto
qed

lemma safety_prop_INTER [simp]:
"(⋀i. i ∈ I ⟹ safety_prop (X i)) ⟹ safety_prop (⋂i∈I. X i)"
fix G and i
assume "⋀i. i ∈ I ⟹ ⊥ ∈ X i ∧
(∀G. Acts G ⊆ (⋃x∈X i. Acts x) ⟶ G ∈ X i)"
then have *: "i ∈ I ⟹ Acts G ⊆ (⋃x∈X i. Acts x) ⟹ G ∈ X i"
by blast
assume "i ∈ I"
moreover assume "Acts G ⊆ (⋃j∈⋂i∈I. X i. Acts j)"
ultimately have "Acts G ⊆ (⋃i∈X i. Acts i)"
by auto
with * ‹i ∈ I› show "G ∈ X i" by blast
qed

lemma safety_prop_INTER1 [simp]:
"(⋀i. safety_prop (X i)) ⟹ safety_prop (⋂i. X i)"
by (rule safety_prop_INTER) simp

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

lemma Allowed_totalize [simp]: "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)"
by (auto simp add: ok_def safety_prop_Acts_iff)

text‹The union of two total programs is total.›
lemma totalize_Join: "totalize F⊔totalize G = totalize (F⊔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⊔G)"