Quelle Comp.thy Sprache: Isabelle

(*  Title:      ZF/UNITY/Comp.thy
    Author:     Sidi O Ehmety, Computer Laboratory
    Copyright   1998  University of Cambridge

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

Revised by Sidi Ehmety on January  2001

Added: a strong form of the order relation over component and localize

Theory ported from HOL.

*)

section\<open>Composition\<close>

theory Comp imports Union Increasing begin

definition
  component :: "[i,i]\o" (infixl \component\ 65) where
  "F component H \ (\G. F \ G = H)"

definition
  strict_component :: "[i,i]\o" (infixl \strict'_component\ 65) where
  "F strict_component H \ F component H \ F\H"

definition
  (* A stronger form of the component relation *)
  component_of :: "[i,i]\o" (infixl \component'_of\ 65) where
  "F component_of H \ (\G. F ok G \ F \ G = H)"

definition
  strict_component_of :: "[i,i]\o" (infixl \strict'_component'_of\ 65) where
  "F strict_component_of H \ F component_of H \ F\H"

definition
  (* Preserves a state function f, in particular a variable *)
  preserves :: "(i\i)\i" where
  "preserves(f) \ {F:program. \z. F: stable({s:state. f(s) = z})}"

definition
  fun_pair :: "[i\i, i \i] \(i\i)" where
  "fun_pair(f, g) \ \x. "

definition
  localize  :: "[i\i, i] \ i" where
  "localize(f,F) \ mk_program(Init(F), Acts(F),
                       AllowedActs(F) \<inter> (\<Union>G\<in>preserves(f). Acts(G)))"


(*** component and strict_component relations ***)

lemma componentI:
     "H component F | H component G \ H component (F \ G)"
apply (unfold component_def, auto)
apply (rule_tac x = "Ga \ G" in exI)
apply (rule_tac [2] x = "G \ F" in exI)
apply (auto simp add: Join_ac)
done

lemma component_eq_subset:
     "G \ program \ (F component G) \
   (Init(G) \<subseteq> Init(F) \<and> Acts(F) \<subseteq> Acts(G) \<and> AllowedActs(G) \<subseteq> AllowedActs(F))"
apply (unfold component_def, auto)
apply (rule exI)
apply (rule program_equalityI, auto)
done

lemma component_SKIP [simp]: "F \ program \ SKIP component F"
  unfolding component_def
apply (rule_tac x = F in exI)
apply (force intro: Join_SKIP_left)
done

lemma component_refl [simp]: "F \ program \ F component F"
  unfolding component_def
apply (rule_tac x = F in exI)
apply (force intro: Join_SKIP_right)
done

lemma SKIP_minimal: "F component SKIP \ programify(F) = SKIP"
apply (rule program_equalityI)
apply (simp_all add: component_eq_subset, blast)
done

lemma component_Join1: "F component (F \ G)"
by (unfold component_def, blast)

lemma component_Join2: "G component (F \ G)"
  unfolding component_def
apply (simp (no_asm) add: Join_commute)
apply blast
done

lemma Join_absorb1: "F component G \ F \ G = G"
by (auto simp add: component_def Join_left_absorb)

lemma Join_absorb2: "G component F \ F \ G = F"
by (auto simp add: Join_ac component_def)

lemma JOIN_component_iff:
     "H \ program\(JOIN(I,F) component H) \ (\i \ I. F(i) component H)"
apply (case_tac "I=0", force)
apply (simp (no_asm_simp) add: component_eq_subset)
apply auto
apply blast
apply (rename_tac "y")
apply (drule_tac c = y and A = "AllowedActs (H)" in subsetD)
apply (blast elim!: not_emptyE)+
done

lemma component_JOIN: "i \ I \ F(i) component (\i \ I. (F(i)))"
  unfolding component_def
apply (blast intro: JOIN_absorb)
done

lemma component_trans: "\F component G; G component H\ \ F component H"
  unfolding component_def
apply (blast intro: Join_assoc [symmetric])
done

lemma component_antisym:
     "\F \ program; G \ program\ \(F component G \ G component F) \ F = G"
apply (simp (no_asm_simp) add: component_eq_subset)
apply clarify
apply (rule program_equalityI, auto)
done

lemma Join_component_iff:
     "H \ program \
      ((F \<squnion> G) component H) \<longleftrightarrow> (F component H \<and> G component H)"
apply (simp (no_asm_simp) add: component_eq_subset)
apply blast
done

lemma component_constrains:
     "\F component G; G \ A co B; F \ program\ \ F \ A co B"
apply (frule constrainsD2)
apply (auto simp add: constrains_def component_eq_subset)
done

(*** preserves ***)

lemma preserves_is_safety_prop [simp]: "safety_prop(preserves(f))"
  unfolding preserves_def safety_prop_def
apply (auto dest: ActsD simp add: stable_def constrains_def)
apply (drule_tac c = act in subsetD, auto)
done

lemma preservesI [rule_format]:
     "\z. F \ stable({s \ state. f(s) = z}) \ F \ preserves(f)"
apply (auto simp add: preserves_def)
apply (blast dest: stableD2)
done

lemma preserves_imp_eq:
     "\F \ preserves(f); act \ Acts(F); \s,t\ \ act\ \ f(s) = f(t)"
  unfolding preserves_def stable_def constrains_def
apply (subgoal_tac "s \ state \ t \ state")
prefer 2 apply (blast dest!: Acts_type [THEN subsetD], force)
done

lemma Join_preserves [iff]:
"(F \ G \ preserves(v)) \
      (programify(F) \<in> preserves(v) \<and> programify(G) \<in> preserves(v))"
by (auto simp add: preserves_def INT_iff)

lemma JOIN_preserves [iff]:
     "(JOIN(I,F): preserves(v)) \ (\i \ I. programify(F(i)):preserves(v))"
by (auto simp add: JOIN_stable preserves_def INT_iff)

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

lemma fun_pair_apply [simp]: "fun_pair(f,g,x) = "
  unfolding fun_pair_def
apply (simp (no_asm))
done

lemma preserves_fun_pair:
     "preserves(fun_pair(v,w)) = preserves(v) \ preserves(w)"
apply (rule equalityI)
apply (auto simp add: preserves_def stable_def constrains_def, blast+)
done

lemma preserves_fun_pair_iff [iff]:
     "F \ preserves(fun_pair(v, w)) \ F \ preserves(v) \ preserves(w)"
by (simp add: preserves_fun_pair)

lemma fun_pair_comp_distrib:
     "(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)"
by (simp add: fun_pair_def metacomp_def)

lemma comp_apply [simp]: "(f comp g)(x) = f(g(x))"
by (simp add: metacomp_def)

lemma preserves_type: "preserves(v)<=program"
by (unfold preserves_def, auto)

lemma preserves_into_program [TC]: "F \ preserves(f) \ F \ program"
by (blast intro: preserves_type [THEN subsetD])

lemma subset_preserves_comp: "preserves(f) \ preserves(g comp f)"
apply (auto simp add: preserves_def stable_def constrains_def)
apply (drule_tac x = "f (xb)" in spec)
apply (drule_tac x = act in bspec, auto)
done

lemma imp_preserves_comp: "F \ preserves(f) \ F \ preserves(g comp f)"
by (blast intro: subset_preserves_comp [THEN subsetD])

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

lemma preserves_imp_stable:
     "F \ preserves(f) \ F \ stable({s \ state. P(f(s))})"
by (blast intro: preserves_subset_stable [THEN subsetD])

lemma preserves_imp_increasing:
"\F \ preserves(f); \x \ state. f(x):A\ \ F \ Increasing.increasing(A, r, f)"
  unfolding Increasing.increasing_def
apply (auto intro: preserves_into_program)
apply (rule_tac P = "\x. \k, x\:r" in preserves_imp_stable, auto)
done

lemma preserves_id_subset_stable:
"st_set(A) \ preserves(\x. x) \ stable(A)"
apply (unfold preserves_def stable_def constrains_def, auto)
apply (drule_tac x = xb in spec)
apply (drule_tac x = act in bspec)
apply (auto dest: ActsD)
done

lemma preserves_id_imp_stable:
     "\F \ preserves(\x. x); st_set(A)\ \ F \ stable(A)"
by (blast intro: preserves_id_subset_stable [THEN subsetD])

(** Added by Sidi **)
(** component_of **)

(*  component_of is stronger than component *)
lemma component_of_imp_component:
"F component_of H \ F component H"
apply (unfold component_def component_of_def, blast)
done

(* component_of satisfies many of component's properties *)
lemma component_of_refl [simp]: "F \ program \ F component_of F"
  unfolding component_of_def
apply (rule_tac x = SKIP in exI, auto)
done

lemma component_of_SKIP [simp]: "F \ program \SKIP component_of F"
apply (unfold component_of_def, auto)
apply (rule_tac x = F in exI, auto)
done

lemma component_of_trans:
     "\F component_of G; G component_of H\ \ F component_of H"
  unfolding component_of_def
apply (blast intro: Join_assoc [symmetric])
done

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

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

lemma localize_AllowedActs_eq [simp]:
"AllowedActs(localize(v,F)) = AllowedActs(F) \ (\G \ preserves(v). Acts(G))"
  unfolding localize_def
apply (rule equalityI)
apply (auto dest: Acts_type [THEN subsetD])
done

(** Theorems used in ClientImpl **)

lemma stable_localTo_stable2:
"\F \ stable({s \ state. P(f(s), g(s))}); G \ preserves(f); G \ preserves(g)\
      \<Longrightarrow> F \<squnion> G \<in> stable({s \<in> state. P(f(s), g(s))})"
apply (auto dest: ActsD preserves_into_program simp add: stable_def constrains_def)
apply (case_tac "act \ Acts (F) ")
apply auto
apply (drule preserves_imp_eq)
apply (drule_tac [3] preserves_imp_eq, auto)
done

lemma Increasing_preserves_Stable:
     "\F \ stable({s \ state. :r}); G \ preserves(f);
         F \<squnion> G \<in> Increasing(A, r, g);
         \<forall>x \<in> state. f(x):A \<and> g(x):A\<rbrakk>
      \<Longrightarrow> F \<squnion> G \<in> Stable({s \<in> state. <f(s), g(s)>:r})"
apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
apply (simp_all add: constrains_type [THEN subsetD] preserves_type [THEN subsetD])
apply (blast intro: constrains_weaken)
(*The G case remains*)
apply (auto dest: ActsD simp add: preserves_def stable_def constrains_def ball_conj_distrib all_conj_distrib)
(*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 = "\k\A. \act \ Acts (F) . P (k,act)" for P in thin_rl)
apply (subgoal_tac "f (x) = f (xa) ")
apply (auto dest!: bspec)
done

(** Lemma used in AllocImpl **)

lemma Constrains_UN_left:
     "\\x \ I. F \ A(x) Co B; F \ program\ \ F:(\x \ I. A(x)) Co B"
by (unfold Constrains_def constrains_def, auto)

lemma stable_Join_Stable:
"\F \ stable({s \ state. P(f(s), g(s))});
     \<forall>k \<in> A. F \<squnion> G \<in> Stable({s \<in> state. P(k, g(s))});
     G \<in> preserves(f); \<forall>s \<in> state. f(s):A\<rbrakk>
  \<Longrightarrow> F \<squnion> G \<in> Stable({s \<in> state. P(f(s), g(s))})"
  unfolding stable_def Stable_def preserves_def
apply (rule_tac A = "(\k \ A. {s \ state. f(s)=k} \ {s \ state. P (f (s), g (s))})" in Constrains_weaken_L)
prefer 2 apply blast
apply (rule Constrains_UN_left, auto)
apply (rule_tac A = "{s \ state. f(s)=k} \ {s \ state. P (f (s), g (s))} \ {s \ state. P (k, g (s))}" and A' = "({s \ state. f(s)=k} \ {s \ state. P (f (s), g (s))}) \ {s \ state. P (k, g (s))}" in Constrains_weaken)
prefer 2 apply blast
prefer 2 apply blast
apply (rule Constrains_Int)
apply (rule constrains_imp_Constrains)
apply (auto simp add: constrains_type [THEN subsetD])
apply (blast intro: constrains_weaken)
apply (drule_tac x = k in spec)
apply (blast intro: constrains_weaken)
done

end

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.