Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Comp.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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\<open>Composition: Basic Primitives\<close>

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 \<inter> (\<Union>G \<in> preserves v. Acts G))"

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

subsection\<open>The component relation\<close>
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 \<subseteq> Init F & Acts F \<subseteq> Acts G & AllowedActs G \<subseteq> 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\<open>The preserves property\<close>

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 \<in> preserves (funPair v w)) = (F \<in> preserves v \<inter> 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 \<in> preserves v;  G \<in> preserves w |]
      ==> F\<squnion>G \<in> 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\<squnion>G \<in> Stable {s. v s \<le> 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 \<le> *)
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 \<le> *)
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

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.