Theory Comp

(*  Title:      HOL/UNITY/Comp.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Author:     Sidi Ehmety

Composition.

From Chandy and Sanders, "Reasoning About Program Composition",
Technical Report 2000-003, University of Florida, 2000.
*)

section‹Composition: Basic Primitives›

theory Comp
imports Union
begin

instantiation program :: (type) ord
begin

definition component_def: "F ≤ H ⟷ (∃G. F⊔G = H)"

definition strict_component_def: "F < (H::'a program) ⟷ (F ≤ H & F ≠ H)"

instance ..

end

definition component_of :: "'a program =>'a program=> bool" (infixl "component'_of" 50)
  where "F component_of H == ∃G. F ok G & F⊔G = H"

definition strict_component_of :: "'a program⇒'a program=> bool" (infixl "strict'_component'_of" 50)
  where "F strict_component_of H == F component_of H & F≠H"

definition preserves :: "('a=>'b) => 'a program set"
  where "preserves v == ⋂z. stable {s. v s = z}"

definition localize :: "('a=>'b) => 'a program => 'a program" where
  "localize v F == mk_program(Init F, Acts F,
                              AllowedActs F ∩ (⋃G ∈ preserves v. Acts G))"

definition funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
  where "funPair f g == %x. (f x, g x)"


subsection‹The component relation›
lemma componentI: "H ≤ F | H ≤ G ==> H ≤ (F⊔G)"
apply (unfold component_def, auto)
apply (rule_tac x = "G⊔Ga" in exI)
apply (rule_tac [2] x = "G⊔F" in exI)
apply (auto simp add: Join_ac)
done

lemma component_eq_subset:
     "(F ≤ G) =
      (Init G ⊆ Init F & Acts F ⊆ Acts G & AllowedActs G ⊆ AllowedActs F)"
apply (unfold component_def)
apply (force intro!: exI program_equalityI)
done

lemma component_SKIP [iff]: "SKIP ≤ F"
apply (unfold component_def)
apply (force intro: Join_SKIP_left)
done

lemma component_refl [iff]: "F ≤ (F :: 'a program)"
apply (unfold component_def)
apply (blast intro: Join_SKIP_right)
done

lemma SKIP_minimal: "F ≤ SKIP ==> F = SKIP"
by (auto intro!: program_equalityI simp add: component_eq_subset)

lemma component_Join1: "F ≤ (F⊔G)"
by (unfold component_def, blast)

lemma component_Join2: "G ≤ (F⊔G)"
apply (unfold component_def)
apply (simp add: Join_commute, blast)
done

lemma Join_absorb1: "F ≤ G ==> F⊔G = G"
by (auto simp add: component_def Join_left_absorb)

lemma Join_absorb2: "G ≤ F ==> F⊔G = F"
by (auto simp add: Join_ac component_def)

lemma JN_component_iff: "((JOIN I F) ≤ H) = (∀i ∈ I. F i ≤ H)"
by (simp add: component_eq_subset, blast)

lemma component_JN: "i ∈ I ==> (F i) ≤ (⨆i ∈ I. (F i))"
apply (unfold component_def)
apply (blast intro: JN_absorb)
done

lemma component_trans: "[| F ≤ G; G ≤ H |] ==> F ≤ (H :: 'a program)"
apply (unfold component_def)
apply (blast intro: Join_assoc [symmetric])
done

lemma component_antisym: "[| F ≤ G; G ≤ F |] ==> F = (G :: 'a program)"
apply (simp (no_asm_use) add: component_eq_subset)
apply (blast intro!: program_equalityI)
done

lemma Join_component_iff: "((F⊔G) ≤ H) = (F ≤ H & G ≤ H)"
by (simp add: component_eq_subset, blast)

lemma component_constrains: "[| F ≤ G; G ∈ A co B |] ==> F ∈ A co B"
by (auto simp add: constrains_def component_eq_subset)

lemma component_stable: "[| F ≤ G; G ∈ stable A |] ==> F ∈ stable A"
by (auto simp add: stable_def component_constrains)

(*Used in Guar.thy to show that programs are partially ordered*)
lemmas program_less_le = strict_component_def


subsection‹The preserves property›

lemma preservesI: "(!!z. F ∈ stable {s. v s = z}) ==> F ∈ preserves v"
by (unfold preserves_def, blast)

lemma preserves_imp_eq:
     "[| F ∈ preserves v;  act ∈ Acts F;  (s,s') ∈ act |] ==> v s = v s'"
