(* Title: ZF/UNITY/Union.thy
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
Unions of programs
Partly from Misra's Chapter 5 \<in> Asynchronous Compositions of Programs
Theory ported form HOL..
*)
theory Union imports SubstAx FP
begin
definition
(*FIXME: conjoin Init(F) \<inter> Init(G) \<noteq> 0 *)
ok :: "[i, i] => o" (infixl \<open>ok\<close> 65) where
"F ok G == Acts(F) \ AllowedActs(G) &
Acts(G) \<subseteq> AllowedActs(F)"
definition
(*FIXME: conjoin (\<Inter>i \<in> I. Init(F(i))) \<noteq> 0 *)
OK :: "[i, i=>i] => o" where
"OK(I,F) == (\i \ I. \j \ I-{i}. Acts(F(i)) \ AllowedActs(F(j)))"
definition
JOIN :: "[i, i=>i] => i" where
"JOIN(I,F) == if I = 0 then SKIP else
mk_program(\<Inter>i \<in> I. Init(F(i)), \<Union>i \<in> I. Acts(F(i)),
\<Inter>i \<in> I. AllowedActs(F(i)))"
definition
Join :: "[i, i] => i" (infixl \<open>\<squnion>\<close> 65) where
"F \ G == mk_program (Init(F) \ Init(G), Acts(F) \ Acts(G),
AllowedActs(F) \<inter> AllowedActs(G))"
definition
(*Characterizes safety properties. Used with specifying AllowedActs*)
safety_prop :: "i => o" where
"safety_prop(X) == X\program &
SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)"
syntax
"_JOIN1" :: "[pttrns, i] => i" (\<open>(3\<Squnion>_./ _)\<close> 10)
"_JOIN" :: "[pttrn, i, i] => i" (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10)
translations
"\x \ A. B" == "CONST JOIN(A, (\x. B))"
"\x y. B" == "\x. \y. B"
"\x. B" == "CONST JOIN(CONST state, (\x. B))"
subsection\<open>SKIP\<close>
lemma reachable_SKIP [simp]: "reachable(SKIP) = state"
by (force elim: reachable.induct intro: reachable.intros)
text\<open>Elimination programify from ok and \<squnion>\<close>
lemma ok_programify_left [iff]: "programify(F) ok G \ F ok G"
by (simp add: ok_def)
lemma ok_programify_right [iff]: "F ok programify(G) \ F ok G"
by (simp add: ok_def)
lemma Join_programify_left [simp]: "programify(F) \ G = F \ G"
by (simp add: Join_def)
lemma Join_programify_right [simp]: "F \ programify(G) = F \ G"
by (simp add: Join_def)
subsection\<open>SKIP and safety properties\<close>
lemma SKIP_in_constrains_iff [iff]: "(SKIP \ A co B) \ (A\B & st_set(A))"
by (unfold constrains_def st_set_def, auto)
lemma SKIP_in_Constrains_iff [iff]: "(SKIP \ A Co B)\ (state \ A\B)"
by (unfold Constrains_def, auto)
lemma SKIP_in_stable [iff]: "SKIP \ stable(A) \ st_set(A)"
by (auto simp add: stable_def)
lemma SKIP_in_Stable [iff]: "SKIP \ Stable(A)"
by (unfold Stable_def, auto)
subsection\<open>Join and JOIN types\<close>
lemma Join_in_program [iff,TC]: "F \ G \ program"
by (unfold Join_def, auto)
lemma JOIN_in_program [iff,TC]: "JOIN(I,F) \ program"
by (unfold JOIN_def, auto)
subsection\<open>Init, Acts, and AllowedActs of Join and JOIN\<close>
lemma Init_Join [simp]: "Init(F \ G) = Init(F) \ Init(G)"
by (simp add: Int_assoc Join_def)
lemma Acts_Join [simp]: "Acts(F \ G) = Acts(F) \ Acts(G)"
by (simp add: Int_Un_distrib2 cons_absorb Join_def)
lemma AllowedActs_Join [simp]: "AllowedActs(F \ G) =
AllowedActs(F) \<inter> AllowedActs(G)"
apply (simp add: Int_assoc cons_absorb Join_def)
done
subsection\<open>Join's algebraic laws\<close>
lemma Join_commute: "F \ G = G \ F"
by (simp add: Join_def Un_commute Int_commute)
lemma Join_left_commute: "A \ (B \ C) = B \ (A \ C)"
apply (simp add: Join_def Int_Un_distrib2 cons_absorb)
apply (simp add: Un_ac Int_ac Int_Un_distrib2 cons_absorb)
done
lemma Join_assoc: "(F \ G) \ H = F \ (G \ H)"
by (simp add: Un_ac Join_def cons_absorb Int_assoc Int_Un_distrib2)
subsection\<open>Needed below\<close>
lemma cons_id [simp]: "cons(id(state), Pow(state * state)) = Pow(state*state)"
by auto
lemma Join_SKIP_left [simp]: "SKIP \ F = programify(F)"
apply (unfold Join_def SKIP_def)
apply (auto simp add: Int_absorb cons_eq)
done
lemma Join_SKIP_right [simp]: "F \ SKIP = programify(F)"
apply (subst Join_commute)
apply (simp add: Join_SKIP_left)
done
lemma Join_absorb [simp]: "F \ F = programify(F)"
by (rule program_equalityI, auto)
lemma Join_left_absorb: "F \ (F \ G) = F \ G"
by (simp add: Join_assoc [symmetric])
subsection\<open>Join is an AC-operator\<close>
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
subsection\<open>Eliminating programify form JOIN and OK expressions\<close>
lemma OK_programify [iff]: "OK(I, %x. programify(F(x))) \ OK(I, F)"
by (simp add: OK_def)
lemma JOIN_programify [iff]: "JOIN(I, %x. programify(F(x))) = JOIN(I, F)"
by (simp add: JOIN_def)
subsection\<open>JOIN\<close>
lemma JOIN_empty [simp]: "JOIN(0, F) = SKIP"
by (unfold JOIN_def, auto)
lemma Init_JOIN [simp]:
"Init(\i \ I. F(i)) = (if I=0 then state else (\i \ I. Init(F(i))))"
by (simp add: JOIN_def INT_extend_simps del: INT_simps)
lemma Acts_JOIN [simp]:
"Acts(JOIN(I,F)) = cons(id(state), \i \ I. Acts(F(i)))"
apply (unfold JOIN_def)
apply (auto simp del: INT_simps UN_simps)
apply (rule equalityI)
apply (auto dest: Acts_type [THEN subsetD])
done
lemma AllowedActs_JOIN [simp]:
"AllowedActs(\i \ I. F(i)) =
(if I=0 then Pow(state*state) else (\<Inter>i \<in> I. AllowedActs(F(i))))"
apply (unfold JOIN_def, auto)
apply (rule equalityI)
apply (auto elim!: not_emptyE dest: AllowedActs_type [THEN subsetD])
done
lemma JOIN_cons [simp]: "(\i \ cons(a,I). F(i)) = F(a) \ (\i \ I. F(i))"
by (rule program_equalityI, auto)
lemma JOIN_cong [cong]:
"[| I=J; !!i. i \ J ==> F(i) = G(i) |] ==>
(\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> J. G(i))"
by (simp add: JOIN_def)
subsection\<open>JOIN laws\<close>
lemma JOIN_absorb: "k \ I ==>F(k) \ (\i \ I. F(i)) = (\i \ I. F(i))"
apply (subst JOIN_cons [symmetric])
apply (auto simp add: cons_absorb)
done
lemma JOIN_Un: "(\i \ I \ J. F(i)) = ((\i \ I. F(i)) \ (\i \ J. F(i)))"
apply (rule program_equalityI)
apply (simp_all add: UN_Un INT_Un)
apply (simp_all del: INT_simps add: INT_extend_simps, blast)
done
lemma JOIN_constant: "(\i \ I. c) = (if I=0 then SKIP else programify(c))"
by (rule program_equalityI, auto)
lemma JOIN_Join_distrib:
"(\i \ I. F(i) \ G(i)) = (\i \ I. F(i)) \ (\i \ I. G(i))"
apply (rule program_equalityI)
apply (simp_all add: INT_Int_distrib, blast)
done
lemma JOIN_Join_miniscope: "(\i \ I. F(i) \ G) = ((\i \ I. F(i) \ G))"
by (simp add: JOIN_Join_distrib JOIN_constant)
text\<open>Used to prove guarantees_JOIN_I\<close>
lemma JOIN_Join_diff: "i \ I==>F(i) \ JOIN(I - {i}, F) = JOIN(I, F)"
apply (rule program_equalityI)
apply (auto elim!: not_emptyE)
done
subsection\<open>Safety: co, stable, FP\<close>
(*Fails if I=0 because it collapses to SKIP \<in> A co B, i.e. to A\<subseteq>B. So an
alternative precondition is A\<subseteq>B, but most proofs using this rule require
I to be nonempty for other reasons anyway.*)
lemma JOIN_constrains:
"i \ I==>(\i \ I. F(i)) \ A co B \ (\i \ I. programify(F(i)) \ A co B)"
apply (unfold constrains_def JOIN_def st_set_def, auto)
prefer 2 apply blast
apply (rename_tac j act y z)
apply (cut_tac F = "F (j) " in Acts_type)
apply (drule_tac x = act in bspec, auto)
done
lemma Join_constrains [iff]:
"(F \ G \ A co B) \ (programify(F) \ A co B & programify(G) \ A co B)"
by (auto simp add: constrains_def)
lemma Join_unless [iff]:
"(F \ G \ A unless B) \
(programify(F) \<in> A unless B & programify(G) \<in> 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 \<in> (A \<inter> B) co (A' \<union> B')"
apply (subgoal_tac "st_set (A) & st_set (B) & F \ program & G \ program")
prefer 2 apply (blast dest: constrainsD2, simp)
apply (blast intro: constrains_weaken)
done
(*If I=0, it degenerates to SKIP \<in> state co 0, which is false.*)
lemma JOIN_constrains_weaken:
assumes major: "(!!i. i \ I ==> F(i) \ A(i) co A'(i))"
and minor: "i \ I"
shows "(\i \ I. F(i)) \ (\i \ I. A(i)) co (\i \ I. A'(i))"
apply (cut_tac minor)
apply (simp (no_asm_simp) add: JOIN_constrains)
apply clarify
apply (rename_tac "j")
apply (frule_tac i = j in major)
apply (frule constrainsD2, simp)
apply (blast intro: constrains_weaken)
done
lemma JOIN_stable:
"(\i \ I. F(i)) \ stable(A) \ ((\i \ I. programify(F(i)) \ stable(A)) & st_set(A))"
apply (auto simp add: stable_def constrains_def JOIN_def)
apply (cut_tac F = "F (i) " in Acts_type)
apply (drule_tac x = act in bspec, auto)
done
lemma initially_JOIN_I:
assumes major: "(!!i. i \ I ==>F(i) \ initially(A))"
and minor: "i \ I"
shows "(\i \ I. F(i)) \ initially(A)"
apply (cut_tac minor)
apply (auto elim!: not_emptyE simp add: Inter_iff initially_def)
apply (frule_tac i = x in major)
apply (auto simp add: initially_def)
done
lemma invariant_JOIN_I:
assumes major: "(!!i. i \ I ==> F(i) \ invariant(A))"
and minor: "i \ I"
shows "(\i \ I. F(i)) \ invariant(A)"
apply (cut_tac minor)
apply (auto intro!: initially_JOIN_I dest: major simp add: invariant_def JOIN_stable)
apply (erule_tac V = "i \ I" in thin_rl)
apply (frule major)
apply (drule_tac [2] major)
apply (auto simp add: invariant_def)
apply (frule stableD2, force)+
done
lemma Join_stable [iff]:
" (F \ G \ stable(A)) \
(programify(F) \<in> stable(A) & programify(G) \<in> stable(A))"
by (simp add: stable_def)
lemma initially_JoinI [intro!]:
"[| F \ initially(A); G \ initially(A) |] ==> F \ G \ initially(A)"
by (unfold initially_def, auto)
lemma invariant_JoinI:
"[| F \ invariant(A); G \ invariant(A) |]
==> F \<squnion> G \<in> invariant(A)"
apply (subgoal_tac "F \ program&G \ program")
prefer 2 apply (blast dest: invariantD2)
apply (simp add: invariant_def)
apply (auto intro: Join_in_program)
done
(* Fails if I=0 because \<Inter>i \<in> 0. A(i) = 0 *)
lemma FP_JOIN: "i \ I ==> FP(\i \ I. F(i)) = (\i \ I. FP (programify(F(i))))"
by (auto simp add: FP_def Inter_def st_set_def JOIN_stable)
subsection\<open>Progress: transient, ensures\<close>
lemma JOIN_transient:
"i \ I ==>
(\<Squnion>i \<in> I. F(i)) \<in> transient(A) \<longleftrightarrow> (\<exists>i \<in> I. programify(F(i)) \<in> transient(A))"
apply (auto simp add: transient_def JOIN_def)
apply (unfold st_set_def)
apply (drule_tac [2] x = act in bspec)
apply (auto dest: Acts_type [THEN subsetD])
done
lemma Join_transient [iff]:
"F \ G \ transient(A) \
(programify(F) \<in> transient(A) | programify(G) \<in> transient(A))"
apply (auto simp add: transient_def Join_def Int_Un_distrib2)
done
lemma Join_transient_I1: "F \ transient(A) ==> F \ G \ transient(A)"
by (simp add: Join_transient transientD2)
lemma Join_transient_I2: "G \ transient(A) ==> F \ G \ transient(A)"
by (simp add: Join_transient transientD2)
(*If I=0 it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A\<subseteq>B) *)
lemma JOIN_ensures:
"i \ I ==>
(\<Squnion>i \<in> I. F(i)) \<in> A ensures B \<longleftrightarrow>
((\<forall>i \<in> I. programify(F(i)) \<in> (A-B) co (A \<union> B)) &
(\<exists>i \<in> I. programify(F(i)) \<in> A ensures B))"
by (auto simp add: ensures_def JOIN_constrains JOIN_transient)
lemma Join_ensures:
"F \ G \ A ensures B \
(programify(F) \<in> (A-B) co (A \<union> B) & programify(G) \<in> (A-B) co (A \<union> B) &
(programify(F) \<in> transient (A-B) | programify(G) \<in> transient (A-B)))"
apply (unfold ensures_def)
apply (auto simp add: Join_transient)
done
lemma stable_Join_constrains:
"[| F \ stable(A); G \ A co A' |]
==> F \<squnion> G \<in> A co A'"
apply (unfold stable_def constrains_def Join_def st_set_def)
apply (cut_tac F = F in Acts_type)
apply (cut_tac F = G in Acts_type, force)
done
(*Premise for G cannot use Always because F \<in> Stable A is
weaker than G \<in> stable A *)
lemma stable_Join_Always1:
"[| F \ stable(A); G \ invariant(A) |] ==> F \ G \ Always(A)"
apply (subgoal_tac "F \ program & G \ program & st_set (A) ")
prefer 2 apply (blast dest: invariantD2 stableD2)
apply (simp add: Always_def invariant_def initially_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 (subgoal_tac "F \ program & G \ program & st_set (A) ")
prefer 2 apply (blast dest: stableD2 ensures_type [THEN subsetD])
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 \ G \ A ensures B"
apply (subst Join_commute)
apply (blast intro: stable_Join_ensures1)
done
subsection\<open>The ok and OK relations\<close>
lemma ok_SKIP1 [iff]: "SKIP ok F"
by (auto dest: Acts_type [THEN subsetD] simp add: ok_def)
lemma ok_SKIP2 [iff]: "F ok SKIP"
by (auto dest: Acts_type [THEN subsetD] simp add: ok_def)
lemma ok_Join_commute:
"(F ok G & (F \ G) ok H) \ (G ok H & F ok (G \ 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]
lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) \ (F ok G & (F \ G) ok H)"
by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb
Int_Un_distrib2 Ball_def, safe, force+)
lemma ok_Join_iff1 [iff]: "F ok (G \ H) \ (F ok G & F ok H)"
by (auto simp add: ok_def)
lemma ok_Join_iff2 [iff]: "(G \ 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 \ G) ok H |] ==> F ok (G \ H)"
by (auto simp add: ok_def)
lemma ok_JOIN_iff1 [iff]: "F ok JOIN(I,G) \ (\i \ I. F ok G(i))"
by (force dest: Acts_type [THEN subsetD] elim!: not_emptyE simp add: ok_def)
lemma ok_JOIN_iff2 [iff]: "JOIN(I,G) ok F \ (\i \ I. G(i) ok F)"
apply (auto elim!: not_emptyE simp add: ok_def)
apply (blast dest: Acts_type [THEN subsetD])
done
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)
lemma OK_0 [iff]: "OK(0,F)"
by (simp add: OK_def)
lemma OK_cons_iff:
"OK(cons(i, I), F) \
(i \<in> I & OK(I, F)) | (i\<notin>I & OK(I, F) & F(i) ok JOIN(I,F))"
apply (simp add: OK_iff_ok)
apply (blast intro: ok_sym)
done
subsection\<open>Allowed\<close>
lemma Allowed_SKIP [simp]: "Allowed(SKIP) = program"
by (auto dest: Acts_type [THEN subsetD] simp add: Allowed_def)
lemma Allowed_Join [simp]:
"Allowed(F \ G) =
Allowed(programify(F)) \<inter> Allowed(programify(G))"
apply (auto simp add: Allowed_def)
done
lemma Allowed_JOIN [simp]:
"i \ I ==>
Allowed(JOIN(I,F)) = (\<Inter>i \<in> I. Allowed(programify(F(i))))"
apply (auto simp add: Allowed_def, blast)
done
lemma ok_iff_Allowed:
"F ok G \ (programify(F) \ Allowed(programify(G)) &
programify(G) \<in> Allowed(programify(F)))"
by (simp add: ok_def Allowed_def)
lemma OK_iff_Allowed:
"OK(I,F) \
(\<forall>i \<in> I. \<forall>j \<in> I-{i}. programify(F(i)) \<in> Allowed(programify(F(j))))"
apply (auto simp add: OK_iff_ok ok_iff_Allowed)
done
subsection\<open>safety_prop, for reasoning about given instances of "ok"\<close>
lemma safety_prop_Acts_iff:
"safety_prop(X) ==> (Acts(G) \ cons(id(state), (\F \ X. Acts(F)))) \ (programify(G) \ X)"
apply (simp (no_asm_use) add: safety_prop_def)
apply clarify
apply (case_tac "G \ program", simp_all, blast, safe)
prefer 2 apply force
apply (force simp add: programify_def)
done
lemma safety_prop_AllowedActs_iff_Allowed:
"safety_prop(X) ==>
(\<Union>G \<in> X. Acts(G)) \<subseteq> AllowedActs(F) \<longleftrightarrow> (X \<subseteq> Allowed(programify(F)))"
apply (simp add: Allowed_def safety_prop_Acts_iff [THEN iff_sym]
safety_prop_def, blast)
done
lemma Allowed_eq:
"safety_prop(X) ==> Allowed(mk_program(init, acts, \F \ X. Acts(F))) = X"
apply (subgoal_tac "cons (id (state), \(RepFun (X, Acts)) \ Pow (state * state)) = \(RepFun (X, Acts))")
apply (rule_tac [2] equalityI)
apply (simp del: UN_simps add: Allowed_def safety_prop_Acts_iff safety_prop_def, auto)
apply (force dest: Acts_type [THEN subsetD] simp add: safety_prop_def)+
done
lemma def_prg_Allowed:
"[| F == mk_program (init, acts, \F \ X. Acts(F)); safety_prop(X) |]
==> Allowed(F) = X"
by (simp add: Allowed_eq)
(*For safety_prop to hold, the property must be satisfiable!*)
lemma safety_prop_constrains [iff]:
"safety_prop(A co B) \ (A \ B & st_set(A))"
by (simp add: safety_prop_def constrains_def st_set_def, blast)
(* To be used with resolution *)
lemma safety_prop_constrainsI [iff]:
"[| A\B; st_set(A) |] ==>safety_prop(A co B)"
by auto
lemma safety_prop_stable [iff]: "safety_prop(stable(A)) \ st_set(A)"
by (simp add: stable_def)
lemma safety_prop_stableI: "st_set(A) ==> safety_prop(stable(A))"
by auto
lemma safety_prop_Int [simp]:
"[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X \ Y)"
apply (simp add: safety_prop_def, safe, blast)
apply (drule_tac [2] B = "\(RepFun (X \ Y, Acts))" and C = "\(RepFun (Y, Acts))" in subset_trans)
apply (drule_tac B = "\(RepFun (X \ Y, Acts))" and C = "\(RepFun (X, Acts))" in subset_trans)
apply blast+
done
(* If I=0 the conclusion becomes safety_prop(0) which is false *)
lemma safety_prop_Inter:
assumes major: "(!!i. i \ I ==>safety_prop(X(i)))"
and minor: "i \ I"
shows "safety_prop(\i \ I. X(i))"
apply (simp add: safety_prop_def)
apply (cut_tac minor, safe)
apply (simp (no_asm_use) add: Inter_iff)
apply clarify
apply (frule major)
apply (drule_tac [2] i = xa in major)
apply (frule_tac [4] i = xa in major)
apply (auto simp add: safety_prop_def)
apply (drule_tac B = "\(RepFun (\(RepFun (I, X)), Acts))" and C = "\(RepFun (X (xa), Acts))" in subset_trans)
apply blast+
done
lemma def_UNION_ok_iff:
"[| F == mk_program(init,acts, \G \ X. Acts(G)); safety_prop(X) |]
==> F ok G \<longleftrightarrow> (programify(G) \<in> X & acts \<inter> Pow(state*state) \<subseteq> AllowedActs(G))"
apply (unfold ok_def)
apply (drule_tac G = G in safety_prop_Acts_iff)
apply (cut_tac F = G in AllowedActs_type)
apply (cut_tac F = G in Acts_type, auto)
done
end
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
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.
|