by (unfold preserves_def stable_def constrains_def, force)

lemma Join_preserves [iff]:
     "(F⊔G ∈ preserves v) = (F ∈ preserves v & G ∈ preserves v)"
by (unfold preserves_def, auto)

lemma JN_preserves [iff]:
     "(JOIN I F ∈ preserves v) = (∀i ∈ I. F i ∈ preserves v)"
by (simp add: JN_stable preserves_def, blast)

lemma SKIP_preserves [iff]: "SKIP ∈ preserves v"
by (auto simp add: preserves_def)

lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)"
by (simp add:  funPair_def)

lemma preserves_funPair: "preserves (funPair v w) = preserves v ∩ preserves w"
by (auto simp add: preserves_def stable_def constrains_def, blast)

(* (F ∈ preserves (funPair v w)) = (F ∈ preserves v ∩ preserves w) *)
declare preserves_funPair [THEN eqset_imp_iff, iff]


lemma funPair_o_distrib: "(funPair f g) o h = funPair (f o h) (g o h)"
by (simp add: funPair_def o_def)

lemma fst_o_funPair [simp]: "fst o (funPair f g) = f"
by (simp add: funPair_def o_def)

lemma snd_o_funPair [simp]: "snd o (funPair f g) = g"
by (simp add: funPair_def o_def)

lemma subset_preserves_o: "preserves v ⊆ preserves (w o v)"
by (force simp add: preserves_def stable_def constrains_def)

lemma preserves_subset_stable: "preserves v ⊆ stable {s. P (v s)}"
apply (auto simp add: preserves_def stable_def constrains_def)
apply (rename_tac s' s)
apply (subgoal_tac "v s = v s'")
apply (force+)
done

lemma preserves_subset_increasing: "preserves v ⊆ increasing v"
by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def)

lemma preserves_id_subset_stable: "preserves id ⊆ stable A"
by (force simp add: preserves_def stable_def constrains_def)


(** For use with def_UNION_ok_iff **)

lemma safety_prop_preserves [iff]: "safety_prop (preserves v)"
by (auto intro: safety_prop_INTER1 simp add: preserves_def)


(** Some lemmas used only in Client.thy **)

lemma stable_localTo_stable2:
     "[| F ∈ stable {s. P (v s) (w s)};
         G ∈ preserves v;  G ∈ preserves w |]
      ==> F⊔G ∈ stable {s. P (v s) (w s)}"
apply simp
apply (subgoal_tac "G ∈ preserves (funPair v w) ")
 prefer 2 apply simp
apply (drule_tac P1 = "case_prod Q" for Q in preserves_subset_stable [THEN subsetD], 
       auto)
done

lemma Increasing_preserves_Stable:
     "[| F ∈ stable {s. v s ≤ w s};  G ∈ preserves v; F⊔G ∈ Increasing w |]
      ==> F⊔G ∈ Stable {s. v s ≤ w s}"
apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
apply (blast intro: constrains_weaken)
(*The G case remains*)
apply (auto simp add: preserves_def stable_def constrains_def)
(*We have a G-action, so delete assumptions about F-actions*)
apply (erule_tac V = "∀act ∈ Acts F. P act" for P in thin_rl)
apply (erule_tac V = "∀z. ∀act ∈ Acts F. P z act" for P in thin_rl)
apply (subgoal_tac "v x = v xa")
 apply auto
apply (erule order_trans, blast)
done

(** component_of **)

(*  component_of is stronger than ≤ *)
lemma component_of_imp_component: "F component_of H ==> F ≤ H"
by (unfold component_def component_of_def, blast)


(* component_of satisfies many of the same properties as ≤ *)
lemma component_of_refl [simp]: "F component_of F"
apply (unfold component_of_def)
apply (rule_tac x = SKIP in exI, auto)
done

lemma component_of_SKIP [simp]: "SKIP component_of F"
by (unfold component_of_def, auto)

lemma component_of_trans:
     "[| F component_of G; G component_of H |] ==> F component_of H"
apply (unfold component_of_def)
apply (blast intro: Join_assoc [symmetric])
done

lemmas strict_component_of_eq = strict_component_of_def

(** localize **)
lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
by (simp add: localize_def)

lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F"
by (simp add: localize_def)

lemma localize_AllowedActs_eq [simp]:
   "AllowedActs (localize v F) = AllowedActs F ∩ (⋃G ∈ preserves v. Acts G)"
by (unfold localize_def, auto)

end